Equivalence-modulo-lens calculus

We define a relation ProgramDenotation.EquivModuloLens L p q capturing "p and q have equal wps on any post that doesn't read lens L".

This packages the recurring pattern in cryptographic game-hopping where two games differ only by writes to an auxiliary tracking variable, and those writes are invisible at the wp level for posts ignoring the tracking variable.

The calculus has closure rules (reflexivity, symmetry, transitivity, bind congruence) and base instances (e.g. pure () ≈ set L v for any lens L, value v). Tracking-flag elision proofs reduce to short chains of these rules.

def GaudisCrypt.ProgramDenotation.EquivModuloLens {γ s α : Type} (L : Lens γ s) (p q : ProgramDenotation s α) : Prop

ProgramDenotation.EquivModuloLens L p q — p and q have equal wps on any L-ignoring post.

Equations

• GaudisCrypt.ProgramDenotation.EquivModuloLens L p q = ∀ (F : α × s → ENNReal), GaudisCrypt.IgnoresLens L F → ∀ (σ : s), p.wp F σ = q.wp F σ

theorem GaudisCrypt.ProgramDenotation.EquivModuloLens.refl {γ s α : Type} {L : Lens γ s} (p : ProgramDenotation s α) : EquivModuloLens L p p

theorem GaudisCrypt.ProgramDenotation.EquivModuloLens.symm {γ s α : Type} {L : Lens γ s} {p q : ProgramDenotation s α} (h : EquivModuloLens L p q) : EquivModuloLens L q p

theorem GaudisCrypt.ProgramDenotation.EquivModuloLens.trans {γ s α : Type} {L : Lens γ s} {p q r : ProgramDenotation s α} (h1 : EquivModuloLens L p q) (h2 : EquivModuloLens L q r) : EquivModuloLens L p r

theorem GaudisCrypt.ProgramDenotation.EquivModuloLens.bind_eq_k {γ s α β : Type} {L : Lens γ s} [DecidableEq γ] {p p' : ProgramDenotation s α} {k : α → ProgramDenotation s β} (h_p : EquivModuloLens L p p') (h_k : ∀ (a : α), (k a).inFootprint L.footprintᶜ) : EquivModuloLens L (p >>= k) (p' >>= k)

Bind with the SAME L-disjoint continuation on both sides: if p ≈_L p' and k doesn't touch L, then p >>= k ≈_L p' >>= k.

theorem GaudisCrypt.ProgramDenotation.EquivModuloLens.bind_eq_p {γ s α β : Type} {L : Lens γ s} {p : ProgramDenotation s α} {k k' : α → ProgramDenotation s β} (h_k : ∀ (a : α), EquivModuloLens L (k a) (k' a)) : EquivModuloLens L (p >>= k) (p >>= k')

Bind with the SAME prefix and equivalent continuations: if ∀ a, k a ≈_L k' a, then p >>= k ≈_L p >>= k'.

theorem GaudisCrypt.ProgramDenotation.EquivModuloLens.bind {γ s α β : Type} {L : Lens γ s} [DecidableEq γ] {p p' : ProgramDenotation s α} {k k' : α → ProgramDenotation s β} (h_p : EquivModuloLens L p p') (h_k : ∀ (a : α), EquivModuloLens L (k a) (k' a)) (h_k_inFootprint : ∀ (a : α), (k a).inFootprint L.footprintᶜ) : EquivModuloLens L (p >>= k) (p' >>= k')

Full bind congruence: p ≈_L p' AND ∀ a, k a ≈_L k' a AND k is L-disjoint (per element) → p >>= k ≈_L p' >>= k'.

theorem GaudisCrypt.ProgramDenotation.EquivModuloLens.set_equiv_pure {γ s : Type} {L : Lens γ s} (v : γ) : EquivModuloLens L (set L v) (pure ())

A set L v is equivalent (modulo L) to pure ().

theorem GaudisCrypt.ProgramDenotation.EquivModuloLens.pure_equiv_set {γ s : Type} {L : Lens γ s} (v : γ) : EquivModuloLens L (pure ()) (set L v)

pure () is equivalent (modulo L) to set L v (symmetric form).

theorem GaudisCrypt.ProgramDenotation.EquivModuloLens.cond_set_equiv_pure {γ s : Type} {L : Lens γ s} (cond : Prop) [Decidable cond] (v : γ) : EquivModuloLens L (if cond then set L v else pure ()) (pure ())

A conditional set L v is equivalent to pure ().

theorem GaudisCrypt.ProgramDenotation.EquivModuloLens.wp_eq {γ s α : Type} {L : Lens γ s} {p q : ProgramDenotation s α} (h : EquivModuloLens L p q) (F : α × s → ENNReal) (h_F : IgnoresLens L F) (σ : s) : p.wp F σ = q.wp F σ

Transfer to wp: if p ≈_L q and F is L-ignoring, then their wps agree.

theorem GaudisCrypt.loop_n_congr {s γ : Type} [DecidableEq γ] {L : Lens γ s} {body body' : ProgramDenotation s Unit} (h_body : body.inFootprint L.footprintᶜ) (h_eq : ProgramDenotation.EquivModuloLens L body body') (n : ℕ) : ProgramDenotation.EquivModuloLens L (loop_n n body) (loop_n n body')

Loop congruence for the equiv-modulo-lens calculus: if two bodies are ≈_L-equivalent, so are their loop_n iterates. Requires the reference body body to be L-disjoint so that loop_n n body is also L-disjoint (needed by the bind congruence in the inductive step).

theorem GaudisCrypt.loop_n_then_congr {s γ : Type} [DecidableEq γ] {L : Lens γ s} {body body' final final' : ProgramDenotation s Unit} (h_body : body.inFootprint L.footprintᶜ) (h_body_eq : ProgramDenotation.EquivModuloLens L body body') (h_final : final.inFootprint L.footprintᶜ) (h_final_eq : ProgramDenotation.EquivModuloLens L final final') (n : ℕ) : ProgramDenotation.EquivModuloLens L (do loop_n n body final) do loop_n n body' final'

Loop + trailing congruence: if body ≈_L body' and final ≈_L final', with both body and final being L-disjoint, then loop_n n body >>= final ≈_L loop_n n body' >>= final'.

Combines loop_n_congr and ProgramDenotation.EquivModuloLens.bind in one step.