Syntactic purity: state-free deep code evaluates to `IsPure` #

This file provides the syntactic backend for SPComp.IsPure goals:

RawCode.StateFree — an inductive predicate marking code built only from ret / bind / sample / fail (no get, no put, no oracleCall, no embed).
RawCode.eval_isPure_of_stateFree — soundness: state-free code evaluates to a heap-independent (IsPure) computation.
ssprove_ispure_reflect — a tactic that reifies the program of an SPComp.IsPure goal into RawCode via Reflect.reifySPComp and changes the goal to IsPure of the reified code's eval (definitional, since the reflection equations eval_ret / eval_bind / eval_sample / eval_fail are all rfl).
ssprove_statefree — constructor search discharging StateFree goals.

Representation choice: `Prop`, not `Bool` #

RawCode.bind binds its continuation as a function k : α → RawCode β (HOAS-style), so a Bool-valued structural decider cannot traverse it: there is no way to inspect k without an argument, and no way to enumerate α in general. We therefore use an inductive predicate whose bind rule quantifies over all continuation values (∀ b, StateFree (k b)), exactly mirroring the existing RawCode.NoOracleCall. The tactic establishes it by constructor search (apply/intro cascade) instead of decide.

Hierarchy #

Syntactically state-free is strictly stronger than IsPure: e.g. get ℓ >>= fun _ => ret 0 is semantically heap-independent (hence IsPure) but not StateFree. IsPure in turn is strictly stronger than any support-level fact. Sampling and failure are compatible with purity; only get/put (and opaque code: oracleCall, embed) break the syntactic criterion.

source

inductive CatCrypt.Deep.RawCode.StateFree {α : Type u} :

RawCode α → Prop

A RawCode tree is state-free when it is built only from ret, bind, sample, and fail — no heap access (get/put) and no opaque code (oracleCall, embed).

The bind rule quantifies over all continuation values, since the continuation is a function (the free monad binds via Lean functions).

ret {α : Type u} (a : α) : (RawCode.ret a).StateFree
bind {α β : Type u} {c : RawCode β} {k : β → RawCode α} (hc : c.StateFree) (hk : ∀ (b : β), (k b).StateFree) : (c.bind k).StateFree
sample {T : Type u} [Fintype T] [Nonempty T] : (RawCode.sample T).StateFree
fail {α : Type u} : RawCode.fail.StateFree

Instances For

source

theorem CatCrypt.Deep.RawCode.eval_isPure_of_stateFree {α : Type u} {c : RawCode α} (h : c.StateFree) :

c.eval.IsPure

Soundness of the syntactic purity criterion: state-free code evaluates to a heap-independent computation.

Induction over the StateFree derivation; each case is the matching IsPure combinator (pure_isPure / bind_isPure / sample_isPure / fail_isPure).

Tactic front-end #

ssprove_ispure_reflect does the reflection step; ssprove_statefree discharges the resulting StateFree side goal. They are combined into ssprove_ispure_syn in CatCrypt.Tactics.VC.

source

def CatCrypt.Deep.tacticSsprove_ispure_reflect :

Lean.ParserDescr

Reify the program c of an SPComp.IsPure c goal into RawCode and change the goal to SPComp.IsPure r.eval where r = rawCode% c. The change is definitional because the reflection equations for ret/bind/sample/fail (and get/set) hold by rfl.

Fails (cleanly, for first-fallback) when the program contains unreifiable subterms: applications of abstract functions, embed, oracle calls, ite, or anything whose head is not an SPComp constructor after whnf.

Equations