Generic UC Monad Typeclass

This file abstracts the 4 axioms that any monad needs for the UC factorization framework to work:

1. Coproducts (A1): ucMapSum — parallel composition on Sum
2. Affine/failure (A2): ucFail — abort/discard
3. Pseudometric (A3): ucSdist — statistical distance with PPL
4. Monad laws (A4): LawfulMonad — associativity and unit laws

All factorization theorems from UCFactorization.lean, UC.lean, and UCAlg.lean are reproved generically over any monad satisfying these axioms.

Two-Layer Architecture

The theory splits cleanly into two layers:

Standard layer (A1+A2+A4 — any affine monad): Protocol categories, simulator composition, exact (ungraded) simulator-existence preorder, and exact UC emulation, for any monad with coproducts and failure. Captures deterministic simulation and compiler correctness.

Metric-enriched layer (adds A3 — requires probabilistic/quantitative structure): Approximate factorization, ε-bounds, game hopping, statistical UC emulation. Makes Kl(T) into a Lawvere metric space (ℝ≥0∞-enriched category, BMPP 2022). This is the discriminating axiom: only monads with a probabilistic or nondeterministic base give meaningful intermediate distances.

Main definitions

Standard layer (no metric)

• UCMonadBase — A1 + A4: lawful monad with coproduct structure
• UCMonadAffine — A2: failure/abort
• UCPure — purity predicate / central submonad (Carette-Lemonnier-Zamdzhiev 2022)
• UCMonad.ProtObj — generic protocol object
• UCMonad.ProtMor — generic protocol morphism (simulator adapter)
• UCMonad.ExactUCEmulates — exact UC emulation (no metric needed)

Metric-enriched layer

• UCMonadMetric — A3: Lawvere metric on Kl(T) with PPL (non-expansiveness)
• UCMonad — all four axioms combined
• UCMonad.approxFact — ε-approximate factorization
• UCMonad.UCEmulates — generic UC emulation with ε-bound
• UCMonad.SimConstruction — algebraic simulator map
• UCMonad.UCEmulatesAlg — algebraic UC emulation

Main results

Standard layer

• protMor_comp, protMor_comp_assoc — simulator composition
• factPre_refl, factPre_trans — exact factorization preorder
• ExactUCEmulates_refl, ExactUCEmulates_trans — exact UC emulation
• ExactUCEmulates_of_factPre — factorization → exact UC emulation

Metric-enriched layer

• approxFact_refl, approxFact_trans, approxFact_mono
• approxFact_implies_UCEmulates — factorization → UC emulation
• UCEmulates_refl, UCEmulates_trans, UCEmulates_mono
• UCEmulatesAlg.forget, .refl, .trans, .trans_general
• UCEmulates_of_ExactUCEmulates — exact → approximate (ε = 0)

Design

This file has no CatCrypt imports — it is self-contained, depending only on Mathlib for ℝ≥0∞. The concrete SPComp instance is in UCMonad/SPCompInstance.lean.

Section 1: Typeclass Hierarchy

class UCMonad.UCMonadBase (T : Type → Type) extends Monad T, LawfulMonad T : Type 1

A1 + A4: Lawful monad with coproduct structure (mapSum).

ucMapSum f g applies f on .inl and g on .inr, with functoriality laws ensuring it respects pure and Kleisli composition.

• map {α β : Type} : (α → β) → T α → T β
• mapConst {α β : Type} : α → T β → T α
• pure {α : Type} : α → T α
• seq {α β : Type} : T (α → β) → (Unit → T α) → T β
• seqLeft {α β : Type} : T α → (Unit → T β) → T α
• seqRight {α β : Type} : T α → (Unit → T β) → T β
• bind {α β : Type} : T α → (α → T β) → T β
• map_const {α β : Type} : Functor.mapConst = Functor.map ∘ Function.const β
• id_map {α : Type} (x : T α) : id <$> x = x
• comp_map {α β γ : Type} (g : α → β) (h : β → γ) (x : T α) : (h ∘ g) <$> x = h <$> g <$> x
• seqLeft_eq {α β : Type} (x : T α) (y : T β) : x <* y = Function.const β <$> x <*> y
• seqRight_eq {α β : Type} (x : T α) (y : T β) : x *> y = Function.const α id <$> x <*> y
• pure_seq {α β : Type} (g : α → β) (x : T α) : pure g <*> x = g <$> x
• map_pure {α β : Type} (g : α → β) (x : α) : g <$> pure x = pure (g x)
• seq_pure {α β : Type} (g : T (α → β)) (x : α) : g <*> pure x = (fun (h : α → β) => h x) <$> g
• seq_assoc {α β γ : Type} (x : T α) (g : T (α → β)) (h : T (β → γ)) : h <*> (g <*> x) = Function.comp <$> h <*> g <*> x
• bind_pure_comp {α β : Type} (f : α → β) (x : T α) : (do let a ← x pure (f a)) = f <$> x
• bind_map {α β : Type} (f : T (α → β)) (x : T α) : (do let x_1 ← f x_1 <$> x) = f <*> x
• pure_bind {α β : Type} (x : α) (f : α → T β) : pure x >>= f = f x
• bind_assoc {α β γ : Type} (x : T α) (f : α → T β) (g : β → T γ) : x >>= f >>= g = x >>= fun (x : α) => f x >>= g
• ucMapSum {α β γ δ : Type} (f : α → T β) (g : γ → T δ) : α ⊕ γ → T (β ⊕ δ)

  Parallel composition on Sum: applies f to .inl, g to .inr.

