Deterministic Code Interpretation

This file provides interpDet, which interprets deterministic RawCode into StateM Heap, and proves soundness: interpDet agrees with eval on deterministic code (evaluating to a Dirac distribution).

Main definitions

• interpDet - Interpret deterministic RawCode into StateM Heap
• interpDet_sound - Soundness: interpDet agrees with eval

Design

interpDet takes an IsDeterministic proof to eliminate the sample/fail cases via absurd. We recurse on RawCode (which lives in Type) since IsDeterministic lives in Prop and cannot eliminate into Type.

noncomputable def CatCrypt.Deep.interpDet {α : Type} (c : RawCode α) : IsDeterministic c → StateM Core.Heap α

Interpret deterministic RawCode into StateM Heap.

This gives a concrete, efficient semantics for deterministic code. The result is a pure state-passing function with no probability involved.

Takes the IsDeterministic proof to eliminate the sample/fail cases via absurd. We recurse on RawCode (which lives in Type) and use the proof to derive False in unreachable branches.

Equations

• CatCrypt.Deep.interpDet (CatCrypt.Deep.RawCode.ret a) x_4 = pure a
• CatCrypt.Deep.interpDet (c.bind k) h = do let a ← CatCrypt.Deep.interpDet c ⋯ CatCrypt.Deep.interpDet (k a) ⋯
• CatCrypt.Deep.interpDet (CatCrypt.Deep.RawCode.get ℓ) x_3 = do let h ← StateT.get pure { down := h.get ℓ }
• CatCrypt.Deep.interpDet (CatCrypt.Deep.RawCode.put ℓ v) x_3 = do let h ← StateT.get StateT.set (h.set ℓ v) pure { down := () }
• CatCrypt.Deep.interpDet (CatCrypt.Deep.RawCode.sample x✝) h = absurd h ⋯
• CatCrypt.Deep.interpDet CatCrypt.Deep.RawCode.fail h = absurd h ⋯
• CatCrypt.Deep.interpDet (CatCrypt.Deep.RawCode.oracleCall op dom x✝ x_4) h = absurd h ⋯
• CatCrypt.Deep.interpDet (CatCrypt.Deep.RawCode.embed c) h = absurd h ⋯

noncomputable def CatCrypt.Deep.DetCode.toStateM {α : Type} (dc : DetCode α) : StateM Core.Heap α

Convert a DetCode to StateM Heap using interpDet.

Equations

• dc.toStateM = CatCrypt.Deep.interpDet dc.code ⋯

Soundness

The key theorem: for deterministic code, interpDet computes the same result as eval, but deterministically (as a Dirac distribution).

theorem CatCrypt.Deep.interpDet_sound {α : Type} (c : RawCode α) (hdet : IsDeterministic c) (h : Core.Heap) : c.eval h = Prob.SDistr.pure (StateT.run (interpDet c hdet) h)

Running interpDet on a deterministic code produces a result (a, h') such that eval c from heap h gives the Dirac distribution on (some (a, h')).

This connects the deterministic (StateM) and probabilistic (SPComp) semantics: for deterministic code, there is exactly one possible outcome with probability 1.

theorem CatCrypt.Deep.det_self_advantage_zero {α : Type} (c : RawCode α) (_hdet : IsDeterministic c) (h : Core.Heap) : c.eval h = c.eval h

Corollary: deterministic code has zero advantage against itself. Any two runs of the same deterministic code from the same heap produce identical distributions.