feat(interval): add feedback-guided search policy

HexInterval/Experiment/AdaptivePolicy.lean

@@ -0,0 +1,196 @@
+/-
+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 HexInterval.Experiment.StagedPolicy
+
+@[expose] public section
+
+/-!
+# A feedback-guided interval-search policy
+
+This policy refines `StagedPolicy` without inspecting facts, operation names,
+or package keys. It learns from observations attached to engine-authenticated
+events: engine-derived fact-version changes and bounded, package-reported
+logical work. Stable application sites retain useful history across changed
+input versions, while the exact invocation snapshot prevents an old fixed
+point from suppressing newly woken work.
+
+The scores choose search order only.  Every selected offer is revalidated by
+`PolicySession`, and proof replay is independent of this module.
+-/
+
+namespace Hex.Interval.Experiment.AdaptivePolicy
+
+open Propagator Propagator.Policy TargetRun
+
+/-- Replaceable integer coefficients for the first feedback experiment. -/
+structure Config where
+  staged : StagedPolicy.Config := {}
+  optimism : Nat := 16
+  gainWeight : Nat := 96
+  noChangePenalty : Nat := 12
+  ageBonusCap : Nat := 4
+  fairnessAge : Nat := 20
+  maxRecords : Nat := 256
+  deriving DecidableEq, Repr
+
+/-- Stable, package-opaque identity at which feedback is accumulated.  The
+changing invocation snapshot is stored separately in `Record.last`. -/
+inductive Key where
+  | invocation (scope : ScopeId) (application : ApplicationId) (rule : RuleKey)
+      (anchor : NodeId) (kind : ActionKind) (effort generation : Nat)
+  | equality (scope : ScopeId) (equality : EqualityId)
+  deriving DecidableEq
+
+/-- The exact engine snapshot on which an observation was made. -/
+inductive Snapshot where
+  | invocation (invocation : InvocationKey)
+  | equality (equality : EqualityWorkKey)
+  deriving DecidableEq
+
+/-- Bounded search observations accumulated for one selectable transition. -/
+structure Record where
+  key : Key
+  runs : Nat := 0
+  improvements : Nat := 0
+  noChanges : Nat := 0
+  /-- Consecutive fixed points on the exact last snapshot.  This resets when
+  input versions change, so stale fixed points do not demote new work. -/
+  stagnant : Nat := 0
+  work : Nat := 0
+  last : Option Snapshot := none
+
+structure State where
+  config : Config
+  records : List Record := []
+
+def State.initial (config : Config := {}) : State := { config }
+
+/-- Package-reported deterministic work is a bounded scheduling hint, never
+proof evidence or an engine-independent measurement. -/
+def work (cost : CostObservation) : Nat :=
+  cost.arithmeticWork + cost.visitedEntries + cost.estimatedProofNodes
+
+def ruleKey (invocation : InvocationKey) : Key :=
+  .invocation invocation.scope invocation.application invocation.rule invocation.anchor
+    invocation.kind invocation.effort invocation.generation
+
+def equalityKey (equality : EqualityWorkKey) : Key :=
+  .equality equality.scope equality.equality
+
+def offerKey? : OfferKey -> Option Key
+  | .invoke invocation => some (ruleKey invocation)
+  | .equality equality => some (equalityKey equality)
+  | .retry source effort => some (ruleKey { source with effort })
+  | .instantiate _ _ | .split _ _ _ _ => none
+
+def offerSnapshot? : OfferKey -> Option Snapshot
+  | .invoke invocation => some (.invocation invocation)
+  | .equality equality => some (.equality equality)
+  | .retry source effort => some (.invocation { source with effort })
+  | .instantiate _ _ | .split _ _ _ _ => none
+
+def find? (records : List Record) (key : Key) : Option Record :=
+  records.find? fun record => record.key == key
+
+def replace (limit : Nat) (records : List Record) (record : Record) : List Record :=
+  (record :: records.filter fun old => old.key != record.key).take limit
+
+def alter (limit : Nat) (records : List Record) (key : Key)
+    (change : Record -> Record) : List Record :=
+  replace limit records (change ((find? records key).getD { key }))
+
+def recordRule (limit : Nat) (records : List Record)
+    (observation : RuleObservation Fact) : List Record :=
+  let snapshot := Snapshot.invocation observation.invocation
+  alter limit records (ruleKey observation.invocation) fun record =>
+    { record with
+      runs := record.runs + 1
+      improvements := record.improvements + observation.changes.size
+      noChanges := record.noChanges + if observation.outcome == .noChange then 1 else 0
+      stagnant := if observation.outcome != .noChange then 0
+        else if record.last == some snapshot then record.stagnant + 1 else 1
+      work := record.work + work observation.cost
+      last := some snapshot }
+
+def recordEquality (limit : Nat) (records : List Record)
+    (observation : EqualityObservation Fact) : List Record :=
+  let snapshot := Snapshot.equality observation.key
+  alter limit records (equalityKey observation.key) fun record =>
+    { record with
+      runs := record.runs + 1
+      improvements := record.improvements + observation.changes.size
+      noChanges := record.noChanges + if observation.outcome == .noChange then 1 else 0
+      stagnant := if observation.outcome != .noChange then 0
+        else if record.last == some snapshot then record.stagnant + 1 else 1
+      work := record.work + observation.narrowCalls
+      last := some snapshot }
+
+def update : State -> Event Fact -> State
+  | state, .rule observation =>
+      { state with records := recordRule state.config.maxRecords state.records observation }
+  | state, .equality observation =>
+      { state with records := recordEquality state.config.maxRecords state.records observation }
+  | state, .instance _ | state, .dismissed | state, .rejected _ |
+      state, .invalidPayload _ | state, .rejectedPayload _ => state
+
+/-- Learned benefit before fairness.  All arithmetic is deterministic `Nat`
+arithmetic; subtraction saturates at zero. -/
+def learnedScore (config : Config) (record : Option Record)
+    (snapshot : Option Snapshot) (age : Nat) : Nat :=
+  let ageBonus := Nat.min age config.ageBonusCap
+  match record with
+  | none => config.optimism + ageBonus
+  | some record =>
+      let gain := config.gainWeight * record.improvements / (record.work + record.runs + 1)
+      if record.last != snapshot then Nat.max config.optimism gain + ageBonus
+      else gain + ageBonus - config.noChangePenalty * record.stagnant
+
+structure Ranked where
+  offer : OfferView
+  fair : Bool
+  stage : Nat
+  score : Nat
+
+def rankOffer (state : State) (offer : OfferView) : Ranked :=
+  let record := (offerKey? offer.key).bind (find? state.records)
+  let snapshot := offerSnapshot? offer.key
+  { offer
+    fair := state.config.fairnessAge <= offer.age
+    stage := StagedPolicy.rank offer
+    score := learnedScore state.config record snapshot offer.age }
+
+/-- Offers at or beyond `fairnessAge` form the first tier.  On a finite frontier,
+selection consumes offers, so this tier ensures every continuously eligible
+offer is eventually sampled.  Within one tier the staged semantic class still
+wins, then learned score, age, and finally stable input order. -/
+def better (candidate current : Ranked) : Bool :=
+  (candidate.fair && !current.fair) ||
+    (candidate.fair == current.fair && candidate.stage < current.stage) ||
+    (candidate.fair == current.fair && candidate.stage == current.stage &&
+      (current.score < candidate.score ||
+        (current.score == candidate.score && current.offer.age < candidate.offer.age)))
+
+def choose? (state : State) (offers : Array OfferView) : Option OfferView :=
+  (offers.foldl (fun best offer =>
+    if !StagedPolicy.allowed state.config.staged offer then best
+    else
+      let candidate := rankOffer state offer
+      match best with
+      | none => some candidate
+      | some current => if better candidate current then some candidate else best) none).map
+    (fun ranked => ranked.offer)
+
+def controller : TargetRun.Controller Fact State where
+  update := update
+  choose := fun state view =>
+    match choose? state view.offers with
+    | some offer => .select offer state
+    | none => .stop state
+
+end Hex.Interval.Experiment.AdaptivePolicy

