From 949fb654b084074a37b686a013d7b835bdcbf174 Mon Sep 17 00:00:00 2001 From: Yingte Xu Date: Tue, 10 Mar 2026 09:27:12 +0100 Subject: [PATCH 1/3] Add checks to ensure post-execution memory independence in pr-rewrite --- src/phl/ecPhlPrRw.ml | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) diff --git a/src/phl/ecPhlPrRw.ml b/src/phl/ecPhlPrRw.ml index 0ce2bab37a..72a2606bf6 100644 --- a/src/phl/ecPhlPrRw.ml +++ b/src/phl/ecPhlPrRw.ml @@ -251,8 +251,18 @@ 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. *) + let post_mem = Mid.singleton k.m () in + if not (Mid.set_disjoint k.inv.f_fv post_mem) then + tc_error !!tc + "Pr-rewrite: the value compared to res must not depend on \ + the post-execution memory"; + if not (Mid.set_disjoint d.inv.f_fv post_mem) then + tc_error !!tc + "Pr-rewrite: the distribution must not depend on \ + the post-execution memory"; (pr_mu1_le_eq_mu1 pr_mem pr_fun pr_args resv k.inv k_id d.inv, 2) | (`MuEq | `MuSub as kind) -> begin From eff407e045b32430c2e4e864c890568f10bd93ea Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Tue, 10 Mar 2026 10:32:20 +0100 Subject: [PATCH 2/3] Fix error msg + used memory --- src/phl/ecPhlPrRw.ml | 11 ++++------- 1 file changed, 4 insertions(+), 7 deletions(-) diff --git a/src/phl/ecPhlPrRw.ml b/src/phl/ecPhlPrRw.ml index 72a2606bf6..090ad3fa0e 100644 --- a/src/phl/ecPhlPrRw.ml +++ b/src/phl/ecPhlPrRw.ml @@ -254,15 +254,12 @@ let t_pr_rewrite_low (s, (dof: (_ -> _ -> _ -> ss_inv) option)) tc = (* 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. *) - let post_mem = Mid.singleton k.m () in - if not (Mid.set_disjoint k.inv.f_fv post_mem) then + if Mid.mem k.m k.inv.f_fv then tc_error !!tc - "Pr-rewrite: the value compared to res must not depend on \ - the post-execution memory"; - if not (Mid.set_disjoint d.inv.f_fv post_mem) then + "Pr-rewrite: the value compared to res must not depend on memories"; + if Mid.mem d.m d.inv.f_fv then tc_error !!tc - "Pr-rewrite: the distribution must not depend on \ - the post-execution memory"; + "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 From 11615960210d08a825266fc3d4f25b074c652b35 Mon Sep 17 00:00:00 2001 From: oskgo <92018610+oskgo@users.noreply.github.com> Date: Tue, 17 Mar 2026 12:33:38 +0100 Subject: [PATCH 3/3] Filter Prs with non-constant rhs already during selection --- src/phl/ecPhlPrRw.ml | 21 ++++++++++++++------- 1 file changed, 14 insertions(+), 7 deletions(-) diff --git a/src/phl/ecPhlPrRw.ml b/src/phl/ecPhlPrRw.ml index 090ad3fa0e..72c8f04685 100644 --- a/src/phl/ecPhlPrRw.ml +++ b/src/phl/ecPhlPrRw.ml @@ -117,6 +117,13 @@ let destr_pr_has pr = Some(ty_elem, {m;inv=f_f}, {m;inv=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. @@ -141,7 +148,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 @@ -223,13 +230,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) @@ -255,8 +262,8 @@ let t_pr_rewrite_low (s, (dof: (_ -> _ -> _ -> ss_inv) option)) tc = 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 - tc_error !!tc - "Pr-rewrite: the value compared to res must not depend on memories"; + (* 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";