pRHL lens rules: self-shift, framing, and the EquivModuloLens bridge

These are the rules that interact with the lens-based memory model:

• ProgramDenotation.rel.self_shift / ProgramDenotation.relE.self_lens_set — relate a program to itself from two starting states that differ by an update outside its footprint (the relational packaging of ProgramDenotation.wp_shift_input_prob). This is the rule every client involving an abstract adversary needs.
• ProgramDenotation.rel.frame — strengthen a judgment with value constraints on lenses outside each side's footprint (the relational packaging of ProgramDenotation.wp_strengthen_lens_preserved_footprint).
• ProgramDenotation.EquivModuloLens.to_relE / ProgramDenotation.relE.to_equivModuloLens — EquivModuloLens L p q is exactly the diagonal relE whose post relates pairs with equal results and equal L-complement content. The existing EquivModuloLens calculus remains the ergonomic API for the diagonal case; this bridge lets its lemmas feed rel chains and vice versa.

theorem GaudisCrypt.ProgramDenotation.rel.self_shift {s α : Type} {p : ProgramDenotation s α} {R : Footprint s} (hp : p.inFootprint R) {f : s → s} (hf : diracKer f ∈ Rᶜ.updates) : p.rel p (fun (σ₁ σ₂ : s) => σ₂ = f σ₁) fun (x y : α × s) => y.1 = x.1 ∧ y.2 = f x.2

Self-shift: running p from f σ (for f outside p's footprint) relates to running p from σ with the shift carried into the post.

theorem GaudisCrypt.ProgramDenotation.rel.frame {s₁ s₂ α β γ₁ γ₂ : Type} (L : Lens γ₁ s₁) (M : Lens γ₂ s₂) {p : ProgramDenotation s₁ α} {q : ProgramDenotation s₂ β} (hp : p.inFootprint L.footprintᶜ) (hq : q.inFootprint M.footprintᶜ) {Pre : s₁ → s₂ → Prop} {Post : α × s₁ → β × s₂ → Prop} (h : p.rel q Pre Post) (v : γ₁) (w : γ₂) : p.rel q (fun (σ₁ : s₁) (σ₂ : s₂) => Pre σ₁ σ₂ ∧ L.get σ₁ = v ∧ M.get σ₂ = w) fun (x : α × s₁) (y : β × s₂) => Post x y ∧ L.get x.2 = v ∧ M.get y.2 = w

Framing: a judgment can be strengthened with value constraints on a lens outside each side's footprint. The proof strengthens the left post with the L-frame (wp_strengthen_lens_preserved_footprint) and interpolates the right post with a ⊤-override off the M-frame.

theorem GaudisCrypt.ProgramDenotation.relE.self_shift {s α : Type} {p : ProgramDenotation s α} {R : Footprint s} (hp : p.inFootprint R) {f : s → s} (hf : diracKer f ∈ Rᶜ.updates) : p.relE p (fun (σ₁ σ₂ : s) => σ₂ = f σ₁) fun (x y : α × s) => y.1 = x.1 ∧ y.2 = f x.2

Two-sided form of ProgramDenotation.rel.self_shift.

theorem GaudisCrypt.ProgramDenotation.relE.self_lens_set {s α γ : Type} {p : ProgramDenotation s α} (L : Lens γ s) (hp : p.inFootprint L.footprintᶜ) (v : γ) : p.relE p (fun (σ₁ σ₂ : s) => σ₂ = L.set v σ₁) fun (x y : α × s) => y.1 = x.1 ∧ y.2 = L.set v x.2

Self-shift specialized to a lens write outside p's footprint: running p from L.set v σ vs from σ.

theorem GaudisCrypt.ProgramDenotation.relE.frame {s₁ s₂ α β γ₁ γ₂ : Type} (L : Lens γ₁ s₁) (M : Lens γ₂ s₂) {p : ProgramDenotation s₁ α} {q : ProgramDenotation s₂ β} (hp : p.inFootprint L.footprintᶜ) (hq : q.inFootprint M.footprintᶜ) {Pre : s₁ → s₂ → Prop} {Post : α × s₁ → β × s₂ → Prop} (h : p.relE q Pre Post) (v : γ₁) (w : γ₂) : p.relE q (fun (σ₁ : s₁) (σ₂ : s₂) => Pre σ₁ σ₂ ∧ L.get σ₁ = v ∧ M.get σ₂ = w) fun (x : α × s₁) (y : β × s₂) => Post x y ∧ L.get x.2 = v ∧ M.get y.2 = w

Two-sided framing.

The EquivModuloLens bridge

theorem GaudisCrypt.ProgramDenotation.EquivModuloLens.to_relE {s α γ : Type} {L : Lens γ s} {p q : ProgramDenotation s α} (h : EquivModuloLens L p q) : p.relE q Eq fun (x y : α × s) => x.1 = y.1 ∧ L.compl.get x.2 = L.compl.get y.2

EquivModuloLens → relE: an equivalence-modulo-L is the diagonal relE at the post "equal results, equal L-complement content".

theorem GaudisCrypt.ProgramDenotation.relE.to_equivModuloLens {s α γ : Type} {L : Lens γ s} {p q : ProgramDenotation s α} (h : p.relE q Eq fun (x y : α × s) => x.1 = y.1 ∧ L.compl.get x.2 = L.compl.get y.2) : EquivModuloLens L p q

relE → EquivModuloLens: conversely, the diagonal relE at the L-complement-equality post yields an equivalence-modulo-L.