Discrete subprobability monad

noncomputable def GaudisCrypt.SubProbability.expected {a : Type u_1} (μ : SubProbability a) (f : a → ENNReal) : ENNReal

Expected value of f under the distribution μ

Equations

• μ.expected f = ∫⁻ (x : a), f x ∂↑μ

theorem GaudisCrypt.uniform_expected {a : Type u_1} [Fintype a] [Nonempty a] (f : a → ENNReal) : SubProbability.uniform.expected f = ∑ x : a, f x / ↑(Fintype.card a)

theorem GaudisCrypt.uniformOfFinset_expected {a : Type} [Fintype a] (fs : Finset a) (hs : fs.Nonempty) (f : a → ENNReal) : (SubProbability.uniformOfFinset fs hs).expected f = ∑ x ∈ fs, f x / ↑fs.card

theorem GaudisCrypt.expected_pure {a : Type u_1} {f : a → ENNReal} (x : a) : (pure x).expected f = f x

theorem GaudisCrypt.SubProbability.expected_bind {α β : Type} (μ : SubProbability α) (k : α → SubProbability β) (F : β → ENNReal) : (μ >>= k).expected F = μ.expected fun (a : α) => (k a).expected F

SubProbability expected-bind: integrate F against μ >>= k by integrating (k ·).expected F against μ.

theorem GaudisCrypt.expectation_indicator {a : Type u_1} (mu : SubProbability a) (s : Set a) (c : ENNReal) : mu.expected (s.indicator fun (x : a) => c) = c * ↑(mu.ofEvent s)

theorem GaudisCrypt.expectation_mono {i : Type u_1} {a : Type u_2} [Preorder i] (μ : i → SubProbability a) (f : i → a → ENNReal) (hμ : Monotone μ) (hf : Monotone f) : Monotone fun (x : i) => (μ x).expected (f x)

