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.

[strub]

Write a better commit message.

(explain what you actually fix. It is OK to have the commit message be the PR message. But "fix ehoare" is useless when you look at the history)

[strub]

@oskgo I incorporated your example, but it is not working. Is qed should be a abort?

[namasikanam]

@oskgo I incorporated your example, but it is not working. Is qed should be a abort?

@strub This is a counterexample, which should not be working. I'm not sure what's the best way to incorporate this example. Do we have other negative examples in tests?

[namasikanam]

@oskgo I incorporated your example, but it is not working. Is qed should be a abort?

@strub This is a counterexample, which should not be working. I'm not sure what's the best way to incorporate this example. Do we have other negative examples in tests?

I checked other negative examples and updated the example of @oskgo : explicitly mark the expected failure by fail and then abort.