State-independent lift SDistr → SPComp

The canonical stateless embedding of a distribution SDistr α into the stateful probabilistic computation monad SPComp α, obtained by threading the heap through unchanged. This is pure CatCrypt program-logic content — it mentions no external probability library — so it lives in the minimal core basis, where both SDistr and SPComp are defined.

The UCMonadMorphism packaging (sdistrLift) and the VCVio interoperability built on top of this lift live downstream (CatCrypt.Crypto.UCMonad.SDistrLift and the catcrypt-vcvio package), which is why those consumers can depend on a VCVio-free core module rather than dragging the VCVio library into their closure.

Main definitions

• sdistrToSPComp — the state-independent lift.

Main results

• sdistrToSPComp_pure / sdistrToSPComp_bind — monad-morphism laws.
• sdistrToSPComp_isPure — the lift produces heap-independent computations.
• bind_sdistrToSPComp_eq — running a bind of the lift at a heap.
• marginalize_heap — marginalising the heap out of an SDistr (Bool × Heap).

noncomputable def CatCrypt.Crypto.SDistrLift.sdistrToSPComp {α : Type} (d : Prob.SDistr α) : Core.SPComp α

Lift SDistr to SPComp by ignoring the heap.

Equations

• CatCrypt.Crypto.SDistrLift.sdistrToSPComp d h = d.bind fun (a : α) => CatCrypt.Prob.SDistr.pure (a, h)

@[simp]

theorem CatCrypt.Crypto.SDistrLift.sdistrToSPComp_run {α : Type} (d : Prob.SDistr α) (h : Core.Heap) : sdistrToSPComp d h = d.bind fun (a : α) => Prob.SDistr.pure (a, h)

theorem CatCrypt.Crypto.SDistrLift.sdistrToSPComp_pure {α : Type} (a : α) : sdistrToSPComp (Prob.SDistr.pure a) = Core.SPComp.pure a

The state-independent lift preserves pure.

theorem CatCrypt.Crypto.SDistrLift.sdistrToSPComp_bind {α β : Type} (d : Prob.SDistr α) (f : α → Prob.SDistr β) : sdistrToSPComp (d.bind f) = (sdistrToSPComp d).bind fun (a : α) => sdistrToSPComp (f a)

The state-independent lift preserves bind.

theorem CatCrypt.Crypto.SDistrLift.sdistrToSPComp_isPure {α : Type} (d : Prob.SDistr α) : (sdistrToSPComp d).IsPure

The state-independent lift produces IsPure computations.

theorem CatCrypt.Crypto.SDistrLift.bind_sdistrToSPComp_eq {β : Type} (d : Prob.SDistr β) (D : β → Core.SPComp Bool) (h₀ : Core.Heap) : (sdistrToSPComp d).bind D h₀ = d.bind fun (b : β) => D b h₀

Running a bind of the state-independent lift against a distinguisher at a fixed heap collapses to the underlying SDistr bind.

theorem CatCrypt.Crypto.SDistrLift.marginalize_heap (M : Prob.SDistr (Bool × Core.Heap)) : ∑' (h : Core.Heap), M (some (true, h)) = (M.bind fun (p : Bool × Core.Heap) => Prob.SDistr.pure p.1) (some true)

Marginalising the heap out of an SDistr (Bool × Heap): summing the probability of (true, ·) over all heaps equals the probability of true under the first-projection push-forward.