VC tactics: mvcgen-driven closers for SPComp side conditions

The support-level Std.Do bridge (CatCrypt.Core.StdDoBridge) makes mvcgen walk SPComp do-blocks. This file packages that into goal-shape-dispatched tactics for the recurring side conditions of CatCrypt's security proofs:

• ssprove_ispure — closes SPComp.IsPure c goals. It first tries the syntactic backend ssprove_ispure_syn (reify c into RawCode via Reflect.reifySPComp, apply RawCode.eval_isPure_of_stateFree, discharge StateFree by constructor search — see CatCrypt.Deep.PureCode), then falls back to the structural combinator cascade ssprove_ispure_cascade (bind_isPure / sample_isPure / pure_isPure / fail_isPure / liftSDistr_isPure / assumption). The syntactic branch only fires on fully concrete programs (sample/pure/fail/bind); the cascade additionally handles abstract sub-programs via hypotheses. IsPure is a distribution-equality statement (heap-independence of the whole distribution), strictly stronger than any support-level fact, so it is not Triple-expressible: the bridge's isPure_wpProp_iff consumes an IsPure witness (it simplifies wpProp given purity); it cannot produce one. Hence the structural/syntactic routes for this goal shape.
• ssprove_nofail — closes SPComp.NoFail c by lowering through triple_noThrow_true_iff_noFail, running mvcgen over the bridge's @[spec] lemmas, and finishing with the closing-simp cascade. These are exactly the NoFail side goals ssprove_upto produces.
• ssprove_phoare — lowers a unary pHoare goal through pHoare_iff_triple and runs mvcgen; VCs the closer cascade misses are left to the user (partial progress is intended).
• ssprove_vc — umbrella: first | ssprove_ispure | ssprove_nofail | ssprove_phoare.

Each tactic also takes an optional ident list (e.g. ssprove_nofail [myGame]) that unfolds the named definitions first, so mvcgen / the combinator cascade can see the underlying do-block.

Closing-simp cascade

The bridge's examples show the closing idiom for the VCs mvcgen leaves: either pure rfl, or a simp with the WP-unfolding lemmas plus the support-shape lemmas and Heap.get_set_same.

def CatCrypt.Tactics.VC.tacticSp_vc_close : Lean.ParserDescr

Closer for mvcgen-generated VCs on SPComp goals: rfl, then the bridge unfolding simp set, then simp_all. Fails if any goal survives.

Equations

• CatCrypt.Tactics.VC.tacticSp_vc_close = Lean.ParserDescr.node `CatCrypt.Tactics.VC.tacticSp_vc_close 1024 (Lean.ParserDescr.nonReservedSymbol "sp_vc_close" false)

def CatCrypt.Tactics.VC.tacticSp_vc_close? : Lean.ParserDescr

Best-effort variant of sp_vc_close: never fails, leaves the VCs the cascade misses (used by ssprove_phoare, where partial progress is the point).

Equations

• CatCrypt.Tactics.VC.tacticSp_vc_close? = Lean.ParserDescr.node `CatCrypt.Tactics.VC.tacticSp_vc_close? 1024 (Lean.ParserDescr.nonReservedSymbol "sp_vc_close?" false)

ssprove_ispure

def CatCrypt.Tactics.VC.tacticSsprove_ispure_syn : Lean.ParserDescr

ssprove_ispure_syn closes SPComp.IsPure c goals for fully concrete c built from sample / pure / fail / bind (and do-notation over them) by the syntactic route: reify c into RawCode, apply the soundness lemma RawCode.eval_isPure_of_stateFree, and discharge StateFree by constructor search. Depth-independent: no per-step combinator search. Fails cleanly (for first-fallback) on programs containing abstract sub-programs, liftSDistr, ite, or heap access.

Equations

• CatCrypt.Tactics.VC.tacticSsprove_ispure_syn = Lean.ParserDescr.node `CatCrypt.Tactics.VC.tacticSsprove_ispure_syn 1024 (Lean.ParserDescr.nonReservedSymbol "ssprove_ispure_syn" false)

def CatCrypt.Tactics.VC.«tacticSsprove_ispure_syn[_,,]» : Lean.ParserDescr

ssprove_ispure_syn [d₁, d₂, ...] unfolds the named game definitions first, then runs the syntactic route.

Equations

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

def CatCrypt.Tactics.VC.tacticSsprove_ispure_cascade : Lean.ParserDescr

ssprove_ispure_cascade closes SPComp.IsPure c goals for c built from sample / pure / fail / liftSDistr / bind (and hypotheses), by the structural combinator cascade. The leading show is the goal-shape guard that makes ssprove_vc dispatch correctly.

Equations

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

def CatCrypt.Tactics.VC.tacticSsprove_ispure : Lean.ParserDescr

ssprove_ispure closes SPComp.IsPure c goals: syntactic backend first (ssprove_ispure_syn — all-or-nothing), then the structural combinator cascade (ssprove_ispure_cascade — handles abstract sub-programs via hypotheses).

Equations

• CatCrypt.Tactics.VC.tacticSsprove_ispure = Lean.ParserDescr.node `CatCrypt.Tactics.VC.tacticSsprove_ispure 1024 (Lean.ParserDescr.nonReservedSymbol "ssprove_ispure" false)