• ucMapSum_inl {α β γ δ : Type} (f : α → T β) (g : γ → T δ) (a : α) : ucMapSum f g (Sum.inl a) = do let b ← f a pure (Sum.inl b)

  ucMapSum f g (.inl a) = f a >>= fun b => pure (.inl b)

• ucMapSum_inr {α β γ δ : Type} (f : α → T β) (g : γ → T δ) (c : γ) : ucMapSum f g (Sum.inr c) = do let d ← g c pure (Sum.inr d)

  ucMapSum f g (.inr c) = g c >>= fun d => pure (.inr d)

• ucMapSum_pure_pure {α β : Type} : ucMapSum pure pure = pure

  Identity: ucMapSum pure pure = pure

• ucMapSum_pure_kleisli {α β γ δ : Type} (f : β → T γ) (g : γ → T δ) : (fun (x : α ⊕ β) => ucMapSum pure f x >>= ucMapSum pure g) = ucMapSum pure fun (b : β) => f b >>= g

  Kleisli functoriality: (id ⊕ f) ∘ₖ (id ⊕ g) = id ⊕ (f ∘ₖ g)

class UCMonad.UCMonadAffine (T : Type → Type) extends UCMonad.UCMonadBase T : Type 1

A2: Failure/abort operation satisfying the affine property.

• map {α β : Type} : (α → β) → T α → T β
• mapConst {α β : Type} : α → T β → T α
• pure {α : Type} : α → T α
• seq {α β : Type} : T (α → β) → (Unit → T α) → T β
• seqLeft {α β : Type} : T α → (Unit → T β) → T α
• seqRight {α β : Type} : T α → (Unit → T β) → T β
• bind {α β : Type} : T α → (α → T β) → T β
• map_const {α β : Type} : Functor.mapConst = Functor.map ∘ Function.const β
• id_map {α : Type} (x : T α) : id <$> x = x
• comp_map {α β γ : Type} (g : α → β) (h : β → γ) (x : T α) : (h ∘ g) <$> x = h <$> g <$> x
• seqLeft_eq {α β : Type} (x : T α) (y : T β) : x <* y = Function.const β <$> x <*> y
• seqRight_eq {α β : Type} (x : T α) (y : T β) : x *> y = Function.const α id <$> x <*> y
• pure_seq {α β : Type} (g : α → β) (x : T α) : pure g <*> x = g <$> x
• map_pure {α β : Type} (g : α → β) (x : α) : g <$> pure x = pure (g x)
• seq_pure {α β : Type} (g : T (α → β)) (x : α) : g <*> pure x = (fun (h : α → β) => h x) <$> g
• seq_assoc {α β γ : Type} (x : T α) (g : T (α → β)) (h : T (β → γ)) : h <*> (g <*> x) = Function.comp <$> h <*> g <*> x
• bind_pure_comp {α β : Type} (f : α → β) (x : T α) : (do let a ← x pure (f a)) = f <$> x
• bind_map {α β : Type} (f : T (α → β)) (x : T α) : (do let x_1 ← f x_1 <$> x) = f <*> x
• pure_bind {α β : Type} (x : α) (f : α → T β) : pure x >>= f = f x
• bind_assoc {α β γ : Type} (x : T α) (f : α → T β) (g : β → T γ) : x >>= f >>= g = x >>= fun (x : α) => f x >>= g
• ucMapSum {α β γ δ : Type} (f : α → T β) (g : γ → T δ) : α ⊕ γ → T (β ⊕ δ)
• ucMapSum_inl {α β γ δ : Type} (f : α → T β) (g : γ → T δ) (a : α) : ucMapSum f g (Sum.inl a) = do let b ← f a pure (Sum.inl b)
• ucMapSum_inr {α β γ δ : Type} (f : α → T β) (g : γ → T δ) (c : γ) : ucMapSum f g (Sum.inr c) = do let d ← g c pure (Sum.inr d)
• ucMapSum_pure_pure {α β : Type} : ucMapSum pure pure = pure
• ucMapSum_pure_kleisli {α β γ δ : Type} (f : β → T γ) (g : γ → T δ) : (fun (x : α ⊕ β) => ucMapSum pure f x >>= ucMapSum pure g) = ucMapSum pure fun (b : β) => f b >>= g
• ucFail {α : Type} : T α

  The failing computation.

