diff --git a/HexInterval/SPEC/hex-interval.md b/HexInterval/SPEC/hex-interval.md index 4e03e0d53..2b0a249b5 100644 --- a/HexInterval/SPEC/hex-interval.md +++ b/HexInterval/SPEC/hex-interval.md @@ -1711,6 +1711,18 @@ runs the arbitrary exponential propagator in each, and retains two target leaves. Separate guards show that one global step leaves both children pending, and that zero split or one-leaf budgets retain an explicitly blocked root. +A second Mathlib-free runtime canary now makes the scheduling abstraction +observable on live work. Its root splits one source; the side-aware policy +fork sends only the left child to split a second source, while the right child +immediately runs the arbitrary exponential propagator. After the nested split, +the depth-first frontier is `[left-left, left-right, right]` and the +breadth-first frontier is `[right, left-left, left-right]`; both complete to +the same five-node retained tree. This catches an ignored `Side` argument and +an accidental exchange of the scheduler's old and fresh queues. The second +source is deliberately irrelevant to the exponential target, so this is a +scheduling and accounting canary, not the still-required useful nested +subdivision benchmark. + This runtime tree contains no proof evidence. The separate generic `BranchProof` frontend now folds a settled retained tree bottom-up. It first binds every leaf and split result back to its exact scope, base program, and diff --git a/conformance/HexInterval/NestedBranchConformance.lean b/conformance/HexInterval/NestedBranchConformance.lean new file mode 100644 index 000000000..bddca0b52 --- /dev/null +++ b/conformance/HexInterval/NestedBranchConformance.lean @@ -0,0 +1,164 @@ +/- +Copyright (c) 2026 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kim Morrison +-/ + +import HexInterval.Experiment.BranchTree +import HexInterval.Experiment.ExpSign + +/-! +# Nested branch scheduling conformance + +This Mathlib-free canary builds a live two-level split tree. The left child +splits a second source while the right child closes immediately, so the child +policy fork is genuinely side-sensitive and depth-first and breadth-first +frontiers differ on live pending work. +-/ + +namespace Hex.Interval.NestedBranchConformance + +open Experiment +open Propagator PolicySession SemanticReplay TargetRun BranchStart BranchTree +open ExpSign + +private def program : Program := + { operations + nodes := #[sourceInstruction, sourceInstruction, expInstruction] } + +private def target : NodeFact Bound := + { node := node 2, fact := .nonnegative } + +private def input : CheckerInput Bound := + { baseProgram := program + initialFacts := #[.all, .all, .all] + target } + +private inductive Route where + | root + | splitLeft + | close + deriving DecidableEq, Repr + +private def splitAt (wanted : NodeId) (view : Policy.View Bound) : + Option Policy.OfferView := + view.offers.toList.find? fun offer => + match offer.key with + | .invoke invocation => + invocation.rule == splitRuleKey && invocation.anchor == wanted + | .split _ seen _ _ => seen.node == wanted + | _ => false + +private def expAt (wanted : NodeId) (view : Policy.View Bound) : + Option Policy.OfferView := + view.offers.toList.find? fun offer => + match offer.key with + | .invoke invocation => + invocation.rule == expRuleKey && invocation.anchor == wanted + | _ => false + +private def controller : Controller Bound Route := + { update := fun state _ => state + choose := fun state view => + let selected := + match state with + | .root => splitAt (node 0) view + | .splitLeft => splitAt (node 1) view + | .close => expAt (node 2) view + match selected with + | some offer => .select offer state + | none => .stop state } + +private def fork : Route -> Side -> Route + | .root, .left => .splitLeft + | .root, .right => .close + | .splitLeft, _ => .close + | .close, _ => .close + +private def splitter : Splitter Bound := + { split := fun graph splitNode instruction parent point => + if graph.node? splitNode == some instruction && + instruction.domain == real && parent == .all && point == 0 then + some (.nonnegative, .negative) + else + none } + +private def resources : BranchTree.Limits := + { branch := { maxDepth := 3, maxScopes := 5 } + maxSteps := 5 + maxSplits := 2 + maxLeaves := 3 + leafFuel := limits.policy.maxDecisions } + +private def config (order : Order) : Config Bound Route := + { factDomain + packages := splitPackages + sessionLimits := limits + controller + splitter + forkPolicy := fork + order + limits := resources } + +private def run? (order : Order) (fuel : Nat) : Option (State Bound Route) := do + let .ok state := BranchTree.start (config order) { index := 0 } input .root + | none + let .ok state := BranchTree.runFrom (config order) fuel state | none + some state + +private def leafReached? (entry : Node Bound Route) : Bool := + match entry with + | .leaf source (.result result) => + source.input.target == target && + match result.stop with + | .target reached => reached.seen.node == target.node && + reached.fact == .nonnegative + | _ => false + | _ => false + +#guard fork .root .left == .splitLeft +#guard fork .root .right == .close + +#guard + (run? .depthFirst 2).any fun state => + state.steps == 2 && state.splits == 2 && state.leaves == 3 && + state.frontier == [{ index := 3 }, { index := 4 }, { index := 2 }] + +#guard + (run? .breadthFirst 2).any fun state => + state.steps == 2 && state.splits == 2 && state.leaves == 3 && + state.frontier == [{ index := 2 }, { index := 3 }, { index := 4 }] + +#guard + (run? .depthFirst 5).any fun state => + state.settled && state.steps == 5 && state.splits == 2 && + state.leaves == 3 && state.nodes.size == 5 && + match state.nodes[0]?, state.nodes[1]?, state.nodes[2]?, + state.nodes[3]?, state.nodes[4]? with + | some (BranchTree.Node.split root _ rootChildren left right), + some (BranchTree.Node.split nested _ nestedChildren nestedLeft nestedRight), + some rightLeaf, some nestedLeftLeaf, some nestedRightLeaf => + root.policyState == .root && left.index == 1 && right.index == 2 && + rootChildren.leftScope.index == 1 && + rootChildren.rightScope.index == 2 && + rootChildren.left.initialFacts == #[.nonnegative, .all, .all] && + rootChildren.right.initialFacts == #[.negative, .all, .all] && + nested.policyState == .splitLeft && + nestedLeft.index == 3 && nestedRight.index == 4 && + nestedChildren.leftScope.index == 3 && + nestedChildren.rightScope.index == 4 && + nestedChildren.left.initialFacts == + #[.nonnegative, .nonnegative, .all] && + nestedChildren.right.initialFacts == + #[.nonnegative, .negative, .all] && + leafReached? rightLeaf && leafReached? nestedLeftLeaf && + leafReached? nestedRightLeaf + | _, _, _, _, _ => false + +#guard + (run? .breadthFirst 5).any fun state => + state.settled && state.steps == 5 && state.splits == 2 && + state.leaves == 3 && state.nodes.size == 5 && + state.nodes.toList.countP leafReached? == 3 + +end Hex.Interval.NestedBranchConformance diff --git a/lakefile.lean b/lakefile.lean index 294301877..a869c195a 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -402,7 +402,7 @@ lean_lib HexRCFProofProbeScientific where -- `*_emit_fixtures` exes below, carrying `srcDir := "conformance"`. lean_lib HexConformance where srcDir := "conformance" - globs := #[`HexArith.Conformance, `HexArith.CrossCheck, `HexBerlekamp.Conformance, `HexBerlekampZassenhaus.Conformance, `HexBerlekampZassenhaus.CrossCheck, `HexConway.Conformance, `HexGF2.Conformance, `HexGF2.CrossCheck, `HexGF2.FastCheck, `HexGFq.Conformance, `HexGFq.CrossCheck, `HexGFqField.Conformance, `HexGFqRing.Conformance, `HexGramSchmidt.Conformance, `HexHensel.Conformance, `HexHensel.CrossCheck, `HexInterval.Conformance, `HexInterval.CenterConformance, `HexInterval.ScaleConformance, `HexInterval.PropagatorConformance, `HexInterval.ScopeConformance, `HexInterval.StructuralMatcherConformance, `HexInterval.MatcherSchedulerConformance, `HexInterval.StructureViewConformance, `HexInterval.PolicyConformance, `HexInterval.PolicyFrontierConformance, `HexInterval.PolicyDriverConformance, `HexInterval.PackageRegistryConformance, `HexInterval.DyadicIntervalConformance, `HexInterval.DyadicRulesConformance, `HexInterval.PayloadArenaConformance, `HexInterval.PayloadSessionConformance, `HexInterval.PolicySessionConformance, `HexInterval.PolicyFunctionConformance, `HexInterval.SemanticReplayConformance, `HexInterval.ChronologicalReplayConformance, `HexInterval.GenericInstanceReconstructionConformance, `HexInterval.ProofEmitterConformance, `HexInterval.TraceReplayConformance, `HexInterval.SinTenIntervalConformance, `HexIntervalMathlib.SineSignConformance, `HexIntervalMathlib.SineProofConformance, `HexIntervalMathlib.SineTacticConformance, `HexIntervalMathlib.ProofRegistryConformance, `HexIntervalMathlib.ExpSignConformance, `HexIntervalMathlib.ReluConformance, `HexIntervalMathlib.RefuteConformance, `HexIntervalMathlib.PntLogTableConformance, `HexIntervalMathlib.PntNestedLogConformance, `HexIntervalMathlib.PntExpTailConformance, `HexIntervalMathlib.SinTenConformance, `HexIntervalMathlib.SinTenIntervalConformance, `HexLLL.Conformance, `HexMatrix.Conformance, `HexMvPolyFixtures, `HexMvPoly.Conformance, `HexMvPolyMathlib.Conformance, `HexRowReduce.Conformance, `HexDeterminant.Conformance, `HexBareiss.Conformance, `HexModArith.Conformance, `HexModArith.FastCheck, `HexNumberField.Conformance, `HexNumberFieldTower.Conformance, `HexPoly.Conformance, `HexPolyFp.Conformance, `HexPolyZ.Conformance, `HexRCF.Conformance, `HexRealRoots.Conformance, `HexRealRootsMathlib.Conformance, `HexResultant.Conformance, `HexRoots.Conformance].map Glob.one + globs := #[`HexArith.Conformance, `HexArith.CrossCheck, `HexBerlekamp.Conformance, `HexBerlekampZassenhaus.Conformance, `HexBerlekampZassenhaus.CrossCheck, `HexConway.Conformance, `HexGF2.Conformance, `HexGF2.CrossCheck, `HexGF2.FastCheck, `HexGFq.Conformance, `HexGFq.CrossCheck, `HexGFqField.Conformance, `HexGFqRing.Conformance, `HexGramSchmidt.Conformance, `HexHensel.Conformance, `HexHensel.CrossCheck, `HexInterval.Conformance, `HexInterval.CenterConformance, `HexInterval.ScaleConformance, `HexInterval.PropagatorConformance, `HexInterval.ScopeConformance, `HexInterval.StructuralMatcherConformance, `HexInterval.MatcherSchedulerConformance, `HexInterval.NestedBranchConformance, `HexInterval.StructureViewConformance, `HexInterval.PolicyConformance, `HexInterval.PolicyFrontierConformance, `HexInterval.PolicyDriverConformance, `HexInterval.PackageRegistryConformance, `HexInterval.DyadicIntervalConformance, `HexInterval.DyadicRulesConformance, `HexInterval.PayloadArenaConformance, `HexInterval.PayloadSessionConformance, `HexInterval.PolicySessionConformance, `HexInterval.PolicyFunctionConformance, `HexInterval.SemanticReplayConformance, `HexInterval.ChronologicalReplayConformance, `HexInterval.GenericInstanceReconstructionConformance, `HexInterval.ProofEmitterConformance, `HexInterval.TraceReplayConformance, `HexInterval.SinTenIntervalConformance, `HexIntervalMathlib.SineSignConformance, `HexIntervalMathlib.SineProofConformance, `HexIntervalMathlib.SineTacticConformance, `HexIntervalMathlib.ProofRegistryConformance, `HexIntervalMathlib.ExpSignConformance, `HexIntervalMathlib.ReluConformance, `HexIntervalMathlib.RefuteConformance, `HexIntervalMathlib.PntLogTableConformance, `HexIntervalMathlib.PntNestedLogConformance, `HexIntervalMathlib.PntExpTailConformance, `HexIntervalMathlib.SinTenConformance, `HexIntervalMathlib.SinTenIntervalConformance, `HexLLL.Conformance, `HexMatrix.Conformance, `HexMvPolyFixtures, `HexMvPoly.Conformance, `HexMvPolyMathlib.Conformance, `HexRowReduce.Conformance, `HexDeterminant.Conformance, `HexBareiss.Conformance, `HexModArith.Conformance, `HexModArith.FastCheck, `HexNumberField.Conformance, `HexNumberFieldTower.Conformance, `HexPoly.Conformance, `HexPolyFp.Conformance, `HexPolyZ.Conformance, `HexRCF.Conformance, `HexRealRoots.Conformance, `HexRealRootsMathlib.Conformance, `HexResultant.Conformance, `HexRoots.Conformance].map Glob.one -- Public umbrellas intentionally contain only the supported API. Executable -- examples and regression tests are compiled through this separate target so diff --git a/progress/20260811T174943Z.md b/progress/20260811T174943Z.md new file mode 100644 index 000000000..453dc2316 --- /dev/null +++ b/progress/20260811T174943Z.md @@ -0,0 +1,27 @@ +# Accomplished + +- Added a Mathlib-free live two-level branch tree whose left child performs a + second split and whose right child immediately runs the exponential + propagator. +- Made the child policy fork depend on `Side`, so exchanging left and right is + observable in the retained tree. +- Checked the exact live depth-first and breadth-first frontiers after the + nested split, and checked that both orders settle to three target leaves. +- Documented that this second split is intentionally a scheduling canary, not + yet a useful nested subdivision benchmark. + +# Current frontier + +Live scheduling now exercises both delivered frontier orders and a +side-sensitive child policy. The nested split does not affect the target, so +proof-tree recursion and search usefulness are still separate canaries. + +# Next step + +Introduce the first actual interval fact representation with open, closed, +and unbounded endpoints. Reuse the same nested tree with a target whose child +proofs genuinely improve because of subdivision. + +# Blockers + +None. diff --git a/progress/20260814T194607Z.md b/progress/20260814T194607Z.md new file mode 100644 index 000000000..70df06c76 --- /dev/null +++ b/progress/20260814T194607Z.md @@ -0,0 +1,34 @@ +# PR #9226 local reconciliation + +## Accomplished + +- Replayed only the nested live-branch scheduling canary onto exact merged + #9225 main `54b82bee520e74eeab2e15d5fb44a57f82aa969c`. +- Preserved all current branch-proof, PNT-log, Machin, and endpoint-sine + registrations while adding only `HexInterval.NestedBranchConformance` to the + conformance target. +- Audited that the live two-step frontier makes both `schedule rest fresh` + ordering and the `Side` argument to `forkPolicy` observable: depth-first and + breadth-first retain distinct exact frontiers, while either side-insensitive + route breaks the pinned split, leaf, and settled-tree accounting. +- Checked the exact retained node identities, child scopes, inherited fact + arrays, three target leaves, and the SPEC's honest statement that the second + split is target-irrelevant. +- Recomputed the proof-only Lake exemption for exact resolved blob + `d3be6e3f3c99f2bbc3685500563a49f90059d5c1`. +- Built the focused nested-branch and inherited interval targets and passed the + static, trust-surface, freshness, PNT-inventory, diff, and banned-term checks. + +## Current frontier + +- The feature is prepared as a clean local commit on merged #9225 and remains + intentionally unpushed while the exp-tail PR advances `main`. + +## Next step + +- Rebase this prepared feature once onto the final post-exp-tail `main`, refresh + only exact freshness metadata if required, then run final review and CI. + +## Blockers + +- None. diff --git a/progress/20260814T200753Z.md b/progress/20260814T200753Z.md new file mode 100644 index 000000000..9648ae747 --- /dev/null +++ b/progress/20260814T200753Z.md @@ -0,0 +1,28 @@ +# PR #9226 final reconciliation + +## Accomplished + +- Rebased the audited nested-branch scheduling canary onto exact post-#9261 + main `37bda079c4c9974da49c9e8a8559a66d2e671b45`. +- Preserved the complete PNT log-table, nested-log, and exponential-tail + experiments and conformance registrations while adding only the nested-branch + conformance target. +- Refreshed the narrow proof-only Lake exemption to exact resolved blob + `a869c195af5b211b96e848d4f11754abb64ebcc8`. +- Rebuilt the nested-branch and inherited branch-proof, ReLU, PNT, and sine + targets successfully and reran all focused static, trust, freshness, + inventory, diff, and banned-term checks. + +## Current frontier + +- The exact reconciled candidate is ready to push for final independent review + and exact-head CI. + +## Next step + +- Push and retarget PR #9226 to `main`, then require fresh Opus approval and + exact-head CI success before marking it merge-ready. + +## Blockers + +- None. diff --git a/scripts/bench/proof_only_runtime_exemptions.json b/scripts/bench/proof_only_runtime_exemptions.json index 7b92cd389..4aabff9e7 100644 --- a/scripts/bench/proof_only_runtime_exemptions.json +++ b/scripts/bench/proof_only_runtime_exemptions.json @@ -185,6 +185,12 @@ "current_blob": "2943018771d8ab5c7c256f28ce299320c7a646e0", "reason": "Additionally registers the Mathlib-free pinned exponential-tail chronology experiment, its proof-only real-semantics companion, and conformance module; the factorization service target and executable dependency graph are unchanged." }, + { + "path": "lakefile.lean", + "baseline_blob": "6dd80771ae2212333b2a9b925b52056e0037ff56", + "current_blob": "a869c195af5b211b96e848d4f11754abb64ebcc8", + "reason": "Additionally registers the Mathlib-free HexInterval nested-branch conformance module only; the factorization service target and executable dependency graph are unchanged." + }, { "path": "HexBerlekamp/FactorTacticTests.lean", "baseline_blob": "4063e15934a89c671ac72d201fa60c2ef6feaf59",