ensure consistent memories

Author: oskgo

src/phl/ecPhlConseq.ml

@@ -191,6 +191,8 @@ let t_eagerF_conseq pre post tc =
 (* -------------------------------------------------------------------- *)
 let t_equivS_conseq pre post tc =
   let es = tc1_as_equivS tc in
+  let pre = ts_inv_rebind pre (fst es.es_ml) (fst es.es_mr) in
+  let post = ts_inv_rebind post (fst es.es_ml) (fst es.es_mr) in
   let cond1, cond2 = conseq_cond_ts (es_pr es) (es_po es) pre post in
   let concl1 = f_forall_mems_ts_inv es.es_ml es.es_mr cond1 in
   let concl2 = f_forall_mems_ts_inv es.es_ml es.es_mr cond2 in

src/phl/ecPhlEqobs.ml

@@ -435,22 +435,23 @@ let process_eqs env tc f =
          (EcPrinting.pp_form ppe) f.inv)
 
 (* -------------------------------------------------------------------- *)
-let process_hint tc hyps (feqs, inv) =
+let process_hint ml mr tc hyps (feqs, inv) =
   let env = LDecl.toenv hyps in
   let doinv pf = TTC.tc1_process_prhl_form tc tbool pf in
   let doeq pf = process_eqs env tc (doinv pf) in
   let dof g = omap (EcTyping.trans_gamepath env) g in
   let geqs =
     List.map (fun ((f1,f2),geq) -> dof f1, dof f2, doeq geq)
       feqs in
-  let ginv = odfl {ml=mleft;mr=mright;inv=f_true} (omap doinv inv) in
+  let ginv = odfl {ml;mr;inv=f_true} (omap doinv inv) in
   geqs, ginv
 
 (* -------------------------------------------------------------------- *)
 let process_eqobs_inS info tc =
   let env, hyps, _ = FApi.tc1_eflat tc in
   let es = tc1_as_equivS tc in
-  let spec, inv = process_hint tc hyps info.EcParsetree.sim_hint in
+  let ml, mr = fst es.es_ml, fst es.es_mr in
+  let spec, inv = process_hint ml mr tc hyps info.EcParsetree.sim_hint in
   let eqo =
     match info.EcParsetree.sim_eqs with
     | Some pf ->
@@ -492,7 +493,8 @@ let process_eqobs_inF info tc =
     tc_error !!tc "no positions excepted";
   let env, hyps, _ = FApi.tc1_eflat tc in
   let ef = tc1_as_equivF tc in
-  let spec, inv = process_hint tc hyps info.EcParsetree.sim_hint in
+  let ml, mr = ef.ef_ml, ef.ef_mr in
+  let spec, inv = process_hint ml mr tc hyps info.EcParsetree.sim_hint in
   let fl = ef.ef_fl and fr = ef.ef_fr in
   let eqo =
     match info.EcParsetree.sim_eqs with

src/phl/ecPhlLoopTx.ml

@@ -320,7 +320,7 @@ let process_unroll_for side cpos tc =
       let (h', pos', z') = oget hds.(i-1) in
       FApi.t_seqs [
         EcPhlWp.t_wp (Some (Single (Zpr.cpos (pos-2))));
-        EcPhlApp.t_hoare_app (Zpr.cpos (pos' - 1)) (map_ss_inv2 f_eq x {m;inv=f_int z'}) @+
+        EcPhlApp.t_hoare_app (Zpr.cpos (pos' - 1)) (map_ss_inv2 f_eq x {m=goal_m;inv=f_int z'}) @+
         [t_apply_hd h'; t_conseq_nm] ] tc
   in