Fixing the free memory of the second goal of byehoare

src/phl/ecPhlDeno.ml

@@ -86,6 +86,8 @@ let t_phoare_deno_r pre post tc =
 
 (* -------------------------------------------------------------------- *)
 let t_ehoare_deno_r pre post tc =
+  assert (pre.m = post.m);
+  let m = pre.m in
   let env, _, concl = FApi.tc1_eflat tc in
 
   let f, bd =
@@ -99,11 +101,11 @@ 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 _, mpo = EcEnv.Fun.hoareF_memenv 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
-  let smem = Fsubst.f_bind_mem Fsubst.f_subst_id (fst mpr) pr.pr_mem in
+  let sargs = PVM.add env pv_arg m pr.pr_args PVM.empty in
+  let smem = Fsubst.f_bind_mem Fsubst.f_subst_id m pr.pr_mem in
   let pre = Fsubst.f_subst smem (PVM.subst env sargs pre.inv) in
   let concl_pr = f_xreal_le pre (f_r2xr bd) in
 

tests/byehoare-arg.ec

@@ -0,0 +1,28 @@
+require import AllCore Int Real Xreal.
+
+module M = {
+  proc main_int(x : int) = {
+    return x; 
+  }
+
+  proc main_bool(x : bool) = {
+    return x; 
+  }
+}.
+
+lemma L &m (_x : int):
+  Pr [ M.main_int(_x) @ &m : _x = res ] <= 1%r.
+proof.
+byehoare (_: ((arg = _x) `|` (1%xr)) ==> _) => //.
+- proc; auto => &hr.
+  by apply xle_cxr_r => ->.
+qed.
+
+lemma L1 (&m: {arg: bool}): !arg{m} =>
+  Pr [ M.main_bool(true) @ &m : true] <= 0%r.
+proof.
+move => arg_eq.
+byehoare (_: (!arg{m})%xr ==> _).
++ proc; auto. by rewrite arg_eq.
+fail by auto.
+abort.