Raw Packages

This file defines raw packages - collections of typed function implementations. A raw package maps operation identifiers to their implementations.

Main definitions

• TypedFun - A typed function implementation (input type, output type, implementation)
• RawPackage - A collection of typed function implementations
• RawPackage.link - Sequential composition (linking) — shallow-layer no-op stub (returns its first argument unchanged, because RawPackage stores oracle-free typed functions with nothing to substitute). Real oracle-substituting linking lives in the deep embedding: CatCrypt.Deep.Package.link, proven correct and associative by runPkg_link / runPkg_link_assoc in NomAdvantage.
• RawPackage.par - Parallel composition
• RawPackage.id - Identity package

References

• Larsen and Schürmann, Nominal State-Separating Proofs

structure CatCrypt.Package.TypedFun : Type 1

A typed function: source type, target type, and implementation

• src : Type

  Input type

• tgt : Type

  Output type

• impl : self.src → Core.SPComp self.tgt

  Implementation: src → SPComp tgt

@[implicit_reducible]

noncomputable instance CatCrypt.Package.instDecidableEqTypedFun : DecidableEq TypedFun

DecidableEq for TypedFun

Equations

• CatCrypt.Package.instDecidableEqTypedFun = Classical.decEq CatCrypt.Package.TypedFun

structure CatCrypt.Package.PackageEntry : Type 1

Package entry: operation id with its typed implementation

• id : ℕ
• fun_ : TypedFun

@[implicit_reducible]

noncomputable instance CatCrypt.Package.instDecidableEqPackageEntry : DecidableEq PackageEntry

DecidableEq for PackageEntry (needed for Finset operations)

Equations

• CatCrypt.Package.instDecidableEqPackageEntry = Classical.decEq CatCrypt.Package.PackageEntry

structure CatCrypt.Package.RawPackage : Type 1

Raw package: a finite collection of typed function implementations. Each entry maps an operation id to its implementation.

• entries : Finset PackageEntry
• unique_ids (e₁ e₂ : PackageEntry) : e₁ ∈ self.entries → e₂ ∈ self.entries → e₁.id = e₂.id → e₁ = e₂

def CatCrypt.Package.RawPackage.empty : RawPackage

Empty package

Equations

• CatCrypt.Package.RawPackage.empty = { entries := ∅, unique_ids := CatCrypt.Package.RawPackage.empty._proof_1 }

@[implicit_reducible]

instance CatCrypt.Package.RawPackage.instEmptyCollection : EmptyCollection RawPackage

Equations

• CatCrypt.Package.RawPackage.instEmptyCollection = { emptyCollection := CatCrypt.Package.RawPackage.empty }

noncomputable def CatCrypt.Package.RawPackage.ids (P : RawPackage) : Finset ℕ

The set of operation ids implemented by the package

Equations

• P.ids = Finset.image (fun (x : CatCrypt.Package.PackageEntry) => x.id) P.entries

def CatCrypt.Package.RawPackage.has (P : RawPackage) (id : ℕ) (S T : Type) : Prop

Check if a package implements an operation with given id and types

Equations

• P.has id S T = ∃ e ∈ P.entries, e.id = id ∧ e.fun_.src = S ∧ e.fun_.tgt = T

noncomputable def CatCrypt.Package.RawPackage.lookup (P : RawPackage) (id : ℕ) : Option TypedFun

Lookup an implementation by id (noncomputable)

Equations

• P.lookup id = if h : ∃ e ∈ P.entries, e.id = id then some (Classical.choose h).fun_ else none

noncomputable def CatCrypt.Package.RawPackage.singleton (id : ℕ) (S T : Type) (f : S → Core.SPComp T) : RawPackage

Single function package

Equations

• CatCrypt.Package.RawPackage.singleton id S T f = { entries := {{ id := id, fun_ := { src := S, tgt := T, impl := f } }}, unique_ids := ⋯ }

def CatCrypt.Package.RawPackage.Disjoint (P₁ P₂ : RawPackage) : Prop

Two packages are disjoint if they share no operation ids

Equations

• P₁.Disjoint P₂ = Disjoint P₁.ids P₂.ids

noncomputable def CatCrypt.Package.RawPackage.par (P₁ P₂ : RawPackage) (h : P₁.Disjoint P₂) : RawPackage

Parallel composition: combine two packages with disjoint ids

Equations

• P₁.par P₂ h = { entries := P₁.entries ∪ P₂.entries, unique_ids := ⋯ }

theorem CatCrypt.Package.RawPackage.par_ids {P₁ P₂ : RawPackage} (h : P₁.Disjoint P₂) : (P₁.par P₂ h).ids = P₁.ids ∪ P₂.ids

noncomputable def CatCrypt.Package.RawPackage.resolve (P : RawPackage) (id : ℕ) {S T : Type} (x : S) : Core.SPComp T

Resolve: find the implementation for an operation id and call it. Returns fail if the operation is not implemented.

Equations

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

noncomputable def CatCrypt.Package.RawPackage.link (P₁ _P₂ : RawPackage) : RawPackage

Sequential composition (linking): P₁ imports from P₂.

WARNING: This is a stub that returns P₁ unchanged. The shallow RawPackage representation stores typed functions (S → SPComp T) that have no notion of oracle calls, so there is nothing to substitute. This makes link a no-op.

For real package linking, use the deep embedding layer:

• DeepPackage.link in CatCrypt.Deep.Package performs actual oracle substitution via RawCode.substOracle
• runPkg_link in CatCrypt.Crypto.NomAdvantage proves correctness
• runPkg_link_assoc proves associativity at the evaluation level

Equations

• P₁.link _P₂ = P₁

noncomputable def CatCrypt.Package.RawPackage.idPkg (I : Interface) : RawPackage

Identity package: implements an interface by just forwarding

Equations

• CatCrypt.Package.RawPackage.idPkg I = CatCrypt.Package.RawPackage.empty

theorem CatCrypt.Package.RawPackage.empty_ids : ∅.ids = ∅

theorem CatCrypt.Package.RawPackage.empty_not_has (id : ℕ) (S T : Type) : ¬empty.has id S T