From 67f669eb12aa324f61b2c3d4a202dfd59373edca Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 11 Aug 2026 17:21:41 +0000 Subject: [PATCH 1/4] Propagate provenance honesty through policy run; progress 20260811T171522Z --- HexInterval/Experiment/TargetRun.lean | 218 ++++++++++++++++++ HexInterval/SPEC/hex-interval.md | 33 ++- .../ExpSignConformance.lean | 78 ++++++- lakefile.lean | 1 + progress/20260811T140200Z.md | 32 +++ progress/20260811T164450Z.md | 23 ++ progress/20260811T170026Z.md | 18 ++ .../bench/proof_only_runtime_exemptions.json | 6 + 8 files changed, 398 insertions(+), 11 deletions(-) create mode 100644 HexInterval/Experiment/TargetRun.lean create mode 100644 progress/20260811T140200Z.md create mode 100644 progress/20260811T164450Z.md create mode 100644 progress/20260811T170026Z.md diff --git a/HexInterval/Experiment/TargetRun.lean b/HexInterval/Experiment/TargetRun.lean new file mode 100644 index 000000000..edead69c5 --- /dev/null +++ b/HexInterval/Experiment/TargetRun.lean @@ -0,0 +1,218 @@ +/- +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.PolicySession + +@[expose] public section + +/-! +# Target-directed policy runs + +This experiment drives the proof-producing policy-session boundary until the +current fact entails a requested target, propagation saturates, the external +policy stops, a split is prepared, or a resource is exhausted. The controller +is independent of the fact representation and operation packages. It sees a +bounded policy view and may keep arbitrary private state while choosing among +the engine's checked offers. + +Target detection is only a search stopping condition. It applies the fact +domain's `narrow` operation to the current and requested facts; proof emission +must still resolve the returned version and replay a kernel-checked subsumption +step. A faulty controller or target check can therefore cause failure or extra +work, but cannot establish a theorem. +-/ + +namespace Hex.Interval.Experiment.TargetRun + +open Propagator PolicySession + +/-- One external policy decision. The driver fills in the view identity and +uses the chosen offer's complete semantic key when constructing a selection. -/ +inductive Decision (PolicyState : Type) + | select (offer : Propagator.Policy.OfferView) (next : PolicyState) + | dismiss (offer : Propagator.Policy.OfferView) (next : PolicyState) + | stop (next : PolicyState) + +/-- Observations delivered back to the external policy in execution order. -/ +inductive Event (Fact : Type) + | rule (observation : Propagator.Policy.RuleObservation Fact) + | equality (observation : Propagator.Policy.EqualityObservation Fact) + | instance (completion : Propagator.Policy.Completed) + | dismissed + | rejected (reason : Propagator.Policy.Rejection) + | invalidPayload (error : PayloadArena.Invalid) + | rejectedPayload (resource : PayloadArena.Resource) + +/-- An arbitrary upgradeable policy over bounded engine-owned views. -/ +structure Controller (Fact PolicyState : Type) where + update : PolicyState -> Event Fact -> PolicyState + choose : PolicyState -> Propagator.Policy.View Fact -> Decision PolicyState + +/-- The exact retained fact version which triggered target stopping. -/ +structure Reached (Fact : Type) where + seen : SeenVersion + fact : Fact + +/-- Why a target-directed run stopped. -/ +inductive Stop (Fact : Type) + | target (reached : Reached Fact) + | saturated + | contradiction + | split (plan : Propagator.Policy.SplitPlan Fact) + | policyStop (liveOffers : Nat) + | incomplete + | viewResource (error : Propagator.Policy.ViewError) + | engineResource (resource : Propagator.Resource) + | factResource (budget : Nat) + | payloadResource (resource : PayloadArena.Resource) + | invalidReply (error : ReplyError) + | invalidPayload (error : PayloadArena.Invalid) + | rejected (reason : Propagator.Policy.Rejection) + | invalidSession + | fuel + +/-- A run retains the single coherent proof-producing session, arbitrary +policy state, all delivered observations, and its precise stopping reason. -/ +structure Result (Fact PolicyState : Type) where + session : Session Fact + policyState : PolicyState + events : Array (Event Fact) + stop : Stop Fact + +def selection (view : Propagator.Policy.View Fact) + (offer : Propagator.Policy.OfferView) : Propagator.Policy.Selection := + { scope := view.scope + serial := view.serial + programVersion := view.programVersion + id := offer.id + expected := offer.key } + +/-- Check whether the installed fact entails the requested target. This is a +runtime search test, not proof evidence. -/ +def reached? (domain : FactDomain Fact) (target : NodeId) (requested : Fact) + (session : Session Fact) : Option (Reached Fact) := do + let instruction <- session.state.engine.program.node? target + let current <- session.state.engine.facts[target.index]? + let version <- session.state.engine.versions[target.index]? + match domain.narrow instruction.domain current requested with + | .noChange => some { seen := { node := target, version }, fact := current } + | .improved _ | .contradiction _ | .malformed _ | .resourceLimit _ => none + +def record (controller : Controller Fact PolicyState) (event : Event Fact) + (policyState : PolicyState) (events : Array (Event Fact)) : + PolicyState × Array (Event Fact) := + (controller.update policyState event, events.push event) + +def finish (session : Session Fact) (policyState : PolicyState) + (events : Array (Event Fact)) (stop : Stop Fact) : Result Fact PolicyState := + { session, policyState, events, stop } + +/-- Consume one policy-session transition. Recoverable outcomes call the +supplied continuation; terminal outcomes retain the coherent returned session. -/ +def continueWith (controller : Controller Fact PolicyState) + (resume : Session Fact -> PolicyState -> Array (Event Fact) -> Result Fact PolicyState) + (policyState : PolicyState) (events : Array (Event Fact)) + (step : PolicySession.Step Fact) : Result Fact PolicyState := + match step with + | .rule _ observation session => + let (policyState, events) := + record controller (.rule observation) policyState events + resume session policyState events + | .equality _ observation session => + let (policyState, events) := + record controller (.equality observation) policyState events + resume session policyState events + | .instance _ completion session => + let (policyState, events) := + record controller (.instance completion) policyState events + resume session policyState events + | .dismissed _ session => + let (policyState, events) := record controller .dismissed policyState events + resume session policyState events + | .split _ plan session => finish session policyState events (.split plan) + | .rejected _ reason session => + let (policyState, events) := + record controller (.rejected reason) policyState events + if session.live then + resume session policyState events + else + finish session policyState events (.rejected reason) + | .contradiction session => finish session policyState events .contradiction + | .engineResource resource session => + finish session policyState events (.engineResource resource) + | .factResource budget session => + finish session policyState events (.factResource budget) + | .invalidReply error session => + finish session policyState events (.invalidReply error) + | .invalidPayload error session => + let (policyState, events) := + record controller (.invalidPayload error) policyState events + if session.live then + resume session policyState events + else + finish session policyState events (.invalidPayload error) + | .rejectedPayload resource session => + let (policyState, events) := + record controller (.rejectedPayload resource) policyState events + resume session policyState events + | .payloadResource resource session => + finish session policyState events (.payloadResource resource) + | .invalidSession session => finish session policyState events .invalidSession + +/-- Execute a bounded external policy from one coherent proof-producing +session. Split plans are returned to the caller; branch creation is a later +layer. -/ +def driveFrom (domain : FactDomain Fact) (target : NodeId) (requested : Fact) + (controller : Controller Fact PolicyState) : + Nat -> Session Fact -> PolicyState -> Array (Event Fact) -> Result Fact PolicyState + | fuel, session, policyState, events => + if session.state.engine.contradictory then + finish session policyState events .contradiction + else + match reached? domain target requested session with + | some reached => finish session policyState events (.target reached) + | none => + match session.view with + | .resource error next => + finish next policyState events (.viewResource error) + | .contradiction next => + finish next policyState events .contradiction + | .invalidSession next => + finish next policyState events .invalidSession + | .ready view viewed => + if view.offers.isEmpty then + if viewed.complete then + finish viewed policyState events .saturated + else + finish viewed policyState events .incomplete + else + match fuel with + | 0 => finish viewed policyState events .fuel + | remaining + 1 => + let decision := controller.choose policyState view + match decision with + | .stop next => + finish viewed next events (.policyStop view.offers.size) + | .select offer next => + continueWith controller + (driveFrom domain target requested controller remaining) next events + (viewed.choose (.select (selection view offer))) + | .dismiss offer next => + continueWith controller + (driveFrom domain target requested controller remaining) next events + (viewed.choose (.dismiss (selection view offer))) + +termination_by fuel => fuel + +/-- Start a target-directed run with an empty policy-observation stream. -/ +def drive (domain : FactDomain Fact) (target : NodeId) (requested : Fact) + (controller : Controller Fact PolicyState) (fuel : Nat) + (session : Session Fact) (policyState : PolicyState) : Result Fact PolicyState := + driveFrom domain target requested controller fuel session policyState #[] + +end Hex.Interval.Experiment.TargetRun diff --git a/HexInterval/SPEC/hex-interval.md b/HexInterval/SPEC/hex-interval.md index 6b7989360..ebdc99b9a 100644 --- a/HexInterval/SPEC/hex-interval.md +++ b/HexInterval/SPEC/hex-interval.md @@ -1460,13 +1460,32 @@ and it proves `0 ≤ exp (exp x)` from a three-node target graph. Neither case adds a nested-exponential or extra-hypothesis branch to goal closure, semantic model construction, dependency assembly, or proof replay. -This vertical deliberately selects one target rule whose first improvement is -version one. General search must instead let the policy run until target -subsumption, contradiction, or a resource limit and then select the resolved -target version from the retained proof table. The current operation registry -also remains the fixed source/exponential pair. Key-resolved semantic model -selection must land before operation packages may be reordered; array position -is not a permanent package identity. +The target-run experiment removes that one-rule scheduling restriction. +`TargetRun.Controller` is polymorphic in the fact type and in arbitrary +policy-private state. It sees only bounded engine-owned views, chooses or +dismisses checked offers, and receives every recoverable observation in order. +The driver retains the single proof-producing `PolicySession` and stops +distinctly on target subsumption, saturation, contradiction, explicit policy +stop, a prepared split, incompleteness, fuel, malformed state, or each resource +class. It derives selections from the chosen offer and the exact view identity; +packages and function names do not occur in the driver. + +Target subsumption is a runtime stopping test: narrowing the current fact by +the requested fact must report no change. The result records the exact current +fact and version, but neither that test nor the controller is proof evidence. +Proof emission must still resolve the retained version and replay an independent +fact-domain subsumption theorem. The exponential conformance policy simply +selects the first offer. On `exp (exp x)` it therefore improves the inner and +outer nodes in two separate steps, stops at the requested outer bound, and +feeds both chronological events to the unchanged generic proof frontend. + +The current conformance closes only when the retained target fact is exactly +the requested fact. Closing from a strictly stronger retained fact is the next +proof-frontend connection. The driver returns split plans but does not yet +create or join proof branches. The operation registry also remains the fixed +source/exponential pair. Key-resolved semantic model selection must land before +operation packages may be reordered; array position is not a permanent package +identity. The dynamic path is still bounded by the exponential package's engine envelope, which permits at most five nodes and node depth four, even though the goal diff --git a/conformance/HexIntervalMathlib/ExpSignConformance.lean b/conformance/HexIntervalMathlib/ExpSignConformance.lean index ace28c097..4adf52b43 100644 --- a/conformance/HexIntervalMathlib/ExpSignConformance.lean +++ b/conformance/HexIntervalMathlib/ExpSignConformance.lean @@ -8,6 +8,7 @@ import HexIntervalMathlib.Experiment.ExpSign import HexInterval.Experiment.GoalFrontend import HexInterval.Experiment.GoalClosure import HexInterval.Experiment.ProofFrontend +import HexInterval.Experiment.TargetRun import Mathlib.Lean.Elab.Tactic.Meta /-! @@ -212,6 +213,37 @@ def fixtureInput? (input : CheckerInput Bound) : Option Fixture := do | .ok registry => some { session, registry } | .error _ => none +private def firstOffer : TargetRun.Controller Bound Unit := + { update := fun state _ => state + choose := fun state view => + match view.offers[0]? with + | some offer => .select offer state + | none => .stop state } + +private def stopPolicy : TargetRun.Controller Bound Unit := + { update := fun state _ => state + choose := fun state _ => .stop state } + +structure RunFixture extends Fixture where + reached : TargetRun.Reached Bound + events : Array (TargetRun.Event Bound) + +def runRaw? (input : CheckerInput Bound) (controller : TargetRun.Controller Bound Unit) + (fuel : Nat) : Option (TargetRun.Result Bound Unit) := do + let .ok session := PolicySession.Session.start factDomain + input.baseProgram packages input.initialFacts limits + | none + some (TargetRun.drive factDomain input.target.node input.target.fact controller + fuel session ()) + +def runInput? (input : CheckerInput Bound) : Option RunFixture := do + let result <- runRaw? input firstOffer limits.policy.maxDecisions + let .target reached := result.stop | none + match ProofRegistry.build result.session.registry proofPackages with + | .ok registry => + some { session := result.session, registry, reached, events := result.events } + | .error _ => none + #guard fixture?.any fun fixture => fixture.registry.emit.find? expFactSchema.key == some ``expFactSchema @@ -245,6 +277,46 @@ private def nestedInput : CheckerInput Bound := initialFacts := #[.all, .all, .all] target := { node := node 2, fact := .nonnegative } } +#guard + runInput? nestedInput |>.any fun fixture => + fixture.reached.seen == ({ node := node 2, version := 1 } : SeenVersion) && + fixture.reached.fact == .nonnegative && fixture.events.size == 2 && + fixture.session.state.engine.facts == + #[.all, .nonnegative, .nonnegative] && + fixture.session.state.engine.chronology == #[.fact 0, .fact 1] + +#guard + runRaw? nestedInput firstOffer 0 |>.any fun result => + match result.stop with + | .fuel => result.events.isEmpty + | _ => false + +#guard + runRaw? nestedInput stopPolicy limits.policy.maxDecisions |>.any fun result => + match result.stop with + | .policyStop live => live == 2 && result.events.isEmpty + | _ => false + +private def initiallyReached : CheckerInput Bound := + { nestedInput with target := { node := node 0, fact := .all } } + +#guard + runRaw? initiallyReached firstOffer 0 |>.any fun result => + match result.stop with + | .target reached => + reached.seen == ({ node := node 0, version := 0 } : SeenVersion) && + reached.fact == .all && result.events.isEmpty + | _ => false + +private def unreachableTarget : CheckerInput Bound := + { nestedInput with target := { node := node 2, fact := .empty } } + +#guard + runRaw? unreachableTarget firstOffer limits.policy.maxDecisions |>.any fun result => + match result.stop with + | .saturated => result.events.size == 2 && result.session.complete + | _ => false + private def nestedAction : Action := { serial := 0 programVersion := 0 @@ -392,7 +464,7 @@ private def inputContext (result : GoalFrontend.Result Bound) private meta def emitInput (result : GoalFrontend.Result Bound) (base : GoalClosure.BaseProof) : MetaM Expr := do - let some fixture := fixtureInput? result.input + let some fixture := runInput? result.input | throwError "interval_exp: dynamic search or proof registry failed" let some trace := Frontend.trace? fixture.session.state.engine fixture.session.arena | throwError "interval_exp: dynamic chronology quotation failed" @@ -400,10 +472,8 @@ private meta def emitInput (result : GoalFrontend.Result Bound) throwError "interval_exp: exponential rule unexpectedly changed the graph" let state ← ProofFrontend.emitTrace (inputContext result base) trace.program trace.events fixture.registry.emit - let target : SeenVersion := - { node := result.input.target.node, version := 1 } let some proof := - ProofFrontend.findProof? state.known target result.input.target.fact + ProofFrontend.findProof? state.known fixture.reached.seen result.input.target.fact | throwError "interval_exp: dynamic target fact was not emitted" pure proof diff --git a/lakefile.lean b/lakefile.lean index f31652502..4c861820d 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -306,6 +306,7 @@ lean_lib HexIntervalExperiment where `HexInterval.Experiment.PayloadArena, `HexInterval.Experiment.PayloadSession, `HexInterval.Experiment.PolicySession, + `HexInterval.Experiment.TargetRun, `HexInterval.Experiment.SemanticReplay, `HexInterval.Experiment.ChronologicalReplay, `HexInterval.Experiment.GenericInstanceReconstruction, diff --git a/progress/20260811T140200Z.md b/progress/20260811T140200Z.md new file mode 100644 index 000000000..73c2ca4c9 --- /dev/null +++ b/progress/20260811T140200Z.md @@ -0,0 +1,32 @@ +# Target-directed policy runs + +## Accomplished + +- Added a Mathlib-free target runner over the proof-producing policy session. + Arbitrary external controllers can select, dismiss, or stop from bounded + views while retaining private policy state and ordered observations. +- Distinguished target success, saturation, contradiction, prepared splits, + incompleteness, policy stop, fuel, malformed state, and resource failures. +- Kept target subsumption as an untrusted runtime stopping test and retained + the exact installed fact version for later kernel-checked closure. +- Replaced the exponential canary's one-target-offer choice with the generic + runner. The first-offer policy proves nested exponential positivity through + two chronological propagator steps with no function case in the runner. +- Added guards for initial target success, fuel exhaustion, policy stop, + saturation, and the two-step nested target run. + +## Current frontier + +General propagation now runs from the reified graph until the requested fact +is reached. The conformance proof frontend still closes only when the installed +target fact exactly equals the requested fact. + +## Next step + +Connect a strictly stronger installed target fact to the existing generic +fact-domain subsumption proof, then add proof-branch ownership around returned +split plans. + +## Blockers + +None. diff --git a/progress/20260811T164450Z.md b/progress/20260811T164450Z.md new file mode 100644 index 000000000..cf13f4070 --- /dev/null +++ b/progress/20260811T164450Z.md @@ -0,0 +1,23 @@ +# Accomplished + +- Reconciled the generic target-run controller with dynamic reified-goal + execution and the repaired proof frontend stack. +- Preserved exhaustive policy-step handling, bounded controller fuel, exact + target/version selection, and kernel-checked final emission. +- Updated the proof-only Lake exemption to the exact reconciled target-run + registration blob while retaining current factorization exemptions. + +# Current frontier + +The function-agnostic controller can drive a policy session until a requested +fact is reached, contradiction is reported, work saturates, or a resource stop +occurs. It does not yet manage multiple retained subdivision branches. + +# Next step + +Finish builds and checks, push the exact head for review, then reconcile target +subsumption and the proof-side split/join stack. + +# Blockers + +None. diff --git a/progress/20260811T170026Z.md b/progress/20260811T170026Z.md new file mode 100644 index 000000000..14369643d --- /dev/null +++ b/progress/20260811T170026Z.md @@ -0,0 +1,18 @@ +# Accomplished + +- Propagated both compile-checked modeled-goal axiom reports through the + generic policy runner. + +# Current frontier + +Policy execution is unchanged; the generated goal-closure theorems now retain +their explicit standard-axiom regression checks in this descendant. + +# Next step + +Push after the focused build, then propagate the guards through target closure +and the branch stack. + +# Blockers + +None. diff --git a/scripts/bench/proof_only_runtime_exemptions.json b/scripts/bench/proof_only_runtime_exemptions.json index c6167603a..9b69ae11a 100644 --- a/scripts/bench/proof_only_runtime_exemptions.json +++ b/scripts/bench/proof_only_runtime_exemptions.json @@ -125,6 +125,12 @@ "current_blob": "f316525022094da9ec017e2268c929dcc1193816", "reason": "Additionally registers the generic interval goal-closure proof bridge only; the factorization service target and executable dependency graph are unchanged." }, + { + "path": "lakefile.lean", + "baseline_blob": "6dd80771ae2212333b2a9b925b52056e0037ff56", + "current_blob": "4c861820dbf8db07758455a01f04156f59ad2439", + "reason": "Additionally registers the Mathlib-free interval target-run driver only; the factorization service target and executable dependency graph are unchanged." + }, { "path": "HexBerlekamp/FactorTacticTests.lean", "baseline_blob": "4063e15934a89c671ac72d201fa60c2ef6feaf59", From c2f5aa63984d3a8eecb863cdd6aeb0060eeaa3b3 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 12 Aug 2026 05:10:29 +0000 Subject: [PATCH 2/4] chore(interval): reconcile target run onto main; progress 20260812T050638Z --- progress/20260812T050638Z.md | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) create mode 100644 progress/20260812T050638Z.md diff --git a/progress/20260812T050638Z.md b/progress/20260812T050638Z.md new file mode 100644 index 000000000..20ae71360 --- /dev/null +++ b/progress/20260812T050638Z.md @@ -0,0 +1,24 @@ +# Accomplished + +- Reconciled the generic target-run feature onto current `main` after the + dynamic-goal frontend merged. +- Preserved the target-run and exponential conformance Lean patches exactly, + including live target-version selection and ordinary proof replay. +- Retained the dynamic-goal resource-envelope disclosure and guarded axiom + reports; verified the existing proof-only Lake exemption matches this head. + +# Current frontier + +The target runner owns one coherent policy session and distinguishes its +runtime stopping outcomes. The exponential vertical replays the exact retained +target version, but currently closes only when the retained fact equals the +requested fact. + +# Next step + +Add kernel-checked closure from a strictly stronger retained fact, then connect +prepared split plans to branch-owned execution and proof joining. + +# Blockers + +None. From 3eb59f936a5461f16e1a73882a5f80215c0b568a Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 12 Aug 2026 05:27:36 +0000 Subject: [PATCH 3/4] docs(interval): align target-run diagnostic claims; progress 20260812T050638Z --- HexInterval/SPEC/hex-interval.md | 34 +++++++++++++++++--------------- progress/20260812T050638Z.md | 2 ++ 2 files changed, 20 insertions(+), 16 deletions(-) diff --git a/HexInterval/SPEC/hex-interval.md b/HexInterval/SPEC/hex-interval.md index ebdc99b9a..278294ae5 100644 --- a/HexInterval/SPEC/hex-interval.md +++ b/HexInterval/SPEC/hex-interval.md @@ -1450,17 +1450,16 @@ actual reified goal. One variant closes from the live exponential replay; a second consumes a caller hypothesis through the ordered seed path. Neither uses `native_decide`. -This experiment removes the exponential canary's fixed compiled trace. -It starts `PolicySession` from the reifier's actual `CheckerInput`, selects an -offer anchored at the actual target node, quotes that resulting session, and -feeds it to `ProofFrontend` with the dynamic base program, facts, and reflexive -extension proofs. The ordinary tactic theorem now accepts an unrelated -supported exponential hypothesis which appends two nodes after the target, -and it proves `0 ≤ exp (exp x)` from a three-node target graph. Neither case -adds a nested-exponential or extra-hypothesis branch to goal closure, semantic -model construction, dependency assembly, or proof replay. - -The target-run experiment removes that one-rule scheduling restriction. +The dynamic exponential vertical removes the canary's fixed compiled trace. It +starts `PolicySession` from the reifier's actual `CheckerInput`, runs the +target-directed controller below, quotes the retained session, and feeds it to +`ProofFrontend` with the dynamic base program, facts, and reflexive extension +proofs. The ordinary tactic theorem accepts an unrelated supported exponential +hypothesis which appends two nodes after the target, and it proves +`0 ≤ exp (exp x)` from a three-node target graph. Neither case adds a nested- +exponential or extra-hypothesis branch to goal closure, semantic model +construction, dependency assembly, or proof replay. + `TargetRun.Controller` is polymorphic in the fact type and in arbitrary policy-private state. It sees only bounded engine-owned views, chooses or dismisses checked offers, and receives every recoverable observation in order. @@ -1492,11 +1491,14 @@ which permits at most five nodes and node depth four, even though the goal reifier admits up to sixteen nodes and expression depth eight. Thus the single unrelated supported hypothesis above fits, while two such hypotheses or a sufficiently deep nested target fail at session preflight before search. The -current canary helper also collapses that resource stop, absence of a matching -offer, rule failure, and proof-registry failure into one generic diagnostic. -Aligning the two envelopes and preserving the typed stop reason in tactic -diagnostics remain future frontend work; neither limitation is a theorem- -production assumption. +current tactic adapter also collapses session-start failure, every non-target +`TargetRun` stop, and proof-registry failure into one generic diagnostic. +Separately, a missing target or a malformed or resource-limited fact-domain +target probe is conservatively treated as not yet reached, so search may +continue and later return another stop reason. Aligning the two envelopes and +preserving typed session-start, run-stop, and target-probe reasons in tactic +diagnostics remain future frontend work; none of these limitations is a +theorem-production assumption. 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 diff --git a/progress/20260812T050638Z.md b/progress/20260812T050638Z.md index 20ae71360..854cb31ca 100644 --- a/progress/20260812T050638Z.md +++ b/progress/20260812T050638Z.md @@ -6,6 +6,8 @@ including live target-version selection and ordinary proof replay. - Retained the dynamic-goal resource-envelope disclosure and guarded axiom reports; verified the existing proof-only Lake exemption matches this head. +- Updated the SPEC's dynamic-session and diagnostic wording for the generic + multi-step runner, including conservative target-probe failures. # Current frontier From 3cd78d02bcc17a063e8d9f6e94b294ccf6fb1243 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 14 Aug 2026 09:41:40 +0000 Subject: [PATCH 4/4] chore(interval): restack target run onto main; progress 20260814T093731Z --- progress/20260814T093731Z.md | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) create mode 100644 progress/20260814T093731Z.md diff --git a/progress/20260814T093731Z.md b/progress/20260814T093731Z.md new file mode 100644 index 000000000..c712140eb --- /dev/null +++ b/progress/20260814T093731Z.md @@ -0,0 +1,23 @@ +# Accomplished + +- Restacked the approved target-run feature and SPEC-honesty commits onto + current `main` after unrelated finite-field work advanced the base. +- Verified range-diff equality for all three commits and exact patch-ID fidelity + for both TargetRun and exponential conformance Lean changes. +- Preserved current-main content, the dynamic resource/provenance/axiom wording, + and the existing exact proof-only Lake exemption. + +# Current frontier + +The generic target runner and its two-step exponential proof vertical are +unchanged. The PR now has current-main ancestry and requires only exact-head +review and CI before merge readiness. + +# Next step + +Complete the exact-head review and CI gates, then continue with kernel closure +from strictly stronger retained facts and branch execution for split plans. + +# Blockers + +None.