fix byehoare

Author: namasikanam

src/phl/ecPhlDeno.ml

@@ -104,6 +104,7 @@ let t_ehoare_deno_r pre post tc =
   (* 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 pre = ss_inv_rebind pre 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,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.
+