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.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.

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.