`proc change` produces ill-formed goals when introducing new local variables (memory type)

[fdupress]

The following creates an ill-formed goal: the second subgoal of proc change displays a program that uses a local variable b in a memory that does not mention b.

Conversely (and less problematically), the first subgoal makes b appear in the memory type despite the fact that it should only appear in the right memory type.

require import AllCore.

module Toto = {
  proc titi() = {
    var boo: int;

    boo <- boo + 1;
    return boo;
  }
}.

equiv oops:
  Toto.titi ~ Toto.titi: true ==> ={res}.
proof.
proc.
proc change {1} 1: [ b: bool ] { b <- true; boo <- boo + 1; }.
(* left memory has useless b variable *)
+ by auto.
(* left memory has no b variable *)

[fdupress]

easycrypt/src/phl/ecPhlRewrite.ml

Lines 333 to 348 in 76bf9e9

	let goal1 =
	f_equivS
	(snd me) (snd me)
	{ ml; mr; inv = ofold f_and (f_ands pr_eq) frame; }
	(EcAst.stmt stmt) s
	{ ml; mr; inv = f_ands po_eq; }
	in
	let stmt = EcMatching.Zipper.zip { zpr with z_tail = s.s_node @ epilog } in
	(* Second subgoal: continue with the original goal after rewriting the
	selected statement range. *)
	let goal2 =
	EcLowPhlGoal.hl_set_stmt
	side (FApi.tc1_goal tc)
	stmt in

The first goal needs more care:

• If side is left, then the memories should be snd me and tc1_get_stmt other_side tc (where other_side is right).
• If side is right, then the memories should be tc1_get_stmt other_side tc and snd me (where other_side is left).

The second goal needs a lot more care. (The logic for memory selection should be the opposite of the above.