Evaluation Bridge: DeepPackage → PkgImpl

This file bridges DeepPackage (syntactic, oracle-based) to PkgImpl (semantic, SPComp morphisms in Fam(KlSPComp)) via the existing RawCode.eval infrastructure.

Key insight

DeepPackage.link performs syntactic oracle substitution (replacing oracleCall nodes with implementations from another package), while PkgImpl composition uses Kleisli bind. The theorem eval_substOracle connects these:

(code.substOracle env).eval = code.evalWith (eval ∘ env)

Main definitions

• oracleHandler — semantic oracle handler from a package's exports
• evalImpl — evaluate a closed DeepPackage to a PkgImpl
• evalImplWith — evaluate with a custom oracle handler

Main theorems

• evalImpl_link — linking corresponds to evalWith with oracleHandler
• evalImpl_par_eval_left/right — parallel composition dispatches correctly
• runPkg_eq_eval — connects runPkg to the eval bridge

Oracle Handler

noncomputable def CatCrypt.Bridge.oracleHandler (p : Deep.DeepPackage) (op : ℕ) (dom codom : Type) : dom → Core.SPComp codom

Semantic oracle handler from a package's exports. For each operation (op, dom, codom):

• If exported, evaluate the implementation via RawCode.eval
• Otherwise, return SPComp.fail

Equations

• CatCrypt.Bridge.oracleHandler p op dom codom x = if h : (op, dom, codom) ∈ p.exports.ops then (p.impl op dom codom h x).code.eval else CatCrypt.Core.SPComp.fail

theorem CatCrypt.Bridge.oracleHandler_eq_linkEnv_eval (p : Deep.DeepPackage) (op : ℕ) (dom codom : Type) (x : dom) : oracleHandler p op dom codom x = (p.linkEnv op dom codom x).eval

The oracle handler equals evaluating the linkEnv at every operation.

Evaluate DeepPackage to PkgImpl

noncomputable def CatCrypt.Bridge.evalImpl (p : Deep.DeepPackage) : Category.PkgImpl (Category.DeepInterface.toPkgInterface p.exports)

Evaluate a closed DeepPackage to a PkgImpl. Each exported operation (indexed by Fin) is evaluated via RawCode.eval. Unresolved oracle calls become SPComp.fail.

Equations

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

noncomputable def CatCrypt.Bridge.evalImplWith (p : Deep.DeepPackage) (oracle : ℕ → (dom codom : Type) → dom → Core.SPComp codom) : Category.PkgImpl (Category.DeepInterface.toPkgInterface p.exports)

Evaluate a DeepPackage with a custom oracle handler.

Equations

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

Helper Lemmas

theorem CatCrypt.Bridge.link_impl_code (p₁ p₂ : Deep.DeepPackage) (op : ℕ) (dom codom : Type) (h : (op, dom, codom) ∈ p₁.exports.ops) (x : dom) : ((p₁.link p₂).impl op dom codom h x).code = (p₁.impl op dom codom h x).code.substOracle p₂.linkEnv

The linked package's impl code is the substOracle of the first package's code. This is definitionally true from the definitions of link and linkEnv.

Link Correctness

theorem CatCrypt.Bridge.evalImpl_link (p₁ p₂ : Deep.DeepPackage) : evalImpl (p₁.link p₂) = evalImplWith p₁ (oracleHandler p₂)

Link correctness: evaluating a linked package equals evaluating the first package with the second's oracle handler.

This connects DeepPackage.link (syntactic substOracle) to semantic oracle resolution (evalWith).

Par Correctness

theorem CatCrypt.Bridge.evalImpl_par_eval_left (p₁ p₂ : Deep.DeepPackage) (h_sep : p₁.sep p₂) (op : ℕ) (dom codom : Type) (h₁ : (op, dom, codom) ∈ p₁.exports.ops) (h_par : (op, dom, codom) ∈ (p₁.par p₂ h_sep).exports.ops) (x : dom) : ((p₁.par p₂ h_sep).impl op dom codom h_par x).code.eval = (p₁.impl op dom codom h₁ x).code.eval

Parallel composition dispatches left operations to the left package at eval level.

theorem CatCrypt.Bridge.evalImpl_par_eval_right (p₁ p₂ : Deep.DeepPackage) (h_sep : p₁.sep p₂) (op : ℕ) (dom codom : Type) (h₁ : (op, dom, codom) ∉ p₁.exports.ops) (h₂ : (op, dom, codom) ∈ p₂.exports.ops) (h_par : (op, dom, codom) ∈ (p₁.par p₂ h_sep).exports.ops) (x : dom) : ((p₁.par p₂ h_sep).impl op dom codom h_par x).code.eval = (p₂.impl op dom codom h₂ x).code.eval

Parallel composition dispatches right operations to the right package at eval level.

runPkg Connection

