`eager call` unsound if the trailing statement writes or reads the right result

[Yiping106283]

eager call reduces S; x <@ f(a) ~ x' <@ f'(a'); S' : P ==> Q to the eager premise S, f ~ f', S' plus a wp. On the right, x' := res is executed before S', but the eager premise relates memories after f'; S' with the result not stored, and the only side condition checked is that S does not write the left arguments. If S' writes x', the wp still substitutes x'{2} := res (the substitution happens before generalizing over write(S')); if S' reads x', the premise was proved for an S' that saw the pre-call value. Both cases prove a false equiv.

MRE (write case):

require import AllCore.
module M = { var r : int  proc f() : int = { return 1; } }.
lemma eg : eager[M.r <- 0;, M.f ~ M.f, M.r <- 0; : true ==> res{1} = 1 /\ res{2} = 1].
proof. by eager proc; auto. qed.
module G = {
  proc left()  : int = { M.r <- 0; M.r <@ M.f(); return M.r; }   (* returns 1 *)
  proc right() : int = { M.r <@ M.f(); M.r <- 0; return M.r; }   (* returns 0 *)
}.
lemma eqv : equiv[G.left ~ G.right : true ==> res{1} = res{2}].   (* FALSE *)
proof. proc. eager call eg. by auto. qed.
lemma bad &m : false.
proof.
have h1 : Pr[G.left() @ &m : res = 1] = 1%r by byphoare => //; proc; inline *; auto.
have h2 : Pr[G.right() @ &m : res = 1] = 0%r by byphoare => //; hoare; proc; inline *; auto.
have h3 : Pr[G.left() @ &m : res = 1] = Pr[G.right() @ &m : res = 1] by byequiv eqv.
smt().
qed.

Read case: replace M.r <- 0 by a call M.cp() with proc cp() = { M.t <- M.r; } and return M.t (left returns the old M.r, right returns 1); eager call eg; auto is accepted the same way and false follows through a wrapper that sets M.r <- 0.

Root cause: src/phl/ecPhlEager.ml, t_eager_call_r (l. 395-428) only runs check_a on the left arguments and calls EcPhlCall.compute_equiv_call_post ~mods:(swl, swr) (src/phl/ecPhlCall.ml:78-133), which applies wp_asgn_call for the right lvalue (l. 107) before generalize_mod_ts_inv over write(S') ∪ write(f') (l. 119). Missing side condition: the right lvalue must be disjoint from read(S') ∪ write(S') (reordering the substitution and the generalization would only fix the write case).