VC Spec Intermediate Representation

Tactic-level intermediate representation used to classify program-logic specification rules for diagnostic messages, registry bookkeeping, and structural candidate filtering. The discrimination-tree indexing itself lives in Registry.lean and operates on Lean.Meta.Sym.Pattern; the IR defined here is a light-weight summary attached to each @[vcspec] entry.

inductive OracleComp.ProgramLogic.VCSpecKind : Type

Broad category of a @[vcspec] rule, derived from the head of the theorem's statement (Triple, wp, RelTriple, RelWP).

• unaryTriple : VCSpecKind
• unaryWP : VCSpecKind
• relTriple : VCSpecKind
• relWP : VCSpecKind

@[implicit_reducible]

instance OracleComp.ProgramLogic.instInhabitedVCSpecKind : Inhabited VCSpecKind

def OracleComp.ProgramLogic.instInhabitedVCSpecKind.default : VCSpecKind

def OracleComp.ProgramLogic.instBEqVCSpecKind.beq : VCSpecKind → VCSpecKind → Bool

@[implicit_reducible]

instance OracleComp.ProgramLogic.instBEqVCSpecKind : BEq VCSpecKind

def OracleComp.ProgramLogic.instReprVCSpecKind.repr : VCSpecKind → ℕ → Std.Format

@[implicit_reducible]

instance OracleComp.ProgramLogic.instReprVCSpecKind : Repr VCSpecKind

inductive OracleComp.ProgramLogic.VCSpecLookupKey : Type

Coarse lookup shape used to route a rule into the right discrimination tree partition (unary vs relational) at registration time.

• unary (head : Lean.Name) : VCSpecLookupKey
• relational (leftHead rightHead : Lean.Name) : VCSpecLookupKey

@[implicit_reducible]

instance OracleComp.ProgramLogic.instInhabitedVCSpecLookupKey : Inhabited VCSpecLookupKey

def OracleComp.ProgramLogic.instInhabitedVCSpecLookupKey.default : VCSpecLookupKey

def OracleComp.ProgramLogic.instBEqVCSpecLookupKey.beq : VCSpecLookupKey → VCSpecLookupKey → Bool

@[implicit_reducible]

instance OracleComp.ProgramLogic.instBEqVCSpecLookupKey : BEq VCSpecLookupKey

def OracleComp.ProgramLogic.instReprVCSpecLookupKey.repr : VCSpecLookupKey → ℕ → Std.Format

@[implicit_reducible]

instance OracleComp.ProgramLogic.instReprVCSpecLookupKey : Repr VCSpecLookupKey

inductive OracleComp.ProgramLogic.VCSpecCompForm : Type

Outer syntactic shape of a single oracle computation slot of a @[vcspec] rule. Used for coarse secondary filtering when the discrimination tree returns multiple candidates.

• bind : VCSpecCompForm
• pure : VCSpecCompForm
• ite : VCSpecCompForm
• map : VCSpecCompForm
• replicate : VCSpecCompForm
• listMapM : VCSpecCompForm
• listFoldlM : VCSpecCompForm
• query : VCSpecCompForm
• simulateQ : VCSpecCompForm
• other : VCSpecCompForm

@[implicit_reducible]

instance OracleComp.ProgramLogic.instInhabitedVCSpecCompForm : Inhabited VCSpecCompForm

def OracleComp.ProgramLogic.instInhabitedVCSpecCompForm.default : VCSpecCompForm

@[implicit_reducible]

instance OracleComp.ProgramLogic.instBEqVCSpecCompForm : BEq VCSpecCompForm

def OracleComp.ProgramLogic.instBEqVCSpecCompForm.beq : VCSpecCompForm → VCSpecCompForm → Bool

@[implicit_reducible]

instance OracleComp.ProgramLogic.instReprVCSpecCompForm : Repr VCSpecCompForm

def OracleComp.ProgramLogic.instReprVCSpecCompForm.repr : VCSpecCompForm → ℕ → Std.Format

inductive OracleComp.ProgramLogic.VCSpecCompPattern : Type

Combined comp-form of a rule's computation slot(s). Unary rules record a single form; relational rules record both sides.

• unary (form : VCSpecCompForm) : VCSpecCompPattern
• relational (leftForm rightForm : VCSpecCompForm) : VCSpecCompPattern

def OracleComp.ProgramLogic.instInhabitedVCSpecCompPattern.default : VCSpecCompPattern

@[implicit_reducible]

instance OracleComp.ProgramLogic.instInhabitedVCSpecCompPattern : Inhabited VCSpecCompPattern

def OracleComp.ProgramLogic.instBEqVCSpecCompPattern.beq : VCSpecCompPattern → VCSpecCompPattern → Bool

@[implicit_reducible]

instance OracleComp.ProgramLogic.instBEqVCSpecCompPattern : BEq VCSpecCompPattern

@[implicit_reducible]

instance OracleComp.ProgramLogic.instReprVCSpecCompPattern : Repr VCSpecCompPattern

def OracleComp.ProgramLogic.instReprVCSpecCompPattern.repr : VCSpecCompPattern → ℕ → Std.Format

structure OracleComp.ProgramLogic.NormalizedVCSpec : Type

Normalized summary of a @[vcspec] rule attached to every registered entry. The discrimination tree is the primary index; this summary powers kind-filtered iteration helpers and structural-compatibility scoring in the planner.

• kind : VCSpecKind
• lookupKey : VCSpecLookupKey
• compPattern : VCSpecCompPattern

def OracleComp.ProgramLogic.instInhabitedNormalizedVCSpec.default : NormalizedVCSpec

@[implicit_reducible]

instance OracleComp.ProgramLogic.instInhabitedNormalizedVCSpec : Inhabited NormalizedVCSpec

def OracleComp.ProgramLogic.instBEqNormalizedVCSpec.beq : NormalizedVCSpec → NormalizedVCSpec → Bool

@[implicit_reducible]

instance OracleComp.ProgramLogic.instBEqNormalizedVCSpec : BEq NormalizedVCSpec

def OracleComp.ProgramLogic.instReprNormalizedVCSpec.repr : NormalizedVCSpec → ℕ → Std.Format

@[implicit_reducible]

instance OracleComp.ProgramLogic.instReprNormalizedVCSpec : Repr NormalizedVCSpec

def OracleComp.ProgramLogic.classifyVCSpecCompForm (comp : Lean.Expr) : VCSpecCompForm

Rough structural summary of the outer head of a computation slot, keyed on the standard monad operations (>>=, pure, query, if, …).

def OracleComp.ProgramLogic.classifyUnaryCompPattern (comp : Lean.Expr) : VCSpecCompPattern

def OracleComp.ProgramLogic.classifyRelationalCompPattern (oa ob : Lean.Expr) : VCSpecCompPattern