From 949fb654b084074a37b686a013d7b835bdcbf174 Mon Sep 17 00:00:00 2001 From: Yingte Xu Date: Tue, 10 Mar 2026 09:27:12 +0100 Subject: [PATCH 1/2] 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/2] 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