feat(interval): certify bounded raster graphs - #9235

Closed

kim-em wants to merge 112 commits into

agent/interval-adaptive-policyfrom

agent/interval-verified-raster

Commits on Aug 11, 2026

interval: unify semantic and emitter packages
Kim Morrison
committed
fc283e1
interval: seal joint proof registry
Kim Morrison
committed
f1710c0
interval: extract generic proof frontend
Kim Morrison
committed
624643c
interval: validate frontend with exponential package
Kim Morrison
committed
6dcdd69
interval: generalize proof frontend handles
Kim Morrison
committed
640dd64
Merge generic frontend repairs into exp vertical
Kim Morrison
committed
cc9279d
interval: derive checker input from goals
Kim Morrison
committed
6742ec9
interval: repair shared function frontends
Kim Morrison
committed
19fa89a
Merge remote-tracking branch 'origin/agent/interval-exp-vertical' into agent/interval-goal-frontend
Kim Morrison
committed
32ff83b
interval: preserve goal frontend applicability
Kim Morrison
committed
6a969d6
interval: compose operation semantics from packages
Kim Morrison
committed
6c4e209
interval: make hypothesis reification optional
Kim Morrison
committed
cfcd7e1
Merge remote-tracking branch 'origin/agent/interval-goal-frontend' into agent/interval-operation-semantics
Kim Morrison
committed
e9dfb7a
interval: reconcile operation semantics frontend
Kim Morrison
committed
c49c6ce
interval: state operation-model nonvacuity gate
Kim Morrison
committed
b20370a
interval: prove meanings of reified goals
Kim Morrison
committed
3958da8
interval: run search on reified goals
Kim Morrison
committed
5ddeb9e
interval: drive policy runs to target
Kim Morrison
committed
c4558b2
interval: exempt target runner registration
Kim Morrison
committed
0ba9802
interval: close stronger target facts
Kim Morrison
committed
4c8d0bf
interval: state target closure coverage exactly
Kim Morrison
committed
a22cc59
interval: join checked solver splits
Kim Morrison
committed
65667df
interval: extract RealPaver design lessons
Kim Morrison
committed
b89c97d
interval: seed proof branches safely
Kim Morrison
committed
ea3fac1
interval: bind branch seeds to child input
Kim Morrison
committed
7699a16
interval: record branch seed frontier
Kim Morrison
committed
05b436d
interval: seed proofs for branch replay
Kim Morrison
committed
cee8561
Merge remote-tracking branch 'origin/agent/interval-branch-seed' into agent/interval-branch-frontend-v2
Kim Morrison
committed
a424e26
interval: expose the seeded replay fold
Kim Morrison
committed
e042aa6
interval: name the authenticated seeded fold
Kim Morrison
committed
04b951a
interval: replay a live split through exp
Kim Morrison
committed
912bdcc
Merge remote-tracking branch 'origin/agent/interval-branch-frontend-v2' into agent/interval-live-branch
Kim Morrison
committed
895d949
Clarify live split acceptance coverage
Kim Morrison
committed
0dacde3
Prepare exact child sessions from split plans
Kim Morrison
committed
1cec855
Merge remote-tracking branch 'origin/agent/interval-live-branch' into agent/interval-branch-runtime
Kim Morrison
committed
81b5453
Exempt branch-start registration from factor sweep
Kim Morrison
committed
98b07af
interval: authenticate branch starts
Kim Morrison
committed
be15a9b
Add proof-producing contradiction leaves
Kim Morrison
committed
16bf367
interval: restack refutation proofs
Kim Morrison
committed
ad82f6a
Merge repeated instantiation into proof registry
Kim Morrison
committed
07a8f31
Merge remote-tracking branch 'origin/agent/interval-proof-registry' into agent/interval-proof-registry
Kim Morrison
committed
94a8678
Merge proof registry into generic frontend
Kim Morrison
committed
d59eb1a
Merge generic frontend into exponential vertical
Kim Morrison
committed
b8769d6
Merge exponential vertical into goal frontend
Kim Morrison
committed
1561ef1
Merge goal frontend into operation semantics
Kim Morrison
committed
31039d3
Fix operation-semantics progress formatting
Kim Morrison
committed
fab4431
Emit proof-refuted branch leaves

