Repository navigation
Solver portfolio: review stages A–F, scaling study, solver Phases 0–5 and follow-ups - #59
Merged
Merged
Conversation
…econdary plan The external architecture review of 2026-09-28, its claim-by-claim verification with reproducible probes, and the secondary plan (Stages A, E1, B, C, D, E2, F) revised after the 2026-09-30 readiness check, with the seven decisions made as recommended. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…he explanations, across feasibility_limit §3.14 says each deletion trial is bounded by feasibility_limit and by what remains of explanation_limit, and which keyword an unresolved explanation's limit names. The feasibility_limit and explanation_limit keyword docs say the same. A test runs the probe 08a space at the default limit and at 6, 10 and 14, and checks each explanation's rules by brute force. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…n_sizes run several §3.5 and §12.19 name the calls that are one operation (a generation, and explain, classify, coverage, missing_interactions and followups) and say that report and design_sizes run several, each with its own memo. The constraints page and the _LazyRule docstring say the same. A test counts a whole-case predicate's calls in one coverage call: each assignment at most once. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…st is recorded at generation The Report field doc lists which parts of the guarantee line come from generation: the must-include rows, an excursion's distance, base, dropped rows and never-appearing values, a full factorial's "every valid row", and GND's seed. The report docstring, the tutorial, the coverage evidence page and the header of report.jl no longer say the whole line is measured. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
§8.6 and the diagnose docstring say that a case that breaks a rule, or holds more than one Invalid value, is ranked like any other, and that a failing case that broke the rules can leave a suspect no valid case holds, which followups reports as inseparable with no other suspects. The two tests that already cover this now cite §8.6. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
§12.16 says a tabulated rule's exception surfaces when the space is built, and a lazy rule's, including every whole-case rule's, from whichever call evaluated it. The constraints page gives the lazy case beside the tabulated one. The ConstraintError test reaches a throwing whole-case rule through explain and through coverage. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
n_way_coverage has no benchmark callers; classify's docstring no longer says coverage measurement uses it; the feasibility.jl header calls classify unexported and no longer calls isallowed a wrapper over this file; choose_last_parameter!'s docstring gives its real signature; a test comment that holds for one problem says so. The local predicate in cover_ordinary(::IPOG, ...) is renamed from alive to isdead, the name of the _Greedy field that holds the same predicate. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…e macros reject One paragraph at the end of "What the macros treat as a name" lists the forms the macros reject, as the @forbid docstring and §12.6 do, and points to forbid(f, names...) and require(f, names...). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…nation_limit §3.14 and the explanation_limit keyword doc say explanation_limit when that budget stopped a trial or left one untried, which is the rule _deletion_search applies, rather than "when it ran out", which misreads a budget spent to exactly zero by a trial that finished. The constraints page gives its list of calls that can surface a lazy rule's exception as examples. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Records the adjustments made to Stage A's steps and why, and how the full suite's pass count compares with the base commit. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…hem when they differ An inseparable suspect's Followup gains `proofs`, one FollowupProof per kind searched, in the order of `searched`: its rules, labels, other suspects, minimal and limit. The union fields keep their values. `show` prints the union's line when there is one proof or every proof equals the union, and otherwise one clause per kind, so it never presents a union as minimal. The docstrings of `followups`, `Followup` and FollowupProof say that minimality is judged per kind and state the rule for the union's `minimal`. check_followups checks each proof by brute force within its kind, and how the union fields combine the proofs. New items cover probe 04 Examples A, B, B reversed and D, each branch of the union's `minimal`, a kind left unresolved, and empty proofs for :found, :unknown and two Invalid values. The Example C line is rewritten to the per-kind form. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…d of case §3.17 says an inseparable follow-up gives one proof per kind of row searched, each judged minimal within its kind, and that their union is sufficient but need not be minimal. The how-to adds probe 04 Example A: a space with one Invalid value where the kinds need different rules, showing the per-kind line and `proofs`. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…ests or nothing call No production code reaches any of them (design/components_review_verification.md section 5; checked again by grep). Deleted, with their docstrings: combination_number and pairs_in_entry (combinations.jl); all_combinations_matrix, parameter_cnt and the unused local that called it in matches_from_missing, combination_histogram, most_to_cover, most_common_value, first_match_for_parameter, fill_consistent_matches, remove_combinations! and multi_way_coverage (coverage_matrix.jl); fill_missing_test_set_values! and cover_remaining_by_creating_cases (parameter_order.jl); n_way_coverage and the one-argument _Greedy(mc) (greedy_tuples.jl). Tests removed with them: the combination_number item, the first_match_for_parameter, fill_consistent_matches, remove_combinations and multi_way_coverage items, the n_way_coverage item, and the n_way_coverage lines of "GND design size is competitive", which keeps its generate(GND) checks and drops the `using Random` and the IndexCoverage setup it no longer uses. multi_way_coverage's wayness checks (§11.6, §11.7, §11.9) are enforced and tested in Request (test_request.jl); n_way_coverage matched generate(GND) on unconstrained requests (probe 05c), which the GND items test. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…method covers (request.jl) lost its last caller in 234fe9d. full_factorial_rows and its FullFactorialRows iterator, with three Base methods, were called only by test_full_factorial.jl; the public full_factorial tests keep checking the 0.4 order. The never_appear method taking an arity vector had no caller: generate_excursion passes the domain positions. Its docstring now describes the one remaining method. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…llers use No caller varied the matcher; the parameters were left from the matcher experiments that docs/src/man/ipog.md describes. choose_last_parameter! and insert_tuple_into_tests lose theirs and call case_partial_cover (through matches_from_missing) and case_compatible_with_tuple, their defaults. matches_from_missing calls case_partial_cover, which both production callers passed (choose_last_parameter! by its default, choose_last_parameter_filter! explicitly), not its declared default, case_compatible_with_tuple; its one test expects [2, 2] under either. Its docstring now says what it counts instead of "Return a new version of the entry", and insert_tuple_into_tests no longer holds the verdict in a local named `matches`, which shadowed the function of that name. Designs are unchanged: the rows of classic ipog on 60 random arities and strengths, and of covering, all_pairs and all_triples on four spaces with both engines, are identical to the Stage E1 head. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
None has a caller in src/, so a reference sweep lists each of them. A comment beside each says why it stays: misses is one of the five tuple states that a test checks are mutually exclusive; memo_size is instrumentation that benchmark/run.jl reports; plain is for users, as the Report docstring says; targets and components are conveniences for the tests. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
A rename only; the next commit makes it run from there. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…ard output The repository root comes from @__DIR__ instead of a hard-coded path, and the sweep skips its own file. It writes no files: with no argument it prints the names no public entry point reaches, as the probe did; with one of names, refs, shadowed, locals or callgraph it prints that table, tab-separated, with a header. The header comment says how to run it and why it is a list for a person to judge and not a gate. The analysis is unchanged: on the Stage E1 tree the list and all five tables equal the probe's output. The verification report's probe list says where it went. After this stage's deletions, the list holds the unexported classify path (Stage C), plain and its helpers, and the helpers whose definitions say why they stay. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…ents test/checker.jl is included into the same test module as fixture_model.jl, which imports the package, so the oracle's independence was a convention only. The new item parses checker.jl, which drops its comments, and fails if any name, string or docstring left mentions UnitTestDesign. Today the only mentions are in the header comment. Four assertions check the check: comments pass, and a `using`, a qualified call and a docstring fail. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…w-up results benchmark/snapshot.jl prints a fixed corpus as text, one line per field with repr and each result's show text, so that a stage whose invariant is about figures, rows and order can be checked by diffing its output at the stage's base and head. It uses only the public API and the documented fields, and runs unchanged at older commits: at 4d9d424 its output differs from this commit's only in Stage E1's proofs and inseparable lines. The corpus: covering at strengths 1 to 3 with IPOG and GND, excursions and full_factorial on twelve fixed spaces and twelve seeded random ones (lazy, tabulated and whole-case rules, partitions, Invalid values, stronger groups with an invalid parameter, ordinary and negative must-include rows), and positional calls; coverage, missing_interactions, report and design_sizes on the results and on hand-written rows with repeats, rejected rows and two Invalid values, as named tuples, tuples and vectors; diagnose and followups on the probe 04 spaces, on seeded outcomes over the test_diagnose sweep's spaces, and on generated results. Each at the default limits and at tight feasibility and explanation limits. About 80 seconds and 25 MB; two runs print the same bytes. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…lection by _row_list
One reader in space.jl, beside case_indices, takes a NamedTuple, a Tuple or
a vector and owns the four input errors: not a row, the wrong length, an
unknown name or value (case_indices's message after the row's name), and,
when the caller needs a complete row, a missing value. Each message starts
with what the caller calls the row and ends with the contract section it
cites. It replaces _coverage_row, _diagnosis_row, the row branch of
_must_include_matrix, the shape checks of _from_row with the reading half of
excursion_base, and the case_indices calls of isallowed, explain and
_classify_one. Each caller keeps its own policy: coverage and diagnose
rows are complete; the base is ordinary; a positional call takes no
NamedTuple; a vector `from` is values, never engine positions; classify
takes NamedTuple targets.
One collection reader, _row_list, replaces _coverage_rows and the
collection branches of _diagnosis_input and _must_include_rows, with their
wording. coverage keeps its space-first check.
Messages that change, and the pins rewritten for them:
- `from`: "`from` has 2 values; the space has 3 parameters, p1, p2, p3, and
the base is a complete row (contract §7.6)" becomes "the excursion base
`from` has 2 values; the space has 3 parameters (p1, p2, p3) (contract
§7.6)"; "`from` is the base row: a complete NamedTuple, or a tuple of
values in parameter order; got a Dict{Symbol, Int64} (contract §7.6)"
becomes "the excursion base `from` is a Dict{Symbol, Int64}; a row is a
NamedTuple, or a tuple or vector with one value per parameter (contract
§7.6)"; "the excursion base `from` must be a complete row (contract
§7.6); it has no value for b, c" becomes "the excursion base `from`,
(a = 1,), has no value for `b` and `c`; it must name every parameter
(contract §7.6)". test_interface.jl (four pins) and test_excursions.jl.
- isallowed: "isallowed takes a complete case, but (n = 1, m = :a) has no
value for k. Use explain for a partial assignment (contract §1.25)."
becomes "the case, (n = 1, m = :a), has no value for `k`; it must name
every parameter (contract §1.25)". test_explain.jl.
- diagnose: "wrap a single case in a vector" becomes "wrap a single row in
a vector". test_diagnose.jl.
New items: the reader's shapes and four errors, and the collection
reader's (test_space.jl); every caller's errors in the same words
(test_interface.jl). The before/after snapshot is byte-identical.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
… of its values Decision 5. Both now take any row and read it with _row_indices, so a vector is read as a tuple in parameter order, as coverage, diagnose and must_include already read one, and anything that is not a row is the reader's ArgumentError instead of a MethodError. The docstrings say a vector is accepted. A new item checks, over every row of a space with partitions, Invalid values and a whole-case rule, tabulated and lazy, that a vector gives the tuple's answer from isallowed and the tuple's Explanation, field by field, also with partitions written by name; that a malformed vector is refused in the tuple's words; and that a vector of integers is values, not positions. The cross-caller item adds isallowed and explain. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
… would change a figure Decision 7 keeps one answer cache per measurement because a search that finds one component's witness cached has budget left for the next, so it can resolve a target that a fresh search leaves unknown. Probe 03b found no such case among its random spaces, and neither did this corpus: with _measure patched to reuse the previous measurement's context, answer cache included, the snapshot did not change. Two spaces of two independent components, each a few nodes deep, now make it change: with that patch, report's bonus at feasibility_limit = 4 counts 14 unresolved triples instead of 10, and missing_interactions after coverage and report resolves what it otherwise throws for, 28 lines in all. The extended corpus at the Stage B head and at the step 1 head prints the same bytes, as do two runs at the Stage B head. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…ssification _classify_target (Excluded) and _classify! (Exclusion) no longer test explain_partial's outcomes inline; like _classify_one (Classification), they read the status from IndexClassification, whose _STATUS_OF_OUTCOME is the one mapping from a search outcome to a status. _classify! returns that status, and _measure_block! counts by it. The classify docstring says the three share it. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…zy-rule memo _read_rows becomes _prepare_rows(space, memos, rows), returning a PreparedRows: the kept rows, duplicates, rejected rows and slots, which depend on no strength, group or limit, since preparing runs only the direct check. _measure(prepared, space; ..., memos, curves) builds its own FeasibilityContext around the memo it is given, through the new FeasibilityContext(space, memos; feasibility_limit), so each measurement keeps its own answer caches (decision 7); curves = false skips the prefix curves, which only report's base measurement reads. report prepares once and passes one memo to its base and bonus measurements. design_sizes keeps one memo for all its measurements and prepares each design once for its two strengths, measured at the strength and groups coverage(cases; strength = s) uses (_measured_request); its generations keep their own memos. Tests: probe 03b as a property test (every report figure, base and bonus, equals that of a separate coverage call, tabulated and lazy, down to feasibility_limit = 1, including a space of two components where a shared answer cache would change the bonus; design_sizes likewise), and probe 03a (report evaluates a whole-case predicate at most once per assignment; design_sizes' measurements at most once per assignment beyond its generations). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…search state _completable built a _Search, one candidate vector per parameter, for every query it did not answer from the memo, even when every constrained component was assigned or cached and nothing was searched. It now builds one only when a component is pending. Nothing else changes: such a query spent no nodes before and spends none now, and the caches and counters are written as before. Counting, in the next commit, is the reason: on the 30 by 5 all_pairs design, whose bonus asks 287,305 such queries, the search state was 2 KB of the 2.4 KB each query allocated, so a counts-only bonus could not allocate much less than one that lists every target. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Both recounts passed over an excluded code even when a row held it. Every row has been checked valid before the recount, and no valid row holds an excluded target (contract §1.4), so such a row means classification was wrong (review p5-core 5). The recounts now name it, for one bit read per excluded target: the gate shapes' recounts take the same time within 1% (gcc200 0.975 -> 0.980 ms, t6 66.6 ms both). Tests: a snippet writes the layout recount's verdict out from lists (the first target in target order that is required and held by no row, or excluded and held by one); the layout recount item and the random recount item compare with it, and with the list recount wherever no row holds an excluded target. The random item now draws overlapping stronger groups and must-include rows (review p5-evidence 6). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01URSWftXy2VPwQBGhbZQV8D
No test gave the negative recount on the layout a design that fails, so a recount that checked nothing passed every test (review p5-evidence 1). On 150 random spaces with Invalid values, each IPOG design's negative rows, with each row dropped and ordinary values changed, get the verdict written out from lists and, where no row holds an excluded target, the list recount's message; at least 800 of them must fail. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01URSWftXy2VPwQBGhbZQV8D
TargetList: GND and full strength decode the required targets during a call; only classification and the certifier keep no list (review p5-integration 4). IndexExplanation and IndexClassification: no witness when asked with witness = false (p5-integration 5). Feasibility: a component that scoped rules link through every parameter has full-width keys too; a search grows the object's buffers until they reach their size (p5-perf 5). _compact: the targets are generation's RequiredTargets, not a list's (p5-integration 8). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01URSWftXy2VPwQBGhbZQV8D
…ree parameters from a template A cached question looped over every component, filling each free singleton's parameter, so its cost grew with the width (review p5-perf 1). The object now keeps its constrained components' list and a template of the free parameters' first candidates (empty when none is free), and a question merges the assignment into the template without a branch per parameter (half-assigned rows mispredict one) before it looks up the constrained components. Answers, witnesses, nodes, memo_hits, evaluations and cache entries are unchanged (the equivalence test with 31bef0f's code). Measured against the tree before it, minimum of two alternating rounds, load about 4 (provisional): classification of 1,024 binary parameters with a scoped rule 9.11 -> 1.95 s, gcc200 0.072 -> 0.042 s, t6 0.40 -> 0.31 s; a cached question on gcc400 4.6 -> 2.2 us; where every component is constrained (pairs, the ladders) within +1.5% to +4.8%. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01URSWftXy2VPwQBGhbZQV8D
…s rule checks, and what the classification test shares A CI bound on Base.summarysize of a request and its classification at probe 06's n = 128, under 1 MiB (0.18 MB now, 106 MB at 31bef0f; review p5-evidence 7). classify of a target listed twice pins p5-memo's J1: the repeat makes its direct check twice, (:required, 0, 2) where 31bef0f reported (:required, 0, 1) (review p5-evidence 10, p5-integration 3). The classification test's comments say what its list path shares with the production walk and where the shared parts are tested independently (review p5-evidence 8). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01URSWftXy2VPwQBGhbZQV8D
…ucture Each trial built a whole Feasibility, copying and checking the candidates and allocating a table list per parameter and per component, and on gcc400 and CASA at strength 3 explaining implied exclusions was most of classification (review p5-perf 3). A trial is now built by _Feasibility from its parent's validated parts: the same candidates, a subset of the tables and memos, nothing checked again, and the parent's vector for a parameter alone in its component in both. Every Feasibility shares one empty table list among the parameters and components without a table. A trial is still the search Feasibility would build over its rules (tested), so every explanation's rules, minimal, limit, nodes and rule checks are unchanged: classification's question streams hash equal on gcc400, triples-n90 at strength 3 and CASA benchmark_16 at strength 3. Classification, minimum of two alternating rounds (load about 4, provisional): gcc400 5.01 -> 2.35 s (22.2 -> 10.3 GB allocated), triples-n90 at strength 3 3.55 -> 2.85 s, CASA benchmark_16 at strength 3 54.1 -> 27.4 s (230 -> 112 GB, peak 1,545 -> 1,427 MiB); one gcc400 trial 157 -> 75 KB. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01URSWftXy2VPwQBGhbZQV8D
…hunks Review p5-perf 6 found the recount slower on 8 parameters of 64 values (0.37 -> 0.45 ms through validate_design, reproduced) and named the clear of the marks. That clear is chunk-wise already (Base's fill! of a contiguous BitVector view uses fill_chunks!), and clearing by chunks by hand measured the same. The time is the walk over a support's 4,096 codes, which the base's streamed recount didn't make. A support (or negative block) with no excluded target now checks that every code is marked with findnext over the chunks, and names the first unmarked one as the walk did. Recount of one IPOG design, minimum of 9 calls, two alternating rounds, load about 4 (provisional): 8 x 64 values 0.381 -> 0.301 ms; gcc200, t6, 512 binary, 1,024 binary with a scoped rule and the negative recount within -3% to +0.7%. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01URSWftXy2VPwQBGhbZQV8D
…emoved The test asserted that the memo column starts with `memo=`, the whole-assignment memo's field, which p5-memo removed: at the merged head it read `witness_cache[]=98 memo_size()=0` and the test failed, 171 passed and 1 failed (review p5-integration 1, p5-evidence 3). It now asserts the column's `name=count` pairs and the component caches' entry. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01URSWftXy2VPwQBGhbZQV8D
…the rows, and no masked nondeterminism The summary judged gates 2-4 and the rows at keys both trees completed, so a branch line that failed (an internal error, nondeterministic, a stop) where the base completed went unnoticed outside the gated points (gcc400, t5, t6 peak, bin1024 index), the same rows with other counts passed, and a resumed file's later ok line hid an earlier nondeterministic one (review p5-evidence 2). A completion check now fails every key the base completed whose branch line isn't ok, and every branch line that is an error or nondeterministic; the rows check compares required, excluded and bound beside rows and hash; by_key keeps a nondeterministic line over any other. The header says so. The tests add gate_blindspots.jl's scenarios: 181 pass (the old summary code fails 4 of them and errors on 5). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01URSWftXy2VPwQBGhbZQV8D
Since Phase 5 the adapter timed classify_targets (the walk plus a decoded list), a RequiredTargets built from that list, and the list recount, none of which generation runs (review p5-integration 2). It now times _Classified, the engine on classification's targets and the certifier's recount on the layout, as _generate runs them. On 256 binary parameters with a scoped no-op rule: classification 0.031 s and 8.9 MB, validation 1.4 ms and 2.4 KB. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01URSWftXy2VPwQBGhbZQV8D
…trees only `run` left out points whose rules' targets at 24 bytes per parameter per target (plan §2.6) passed --max-memory, a cost Phase 5 removed: it skipped ten CASA strength-3 points that now fit (review p5-integration 6). The default now applies that estimate only to a tree that lists its required targets (before Phase 5, no _required_list), and --max-memory G applies it on any tree, so a comparison across trees can leave out the same points on each. `list` on the Phase 5 tree now runs those ten in process; on 31bef0f, or with --max-memory 1, it skips them as before. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01URSWftXy2VPwQBGhbZQV8D
… memo The worker reports `component_cache`, the entries of the caches by component, and `assignment_memo` is 0 on every Phase 5 tree; the summary kept only the latter (review p5-integration 9). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01URSWftXy2VPwQBGhbZQV8D
The rules bullet compared warm calls now with first calls at the start of the release's work (review p5-evidence 5). It now gives a first call and a warm call on probe 21's 200 and 400 options, against probe 21's first calls; says what classification keeps for a required combination and what IPOG and GND build during a call (p5-evidence 5, p5-integration 7); and says what sets the time at 400 options: explaining the combinations the rules exclude only together, which explanation_limit bounds (review p5-perf 3, 5). The figures are single loaded runs at this branch's head, for the record stage to replace with quiet ones. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01URSWftXy2VPwQBGhbZQV8D
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01URSWftXy2VPwQBGhbZQV8D
…ERS and the release notes The quiet re-measurement (p5_quiet_measurements.md §7) found three cells of the Engines page's cost table more than 25% high, all written before the fix that made a question visit only the constrained components: 250 binary with one rule (0.15 to 0.16 s, now 45 to 60 ms), Auto() on 250 x 4 (6 to 26 ms, now 4 to 18 ms) and 30 x 4 at strength 3 with one rule (73 to 83 ms, now 53 to 55 ms). Nothing else on the page changes. _IPOG_MEMBERS' docstring gives the member-set figures after Phase 5 (slower than the old paths at 29, 7, 0 and 0 of the 777 constrained points for eight, four, two and one members) and four members' peak on the strength-3 model, 1.2 to 1.4 times one member's and below the old paths', in place of "double one strength-3 model's peak memory". The file keeps its line count. The release notes draft's paragraph on constrained models says what Phase 5 did, in the quiet figures, in place of "is meant to reduce this cost". Text only. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01URSWftXy2VPwQBGhbZQV8D
…gets are given The maintainer's review, R3. validate_design skipped the negative recount when classification required no negative target, but since 2f07b70 the recount also checks that no negative row holds a target classification excluded (_held, contract §1.4): a classification that wrongly excluded every negative target let a negative row holding one pass. The recount now runs whenever a _NegativeTargets is given (_recounts); a list from tests and scripts, required targets only, is recounted when non-empty, as before. A new item builds that classification by hand beside a design's negative rows and expects _held's error; at 81f8056 it fails 7 of its 11 assertions. The random negative recount item no longer skips a request with no negative target required (one of its 150, a space with no valid row); its draws and other counts are unchanged. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01URSWftXy2VPwQBGhbZQV8D
The maintainer's review (R1): IPOG's step map knew the layout's storage. _begin_step! assumed a step's base supports come first among its supports, rebuilt them with its own odometer over the parameters before the step's, and called _nbase, _base_strength and _base_with (judgment call 102). The odometer moves into the layout, beside _Supports in request.jl: _each_base_support(supports, p, earlier, buffers) yields (s, support) for each base support that holds p and t - 1 of the ascending set earlier, in increasing position, without unranking. Its position is C(n, t) less the subsets after it, a sum over its places; the common step changes one place and one term. It checks earlier once per walk (ascending in 1:n, without p) and allocates nothing once its buffers (_BaseWalkBuffers, which the caller keeps) have grown. _base_strength and _base_with are gone. _begin_step! reads the step's supports in the order the steps list them, ascending, and takes each one the walk gives from the walk, any other by _support!. It relies on neither base supports coming first nor any order of the layout's: a support the walk gives that the step doesn't list is an internal error. _LookupRun's places becomes walks, the walk's buffers; before and _before! stay, the set IPOG passes. The map, the step order and the rows don't change. Tests: the walk against _support_rank and _support! on every step of random orders and layouts (base strengths 0 to 4, stronger groups, a negative sub-request's shape) and on wide base groups, and exactly the step's base supports at IPOG's order; its input checks; @inferred and zero allocation in test_stability.jl; the map test, retitled, also checks the internal error. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01URSWftXy2VPwQBGhbZQV8D
…through the request's map The maintainer's review, R2. dead(request, partial) wrote the row's value indices into the search's key buffer and called _completable, relying on facts kept in three places (the request's candidates, _feasibility's routing of a negative row, and _candidates) for a key no check had seen. The search now owns that step: _mapped_completable(f, map, positions) takes the request's map from engine positions to value indices, and _mapped_key! writes the key and checks it as _checked_key checks an assignment (length, each position within the map, each value among the candidates). The check reads a table of the map made on the first mapped question (_Mapped, _map!): for each position, its value index if that is a candidate and -1 if not, 0 for unset. One read a parameter without a branch, where the conversion alone branched on an unset entry, which half-assigned rows mispredict. A deletion trial shares its parent's table, since it has the same candidates. Full validation by the decision rule's order: a scan of the candidates (what _checked_key does) cost 4.4-7.0% on review p5-perf's P2 measure against 81f8056; with the table it is x0.48-0.85 (provisional). Request's ResourceLimitError message unchanged; a cached question allocates nothing, for ordinary and negative rows. Every question's answer, nodes, memo_hits, evaluations and cache entries by component are 81f8056's on 13 shapes (classification's questions, hit.jl's rows and negative rows, IPOG). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01URSWftXy2VPwQBGhbZQV8D
…up only the components it assigns Step 2 of the fast path (review p5-perf 1 and 2), which the maintainer took on October 7 (plan §12.3 item 8): p5-fixes' step2_variant.patch, rebased over 4312ae4's split constructor and R2's entry point. `_Unset` records the witness of each constrained component's all-unset sub-assignment as its search stores it; once every component's is cached feasible, a question starts from those witnesses, merged with the assignment without a branch, and looks up only the components that hold an assigned parameter, since each of the others would find its all-unset entry. The same components are searched in the same order, so no answer, witness, node count, memo_hits, evaluations or cache entry changes. Each Feasibility, a deletion trial included, keeps its own record: a trial allocates one or two more vectors of n (2.4-6.5% more bytes). The equivalence test now counts the questions asked on that path (7,311 of 12,000 against 31bef0f's code), and the stability item checks that a hit on it allocates nothing. The docstrings of Feasibility, dead and _completable say what a cached question now costs. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01URSWftXy2VPwQBGhbZQV8D
… layout's walk The Phase 5 follow-ups: feature/solver-p5f-feasibility (the certifier's negative recount whenever negative targets are given, R3; a feasibility-owned entry point for a request's row, R2; step 2 of the fast path) fast-forwarded, and feature/solver-p5f-layout (R1) merged onto it. Both start from 81f8056. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01URSWftXy2VPwQBGhbZQV8D
Reviews p5f-layout 5 and p5f-perf 7 (the layout build's J4): since R1 moved IPOG's base supports onto the layout's walk, only the ranking test called _nbase. It reads the field, as the other tests do. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01URSWftXy2VPwQBGhbZQV8D
…put check Docstrings only. Feasibility and dead(f, partial) now say the same thing about what a cached question costs once every all-unset answer is cached: the pass over the assignment, the direct check, the check of each constrained component for an assigned parameter, and a lookup per component the question partly assigns, since a fully assigned one isn't looked up (reviews p5f-evidence 7, p5f-feasibility 4, p5f-layout 7, p5f-perf 3). The R2 table is kept by its map's identity (reviews p5f-feasibility 1, p5f-perf 4): _mapped_key! says to pass the same map object every time, since another, even an equal one, rebuilds the table and a map changed in place is used stale; Request says that its candidates, the map dead passes, is one object for the request's life and never changes. _each_base_support checks earlier only at t >= 2 (review p5f-layout 2). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01URSWftXy2VPwQBGhbZQV8D
Review p5f-evidence 2: R3 chose to recount whenever classified negative targets are given, partly because, with no negative row, the recount still checks that the excluded numbers and the required count are the layout's. No test pinned that, so the condition "whenever the design has negative rows" passed the suite. Beside the no-negative-row case, one negative target neither required nor excluded, and a required count that isn't the number left, must each raise the recount's error. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01URSWftXy2VPwQBGhbZQV8D
Review p5f-layout 1: a step whose walk gets a stale set reads every base support by position instead, and the map is the same, so a wrong set was a silent slowdown that every test passed (at 81f8056 it raised). The map test now checks, at every step, that the set the step hands the walk is the parameters before p in the order, and that over it the walk gives exactly the step's base supports. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01URSWftXy2VPwQBGhbZQV8D
…iss on step 2's path Review p5f-perf 8. Both guards on _begin_step! measured a step's second call, when _before! has nothing to insert; one whole pass of the steps in order, through a function barrier, now allocates nothing, in the support item and on IPOG's run with rules and rows. The walk's guard covers base strength 3, as its comment said. A miss on step 2's path allocates only the entry it stores. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01URSWftXy2VPwQBGhbZQV8D
…eps none Review p5f-perf 2: since step 2, every Feasibility built its free parameters' first candidates and a copy of them for the record of all-unset answers, deletion trials and negative-row searches included, though a trial asks one question and its record never pays. Classification allocated 3.4% more at gcc200 and 2.9% more at equality-n32, and 301 negative-row searches retained 3.6% more. The record now lives in the template: at a constrained component's parameters the template holds 0 until the component's all-unset answer is cached, then that answer's witness, so the record costs nothing where some parameter is free (n values of its own where none is). Step 1 can then meet those witnesses in a component it must search, so _look_up! resets a component it doesn't find to the question's values, as step 2's path already did before every lookup; that reset moves into the miss. A deletion trial keeps no record (unset is nothing), so step 2 is held off there. Classification bytes at gcc200 and equality-n32 are 81f8056's to the byte, and a negative-row search retains 104 bytes more than at 81f8056 (the empty R2 table and this record's object), where it retained 2,544 more. No answer, witness, node count or counter changes. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01URSWftXy2VPwQBGhbZQV8D
Review p5f-evidence 1: the equivalence test compares every question with 31bef0f's code, whose memo_hits counted its whole-assignment memo's hits, so it never compared memo_hits on step 2's path; dropping that count passed every test. Each question is now also asked of a twin, the same search with step 2 held off as a deletion trial's is (built from its parent by _Feasibility over every rule, so it keeps no record of all-unset answers, since b6c7a65), and the twin's status, witness, every SearchStats counter and caches must equal the object's after each question. The review's mutation (memo_hits not counted on step 2's path) now fails 1,262 of these comparisons and nothing else. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01URSWftXy2VPwQBGhbZQV8D
Comment only: the sentence b6c7a65 added about deletion trials read badly. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01URSWftXy2VPwQBGhbZQV8D
…m the quiet re-measurement At 400 options with 46 rules, classification with a limit of 1 took 0.2 s where it took 2.1 s (p5f_quiet_measurements.md §7: 0.203-0.205 s against 2.120-2.123 s at 22adb00), not 0.3 and 2.4. Text only. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01URSWftXy2VPwQBGhbZQV8D
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
All work since
release/0.5(0bc6bae), as one branch at c5b9a99. Every local branch of this work is an ancestor of c5b9a99, so nothing had to be merged or rebased: 250 commits, 187 files, +128,003/−3,312.What it holds, oldest first:
design/20260928_secondary_plan.md; the guide isdesign/20260930_walkthrough.md), merged intofeature/faster-solverat 2798ecf. They cover docs truth, dead code, measurement, projection, proof records, isolation searches and rule macros.benchmark/scaling/.Compactrow reducer.Construction, a catalog of algebraic constructions.Autoandrecommend, plus a proven lower bound with every design.Auto()becomes the default engine.Verification
validate_design.IPOG()'s rows on purpose. From Phase 4 on, fixture 1's fingerprint isrows=948 fingerprint=3b06a73a3fd3eec0.benchmark/snapshot.jl's output is byte-identical from the default switch (31bef0f) through c5b9a99.Known, not addressed here
_IPOG_MEMBERS' docstring (src/ipog_core.jl:76–77) still calls the member set provisional and open. The maintainer closed that question on October 7, keeping four members.🤖 Generated with Claude Code
https://claude.ai/code/session_01URSWftXy2VPwQBGhbZQV8D