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

Merged
strub merged 3 commits into from
Mar 20, 2026
+21 −7
Merged

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

Changes from all commits
Commits
Show all changes
3 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
1161596
Filter Prs with non-constant rhs already during selection
oskgo Mar 17, 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
28 changes: 21 additions & 7 deletions src/phl/ecPhlPrRw.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand All @@ -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

Expand Down Expand Up @@ -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)
Expand All @@ -251,8 +258,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
Expand Down
Loading