• ucBind_fail {α β : Type} (c : T α) : (do let _ ← c ucFail) = ucFail

  Binding any computation with ucFail gives ucFail.

class UCMonad.UCMonadMetric (T : Type → Type) extends UCMonad.UCMonadBase T : Type 1

A3: Statistical distance pseudometric with post-processing lemmas (PPL).

Categorically, this makes Kl(T) into a Lawvere metric space (ℝ≥0∞-enriched category) where hom-objects are extended non-negative reals and composition is non-expansive (Lawvere 1973, BMPP 2022). The PPL axioms (ucSdist_comp_right, ucSdist_comp_left) express that Kleisli composition is a non-expansive map on hom-objects — the enriched functoriality condition.

This is the discriminating axiom: A1, A2, A4 hold for any monad with exceptions, but A3 requires a quantitative/probabilistic structure that gives meaningful intermediate distances (0 < ε < ∞). Deterministic monads (StateM, ReaderT, Id) only see distance 0 or ∞, making the enrichment trivial.

Without A3, the exact factorization (Sections 1–3) still works — only the approximate/graded factorization (Section 4+) requires the metric.

• map {α β : Type} : (α → β) → T α → T β
• mapConst {α β : Type} : α → T β → T α
• pure {α : Type} : α → T α
• seq {α β : Type} : T (α → β) → (Unit → T α) → T β
• seqLeft {α β : Type} : T α → (Unit → T β) → T α
• seqRight {α β : Type} : T α → (Unit → T β) → T β
• bind {α β : Type} : T α → (α → T β) → T β
• map_const {α β : Type} : Functor.mapConst = Functor.map ∘ Function.const β
• id_map {α : Type} (x : T α) : id <$> x = x
• comp_map {α β γ : Type} (g : α → β) (h : β → γ) (x : T α) : (h ∘ g) <$> x = h <$> g <$> x
• seqLeft_eq {α β : Type} (x : T α) (y : T β) : x <* y = Function.const β <$> x <*> y
• seqRight_eq {α β : Type} (x : T α) (y : T β) : x *> y = Function.const α id <$> x <*> y
• pure_seq {α β : Type} (g : α → β) (x : T α) : pure g <*> x = g <$> x
• map_pure {α β : Type} (g : α → β) (x : α) : g <$> pure x = pure (g x)
• seq_pure {α β : Type} (g : T (α → β)) (x : α) : g <*> pure x = (fun (h : α → β) => h x) <$> g
• seq_assoc {α β γ : Type} (x : T α) (g : T (α → β)) (h : T (β → γ)) : h <*> (g <*> x) = Function.comp <$> h <*> g <*> x
• bind_pure_comp {α β : Type} (f : α → β) (x : T α) : (do let a ← x pure (f a)) = f <$> x
• bind_map {α β : Type} (f : T (α → β)) (x : T α) : (do let x_1 ← f x_1 <$> x) = f <*> x
• pure_bind {α β : Type} (x : α) (f : α → T β) : pure x >>= f = f x
• bind_assoc {α β γ : Type} (x : T α) (f : α → T β) (g : β → T γ) : x >>= f >>= g = x >>= fun (x : α) => f x >>= g
• ucMapSum {α β γ δ : Type} (f : α → T β) (g : γ → T δ) : α ⊕ γ → T (β ⊕ δ)
• ucMapSum_inl {α β γ δ : Type} (f : α → T β) (g : γ → T δ) (a : α) : ucMapSum f g (Sum.inl a) = do let b ← f a pure (Sum.inl b)
• ucMapSum_inr {α β γ δ : Type} (f : α → T β) (g : γ → T δ) (c : γ) : ucMapSum f g (Sum.inr c) = do let d ← g c pure (Sum.inr d)
• ucMapSum_pure_pure {α β : Type} : ucMapSum pure pure = pure
• ucMapSum_pure_kleisli {α β γ δ : Type} (f : β → T γ) (g : γ → T δ) : (fun (x : α ⊕ β) => ucMapSum pure f x >>= ucMapSum pure g) = ucMapSum pure fun (b : β) => f b >>= g
• ucSdist {α β : Type} : (α → T β) → (α → T β) → ENNReal

  Statistical distance between Kleisli morphisms.

• ucSdist_self {α β : Type} (f : α → T β) : ucSdist f f = 0

  Reflexivity: ucSdist f f = 0

• ucSdist_sym {α β : Type} (f g : α → T β) : ucSdist f g = ucSdist g f

  Symmetry

• ucSdist_triangle {α β : Type} (f g h : α → T β) : ucSdist f h ≤ ucSdist f g + ucSdist g h

  Triangle inequality

• ucSdist_comp_right {α β γ : Type} (f g : α → T β) (k : β → T γ) : (ucSdist (fun (a : α) => f a >>= k) fun (a : α) => g a >>= k) ≤ ucSdist f g

  Right PPL: post-composition doesn't increase distance.

