ProgramDenotation.range and glob foundations — **LEGACY DetermFootprint theory

(quarantined)**

Deprecated / quarantined. This is the deterministic DetermFootprint/inRange program-range theory, superseded by Footprint + ProbProgramRange (the inFootprint analogues — they are countability-free and a read's range does not collapse). Retained only for CounterExamples, which need the DetermFootprint pathology — nothing in the main development imports this file; new code should use Footprint/inFootprint. The probabilistic wp-layer lives in ProbProgramRange; the range-free generic material that used to live here (liftF, loop_n, up_to_bad, IgnoresLens, Lens.lift/factor, …) is now in WeakestPreconditions.

This file defines

• liftF, which embeds a deterministic state-update f : s → s as a ProgramDenotation s Unit,
• ProgramDenotation.inRange p R, capturing that p's reads and writes live in the region R,
• ProgramDenotation.range p, the smallest such R (via sInf),
• ProgramDenotation.range', the family-version for a → ProgramDenotation s b.

The definition uses the commutant Rᶜ (Compl instance from DetermFootprint.lean): p lies in R iff p commutes with everything outside R. By the bicommutant closure of DetermFootprint, this is equivalent to "the actions of p (lifted to deterministic updates) lie in R".

def GaudisCrypt.ProgramDenotation.inRange {s a : Type} (p : ProgramDenotation s a) (R : DetermFootprint s) : Prop

A program is in a DetermFootprint R iff it commutes with every update in Rᶜ (the commutant of R). By bicommutant closure, this is equivalent to "every state-transition p can perform lies in R".

The two sides are compared as ProgramDenotation s a: on the left, f runs before p and p's return is preserved; on the right, p's return is captured, then f runs, then the saved return is produced.

Equations

• p.inRange R = ∀ f ∈ Rᶜ.updates, (do GaudisCrypt.liftF f p) = do let x ← p GaudisCrypt.liftF f pure x

noncomputable def GaudisCrypt.ProgramDenotation.range {s a : Type} (p : ProgramDenotation s a) : DetermFootprint s

The smallest DetermFootprint in which p lives.

Equations

• p.range = sInf {R : DetermFootprint s | p.inRange R}

noncomputable def GaudisCrypt.ProgramDenotation.range' {s a b : Type} (progs : a → ProgramDenotation s b) : DetermFootprint s

Family version: the smallest DetermFootprint in which every progs x lives. Equivalently the supremum ⨆ x, (progs x).range.

Equations

• GaudisCrypt.ProgramDenotation.range' progs = sInf {R : DetermFootprint s | ∀ (x : a), (progs x).inRange R}

glob: the global variables read/written by a program

@[reducible, inline]

noncomputable abbrev GaudisCrypt.ProgramDenotation.Globals {s a : Type} (A : ProgramDenotation s a) : Type

The type of A's global variables: the quotient of state by (A.range)ᶜ-orbit equivalence. Two states have the same Globals value iff they differ only by an update outside A's range — i.e., they are indistinguishable from A's perspective. Use this anywhere Quotient (A.range)ᶜ.orbit_setoid would otherwise appear.

Equations

• A.Globals = Quotient A.rangeᶜ.orbit_setoid

@[reducible, inline]

noncomputable abbrev GaudisCrypt.ProgramDenotation.Globals' {s a b : Type} (progs : a → ProgramDenotation s b) : Type

Family-version type: the globals of the parameterized family progs.

Equations

• GaudisCrypt.ProgramDenotation.Globals' progs = Quotient (GaudisCrypt.ProgramDenotation.range' progs)ᶜ.orbit_setoid

noncomputable def GaudisCrypt.ProgramDenotation.glob {s a : Type} (A : ProgramDenotation s a) : Getter A.Globals s

The global variables of A — a Getter projecting state s onto the data A can observe or modify. Built from A.range via the DetermFootprint-level touched_getter (which uses the commutant Rᶜ-orbit equivalence).

Equations

• A.glob = A.range.touched_getter

noncomputable def GaudisCrypt.ProgramDenotation.glob' {s a b : Type} (progs : a → ProgramDenotation s b) : Getter (Globals' progs) s

Family version of glob.

Equations