theorem CatCrypt.Bridge.runPkg_eq_eval (p : Deep.DeepPackage) (h : (0, Unit, Bool) ∈ p.exports.ops) : Crypto.runPkg p = (p.impl 0 Unit Bool h ()).code.eval

runPkg computes the evaluation of the main (0, Unit, Bool) operation.

Functoriality: Identity Laws

theorem CatCrypt.Bridge.evalImplWith_fail (p : Deep.DeepPackage) : (evalImplWith p fun (x : ℕ) (x_1 x_2 : Type) (x_3 : x_1) => Core.SPComp.fail) = evalImpl p

evalImplWith with the fail handler equals evalImpl. Since evalWith (fun _ _ _ _ => fail) = eval, this is pointwise true.

theorem CatCrypt.Bridge.oracleHandler_id (I : Deep.DeepInterface) (op : ℕ) (dom codom : Type) (x : dom) : oracleHandler (Deep.DeepPackage.id I) op dom codom x = Core.SPComp.fail

The oracle handler of the identity package is always SPComp.fail. The id package forwards all ops as oracleCall, which evaluates to fail.

theorem CatCrypt.Bridge.evalImpl_link_id_right (p : Deep.DeepPackage) : evalImpl (p.link (Deep.DeepPackage.id p.imports)) = evalImpl p

Right identity: linking with the identity package preserves evalImpl.

evalImpl (link p (id p.imports)) = evalImpl p

The id package's oracle handler maps everything to fail, which is the same behavior as unresolved oracle calls in eval.

theorem CatCrypt.Bridge.evalImpl_link_id_left (p : Deep.DeepPackage) : evalImpl ((Deep.DeepPackage.id p.exports).link p) = evalImpl p

Left identity: linking the identity package on the left preserves evalImpl.

evalImpl (link (id p.exports) p) = evalImpl p

The id package's code is oracleCall, which after substOracle with p's linkEnv becomes p's implementation (when the operation is exported).

Functoriality: Associativity

theorem CatCrypt.Bridge.evalImpl_link_assoc (p₁ p₂ p₃ : Deep.DeepPackage) : evalImpl ((p₁.link p₂).link p₃) = evalImpl (p₁.link (p₂.link p₃))

Link associativity at the evalImpl level.

evalImpl (link (link p₁ p₂) p₃) = evalImpl (link p₁ (link p₂ p₃))

Syntactically, link (link p₁ p₂) p₃ ≠ link p₁ (link p₂ p₃) because double substOracle differs from single substOracle with composed env. But semantically (after eval), both agree because:

• Left: (code.substOracle(env₂).substOracle(env₃)).eval
• Right: code.substOracle(env_{link p₂ p₃}).eval
• Both equal code.evalWith(handler) for the same handler.

This generalizes runPkg_link_assoc from the main operation to all operations.

Typed Semantic Packages

A SemPkg is a semantic package at the SPComp level. It maps oracle handlers to oracle handlers: given implementations for import operations, it produces implementations for export operations.

SemPkg forms a proper category (with function composition as linking), and evalImpl factors through it cleanly, avoiding the need for quotienting DeepPackage by eval-equivalence.

@[reducible, inline]

abbrev CatCrypt.Bridge.Handler : Type 1

Untyped oracle handler: provides SPComp implementations for any operation identified by (op : ℕ, dom : Type, codom : Type).

Equations

• CatCrypt.Bridge.Handler = (ℕ → (dom codom : Type) → dom → CatCrypt.Core.SPComp codom)

noncomputable def CatCrypt.Bridge.Handler.fail : Handler

The trivial handler that maps all operations to failure.

Equations

• CatCrypt.Bridge.Handler.fail x✝³ x✝² x✝¹ x✝ = CatCrypt.Core.SPComp.fail

structure CatCrypt.Bridge.SemPkg (I_imp : Deep.DeepInterface) (I_exp : Deep.DeepInterface) : Type 1

A semantic typed package: a function from import oracle handlers to export oracle handlers. The interface parameters I_imp and I_exp track which operations are imported and exported.

This forms a category with function composition as linking:

• Identity: the handler that passes operations through unchanged
• Composition: (g.comp f).resolve oracle = g.resolve (f.resolve oracle)

• resolve : Handler → Handler

  Given an oracle handler (resolving imports), produce an oracle handler (providing exports).

theorem CatCrypt.Bridge.SemPkg.ext {I_imp : Deep.DeepInterface} {I_exp : Deep.DeepInterface} {s₁ s₂ : SemPkg I_imp I_exp} (h : s₁.resolve = s₂.resolve) : s₁ = s₂

theorem CatCrypt.Bridge.SemPkg.ext_iff {I_imp : Deep.DeepInterface} {I_exp : Deep.DeepInterface} {s₁ s₂ : SemPkg I_imp I_exp} : s₁ = s₂ ↔ s₁.resolve = s₂.resolve

