Skip to content

Fix rewrite Pr [mu1_le_eq_mu1]: add missing memory-independence check #930

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
LucianoXu wants to merge 2 commits into
base: main
Choose a base branch
from
+9 −2
Open

Fix rewrite Pr [mu1_le_eq_mu1]: add missing memory-independence check #930

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
949fb65
Add checks to ensure post-execution memory independence in pr-rewrite
LucianoXu Mar 10, 2026
eff407e
Fix error msg + used memory
strub Mar 10, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 9 additions & 2 deletions src/phl/ecPhlPrRw.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -251,8 +251,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
tc_error !!tc
Copy link
Contributor

@oskgo oskgo Mar 10, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The existing rewrite Pr machinery is designed to be able to handle goals with multiple Pr formulas. For this to work successful selection has to mean that the selected rewrite is safe to apply, otherwise you might error out before finding the right Pr to apply.

We should check for memory dependence during selection as well. This makes these errors moot but allows rewrites on formulas like Pr[N.f() @ &m : res = N.x] = Pr[N.f() @ &m : res = true], which are not allowed by this PR.

I think there's a bigger discussion to be had about how to better expose matching/selection failures to the user (in regular rewrite as well), but this is not an easy problem to solve.

Copy link
Member

@strub strub Mar 10, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The matching algorithm is already able to do that. Maybe should we add a way to start from a non empty set of variables.

Copy link
Contributor

@oskgo oskgo Mar 10, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Are you commenting on the third paragraph?

In care you are commenting on first or second, consider this example:

require import DBool.

module N = {
   var x: bool
   proc f() ={return true;}
}.

lemma L1 &m: Pr[N.f() @ &m : res = true] = Pr[N.f() @ &m : res = N.x].
rewrite Pr[mu1_le_eq_mu1 dbool]. (* succeds at rewriting left side *)
abort.

lemma L2 &m: Pr[N.f() @ &m : res = N.x] = Pr[N.f() @ &m : res = true].
pose p:=Pr[N.f() @ &m : res = N.x].
rewrite Pr[mu1_le_eq_mu1 dbool]. (* succeeds at rewriting right side *)
abort.

lemma L3 &m: Pr[N.f() @ &m : res = N.x] = Pr[N.f() @ &m : res = true].
rewrite Pr[mu1_le_eq_mu1 dbool]. (* tries rewriting the left side and errors *)

"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 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
Expand Down
Loading