Merge branch 'main' into eHoare-example

Author: fdupress

src/phl/ecPhlPrRw.ml

@@ -117,6 +117,13 @@ let destr_pr_has pr =
         Some(ty_elem, {m;inv=f_f}, f_l)
       else None
   | _ -> None
+
+let is_eq_w_const_rhs (f: ss_inv): bool =
+  try 
+    let _, rhs = destr_eq f.inv in
+    not (Mid.mem f.m rhs.f_fv)
+  with DestrError _ -> false
+
 (*
  lemma mu_has_le ['a 'b] (P : 'a -> 'b -> bool) (d : 'a distr) (s : 'b list) :
    mu d (fun a => has (P a) s) <= BRA.big predT (fun b => mu d (fun a => P a b)) s.
@@ -140,7 +147,7 @@ exception FoundPr of form
 let select_pr on_ev sid f =
   match f.f_node with
   | Fpr { pr_event = ev } ->
-      if on_ev ev.inv && Mid.set_disjoint f.f_fv sid then raise (FoundPr f)
+      if on_ev ev && Mid.set_disjoint f.f_fv sid then raise (FoundPr f)
       else false
   | _ -> false
 
@@ -222,13 +229,13 @@ let t_pr_rewrite_low (s, (dof: (_ -> _ -> _ -> ss_inv) option)) tc =
 
   let select =
     match kind with
-    | `Mu1LeEqMu1 -> select_pr is_eq
-    | `MuDisj | `MuOr -> select_pr is_or
+    | `Mu1LeEqMu1 -> select_pr is_eq_w_const_rhs
+    | `MuDisj | `MuOr -> select_pr (fun inv -> is_or inv.inv)
     | `MuEq -> select_pr_cmp (EcPath.p_equal EcCoreLib.CI_Bool.p_eq)
-    | `MuFalse -> select_pr is_false
+    | `MuFalse -> select_pr (fun inv -> is_false inv.inv)
     | `MuGe0 -> select_pr_ge0
     | `MuLe1 -> select_pr_le1
-    | `MuNot -> select_pr is_not
+    | `MuNot -> select_pr (fun inv -> is_not inv.inv)
     | `MuSplit -> select_pr (fun _ev -> true)
     | `MuSub -> select_pr_cmp (EcPath.p_equal EcCoreLib.CI_Real.p_real_le)
     | `MuSum -> select_pr (fun _ev -> true)
@@ -250,8 +257,15 @@ let t_pr_rewrite_low (s, (dof: (_ -> _ -> _ -> ss_inv) option)) tc =
       let (resv, k) = map_ss_inv_destr2 destr_eq pr.pr_event in
       let k_id = EcEnv.LDecl.fresh_id hyps "k" in
       let d = (oget dof) tc torw (EcTypes.tdistr k.inv.f_ty) in
-      (* FIXME: Ensure that d.inv does not use d.m *)
-      (* FIXME: Ensure that k.inv does not use k.m *)
+      (* Check that k and d do not reference the post-execution memory.
+         Otherwise the rewrite is unsound: the event `res = k` would use
+         k from the post-state, but `mu1 d k` treats k as a constant. *)
+      if Mid.mem k.m k.inv.f_fv then
+        (* This case should already be filtered by selection *)
+        assert false;
+      if Mid.mem d.m d.inv.f_fv then
+        tc_error !!tc
+          "Pr-rewrite: the distribution must not depend on memories";
       (pr_mu1_le_eq_mu1 pr_mem pr_fun pr_args resv k.inv k_id d.inv, 2)
 
     | (`MuEq | `MuSub as kind) -> begin