Oracle-Exporting Game Packages from Reflected Code

DeepPackage.ofCode (Deep/GamePackage.lean) packages a closed RawCode Bool as the main export (0, Unit, Bool). This file provides the missing dual: a reusable constructor DeepPackage.ofOracle that turns a shallow oracle implementation impl₀ : dom → RawCode codom into a package that exports a single oracle (op, dom, codom) for other packages to call. Fed through rawCode%, a shallow SPComp oracle becomes an oracle-exporting deep package with no hand-written RawCode, no hand-written impl literal, and no hand-written validity proof.

Main definitions

• DeepPackage.ofOracle — the single-export oracle package for impl₀.
• NomPackage.ofOracle — its stateless (∅-location) nominal wrapper.

Main results

• evalOp_ofOracle — evaluating the exported oracle recovers the shallow body (impl₀ x).eval.
• runPkg_ofOracle_zero — the main-export packaging DeepPackage.ofCode is the op = 0, (dom, codom) = (Unit, Bool) instance of ofOracle.
• oracleGame_advantage_eq_shallow — a worked reduction: the deep-package advantage of two reflected oracle games against a forwarding adversary equals the shallow Advantage of the two game bodies.

The oracle-package constructor

noncomputable def CatCrypt.Deep.DeepPackage.ofOracle {L : Core.LocSet} (op : ℕ) (dom codom : Type) (impl₀ : dom → RawCode codom) [∀ (x : dom), IsValid L (impl₀ x)] : DeepPackage

The single-export DeepPackage that exports the oracle (op, dom, codom) and implements it by the shallow family impl₀.

