runWpStepRules Dispatch

Dispatch tactic for raw wp-shaped goals plus the canonical @[wpStep] registrations for every wp_* lemma shipped in VCVio/ProgramLogic/Unary/HoareTriple.lean and VCVio/ProgramLogic/Unary/SimulateQ.lean.

The registrations live here (rather than in the rule files themselves) because Unary/HoareTriple.lean and Unary/SimulateQ.lean sit below the tactic infrastructure in the import DAG, mirroring the centralized attribute [vcspec] block in VCVio/ProgramLogic/Tactics/Relational/Internals.lean.

Canonical registrations

Dispatch

opaque OracleComp.ProgramLogic.wpStepRewriteRuleCache : IO.Ref (Std.HashMap Lean.Name Lean.Meta.Sym.Simp.Theorem)

Cache of Sym rewrite theorem objects for global @[wpStep] declarations.

def OracleComp.ProgramLogic.runWpStepRules : Lean.Elab.Tactic.TacticM Bool

Advance a wp-shaped goal by one rewrite, dispatching via the @[wpStep] registry.

Locates the wp oa post sub-expression of the main target, first asks the registry for syntactic candidates, and then appends normalized fallback candidates. Each candidate is tried through the cached SymM rewrite path.

Returns false when no candidate succeeds, or when the goal contains no wp application at all.