docs(planner): specify certified guided search - #434
Conversation
Define one exact planner whose oracle and guided modes differ only in admissible search strategy. Specify phased commitment workloads, proof-carrying pruning, performance budgets, diagnostics, and a staged migration plan.
PR SummaryLow Risk Overview Replaces the main/precommit group model with epochs, source contracts, and an explicit closing group. Pins Aerie Falcon v1 as two epochs and one eight-group opening batch ( Normative pruning proofs cover the exact Z/E/T body, discrete convex split intervals, incumbent intervals, relaxed suffix bounds, transition dominance, and group symmetry. Current L2-from-Linf-split and local setup-first slice shortcuts are called out as unproved and deferred to later slices. Registers the spec in the live set (15 records) and scans supporting files Reviewed by Cursor Bugbot for commit d7261d9. Bugbot is set up for automated code reviews on this repo. Configure here. |
Documentation blast radius (advisory)These regions may need doc/spec/book updates based on changed paths. Changed files in this PR: 6
|
PCS Profile Benchmark
13 of 13 profiles passed. Times are medians of Each sample verifies the same proof first with the configured multi-threaded pool and then with one thread. Both timings reuse the same verifier setup. Merge-base comparisons are available for Benchmark shards
Public opening statements
One-hot profiles generate deterministic witnesses with one Direct evaluates the public setup contribution during Stage 2. Recursive carries the same check through a Stage 3 setup-product sumcheck. Both modes execute the complete fold schedule and terminal verification. The chunked profiles Generated profiles may select different A, B, and D ring dimensions at different fold levels. The short profile names omit those dimensions. Each sample generates deterministic witnesses and opening points, prepares setup, commits, proves, serializes the proof, checks its size, prepares verifier setup, and verifies the claimed openings. It does not test malformed proofs. Phase time
Proof size and protocol shape
Grinding retries are rejected attempts at each fold, listed in measured-run order. Zero means the first sampled nonce was accepted. Memory and setup size
Deltas are shown only for profiles with a matching merge-base case. Negative is smaller or faster. The uploaded |
Derive the exact recursive witness body, the incumbent split interval, relaxed suffix admissibility, transition dominance, and group symmetry. Define complete future contracts for selective L2 routes and setup-first slice choices.
CI test timing
Run summary
Wall time spans 2 parallel nextest slice shards. Slowest tests
Regressions vs mainNo per-test regressions above the threshold. New slow testsNo new tests ≥30s vs main baseline. |
Summary
This draft PR specifies one exact offline planner with a fast guided normal
path and a diagnostic oracle path.
rules, complete objective, frontier rules, descriptor order, and validator.
search. It does not start an exhaustive fallback planner.
The design is split into one lifecycle specification and two normative support
files:
specs/certified-planner-architecture.mdowns the architecture, acceptance criteria, migration plan, and performance
contract.
specs/certified-planner/pruning-proofs.mdowns the mathematical pruning arguments and checker obligations.
specs/certified-planner/aerie-workload.mdowns the exact Aerie Falcon version 1 planner fixture.
The support files inherit the root specification's status and retirement.
They do not count as separate live specifications.
Diff metadata
6918a2018da6061d6399c74b542017027a7b74b8(main)d7261d9167667ce71a38152a2f5d7d3867cdb621Motivation
The current planner still mixes the semantic search domain with traversal
shortcuts. Three gaps are central.
BoundedBalancedExtremesV1omits recursive splits outside a fixed radiuswithout a complete objective proof.
candidate.
successor witness and suffix.
The current exact suffix frontier is useful after candidates have been built,
but it does not prove that these earlier omissions are safe. The target
architecture keeps one complete audited domain and requires a checked theorem
for every omission.
The existing grouped commitment API also exposes a compiled Akita shape as if
it were the protocol model. Protocols such as Aerie need semantic objects,
challenge separated commitment epochs, and a shared opening batch to be
planned together before they can be lowered to frozen profiles plus one final
group.
Planner architecture
The oracle is a diagnostic execution setting. It enumerates every audited
decision that has not been removed by mandatory equivalences or independently
audited certificates. The guided setting is the normal catalog generation
path. It uses empirical results for search order and validated incumbents, but
it has no additional semantic authority.
Certified pruning results
The proof support file states five concrete results.
The canonical witness layout gives the exact mandatory current group body
[
F(p)=a\left\lceil\frac{N}{2^p}\right\rceil+b2^p
]
inside every cell where security ranks, digit depths, relation geometry,
source encoding, and compression choices are fixed.
The body is discrete convex inside a cell. Every strict contraction or
strict incumbent sublevel is therefore one integer interval.
A completed incumbent gives a closed interval around the analytic balance
point. When the incumbent is close to the lower minimum, only a few integer
splits can still win. This replaces a fixed split radius with a proved
range.
A relaxed suffix search is admissible when it includes every real
transition, charges no more than the real transition, and combines costs
monotonically. Induction over the remaining fold depth proves that its
value is no greater than the true suffix optimum.
A transition may dominate another only when it admits every consumer, has
the same sufficient child state or a proved child mapping, is no worse on
every parent visible projection, and handles descriptor ties.
The support file also proves the interchangeable group symmetry quotient and
defines stable certificate names, conservative unknown behavior, diagnostics,
and oracle comparison tests.
Selective L2 routes and setup first slices remain explicit later
implementation work. The target keeps every route and slice until a complete
transition dominance certificate removes it. A lower A rank, local setup
winner, or smaller next witness is not enough by itself.
Aerie Falcon version 1 workload
The workload support file is pinned to Aerie commit
e102ee371d08770b6fdfcebc33abe169e60e2756, merged PR #52, and the executablemanifest, transcript state machine, and PCS integration at that commit.
The adopted commitment sequence is:
S1,Epsilon,S2SourcesFour,BudgetTwo, andBudgetOnein manifest order.S1 | V | Epsilon.JlTwoandJlOne, which may be computed in parallel, and absorbthem in that order.
JlFouras the Akita final group with the first sevenprofiles frozen.
one complete point owned by each group.
The JL names describe contents, not position.
JlTwopacksD4,D5,JlOnepacks
D6, andJlFourpacksD0throughD3.JlFouris the closing groupbecause the JL4-final lowering produced the better measured recursive ladder.
It is not Aerie's semantic main witness and its bound 6 extraction family does
not own the opening policy.
For padded batches with
N* >= 8, the logical commitment total is2679 N*.For smaller padded batches, the exact total is
2567 N* + 896 N* / min(8, N*). The fixture also records the physicalpower-of-two shape, the
2^13PCS floor, and the zero extension opening rule.Aerie source reconciliation
Some inventory and transcript prose in the pinned Aerie protocol document
still prints the older
JlFour,JlTwo,JlOneorder. The manifest,transcript state machine, composition, PCS implementation, and merged PR #52
all enforce
JlTwo,JlOne,JlFour. This fixture follows that adoptedexecutable order and records the discrepancy instead of treating both orders
as supported.
Open Aerie PR #53 adds adversarial coverage for this order, the digit
alphabets, shard lengths, and minimum batch zero extension. Open PR #54 adds
timing spans without changing the protocol layout.
Performance contract
The proposed routine path is guided catalog generation. The initial
implementation targets are:
fixture when the oracle completes within the audit window.
The absolute limits become blocking when the repository names a reference
runner. Until then, the same host relative limit is the blocking comparison.
Neither target may be met by shrinking the audited decision domain.
Change surface
specs/certified-planner-architecture.mdspecs/certified-planner/pruning-proofs.mdspecs/certified-planner/aerie-workload.mdspecs/PRUNING.mdbook/src/foundations/spec-index.mdscripts/check-spec-references.shSafety and compatibility
This PR changes documentation and a documentation check file only. It does not
change planner code, generated schedules, public APIs, wire formats,
transcripts, setup artifacts, or runtime behavior.
The target contract requires canonical shared security and witness sizing
functions, checked arithmetic, conservative unknown behavior, strict numeric
pruning before descriptor comparison, and expansion through
akita-schedules. Runtime proving and verification cannot depend onakita-planner.Akita makes no backward compatibility guarantee. The implementation plan uses
one direct cutover and permits one policy-free lowering adapter while runtime
catalog shapes migrate.
Commit map
66b5790c2specifies certified guided search and phased commitmentworkloads.
137f9cd08links draft PR docs(planner): specify certified guided search #434 from the specification header.53538b91dadds the formal pruning proofs and the complete L2 and slicemigration contracts.
d7261d916splits the document and updates Aerie to the adopted JL4-finalprotocol.
Validation completed at
d7261d916git diff --checkscripts/generate-schedule-tables.sh, all 13 families with no generateddrift
cargo fmt --all --checktaplo fmt --checkscripts/check-spec-references.shscripts/check-spec-references.sh --all./scripts/check-doc-guardrails.sh, includingmdbook buildtyposover every changed filepython3 -m unittest discover -s scripts/tests -p "test_*.py"with 75 testsakita-verifier,akita-prover,akita-config,akita-planner, andakita-setupcargo machete --with-metadataThe earlier 20,000 case randomized audit of split convexity and incumbent
interval containment remains applicable. A direct before and after comparison
confirmed that the split moved every proof statement and obligation intact.
Specification status and remaining work
This PR completes the proposed architecture and proof contract. It does not
implement the planner migration.
The 12 implementation slices cover the domain census, canonical decisions,
shared oracle, exact split cells, relaxed suffix bounds, selective L2 route
frontier, setup first slice frontier, guide artifacts, workload planning,
Aerie integration, runtime catalog cutover, and performance gates.
Reviewer map
Suggested review order:
semantic contract.
specs/certified-planner/pruning-proofs.mdfor the mathematicalauthority behind each exclusion.
completeness sections for the deferred gaps.
specs/certified-planner/aerie-workload.mdfor the exact challengeboundary, manifest order, logical and physical geometry, and Akita lowering.
plan for acceptance and migration.