• ucSdist_comp_left {α β γ : Type} (f : α → T β) (g₁ g₂ : β → T γ) : (ucSdist (fun (a : α) => f a >>= g₁) fun (a : α) => f a >>= g₂) ≤ ucSdist g₁ g₂

  Left PPL: pre-composition doesn't increase distance.

class UCMonad.UCMonad (T : Type → Type) extends UCMonad.UCMonadMetric T, UCMonad.UCMonadAffine T : Type 1

All four axioms combined: lawful monad + coproducts + failure + pseudometric.

• map {α β : Type} : (α → β) → T α → T β
• mapConst {α β : Type} : α → T β → T α
• pure {α : Type} : α → T α
• seq {α β : Type} : T (α → β) → (Unit → T α) → T β
• seqLeft {α β : Type} : T α → (Unit → T β) → T α
• seqRight {α β : Type} : T α → (Unit → T β) → T β
• bind {α β : Type} : T α → (α → T β) → T β
• map_const {α β : Type} : Functor.mapConst = Functor.map ∘ Function.const β
• id_map {α : Type} (x : T α) : id <$> x = x
• comp_map {α β γ : Type} (g : α → β) (h : β → γ) (x : T α) : (h ∘ g) <$> x = h <$> g <$> x
• seqLeft_eq {α β : Type} (x : T α) (y : T β) : x <* y = Function.const β <$> x <*> y
• seqRight_eq {α β : Type} (x : T α) (y : T β) : x *> y = Function.const α id <$> x <*> y
• pure_seq {α β : Type} (g : α → β) (x : T α) : pure g <*> x = g <$> x
• map_pure {α β : Type} (g : α → β) (x : α) : g <$> pure x = pure (g x)
• seq_pure {α β : Type} (g : T (α → β)) (x : α) : g <*> pure x = (fun (h : α → β) => h x) <$> g
• seq_assoc {α β γ : Type} (x : T α) (g : T (α → β)) (h : T (β → γ)) : h <*> (g <*> x) = Function.comp <$> h <*> g <*> x
• bind_pure_comp {α β : Type} (f : α → β) (x : T α) : (do let a ← x pure (f a)) = f <$> x
• bind_map {α β : Type} (f : T (α → β)) (x : T α) : (do let x_1 ← f x_1 <$> x) = f <*> x
• pure_bind {α β : Type} (x : α) (f : α → T β) : pure x >>= f = f x
• bind_assoc {α β γ : Type} (x : T α) (f : α → T β) (g : β → T γ) : x >>= f >>= g = x >>= fun (x : α) => f x >>= g
• ucMapSum {α β γ δ : Type} (f : α → T β) (g : γ → T δ) : α ⊕ γ → T (β ⊕ δ)
• ucMapSum_inl {α β γ δ : Type} (f : α → T β) (g : γ → T δ) (a : α) : ucMapSum f g (Sum.inl a) = do let b ← f a pure (Sum.inl b)
• ucMapSum_inr {α β γ δ : Type} (f : α → T β) (g : γ → T δ) (c : γ) : ucMapSum f g (Sum.inr c) = do let d ← g c pure (Sum.inr d)
• ucMapSum_pure_pure {α β : Type} : ucMapSum pure pure = pure
• ucMapSum_pure_kleisli {α β γ δ : Type} (f : β → T γ) (g : γ → T δ) : (fun (x : α ⊕ β) => ucMapSum pure f x >>= ucMapSum pure g) = ucMapSum pure fun (b : β) => f b >>= g
• ucSdist {α β : Type} : (α → T β) → (α → T β) → ENNReal
• ucSdist_self {α β : Type} (f : α → T β) : ucSdist f f = 0
• ucSdist_sym {α β : Type} (f g : α → T β) : ucSdist f g = ucSdist g f
• ucSdist_triangle {α β : Type} (f g h : α → T β) : ucSdist f h ≤ ucSdist f g + ucSdist g h
• ucSdist_comp_right {α β γ : Type} (f g : α → T β) (k : β → T γ) : (ucSdist (fun (a : α) => f a >>= k) fun (a : α) => g a >>= k) ≤ ucSdist f g
• ucSdist_comp_left {α β γ : Type} (f : α → T β) (g₁ g₂ : β → T γ) : (ucSdist (fun (a : α) => f a >>= g₁) fun (a : α) => f a >>= g₂) ≤ ucSdist g₁ g₂
• ucFail {α : Type} : T α
• ucBind_fail {α β : Type} (c : T α) : (do let _ ← c UCMonad.ucFail) = UCMonad.ucFail

class UCMonad.UCPure (T : Type → Type) [Monad T] : Type 1

Purity predicate: marks computations as state-independent.

For T = SPComp, this corresponds to SPComp.IsPure. Pure computations commute with all others (Fubini property). In the directed type theory, purity is the !A (of-course) modality.

