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 {γ : Type u_1} {s : Type u_2} {α : Type u_3} (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 {γ : Type u_1} {s : Type (max u v)} {α : Type v} {L : Lens γ s} (p : ProgramDenotation s α) : EquivModuloLens L p p

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

theorem GaudisCrypt.ProgramDenotation.EquivModuloLens.trans {γ : Type u_1} {s : Type (max u v)} {α : Type v} {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 {γ : Type u_1} {s : Type (max u v)} {α β : Type v} {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 {γ : Type u_1} {s : Type (max u v)} {α β : Type v} {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 {γ : Type u_1} {s : Type (max u v)} {α β : Type v} {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'.

The three set/pure () lemmas below mention no result type, so the section's s : Type (max u v) would leave v free and max ?u ?v =?= 1 unsolvable at a Type 1 state. They bind their own s : Type* instead.

theorem GaudisCrypt.ProgramDenotation.EquivModuloLens.set_equiv_pure {γ : Type u_1} {s : Type u_2} {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 {γ : Type u_1} {s : Type u_2} {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 {γ : Type u_1} {s : Type u_2} {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 {γ : Type u_1} {s : Type (max u v)} {α : Type v} {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 u_1} {γ : Type u_2} [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 u_1} {γ : Type u_2} [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.