@[wpStep] Registry

Discrimination-tree backed registry for the equational wp comp post = … rewrites used by the inner driver of vcstep / vcgen for raw wp-shaped goals.

Each @[wpStep] rule is compiled once, at attribute-registration time, into a Sym.Pattern keyed on just the comp argument of the LHS (Sym.mkPatternFromDeclWithKey). That pattern lives in a Sym.DiscrTree so a goal wp oa post can be answered by normalizing oa and querying the tree: the handful of candidate rules that come back are fed to the dispatch tactic which tries rw / simp only in the TacticM layer.

We deliberately do not pre-compile a Sym.Simp.Theorem bundle here: that bundle is only needed by a future SymM-based rewrite loop (see the deferred mvcgen' bridge notes in docs/agents/program-logic.md), and eagerly computing one per registered rule both bloats oleans and drags several Sym.Simp.* modules into the import closure of every downstream tactic consumer. The dispatch tactic today works off the comp-keyed tree alone. If a SymM migration later needs the theorem bundle, it can be rebuilt on demand from getAllWpStepEntries via Sym.Simp.mkTheoremFromDecl.

Entry layout

WpStepEntry mirrors the Lean.Elab.Tactic.Do.SpecAttr.SpecTheorem layout where the shapes line up: proof : SpecProof captures the origin (global decl / local hyp / raw proof) and supports a future SpecTheorem bridge, compPattern : Sym.Pattern carries the comp-keyed pattern, and priority : Nat mirrors core's default.

The dispatch tactic runWpStepRules, together with the canonical registrations for every shipped wp_* lemma, lives in VCVio.ProgramLogic.Tactics.Common.WpStepDispatch.

Future-proofing note

Lean.Meta.Sym.Pattern and Lean.Meta.Sym.Simp.DiscrTree are under active development upstream. If a toolchain bump breaks the registry, the affected surface is confined to the selector in buildWpStepEntry and the lookup path in getRegisteredWpStepEntries; downstream tactic dispatch works through WpStepEntry.declName? and is insulated from Sym API churn.

structure OracleComp.ProgramLogic.WpStepEntry : Type

A registered @[wpStep] lemma.

Layout mirrors Lean.Elab.Tactic.Do.SpecAttr.SpecTheorem as much as the VCVio-specific shape (equational wp rewrites rather than Hoare triples) allows. We store only the comp-keyed Sym.Pattern and an origin marker; the theorem's full LHS pattern is reconstructible on demand via Sym.Simp.mkTheoremFromDecl for any future SymM rewrite path.

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

  Origin of the proof; currently always .global declName for attribute-registered rules, but kept as a SpecProof for future local hypothesis support and core interop.

• compPattern : Lean.Meta.Sym.Pattern

  Sym-level pattern keyed on the comp argument of the LHS. This is the key runWpStepRules dispatch uses, which indexes goals by their wp-argument.

• priority : ℕ

  User-supplied priority, matching core's convention.

def OracleComp.ProgramLogic.instInhabitedWpStepEntry.default : WpStepEntry

@[implicit_reducible]

instance OracleComp.ProgramLogic.instInhabitedWpStepEntry : Inhabited WpStepEntry

@[implicit_reducible]

instance OracleComp.ProgramLogic.instBEqWpStepEntry : BEq WpStepEntry

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

Global declaration name of a @[wpStep] entry, if any.

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

Extract the global declaration name, assuming the entry was registered via @[wpStep] on a global theorem. Returns Name.anonymous for non-global proofs (safe: such entries are not produced today).

structure OracleComp.ProgramLogic.WpStepRegistry : Type

Persistent state for the @[wpStep] registry.

• all retains insertion order, exposed for diagnostics / tooling.
• compTree is the comp-keyed discrimination tree consulted by the current runWpStepRules dispatch.

• all : Array WpStepEntry
• compTree : Lean.Meta.DiscrTree WpStepEntry

@[implicit_reducible]

instance OracleComp.ProgramLogic.instInhabitedWpStepRegistry : Inhabited WpStepRegistry

opaque OracleComp.ProgramLogic.wpStepRegistry : Lean.SimpleScopedEnvExtension WpStepEntry WpStepRegistry

def OracleComp.ProgramLogic.getAllWpStepEntries : Lean.CoreM (Array WpStepEntry)

Retrieve all registered @[wpStep] entries in insertion order.

def OracleComp.ProgramLogic.getRegisteredWpStepEntries (oa : Lean.Expr) : Lean.MetaM (Array WpStepEntry)

Retrieve the @[wpStep] entries whose comp pattern matches oa.

The goal's oa is first instantiated and withReducible whnf-normalized so its head agrees with the registered patterns (which were unfolded once via Sym.preprocessType at registration time). The actual tree traversal is the pure Sym.DiscrTree.getMatch, which already wildcards proof / instance positions and de Bruijn pattern variables.

Returned candidates are still validated by the dispatch tactic when it tries each rewrite, so over-approximation here is harmless.

def OracleComp.ProgramLogic.getRegisteredWpStepEntriesNoWhnf (oa : Lean.Expr) : Lean.MetaM (Array WpStepEntry)

Retrieve @[wpStep] entries without normalizing the computation first.

Raw wp dispatch uses this as the first pass so syntactic zero/nil iterator redexes are offered to their exact rewrite rules before normalized fallback candidates such as successor/cons unfoldings.