Categorically, UCPure is the center (central submonad) of T in the sense of Carette-Lemonnier-Zamdzhiev (LICS 2022). The key property is isPure_comm: pure computations commute with all others, which is equivalent to saying that the pure fragment forms a commutative submonad (the premonoidal center of Kl(T)).

• isPure {α : Type} : T α → Prop

  The purity predicate on individual computations.

• isPure_pure {α : Type} (a : α) : isPure (pure a)

  pure is always pure.

• isPure_bind {α β : Type} (c : T α) (f : α → T β) : isPure c → (∀ (a : α), isPure (f a)) → isPure (c >>= f)

  bind preserves purity.

• isPure_comm {α β γ : Type} (c : T α) (d : T β) (k : α → β → T γ) : isPure c → (do let a ← c let b ← d k a b) = do let b ← d let a ← c k a b

  Commutativity: pure computations commute with all others (Fubini).

  This is the defining property of the central submonad (Carette-Lemonnier-Zamdzhiev, LICS 2022): a computation c is central iff c >>= (fun a => d >>= fun b => k a b) equals d >>= (fun b => c >>= fun a => k a b) for all d and k.

Section 2: Helper Lemmas

theorem UCMonad.ucMapSum_pure_left {T : Type → Type} [UCMonadBase T] {α β γ : Type} (g : β → T γ) (a : α) : UCMonadBase.ucMapSum pure g (Sum.inl a) = pure (Sum.inl a)

theorem UCMonad.ucMapSum_pure_right {T : Type → Type} [UCMonadBase T] {α β γ : Type} (f : α → T β) (c : γ) : UCMonadBase.ucMapSum f pure (Sum.inr c) = pure (Sum.inr c)

theorem UCMonad.ucSdist_le_of_eq {T : Type → Type} [UCMonadMetric T] {α β : Type} {f g : α → T β} (h : f = g) : UCMonadMetric.ucSdist f g = 0

theorem UCMonad.ucSdist_comp_add {T : Type → Type} [UCMonadMetric T] {α β γ : Type} (f₁ f₂ : α → T β) (g₁ g₂ : β → T γ) {ε₁ ε₂ : ENNReal} (hf : UCMonadMetric.ucSdist f₁ f₂ ≤ ε₁) (hg : UCMonadMetric.ucSdist g₁ g₂ ≤ ε₂) : (UCMonadMetric.ucSdist (fun (a : α) => f₁ a >>= g₁) fun (a : α) => f₂ a >>= g₂) ≤ ε₁ + ε₂

Section 3: Generic Protocol Category

structure UCMonad.ProtObj (T : Type → Type) [Monad T] (hon out : Type) : Type 1

A protocol object bundles an interface type with a protocol morphism. Parameterized over any monad T satisfying UCMonadBase.

• iface : Type

  The adversary/simulator interface type

• prot : hon → T (out ⊕ self.iface)

  The protocol: maps honest inputs to honest output + interface

structure UCMonad.ProtMor {T : Type → Type} [UCMonadBase T] {hon out : Type} (P Q : ProtObj T hon out) : Type

A protocol morphism from P to Q consists of a simulator transforming P's interface into Q's interface, with a commutativity proof.

• sim : P.iface → T Q.iface

  The simulator: transforms P's interface to Q's interface

• comm (a : hon) : P.prot a >>= UCMonadBase.ucMapSum pure self.sim = Q.prot a

  Commutativity: (id ⊕ sim) ∘ₖ P.prot = Q.prot

noncomputable def UCMonad.protMor_id {T : Type → Type} [UCMonadBase T] {hon out : Type} (P : ProtObj T hon out) : ProtMor P P

Identity morphism: the pure simulator.

Equations

• UCMonad.protMor_id P = { sim := pure, comm := ⋯ }

noncomputable def UCMonad.protMor_comp {T : Type → Type} [UCMonadBase T] {hon out : Type} {P Q R : ProtObj T hon out} (f : ProtMor P Q) (g : ProtMor Q R) : ProtMor P R

Composition of protocol morphisms: Kleisli-compose the simulators.

Equations

• UCMonad.protMor_comp f g = { sim := fun (x : P.iface) => f.sim x >>= g.sim, comm := ⋯ }

theorem UCMonad.protMor_comp_id_left {T : Type → Type} [UCMonadBase T] {hon out : Type} {P Q : ProtObj T hon out} (f : ProtMor P Q) : (protMor_comp (protMor_id P) f).sim = f.sim

Left identity law for protocol morphism composition.

theorem UCMonad.protMor_comp_id_right {T : Type → Type} [UCMonadBase T] {hon out : Type} {P Q : ProtObj T hon out} (f : ProtMor P Q) : (protMor_comp f (protMor_id Q)).sim = f.sim

Right identity law for protocol morphism composition.

