VCSpec Registry

Discrimination-tree backed registry for @[vcspec] lemmas used by the unary and relational program-logic tactics.

The registry indexes each registered theorem by the computation sub-expression of its conclusion: for unary triples / wp goals this is the OracleComp argument, and for relational triples / RelWP goals this is the left-hand computation. A separate constant-name filter on the right-hand head keeps relational lookups precise without paying for two structural matches.

Implementation notes

Patterns are constructed via Lean.Meta.Sym.mkPatternFromDeclWithKey. That pipeline preprocesses the theorem type (unfolding reducibles, renaming universe parameters, collecting proof / instance argument metadata), internalizes ∀-bound variables as de Bruijn indices, and lets us pick the index key (the computation expression) out of the preprocessed body. The resulting Sym.Pattern is then inserted into a Lean.Meta.DiscrTree via Sym.insertPattern, which wildcards proof / instance arguments and bound variables in the key sequence.

Because Sym.preprocessType unfolds the user-facing abbreviations (Triple, wp, RelTriple, RelWP) into their MAlgOrdered.* / MAlgRelOrdered.* cores, the selector matches on the unfolded heads (plus the folded abbreviations as a safety net). On the lookup side we apply withReducible <| whnf to the goal's computation before querying, matching the normalization performed during pattern preprocessing.

Alignment with core SpecTheorem

Entries mirror the layout of Lean.Elab.Tactic.Do.SpecAttr.SpecTheorem wherever possible:

• proof : SpecProof is reused directly, so entries can be global declarations (the common case for @[vcspec]), local hypotheses, or raw proof expressions. This anticipates the Phase F bridge where a subset of our entries (the Triple-shaped ones) is exposed to mvcgen' via the core SpecExtension.
• pattern : Sym.Pattern is the Sym-side analogue of the combined SpecTheorem.{prog, keys} pair; it carries the program sub-expression, ∀-binder types, level parameters, and proof/instance slot metadata.
• priority : Nat uses the same default as SpecTheorem so attribute overrides carry over cleanly.

Future-proofing note

Lean.Meta.Sym is under active development upstream; minor shape changes to Sym.Pattern, Sym.insertPattern, or Sym.DiscrTree.getMatch between Lean releases should be expected. If a toolchain bump breaks the registry, the affected surface is confined to the selector in buildVCSpecEntry and the lookup path in getRegisteredUnaryVCSpecEntries / getRegisteredRelationalVCSpecEntries; downstream tactic dispatch works through VCSpecEntry.declName? / VCSpecEntry.theoremName! and is insulated from Sym API churn.

structure OracleComp.ProgramLogic.VCSpecEntry : Type

A registered @[vcspec] lemma together with everything the planner needs.

Layout mirrors Lean.Elab.Tactic.Do.SpecAttr.SpecTheorem so the Phase F bridge can lift entries into the core SpecExtension without an extra conversion pass: proof is a shared SpecProof, pattern is the Sym analogue of SpecTheorem.{prog, keys}, and priority uses the same default macro expansion. spec and rightHead? are VCVio-specific diagnostic / planner extras that core does not need.

• proof : Lean.Elab.Tactic.Do.SpecAttr.SpecProof

  Origin of the proof: a global declaration, a local hypothesis, or a raw proof expression. For @[vcspec] attribute registrations this is always .global declName, but keeping the full SpecProof ADT leaves room for a future tactic-level vcspec syntax that feeds hypotheses in directly, and for direct interop with core SpecTheorem.

• pattern : Lean.Meta.Sym.Pattern

  Sym-level pattern used for discrimination-tree indexing. The pattern stores the program sub-expression plus enough bookkeeping (level params, ∀-binder types, proof / instance slots) for Sym.insertPattern and Sym.getMatch to work; it is the Sym-side analogue of SpecTheorem.{prog, keys}.

• spec : NormalizedVCSpec

  Normalized IR summary attached for diagnostics and planner ranking. Not consumed by the discrimination-tree layer.

• rightHead? : Option Lean.Name

  Right-hand head constant used as a secondary filter for relational entries. none for unary entries.

• priority : ℕ

  User-supplied priority; same default as SpecTheorem.priority.

def OracleComp.ProgramLogic.instInhabitedVCSpecEntry.default : VCSpecEntry

@[implicit_reducible]

instance OracleComp.ProgramLogic.instInhabitedVCSpecEntry : Inhabited VCSpecEntry

@[implicit_reducible]

instance OracleComp.ProgramLogic.instBEqVCSpecEntry : BEq VCSpecEntry