Kim Morrison
authored and
kim-em
committed
a65ad95
interval: restack refuted branch frontend
kim-em
committed
4b72b8a
Merge trust repair into proof registry; progress 20260811T163611Z
Kim Morrison
committed
47d74a1
Merge trust repair into generic frontend; progress 20260811T163700Z
Kim Morrison
committed
1d0280d
Merge trust repair into exponential vertical; progress 20260811T163751Z
Kim Morrison
committed
eb02210
Merge trust repair into goal frontend; progress 20260811T163851Z
Kim Morrison
committed
67c6180
Merge trust repair into operation semantics; progress 20260811T163944Z
Kim Morrison
committed
cf62179
Merge operation semantics into goal closure; progress 20260811T164210Z
Kim Morrison
committed
68734cc
Merge goal closure into dynamic execution; progress 20260811T164326Z
Kim Morrison
committed
961f396
Merge dynamic goals into policy runner; progress 20260811T164450Z
Kim Morrison
committed
48c58c1
Merge policy runner into target closure; progress 20260811T164557Z
Kim Morrison
committed
ed80ec9
Merge target closure into split proof boundary; progress 20260811T164716Z
Kim Morrison
committed
d5b70c9
Merge split boundary into branch seeds; progress 20260811T165035Z
Kim Morrison
committed
18b8621
Merge branch seeds into branch frontend; progress 20260811T165206Z
Kim Morrison
committed
d3ae823
Merge branch frontend into live split; progress 20260811T165305Z
Kim Morrison
committed
f7a394d
Merge live split into branch runtime; progress 20260811T165424Z
Kim Morrison
committed
781be88
Merge branch runtime into refutation proof; progress 20260811T165549Z
Kim Morrison
committed
2eef71c
Merge refutation proof into refutation frontend; progress 20260811T165719Z
kim-em
committed
9e8ff8b
Guard goal-closure tactic axioms
Kim Morrison
committed
bb24bb4
Propagate modeled-goal axiom guards; progress 20260811T165931Z
Kim Morrison
committed
d05ea1d
Propagate modeled-goal axiom guards through policy; progress 20260811T170026Z
Kim Morrison
committed
78b1b79
Propagate modeled-goal axiom guards through closure; progress 20260811T170057Z
Kim Morrison
committed
2bbe594
Propagate modeled-goal axiom guards through split; progress 20260811T170132Z
Kim Morrison
committed
2b33959
Propagate modeled-goal axiom guards through branch seeds; progress 20260811T170207Z
Kim Morrison
committed
835dc7a
Propagate modeled-goal axiom guards through branch frontend; progress 20260811T170233Z
Kim Morrison
committed
0831421
Propagate modeled-goal axiom guards through live split; progress 20260811T170324Z
Kim Morrison
committed
1d60a8c
Propagate modeled-goal axiom guards through branch runtime; progress 20260811T170358Z
Kim Morrison
committed
fab9200
Propagate modeled-goal axiom guards through refutation; progress 20260811T170431Z
Kim Morrison
committed
c3caabb
Propagate modeled-goal axiom guards through refutation frontend; progress 20260811T170502Z
kim-em
committed
6330f60
interval: prove ReLU through split branches

Kim Morrison
authored and
kim-em
committed
ab7a70d
Document branch-dependent ReLU evidence

Kim Morrison
authored and
kim-em
committed
ac23267
interval: reconcile ReLU branch stack
kim-em
committed
21d4270
Propagate provenance honesty through proof registry; progress 20260811T171522Z
kim-em
committed
ea3694b
Propagate provenance honesty through generic frontend; progress 20260811T171522Z
kim-em
committed
d6e3523
Propagate provenance honesty through exponential vertical; progress 20260811T171522Z
kim-em
committed
d684a5f
Propagate provenance honesty through goal frontend; progress 20260811T171522Z
kim-em
committed
e9e52f1
Propagate provenance honesty through operation semantics; progress 20260811T171522Z
kim-em
committed
9612469
Propagate provenance honesty through goal closure; progress 20260811T171522Z
kim-em
committed
32b169b
Propagate provenance honesty through dynamic goal; progress 20260811T171522Z
kim-em
committed
e2e0cf1
Propagate provenance honesty through policy run; progress 20260811T171522Z
kim-em
committed
d860291
Propagate provenance honesty through target closure; progress 20260811T171522Z
kim-em
committed
5032a61
Propagate provenance honesty through split design; progress 20260811T171522Z
kim-em
committed
d8f08cd
Propagate provenance honesty through branch seeds; progress 20260811T171522Z
kim-em
committed
314f804
Propagate provenance honesty through branch frontend; progress 20260811T171522Z
kim-em
committed
25439bc
Propagate provenance honesty through live split; progress 20260811T171522Z
kim-em
committed
5e54484
Propagate provenance honesty through branch runtime; progress 20260811T171522Z
kim-em
committed
4f567ac
Propagate provenance honesty through refutation; progress 20260811T171522Z
kim-em
committed
298e724
Propagate provenance honesty through refutation frontend; progress 20260811T171522Z
kim-em
committed
c3023fb
Propagate provenance honesty through ReLU branch; progress 20260811T171522Z
kim-em
committed
72197a3
docs(interval): state ReLU evidence precisely; progress 20260811T165120Z
kim-em
committed
a58d042
feat(interval): retain bounded branch trees

kim-em
authored and
Kim Morrison
committed
feaf830
feat(interval): emit proofs from retained branch trees
kim-em
committed
47bff5d
Tighten branch proof conformance dependencies
kim-em
committed
e20ae06
test(interval): exercise nested branch scheduling
kim-em
committed
b4e0336
feat(interval): prove exact dyadic fact semantics
kim-em
committed
f877a00
feat(interval): replay an arbitrary centered function
kim-em
committed
ce7765b
chore(interval): exempt centered proof registration
kim-em
committed
e212d51
feat(interval): replay a backward function contractor
kim-em
committed
d454f10
fix(interval): bind splits to post-run snapshots
kim-em
committed
5c8b2e2
feat(interval): add a staged search policy
kim-em
committed
c3f8ab7
feat(interval): replay exact subtraction arithmetic
kim-em
committed
c0f0426
feat(interval): add exact branch proof canary
kim-em
committed
dbcd13e
Add adaptive interval policy; progress 20260811T192156Z
kim-em
committed
6733b71
Restack adaptive interval policy; progress 20260811T193116Z
kim-em
committed
dae46a7
fix(interval): make adaptive feedback reachable
kim-em
committed
1d73855
feat(interval): certify a bounded raster graph

kim-em
authored and
Kim Morrison
committed
48defd6