theorem UCMonad.protMor_comp_assoc {T : Type → Type} [UCMonadBase T] {hon out : Type} {P Q R S : ProtObj T hon out} (f : ProtMor P Q) (g : ProtMor Q R) (h : ProtMor R S) : (protMor_comp (protMor_comp f g) h).sim = (protMor_comp f (protMor_comp g h)).sim

Associativity of protocol morphism composition.

def UCMonad.factPre {T : Type → Type} [UCMonadBase T] {hon out : Type} (P Q : ProtObj T hon out) : Prop

Exact factorization preorder (opposite to morphism direction).

Equations

• UCMonad.factPre P Q = Nonempty (UCMonad.ProtMor Q P)

theorem UCMonad.factPre_of_protMor {T : Type → Type} [UCMonadBase T] {hon out : Type} {P Q : ProtObj T hon out} (f : ProtMor Q P) : factPre P Q

theorem UCMonad.factPre_refl {T : Type → Type} [UCMonadBase T] {hon out : Type} (P : ProtObj T hon out) : factPre P P

theorem UCMonad.factPre_trans {T : Type → Type} [UCMonadBase T] {hon out : Type} {P Q R : ProtObj T hon out} (hPQ : factPre P Q) (hQR : factPre Q R) : factPre P R

Section 3b: Exact UC Emulation (Standard Layer — no metric)

The exact factorization and UC emulation depend only on A1+A2+A4 (any affine monad). This is the standard layer of the theory: protocol categories, simulator composition, and exact simulation are available for any monad with coproducts and failure, without requiring a probabilistic metric.

It captures deterministic simulation, compiler correctness, and robust compilation (Patrignani et al., TOPLAS 2024).

The metric-enriched layer (Section 4+) adds A3 to get ε-approximate factorization, statistical distance bounds, and game hopping — requiring a quantitative/probabilistic structure (BMPP 2022).

def UCMonad.ExactUCEmulates {T : Type → Type} [UCMonadBase T] {hon out leak sim_if view : Type} (π : hon → T (out ⊕ leak)) (F : hon → T (out ⊕ sim_if)) : Prop

Exact UC emulation: for all adversaries A, there exists a simulator S such that the real and ideal views are equal (not just close in distance).

This depends only on UCMonadBase (A1+A4) — no metric needed.

Equations

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

theorem UCMonad.ExactUCEmulates_of_factPre {T : Type → Type} [UCMonadBase T] {hon out : Type} {P Q : ProtObj T hon out} {view : Type} (h : factPre P Q) : ExactUCEmulates P.prot Q.prot

Exact factorization implies exact UC emulation (no metric needed).

theorem UCMonad.ExactUCEmulates_refl {T : Type → Type} [UCMonadBase T] {hon out leak view : Type} (π : hon → T (out ⊕ leak)) : ExactUCEmulates π π

Exact UC emulation is reflexive.

theorem UCMonad.ExactUCEmulates_trans {T : Type → Type} [UCMonadBase T] {hon out leak view : Type} {π₁ π₂ π₃ : hon → T (out ⊕ leak)} (h₁ : ExactUCEmulates π₁ π₂) (h₂ : ExactUCEmulates π₂ π₃) : ExactUCEmulates π₁ π₃

Exact UC emulation is transitive (same-interface).

Section 4: Generic Approximate Factorization

def UCMonad.approxFact {T : Type → Type} [UCMonadMetric T] (ε : ENNReal) {hon out : Type} (P Q : ProtObj T hon out) : Prop

ε-approximate factorization preorder.

approxFact ε P Q means: there exists a simulator S : Q.iface → T P.iface such that P.prot is within statistical distance ε of (id ⊕ S) ∘ₖ Q.prot.

Equations

• UCMonad.approxFact ε P Q = ∃ (S : Q.iface → T P.iface), (UCMonad.UCMonadMetric.ucSdist P.prot fun (a : hon) => Q.prot a >>= UCMonad.UCMonadBase.ucMapSum pure S) ≤ ε

theorem UCMonad.approxFact_refl {T : Type → Type} [UCMonadMetric T] {hon out : Type} (P : ProtObj T hon out) : approxFact 0 P P

Reflexivity: identity simulator gives distance 0.

theorem UCMonad.approxFact_mono {T : Type → Type} [UCMonadMetric T] {hon out : Type} {P Q : ProtObj T hon out} {ε₁ ε₂ : ENNReal} (h : approxFact ε₁ P Q) (hle : ε₁ ≤ ε₂) : approxFact ε₂ P Q

Monotonicity: tighter bound implies looser bound.

theorem UCMonad.approxFact_trans {T : Type → Type} [UCMonadMetric T] {hon out : Type} {P Q R : ProtObj T hon out} {ε₁ ε₂ : ENNReal} (h₁ : approxFact ε₁ P Q) (h₂ : approxFact ε₂ Q R) : approxFact (ε₁ + ε₂) P R

Transitivity: simulator chaining gives additive bound.