def OracleComp.ProgramLogic.VCSpecEntry.declName? (entry : VCSpecEntry) : Option Lean.Name

Global declaration name for entries registered via @[vcspec]; none for entries backed by a local hypothesis or raw proof expression.

def OracleComp.ProgramLogic.VCSpecEntry.theoremName! (entry : VCSpecEntry) : Lean.Name

Extract the global declaration name, assuming the entry was registered via @[vcspec] on a global theorem. Panics on local / stx proofs; intended for legacy call sites that pre-date local-hypothesis support.

def OracleComp.ProgramLogic.VCSpecEntry.kind (entry : VCSpecEntry) : VCSpecKind

def OracleComp.ProgramLogic.VCSpecEntry.lookupKey (entry : VCSpecEntry) : VCSpecLookupKey

structure OracleComp.ProgramLogic.VCSpecRegistry : Type

Persistent state for the @[vcspec] registry.

• all retains insertion order, used by kind-indexed iteration helpers.
• unary indexes unary entries by their comp Sym.Pattern.
• relational indexes relational entries by their oa Sym.Pattern; the right-hand head check happens at lookup time.

• all : Array VCSpecEntry
• unary : Lean.Meta.DiscrTree VCSpecEntry
• relational : Lean.Meta.DiscrTree VCSpecEntry

def OracleComp.ProgramLogic.instInhabitedVCSpecRegistry.default : VCSpecRegistry

@[implicit_reducible]

instance OracleComp.ProgramLogic.instInhabitedVCSpecRegistry : Inhabited VCSpecRegistry

opaque OracleComp.ProgramLogic.vcSpecRegistry : Lean.SimpleScopedEnvExtension VCSpecEntry VCSpecRegistry

vcspec_simp simp set

Auxiliary simp set used internally by the unary and relational tactics for transformer-layer normalization (peeling apply_wp, running monadic *.run projections, normalizing lifts, and so on). Mirror of Loom.Tactic.lspecSimpExt.

Users should write @[vcspec]; the attribute first tries to register the declaration as a spec theorem and on failure falls back to inserting it into vcspec_simp. This lets a single attribute handle both spec lemmas and the normalization rewrites needed to massage a goal into spec-applicable shape.

This attribute is not intended to be used directly.

opaque OracleComp.ProgramLogic.vcSpecSimpExt : Lean.Meta.SimpExtension

def OracleComp.ProgramLogic.getVCSpecSimpTheorems : Lean.CoreM Lean.Meta.SimpTheorems

The accumulated simp set behind the vcspec_simp fallback layer of @[vcspec]. Used by runVCSpecSimp to normalize transformer-stack wp goals before spec dispatch.

Preprocessed-body head matchers

Sym.preprocessType aggressively unfolds reducible abbreviations (including our own Triple, wp, RelTriple, RelWP wrappers) before handing the body to the selector. These helpers match on both the folded (OracleComp.ProgramLogic.…) and unfolded (MAlgOrdered.… / MAlgRelOrdered.…) heads so registrations are robust to future reducibility shifts.

def OracleComp.ProgramLogic.getRegisteredUnaryVCSpecEntries (comp : Lean.Expr) : Lean.MetaM (Array VCSpecEntry)

def OracleComp.ProgramLogic.getRegisteredUnaryVCSpecEntriesNoWhnf (comp : Lean.Expr) : Lean.MetaM (Array VCSpecEntry)

Retrieve unary @[vcspec] entries without reducible whnf on the computation.

This is only for raw wp structural dispatch, where the syntactic head is already the surface we want to step and reducing zero/nil iterator terms can unfold into larger monadic expressions.

def OracleComp.ProgramLogic.getRegisteredRelationalVCSpecEntries (oa ob : Lean.Expr) : Lean.MetaM (Array VCSpecEntry)

def OracleComp.ProgramLogic.getRegisteredUnaryVCSpecTheorems (comp : Lean.Expr) : Lean.MetaM (Array Lean.Name)

def OracleComp.ProgramLogic.getRegisteredRelationalVCSpecTheorems (oa ob : Lean.Expr) : Lean.MetaM (Array Lean.Name)

def OracleComp.ProgramLogic.getVCSpecEntriesOfKind (kind : VCSpecKind) : Lean.CoreM (Array VCSpecEntry)

def OracleComp.ProgramLogic.getVCSpecTheoremsOfKind (kind : VCSpecKind) : Lean.CoreM (Array Lean.Name)