fix alpha-conversion problems in ehoare

Author: bgregoir

src/phl/ecPhlApp.ml

@@ -26,12 +26,13 @@ let t_hoare_app_r i phi tc =
 let t_hoare_app = FApi.t_low2 "hoare-app" t_hoare_app_r
 
 (* -------------------------------------------------------------------- *)
-let t_ehoare_app_r i f tc =
+let t_ehoare_app_r i phi tc =
   let env = FApi.tc1_env tc in
   let hs = tc1_as_ehoareS tc in
   let s1, s2 = s_split env i hs.ehs_s in
-  let a = f_eHoareS (snd hs.ehs_m) (ehs_pr hs) (stmt s1) f in
-  let b = f_eHoareS (snd hs.ehs_m) f (stmt s2) (ehs_po hs) in
+  let phi = ss_inv_rebind phi (fst hs.ehs_m) in
+  let a = f_eHoareS (snd hs.ehs_m) (ehs_pr hs) (stmt s1) phi in
+  let b = f_eHoareS (snd hs.ehs_m) phi (stmt s2) (ehs_po hs) in
   FApi.xmutate1 tc `HlApp [a; b]
 
 let t_ehoare_app = FApi.t_low2 "hoare-app" t_ehoare_app_r
@@ -124,11 +125,11 @@ let t_equiv_app_onesided side i pre post tc =
   let (ml, mr) = fst es.es_ml, fst es.es_mr in
   let s, s', p', q' =
     match side with
-    | `Left  -> 
+    | `Left  ->
       let p' = ss_inv_generalize_as_left pre ml mr in
       let q' = ss_inv_generalize_as_left post ml mr in
       es.es_sl, es.es_sr, p', q'
-    | `Right -> 
+    | `Right ->
       let p' = ss_inv_generalize_as_right pre ml mr in
       let q' = ss_inv_generalize_as_right post ml mr in
       es.es_sr, es.es_sl, p', q'

src/phl/ecPhlConseq.ml

@@ -39,11 +39,11 @@ let bd_goal_r fcmp fbd cmp bd =
   | FHle, (FHle | FHeq) -> Some (map_ss_inv2 f_real_le bd fbd)
   | FHge, (FHge | FHeq) -> Some (map_ss_inv2 f_real_le fbd bd)
   | FHeq, FHeq          -> Some (map_ss_inv2 f_eq bd fbd)
-  | FHeq, FHge          -> Some (map_ss_inv2 f_and 
-          (map_ss_inv1 ((EcUtils.flip f_eq) f_r1) fbd) 
+  | FHeq, FHge          -> Some (map_ss_inv2 f_and
+          (map_ss_inv1 ((EcUtils.flip f_eq) f_r1) fbd)
           (map_ss_inv1 ((EcUtils.flip f_eq) f_r1) bd))
-  | FHeq, FHle          -> Some (map_ss_inv2 f_and 
-          (map_ss_inv1 ((EcUtils.flip f_eq) f_r0) fbd) 
+  | FHeq, FHle          -> Some (map_ss_inv2 f_and
+          (map_ss_inv1 ((EcUtils.flip f_eq) f_r0) fbd)
           (map_ss_inv1 ((EcUtils.flip f_eq) f_r0) bd))
   | _   , _             -> None
 
@@ -453,6 +453,9 @@ let t_bdHoareS_conseq_nm = gen_conseq_nm t_bdHoareS_notmod t_bdHoareS_conseq
 let t_ehoareF_concave (fc: ss_inv) pre post tc =
   let env = FApi.tc1_env tc in
   let hf = tc1_as_ehoareF tc in
+  let pre = ss_inv_rebind pre hf.ehf_m in
+  let post = ss_inv_rebind post hf.ehf_m in
+  let fc = ss_inv_rebind fc hf.ehf_m in
   let f = hf.ehf_f in
   let mpr,mpo = Fun.hoareF_memenv hf.ehf_m f env in
   let fsig = (Fun.by_xpath f env).f_sig in
@@ -491,6 +494,9 @@ let t_ehoareS_concave (fc: ss_inv) (* xreal -> xreal *) pre post tc =
   let hs = tc1_as_ehoareS tc in
   let s = hs.ehs_s in
   let m = fst hs.ehs_m in
+  let pre = ss_inv_rebind pre m in
+  let post = ss_inv_rebind post m in
+  let fc = ss_inv_rebind fc m in
   (* ensure that f only depend of notmod *)
   let modi = s_write env s in
   let fv = PV.fv env m fc.inv in
@@ -614,7 +620,7 @@ let process_concave ((info, fc) : pformula option tuple2 gppterm * pformula) tc
 
     let pre   = map_ss_inv1 (fun gpre -> pre |> omap (TTC.pf_process_form !!tc penv txreal) |> odfl gpre) gpre  in
     let post  = map_ss_inv1 (fun gpost -> post |> omap (TTC.pf_process_form !!tc qenv txreal) |> odfl gpost) gpost in
-    
+
     fmake pre post
 
   in
@@ -665,9 +671,9 @@ let t_hoareS_conseq_conj pre post pre' post' tc =
   let hs = tc1_as_hoareS tc in
   let pre'' = map_ss_inv2 f_and pre' pre in
   let post'' = map_ss_inv2 f_and post' post in
-  if not (ss_inv_alpha_eq hyps (hs_pr hs) pre'') 
+  if not (ss_inv_alpha_eq hyps (hs_pr hs) pre'')
     then tc_error !!tc "invalid pre-condition";
-  if not (ss_inv_alpha_eq hyps (hs_po hs) post'') 
+  if not (ss_inv_alpha_eq hyps (hs_po hs) post'')
     then tc_error !!tc "invalid post-condition";
   let concl1 = f_hoareS (snd hs.hs_m) pre hs.hs_s post in
   let concl2 = f_hoareS (snd hs.hs_m) pre' hs.hs_s post' in
@@ -679,7 +685,7 @@ let t_hoareF_conseq_conj pre post pre' post' tc =
   let hf = tc1_as_hoareF tc in
   let pre'' = map_ss_inv2 f_and pre' pre in
   let post'' = map_ss_inv2 f_and post' post in
-  if not (ss_inv_alpha_eq hyps (hf_pr hf) pre'') 
+  if not (ss_inv_alpha_eq hyps (hf_pr hf) pre'')
   then tc_error !!tc "invalid pre-condition";
   if not (ss_inv_alpha_eq hyps (hf_po hf) post'')
   then tc_error !!tc "invalid post-condition";
@@ -696,7 +702,7 @@ let t_bdHoareS_conseq_conj ~add post post' tc =
   if not (ss_inv_alpha_eq hyps (bhs_po hs) postc) then
     tc_error !!tc "invalid post-condition";
   let concl1 = f_hoareS (snd hs.bhs_m) (bhs_pr hs) hs.bhs_s post in
-  let concl2 = f_bdHoareS (snd hs.bhs_m) (bhs_pr hs) hs.bhs_s posth 
+  let concl2 = f_bdHoareS (snd hs.bhs_m) (bhs_pr hs) hs.bhs_s posth
                  hs.bhs_cmp (bhs_bd hs) in
   FApi.xmutate1 tc `HlConseqBd [concl1; concl2]
 
