From 3f45d03c8f7f9ff4b5f4c5061f2b33b3e3fe81d1 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 11 Aug 2026 17:20:49 +0000 Subject: [PATCH 1/2] Propagate provenance honesty through dynamic goal; progress 20260811T171522Z --- HexInterval/SPEC/hex-interval.md | 33 ++++++--- .../ExpSignConformance.lean | 74 +++++++++++++++++-- progress/20260811T134139Z.md | 25 +++++++ progress/20260811T164326Z.md | 22 ++++++ progress/20260811T165931Z.md | 20 +++++ 5 files changed, 154 insertions(+), 20 deletions(-) create mode 100644 progress/20260811T134139Z.md create mode 100644 progress/20260811T164326Z.md create mode 100644 progress/20260811T165931Z.md diff --git a/HexInterval/SPEC/hex-interval.md b/HexInterval/SPEC/hex-interval.md index a9819e45a..544eaef8b 100644 --- a/HexInterval/SPEC/hex-interval.md +++ b/HexInterval/SPEC/hex-interval.md @@ -1392,9 +1392,10 @@ 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. `GoalClosure` now supplies those two proof bridges; running compiled -search on the resulting dynamic checker input remains the next frontend -experiment rather than an assumed capability. +recipes. `GoalClosure` supplies those two proof bridges, and the dynamic +exponential vertical below now starts compiled search on the resulting checker +input. A general policy-driven target-closure loop remains future work rather +than an assumed capability. The first package-composed semantics experiment removes a second fixed-graph assumption. An operation-meaning package supplies an opaque operation signature @@ -1448,15 +1449,23 @@ 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 still uses the exponential canary's fixed compiled search -trace when the target is not already a caller fact, so it presently requires -the reified graph to be exactly that two-node target graph. The next step is to -start the generic session from the reifier's `CheckerInput`, select the target -node in that session, and feed its dynamically quoted trace to -`ProofFrontend`. That removes the last exact-graph check and lets supported -hypotheses append unrelated nodes without changing proof production. Key- -resolved semantic model selection must land before operation packages may be -reordered; array position is not a permanent package identity. +The next 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. + +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 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/conformance/HexIntervalMathlib/ExpSignConformance.lean b/conformance/HexIntervalMathlib/ExpSignConformance.lean index 2e2b3e218..ace28c097 100644 --- a/conformance/HexIntervalMathlib/ExpSignConformance.lean +++ b/conformance/HexIntervalMathlib/ExpSignConformance.lean @@ -161,12 +161,15 @@ def offer? (session : PolicySession.Session Bound) viewed) | .resource _ _ | .contradiction _ | .invalidSession _ => none -def invokesExp (offer : Propagator.Policy.OfferView) : Bool := +def invokesExpAt (target : NodeId) (offer : Propagator.Policy.OfferView) : Bool := match offer.key with | .invoke invocation => - invocation.rule == expRuleKey && invocation.anchor == node 1 + invocation.rule == expRuleKey && invocation.anchor == target | _ => false +def invokesExp (offer : Propagator.Policy.OfferView) : Bool := + invokesExpAt (node 1) offer + def contracted? : Option (PolicySession.Session Bound) := do let .ok session := start | none let (_, selection, viewed) ← offer? session invokesExp @@ -195,6 +198,20 @@ def fixture? : Option Fixture := do | .ok registry => some { session, registry } | .error _ => none +def fixtureInput? (input : CheckerInput Bound) : Option Fixture := do + let .ok session := PolicySession.Session.start factDomain + input.baseProgram packages input.initialFacts limits + | none + let (_, selection, viewed) ← offer? session (invokesExpAt input.target.node) + let session ← + match viewed.choose (.select selection) with + | .rule _ observation next => + if observation.outcome == .success then some next else none + | _ => none + match ProofRegistry.build session.registry proofPackages with + | .ok registry => some { session, registry } + | .error _ => none + #guard fixture?.any fun fixture => fixture.registry.emit.find? expFactSchema.key == some ``expFactSchema @@ -352,13 +369,49 @@ private meta def emitEvidence : MetaM Expr := do | throwError "interval_exp: target fact was not emitted" pure proof +private def inputContext (result : GoalFrontend.Result Bound) + (base : GoalClosure.BaseProof) : ProofFrontend.Context Bound Name := + { encoder := boundEncoder + resolveSchema := pure + semantics := mkConst ``semantics + domain := mkConst ``boundSchema + laws := mkConst ``laws + stableLaw := mkConst ``stableLaw + input := base.input + assumed := ``seedAssumed + baseFacts := result.baseFacts + baseFactsTerm := base.facts + baseProgram := result.input.baseProgram + baseProgramTerm := base.program + basePrefix := base.basePrefix + baseWithin := base.within + initialExtension := base.extension + finalPrefix := base.basePrefix + sameOperations := base.sameOperations + top := boundSchema.top } + +private meta def emitInput (result : GoalFrontend.Result Bound) + (base : GoalClosure.BaseProof) : MetaM Expr := do + let some fixture := fixtureInput? 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" + unless trace.program == result.input.baseProgram do + 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 + | throwError "interval_exp: dynamic target fact was not emitted" + pure proof + private def expTarget (x : ℝ) : Prop := 0 ≤ Real.exp x private meta def proveModeledExp (target : Expr) : MetaM Expr := do let result ← reifyGoal target - unless result.input.baseProgram == ExpSign.program do - throwError "interval_exp model test: expected the exact target graph" let some fallback := GoalClosure.termAt? result.terms { index := 0 } | throwError "interval_exp model test: missing source expression" if (← observing? <| GoalClosure.proveModel (mkConst ``Real) fallback @@ -385,10 +438,7 @@ private meta def proveModeledExp (target : Expr) : MetaM Expr := do mkAppM ``seedAssumed #[base.program, base.facts, mkNatLit index, factTerm, found] | none => - if result.baseFacts == ExpSign.baseFacts then - emitEvidence - else - throwError "interval_exp model test: fixed trace has different base facts" + emitInput result base let proof ← mkAppM ``Evidence.proof #[evidence, model.valuation, model.proof, facts] unless ← isDefEq (← inferType proof) target do @@ -425,6 +475,14 @@ info: 'Hex.IntervalMathlib.ExpSignConformance.tacticExpModeledSeed' depends on a #guard_msgs in #print axioms tacticExpModeledSeed +theorem tacticExpModeledExtra (x y : ℝ) (_hy : 0 ≤ Real.exp y) : + 0 ≤ Real.exp x := by + interval_exp_model + +theorem tacticExpModeledNested (x : ℝ) : + 0 ≤ Real.exp (Real.exp x) := by + interval_exp_model + private meta def proveExp (target : Expr) : MetaM Expr := do let reified ← reifyGoal target unless sameTargetGraph reified.input do diff --git a/progress/20260811T134139Z.md b/progress/20260811T134139Z.md new file mode 100644 index 000000000..8aa0ff1a8 --- /dev/null +++ b/progress/20260811T134139Z.md @@ -0,0 +1,25 @@ +# Accomplished + +- Started exponential search from the goal reifier's actual checker input + instead of the fixed two-node fixture. +- Selected the exponential offer at the actual target node and passed that + session's own quoted trace through the generic proof frontend. +- Added ordinary modeled tactic theorems for a graph extended by an unrelated + supported hypothesis and for the distinct three-node goal `exp (exp x)`. + +# Current frontier + +The arbitrary-function frontend now connects goal recognition, dynamic search, +package semantics, proof replay, caller assumptions, and final Lean closure for +several graph shapes. The exponential client deliberately performs one selected +target contraction. + +# Next step + +Replace the one-action exponential driver with a generic policy loop that runs +until target subsumption, contradiction, or a resource limit and then closes +the resolved target version. + +# Blockers + +None. diff --git a/progress/20260811T164326Z.md b/progress/20260811T164326Z.md new file mode 100644 index 000000000..2919e6869 --- /dev/null +++ b/progress/20260811T164326Z.md @@ -0,0 +1,22 @@ +# Accomplished + +- Reconciled dynamic goal execution with the repaired goal-closure, + operation-semantics, and arbitrary-function frontend stack. +- Preserved the policy session's use of the exact reified `CheckerInput`, + dynamic trace quotation, package-composed semantic model, and kernel-checked + target theorem. + +# Current frontier + +The exponential canary no longer requires an exact two-node fixture: nested +and unrelated supported graph nodes can be present while the live policy +session selects the exact target fact and the frontend reconstructs its proof. + +# Next step + +Finish builds and checks, push this exact head for review, then reconcile the +generic policy-run controller and target subsumption layer. + +# Blockers + +None. diff --git a/progress/20260811T165931Z.md b/progress/20260811T165931Z.md new file mode 100644 index 000000000..13f2b5cad --- /dev/null +++ b/progress/20260811T165931Z.md @@ -0,0 +1,20 @@ +# Accomplished + +- Propagated compile-checked axiom reports for both goal-closure exponential + theorems into dynamic goal execution. +- Preserved the extra-node and nested-goal canaries around the new reports. + +# Current frontier + +Dynamic search and proof construction are unchanged. Both earlier modeled-goal +entry points now fail compilation if their axiom dependencies differ from the +standard `propext`, `Classical.choice`, and `Quot.sound` set. + +# Next step + +Push this exact head after focused checks, then propagate the same trust canary +through the policy and branch descendants. + +# Blockers + +None. From 8e157a91a1869e9ca9b905dcd4982942aa598074 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 12 Aug 2026 04:36:58 +0000 Subject: [PATCH 2/2] docs(interval): disclose dynamic goal resource envelope; progress 20260812T043304Z --- HexInterval/SPEC/hex-interval.md | 18 +++++++++++++++--- progress/20260812T043304Z.md | 25 +++++++++++++++++++++++++ 2 files changed, 40 insertions(+), 3 deletions(-) create mode 100644 progress/20260812T043304Z.md diff --git a/HexInterval/SPEC/hex-interval.md b/HexInterval/SPEC/hex-interval.md index 544eaef8b..6b7989360 100644 --- a/HexInterval/SPEC/hex-interval.md +++ b/HexInterval/SPEC/hex-interval.md @@ -1385,8 +1385,9 @@ 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. +fixed-fixture exponential tactic currently requires only the target-reachable +operation and node prefixes, and the target fact, to match its 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 @@ -1449,7 +1450,7 @@ 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`. -The next experiment removes the exponential canary's fixed compiled trace. +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 @@ -1467,6 +1468,17 @@ 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 +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. + 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 expected interleaving before it reads historical values through diff --git a/progress/20260812T043304Z.md b/progress/20260812T043304Z.md new file mode 100644 index 000000000..9322c478a --- /dev/null +++ b/progress/20260812T043304Z.md @@ -0,0 +1,25 @@ +# Accomplished + +- Reconciled the dynamic-goal frontend commit onto current `main` after its + former stacked base merged. +- Preserved the exact reified-input session, dynamic target selection, live + quotation, and generic proof-emission feature patch. +- Documented the tighter exponential engine envelope and its currently generic + resource diagnostic alongside the broader goal-reifier envelope. + +# Current frontier + +The dynamic exponential vertical supports the demonstrated extra-node and +nested-target canaries, but its session preflight remains limited to five nodes +and node depth four even though goal reification accepts sixteen nodes and +expression depth eight. + +# Next step + +Align frontend and engine resource envelopes, preserve typed stop reasons in +tactic diagnostics, and replace the one-action canary driver with a generic +target-closure loop. + +# Blockers + +None.