noncomputable def CatCrypt.Bridge.SemPkg.id (I : Deep.DeepInterface) : SemPkg I I

Identity semantic package: passes the handler through unchanged.

Equations

• CatCrypt.Bridge.SemPkg.id I = { resolve := id }

noncomputable def CatCrypt.Bridge.SemPkg.comp {I_imp : Deep.DeepInterface} {I_exp : Deep.DeepInterface} {I_mid : Deep.DeepInterface} (g : SemPkg I_mid I_exp) (f : SemPkg I_imp I_mid) : SemPkg I_imp I_exp

Composition of semantic packages: resolve imports of g through f.

Equations

• g.comp f = { resolve := fun (oracle : CatCrypt.Bridge.Handler) => g.resolve (f.resolve oracle) }

@[simp]

theorem CatCrypt.Bridge.SemPkg.id_resolve (I : Deep.DeepInterface) (h : Handler) : (id I).resolve h = h

@[simp]

theorem CatCrypt.Bridge.SemPkg.comp_resolve {I_imp : Deep.DeepInterface} {I_exp : Deep.DeepInterface} {I_mid : Deep.DeepInterface} (g : SemPkg I_mid I_exp) (f : SemPkg I_imp I_mid) (h : Handler) : (g.comp f).resolve h = g.resolve (f.resolve h)

theorem CatCrypt.Bridge.SemPkg.comp_assoc {I_exp : Deep.DeepInterface} {I₁ : Deep.DeepInterface} {I₂ : Deep.DeepInterface} {I₃ : Deep.DeepInterface} (h : SemPkg I₃ I_exp) (g : SemPkg I₂ I₃) (f : SemPkg I₁ I₂) : h.comp (g.comp f) = (h.comp g).comp f

Composition is associative.

theorem CatCrypt.Bridge.SemPkg.id_comp {I_imp : Deep.DeepInterface} {I_exp : Deep.DeepInterface} (f : SemPkg I_imp I_exp) : (id I_exp).comp f = f

Left identity for composition.

theorem CatCrypt.Bridge.SemPkg.comp_id {I_imp : Deep.DeepInterface} {I_exp : Deep.DeepInterface} (f : SemPkg I_imp I_exp) : f.comp (id I_imp) = f

Right identity for composition.

DeepPackage → SemPkg

noncomputable def CatCrypt.Bridge.toSemPkg (p : Deep.DeepPackage) : SemPkg p.imports p.exports

Convert a DeepPackage to a semantic package. For each operation in the exports, evaluates the implementation with the given oracle handler. Non-exported operations return fail.

Equations

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

theorem CatCrypt.Bridge.toSemPkg_fail (p : Deep.DeepPackage) : (toSemPkg p).resolve Handler.fail = oracleHandler p

toSemPkg with the fail handler gives the same as oracleHandler. Both evaluate the code, but oracleHandler uses eval (= evalWith fail).

theorem CatCrypt.Bridge.toSemPkg_link (p₁ p₂ : Deep.DeepPackage) (oracle : Handler) (op : ℕ) (dom codom : Type) (x : dom) : (toSemPkg (p₁.link p₂)).resolve oracle op dom codom x = (toSemPkg p₁).resolve ((toSemPkg p₂).resolve oracle) op dom codom x

toSemPkg preserves linking (pointwise): evaluating a linked package is the same as composing the semantic handlers.

For any oracle handler oracle and operation (op, dom, codom): toSemPkg(link p₁ p₂).resolve oracle = toSemPkg(p₁).resolve(toSemPkg(p₂).resolve oracle)

This is the fundamental functoriality theorem. It follows from evalWith_substOracle: oracle substitution composes with evalWith.

theorem CatCrypt.Bridge.toSemPkg_id_mem (I : Deep.DeepInterface) (oracle : Handler) (op : ℕ) (dom codom : Type) (x : dom) (h : (op, dom, codom) ∈ I.ops) : (toSemPkg (Deep.DeepPackage.id I)).resolve oracle op dom codom x = oracle op dom codom x

toSemPkg preserves identity for exported operations.

For operations in I.ops, toSemPkg (id I) acts as the identity handler. (For operations NOT in I.ops, toSemPkg (id I) returns fail, since DeepPackage.id I only forwards operations declared in I.)

Category Instance for DeepInterface

SemPkg satisfies the axioms of a Mathlib Category on DeepInterface objects:

• Hom I J := SemPkg I J (semantic packages as morphisms)
• Composition is diagrammatic: f ≫ g = g.comp f (apply f first, then g)
• Identity and associativity follow from SemPkg.id_comp, SemPkg.comp_id, SemPkg.comp_assoc

This gives access to ≫ notation, Category.assoc, and categorical tactics.

@[implicit_reducible]

noncomputable instance CatCrypt.Bridge.instCategoryDeepInterface : CategoryTheory.Category.{1, u_1 + 1} Deep.DeepInterface

Equations

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