It has locations L, no imports, and exactly one export. The impl field matches an incoming request (op', dom', codom') against the singleton export list: membership forces dom' = dom and codom' = codom, and the bundle ValidCodeBundle.auto (impl₀ x) is cast across both type equalities (recall (op, dom, codom) parses as (op, (dom, codom)), so the two equalities are extracted from nested Prod.mk.injEq). Validity is discharged automatically from [∀ x, IsValid L (impl₀ x)].

Equations

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

theorem CatCrypt.Deep.evalOp_ofOracle {L : Core.LocSet} (op : ℕ) (dom codom : Type) (impl₀ : dom → RawCode codom) [∀ (x : dom), IsValid L (impl₀ x)] (x : dom) : (DeepPackage.ofOracle op dom codom impl₀).evalOp op dom codom ⋯ x = (impl₀ x).eval

Evaluating the exported oracle of DeepPackage.ofOracle recovers the shallow body (impl₀ x).eval: a game oracle's package evaluation is exactly the shallow game body's eval.

noncomputable def CatCrypt.Deep.NomPackage.ofOracle (op : ℕ) (dom codom : Type) (impl₀ : dom → RawCode codom) [∀ (x : dom), IsValid ∅ (impl₀ x)] : NomPackage

The stateless nominal wrapper of DeepPackage.ofOracle: no locations, so the location invariant reduces to ∅ = ∅.image _.

Equations

• CatCrypt.Deep.NomPackage.ofOracle op dom codom impl₀ = { pkg := CatCrypt.Deep.DeepPackage.ofOracle op dom codom impl₀, locs_eq := CatCrypt.Deep.NomPackage.ofOracle._proof_1 }

theorem CatCrypt.Deep.runPkg_ofOracle_zero {L : Core.LocSet} (c : RawCode Bool) [IsValid L c] : Crypto.runPkg (DeepPackage.ofOracle 0 Unit Bool fun (x : Unit) => c) = c.eval

DeepPackage.ofCode c is the op = 0, (dom, codom) = (Unit, Bool) instance of DeepPackage.ofOracle: running it recovers c.eval, so the main-export packaging is a special case of the oracle-export packaging.

Feeding the constructor from shallow code by reflection

A shallow oracle f : dom → SPComp codom becomes an oracle package with no hand-written RawCode: reflect the (inlined) body under the domain binder with rawCode%, which handles the bound variable as a free variable. A bare fun x => rawCode% (f x) referencing a top-level def f does not elaborate — the reifier normalizes to weak-head-normal form under reducible transparency, which leaves f x opaque; inlining f's body exposes the SPComp head.

noncomputable def CatCrypt.Deep.sampleOracle : Bool → Core.SPComp Bool

A shallow one-bit oracle: XOR the query with a fresh uniform key.

Equations

• CatCrypt.Deep.sampleOracle m = (CatCrypt.Core.SPComp.sample Bool).bind fun (k : Bool) => CatCrypt.Core.SPComp.pure (k ^^ m)

noncomputable def CatCrypt.Deep.sampleOraclePkg : DeepPackage

The oracle package for sampleOracle, produced by reflecting the inlined body under the domain binder — no hand-written RawCode, impl literal, or validity proof.

Equations

• CatCrypt.Deep.sampleOraclePkg = CatCrypt.Deep.DeepPackage.ofOracle 1 Bool Bool fun (m : Bool) => (CatCrypt.Deep.RawCode.sample Bool).bind fun (k : Bool) => CatCrypt.Deep.RawCode.ret (k ^^ m)

Worked reduction: reflected oracle games vs a forwarding adversary

The two closed shallow game bodies are the one-time-pad ciphertext for a fixed message (realRaw) and a fresh uniform bit (idealRaw) — the real/ideal pair of one-time secrecy. Each is reflected into RawCode and packaged as an oracle game exporting (1, Unit, Bool); the adversary forwards the oracle unchanged. The advantage of the whole deep-package/adversary construction collapses, by reflection and linking correctness, to the shallow Advantage of the two bodies — the quantity a bijection coupling bounds.

noncomputable def CatCrypt.Deep.realRaw : RawCode Bool

Real body: one-time-pad encryption of the fixed message true.

Equations

• CatCrypt.Deep.realRaw = (CatCrypt.Deep.RawCode.sample Bool).bind fun (k : Bool) => CatCrypt.Deep.RawCode.ret (k ^^ true)

noncomputable def CatCrypt.Deep.idealRaw : RawCode Bool

Ideal body: a fresh uniform bit.

Equations

• CatCrypt.Deep.idealRaw = (CatCrypt.Deep.RawCode.sample Bool).bind fun (k : Bool) => CatCrypt.Deep.RawCode.ret k

instance CatCrypt.Deep.instValidRealRaw : IsValid ∅ realRaw

instance CatCrypt.Deep.instValidIdealRaw : IsValid ∅ idealRaw

noncomputable def CatCrypt.Deep.realGame : NomPackage

Real oracle game, exporting (1, Unit, Bool).

Equations

• CatCrypt.Deep.realGame = CatCrypt.Deep.NomPackage.ofOracle 1 Unit Bool fun (x : Unit) => CatCrypt.Deep.realRaw

noncomputable def CatCrypt.Deep.idealGame : NomPackage

Ideal oracle game, exporting (1, Unit, Bool).

Equations

• CatCrypt.Deep.idealGame = CatCrypt.Deep.NomPackage.ofOracle 1 Unit Bool fun (x : Unit) => CatCrypt.Deep.idealRaw

noncomputable def CatCrypt.Deep.forwardAdv : NomPackage

Forwarding adversary: exports the main procedure (0, Unit, Bool) and implements it by a single oracle call (1, Unit, Bool), returning the result unchanged. Built through the same ofOracle constructor.

Equations

• CatCrypt.Deep.forwardAdv = CatCrypt.Deep.NomPackage.ofOracle 0 Unit Bool fun (x : Unit) => CatCrypt.Deep.RawCode.oracleCall 1 Unit Bool ()

theorem CatCrypt.Deep.runPkg_link_forward (body : RawCode Bool) [IsValid ∅ body] : Crypto.runPkg (forwardAdv.pkg.link (NomPackage.ofOracle 1 Unit Bool fun (x : Unit) => body).pkg) = body.eval

Running the forwarding adversary linked with an oracle game NomPackage.ofOracle 1 Unit Bool (fun _ => body) yields exactly the game body's evaluation body.eval. The oracle call in the adversary's main procedure is resolved, through linking, against the game's single export.

theorem CatCrypt.Deep.oracleGame_advantage_eq_shallow : Crypto.DeepNomAdvantage realGame idealGame forwardAdv = Crypto.Advantage realRaw.eval idealRaw.eval

Worked reduction. The deep-package advantage of the two reflected oracle games against the forwarding adversary equals the shallow Advantage of the two game bodies — the one-time-secrecy advantage that a bijection coupling bounds.