Up-To-Bad Tactic

This file provides the ssprove_upto tactic, packaging the up-to-bad lemma inventory of CatCrypt.Crypto.BadEvent into a single goal-shape-dispatched tactic (analogous to VCVio's by_upto bad and EasyCrypt's byupto).

Main definitions

• ssprove_upto bad — on a goal Advantage G₀ G₁ ≤ ε or AdvantageA G₀ G₁ A ≤ ε, applies the matching fundamental-lemma extraction (uptobad_advantage / uptobadA_advantage) with bad-event witness bad, leaving the canonical side goals: identical-until-bad, NoFail for both games, and prTrue bad Heap.empty ≤ ε. On a hybrid goal Advantage (G 0) (G n) ≤ n * ε with bad : ℕ → SPComp Bool, applies advantage_hybrid_upto_bad, leaving the per-step UpToBad goal.
• ssprove_upto (bare) — discharges the goal from a bundled UpToBad/UpToBadA hypothesis in context; if none is found, it applies the plain extraction with a ?bad metavariable goal for the witness.

Lemma inventory packaged

Goal shape	Lemma applied
Advantage G₀ G₁ ≤ ε	uptobad_advantage (unbundled via anonymous constructor; subsumes advantage_upto_bad and lazy_eager_upto_bad)
AdvantageA G₀ G₁ A ≤ ε	uptobadA_advantage (subsumes advantage_upto_bad_A)
Advantage (G 0) (G n) ≤ n * ε	advantage_hybrid_upto_bad (when bad : ℕ → SPComp Bool)

Usage

example ... : Advantage G₀ G₁ ≤ ε := by
  ssprove_upto bad
  · exact h_iub   -- IdenticalUntilBad G₀ G₁ bad
  · exact hnf₀    -- SPComp.NoFail G₀
  · exact hnf₁    -- SPComp.NoFail G₁
  · exact h_bad   -- prTrue bad Heap.empty ≤ ε

References

• Shoup, Sequences of Games, ePrint 2004/332, Lemma 1.
• Bellare & Rogaway, Code-Based Game-Playing Proofs, EUROCRYPT 2006.
• VCVio's by_upto / EasyCrypt's byupto (equivalent tactic surface).

def CatCrypt.Tactics.UpToBad.tacticSsprove_upto_ : Lean.ParserDescr

ssprove_upto bad applies the up-to-bad fundamental lemma with bad-event witness bad, dispatching on the goal shape:

• AdvantageA G₀ G₁ A ≤ ε (with bad : SPComp Bool) — via uptobadA_advantage; side goals: ∀ A, IdenticalUntilBad (G₀.bind A) (G₁.bind A) bad, SPComp.NoFail G₀, SPComp.NoFail G₁, prTrue bad Heap.empty ≤ ε, ∀ a, SPComp.NoFail (A a).
• Advantage (G 0) (G n) ≤ n * ε (with bad : ℕ → SPComp Bool) — via advantage_hybrid_upto_bad; side goal: ∀ i, i < n → UpToBad (G i) (G (i+1)) (bad i) ε.
• Advantage G₀ G₁ ≤ ε (with bad : SPComp Bool) — via uptobad_advantage; side goals: IdenticalUntilBad G₀ G₁ bad, SPComp.NoFail G₀, SPComp.NoFail G₁, prTrue bad Heap.empty ≤ ε.

Equations

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

def CatCrypt.Tactics.UpToBad.tacticSsprove_upto : Lean.ParserDescr

Bare ssprove_upto: discharges Advantage G₀ G₁ ≤ ε / AdvantageA G₀ G₁ A ≤ ε from a bundled UpToBad / UpToBadA hypothesis in context (the adversary NoFail side condition is also searched by assumption). If no bundle is in context, falls back to the plain extraction with an explicit ?bad witness goal.

Equations

• CatCrypt.Tactics.UpToBad.tacticSsprove_upto = Lean.ParserDescr.node `CatCrypt.Tactics.UpToBad.tacticSsprove_upto 1024 (Lean.ParserDescr.nonReservedSymbol "ssprove_upto" false)

Tactic Tests

These examples verify the ssprove_upto dispatch produces the canonical side goals. They mirror the hypothesis shapes of the BadEvent lemmas.