theorem UCMonad.approxFact_of_factPre {T : Type → Type} [UCMonadMetric T] {hon out : Type} {P Q : ProtObj T hon out} (h : factPre P Q) : approxFact 0 P Q

Exact factorization implies approximate factorization at ε = 0.

theorem UCMonad.approxFact_of_sdist {T : Type → Type} [UCMonadMetric T] {hon out iface : Type} {ε : ENNReal} (π F : hon → T (out ⊕ iface)) (h : UCMonadMetric.ucSdist π F ≤ ε) : approxFact ε { iface := iface, prot := π } { iface := iface, prot := F }

Same-interface sdist bound gives approximate factorization.

Section 5: Generic UC Emulation

def UCMonad.UCEmulates {T : Type → Type} [UCMonadMetric T] (ε : ENNReal) {hon out leak sim_if view : Type} (π : hon → T (out ⊕ leak)) (F : hon → T (out ⊕ sim_if)) : Prop

Protocol π UC-emulates ideal functionality F with statistical error ε.

For ALL adversaries A, there EXISTS a simulator S such that the ucSdist of the post-adversary views is ≤ ε.

Equations

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

def UCMonad.UCEmulatesPerfect {T : Type → Type} [UCMonadMetric T] {hon out leak sim_if : Type} (view : Type) (π : hon → T (out ⊕ leak)) (F : hon → T (out ⊕ sim_if)) : Prop

Perfect UC emulation: ε = 0.

Equations

• UCMonad.UCEmulatesPerfect view π F = UCMonad.UCEmulates 0 π F

theorem UCMonad.UCEmulates_of_sdist {T : Type → Type} [UCMonadMetric T] {hon out leak view : Type} (ε : ENNReal) (π F : hon → T (out ⊕ leak)) (h : UCMonadMetric.ucSdist π F ≤ ε) : UCEmulates ε π F

Same-interface UC: if ucSdist π F ≤ ε, then UCEmulates ε with S = A.

theorem UCMonad.UCEmulates_mono {T : Type → Type} [UCMonadMetric T] {hon out leak sim_if view : Type} {π : hon → T (out ⊕ leak)} {F : hon → T (out ⊕ sim_if)} {ε₁ ε₂ : ENNReal} (h : UCEmulates ε₁ π F) (hle : ε₁ ≤ ε₂) : UCEmulates ε₂ π F

Monotonicity: UC emulation with tighter bound implies looser bound.

theorem UCMonad.UCEmulates_refl {T : Type → Type} [UCMonadMetric T] {hon out leak view : Type} (π : hon → T (out ⊕ leak)) : UCEmulates 0 π π

Reflexivity: any protocol UC-emulates itself perfectly (same-interface).

theorem UCMonad.UCEmulates_trans {T : Type → Type} [UCMonadMetric T] {hon out leak view : Type} {ε₁ ε₂ : ENNReal} {π₁ π₂ π₃ : hon → T (out ⊕ leak)} (h₁ : UCEmulates ε₁ π₁ π₂) (h₂ : UCEmulates ε₂ π₂ π₃) : UCEmulates (ε₁ + ε₂) π₁ π₃

Transitivity of UC emulation (same-interface case).

theorem UCMonad.approxFact_implies_UCEmulates {T : Type → Type} [UCMonadMetric T] {hon out : Type} {P Q : ProtObj T hon out} {view : Type} {ε : ENNReal} (h : approxFact ε P Q) : UCEmulates ε P.prot Q.prot

Approximate factorization implies UC emulation.

theorem UCMonad.exact_factorization_implies_UCEmulatesPerfect {T : Type → Type} [UCMonadMetric T] {hon out : Type} {P Q : ProtObj T hon out} (view : Type) (h : factPre P Q) : UCEmulatesPerfect view P.prot Q.prot

Exact factorization implies perfect UC emulation.

Bridge: exact → approximate

theorem UCMonad.UCEmulates_of_ExactUCEmulates {T : Type → Type} [UCMonadMetric T] {hon out leak sim_if view : Type} {π : hon → T (out ⊕ leak)} {F : hon → T (out ⊕ sim_if)} (h : ExactUCEmulates π F) : UCEmulates 0 π F

Exact UC emulation implies approximate UC emulation at ε = 0.

Section 6: Generic Algebraic UC (Explicit Simulator Construction)

def UCMonad.SimConstruction (T : Type → Type) [Monad T] (leak sim_if view : Type) : Type

A simulator construction: a functorial map from adversaries to simulators.

Equations

• UCMonad.SimConstruction T leak sim_if view = ((leak → T view) → sim_if → T view)

def UCMonad.SimConstruction.id {T : Type → Type} [Monad T] {leak view : Type} : SimConstruction T leak leak view

Identity simulator construction (same-interface).

Equations

• UCMonad.SimConstruction.id = id

