Fixing the free memory of the second goal of byehoare

[namasikanam]

The second goal generated from byehoare is unsound, in which the procedure arguments are bound in a free memory.

This is a small bug introduced in #789 . We need to bind the precondition to the memory in probability expression.

Thank @lyonel2017 for helping fix this bug.

[oskgo]

Nice catch.

There's still a bug though:

require import Real Xreal.

module M = {
  proc main(x : bool) = {
    return x; 
  }
}.

lemma L1 (&m: {arg: bool}): !arg{m} =>
  Pr [ M.main(true) @ &m : true] <= 0%r.
proof.
move => arg_eq.
byehoare (_: (!arg{m})%xr ==> _) => //.
proc; auto. by rewrite arg_eq.
qed.