Merge pull request #9210 from kim-em/agent/interval-goal-frontend

interval: derive checker input from Lean goals

Author: kim-em

HexInterval/Experiment/GoalFrontend.lean

@@ -0,0 +1,255 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+
+module
+
+public import Lean
+public import HexInterval.Experiment.SemanticReplay
+
+@[expose] public section
+
+/-!
+# Extensible goal reification
+
+This experiment derives a typed expression program and checker input from Lean
+expressions without a central case split over mathematical functions.  Each
+package owns one operation signature and a recognizer for that operation.
+Reification tries all packages with the requested output domain, rejects
+ambiguous matches, recursively reifies arguments in signature order, and
+performs exact-expression common-subexpression elimination.
+
+Fact parsing is a separate adapter.  It maps caller propositions to a term,
+domain, and fact.  Unrecognized hypotheses are ignored, while the target must
+be recognized exactly.  This division lets interval domains choose their own
+open/closed fact language without putting it in the expression-DAG builder.
+-/
+
+namespace Hex.Interval.Experiment.GoalFrontend
+
+open Lean Meta
+open Propagator SemanticReplay
+
+/-- Deterministic bounds for package discovery and recursive graph building. -/
+structure Limits where
+  maxPackages : Nat
+  maxNodes : Nat
+  maxDepth : Nat
+  deriving DecidableEq, Repr
+
+/-- One package-owned Lean-syntax view of an opaque engine operation.
+
+Nullary packages represent caller variables or constants.  A recognizer must
+return arguments in the exact order declared by `operation.inputs`. -/
+structure Package where
+  operation : Operation
+  recognize : Expr → MetaM (Option (List Expr))
+
+/-- A validated operation/recognizer registry. -/
+structure Registry where
+  private mk ::
+  limits : Limits
+  packages : Array Package
+  operations : Array Operation
+
+private def makeRegistry (limits : Limits) (packages : Array Package)
+    (operations : Array Operation) : Registry :=
+  { limits, packages, operations }
+
+namespace Registry
+
+private def uniqueKeys : List Operation → Bool
+  | [] => true
+  | operation :: rest =>
+      !(rest.any fun other => other.key == operation.key) && uniqueKeys rest
+
+/-- Validate finite package assembly before inspecting a goal. -/
+opaque build (limits : Limits) (packages : Array Package) :
+    Except String Registry := do
+  if packages.size > limits.maxPackages then
+    throw "too many goal-reification packages"
+  let operations := packages.map (fun package => package.operation)
+  if !uniqueKeys operations.toList then
+    throw "duplicate goal-reification operation key"
+  pure (makeRegistry limits packages operations)
+
+end Registry
+
+/-- One exact Lean expression already assigned to a graph node and domain. -/
+structure TermRef where
+  expression : Expr
+  domain : DomainId
+  node : NodeId
+
+/-- Mutable-by-return graph construction state. -/
+structure State where
+  nodes : Array Node := #[]
+  terms : Array TermRef := #[]
+
+/-- A proposition parsed into one fact about one Lean term. -/
+structure Claim (Fact : Type) where
+  expression : Expr
+  domain : DomainId
+  fact : Fact
+
+/-- Domain-specific recognition of hypotheses and the requested target. -/
+structure Parser (Fact : Type) where
+  parse : Expr → MetaM (Option (Claim Fact))
+
+/-- One caller proposition contributing to a version-zero meet. -/
+structure Assumption (Fact : Type) where
+  fact : Fact
+  proof : Expr
+
+/-- Complete provenance for one caller-owned version-zero fact.
+
+The empty list denotes domain top.  Each later entry must be combined in order
+through the fact-domain meet theorem, so several hypotheses about the same
+expression cannot overwrite one another's proof dependency. -/
+structure Seed (Fact : Type) where
+  assumptions : List (Assumption Fact) := []
+
+/-- Exact frontend result, including the syntax-to-node map needed to connect
+kernel expressions to the opaque program. -/
+structure Result (Fact : Type) where
+  input : CheckerInput Fact
+  baseFacts : List (NodeFact Fact)
+  seeds : Array (Seed Fact)
+  terms : Array TermRef
+
+def State.find? (state : State) (expression : Expr) (domain : DomainId) :
+    Option NodeId := do
+  let found ← state.terms.toList.find? fun term =>
+    term.domain == domain && term.expression == expression
+  pure found.node
+
+/-- Select exactly one package for an expression and expected output domain.
+No matching package is ordinary absence; malformed or ambiguous matches remain
+hard errors. -/
+def select? (registry : Registry) (expression : Expr) (domain : DomainId) :
+    MetaM (Option (Nat × Package × List Expr)) := do
+  let mut selected : Option (Nat × Package × List Expr) := none
+  for index in [0:registry.packages.size] do
+    let some package := registry.packages[index]?
+      | throwError "interval goal frontend: package index escaped its registry"
+    if package.operation.output == domain then
+      let match? ← withoutModifyingState <| package.recognize expression
+      match match? with
+      | none => pure ()
+      | some arguments =>
+          if arguments.length != package.operation.inputs.length then
+            throwError
+              "interval goal frontend: package returned the wrong argument count"
+          if selected.isSome then
+            throwError "interval goal frontend: ambiguous expression package"
+          selected := some (index, package, arguments)
+  pure selected
+
+/-- Recursively append one expression and its dependencies to the SSA graph.
+Absence means that the expression is unsupported or exceeds the graph budget;
+the input state is immutable, so a caller may discard the whole attempt. -/
+partial def reifyTerm? (registry : Registry) (expression : Expr)
+    (domain : DomainId) (depth : Nat) (state : State) :
+    MetaM (Option (NodeId × State)) := do
+  if registry.limits.maxDepth < depth then
+    return none
+  if let some node := state.find? expression domain then
+    return some (node, state)
+  let some (operationIndex, package, arguments) ←
+      select? registry expression domain
+    | return none
+  let mut state := state
+  let mut nodes := []
+  for (argument, argumentDomain) in arguments.zip package.operation.inputs do
+    let some (node, next) ←
+        reifyTerm? registry argument argumentDomain (depth + 1) state
+      | return none
+    state := next
+    nodes := nodes.concat node
+  if registry.limits.maxNodes ≤ state.nodes.size then
+    return none
+  let node : NodeId := { index := state.nodes.size }
+  let instruction : Node :=
+    { domain
+      op := { index := operationIndex }
+      args := nodes }
+  pure <| some
+    (node,
+      { nodes := state.nodes.push instruction
+        terms := state.terms.push { expression, domain, node } })
+
+private def installedFact (domain : FactDomain Fact) (nodeDomain : DomainId)
+    (current proposed : Fact) : Except String Fact :=
+  match domain.narrow nodeDomain current proposed with
+  | .noChange => pure current
+  | .improved installed | .contradiction installed => pure installed
+  | .malformed _ => throw "malformed caller interval fact"
+  | .resourceLimit _ => throw "caller interval fact exceeded its resource bound"
+
+/-- Reify a target and all recognized local hypotheses into one checker input.
+
+The target is traversed first, so its node and dependencies have stable early
+identifiers.  Later hypotheses reuse those nodes by exact-expression CSE and
+may append additional expressions needed only by their facts. -/
+opaque reify (registry : Registry) (factDomain : FactDomain Fact)
+    (parser : Parser Fact) (hypotheses : List (Expr × Expr)) (target : Expr) :
+    MetaM (Result Fact) := do
+  let some targetClaim ← withoutModifyingState <| parser.parse target
+    | throwError "interval goal frontend: target is not an interval claim"
+  let some (targetNode, initial) ←
+      reifyTerm? registry targetClaim.expression targetClaim.domain 0 {}
+    | throwError "interval goal frontend: target expression is unsupported or exceeds its resource bound"
+  let mut state := initial
+  let mut assumed : List (NodeFact Fact × Expr) := []
+  for (proposition, proof) in hypotheses do
+    let parsed ← withoutModifyingState <| parser.parse proposition
+    match parsed with
+    | none => pure ()
+    | some claim =>
+        match ← reifyTerm? registry claim.expression claim.domain 0 state with
+        | none => pure ()
+        | some (node, next) =>
+            state := next
+            assumed := assumed.concat ({ node, fact := claim.fact }, proof)
+  let program : Program :=
+    { operations := registry.operations
+      nodes := state.nodes }
+  unless program.check do
+    throwError "interval goal frontend: reified program failed structural validation"
+  let mut facts := #[]
+  let mut seeds := #[]
+  for index in [0:state.nodes.size] do
+    let some instruction := state.nodes[index]?
+      | throwError "interval goal frontend: node index escaped the graph"
+    facts := facts.push (factDomain.top instruction.domain)
+    seeds := seeds.push {}
+  for (fact, proof) in assumed do
+    let some instruction := state.nodes[fact.node.index]?
+      | throwError "interval goal frontend: assumption node escaped the graph"
+    let some current := facts[fact.node.index]?
+      | throwError "interval goal frontend: assumption fact escaped the graph"
+    let some seed := seeds[fact.node.index]?
+      | throwError "interval goal frontend: assumption seed escaped the graph"
+    let installed ←
+      match installedFact factDomain instruction.domain current fact.fact with
+      | .ok installed => pure installed
+      | .error message => throwError "interval goal frontend: {message}"
+    facts := facts.set! fact.node.index installed
+    seeds := seeds.set! fact.node.index
+      { assumptions := seed.assumptions.concat { fact := fact.fact, proof } }
+  let targetFact : NodeFact Fact :=
+    { node := targetNode, fact := targetClaim.fact }
+  pure
+    { input :=
+        { baseProgram := program
+          initialFacts := facts
+          target := targetFact }
+      baseFacts :=
+        List.ofFn fun index : Fin facts.size =>
+          { node := { index := index.val }, fact := facts[index] }
+      seeds
+      terms := state.terms }
+
+end Hex.Interval.Experiment.GoalFrontend

