Prob program-range wp-layer

The Footprint analogue of the wp-layer in ProgramRange (countability-free): pushing a deterministic outside-update across wp (wp_shift_input_prob), and the lens-preservation bounds (wp_le_of_factors_footprint and its 2- and 3-lens forms, wp_strengthen_lens_preserved_footprint). Foundation for migrating the RO crypto stack off DetermFootprint/inRange.

theorem GaudisCrypt.ProgramDenotation.wp_shift_input_prob {s a : Type} {p : ProgramDenotation s a} {R : Footprint s} (hp : p.inFootprint R) {f : s → s} (hf : diracKer f ∈ Rᶜ.updates) (F : a × s → ENNReal) (σ : s) : p.wp F (f σ) = p.wp (fun (xs : a × s) => F (xs.1, f xs.2)) σ

wp_shift_input over Footprint — countability-free. The probabilistic analogue of ProgramDenotation.wp_shift_input: a program in range R lets a deterministic outside-update f (a Dirac kernel in Rᶜ) be pushed from the input to the output of wp. Same proof, via inFootprint_subprob.

theorem GaudisCrypt.ProgramDenotation.wp_le_of_factors_footprint {s α γ : Type} (L : Lens γ s) {prog : ProgramDenotation s α} (h_inRange : prog.inFootprint L.footprintᶜ) {P : s → ENNReal} (h_factors : ∀ (σ σ' : s), L.get σ' = L.get σ → P σ' = P σ) (σ : s) : prog.wp (fun (xs : α × s) => P xs.2) σ ≤ P σ

Preservation under in-range, over Footprint — countability-free analogue of ProgramDenotation.wp_le_of_factors: if prog's probabilistic footprint avoids L (inFootprint (L.footprint)ᶜ) and P factors through L.get, then prog.wp (P ∘ snd) σ ≤ P σ.

theorem GaudisCrypt.ProgramDenotation.wp_strengthen_lens_preserved_footprint {s α γ : Type} [DecidableEq γ] (L : Lens γ s) {p : ProgramDenotation s α} (h_inRange : p.inFootprint L.footprintᶜ) (F : α × s → ENNReal) (σ : s) : p.wp F σ = p.wp (fun (aσ' : α × s) => if L.get aσ'.2 = L.get σ then F aσ' else 0) σ

Lens-preservation strengthening over Footprint — countability-free analogue of ProgramDenotation.wp_strengthen_lens_preserved.

theorem GaudisCrypt.ProgramDenotation.wp_le_of_factors_two_footprint {s α γ₁ γ₂ : Type} [DecidableEq γ₁] [DecidableEq γ₂] (L₁ : Lens γ₁ s) (L₂ : Lens γ₂ s) {prog : ProgramDenotation s α} (h₁ : prog.inFootprint L₁.footprintᶜ) (h₂ : prog.inFootprint L₂.footprintᶜ) {P : s → ENNReal} (h_factors : ∀ (σ σ' : s), L₁.get σ' = L₁.get σ → L₂.get σ' = L₂.get σ → P σ' = P σ) (σ : s) : prog.wp (fun (xs : α × s) => P xs.2) σ ≤ P σ

Two-lens preservation over Footprint — countability-free analogue of ProgramDenotation.wp_le_of_factors_two.

theorem GaudisCrypt.ProgramDenotation.wp_le_of_factors_three_footprint {s α γ₁ γ₂ γ₃ : Type} [DecidableEq γ₁] [DecidableEq γ₂] [DecidableEq γ₃] (L₁ : Lens γ₁ s) (L₂ : Lens γ₂ s) (L₃ : Lens γ₃ s) {prog : ProgramDenotation s α} (h₁ : prog.inFootprint L₁.footprintᶜ) (h₂ : prog.inFootprint L₂.footprintᶜ) (h₃ : prog.inFootprint L₃.footprintᶜ) {P : s → ENNReal} (h_factors : ∀ (σ σ' : s), L₁.get σ' = L₁.get σ → L₂.get σ' = L₂.get σ → L₃.get σ' = L₃.get σ → P σ' = P σ) (σ : s) : prog.wp (fun (xs : α × s) => P xs.2) σ ≤ P σ

Three-lens preservation over Footprint — countability-free analogue of ProgramDenotation.wp_le_of_factors_three.

theorem GaudisCrypt.ProgramDenotation.wp_zero_of_lens_preserves_footprint {s α γ : Type} [DecidableEq γ] {L : Lens γ s} {p : ProgramDenotation s α} (h_p : p.inFootprint L.footprintᶜ) {F : α × s → ENNReal} {v : γ} (h_F_zero : ∀ (aσ : α × s), L.get aσ.2 = v → F aσ = 0) {σ : s} (h_σ : L.get σ = v) : p.wp F σ = 0

wp vanishes on a preserved-lens zero region — the inFootprint analogue of ProgramDenotation.wp_zero_of_lens_preserves: if p avoids L, F vanishes whenever L.get = v, and we start at L.get σ = v, then p.wp F σ = 0.

theorem GaudisCrypt.ProgramDenotation.wp_set_disjoint_no_op_footprint {s γ : Type} [DecidableEq γ] {L : Lens γ s} {α : Type} {rest : ProgramDenotation s α} (h_rest : rest.inFootprint L.footprintᶜ) (v : γ) (F : α × s → ENNReal) (h_F : ∀ (aσ : α × s), F (aσ.1, L.set v aσ.2) = F aσ) (σ : s) : (do set L v rest).wp F σ = rest.wp F σ

Dead write across a disjoint footprint — the inFootprint analogue of ProgramDenotation.wp_set_disjoint_no_op. If rest lives in (L.footprint)ᶜ and the post F ignores L, then a preceding ProgramDenotation.set L v is a no-op for the wp.

theorem GaudisCrypt.ProgramDenotation.wp_conditional_set_disjoint_no_op_footprint {s γ : Type} [DecidableEq γ] {L : Lens γ s} {α : Type} (cond : Prop) [Decidable cond] (v : γ) {rest : ProgramDenotation s α} (h_rest : rest.inFootprint L.footprintᶜ) (F : α × s → ENNReal) (h_F : ∀ (aσ : α × s), F (aσ.1, L.set v aσ.2) = F aσ) (σ : s) : (do if cond then set L v else pure () rest).wp F σ = rest.wp F σ

Conditional dead write across a disjoint footprint — the inFootprint analogue of ProgramDenotation.wp_conditional_set_disjoint_no_op.

theorem GaudisCrypt.ProgramDenotation.wp_get_then_conditional_set_disjoint_no_op_footprint {s γ δ : Type} [DecidableEq γ] {L_get : Lens δ s} {L_set : Lens γ s} {α : Type} (pred : δ → Prop) [DecidablePred pred] (v : γ) {rest : ProgramDenotation s α} (h_rest : rest.inFootprint L_set.footprintᶜ) (F : α × s → ENNReal) (h_F : ∀ (aσ : α × s), F (aσ.1, L_set.set v aσ.2) = F aσ) (σ : s) : (do let cx ← get L_get if pred cx then set L_set v else pure () rest).wp F σ = rest.wp F σ

Get-then-conditional-set is a no-op across a disjoint footprint — the inFootprint analogue of ProgramDenotation.wp_get_then_conditional_set_disjoint_no_op.

theorem GaudisCrypt.ProgramDenotation.inFootprint_toProgramDenotation {s a : Type} (μ : SubProbability a) : μ.toProgramDenotation.inFootprint ⊥

A state-independent sampled value has trivial probabilistic footprint — the Footprint analogue of ProgramDenotation.inRange_toProgramDenotation (at ⊥; lift to any R with inFootprint_mono … bot_le). Same swap argument as inFootprint_uniform.

theorem GaudisCrypt.ProgramDenotation.inFootprint_uniformOfFinset {s α : Type} (fs : Finset α) (hs : fs.Nonempty) : (uniformOfFinset fs hs).inFootprint ⊥

ProgramDenotation.uniformOfFinset has trivial probabilistic footprint — the Footprint analogue of ProgramDenotation.inRange_uniformOfFinset.

theorem GaudisCrypt.loop_n_inFootprint {s : Type} {R : Footprint s} (body : ProgramDenotation s Unit) (h_body : body.inFootprint R) (n : ℕ) : (loop_n n body).inFootprint R

loop_n n body stays in the same footprint as body — the Footprint analogue of loop_n_inRange.

theorem GaudisCrypt.IgnoresLens.comp_inFootprint {γ s α β : Type} {L : Lens γ s} {F : β × s → ENNReal} (h_F : IgnoresLens L F) (k : α → ProgramDenotation s β) (h_k : ∀ (a : α), (k a).inFootprint L.footprintᶜ) : IgnoresLens L fun (aσ : α × s) => (k aσ.1).wp F aσ.2

L-ignoring is preserved when post-composing with an L-disjoint program — the Footprint analogue of IgnoresLens.comp_inRange.

theorem GaudisCrypt.factor_of_inFootprint {c s a : Type} [Nonempty s] (L : Lens c s) {Adv : ProgramDenotation s a} (h : Adv.inFootprint L.footprint) : Adv = L.lift (L.factor Adv)

Factorization: a program confined to L's probabilistic range comes from running some inner program on the L-content. The inFootprint analogue of Lens.factor_of_inRange.