def UCMonad.SimConstruction.comp {T : Type → Type} [Monad T] {leak₁ leak₂ leak₃ view : Type} (Sim₁ : SimConstruction T leak₁ leak₂ view) (Sim₂ : SimConstruction T leak₂ leak₃ view) : SimConstruction T leak₁ leak₃ view

Composition of simulator constructions.

Equations

• Sim₁.comp Sim₂ = Sim₂ ∘ Sim₁

@[simp]

theorem UCMonad.SimConstruction.id_comp {T : Type → Type} [Monad T] {leak₁ leak₂ view : Type} (Sim : SimConstruction T leak₁ leak₂ view) : id.comp Sim = Sim

@[simp]

theorem UCMonad.SimConstruction.comp_id {T : Type → Type} [Monad T] {leak₁ leak₂ view : Type} (Sim : SimConstruction T leak₁ leak₂ view) : Sim.comp id = Sim

theorem UCMonad.SimConstruction.comp_assoc {T : Type → Type} [Monad T] {leak₁ leak₂ leak₃ leak₄ view : Type} (Sim₁ : SimConstruction T leak₁ leak₂ view) (Sim₂ : SimConstruction T leak₂ leak₃ view) (Sim₃ : SimConstruction T leak₃ leak₄ view) : (Sim₁.comp Sim₂).comp Sim₃ = Sim₁.comp (Sim₂.comp Sim₃)

def UCMonad.UCEmulatesAlg {T : Type → Type} [UCMonadMetric T] (ε : ENNReal) {hon out leak sim_if view : Type} (π : hon → T (out ⊕ leak)) (F : hon → T (out ⊕ sim_if)) (Sim : SimConstruction T leak sim_if view) : Prop

Algebraic UC emulation with explicit simulator construction.

Equations

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

theorem UCMonad.UCEmulatesAlg.forget {T : Type → Type} [UCMonadMetric T] {ε : ENNReal} {hon out leak sim_if view : Type} {π : hon → T (out ⊕ leak)} {F : hon → T (out ⊕ sim_if)} {Sim : SimConstruction T leak sim_if view} (h : UCEmulatesAlg ε π F Sim) : UCEmulates ε π F

Forget the algebraic witness: UCEmulatesAlg → UCEmulates.

theorem UCMonad.UCEmulatesAlg.mono {T : Type → Type} [UCMonadMetric T] {ε₁ ε₂ : ENNReal} {hon out leak sim_if view : Type} {π : hon → T (out ⊕ leak)} {F : hon → T (out ⊕ sim_if)} {Sim : SimConstruction T leak sim_if view} (h : UCEmulatesAlg ε₁ π F Sim) (hle : ε₁ ≤ ε₂) : UCEmulatesAlg ε₂ π F Sim

Monotonicity for algebraic UC.

theorem UCMonad.UCEmulatesAlg.refl {T : Type → Type} [UCMonadMetric T] {hon out leak view : Type} (π : hon → T (out ⊕ leak)) : UCEmulatesAlg 0 π π SimConstruction.id

Reflexivity: any protocol emulates itself with Sim = id.

theorem UCMonad.UCEmulatesAlg_of_sdist {T : Type → Type} [UCMonadMetric T] {hon out leak view : Type} (ε : ENNReal) (π F : hon → T (out ⊕ leak)) (h : UCMonadMetric.ucSdist π F ≤ ε) : UCEmulatesAlg ε π F SimConstruction.id

From sdist: same-interface with Sim = id.

theorem UCMonad.UCEmulatesAlg.trans {T : Type → Type} [UCMonadMetric T] {hon out leak view : Type} {ε₁ ε₂ : ENNReal} {π₁ π₂ π₃ : hon → T (out ⊕ leak)} {Sim₁ Sim₂ : SimConstruction T leak leak view} (h₁ : UCEmulatesAlg ε₁ π₁ π₂ Sim₁) (h₂ : UCEmulatesAlg ε₂ π₂ π₃ Sim₂) : UCEmulatesAlg (ε₁ + ε₂) π₁ π₃ (Sim₂ ∘ Sim₁)

Same-interface transitivity via simulator composition.

theorem UCMonad.UCEmulatesAlg.trans_general {T : Type → Type} [UCMonadMetric T] {hon out leak₁ leak₂ leak₃ view : Type} {ε₁ ε₂ : ENNReal} {π₁ : hon → T (out ⊕ leak₁)} {π₂ : hon → T (out ⊕ leak₂)} {π₃ : hon → T (out ⊕ leak₃)} {Sim₁ : SimConstruction T leak₁ leak₂ view} {Sim₂ : SimConstruction T leak₂ leak₃ view} (h₁ : UCEmulatesAlg ε₁ π₁ π₂ Sim₁) (h₂ : UCEmulatesAlg ε₂ π₂ π₃ Sim₂) : UCEmulatesAlg (ε₁ + ε₂) π₁ π₃ (Sim₁.comp Sim₂)

General transitivity through different interface types.