HexInterval/SPEC/hex-interval.md

@@ -1348,8 +1348,9 @@ direct emission. The current replay applications and final closure remain
 indexed by the exact `CheckerInput.baseProgram` and target. The emitter also
 seeds each instance event's fresh nodes with domain top after checking their
 lookup in the reified final program. The real-sine tactic is now a client of
-this module rather than the owner of the fold, but it still names the canary's
-fixed base graph, base list, semantic bridge, and final target.
+this module rather than the owner of the fold. Its semantic bridge and final
+proof closure still name the canary's fixed base graph, declared base list,
+and target; the goal reifier below begins removing that specialization.
 
 A second live vertical validates this separation with `Real.exp`. Its
 Mathlib-free package uses a distinct three-element fact lattice, contributes
@@ -1359,9 +1360,40 @@ one replay schema. The same policy session, joint package registry,
 fact-polymorphic quotation, shared structural encoder, and generic evidence
 fold produce the ordinary theorem `0 ≤ Real.exp x`. Thus both a multi-package
 graph-growing sine proof and a single-rule exponential proof pass through the
-same frontend API without a function switch. The next frontend experiment
-must derive the fixed context pieces and the caller-input binding from an
-arbitrary caller expression.
+same frontend API without a function switch. The goal reifier below derives
+candidate context pieces from an arbitrary caller expression, but generic
+proof emission has not yet bound its recorded seed recipe to the frontend's
+declared base list.
+
+The first goal-reification experiment now derives the exponential canary's
+base program, version-zero fact array, and target fact from the actual Lean
+goal before running its compiled fixture. Expression packages contribute an
+opaque operation signature and a Lean-expression recognizer; the reifier has
+no switch for exponential, sine, or any other mathematical function. It tries
+all packages with the required output domain, requires a unique match and
+exact arity, and runs each recognizer without retaining changes to elaborator
+state. It recursively reifies arguments in signature order, performs exact
+expression/domain CSE, validates the resulting SSA program, and enforces
+package, node, and depth limits. A separate fact parser maps propositions to a
+term, domain, and fact, so interval endpoint and open/closed semantics do not
+enter graph construction. Parser calls likewise retain no elaborator-state
+changes. The target is reified first and is strict: an unsupported or
+over-budget target fails. A parsed hypothesis is optional information; if its
+term or a recursive dependency has no package or exceeds the remaining graph
+budget, that whole immutable attempt is discarded. Malformed arity and
+ambiguous package matches remain hard registry errors. All accepted hypotheses
+narrowing the same version-zero node remain in an ordered seed recipe; later
+hypotheses cannot overwrite an earlier proof dependency, while facts about
+other recognized expressions may append a suffix after the target graph. The
+exponential tactic currently requires only the target-reachable operation and
+node prefixes, and the target fact, to match its fixed semantic/proof fixture.
+Extra supported, duplicate, unsupported-real, and non-real hypotheses therefore
+do not disable an otherwise applicable proof; later operation packages may
+also extend the registry after the target prefix. Removing that last prefix
+comparison requires package-compositional construction of the program
+semantics and generic proof emission for the recorded top/assumption seed
+recipes; it remains the next frontend experiment rather than an assumed
+capability.
 
 The fixed canary also requires a live session with no dropped work and an exact
 proof history of one instance, one equality, three fact events, and the