fix byehoare

Author: namasikanam

src/phl/ecPhlDeno.ml

@@ -99,7 +99,7 @@ let t_ehoare_deno_r pre post tc =
 
   let pr = destr_pr f in
   let concl_e = f_eHoareF pre pr.pr_fun post in
-  let mpr, mpo = EcEnv.Fun.hoareF_memenv pr.pr_mem pr.pr_fun env in
+  let mpr, mpo = EcEnv.Fun.hoareF_memenv pre.m pr.pr_fun env in
   (* pre <= bd *)
   (* building the substitution for the pre *)
   let sargs = PVM.add env pv_arg (fst mpr) pr.pr_args PVM.empty in

tests/byehoare-arg.ec

@@ -0,0 +1,16 @@
+require import AllCore Int Real Xreal.
+
+module M = {
+  proc main(x : int) = {
+    return x; 
+  }
+}.
+
+lemma L &m (_x : int):
+  Pr [ M.main(_x) @ &m : _x = res ] <= 1%r.
+proof.
+byehoare (_: ((arg = _x) `|` (1%xr)) ==> _) => //.
+- proc; auto => &hr.
+  by apply xle_cxr_r => ->.
+qed.
+