theorem GaudisCrypt.recursion_expected {a : Type u_1} {b : a → Type} (F : ((x : a) → SubProbability (b x)) →𝒄 (x : a) → SubProbability (b x)) (Ψ : ((x : a) → (b x → ENNReal) →o ENNReal) →o (x : a) → (b x → ENNReal) →o ENNReal) (h : ∀ (X : (x : a) → SubProbability (b x)), (Ψ fun (x : a) => { toFun := fun (f : b x → ENNReal) => (X x).expected f, monotone' := ⋯ }) = fun (x : a) => { toFun := fun (f : b x → ENNReal) => (F X x).expected f, monotone' := ⋯ }) (x : a) (f : b x → ENNReal) : (F.lfp x).expected f = (OrderHom.lfp Ψ x) f

Stateful programs

@[reducible]

def GaudisCrypt.ProgramDenotation.Post (s : Type u_1) (a : Type u_2) : Type (max u_1 u_2)

Equations

• GaudisCrypt.ProgramDenotation.Post s a = (a × s → ENNReal)

@[reducible]

def GaudisCrypt.ProgramDenotation.Pre (s : Sort u_1) : Sort (max 1 u_1)

Equations

• GaudisCrypt.ProgramDenotation.Pre s = (s → ENNReal)

noncomputable def GaudisCrypt.ProgramDenotation.wp {s a : Type} (prog : ProgramDenotation s a) (f : Post s a) : Pre s

Equations

• prog.wp f st = (prog st).expected f

theorem GaudisCrypt.final_probability_wp {a s : Type} [DecidableEq a] (prog : ProgramDenotation s a) (st : s) (x : a) : ↑(prog.finalProb1 st x) = prog.wp (fun (x_1 : a × s) => match x_1 with | (y, snd) => if y = x then 1 else 0) st

theorem GaudisCrypt.final_probability_wp' {a s : Type} [DecidableEq a] (prog : ProgramDenotation s a) (st : s) (x : a) : prog.finalProb1 st x = (prog.wp (fun (x_1 : a × s) => match x_1 with | (y, snd) => if y = x then 1 else 0) st).toNNReal

theorem GaudisCrypt.wp_lift {a s : Type} (μ : SubProbability a) (f : ProgramDenotation.Post s a) : μ.toProgramDenotation.wp f = fun (st : s) => μ.expected fun (x : a) => f (x, st)

theorem GaudisCrypt.wp_uniform {a s : Type} [h : Fintype a] [h✝ : Nonempty a] (f : ProgramDenotation.Post s a) : ProgramDenotation.uniform.wp f = fun (s_1 : s) => ∑ i : a, f (i, s_1) / ↑(Fintype.card a)

theorem GaudisCrypt.wp_uniformOfFinset {st a : Type} [Fintype a] (fs : Finset a) (hs : fs.Nonempty) (f : ProgramDenotation.Post st a) : (ProgramDenotation.uniformOfFinset fs hs).wp f = fun (σ : st) => ∑ i ∈ fs, f (i, σ) / ↑fs.card

theorem GaudisCrypt.wp_bind {s α β : Type} (prog : ProgramDenotation s α) (f : α → ProgramDenotation s β) (g : ProgramDenotation.Post s β) : (prog >>= f).wp g = prog.wp fun (x : α × s) => match x with | (a, s') => (f a).wp g s'

theorem GaudisCrypt.wp_pure {s α : Type} (x : α) (f : ProgramDenotation.Post s α) : (pure x).wp f = fun (st : s) => f (x, st)

Postcondition combinators for wp

Basic monotonicity, the 0-postcondition, the constant-postcondition bound (from sub-probability mass), linearity, and constant scaling. These are pure consequences of wp = lintegral against the SubProb measure.

theorem GaudisCrypt.ProgramDenotation.wp_le_wp_of_le {s a : Type} (p : ProgramDenotation s a) (F G : Post s a) (h : ∀ (x : a × s), F x ≤ G x) (σ : s) : p.wp F σ ≤ p.wp G σ

Pointwise monotonicity of wp in the postcondition.

theorem GaudisCrypt.ProgramDenotation.wp_zero_post {s a : Type} (p : ProgramDenotation s a) (σ : s) : p.wp (fun (x : a × s) => 0) σ = 0

wp of the constant 0 postcondition is 0.

theorem GaudisCrypt.ProgramDenotation.wp_const_le {s a : Type} (p : ProgramDenotation s a) (c : ENNReal) (σ : s) : p.wp (fun (x : a × s) => c) σ ≤ c

wp of the constant c postcondition is at most c, since the underlying measure is a sub-probability (total mass ≤ 1).

theorem GaudisCrypt.ProgramDenotation.wp_add {s a : Type} (p : ProgramDenotation s a) (F G : Post s a) (σ : s) : p.wp (fun (aσ : a × s) => F aσ + G aσ) σ = p.wp F σ + p.wp G σ

Linearity of wp in the postcondition.

theorem GaudisCrypt.ProgramDenotation.wp_const_mul {s a : Type} (p : ProgramDenotation s a) (c : ENNReal) (F : Post s a) (σ : s) : p.wp (fun (aσ : a × s) => c * F aσ) σ = c * p.wp F σ

Constant scaling of wp.

theorem GaudisCrypt.ProgramDenotation.wp_finset_sum {s α β : Type} [Fintype β] (p : ProgramDenotation s α) (F : β → α × s → ENNReal) (σ : s) : p.wp (fun (aσ : α × s) => ∑ b : β, F b aσ) σ = ∑ b : β, p.wp (F b) σ

wp commutes with finite sums of postconditions.

theorem GaudisCrypt.wp_ite {s α : Type} (b : Bool) (p1 p2 : ProgramDenotation s α) (f : α × s → ENNReal) (st : s) : (if b = true then p1 else p2).wp f st = if b = true then p1.wp f st else p2.wp f st

theorem GaudisCrypt.wp_set_state {s : Type} (st' : s) (f : Unit × s → ENNReal) (st : s) : ProgramDenotation.wp (StateT.set st') f st = f ((), st')

theorem GaudisCrypt.wp_get_state {s : Type} (f : ProgramDenotation.Post s s) : ProgramDenotation.wp StateT.get f = fun (st : s) => f (st, st)

theorem GaudisCrypt.wp_mono {i : Type u_1} {s a : Type} [Preorder i] (μ : i → ProgramDenotation s a) (f : i → ProgramDenotation.Post s a) (hμ : Monotone μ) (hf : Monotone f) : Monotone fun (x : i) => (μ x).wp (f x)

theorem GaudisCrypt.recursion_wp {a : Type u_1} {s b : a → Type} (F : ((x : a) → ProgramDenotation (s x) (b x)) →𝒄 (x : a) → ProgramDenotation (s x) (b x)) (Ψ : ((x : a) → ProgramDenotation.Post (s x) (b x) →o ProgramDenotation.Pre (s x)) →o (x : a) → ProgramDenotation.Post (s x) (b x) →o ProgramDenotation.Pre (s x)) (h : ∀ (X : (x : a) → ProgramDenotation (s x) (b x)) (x : a) (f : ProgramDenotation.Post (s x) (b x)), (Ψ (fun (x : a) => { toFun := fun (f : ProgramDenotation.Post (s x) (b x)) => (X x).wp f, monotone' := ⋯ }) x) f = (F X x).wp f) (x : a) (f : ProgramDenotation.Post (s x) (b x)) : (recursion F x).wp f = (OrderHom.lfp Ψ x) f

def GaudisCrypt.tailrec_wp {b : Type u_1} {c : Type u_2} {a : Type u_3} [CompleteLattice b] [CompleteLattice c] (Φ : a → b →o c →o c) : (a → b →o c) →o a → b →o c

For tailrecursive programs (in particular while-loops), we can write the wp iteration function (argument to recursion_wp[_simple]) as tailrec_wp something. In this case, we'll have some nicer properties. (See while_wp_unfold below for example.)

Equations

• GaudisCrypt.tailrec_wp Φ = { toFun := fun (trafo : a → b →o c) (x : a) => { toFun := fun (post : b) => ((Φ x) post) ((trafo x) post), monotone' := ⋯ }, monotone' := ⋯ }

noncomputable def GaudisCrypt.while_iteration_wp {s : Type} (c : ProgramDenotation s Bool) (p : ProgramDenotation s Unit) : Unit → ProgramDenotation.Post s Unit →o ProgramDenotation.Pre s →o ProgramDenotation.Pre s

Equations

• One or more equations did not get rendered due to their size.

theorem GaudisCrypt.wp_recursion_tailrec_simplify {b : Type u_1} {c : Type u_2} {a : Type u_3} [CompleteLattice b] [CompleteLattice c] (Φ : a → b →o c →o c) (post : b) (x : a) : (OrderHom.lfp (tailrec_wp Φ) x) post = OrderHom.lfp ((Φ x) post)

theorem GaudisCrypt.wp_while' {state✝ : Type} {c : ProgramDenotation state✝ Bool} {p : ProgramDenotation state✝ Unit} {f : ProgramDenotation.Post state✝ Unit} : (while_loop c p).wp f = (OrderHom.lfp (tailrec_wp (while_iteration_wp c p)) ()) f

theorem GaudisCrypt.wp_while {state✝ : Type} {c : ProgramDenotation state✝ Bool} {p : ProgramDenotation state✝ Unit} {f : ProgramDenotation.Post state✝ Unit} : (while_loop c p).wp f = OrderHom.lfp ((while_iteration_wp c p ()) f)

theorem GaudisCrypt.wp_while_unfold {s : Type} (b : ProgramDenotation s Bool) (body : ProgramDenotation s Unit) (post : ProgramDenotation.Post s Unit) : (while_loop b body).wp post = b.wp fun (x : Bool × s) => match x with | (x, st) => if x = true then body.wp (fun (x : Unit × s) => match x with | (fst, st) => (while_loop b body).wp post st) st else post ((), st)

theorem GaudisCrypt.wp_while_invariant {s : Type} (b : ProgramDenotation s Bool) (body : ProgramDenotation s Unit) (I : ProgramDenotation.Pre s) (f : ProgramDenotation.Post s Unit) (h : (b.wp fun (x : Bool × s) => match x with | (x, st) => if x = true then body.wp (fun (x : Unit × s) => match x with | (fst, st) => I st) st else f ((), st)) ≤ I) : (while_loop b body).wp f ≤ I

theorem GaudisCrypt.wp_get {s α : Type} (v : Lens α s) (f : ProgramDenotation.Post s α) : (ProgramDenotation.get v).wp f = fun (st : s) => f (v.get st, st)

theorem GaudisCrypt.wp_set {s α : Type} (v : Lens α s) (x : α) (f : ProgramDenotation.Post s Unit) : (ProgramDenotation.set v x).wp f = fun (st : s) => f ((), v.set x st)

Mass-1 (full probability) lemmas

A program p has mass 1 at state σ iff p.wp (fun _ => 1) σ = 1, i.e., the total sub-probability mass produced by p at σ equals 1. This holds for every "real" probabilistic operation in the language (pure, get, set, uniform, …), and is preserved by >>=. The lemmas below let proofs about identical-until-bad analyses and similar mass-conservation arguments compose mass-1 facts cleanly.

theorem GaudisCrypt.ProgramDenotation.pure_mass_one {s α : Type} (x : α) (σ : s) : (pure x).wp (fun (x : α × s) => 1) σ = 1

pure x has mass 1.

theorem GaudisCrypt.ProgramDenotation.get_mass_one {s α : Type} (L : Lens α s) (σ : s) : (get L).wp (fun (x : α × s) => 1) σ = 1

ProgramDenotation.get L has mass 1.

theorem GaudisCrypt.ProgramDenotation.set_mass_one {s α : Type} (L : Lens α s) (v : α) (σ : s) : (set L v).wp (fun (x : Unit × s) => 1) σ = 1

ProgramDenotation.set L v has mass 1.

theorem GaudisCrypt.ProgramDenotation.uniform_mass_one {s α : Type} [Fintype α] [Nonempty α] (σ : s) : uniform.wp (fun (x : α × s) => 1) σ = 1

ProgramDenotation.uniform has mass 1 (the uniform distribution sums to 1 over its finite, non-empty support).

theorem GaudisCrypt.ProgramDenotation.uniformOfFinset_mass_one {s α : Type} [Fintype α] (fs : Finset α) (hs : fs.Nonempty) (σ : s) : (uniformOfFinset fs hs).wp (fun (x : α × s) => 1) σ = 1

ProgramDenotation.uniformOfFinset has mass 1.

theorem GaudisCrypt.ProgramDenotation.mass_bind {s α β : Type} (p : ProgramDenotation s α) (k : α → ProgramDenotation s β) (hp : ∀ (σ : s), p.wp (fun (x : α × s) => 1) σ = 1) (hk : ∀ (a : α) (σ : s), (k a).wp (fun (x : β × s) => 1) σ = 1) (σ : s) : (p >>= k).wp (fun (x : β × s) => 1) σ = 1

Mass-1 composes through >>=: if p and every k a have mass 1, then so does p >>= k. The workhorse for chaining mass-conservation facts through composite programs.

Getter/setter, zoom, and procedure-wrapper rules

The wp rules for the remaining ProgramDenotation primitives (generic getters and setters, zoom), and for running procedures (procWrap): together they let a game's wp be pushed through its whole call structure.

theorem GaudisCrypt.wp_get_g {s α T : Type} [AsGetter T α s] (v : T) (f : ProgramDenotation.Post s α) : (ProgramDenotation.get v).wp f = fun (st : s) => f ((AsGetter.toG v).get st, st)

theorem GaudisCrypt.wp_set_g {s α T : Type} [AsSetter T α s] (v : T) (x : α) (f : ProgramDenotation.Post s Unit) : (ProgramDenotation.set v x).wp f = fun (st : s) => f ((), (AsSetter.toS v).set x st)

theorem GaudisCrypt.wp_zoom {s t α : Type} (L : Lens s t) (p : ProgramDenotation s α) (f : ProgramDenotation.Post t α) : (ProgramDenotation.zoom L p).wp f = fun (st : t) => p.wp (fun (as' : α × s) => f (as'.1, L.set as'.2 st)) (L.get st)

theorem GaudisCrypt.procedureDenotation_eq_procWrap [ProgramSpec] {sig : ProcedureSignature} (p : Procedure sig) (args : sig.ParamType) : procedureDenotation p args = procWrap p.return_val (sig.localVariableInit p.locals args) (programDenotation p.body)

procedureDenotation of a plain procedure is procWrap of its body (the closed-procedure sibling of procedureDenotation_eq_procWrap_gen).

theorem GaudisCrypt.wp_procWrap [ProgramSpec] {sig : ProcedureSignature} {L : Type} (rv : Getter sig.ret (ProcedureState L)) (init : L) (B : ProgramDenotation (ProcedureState L) Unit) (f : ProgramDenotation.Post State sig.ret) : (procWrap rv init B).wp f = fun (st : State) => B.wp (fun (p : Unit × ProcedureState L) => f (rv.get p.2, p.2.global)) { global := st, locals := init }

@[simp]

theorem GaudisCrypt.procedureWithHoles_eta [ProgramSpec] {holes : HoleSigs} {sig : ProcedureSignature} (p : ProcedureWithHoles holes sig) : { locals := p.locals, body := p.body, return_val := p.return_val } = p

Structure-eta for procedures, as a simp lemma: instantiation (and the call' denotation) decompose a procedure into its fields; this resurfaces the named procedure.

Generic program/wp toolkit (re-homed from ProgramRange.lean)

Range-free material: the deterministic-update embedding liftF, wp extensionality, the bounded-loop combinator loop_n with its mass/linear-bound lemmas, value-marginal bridges, IgnoresLens, the up-to-bad lemma, and the lens lift/factor constructions. None of it mentions DetermFootprint/inRange; footprint-hypothesis variants live in ProgramRange.lean (legacy) and ProbProgramRange.lean (current).

noncomputable def GaudisCrypt.liftF {s : Type} (f : s → s) : ProgramDenotation s Unit

Lift a deterministic state update f : s → s to a ProgramDenotation s Unit.

Equations

• GaudisCrypt.liftF f st = pure ((), f st)

theorem GaudisCrypt.ProgramDenotation.ext_of_wp {s a : Type} (p q : ProgramDenotation s a) (h : ∀ (f : Post s a), p.wp f = q.wp f) : p = q

Programs equal at all postconditions of their wp are equal.

theorem GaudisCrypt.wp_liftF {s : Type} (f : s → s) (F : ProgramDenotation.Post s Unit) : (liftF f).wp F = fun (st : s) => F ((), f st)

The wp of liftF f simply applies the postcondition at the f-shifted state.

Bounded-loop combinator

A generic n-fold iterator and its basic invariance/bound theorems.

noncomputable def GaudisCrypt.loop_n {s : Type} (n : ℕ) (body : ProgramDenotation s Unit) : ProgramDenotation s Unit

Run body exactly n times. Generic bounded loop combinator.

Equations

• GaudisCrypt.loop_n 0 body = pure ()
• GaudisCrypt.loop_n n_2.succ body = do body GaudisCrypt.loop_n n_2 body

theorem GaudisCrypt.loop_n_mass_one {s : Type} (body : ProgramDenotation s Unit) (h_body : ∀ (σ : s), body.wp (fun (x : Unit × s) => 1) σ = 1) (n : ℕ) (σ : s) : (loop_n n body).wp (fun (x : Unit × s) => 1) σ = 1

Mass conservation for loop_n: if body has mass 1 at every state, then so does loop_n n body.

theorem GaudisCrypt.loop_n_wp_linear_bound {s : Type} (body : ProgramDenotation s Unit) (f : s → ENNReal) (c : ENNReal) (h_body : ∀ (σ : s), body.wp (fun (aσ : Unit × s) => f aσ.2) σ ≤ f σ + c) (n : ℕ) (σ : s) : (loop_n n body).wp (fun (aσ : Unit × s) => f aσ.2) σ ≤ f σ + ↑n * c

Linear bump bound for loop_n with respect to a state-projected potential. If body bumps f by ≤ c per iteration, then loop_n n body bumps f by ≤ n*c.

theorem GaudisCrypt.ProgramDenotation.wp_value_eq_marginal_expected {s α : Type} (p : ProgramDenotation s α) (G : α → ENNReal) (σ : s) : p.wp (fun (aσ : α × s) => G aσ.1) σ = (do let aσ ← p σ pure aσ.1).expected G

wp of a value-only post = expected value under the value-marginal. For any G : α → ENNReal, p.wp (fun aσ => G aσ.1) σ equals the expected value of G under the marginal distribution p σ >>= fun aσ => pure aσ.1.

theorem GaudisCrypt.ProgramDenotation.wp_eq_of_marginal_eq {s α : Type} {p q : ProgramDenotation s α} (h_marg : ∀ (σ : s), (do let aσ ← p σ pure aσ.1) = do let aσ ← q σ pure aσ.1) (G : α → ENNReal) (σ : s) : p.wp (fun (aσ : α × s) => G aσ.1) σ = q.wp (fun (aσ : α × s) => G aσ.1) σ

Marginal-equality lifts to wp-equality for value-only posts. If two programs agree on the value-marginal distribution at every starting state, they agree on the wp of any post of the form fun aσ => G aσ.1. This is the generic bridge from a SubProb-level transfer theorem to a wp-level one — used by cr_transfer_wp_of_bit, ow_transfer_wp_of_bit, etc.

def GaudisCrypt.IgnoresLens {γ s α : Type} (L : Lens γ s) (F : α × s → ENNReal) : Prop

A post F ignores lens L if it doesn't depend on L-content of its state argument: setting L to any value leaves F unchanged.

Equations

• GaudisCrypt.IgnoresLens L F = ∀ (aσ : α × s) (v : γ), F (aσ.1, L.set v aσ.2) = F aσ

Identical-until-bad

The "fundamental lemma of game-playing" (Bellare-Rogaway, one-sided form): if two programs p and q agree on every postcondition that vanishes on "bad" outcomes, then p.wp G σ ≤ q.wp G σ + p.wp (G restricted to bad).

In our applications, bad is a state predicate (e.g., "the adversary queried chal_x"), p is the original game, q is the simplified "branch-eliminated" game, and G is the win indicator. We get P[p wins] ≤ P[q wins] + P[p triggered bad].

theorem GaudisCrypt.ProgramDenotation.up_to_bad {s α : Type} {p q : ProgramDenotation s α} {bad : s → Prop} [DecidablePred bad] (G : α × s → ENNReal) (h_agree_on_good : ∀ (σ : s), p.wp (fun (aσ : α × s) => if bad aσ.2 then 0 else G aσ) σ = q.wp (fun (aσ : α × s) => if bad aσ.2 then 0 else G aσ) σ) (σ : s) : p.wp G σ ≤ q.wp G σ + p.wp (fun (aσ : α × s) => if bad aσ.2 then G aσ else 0) σ

Up-to-bad (wp form). If p and q agree on the restriction of any post to ¬ bad, then p.wp G σ ≤ q.wp G σ + p.wp (G | bad) σ.

noncomputable def GaudisCrypt.Lens.lift {c s a : Type} (L : Lens c s) (P : ProgramDenotation c a) : ProgramDenotation s a

Lift an "inner" program along a lens: L.lift P runs P on the L-content of state and writes the result back, leaving the outside untouched.

Equations

• L.lift P σ = do let xc ← P (L.get σ) pure (xc.1, L.set xc.2 σ)

noncomputable def GaudisCrypt.Lens.factor {c s a : Type} [Nonempty s] (L : Lens c s) (Adv : ProgramDenotation s a) : ProgramDenotation c a

Given Adv : ProgramDenotation s a confined to L's range, factor it through an inner program ProgramDenotation c a. The construction picks an arbitrary state to "pad" the inner input; factor_of_inRange shows this padding doesn't matter when Adv.inRange L.range.

Equations

• L.factor Adv c₀ = do let xσ ← Adv (L.set c₀ (Classical.arbitrary s)) pure (xσ.1, L.get xσ.2)

theorem GaudisCrypt.SubProbability.bind_assoc' {α β γ : Type} (μ : SubProbability α) (g : α → SubProbability β) (h' : β → SubProbability γ) : μ >>= g >>= h' = μ >>= fun (x : α) => g x >>= h'

SubProbability bind is associative.

theorem GaudisCrypt.ProgramDenotation.bind_uniform_comm {s α β a : Type} [Fintype α] [Nonempty α] (p : ProgramDenotation s β) (k : α → ProgramDenotation s a) : (p >>= fun (x : β) => uniform >>= k) = do let y ← uniform let _ ← p k y

ProgramDenotation.uniform commutes with any program. Because ProgramDenotation.uniform is state-preserving and produces an independent sample, it can be hoisted out of any preceding bind (and its output passed through to the continuation). The result of the preceding program is discarded.

Generalises adv_commutes_uniform (formerly in RO.lean) to arbitrary programs and return types — the proof never used RO-specific facts.

theorem GaudisCrypt.ProgramDenotation.wp_lift {c s α : Type} (L : Lens c s) (P : ProgramDenotation c α) (F : Post s α) : (L.lift P).wp F = fun (σ : s) => P.wp (fun (ac : α × c) => F (ac.1, L.set ac.2 σ)) (L.get σ)

wp of a lifted program: run P on the L-content and re-set the result.

theorem GaudisCrypt.Lens.lift_lift_chain {c s d a : Type} (L : Lens c s) (v : Lens d c) (Q : ProgramDenotation d a) : L.lift (v.lift Q) = (L.chain v).lift Q

Lift composes via chain. Lifting Q along v and then along L is lifting Q along the composite lens L ∘ v.

theorem GaudisCrypt.ProgramDenotation.wp_toProgramDenotation {s a : Type} (μ : SubProbability a) (G : Post s a) : μ.toProgramDenotation.wp G = fun (σ : s) => μ.expected fun (x : a) => G (x, σ)

wp of a sampled value (μ.toProgramDenotation = StateT.lift μ): it samples its return from μ and leaves the state untouched.