Package Interfaces and Fam(KlSPComp) Morphisms

A package interface specifies operation signatures via an index type ι with domain and codomain families in KlSPComp.

A package implementation (PkgImpl) is a morphism in Fam(KlSPComp) from the domain family to the codomain family. Fam composition is Kleisli sequencing (bind at each operation), NOT oracle substitution. See SemPkg.lean for the package category with substitution-style composition.

Linking vs composition: PkgImpl.link computes as SPComp.bind at each operation index — this is a data pipeline (first-order), not oracle resolution (second-order). Cryptographic package linking is oracle substitution, which is modeled by the Category PkgInterface in SemPkg.lean.

Parallel composition (PkgImpl.par) dispatches operations by Sum index. This IS the correct parallel composition and is shared with the package category.

Main definitions

• PkgInterface — operation signatures (index type, domains, codomains)
• PkgInterface.tensor — parallel combination (Sum on indices)
• PkgInterface.unit — empty interface (Empty index)
• PkgImpl — Fam(KlSPComp) morphism (Kleisli arrow at each operation)
• PkgImpl.ofImpls — construct from componentwise implementations (σ = id)
• PkgImpl.link — Kleisli-bind composition (NOT oracle substitution)
• PkgImpl.par — parallel composition via Fam tensor
• DeepInterface.toPkgInterface — bridge from deep-embedding interfaces

Semantic characterization

• link_map: linking at operation i is SPComp.bind (p₁.map i x) (p₂.map (p₁.σ i))
• par_map_inl: parallel at .inl i dispatches to p₁.map i
• par_map_inr: parallel at .inr j dispatches to p₂.map j

SMC structure

Since PkgInterface.tensor/unit correspond definitionally to FamObj.tensorObj/unitObj, the monoidal category laws apply directly to PkgImpl parallel composition. The full SMC structure on PkgInterface (with substitution-style composition) is in SemPkg.lean.

Package Interface

structure CatCrypt.Category.PkgInterface : Type 1

A package interface specifies operation signatures. Each operation is indexed by ι with domain type doms i and codomain type codoms i, both living in KlSPComp (= Type, viewed as objects of the Kleisli category of SPComp).

• ι : Type

  Index type for operations

• doms : self.ι → Core.KlSPComp

  Domain type of each operation

• codoms : self.ι → Core.KlSPComp

  Codomain type of each operation

def CatCrypt.Category.PkgInterface.domFam (I : PkgInterface) : FamObj Core.KlSPComp

The domain family as a FamObj KlSPComp.

Equations

• I.domFam = { ι := I.ι, objs := I.doms }

def CatCrypt.Category.PkgInterface.codomFam (I : PkgInterface) : FamObj Core.KlSPComp

The codomain family as a FamObj KlSPComp.

Equations

• I.codomFam = { ι := I.ι, objs := I.codoms }

Tensor and Unit

def CatCrypt.Category.PkgInterface.tensor (I J : PkgInterface) : PkgInterface

Parallel combination of interfaces: index by Sum, families by Sum.elim.

Equations

• I.tensor J = { ι := I.ι ⊕ J.ι, doms := Sum.elim I.doms J.doms, codoms := Sum.elim I.codoms J.codoms }

def CatCrypt.Category.PkgInterface.unit : PkgInterface

The empty interface (no operations).

Equations

• CatCrypt.Category.PkgInterface.unit = { ι := Empty, doms := Empty.elim, codoms := Empty.elim }

Correspondence with Fam's tensor and unit

These are all rfl because both sides expand to the same ⟨ι₁ ⊕ ι₂, Sum.elim ...⟩ (resp. ⟨Empty, Empty.elim⟩). This definitional equality is the key insight: packages inherit their SMC structure from Fam.lean with zero proof effort.

@[simp]

theorem CatCrypt.Category.PkgInterface.tensor_domFam (I J : PkgInterface) : (I.tensor J).domFam = I.domFam.tensorObj J.domFam

@[simp]

theorem CatCrypt.Category.PkgInterface.tensor_codomFam (I J : PkgInterface) : (I.tensor J).codomFam = I.codomFam.tensorObj J.codomFam

@[simp]

theorem CatCrypt.Category.PkgInterface.unit_domFam : unit.domFam = FamObj.unitObj

@[simp]

theorem CatCrypt.Category.PkgInterface.unit_codomFam : unit.codomFam = FamObj.unitObj

Package Implementation

@[reducible, inline]

abbrev CatCrypt.Category.PkgImpl (I : PkgInterface) : Type

A package implementation for interface I is a morphism in Fam(KlSPComp) from the domain family to the codomain family.

Concretely, this consists of:

• An equivalence σ : I.ι ≃ I.ι permuting operation indices
• Implementations map i : I.doms i → SPComp (I.codoms (σ i)) for each operation

When σ = id (the common case), each operation i has a direct implementation I.doms i → SPComp (I.codoms i).

Equations

• CatCrypt.Category.PkgImpl I = (I.domFam ⟶ I.codomFam)

Construction

def CatCrypt.Category.PkgImpl.ofImpls (I : PkgInterface) (impls : (i : I.ι) → I.doms i → Core.SPComp (I.codoms i)) : PkgImpl I

Construct a package from componentwise implementations (with σ = id).

Equations

• CatCrypt.Category.PkgImpl.ofImpls I impls = { σ := Equiv.refl I.domFam.ι, map := impls }

@[simp]

theorem CatCrypt.Category.PkgImpl.ofImpls_σ (I : PkgInterface) (impls : (i : I.ι) → I.doms i → Core.SPComp (I.codoms i)) : (ofImpls I impls).σ = Equiv.refl I.domFam.ι

