Std.Do / mvcgen bridge for SPComp

Support-level Std.Do view of SPComp: a Std.Do.WP/Std.Do.WPMonad instance whose weakest precondition is almost-sure (support-level) satisfaction of the postcondition. This makes mvcgen usable for functional-correctness goals about SPComp do-blocks. Quantitative bounds (sdist, advantage) live outside PredTrans — expectation transformers are monotone but not conjunctive, so they cannot inhabit PredTrans.conjunctiveRaw; they belong to the Advantage/sdist layer.

The design mirrors VCVio's proposition-level bridge for OracleComp (VCVio/ProgramLogic/Unary/StdDoBridge.lean).

Post shape

SPComp α = Heap → SDistr (α × Heap) is the monad StateT Heap (OptionT-over-PMF): failure (SDistr's none) carries no final heap. The structural mirror of that stack is

• spPostShape = .arg Heap (.except PUnit .pure)

so assertions are Heap → ULift Prop and postconditions carry a heap-free failure barrel PUnit → ULift Prop. The alternative shape .except PUnit (.arg Heap .pure) would give the failure barrel a Heap argument that the semantics cannot supply (there is no heap at failure), and wp_bind fails for it; with the heap-free barrel both WPMonad laws hold on the nose.

⇓ r => ... (total correctness: the program must not fail) and ⇓? r => ... (partial correctness: nothing asserted on failure) both make sense for this shape; ⇓?-triples coincide with the unary pHoare judgment, and ⇓-triples additionally assert SPComp.NoFail.

Main definitions

• SPComp.wpProp — support-level weakest precondition as a plain predicate
• SPComp.wpSupport, SPComp.instWP, SPComp.instWPMonad — the Std.Do instances at shape spPostShape
• adequacy: wpProp_iff_forall_support, triple_mayThrow_iff, triple_noThrow_iff, pHoare_iff_triple, triple_noThrow_true_iff_noFail, isPure_wpProp_iff
• @[spec] lemmas for SPComp.get/set/sample/fail so mvcgen walks SPComp do-blocks

Reached via the CatCrypt.Tactics umbrella through Tactics/VC.lean (ssprove_nofail / ssprove_phoare lower goals into this bridge).

SDistr support lemmas for bind

Support and failure mass of SDistr.bind, in the ≠ 0 form used by the support-level WP.

theorem CatCrypt.Prob.SDistr.bind_apply_some_ne_zero_iff {α β : Type u} (d : SDistr α) (f : α → SDistr β) (b : β) : (d.bind f) (some b) ≠ 0 ↔ ∃ (a : α), d (some a) ≠ 0 ∧ (f a) (some b) ≠ 0

theorem CatCrypt.Prob.SDistr.bind_apply_none_ne_zero_iff {α β : Type u} (d : SDistr α) (f : α → SDistr β) : (d.bind f) none ≠ 0 ↔ d none ≠ 0 ∨ ∃ (a : α), d (some a) ≠ 0 ∧ (f a) none ≠ 0

theorem CatCrypt.Prob.SDistr.pure_apply_some_ne_zero_iff {α : Type u} (x y : α) : (pure x) (some y) ≠ 0 ↔ x = y

(SDistr.pure x) (some y) ≠ 0 iff x = y (point-mass support).

SPComp-level support lemmas

theorem CatCrypt.Core.SPComp.bind_apply_some_ne_zero_iff {α β : Type} (c : SPComp α) (f : α → SPComp β) (h : Heap) (b : β) (h'' : Heap) : (c.bind f h) (some (b, h'')) ≠ 0 ↔ ∃ (a : α) (h' : Heap), (c h) (some (a, h')) ≠ 0 ∧ (f a h') (some (b, h'')) ≠ 0

Support of a bound computation, in ≠ 0 form.

theorem CatCrypt.Core.SPComp.bind_apply_none_ne_zero_iff {α β : Type} (c : SPComp α) (f : α → SPComp β) (h : Heap) : (c.bind f h) none ≠ 0 ↔ (c h) none ≠ 0 ∨ ∃ (a : α) (h' : Heap), (c h) (some (a, h')) ≠ 0 ∧ (f a h') none ≠ 0

Failure mass of a bound computation, in ≠ 0 form.

The support-level weakest precondition

def CatCrypt.Core.SPComp.wpProp {α : Type u_1} (c : SPComp α) (post : α → Heap → Prop) : Heap → Prop

Support-level (almost-sure) weakest precondition for SPComp: from initial heap h, every outcome (a, h') in the support of c h satisfies post a h'. Says nothing about the failure mass — see the failure barrel of wpSupport for that.

Equations

• c.wpProp post h = ∀ (a : α) (h' : CatCrypt.Core.Heap), (c h) (some (a, h')) ≠ 0 → post a h'

theorem CatCrypt.Core.SPComp.wpProp_iff_forall_support {α : Type u_1} (c : SPComp α) (post : α → Heap → Prop) (h : Heap) : c.wpProp post h ↔ ∀ p ∈ (c h).support, post p.1 p.2

Adequacy: wpProp is the ∀-over-support statement.

@[reducible, inline]

abbrev CatCrypt.Core.SPComp.spPostShape : Std.Do.PostShape

The Std.Do post shape for SPComp: one state layer (Heap) over one heap-free failure layer (PUnit, the subprobability defect of SDistr).

Equations

• CatCrypt.Core.SPComp.spPostShape = Std.Do.PostShape.arg CatCrypt.Core.Heap (Std.Do.PostShape.except PUnit.{1} Std.Do.PostShape.pure)

def CatCrypt.Core.SPComp.wpSupport {α : Type} (c : SPComp α) : Std.Do.PredTrans spPostShape α

The support-level predicate transformer of an SPComp computation: success barrel = wpProp, failure barrel = guard on nonzero failure mass.

Equations

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

@[instance_reducible]

instance CatCrypt.Core.SPComp.instWP : Std.Do.WP SPComp spPostShape

Equations

• CatCrypt.Core.SPComp.instWP = { wp := fun {α : Type} (c : CatCrypt.Core.SPComp α) => c.wpSupport }

theorem CatCrypt.Core.SPComp.wp_eq {α : Type} (c : SPComp α) : Std.Do.wp c = c.wpSupport

theorem CatCrypt.Core.SPComp.wpSupport_apply_down {α : Type} (c : SPComp α) (Q : Std.Do.PostCond α spPostShape) (h : Heap) : (c.wpSupport.apply Q h).down ↔ (∀ (a : α) (h' : Heap), (c h) (some (a, h')) ≠ 0 → (Q.1 a h').down) ∧ ((c h) none ≠ 0 → (Q.2.1 PUnit.unit).down)

Unfolding lemma for the support-level WP. Deliberately not @[simp]: mvcgen must keep wp⟦·⟧ opaque and walk via @[spec] lemmas.

@[instance_reducible]

instance CatCrypt.Core.SPComp.instWPMonad : Std.Do.WPMonad SPComp spPostShape

Equations

• CatCrypt.Core.SPComp.instWPMonad = { toLawfulMonad := CatCrypt.Core.SPComp.instWPMonad._proof_1, toWP := CatCrypt.Core.SPComp.instWP, wp_pure := ⋯, wp_bind := ⋯ }

Adequacy: triples vs wpProp, pHoare, NoFail, IsPure

theorem CatCrypt.Core.SPComp.triple_of_forall {α : Type} (c : SPComp α) (P : Std.Do.Assertion spPostShape) (Q : Std.Do.PostCond α spPostShape) (hsucc : ∀ (h : Heap), (P h).down → ∀ (a : α) (h' : Heap), (c h) (some (a, h')) ≠ 0 → (Q.1 a h').down) (hfail : ∀ (h : Heap), (P h).down → (c h) none ≠ 0 → (Q.2.1 PUnit.unit).down) : ⦃P⦄ c ⦃Q⦄

A Triple from pointwise success/failure obligations.

theorem CatCrypt.Core.SPComp.triple_mayThrow_iff {α : Type} (c : SPComp α) (P : Heap → Prop) (post : α → Heap → Prop) : ⦃fun (h : Heap) => ⌜P h⌝⦄ c ⦃Std.Do.PostCond.mayThrow fun (a : α) (h : Heap) => ⌜post a h⌝⦄ ↔ ∀ (h : Heap), P h → c.wpProp post h

Adequacy for partial correctness (⇓?): a mayThrow triple is exactly the universally-quantified wpProp statement. Nothing is asserted about the failure mass.

theorem CatCrypt.Core.SPComp.triple_noThrow_iff {α : Type} (c : SPComp α) (P : Heap → Prop) (post : α → Heap → Prop) : ⦃fun (h : Heap) => ⌜P h⌝⦄ c ⦃Std.Do.PostCond.noThrow fun (a : α) (h : Heap) => ⌜post a h⌝⦄ ↔ ∀ (h : Heap), P h → c.wpProp post h ∧ (c h) none = 0

Adequacy for total correctness (⇓): a noThrow triple is wpProp plus zero failure mass from every P-heap.

theorem CatCrypt.Core.SPComp.pHoare_iff_triple {α : Type} (P : Unary.UPre) (c : SPComp α) (Q : Unary.UPost α) : Unary.pHoare P c Q ↔ ⦃fun (h : Heap) => ⌜P h⌝⦄ c ⦃Std.Do.PostCond.mayThrow fun (a : α) (h : Heap) => ⌜Q a h⌝⦄

The unary pHL judgment (CatCrypt.Unary.pHoare) is exactly the partial-correctness (⇓?) Std.Do triple.

theorem CatCrypt.Core.SPComp.triple_noThrow_true_iff_noFail {α : Type} (c : SPComp α) : ⦃fun (x : Heap) => ⌜True⌝⦄ c ⦃Std.Do.PostCond.noThrow fun (x : α) (x_1 : Heap) => ⌜True⌝⦄ ↔ Crypto.SPComp.NoFail c

SPComp.NoFail is the trivial total-correctness triple: the failure barrel ⌜False⌝ of noThrow forces zero failure mass.

theorem CatCrypt.Core.SPComp.isPure_wpProp_iff {α : Type} {c : SPComp α} {d : Prob.SDistr α} (hd : ∀ (h : Heap), c h = d.bind fun (a : α) => Prob.SDistr.pure (a, h)) (post : α → Heap → Prop) (h : Heap) : c.wpProp post h ↔ ∀ (a : α), d (some a) ≠ 0 → post a h

For an IsPure computation with witness distribution d, the support-level WP is the ∀-over-d.support statement at the unchanged heap.

@[spec] lemmas for the SPComp primitives

These let mvcgen walk SPComp do-blocks: the generic Std.Do.Spec.bind / Spec.pure handle the monadic skeleton (via instWPMonad), and these lemmas handle the leaves.

theorem CatCrypt.Core.SPComp.Spec.get (l : Location) {Q : Std.Do.PostCond l.ty spPostShape} : ⦃fun (h : Heap) => Q.1 (h.get l) h⦄ SPComp.get l ⦃Q⦄

Spec for SPComp.get: returns the heap's value at l, heap unchanged, never fails.

theorem CatCrypt.Core.SPComp.Spec.set (l : Location) (v : l.ty) {Q : Std.Do.PostCond Unit spPostShape} : ⦃fun (h : Heap) => Q.1 () (h.set l v)⦄ SPComp.set l v ⦃Q⦄

Spec for SPComp.set: writes v at l, returns (), never fails.

theorem CatCrypt.Core.SPComp.Spec.sample (A : Type) [Fintype A] [Nonempty A] {Q : Std.Do.PostCond A spPostShape} : ⦃fun (h : Heap) => Std.Do.SPred.forall fun (a : A) => Q.1 a h⦄ SPComp.sample A ⦃Q⦄

Spec for SPComp.sample: the result can be any element of A (uniform has full support), heap unchanged, never fails.

theorem CatCrypt.Core.SPComp.Spec.fail {α : Type} {Q : Std.Do.PostCond α spPostShape} : ⦃fun (x : Heap) => Q.2.1 PUnit.unit⦄ SPComp.fail ⦃Q⦄

Spec for SPComp.fail: empty support, always fails — the precondition is the failure barrel.

theorem CatCrypt.Core.SPComp.Spec.purePrim {α : Type} (a : α) {Q : Std.Do.PostCond α spPostShape} : ⦃Q.1 a⦄ pure a ⦃Q⦄

Spec for the prefix form SPComp.pure (the generic Std.Do.Spec.pure covers Pure.pure; this covers explicit SPComp.pure leaves).

Examples: mvcgen-closed functional-correctness triples

@[reducible, inline]

abbrev CatCrypt.Core.StdDoBridgeExamples.bLoc : Location

Demo location storing a Bool.

Equations

• CatCrypt.Core.StdDoBridgeExamples.bLoc = { id := 0, ty := Bool, fintype := Bool.fintype, inhabited := instInhabitedBool }