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.

[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.