Repository navigation
Tooling: overlap bit589 and complex741 in the #741 ancestry replay, 17% (50% with --complex-jobs 3) less wall time (no new kappa) - #1101
Conversation
…eplay (no new kappa) New sibling driver; verify_frontier741.py stays unchanged (hash-pinned). Same commands, env and output layout; fail-fast. About 17% less wall time, same output tree modulo timings and digests of timing-bearing files. Substantial AI assistance.
34c789c to
4329398
Compare
|
Linux evidence for this PR (addresses the "Linux CI not run" open item in the note). Run: https://github.com/rcfc-jreed/integer-mult-bounds/actions/runs/38447255855 on fork branch Setup follows
All three passed with the same exact result. Caveats: one run each, and each job ran on a different hosted VM, so absolute times are noisy (bit589 alone took 222 to 398 s across the three). Treat the ratios as indicative. They are consistent in direction with the WSL measurements in the note (-17% and -50%). Not run on Linux: the downstream #799 and #1042 replays with this driver's output. |
…r's output as ancestor
|
Downstream check added: the concurrent driver's output was used as --ancestor\ for \�erify_frontier799.py\ (WSL, default concurrent mode). Result: \PASS_REBUILT_PR589_PR799_COMPOSITION, kappa 1661634653669567/10^18, in 203 s, and \�erify_replay_coverage.py --frontier 799 --ancestor ...\ printed \PASS_COMPLETE_PR799_REPLAY_COVERAGE. It is recorded as reused ancestry ( |
|
End-to-end result added (WSL, rebased PR tree, same checkout, one run each, back to back). Cold \�erify_frontier1042.py: 1560 s. New path (concurrent 741 driver 467 s -> \�erify_frontier799.py --ancestor\ 189 s -> \�erify_frontier1042.py --baseline799\ 756 s): 1412 s, i.e. 148 s (9.5%) less. Both ended in \PASS_COMPLETE_PR1042_COMPOSITION, kappa 0.001672188119205421. About 132 s of the saving is the #741 part; the rest is run-to-run noise in 1042's own stages. Single runs, so treat as roughly +/-2%. Details and caveats are in the updated note. |
|
100-PR batch review at Merged to Reviewed scope: Opt-in concurrent PR589/741 replay driver; focused tests check exact supplier commands, environment scrubbing, completion ordering and failure cancellation. No independent full-chain timing claim. The pinned scoped command passed; the batch ledger contains its command, input hashes, environment and log. This incorporates the research/tooling contribution and does not change the selected κ or discharge the inherited multiplication-theorem assumptions. Batch review, attribution and evidence. Thank you for the contribution. |
Exact-head retention and overlap facts for #1101, #1108, #1142, #1151, #1277, #1361, #1509 and #1646 against main 1f7a934, with a stdlib checker. #1142 fails on current main (stale selected-record pin) and re-adds an earlier copy of #1108's package (add/add conflict). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Concurrent bit/complex replay of the #589 + #741 ancestry
Status: tooling improvement. It changes no construction, bound, certificate or
selected record, and claims no new kappa.
What changed
scripts/verify_frontier741.py(the cold ancestry replay thatverify_frontier799.pyruns, and hence the selected
make frontier1042-verifychain) runsbit589tocompletion and then
complex741. Neither reads anything theother writes:
bit589writes only under<work>/bit,complex741only under<work>/complex, and the binding step needs both. The newscripts/verify_frontier741_concurrent.pyruns the same two commands at the sametime, then the same binding script.
verify_frontier741.pyis untouched because its sha256 is pinned incertificates/selected-result.jsonand the checkpoint certificates. The new driveris a sibling that writes the same layout (
bit/,complex/,bit589.log,complex741.log,STEPS.json,RESULT.json) plus aCONCURRENCY.jsonwith wall andsummed job times. If either supplier fails, the other is stopped (process group
SIGTERM, then SIGKILL after 20 s), the failing log is named, and nothing is bound.
--complex-jobs N(N>1) swaps in the existing dependency-scheduled complex replay(
verify_complex741_parallel.py, #853); the default of 1 runsverify.pyunchanged sothat this change is measured on its own.
Reproduce
Expected: the first prints
PASS selected finite composition; inherited hypotheses remain, andRESULT.jsonhas statusPASS_REBUILT_PR589_PR741_COMPOSITION, kappa1661202643272239/1000000000000000000. The second printsPASS_COMPLETE_PR741_REPLAY_COVERAGE. The tests (8) take about 3 s.Developed and measured at base commit
2921874911956718fcaaaf9396fe8267b3cfa9f0.The branch is rebased onto
ba82555c(main when submitted);verify_frontier741.py,its pinned hash, the bindings script and both supplier packages are unchanged between
the two, and the tests were re-run on the rebased tree. Benchmark environment (not the
CI image): WSL2 Ubuntu 24.04, 28 logical CPUs, 7 GB RAM; Python 3.12.15, numpy 2.5.4,
scipy 1.18.1, sympy 1.14.0; the C++17 checkers built with
zig c++(ziglang 0.17.0,clang 22.1.8) against Boost 1.86.0 headers. No system compiler was available.
Measurement
Same checkout, same fresh output path each time, one run at a time on an otherwise idle
machine. The first row used different checkout/output paths and is timing only.
--complex-jobs 3Sequential mean 590 s, concurrent mean 487 s: about 17% less wall time, 100 to 120 s
saved. The concurrent run is bounded below by
complex741(critical path 469 to 495 s),so the bit supplier is hidden but nothing else is. With
--complex-jobs 3the complexchain shortens to the dependency chain of #853 and the bit supplier is again fully
hidden: 293 s, about 50% less than sequential (one sample). That is 3 sequential, 2
concurrent and 1 combined samples on one machine; treat the ratios as indicative, not
as precise speedups. #853 alone would leave
bit589(about 140 s) in series with thecomplex replay; that exact configuration was not run here.
Coverage is unchanged
tests/test_frontier741_concurrent.pyparsesverify_frontier741.pyand requires theconcurrent driver's
bit589,complex741andbindingscommands, stage order andenvironment scrub (
PYTHONOPTIMIZE,WITNESS_DISCOVER,WITNESS_RECORD,SW4_PIN)to equal the original's. If the original changes, the test fails.
file: 385 common files, 101 differ. A second original run differs from the first in
exactly the same 101 files, so the concurrent schedule adds no new difference. After
removing
seconds/elapsedfields and SHA-256 values (digests of files that embedtimings), every differing JSON file is identical in both comparisons. The remaining
differing files are logs.
verify_replay_coverage.py --frontier 741and theoriginal bindings check.
bit_lower_decimalfails the bindings check (
Rebuilt bit differs); one extra byte appended tocomplex/global-replay/ASSEMBLY.jsonfails coverage (Required ancestry artifact hash differs); a deletedbit/xcheck.jsonfails.-Oto the complexcommand, removing
SW4_PINfrom the scrub, not stopping the sibling after a failure,and waiting for each job right after launching it are each caught. (The
SW4_PINmutation first survived; the test now sets the variable before checking the scrub.)
Scope and open items
listed in
certificates/selected-result.jsonremains.be passed as
--ancestortoverify_frontier799.py. That was run once (WSL, defaultconcurrent mode, base
2921874; the 799 scripts are unchanged on later main):verify_frontier799.py --work W --ancestor <output>passed in 203 s withPASS_REBUILT_PR589_PR799_COMPOSITION, kappa1661634653669567/10^18, andverify_replay_coverage.py --frontier 799 --ancestor <output>printedPASS_COMPLETE_PR799_REPLAY_COVERAGE. It records the ancestor as reused(
reused_ancestry: true), as for any externally produced ancestor. Nothing herechanges what
make frontier1042-verify(orfrontier942-verify) runs.frontier1042on the rebased PR tree (WSL, same checkout, one runeach, one after the other): the original
verify_frontier1042.pytook 1560 s(
baseline799-cold788 s, its own stages 772 s). The new path (concurrent driver 467 s,then
verify_frontier799.py --ancestor189 s, thenverify_frontier1042.py --baseline799756 s, with the ancestor moved to<baseline799>/ancestoras that script expects) took 1412 s, 148 s or 9.5% less.Both ended in
PASS_COMPLETE_PR1042_COMPOSITIONwith kappa0.001672188119205421; the new path recordsreused_completed_baseline: true. About132 s of the saving is the 741 part (788 s to 656 s); the rest is run-to-run noise in
1042's own stages (chain 479 s vs 464 s). Single runs, so about +/-2% should be
assumed. The Conditional κ = 0.001661960547713947: T37 whole-owner packing and all-T bound #942 replay was not run with it.
complex741only anddoes not overlap the bit supplier; no open or merged PR found by search touches
verify_frontier741.pyor overlapsbit589withcomplex741. The two arecomplementary: with
--complex-jobs 3the complex chain hidesbit589entirely (tableabove).
--complex-jobs 3was run cold once (293 s). Its output has the same 385 files as thesequential tree and passes
verify_replay_coverage.py --frontier 741. Against thesequential tree it differs in the 101 noise files plus
complex741.log, whose 45lines differ only in the order of
RUN/PASSprogress messages; every differing JSONfile is identical after masking
secondsand SHA-256 values.u8-nativestage (about 254 s) and the cold Conditional κ = 0.001661634653669567: four paired read exchanges on PR741's frame-coalesced word #799nativestage (about 393 s)dominate the remaining serial time and were not examined.
completed it.
Credit and disclosure
Builds on the pinned
verify_frontier741.pydriver,verify_frontier741_bindings.py(Douglas Colkitt, with OpenAI Codex assistance), the
dependency-scheduled complex replay of #853 (Aaron / navinor), and the
--jobspatternof
verify_frontier596.py. Track: verification engineering, assignment seed 90, basecommit above. Substantial AI assistance (Claude, in Cursor) in analysis, code, tests
and this note. Contributor: James Reed (@rcfc-jreed).