def CatCrypt.Tactics.VC.«tacticSsprove_ispure[_,,]» : Lean.ParserDescr

ssprove_ispure [d₁, d₂, ...] unfolds the named game definitions first, then runs the syntactic-then-cascade dispatch.

Equations

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

ssprove_nofail

def CatCrypt.Tactics.VC.tacticSsprove_nofail : Lean.ParserDescr

ssprove_nofail closes SPComp.NoFail c: lowers to the trivial total-correctness triple via triple_noThrow_true_iff_noFail, runs mvcgen over the bridge's @[spec] lemmas, and closes the VCs with sp_vc_close. This is the shape of the NoFail side goals ssprove_upto leaves.

Equations

• CatCrypt.Tactics.VC.tacticSsprove_nofail = Lean.ParserDescr.node `CatCrypt.Tactics.VC.tacticSsprove_nofail 1024 (Lean.ParserDescr.nonReservedSymbol "ssprove_nofail" false)

def CatCrypt.Tactics.VC.«tacticSsprove_nofail[_,,]» : Lean.ParserDescr

ssprove_nofail [d₁, d₂, ...] unfolds the named game definitions first so mvcgen can walk the do-block.

Equations

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

ssprove_phoare

def CatCrypt.Tactics.VC.tacticSsprove_phoare : Lean.ParserDescr

ssprove_phoare lowers a unary pHL goal pHoare P c Q to the partial-correctness (⇓?) Std.Do triple via pHoare_iff_triple, runs mvcgen, and best-effort-closes the VCs. VCs the cascade misses are left open for the user.

Equations

• CatCrypt.Tactics.VC.tacticSsprove_phoare = Lean.ParserDescr.node `CatCrypt.Tactics.VC.tacticSsprove_phoare 1024 (Lean.ParserDescr.nonReservedSymbol "ssprove_phoare" false)

def CatCrypt.Tactics.VC.«tacticSsprove_phoare[_,,]» : Lean.ParserDescr

ssprove_phoare [d₁, d₂, ...] unfolds the named definitions first.

Equations

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

ssprove_vc umbrella

def CatCrypt.Tactics.VC.tacticSsprove_vc : Lean.ParserDescr

ssprove_vc dispatches on the goal head: SPComp.IsPure → ssprove_ispure, SPComp.NoFail → ssprove_nofail, pHoare → ssprove_phoare.

Equations

• CatCrypt.Tactics.VC.tacticSsprove_vc = Lean.ParserDescr.node `CatCrypt.Tactics.VC.tacticSsprove_vc 1024 (Lean.ParserDescr.nonReservedSymbol "ssprove_vc" false)

def CatCrypt.Tactics.VC.«tacticSsprove_vc[_,,]» : Lean.ParserDescr

ssprove_vc [d₁, d₂, ...] unfolds the named definitions first.

Equations

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

Tactic Tests

IsPure of a sampled do-block, NoFail of a sample/set/get block (the side-goal shape ssprove_upto produces), and a pHoare lowering.

@[reducible, inline]

abbrev vcLoc : CatCrypt.Core.Location

Demo location storing a Bool.

Equations

• vcLoc = { id := 0, ty := Bool, fintype := Bool.fintype, inhabited := instInhabitedBool }

Syntactic-branch tests (ssprove_ispure_syn)

noncomputable def vcG₀ : CatCrypt.Core.SPComp Bool

Demo game writing its sampled bit to the heap.

Equations

• vcG₀ = do let b ← CatCrypt.Core.SPComp.sample Bool CatCrypt.Core.SPComp.set vcLoc b pure b

noncomputable def vcG₁ : CatCrypt.Core.SPComp Bool

Demo game writing the negated bit.

Equations

• vcG₁ = do let b ← CatCrypt.Core.SPComp.sample Bool CatCrypt.Core.SPComp.set vcLoc !b pure b