Eval Completeness: Embedding SPComp into RawCode

The embed constructor of RawCode embeds an arbitrary SPComp α computation into RawCode α, making eval : RawCode α → SPComp α surjective. This file packages that constructor as RawCode.ofSPComp together with the equations witnessing that the deep embedding (syntactic free monad) can represent any computation expressible in the shallow embedding (semantic domain).

Main results

• RawCode.ofSPComp — embeds any SPComp α into RawCode α
• RawCode.ofSPComp_eval — eval ∘ ofSPComp = id (right inverse of eval)
• RawCode.substOracle_ofSPComp — ofSPComp code is invariant under oracle substitution
• ValidCode.ofSPComp — ofSPComp code is valid for any location set
• RawCode.ofSPComp_evalWith — evalWith on ofSPComp ignores the handler
• ValidCodeBundle.ofSPComp — the bundled valid-code witness

Rewinding warning: because embed can represent any SPComp — including state-resetting operations like heapReset (which discards the current heap and replaces it with a saved snapshot) — it enables rewinding adversaries. This is what makes the nomPkg_absorb construction go through, but it is unsound in quantum UC due to no-cloning. For quantum-safe results, use the IsPure + NoFail path (sdist_of_deepNomAdvantage), which does not depend on these definitions.

Embedding SPComp into RawCode

@[match_pattern]

def CatCrypt.Deep.RawCode.ofSPComp {α : Type} (c : Core.SPComp α) : RawCode α

Embed an arbitrary SPComp into RawCode. This is the right inverse of eval : RawCode α → SPComp α.

Equations

• CatCrypt.Deep.RawCode.ofSPComp c = CatCrypt.Deep.RawCode.embed c

@[simp]

theorem CatCrypt.Deep.RawCode.ofSPComp_eval {α : Type} (c : Core.SPComp α) : (ofSPComp c).eval = c

ofSPComp is a right inverse of eval. Evaluating the embedded code recovers the original computation.

@[simp]

theorem CatCrypt.Deep.RawCode.substOracle_ofSPComp {α : Type} (c : Core.SPComp α) (env : ℕ → (dom codom : Type) → dom → RawCode codom) : (ofSPComp c).substOracle env = ofSPComp c

ofSPComp produces code that is invariant under oracle substitution. Since the embedded code represents a closed computation (no external oracle dependencies), substituting oracles has no effect.

theorem CatCrypt.Deep.ValidCode.ofSPComp {α : Type} (c : Core.SPComp α) (L : Core.LocSet) : ValidCode L α (RawCode.ofSPComp c)

ofSPComp code is valid for any location set. Since the embedded code's heap access pattern is opaque, the ValidCode.embed constructor declares it valid for any location set.

Derived Results

theorem CatCrypt.Deep.RawCode.ofSPComp_evalWith {α : Type} (c : Core.SPComp α) (handler : ℕ → (dom codom : Type) → dom → Core.SPComp codom) : evalWith handler (ofSPComp c) = c

evalWith on ofSPComp ignores the oracle handler. Since ofSPComp has no oracle calls, the handler is irrelevant.

noncomputable def CatCrypt.Deep.ValidCodeBundle.ofSPComp {α : Type} (c : Core.SPComp α) (L : Core.LocSet) : ValidCodeBundle L α

ValidCodeBundle from ofSPComp, for constructing DeepPackage implementations.

Equations

• CatCrypt.Deep.ValidCodeBundle.ofSPComp c L = { code := CatCrypt.Deep.RawCode.ofSPComp c, valid := ⋯ }