HexInterval/SPEC/hex-interval.md

@@ -3379,6 +3379,37 @@ changes, no-change and inapplicable outcomes,
 extensions, failures, dismissals, and rejected selections. These counters are
 diagnostic inputs for later scoring, not evidence.
 
+The first feedback-guided variant keeps the same function- and
+representation-independent stages but accumulates observations at a stable
+engine-owned application or equality site. Its bounded integer score rewards
+engine-derived installed fact-version changes relative to bounded,
+package-reported deterministic arithmetic, traversal, proof-node, or
+equality-narrowing work. That reported work is only a search hint and is not
+proof evidence or an independently measured engine cost. The record also
+retains the last complete invocation snapshot. A repeated `noChange` on that
+exact snapshot subtracts a configurable penalty, while changed input versions
+reset that consecutive fixed-point penalty and receive at least the untried
+optimism score.
+Thus useful history survives an ordinary wake-up without letting an obsolete
+fixed point suppress newly eligible work. The shipped coefficients are covered
+by conformance: one unit-cost improvement outranks an untried peer, a repeated
+fixed point falls below it, and a changed-version wake-up reuses the stable gain.
+The fixed-point penalty applies only when an already observed exact invocation
+is offered again without a snapshot change. Ordinary wake-ups change the
+snapshot, so this first policy promotes historically productive sites but does
+not generally demote unproductive sites across successive input versions.
+
+The feedback table has an explicit deterministic record bound and evicts the
+least recently updated stable site when full. Instantiation and split offers
+retain their staged rank but do not yet have feedback records; invocation, retry, and
+equality work do. Offers at or beyond the configured fairness age form the first
+tier. On the normative finite frontier, where selection consumes an offer, this
+eventually samples every continuously eligible item; stable offer order remains
+the last tie-break. This policy still does not interpret interval width, target
+distance, mathematical function, or package key. It tests the upgradeable
+feedback seam before domain-specific potential features are admitted through an
+equally bounded interface.
+
 A live Mathlib-free arbitrary-function canary presents two exponential
 forward contractors and one source split rule in the same frontier. The policy
 selects both fact improvements, then invokes the split probe, then returns its