@[simp]

theorem CatCrypt.Category.PkgImpl.ofImpls_map (I : PkgInterface) (impls : (i : I.ι) → I.doms i → Core.SPComp (I.codoms i)) (i : I.ι) : (ofImpls I impls).map i = impls i

Linking = Fam Composition (Kleisli Sequencing)

Note: This is Kleisli-bind composition (sequencing), not oracle substitution. At each operation i, link computes as SPComp.bind (p₁.map i x) (p₂.map (p₁.σ i)), i.e., run p₁, then feed the result into p₂. This models a data pipeline, not cryptographic package linking (which is oracle resolution — see SemPkg.lean).

noncomputable def CatCrypt.Category.PkgImpl.link {D M C : FamObj Core.KlSPComp} (p₁ : D ⟶ M) (p₂ : M ⟶ C) : D ⟶ C

Linking two packages: composition in Fam(KlSPComp).

Equations

• CatCrypt.Category.PkgImpl.link p₁ p₂ = CategoryTheory.CategoryStruct.comp p₁ p₂

@[simp]

theorem CatCrypt.Category.PkgImpl.link_σ {D M C : FamObj Core.KlSPComp} (p₁ : D ⟶ M) (p₂ : M ⟶ C) : (link p₁ p₂).σ = p₁.σ.trans p₂.σ

The index permutation of a linked package is the composition of permutations.

@[simp]

theorem CatCrypt.Category.PkgImpl.link_map {D M C : FamObj Core.KlSPComp} (p₁ : D ⟶ M) (p₂ : M ⟶ C) (i : D.ι) (x : D.objs i) : (link p₁ p₂).map i x = (p₁.map i x).bind (p₂.map (p₁.σ i))

Linking computes as Kleisli bind at each operation: run p₁ on the input, then feed the result to p₂.

Parallel Composition = Fam Tensor

Parallel composition dispatches operations to the correct component:

• Operations indexed by Sum.inl i go to the left package p₁
• Operations indexed by Sum.inr j go to the right package p₂

noncomputable def CatCrypt.Category.PkgImpl.par {I J : PkgInterface} (p₁ : PkgImpl I) (p₂ : PkgImpl J) : PkgImpl (I.tensor J)

Parallel composition of packages: tensor in Fam(KlSPComp).

Equations

• p₁.par p₂ = CategoryTheory.MonoidalCategoryStruct.tensorHom p₁ p₂

@[simp]

theorem CatCrypt.Category.PkgImpl.par_σ_inl {I J : PkgInterface} (p₁ : PkgImpl I) (p₂ : PkgImpl J) (i : I.ι) : (p₁.par p₂).σ (Sum.inl i) = Sum.inl (p₁.σ i)

Left operations are permuted by p₁'s permutation.

@[simp]

theorem CatCrypt.Category.PkgImpl.par_σ_inr {I J : PkgInterface} (p₁ : PkgImpl I) (p₂ : PkgImpl J) (j : J.ι) : (p₁.par p₂).σ (Sum.inr j) = Sum.inr (p₂.σ j)

Right operations are permuted by p₂'s permutation.

@[simp]

theorem CatCrypt.Category.PkgImpl.par_map_inl {I J : PkgInterface} (p₁ : PkgImpl I) (p₂ : PkgImpl J) (i : I.ι) (x : I.doms i) : (p₁.par p₂).map (Sum.inl i) x = p₁.map i x

At a left operation .inl i, parallel composition dispatches to p₁.

@[simp]

theorem CatCrypt.Category.PkgImpl.par_map_inr {I J : PkgInterface} (p₁ : PkgImpl I) (p₂ : PkgImpl J) (j : J.ι) (x : J.doms j) : (p₁.par p₂).map (Sum.inr j) x = p₂.map j x

At a right operation .inr j, parallel composition dispatches to p₂.

SMC Laws for Parallel Composition

The monoidal laws for parallel composition (tensor, associator, braiding) hold for PkgImpl via the definitional equality between PkgInterface.tensor/unit and FamObj.tensorObj/unitObj. These are inherited from Fam.lean.

The full symmetric monoidal category structure on PkgInterface — with substitution-style composition (oracle resolution) rather than Fam's Kleisli sequencing — is in SemPkg.lean.

Bridge: DeepInterface → PkgInterface

def CatCrypt.Category.DeepInterface.toPkgInterface (I : Deep.DeepInterface) : PkgInterface

Convert a DeepInterface (list-based, from the deep embedding) to a PkgInterface (family-based, for the categorical framework) via Fin indexing. Each position in the operation list becomes a Fin index.

Equations

• CatCrypt.Category.DeepInterface.toPkgInterface I = { ι := Fin I.ops.length, doms := fun (i : Fin I.ops.length) => (I.ops.get i).2.1, codoms := fun (i : Fin I.ops.length) => (I.ops.get i).2.2 }

def CatCrypt.Category.DeepInterface.append (I J : Deep.DeepInterface) : Deep.DeepInterface

Append two deep interfaces (concatenate operation lists).

Equations

• CatCrypt.Category.DeepInterface.append I J = { ops := I.ops ++ J.ops }

The tensor of toPkgInterface corresponds to the append of DeepInterface: (I.append J).toPkgInterface and I.toPkgInterface.tensor J.toPkgInterface have the same operations, indexed by Fin (m + n) vs Fin m ⊕ Fin n respectively. The equivalence finSumFinEquiv from Mathlib connects these index types, with List.getElem_append_left/List.getElem_append_right showing the families match.