Reflection: SPComp → RawCode

An elaboration-time reifier that turns a shallow SPComp α program (built from the six core constructors SPComp.pure, SPComp.bind, SPComp.sample, SPComp.get, SPComp.set, SPComp.fail, and/or do-notation) into the corresponding syntactic RawCode α term.

Usage

def myProg : SPComp Bool := do
  let b ← SPComp.sample Bool
  SPComp.set myLoc b
  return b

def myProgRaw : RawCode Bool := rawCode% myProg

Translation

SPComp constructor	RawCode image
SPComp.pure a	RawCode.ret a
SPComp.bind c k	RawCode.bind (reify c) (fun x => reify (k x))
SPComp.sample α	RawCode.sample α
SPComp.get ℓ	RawCode.bind (RawCode.get ℓ) (fun x => RawCode.ret x.down)
SPComp.set ℓ v	RawCode.bind (RawCode.put ℓ v) (fun _ => RawCode.ret ())
SPComp.fail	RawCode.fail

The get/set cases use an extra RawCode.bind because RawCode.get returns RawCode (ULift ℓ.ty) (the universe-polymorphic deep embedding lifts the location type), while SPComp.get returns SPComp ℓ.ty. The post-composition with RawCode.ret ∘ ULift.down re-lands at the author's expected type.

The reifier pattern-matches on weak-head-normal heads; the Monad SPComp instance unfolds under whnf, so programs written with do-notation or >>= land on the SPComp.bind / SPComp.pure heads automatically.

Scope

Handles the six canonical constructors directly. Any other SPComp-typed subterm — a call to an abstract primitive f a : SPComp β, a locally-bound oracle f : α → SPComp β, or an opaque constant that does not delta-unfold to a constructor — is reflected as RawCode.embed, an opaque leaf holding the shallow subterm. Since RawCode.eval (embed c) = c definitionally, the reified program still round-trips, and IsValid.embed supplies its validity proof. The reifier never fails on an SPComp-typed term. (A structured RawCode.oracleCall image is also available for opaque heads that are intended to be linked later via substOracle; it is not the default because its eval is SPComp.fail, so it does not round-trip.)

Correctness

For any SPComp program built from the canonical constructors, evaluation of the reified form reduces definitionally (up to the pure-right monad law for get/set) to the original shallow program. The built-in simp lemmas in Deep/Eval.lean (eval_ret, eval_bind, eval_get, eval_put, eval_sample, eval_fail) normalize round-trip identities.

partial def CatCrypt.Deep.Reflect.normalizeHead (e : Lean.Expr) : Lean.MetaM Lean.Expr

Reduce to a form whose head is an SPComp constructor. We whnfR first (which does not unfold SPComp.bind/SPComp.pure, since they are not @[reducible]). If the head is a type-class bind/pure (from do-notation / >>=) we re-project through the instance with full whnf. If the head is any other definition — a top-level def game : SPComp α, an abbreviation, a scheme-field projection — we delta-unfold it and retry, so a named program reflects as readily as an inline one. The six SPComp constructors are matched before the unfold fallback, so they stay opaque and reflection stops at them rather than collapsing into the Heap → SDistr body.

partial def CatCrypt.Deep.Reflect.reifySPComp (e : Lean.Expr) : Lean.MetaM Lean.Expr

Recursively rewrite an SPComp α expression into a RawCode α term.

def CatCrypt.Deep.Reflect.«termRawCode%_» : Lean.ParserDescr

rawCode% e elaborates e as an SPComp α and reifies it to a RawCode α term at elaboration time.

Equations

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

Smoke tests

rawCode% accepts either an inline SPComp expression or a named program: its head is reduced with whnfR, the Monad SPComp instance is projected at .instances transparency for do-notation / >>=, and any other definition (a top-level def game : SPComp α, an abbreviation, a scheme-field projection) is delta-unfolded and retried — while the six SPComp constructors stay opaque, so reflection stops at them instead of collapsing into the Heap → SDistr body. A subterm whose head is none of these after unfolding (a call to an abstract primitive f a, a locally-bound oracle, an opaque constant) is reflected as an embed leaf and round-trips through eval.

noncomputable def deepCoin : CatCrypt.Deep.RawCode Bool

Sample-then-return, inlined in rawCode%.

Equations

• deepCoin = (CatCrypt.Deep.RawCode.sample Bool).bind fun (b : Bool) => CatCrypt.Deep.RawCode.ret b

noncomputable def deepFail : CatCrypt.Deep.RawCode Bool

Failure.

Equations

• deepFail = CatCrypt.Deep.RawCode.fail

noncomputable def deepPure : CatCrypt.Deep.RawCode ℕ

pure applied directly.

Equations

• deepPure = CatCrypt.Deep.RawCode.ret 42

noncomputable def smokeGame : CatCrypt.Core.SPComp Bool

A top-level def written in do-notation reflects without inlining: the reifier unfolds smokeGame and projects the monad instance, stopping at the SPComp constructors.

Equations

• smokeGame = do let b ← CatCrypt.Core.SPComp.sample Bool CatCrypt.Core.SPComp.pure (b ^^ true)

noncomputable def smokeGameRaw : CatCrypt.Deep.RawCode Bool

Equations

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

theorem smokeGame_reflect : smokeGameRaw.eval = smokeGame

The reflected named program evaluates back to the original shallow game.

noncomputable def smokeOracle : Bool → CatCrypt.Core.SPComp Bool

A named oracle family reflects under a binder: fun m => rawCode% (f m) unfolds f applied to the bound m.

Equations

• smokeOracle m = do let k ← CatCrypt.Core.SPComp.sample Bool CatCrypt.Core.SPComp.pure (k ^^ m)

noncomputable def smokeOracleRaw : Bool → CatCrypt.Deep.RawCode Bool

Equations

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

Reflecting abstract-primitive games

An abstract f : Bool → SPComp Bool models a call to a primitive the game does not implement. rawCode% reflects f true as an embed leaf instead of throwing, and the reflected program round-trips through eval.

noncomputable def deepAbstract (f : Bool → CatCrypt.Core.SPComp Bool) : CatCrypt.Deep.RawCode Bool

A game calling an abstract primitive reflects to a RawCode (does not throw): f true becomes an embed leaf, the trailing SPComp.pure a ret.

Equations

• deepAbstract f = (CatCrypt.Deep.RawCode.embed (f true)).bind fun (b : Bool) => CatCrypt.Deep.RawCode.ret b

theorem deepAbstract_reflect (f : Bool → CatCrypt.Core.SPComp Bool) : (deepAbstract f).eval = (f true).bind CatCrypt.Core.SPComp.pure

eval round-trips the abstract-primitive game to the original shallow term. Definitional: eval (embed (f true)) = f true and eval (ret b) = pure b, then η collapses fun b => SPComp.pure b to SPComp.pure.

noncomputable def deepMixed (f : Bool → CatCrypt.Core.SPComp Bool) : CatCrypt.Deep.RawCode Bool

Concrete and opaque heads coexist: sample Bool reflects to RawCode.sample, the following abstract f b to an embed leaf.

Equations

• deepMixed f = (CatCrypt.Deep.RawCode.sample Bool).bind fun (b : Bool) => CatCrypt.Deep.RawCode.embed (f b)

theorem deepMixed_reflect (f : Bool → CatCrypt.Core.SPComp Bool) : (deepMixed f).eval = (CatCrypt.Core.SPComp.sample Bool).bind fun (b : Bool) => f b

The mixed game round-trips: the sample and the embedded f b both evaluate back to their shallow images.