• GaudisCrypt.ProgramDenotation.glob' progs = (GaudisCrypt.ProgramDenotation.range' progs).touched_getter

Structural lemmas

theorem GaudisCrypt.ProgramDenotation.inRange_pure {s a : Type} (x : a) (R : DetermFootprint s) : (pure x).inRange R

pure x is in every range — it touches no state.

theorem GaudisCrypt.ProgramDenotation.inRange_bind {s a b : Type} {p : ProgramDenotation s a} {f : a → ProgramDenotation s b} {R : DetermFootprint s} (hp : p.inRange R) (hf : ∀ (x : a), (f x).inRange R) : (p >>= f).inRange R

Bind composition: if p and every f x live in R, then so does p >>= f.

theorem GaudisCrypt.ProgramDenotation.inRange_mono {s a : Type} {p : ProgramDenotation s a} {R R' : DetermFootprint s} (h : p.inRange R) (hR : R ≤ R') : p.inRange R'

Monotonicity: a larger range still contains the program.

Primitive inRange lemmas

These say that a primitive program (uniform, set, get) lives in the obvious range.

theorem GaudisCrypt.ProgramDenotation.inRange_uniform {s α : Type} [Fintype α] [Nonempty α] : uniform.inRange ⊥

ProgramDenotation.uniform lives in the trivial range (it doesn't touch state).

theorem GaudisCrypt.ProgramDenotation.inRange_uniformOfFinset {s α : Type} [Fintype α] (fs : Finset α) (hs : fs.Nonempty) : (uniformOfFinset fs hs).inRange ⊥

ProgramDenotation.uniformOfFinset lives in the trivial range (it doesn't touch state — it only samples its return value).

theorem GaudisCrypt.ProgramDenotation.inRange_set {s a : Type} (v : Lens a s) (x : a) : (set v x).inRange v.range

ProgramDenotation.set v x lives in v.range.

theorem GaudisCrypt.ProgramDenotation.inRange_get {s a : Type} (v : Lens a s) : (get v).inRange v.range

ProgramDenotation.get v lives in v.range: it reads from v, doesn't write.

theorem GaudisCrypt.ProgramDenotation.set_inRange_compl_of_disjoint {s α β : Type} (v : Lens α s) (L : Lens β s) [disjoint v L] (x : α) : (set v x).inRange L.compl.range

ProgramDenotation.set is in L.compl.range when the setter v is disjoint from the reader L. Common one-liner replacing inRange_mono (inRange_set _ _) (Lens.range_le_compl_of_disjoint v L).

theorem GaudisCrypt.ProgramDenotation.get_inRange_compl_of_disjoint {s α β : Type} (v : Lens α s) (L : Lens β s) [disjoint v L] : (get v).inRange L.compl.range

ProgramDenotation.get is in L.compl.range when the reader v is disjoint from L. Common one-liner replacing inRange_mono (inRange_get _) (Lens.range_le_compl_of_disjoint v L).

theorem GaudisCrypt.loop_n_inRange {s : Type} {R : DetermFootprint s} (body : ProgramDenotation s Unit) (h_body : body.inRange R) (n : ℕ) : (loop_n n body).inRange R

loop_n n body stays in the same range as body.

SubProbability-level characterization of inRange

theorem GaudisCrypt.ProgramDenotation.inRange_subprob {s a : Type} {p : ProgramDenotation s a} {R : DetermFootprint s} (hp : p.inRange R) {f : s → s} (hf : f ∈ Rᶜ.updates) (σ : s) : p (f σ) = do let xs ← p σ pure (xs.1, f xs.2)

inRange lifted to the SubProbability level: at state σ, applying a commutant update f ∈ Rᶜ before p gives the same distribution as running p first and then applying f to the state coordinate of each outcome.

theorem GaudisCrypt.ProgramDenotation.wp_shift_input {s a : Type} {p : ProgramDenotation s a} {R : DetermFootprint s} (hp : p.inRange R) {f : s → s} (hf : 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 form of inRange: shifting the input state by f ∈ Rᶜ is equivalent to post-composing f on the state coordinate of the postcondition.

theorem GaudisCrypt.ProgramDenotation.wp_strengthen_lens_preserved {s α γ : Type} [DecidableEq γ] (L : Lens γ s) {p : ProgramDenotation s α} (h_inRange : p.inRange L.compl.range) (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: if prog modifies only the complement of L, then on the support of prog σ every output state has the same L.get as σ. We can therefore strengthen the postcondition with an if L.get = L.get σ then F else 0 check without changing the wp value.

Proved by a double-shift via ProgramDenotation.wp_shift_input: shifting F and the strengthened post by f := L.liftFunction (Function.const _ (L.get σ)) (which forces L.get to L.get σ) makes both inner posts identical, so the wp values match.

theorem GaudisCrypt.IgnoresLens.comp_inRange {γ s α β : Type} [DecidableEq γ] {L : Lens γ s} {F : β × s → ENNReal} (h_F : IgnoresLens L F) (k : α → ProgramDenotation s β) (h_k : ∀ (a : α), (k a).inRange L.compl.range) : IgnoresLens L fun (aσ : α × s) => (k aσ.1).wp F aσ.2

L-ignoring is preserved when post-composing with an L-disjoint program.

theorem GaudisCrypt.ProgramDenotation.wp_invariant_under_lens_set {s α γ : Type} [DecidableEq γ] (L : Lens γ s) {p : ProgramDenotation s α} (h_p : p.inRange L.compl.range) (v : γ) {F : α × s → ENNReal} (h_F : ∀ (aσ : α × s), F (aσ.1, L.set v aσ.2) = F aσ) (σ : s) : p.wp F (L.set v σ) = p.wp F σ

wp is invariant under L.set v on input when p is L-disjoint and F is invariant under L.set v on its state argument. The intuition: writing v into L before p is invisible because p doesn't read L, and F doesn't see the L-content of the output.

Note: the hypothesis on F is single-value (only requires invariance at this v), not the full IgnoresLens (invariance at every value). Callers that have the stronger IgnoresLens L F can supply fun aσ => h_F aσ v.

theorem GaudisCrypt.ProgramDenotation.wp_cond_set_invisible {s γ : Type} (L : Lens γ s) (cond : Prop) [Decidable cond] (v : γ) (F : Unit × s → ENNReal) (h_F : ∀ (aσ : Unit × s), F (aσ.1, L.set v aσ.2) = F aσ) (σ : s) : (if cond then set L v else pure ()).wp F σ = F ((), σ)

Conditional set is wp-invisible at posts that ignore the set value. if c then set L v else pure () has wp equal to F ((), σ) for any post F that doesn't observe L.set v. Both branches converge: when c holds, set L v is invisible by h_F; otherwise pure () is a no-op. Captures the "conditional tracking write" pattern.

theorem GaudisCrypt.ProgramDenotation.wp_get_modify_invisible {s γ : Type} (L : Lens γ s) (g : γ → γ) (F : Unit × s → ENNReal) (h_F : IgnoresLens L F) (σ : s) : (do let a ← get L set L (g a)).wp F σ = F ((), σ)

Read-modify-write on L is wp-invisible at L-ignoring posts. get L >>= fun a => set L (g a) has the same wp as pure () for any pure modification g : γ → γ of the lens value, provided the post F doesn't read L. Captures the "tracking variable updated in place" pattern: the modification is invisible if downstream code doesn't observe L.

theorem GaudisCrypt.ProgramDenotation.wp_zero_of_lens_preserves {s α γ : Type} [DecidableEq γ] {L : Lens γ s} {p : ProgramDenotation s α} (h_p : p.inRange L.compl.range) {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

Vanishing-post zero: if p is L-disjoint, F vanishes on every state where L.get = v, and the input state already has L.get σ = v, then p.wp F σ = 0. Captures the standard "bad-event vanishing" pattern in security proofs: once the bad flag is set, all post-outcomes count as bad too (and the post assigns them 0), so the wp is 0.

theorem GaudisCrypt.ProgramDenotation.wp_set_disjoint_no_op {s γ : Type} [DecidableEq γ] {L : Lens γ s} {α : Type} {rest : ProgramDenotation s α} (h_rest : rest.inRange L.compl.range) (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 σ

Drop a dead write: prepending ProgramDenotation.set L v to a program rest that doesn't touch L's range is a no-op for any post that ignores L's value. Useful for cleaning up bookkeeping writes that downstream code doesn't read.

theorem GaudisCrypt.ProgramDenotation.wp_conditional_set_disjoint_no_op {s γ : Type} [DecidableEq γ] {L : Lens γ s} {α : Type} (cond : Prop) [Decidable cond] (v : γ) {rest : ProgramDenotation s α} (h_rest : rest.inRange L.compl.range) (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: variant of wp_set_disjoint_no_op where the set is gated by a Prop. Useful for the tracking-variable pattern in cryptographic proofs, where an auxiliary flag is conditionally written inside a loop body whose remainder doesn't read it.

theorem GaudisCrypt.ProgramDenotation.wp_get_then_conditional_set_disjoint_no_op {s γ δ : Type} [DecidableEq γ] {L_get : Lens δ s} {L_set : Lens γ s} {α : Type} (pred : δ → Prop) [DecidablePred pred] (v : γ) {rest : ProgramDenotation s α} (h_rest : rest.inRange L_set.compl.range) (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 when the conditional set targets a lens whose compl.range covers the rest. Captures the common shape get L_get >>= fun cx => (if pred cx then set L_set v else pure) >>= rest used in tracking-variable patterns.

theorem GaudisCrypt.ProgramDenotation.wp_le_of_factors {s α γ : Type} (L : Lens γ s) {prog : ProgramDenotation s α} (h_inRange : prog.inRange L.compl.range) {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: if prog modifies only the complement of L, and the postcondition factors through L.get (i.e. depends only on L-content), then prog.wp (P ∘ snd) σ ≤ P σ. The sub-probability mass of prog σ only decreases the value below P σ.

theorem GaudisCrypt.ProgramDenotation.wp_le_of_factors_two {s α γ₁ γ₂ : Type} [DecidableEq γ₁] [DecidableEq γ₂] (L₁ : Lens γ₁ s) (L₂ : Lens γ₂ s) {prog : ProgramDenotation s α} (h₁ : prog.inRange L₁.compl.range) (h₂ : prog.inRange L₂.compl.range) {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: same idea as ProgramDenotation.wp_le_of_factors, but P factors through the pair (L₁.get, L₂.get) and prog preserves both lenses. Iterates wp_strengthen_lens_preserved over two lenses.

theorem GaudisCrypt.ProgramDenotation.wp_le_of_factors_three {s α γ₁ γ₂ γ₃ : Type} [DecidableEq γ₁] [DecidableEq γ₂] [DecidableEq γ₃] (L₁ : Lens γ₁ s) (L₂ : Lens γ₂ s) (L₃ : Lens γ₃ s) {prog : ProgramDenotation s α} (h₁ : prog.inRange L₁.compl.range) (h₂ : prog.inRange L₂.compl.range) (h₃ : prog.inRange L₃.compl.range) {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: same idea as ProgramDenotation.wp_le_of_factors, but P factors through three lens-gets and prog preserves all three. Used for indicators (e.g. OW's useful_preimage) that depend on multiple independent pieces of state.

Orbit fact

Outputs of p.inRange R started at σ must lie (a.e.) in the R-orbit of σ. We state this as the measure of the "outside-orbit" set being zero.

The proof uses the SubProb-level invariance of (p σ).1 under (id × f) pushforward for f ∈ Rᶜ.updates with f σ = σ (which follows from inRange_subprob). The key observation: any f ∈ Rᶜ that "merges" an off-orbit class c' into the σ-class kills the measure of c'.

For general DetermFootprint R, constructing such an f from Rᶜ requires the Rᶜ-action on the orbit quotient to be rich enough to move any non-σ-class to the σ-class. This holds at least for lens-derived ranges (R = l.range).

def GaudisCrypt.DetermFootprint.HasOrbitCollapse {m : Type u_1} (R : DetermFootprint m) (σ : m) : Prop

A DetermFootprint R collapses to σ if there is a single Rᶜ-update that fixes σ and sends every state into the R-orbit of σ.

For lens-derived R = l.range, this is provided by l.compl.liftFunction (const [σ]): a complement-set that "resets" any state's complement to match σ's. For an abelian bicommutant-closed R, no such update exists.

Equations

• GaudisCrypt.DetermFootprint.HasOrbitCollapse R σ = ∃ f ∈ Rᶜ.updates, f σ = σ ∧ ∀ (s : m), ∃ u ∈ R.updates, u σ = f s

theorem GaudisCrypt.ProgramDenotation.inRange_orbit_of_collapse {s a : Type} {p : ProgramDenotation s a} {R : DetermFootprint s} (hp : p.inRange R) (σ : s) (hcoll : DetermFootprint.HasOrbitCollapse R σ) : ↑(p σ) (Set.univ ×ˢ {s' : s | ∀ u ∈ R.updates, u σ ≠ s'}) = 0

The orbit fact under the HasOrbitCollapse hypothesis: outcomes of p σ are a.e. in R-orbit(σ).

theorem GaudisCrypt.Lens.range_hasOrbitCollapse {s c : Type} (l : Lens c s) (σ : s) : DetermFootprint.HasOrbitCollapse l.range σ

Lens-derived ranges always collapse.

theorem GaudisCrypt.ProgramDenotation.inRange_orbit {s a : Type} {p : ProgramDenotation s a} {R : DetermFootprint s} (hp : p.inRange R) (σ : s) (hcoll : DetermFootprint.HasOrbitCollapse R σ) : ↑(p σ) (Set.univ ×ˢ {s' : s | ∀ u ∈ R.updates, u σ ≠ s'}) = 0

The general orbit fact, packaged with the HasOrbitCollapse precondition. For arbitrary DetermFootprint R, the precondition needs to be supplied externally; for lens-derived R, Lens.range_hasOrbitCollapse discharges it.

theorem GaudisCrypt.ProgramDenotation.commute_of_disjoint {s a b : Type} [Countable a] [Countable b] [Countable s] {p : ProgramDenotation s a} {q : ProgramDenotation s b} {R R' : DetermFootprint s} (hp : p.inRange R) (hq : q.inRange R') (hdisj : R ≤ R'ᶜ) (hp_coll : ∀ (σ : s), DetermFootprint.HasOrbitCollapse R σ) (hq_coll : ∀ (σ : s), DetermFootprint.HasOrbitCollapse R' σ) : (do let x ← p let y ← q pure (x, y)) = do let y ← q let x ← p pure (x, y)

Headline payoff lemma: programs with disjoint ranges commute.

If p lives in R and q lives in R', and the two ranges are disjoint (R ≤ R'ᶜ, equivalently every R-update commutes with every R'-update), then p and q may be run in either order with the same (output, state) distribution.

Additional hypotheses:

• hp_coll, hq_coll: for every starting state σ, a Rᶜ/R'ᶜ-update that "collapses" the orbit of σ to a single point. Lens-derived ranges discharge these via Lens.range_hasOrbitCollapse.
• [Countable a] [Countable b] [Countable s]: needed to discharge the AEMeasurable side condition of MeasureTheory.lintegral_lintegral_swap — for countable types with top σ-algebra every function is measurable.

Proof outline:

1. R ≤ R'ᶜ ⇒ R.updates ⊆ R'ᶜ.updates (and symmetrically R' ≤ Rᶜ).
2. Apply ProgramDenotation.ext_of_wp and unfold wp_bind/wp_pure on both sides.
3. For each outcome (x, s_p) of p σ in the support: by inRange_orbit_of_collapse (using hp_coll), there is u_p ∈ R.updates with u_p σ = s_p. Choose via Classical.choice. Symmetrically v_q for q.
4. Step (a) — rewrite the inner (q xs.2).expected to (q σ).expected (post-shift) via inRange_subprob hq and lintegral_congr_ae (ae on hp_orbit).
5. Step (b) — Fubini swap via MeasureTheory.lintegral_lintegral_swap.
6. Step (c) — rewrite U xs ys.2 = V ys xs.2 using disjoint commutativity, ae on both hp_orbit and hq_orbit.
7. Step (d) — rewrite the inner (p σ).expected (... V ys xs.2 ...) to (p ys.2).expected (...) via inRange_subprob hp and lintegral_congr_ae.
8. Result matches RHS by rfl.

theorem GaudisCrypt.ProgramDenotation.commute_of_disjoint' {s a b : Type} [Countable a] [Countable b] [Countable s] (p : ProgramDenotation s a) (q : ProgramDenotation s b) (hp : p.inRange p.range) (hq : q.inRange q.range) (hdisj : p.range ≤ q.rangeᶜ) (hp_coll : ∀ (σ : s), DetermFootprint.HasOrbitCollapse p.range σ) (hq_coll : ∀ (σ : s), DetermFootprint.HasOrbitCollapse q.range σ) : (do let x ← p let y ← q pure (x, y)) = do let y ← q let x ← p pure (x, y)

Thin wrapper that specialises the disjointness statement to each program's own range. The user-facing signature mentions only p.range and q.range (no auxiliary R, R'). The two inRange p p.range / inRange q q.range premises must be discharged by the caller.

theorem GaudisCrypt.ProgramDenotation.commute_of_disjoint_lens {s a b c d : Type} [Countable a] [Countable b] [Countable s] {p : ProgramDenotation s a} {q : ProgramDenotation s b} {l : Lens c s} {l' : Lens d s} (hp : p.inRange l.range) (hq : q.inRange l'.range) (hdisj : l.range ≤ l'.rangeᶜ) : (do let x ← p let y ← q pure (x, y)) = do let y ← q let x ← p pure (x, y)

Lens-derived variant: when p and q live in lens-derived ranges, the HasOrbitCollapse premises are discharged automatically by Lens.range_hasOrbitCollapse. So the user only needs to supply the inRange proofs and the disjointness of the lens ranges.

Lens lifting and factoring

If Adv : ProgramDenotation s a is confined to a lens window L : Lens c s (i.e. Adv.inRange L.range), then Adv is the lifting of some "inner" program Adv' : ProgramDenotation c a along L. This is the converse to the obvious direction that any lift lives in the lens's range.

theorem GaudisCrypt.Lens.factor_of_inRange {c s a : Type} [Nonempty s] (L : Lens c s) {Adv : ProgramDenotation s a} (h : Adv.inRange L.range) : Adv = L.lift (L.factor Adv)

Factorization theorem: every program confined to a lens window comes from running some inner program on the L-content.

The witness is L.factor Adv (which depends on an arbitrary "padding" state); the equation Adv = L.lift (L.factor Adv) holds because Adv.inRange L.range makes Adv insensitive to the padding's outside content.

Lifting a confined program along a chained lens

These close the lift_inRange_chain obligation used by the RO syntactic- equivalence development. All ranges here are lens ranges, so the orbit machinery is not needed — the facts are pure lens algebra plus the existing inRange_get/inRange_set extractions.

theorem GaudisCrypt.Lens.lift_inRange_self {c s a : Type} (M : Lens c s) (Q : ProgramDenotation c a) : (M.lift Q).inRange M.range

A lift lives in its lens's range. For any inner program Q, the lift M.lift Q is confined to M.range: it only touches the M-window.

theorem GaudisCrypt.Lens.lift_inRange_chain {c s d a : Type} [Nonempty c] (L : Lens c s) (v : Lens d c) (P : ProgramDenotation c a) (hP : P.inRange v.range) : (L.lift P).inRange (L.chain v).range

Lift confines the footprint through the chained lens. A program P confined to window v lifts (along L) to one confined to the composite L ∘ v. Proof: P factors as v.lift (v.factor P) (by factor_of_inRange), lift composition turns the double lift into a single (L.chain v) lift, and lift_inRange_self confines that to (L.chain v).range.

theorem GaudisCrypt.ProgramDenotation.inRange_toProgramDenotation {s a : Type} (μ : SubProbability a) (R : DetermFootprint s) : μ.toProgramDenotation.inRange R

A sampled value lives in every range. μ.toProgramDenotation only draws its return value; it never touches the state, so it commutes with every update.

theorem GaudisCrypt.Lens.chain_range_le {a b c : Type} (L : Lens b c) (v : Lens a b) : (L.chain v).range ≤ L.range

Chaining focuses a sub-window: (L.chain v).range ≤ L.range. Every L∘v-update is an L-update (acting only inside the L-window).