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

[LucianoXu]

Summary

rewrite Pr [mu1_le_eq_mu1 d] is unsound when the value k in the event res = k depends on the post-execution memory. This PR adds the missing check flagged by the FIXME comments at ecPhlPrRw.ml:254-255.

Proof of false

The following EasyCrypt file proves false by exploiting this bug:

(* Bug: rewrite Pr [mu1_le_eq_mu1 d] does not check that k in
   res = k is memory-independent. When k = N.x (modified by proc),
   the event "res = N.x" uses N.x from the POST-state, but the
   rewritten formula "mu1 d N.x" treats it as a constant. *)

require import AllCore Distr DBool.

module N = {
  var x : bool
  proc f() : bool = {
    var r : bool;
    r <$ dbool;
    x <- r;
    return r;
  }
}.

lemma N_f_ll : islossless N.f.
proof. proc. auto. smt(dbool_ll). qed.

(* For any constant k, Pr[res = k] <= mu1 dbool k — sound *)
lemma N_f_mu1 &m k :
  Pr[N.f() @ &m : res = k] <= mu1 dbool k.
proof.
byphoare (_: true ==> _) => //.
proc. wp. rnd. skip. progress.
qed.

(* Fact 1: Pr[res = N.x] = 1 since x = res in the post-state *)
lemma pr_eq_one &m :
  Pr[N.f() @ &m : res = N.x] = 1%r.
proof.
have h1 : Pr[N.f() @ &m : res = N.x] >= 1%r.
  byphoare (_: true ==> res = N.x) => //.
  proc. wp. rnd. skip. auto. smt(dbool_ll).
have h2 : Pr[N.f() @ &m : res = N.x] <= 1%r by rewrite Pr[mu_le1].
smt().
qed.

(* Fact 2: BUG — rewrite Pr transforms Pr[res = N.x] to mu1 dbool N.x{dangling} = 1/2 *)
lemma pr_eq_half &m :
  Pr[N.f() @ &m : res = N.x] = 1%r / 2%r.
proof.
rewrite Pr [mu1_le_eq_mu1 dbool].
- exact N_f_ll.
- exact (N_f_mu1 &m).
rewrite dbool1E. auto.
qed.

(* Contradiction: 1 = 1/2 *)
lemma proof_of_false : false.
proof.
have : forall &m, false.
  move => &m.
  have h1 := pr_eq_one &m.
  have h2 := pr_eq_half &m.
  smt().
smt().
qed.

Before fix: easycrypt compile -no-eco novel_prrw_false.ec exits 0 (proves false).

After fix: exits 1 with error:

[critical] Pr-rewrite: the value compared to res must not depend on the post-execution memory

Root cause

The mu1_le_eq_mu1 rewrite transforms Pr[M.f() @ &m : res = k] into mu1 d k. This is sound when k is a constant (independent of the post-execution memory). But when k references a global variable modified by the procedure (e.g., N.x):

• The event res = N.x evaluates N.x in the post-state, where N.x = res always holds → probability 1
• The rewritten mu1 dbool N.x treats N.x as a constant (dangling memory reference) → 1/2
• Contradiction: 1 = 1/2

The source code already had FIXME comments at ecPhlPrRw.ml:254-255 acknowledging the missing checks.

Fix

Added checks that both k (the value compared to res) and d (the distribution) have free variables disjoint from the post-execution memory identifier. If either depends on the post-memory, a clear error is emitted.

Disclosure

This bug was discovered and this fix was authored with the assistance of Claude Code (Anthropic).

🤖 Generated with Claude Code

[Copilot]

Pull request overview

This PR addresses a soundness bug in the mu1_le_eq_mu1 probability rewrite: rewriting Pr[... : res = k] into mu1 d k is unsound when k depends on the post-execution memory.

Changes:

• Added a check rejecting rewrites where the compared value k depends on the post-execution memory.
• Added a similar post-memory dependency check for the distribution argument d, emitting clearer critical errors.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[Copilot]

The new distribution check only ensures d.inv is disjoint from the post-event memory id (k.m), but it does not enforce the original FIXME requirement that d.inv must not reference its own parsing memory (d.m, typically the fresh &hr created in t_pr_rewrite). If d.inv mentions d.m, the rewrite can still introduce a dangling/free memory identifier in mu1 d k, which is exactly what the old FIXME was warning about. Consider also checking Mid.set_disjoint d.inv.f_fv (Mid.singleton d.m ()) (or otherwise rebinding/quantifying d.m) in addition to (or instead of) the post-memory check.

[strub]

@oskgo The FIXME above is from you. Can you fix the memory?

[oskgo]

#932

[strub]

@LucianoXu

Thanks.

Here, the bug was already documented in the source code (don't ask me why). I think that we have a bunch of comments with FIXME like this. I suggest that you add this information to the prompt (i.e. "The EasyCrypt source code contains FIXME. Target them."). I can see more of them in the same file, and certainly in others.

[oskgo]

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.

[strub]

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

[oskgo]

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 *)