@@ -765,7 +771,7 @@ let t_equivS_conseq_bd side pr po tc =
       let pos = ss_inv_generalize_as_left po ml mr in
       let prs = ss_inv_generalize_as_left pr ml mr in
       es.es_ml, es.es_sl, es.es_sr, prs, pos
-    | `Right -> 
+    | `Right ->
       let pos = ss_inv_generalize_as_right po ml mr in
       let prs = ss_inv_generalize_as_right pr ml mr in
       es.es_mr, es.es_sr, es.es_sl, prs, pos
@@ -921,7 +927,7 @@ let rec t_hi_conseq notmod f1 f2 f3 tc =
     let tac = if notmod then t_hoareS_conseq_nm else t_hoareS_conseq in
 
     t_on1seq 2
-      (tac (map_ss_inv2 f_and (hs_pr hs) (hs_pr hs2)) 
+      (tac (map_ss_inv2 f_and (hs_pr hs) (hs_pr hs2))
             (map_ss_inv2 f_and (hs_po hs) (hs_po hs2)))
       (FApi.t_seqsub
          (t_hoareS_conseq_conj (hs_pr hs2) (hs_po hs2) (hs_pr hs) (hs_po hs))
@@ -962,7 +968,7 @@ let rec t_hi_conseq notmod f1 f2 f3 tc =
     let po2 = ss_inv_rebind (hf_po hs2) hf.hf_m in
     (* check that the pre- and post-conditions are well formed *)
     t_on1seq 2
-      ((tac (map_ss_inv2 f_and pr1 pr2) 
+      ((tac (map_ss_inv2 f_and pr1 pr2)
            (map_ss_inv2 f_and po1 po2)))
       (FApi.t_seqsub
          (t_hoareF_conseq_conj pr2 po2 pr1 po1)
@@ -1162,7 +1168,7 @@ let rec t_hi_conseq notmod f1 f2 f3 tc =
     Some ((_, {f_node = FequivF ef}) as nef), Some((_, f2) as nf2), _ ->
     let hf2 = pf_as_bdhoareF !!tc f2 in
     FApi.t_seqsub
-      (t_bdHoareF_conseq_equiv hf2.bhf_f (ef_pr ef) (ef_po ef) 
+      (t_bdHoareF_conseq_equiv hf2.bhf_f (ef_pr ef) (ef_po ef)
                                          (bhf_pr hf2) (bhf_po hf2) (bhf_bd hf2))
       [t_id; t_id; t_apply_r nef; t_apply_r nf2] tc
 
@@ -1467,7 +1473,7 @@ let process_conseq notmod ((info1, info2, info3) : conseq_ppterm option tuple3)
         let f, pr, po = match f1 with
         | None -> hf.hf_f, hf_pr hf, hf_po hf
         | Some f1 -> match (snd f1).f_node with
-                     | FequivF ef when side = `Left -> 
+                     | FequivF ef when side = `Left ->
                       ef.ef_fr, {m; inv=f_true}, {m; inv=f_true}
                      | _ -> hf.hf_f, hf_pr hf, hf_po hf
         in
@@ -1482,7 +1488,7 @@ let process_conseq notmod ((info1, info2, info3) : conseq_ppterm option tuple3)
         | Some f1 -> match (snd f1).f_node with
                      | FequivF ef when side = `Left ->
                          let f_xreal_1 = f_r2xr f_r1 in
-                         ef.ef_fr, {m=ef.ef_mr; inv=f_xreal_1}, 
+                         ef.ef_fr, {m=ef.ef_mr; inv=f_xreal_1},
                           {m=ef.ef_mr; inv=f_xreal_1}, ef.ef_mr
                      | _ -> hf.ehf_f, ehf_pr hf, ehf_po hf, hf.ehf_m
         in
@@ -1502,7 +1508,7 @@ let process_conseq notmod ((info1, info2, info3) : conseq_ppterm option tuple3)
         let f, pr, po, m = match f1 with
         | None -> bhf.bhf_f, bhf_pr bhf, bhf_po bhf, bhf.bhf_m
         | Some f1 -> match (snd f1).f_node with
-                     | FequivF ef when side = `Left -> ef.ef_fr, 
+                     | FequivF ef when side = `Left -> ef.ef_fr,
                         {m=ef.ef_mr;inv=f_true}, {m=ef.ef_mr;inv=f_true}, ef.ef_mr
                      | _ -> bhf.bhf_f, bhf_pr bhf, bhf_po bhf, bhf.bhf_m
         in

src/phl/ecPhlDeno.ml

@@ -86,8 +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
+  assert (m = post.m);
   let env, _, concl = FApi.tc1_eflat tc in
 
   let f, bd =
@@ -111,6 +111,7 @@ let t_ehoare_deno_r pre post tc =
 
   (* forall m, ev%r%xr <= post *)
   let ev = pr.pr_event in
+  let ev = ss_inv_rebind ev m in
   let concl_po = map_ss_inv2 f_xreal_le (map_ss_inv1 f_b2xr ev) post in
   let concl_po = f_forall_mems_ss_inv mpo concl_po in