Skip to content

Commit b4e0336

Browse files
kim-emkim-em
committed
test(interval): exercise nested branch scheduling
1 parent e20ae06 commit b4e0336

5 files changed

Lines changed: 210 additions & 1 deletion

File tree

‎HexInterval/SPEC/hex-interval.md‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1653,6 +1653,18 @@ runs the arbitrary exponential propagator in each, and retains two target
16531653
leaves. Separate guards show that one global step leaves both children pending,
16541654
and that zero split or one-leaf budgets retain an explicitly blocked root.
16551655

1656+
A second Mathlib-free runtime canary now makes the scheduling abstraction
1657+
observable on live work. Its root splits one source; the side-aware policy
1658+
fork sends only the left child to split a second source, while the right child
1659+
immediately runs the arbitrary exponential propagator. After the nested split,
1660+
the depth-first frontier is `[left-left, left-right, right]` and the
1661+
breadth-first frontier is `[right, left-left, left-right]`; both complete to
1662+
the same five-node retained tree. This catches an ignored `Side` argument and
1663+
an accidental exchange of the scheduler's old and fresh queues. The second
1664+
source is deliberately irrelevant to the exponential target, so this is a
1665+
scheduling and accounting canary, not the still-required useful nested
1666+
subdivision benchmark.
1667+
16561668
This runtime tree contains no proof evidence. The separate generic
16571669
`BranchProof` frontend now folds a settled retained tree bottom-up. It first
16581670
binds every leaf and split result back to its exact scope, base program, and

‎conformance/HexInterval/NestedBranchConformance.lean‎

