Single-Export Game Packages from Reflected Code

A RawCode Bool is packaged as a DeepPackage (respectively NomPackage) whose sole export is the main procedure (0, Unit, Bool) — the entry point that runPkg / runDeep evaluate. Composed with rawCode% (reflection of a shallow SPComp α into a syntactic RawCode α), these constructors realize the round trip from a shallow game to a package and back: runDeep (NomPackage.ofCode (rawCode% g)) equals the original shallow program g.

Main definitions

• DeepPackage.ofCode — the DeepPackage exporting (0, Unit, Bool) and implementing it with a given valid code.
• NomPackage.ofCode — the stateless (∅-location) nominal wrapper.

Main results

• runPkg_ofCode — runPkg (DeepPackage.ofCode c) = c.eval.
• runDeep_ofCode — runDeep (NomPackage.ofCode c) = c.eval.
• runDeep_ofCode_reflect — the end-to-end reflection round trip on a coin-flip game.

noncomputable def CatCrypt.Deep.DeepPackage.ofCode {L : Core.LocSet} (c : RawCode Bool) [IsValid L c] : DeepPackage

The single-export DeepPackage whose main procedure (0, Unit, Bool) is implemented by c. It has locations L, no imports, and exactly one export; the codomain of that export is Bool, into which c's bundle is cast from the singleton-membership equality.

Equations

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

theorem CatCrypt.Deep.runPkg_ofCode {L : Core.LocSet} (c : RawCode Bool) [IsValid L c] : Crypto.runPkg (DeepPackage.ofCode c) = c.eval

Evaluating the main export of DeepPackage.ofCode c yields c.eval.

noncomputable def CatCrypt.Deep.NomPackage.ofCode (c : RawCode Bool) [IsValid ∅ c] : NomPackage

The stateless nominal package whose main procedure is implemented by c. Its underlying DeepPackage uses no locations, so its atom set is empty and the location invariant reduces to ∅ = ∅.image _.

Equations

• CatCrypt.Deep.NomPackage.ofCode c = { pkg := CatCrypt.Deep.DeepPackage.ofCode c, locs_eq := CatCrypt.Deep.NomPackage.ofCode._proof_1 }

theorem CatCrypt.Deep.runDeep_ofCode (c : RawCode Bool) [IsValid ∅ c] : Crypto.runDeep (NomPackage.ofCode c) = c.eval

Evaluating the nominal wrapper yields c.eval.

theorem CatCrypt.Deep.runDeep_ofCode_reflect : Crypto.runDeep (NomPackage.ofCode ((RawCode.sample Bool).bind fun (b : Bool) => RawCode.ret b)) = (Core.SPComp.sample Bool).bind fun (b : Bool) => Core.SPComp.pure b

End-to-end reflection round trip: a shallow coin-flip game reflects into deep code via rawCode%, wraps into a nominal package via NomPackage.ofCode, and runDeep recovers the original shallow program.