SPComp Instance of UCMonad

This file provides the concrete UCMonad SPComp instance, connecting the generic typeclass to the existing CatCrypt infrastructure.

Main results

• UCMonad SPComp — the instance
• mapSumSP — a UC-free local copy of mapSum (keeps this file off the UC layer)

The generic↔concrete bridge lemmas (generic_UCEmulates_iff_concrete, generic_approxFact_iff_concrete) need Crypto.UC, so they live in SPCompUCBridge.lean.

Design

The instance fields map directly:

• ucMapSum → mapSum (from UC.lean)
• ucFail → SPComp.fail (from Code.lean)
• ucSdist → sdist (from SDist.lean)

Re-derive bind_fail_right (private in Affine.lean)

theorem UCMonad.spcomp_bind_fail {α β : Type} (c : CatCrypt.Core.SPComp α) : (c.bind fun (x : α) => CatCrypt.Core.SPComp.fail) = CatCrypt.Core.SPComp.fail

Localized mapSum (UC-free copy)

mapSum lives in UC.lean, which this file must NOT depend on: keeping SPCompInstance off the UC layer is what makes the whole RoundM/ITreeN substrate built on it UC-free (the compiler-boundary cut). mapSum is a pure Sum-parallel-composition, so we keep a local copy here; the proofs mirror UC.lean / UCFactorization.lean.

noncomputable def UCMonad.mapSumSP {α β γ δ : Type} (f : α → CatCrypt.Core.SPComp β) (g : γ → CatCrypt.Core.SPComp δ) : α ⊕ γ → CatCrypt.Core.SPComp (β ⊕ δ)

Equations

• UCMonad.mapSumSP f g (Sum.inl a) = CatCrypt.Core.SPComp.map Sum.inl (f a)
• UCMonad.mapSumSP f g (Sum.inr c) = CatCrypt.Core.SPComp.map Sum.inr (g c)

@[simp]

theorem UCMonad.mapSumSP_inl {α β γ δ : Type} (f : α → CatCrypt.Core.SPComp β) (g : γ → CatCrypt.Core.SPComp δ) (a : α) : mapSumSP f g (Sum.inl a) = CatCrypt.Core.SPComp.map Sum.inl (f a)

@[simp]

theorem UCMonad.mapSumSP_inr {α β γ δ : Type} (f : α → CatCrypt.Core.SPComp β) (g : γ → CatCrypt.Core.SPComp δ) (c : γ) : mapSumSP f g (Sum.inr c) = CatCrypt.Core.SPComp.map Sum.inr (g c)

@[simp]

theorem UCMonad.mapSumSP_pure_left {α β γ : Type} (g : β → CatCrypt.Core.SPComp γ) (a : α) : mapSumSP CatCrypt.Core.SPComp.pure g (Sum.inl a) = CatCrypt.Core.SPComp.pure (Sum.inl a)

@[simp]

theorem UCMonad.mapSumSP_pure_right {α β γ : Type} (f : α → CatCrypt.Core.SPComp β) (c : γ) : mapSumSP f CatCrypt.Core.SPComp.pure (Sum.inr c) = CatCrypt.Core.SPComp.pure (Sum.inr c)

theorem UCMonad.mapSumSP_pure_pure {α β : Type} : mapSumSP CatCrypt.Core.SPComp.pure CatCrypt.Core.SPComp.pure = CatCrypt.Core.SPComp.pure

theorem UCMonad.mapSumSP_pure_kleisli_comp {α β γ δ : Type} (f : β → CatCrypt.Core.SPComp γ) (g : γ → CatCrypt.Core.SPComp δ) : (fun (x : α ⊕ β) => (mapSumSP CatCrypt.Core.SPComp.pure f x).bind (mapSumSP CatCrypt.Core.SPComp.pure g)) = mapSumSP CatCrypt.Core.SPComp.pure fun (b : β) => (f b).bind g

theorem UCMonad.sdist_mapSumSP_le {α₁ α₂ β₁ β₂ : Type} (f₁ f₂ : α₁ → CatCrypt.Core.SPComp α₂) (g₁ g₂ : β₁ → CatCrypt.Core.SPComp β₂) {ε₁ ε₂ : ENNReal} (hf : CatCrypt.Crypto.sdist f₁ f₂ ≤ ε₁) (hg : CatCrypt.Crypto.sdist g₁ g₂ ≤ ε₂) : CatCrypt.Crypto.sdist (mapSumSP f₁ g₁) (mapSumSP f₂ g₂) ≤ max ε₁ ε₂

UC-free copy of RC.sdist_mapSum_le for mapSumSP. Since mapSumSP is definitionally mapSum, this also closes goals stated with mapSum, letting the ITreeN multi-session layer stay off the RC/UC layer. Proof mirrors RC.sdist_mapSum_le.

The UCMonad instance for SPComp

@[instance_reducible]

noncomputable instance UCMonad.instUCMonadSPComp : UCMonad CatCrypt.Core.SPComp

Equations

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

UCPure instance for SPComp

@[instance_reducible]

instance UCMonad.instUCPureSPComp : UCPure CatCrypt.Core.SPComp

SPComp.IsPure satisfies the UCPure interface.

Equations

• UCMonad.instUCPureSPComp = { isPure := fun {α : Type} => CatCrypt.Core.SPComp.IsPure, isPure_pure := ⋯, isPure_bind := ⋯, isPure_comm := ⋯ }