Lines changed: 164 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,164 @@
1+
/-
2+
Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Kim Morrison
5+
-/
6+
7+
import HexInterval.Experiment.BranchTree
8+
import HexInterval.Experiment.ExpSign
9+
10+
/-!
11+
# Nested branch scheduling conformance
12+
13+
This Mathlib-free canary builds a live two-level split tree. The left child
14+
splits a second source while the right child closes immediately, so the child
15+
policy fork is genuinely side-sensitive and depth-first and breadth-first
16+
frontiers differ on live pending work.
17+
-/
18+
19+
namespace Hex.Interval.NestedBranchConformance
20+
21+
open Experiment
22+
open Propagator PolicySession SemanticReplay TargetRun BranchStart BranchTree
23+
open ExpSign
24+
25+
private def program : Program :=
26+
{ operations
27+
nodes := #[sourceInstruction, sourceInstruction, expInstruction] }
28+
29+
private def target : NodeFact Bound :=
30+
{ node := node 2, fact := .nonnegative }
31+
32+
private def input : CheckerInput Bound :=
33+
{ baseProgram := program
34+
initialFacts := #[.all, .all, .all]
35+
target }
36+
37+
private inductive Route where
38+
| root
39+
| splitLeft
40+
| close
41+
deriving DecidableEq, Repr
42+
43+
private def splitAt (wanted : NodeId) (view : Policy.View Bound) :
44+
Option Policy.OfferView :=
45+
view.offers.toList.find? fun offer =>
46+
match offer.key with
47+
| .invoke invocation =>
48+
invocation.rule == splitRuleKey && invocation.anchor == wanted
49+
| .split _ seen _ _ => seen.node == wanted
50+
| _ => false
51+
52+
private def expAt (wanted : NodeId) (view : Policy.View Bound) :
53+
Option Policy.OfferView :=
54+
view.offers.toList.find? fun offer =>
55+
match offer.key with
56+
| .invoke invocation =>
57+
invocation.rule == expRuleKey && invocation.anchor == wanted
58+
| _ => false
59+
60+
private def controller : Controller Bound Route :=
61+
{ update := fun state _ => state
62+
choose := fun state view =>
63+
let selected :=
64+
match state with
65+
| .root => splitAt (node 0) view
66+
| .splitLeft => splitAt (node 1) view
67+
| .close => expAt (node 2) view
68+
match selected with
69+
| some offer => .select offer state
70+
| none => .stop state }
71+
72+
private def fork : Route -> Side -> Route
73+
| .root, .left => .splitLeft
74+
| .root, .right => .close
75+
| .splitLeft, _ => .close
76+
| .close, _ => .close
77+
78+
private def splitter : Splitter Bound :=
79+
{ split := fun graph splitNode instruction parent point =>
80+
if graph.node? splitNode == some instruction &&
81+
instruction.domain == real && parent == .all && point == 0 then
82+
some (.nonnegative, .negative)
83+
else
84+
none }
85+
86+
private def resources : BranchTree.Limits :=
87+
{ branch := { maxDepth := 3, maxScopes := 5 }
88+
maxSteps := 5
89+
maxSplits := 2
90+
maxLeaves := 3
91+
leafFuel := limits.policy.maxDecisions }
92+
93+
private def config (order : Order) : Config Bound Route :=
94+
{ factDomain
95+
packages := splitPackages
96+
sessionLimits := limits
97+
controller
98+
splitter
99+
forkPolicy := fork
100+
order
101+
limits := resources }
102+
103+
private def run? (order : Order) (fuel : Nat) : Option (State Bound Route) := do
104+
let .ok state := BranchTree.start (config order) { index := 0 } input .root
105+
| none
106+
let .ok state := BranchTree.runFrom (config order) fuel state | none
107+
some state
108+
109+
private def leafReached? (entry : Node Bound Route) : Bool :=
110+
match entry with
111+
| .leaf source (.result result) =>
112+
source.input.target == target &&
113+
match result.stop with
114+
| .target reached => reached.seen.node == target.node &&
115+
reached.fact == .nonnegative
116+
| _ => false
117+
| _ => false
118+
119+
#guard fork .root .left == .splitLeft
120+
#guard fork .root .right == .close
121+
122+
#guard
123+
(run? .depthFirst 2).any fun state =>
124+
state.steps == 2 && state.splits == 2 && state.leaves == 3 &&
125+
state.frontier == [{ index := 3 }, { index := 4 }, { index := 2 }]
126+
127+
#guard
128+
(run? .breadthFirst 2).any fun state =>
129+
state.steps == 2 && state.splits == 2 && state.leaves == 3 &&
130+
state.frontier == [{ index := 2 }, { index := 3 }, { index := 4 }]
131+
132+
#guard
133+
(run? .depthFirst 5).any fun state =>
134+
state.settled && state.steps == 5 && state.splits == 2 &&
135+
state.leaves == 3 && state.nodes.size == 5 &&
136+
match state.nodes[0]?, state.nodes[1]?, state.nodes[2]?,
137+
state.nodes[3]?, state.nodes[4]? with
138+
| some (BranchTree.Node.split root _ rootChildren left right),
139+
some (BranchTree.Node.split nested _ nestedChildren nestedLeft nestedRight),
140+
some rightLeaf, some nestedLeftLeaf, some nestedRightLeaf =>
141+
root.policyState == .root && left.index == 1 && right.index == 2 &&
142+
rootChildren.leftScope.index == 1 &&
143+
rootChildren.rightScope.index == 2 &&
144+
rootChildren.left.initialFacts == #[.nonnegative, .all, .all] &&
145+
rootChildren.right.initialFacts == #[.negative, .all, .all] &&
146+
nested.policyState == .splitLeft &&
147+
nestedLeft.index == 3 && nestedRight.index == 4 &&
148+
nestedChildren.leftScope.index == 3 &&
149+
nestedChildren.rightScope.index == 4 &&
150+
nestedChildren.left.initialFacts ==
151+
#[.nonnegative, .nonnegative, .all] &&
152+
nestedChildren.right.initialFacts ==
153+
#[.nonnegative, .negative, .all] &&
154+
leafReached? rightLeaf && leafReached? nestedLeftLeaf &&
155+
leafReached? nestedRightLeaf
156+
| _, _, _, _, _ => false
157+
158+
#guard
159+
(run? .breadthFirst 5).any fun state =>
160+
state.settled && state.steps == 5 && state.splits == 2 &&
161+
state.leaves == 3 && state.nodes.size == 5 &&
162+
state.nodes.toList.countP leafReached? == 3
163+
164+
end Hex.Interval.NestedBranchConformance

‎lakefile.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -392,7 +392,7 @@ lean_lib HexRCFProofProbeScientific where
392392
-- `*_emit_fixtures` exes below, carrying `srcDir := "conformance"`.
393393
lean_lib HexConformance where
394394
srcDir := "conformance"
395-
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, `HexIntervalMathlib.SineSignConformance, `HexIntervalMathlib.SineProofConformance, `HexIntervalMathlib.SineTacticConformance, `HexIntervalMathlib.ProofRegistryConformance, `HexIntervalMathlib.ExpSignConformance, `HexIntervalMathlib.ReluConformance, `HexIntervalMathlib.RefuteConformance, `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
395+
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, `HexIntervalMathlib.SineSignConformance, `HexIntervalMathlib.SineProofConformance, `HexIntervalMathlib.SineTacticConformance, `HexIntervalMathlib.ProofRegistryConformance, `HexIntervalMathlib.ExpSignConformance, `HexIntervalMathlib.ReluConformance, `HexIntervalMathlib.RefuteConformance, `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
396396

397397
-- Public umbrellas intentionally contain only the supported API. Executable
398398
-- examples and regression tests are compiled through this separate target so

‎progress/20260811T174943Z.md‎

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
1+
# Accomplished
2+
3+
- Added a Mathlib-free live two-level branch tree whose left child performs a
4+
second split and whose right child immediately runs the exponential
5+
propagator.
6+
- Made the child policy fork depend on `Side`, so exchanging left and right is
7+
observable in the retained tree.
8+
- Checked the exact live depth-first and breadth-first frontiers after the
9+
nested split, and checked that both orders settle to three target leaves.
10+
- Documented that this second split is intentionally a scheduling canary, not
11+
yet a useful nested subdivision benchmark.
12+
13+
# Current frontier
14+
15+
Live scheduling now exercises both delivered frontier orders and a
16+
side-sensitive child policy. The nested split does not affect the target, so
17+
proof-tree recursion and search usefulness are still separate canaries.
18+
19+
# Next step
20+
21+
Introduce the first actual interval fact representation with open, closed,
22+
and unbounded endpoints. Reuse the same nested tree with a target whose child
23+
proofs genuinely improve because of subdivision.
24+
25+
# Blockers
26+
27+
None.

‎scripts/bench/proof_only_runtime_exemptions.json‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -155,6 +155,12 @@
155155
"current_blob": "b6c186c08df26b407669d53995dca3ffaf8b28e3",
156156
"reason": "Additionally registers the isolated HexInterval branch-proof experiment and its ReLU conformance module only; the factorization service target and executable dependency graph are unchanged."
157157
},
158+
{
159+
"path": "lakefile.lean",
160+
"baseline_blob": "6dd80771ae2212333b2a9b925b52056e0037ff56",
161+
"current_blob": "7ce30195d0df02956ed49017e5fd9a126ccc4777",
162+
"reason": "Additionally registers the Mathlib-free HexInterval nested-branch conformance module only; the factorization service target and executable dependency graph are unchanged."
163+
},
158164
{
159165
"path": "HexBerlekamp/FactorTacticTests.lean",
160166
"baseline_blob": "4063e15934a89c671ac72d201fa60c2ef6feaf59",

0 commit comments

Comments
 (0)