diff --git a/research/finite-bit-rank-cache-seed87/BENCHMARK.json b/research/finite-bit-rank-cache-seed87/BENCHMARK.json new file mode 100644 index 0000000000..27121248cd --- /dev/null +++ b/research/finite-bit-rank-cache-seed87/BENCHMARK.json @@ -0,0 +1,585 @@ +{ + "assignment_seed": 87, + "measurements": [ + { + "cached": { + "rank_calls": { + "block_core": { + "calls": 360, + "eliminations": 63 + }, + "fano": { + "calls": 30, + "eliminations": 2 + }, + "rank_product": { + "calls": 914, + "eliminations": 117 + }, + "rational": { + "calls": 100, + "eliminations": 88 + } + }, + "seconds": { + "block_core": 3.9057648750022054, + "complete_fano_audit": 0.05564216698985547, + "fano": 0.021575249964371324, + "rank_product": 0.17827579099684954, + "rational": 0.02011312497779727 + } + }, + "order": [ + "reference", + "cached" + ], + "reference": { + "rank_calls": { + "block_core": { + "calls": 764, + "eliminations": 63 + }, + "fano": { + "calls": 5532, + "eliminations": 2 + }, + "rank_product": { + "calls": 2869, + "eliminations": 117 + }, + "rational": { + "calls": 264, + "eliminations": 88 + } + }, + "seconds": { + "block_core": 4.920165417017415, + "complete_fano_audit": 0.08286983397556469, + "fano": 0.03891083301277831, + "rank_product": 0.278271000017412, + "rational": 0.013784958980977535 + } + } + }, + { + "cached": { + "rank_calls": { + "block_core": { + "calls": 360, + "eliminations": 63 + }, + "fano": { + "calls": 30, + "eliminations": 2 + }, + "rank_product": { + "calls": 914, + "eliminations": 117 + }, + "rational": { + "calls": 100, + "eliminations": 88 + } + }, + "seconds": { + "block_core": 3.730783916951623, + "complete_fano_audit": 0.060301874997094274, + "fano": 0.02243658300722018, + "rank_product": 0.13013558398233727, + "rational": 0.025101541017647833 + } + }, + "order": [ + "cached", + "reference" + ], + "reference": { + "rank_calls": { + "block_core": { + "calls": 764, + "eliminations": 63 + }, + "fano": { + "calls": 5532, + "eliminations": 2 + }, + "rank_product": { + "calls": 2869, + "eliminations": 117 + }, + "rational": { + "calls": 264, + "eliminations": 88 + } + }, + "seconds": { + "block_core": 4.597513124987017, + "complete_fano_audit": 0.08011312497546896, + "fano": 0.04242445802083239, + "rank_product": 0.2647875409456901, + "rational": 0.020638125017285347 + } + } + }, + { + "cached": { + "rank_calls": { + "block_core": { + "calls": 360, + "eliminations": 63 + }, + "fano": { + "calls": 30, + "eliminations": 2 + }, + "rank_product": { + "calls": 914, + "eliminations": 117 + }, + "rational": { + "calls": 100, + "eliminations": 88 + } + }, + "seconds": { + "block_core": 3.9063674170174636, + "complete_fano_audit": 0.057388458983041346, + "fano": 0.02283995901234448, + "rank_product": 0.18252375000156462, + "rational": 0.018420082982629538 + } + }, + "order": [ + "reference", + "cached" + ], + "reference": { + "rank_calls": { + "block_core": { + "calls": 764, + "eliminations": 63 + }, + "fano": { + "calls": 5532, + "eliminations": 2 + }, + "rank_product": { + "calls": 2869, + "eliminations": 117 + }, + "rational": { + "calls": 264, + "eliminations": 88 + } + }, + "seconds": { + "block_core": 4.268859333009459, + "complete_fano_audit": 0.0647972910082899, + "fano": 0.036896125006023794, + "rank_product": 0.2605865419609472, + "rational": 0.018252375011797994 + } + } + }, + { + "cached": { + "rank_calls": { + "block_core": { + "calls": 360, + "eliminations": 63 + }, + "fano": { + "calls": 30, + "eliminations": 2 + }, + "rank_product": { + "calls": 914, + "eliminations": 117 + }, + "rational": { + "calls": 100, + "eliminations": 88 + } + }, + "seconds": { + "block_core": 3.8020596660207957, + "complete_fano_audit": 0.052058667002711445, + "fano": 0.02010487503139302, + "rank_product": 0.1935030419845134, + "rational": 0.013365958002395928 + } + }, + "order": [ + "cached", + "reference" + ], + "reference": { + "rank_calls": { + "block_core": { + "calls": 764, + "eliminations": 63 + }, + "fano": { + "calls": 5532, + "eliminations": 2 + }, + "rank_product": { + "calls": 2869, + "eliminations": 117 + }, + "rational": { + "calls": 264, + "eliminations": 88 + } + }, + "seconds": { + "block_core": 4.659334875002969, + "complete_fano_audit": 0.079318875039462, + "fano": 0.05847083404660225, + "rank_product": 0.25356350000947714, + "rational": 0.018068709003273398 + } + } + }, + { + "cached": { + "rank_calls": { + "block_core": { + "calls": 360, + "eliminations": 63 + }, + "fano": { + "calls": 30, + "eliminations": 2 + }, + "rank_product": { + "calls": 914, + "eliminations": 117 + }, + "rational": { + "calls": 100, + "eliminations": 88 + } + }, + "seconds": { + "block_core": 3.512706625042483, + "complete_fano_audit": 0.05306062498129904, + "fano": 0.01512783404905349, + "rank_product": 0.1535891669918783, + "rational": 0.011829166964162141 + } + }, + "order": [ + "reference", + "cached" + ], + "reference": { + "rank_calls": { + "block_core": { + "calls": 764, + "eliminations": 63 + }, + "fano": { + "calls": 5532, + "eliminations": 2 + }, + "rank_product": { + "calls": 2869, + "eliminations": 117 + }, + "rational": { + "calls": 264, + "eliminations": 88 + } + }, + "seconds": { + "block_core": 4.753191958006937, + "complete_fano_audit": 0.06779308401746675, + "fano": 0.03607024997472763, + "rank_product": 0.2926543750218116, + "rational": 0.01762112497817725 + } + } + }, + { + "cached": { + "rank_calls": { + "block_core": { + "calls": 360, + "eliminations": 63 + }, + "fano": { + "calls": 30, + "eliminations": 2 + }, + "rank_product": { + "calls": 914, + "eliminations": 117 + }, + "rational": { + "calls": 100, + "eliminations": 88 + } + }, + "seconds": { + "block_core": 3.876512749993708, + "complete_fano_audit": 0.05360904202098027, + "fano": 0.019171749998349696, + "rank_product": 0.19656999997096136, + "rational": 0.019323958025779575 + } + }, + "order": [ + "cached", + "reference" + ], + "reference": { + "rank_calls": { + "block_core": { + "calls": 764, + "eliminations": 63 + }, + "fano": { + "calls": 5532, + "eliminations": 2 + }, + "rank_product": { + "calls": 2869, + "eliminations": 117 + }, + "rational": { + "calls": 264, + "eliminations": 88 + } + }, + "seconds": { + "block_core": 4.614944499975536, + "complete_fano_audit": 0.05475416698027402, + "fano": 0.03842699999222532, + "rank_product": 0.2504682500148192, + "rational": 0.016847915947437286 + } + } + }, + { + "cached": { + "rank_calls": { + "block_core": { + "calls": 360, + "eliminations": 63 + }, + "fano": { + "calls": 30, + "eliminations": 2 + }, + "rank_product": { + "calls": 914, + "eliminations": 117 + }, + "rational": { + "calls": 100, + "eliminations": 88 + } + }, + "seconds": { + "block_core": 3.8495795839698985, + "complete_fano_audit": 0.052967124967835844, + "fano": 0.022841750003863126, + "rank_product": 0.19972337497165427, + "rational": 0.01794745895313099 + } + }, + "order": [ + "reference", + "cached" + ], + "reference": { + "rank_calls": { + "block_core": { + "calls": 764, + "eliminations": 63 + }, + "fano": { + "calls": 5532, + "eliminations": 2 + }, + "rank_product": { + "calls": 2869, + "eliminations": 117 + }, + "rational": { + "calls": 264, + "eliminations": 88 + } + }, + "seconds": { + "block_core": 4.668139374989551, + "complete_fano_audit": 0.06828845897689462, + "fano": 0.04350075003458187, + "rank_product": 0.2675327089964412, + "rational": 0.02064304199302569 + } + } + }, + { + "cached": { + "rank_calls": { + "block_core": { + "calls": 360, + "eliminations": 63 + }, + "fano": { + "calls": 30, + "eliminations": 2 + }, + "rank_product": { + "calls": 914, + "eliminations": 117 + }, + "rational": { + "calls": 100, + "eliminations": 88 + } + }, + "seconds": { + "block_core": 3.376455374993384, + "complete_fano_audit": 0.05965495796408504, + "fano": 0.01985662500374019, + "rank_product": 0.18853966699680313, + "rational": 0.01987924997229129 + } + }, + "order": [ + "cached", + "reference" + ], + "reference": { + "rank_calls": { + "block_core": { + "calls": 764, + "eliminations": 63 + }, + "fano": { + "calls": 5532, + "eliminations": 2 + }, + "rank_product": { + "calls": 2869, + "eliminations": 117 + }, + "rational": { + "calls": 264, + "eliminations": 88 + } + }, + "seconds": { + "block_core": 4.702627125021536, + "complete_fano_audit": 0.07238879200303927, + "fano": 0.045258958998601884, + "rank_product": 0.26025300001492724, + "rational": 0.01715170801617205 + } + } + }, + { + "cached": { + "rank_calls": { + "block_core": { + "calls": 360, + "eliminations": 63 + }, + "fano": { + "calls": 30, + "eliminations": 2 + }, + "rank_product": { + "calls": 914, + "eliminations": 117 + }, + "rational": { + "calls": 100, + "eliminations": 88 + } + }, + "seconds": { + "block_core": 3.8311417079530656, + "complete_fano_audit": 0.051568583003245294, + "fano": 0.020003875019028783, + "rank_product": 0.1941768749966286, + "rational": 0.015324290958233178 + } + }, + "order": [ + "reference", + "cached" + ], + "reference": { + "rank_calls": { + "block_core": { + "calls": 764, + "eliminations": 63 + }, + "fano": { + "calls": 5532, + "eliminations": 2 + }, + "rank_product": { + "calls": 2869, + "eliminations": 117 + }, + "rational": { + "calls": 264, + "eliminations": 88 + } + }, + "seconds": { + "block_core": 4.695428624982014, + "complete_fano_audit": 0.07539145805640146, + "fano": 0.039562500023748726, + "rank_product": 0.2613820409751497, + "rational": 0.02066550002200529 + } + } + } + ], + "medians": { + "block_core": { + "cached_median_seconds": 3.8311417079530656, + "reference_median_seconds": 4.668139374989551, + "speedup": 1.2184721241970669 + }, + "complete_fano_audit": { + "cached_median_seconds": 0.05360904202098027, + "reference_median_seconds": 0.07238879200303927, + "speedup": 1.3503093745773225 + }, + "fano": { + "cached_median_seconds": 0.02010487503139302, + "reference_median_seconds": 0.039562500023748726, + "speedup": 1.9678063137409878 + }, + "rank_product": { + "cached_median_seconds": 0.18853966699680313, + "reference_median_seconds": 0.2613820409751497, + "speedup": 1.3863503905498131 + }, + "rational": { + "cached_median_seconds": 0.018420082982629538, + "reference_median_seconds": 0.018068709003273398, + "speedup": 0.9809244084466128 + } + }, + "platform": "macOS-26.5.2-arm64-arm-64bit", + "python": "3.12.15 (main, Sep 30 2026, 22:04:19) [Clang 21.0.0 (clang-2100.1.1.101)]", + "receipt_sha256": "93acaade285fe35afc2a3ad87283c04c86d0a766d03e432dec738a60a8e52ca3", + "scope": "Exact verifier tooling; no new kappa.", + "status": "PASS_FINITE_BIT_TRANSITION_CACHE", + "tests": { + "cached": { + "tests_run": 53 + }, + "reference": { + "tests_run": 53 + } + } +} diff --git a/research/finite-bit-rank-cache-seed87/CLAIM.md b/research/finite-bit-rank-cache-seed87/CLAIM.md new file mode 100644 index 0000000000..e20d057208 --- /dev/null +++ b/research/finite-bit-rank-cache-seed87/CLAIM.md @@ -0,0 +1,61 @@ +# Finite-bit repeated-transition rank cache + +Claim recorded 2026-10-14 03:05 UTC. Expected finish 03:37 UTC. +Track: verification engineering. OS-random assignment seed: 87. +Base: `680967accfd4311f3241dc154e1f434869747b43`. + +Investigate exact repeated frame-pair ranks inside +`scripts/finite_bit_contract.py:inspect_candidate`. Intern normalized rational +frames and reuse a rank only for an identical ordered pair within one call. +Preserve validation, every physical edge, edge order and the full result. +Deliver an opt-in source-pinned patch, complete same-input differential replay, +failure controls and before/after measurements. Frozen scripts and certificates +stay unchanged; this is verifier tooling, with no new kappa claim. + +Three candidates considered: repeated finite-bit edge ranks; Fano graph +reachability; prime-subset exact arithmetic. The complete Fano profile spent +0.305 of 0.430 profiled seconds in `inspect_candidate`. Prime-subset screening +took 0.068 seconds and scalar Fano replay 0.008 seconds. The selected target +has repeated work across larger rank-product and block-core fixtures too. +Seed 87 fixes the rational perturbation/mutation test stream. + +Initial overlap: 719 open PRs with complete pagination, cached at 03:02 UTC; +local package notes and review ledger; 83 discussion threads and their comments +refreshed immediately before this claim. No pinned coordination issue exists, +so this claim is local as requested. PR808 changes cyclic routing-state search, +not exact edge-rank evaluation. PR1234 and PR1459/1461 address rational span +normalization/containment, not this checker. No matching active claim found. +Titles alone were not used: the repository overlap helper searched PR bodies, +cached discussion comments/replies and local package metadata. Its live refresh +timed out, so the direct discussion inventory supplied the freshness check. + +Acceptance: full receipt equality on unchanged Fano and nonzero rational +rank-product/block-core fixtures; all existing relevant tests on both engines; +invalid input and between-call mutation controls; same-input alternating-order +wall-clock benchmark. No timing threshold is a mathematical acceptance rule. +Stop implementation by 03:27 UTC, reserving the final ten minutes for checking +and handoff. Contributor: Sagar Thakrar, with substantial OpenAI Codex assistance. + +## Result and release + +Completed 2026-10-14 03:26 UTC. [PR1584](https://github.com/CrocSwap/integer-mult-bounds/pull/1584) +contains the opt-in adapter and exact replay. Research commit: +`f1a8ff7d81f33621cc27b744e9eece5aea8bea94`. The final upstream refresh was +`ddb4371c16a5a5de9e363afa8c0d6d7c27429e3c`; all 57 live inputs stayed unchanged. + +Nine alternating fresh-process pairs on Python 3.12.15 give median speedups +1.2185x for both 64-dimensional block-core checks, 1.3864x for rank-product +checks and 1.3503x for the complete Fano audit. The varied rational controls +are about 2% slower. All complete receipts match, with digest +`93acaade285fe35afc2a3ad87283c04c86d0a766d03e432dec738a60a8e52ca3`. +Both engines pass all 53 existing tests on Python 3.12.15 and 3.14.8, eleven +rejection controls and the mutate/restore check. Registered replay passes +under inherited `PYTHONOPTIMIZE=2`; a worker invoked directly with `-O` fails. +Metadata pins, Python 3.10 grammar, JSON and whitespace checks pass. + +Final overlap refresh covered 723 open PR bodies through PR1582 and 86 +discussion threads, 228 records including comments/replies with no pagination +gaps. Only the distinct PR808 routing-state optimization matched the checker +name. No matching active claim or pinned coordination issue was found. +No selected cold replay, Linux execution, native compiler, hosting, precision, +tape or analytic-interface proof was attempted. No new kappa. Scope released. diff --git a/research/finite-bit-rank-cache-seed87/PORTABILITY.json b/research/finite-bit-rank-cache-seed87/PORTABILITY.json new file mode 100644 index 0000000000..4f5f685c03 --- /dev/null +++ b/research/finite-bit-rank-cache-seed87/PORTABILITY.json @@ -0,0 +1,105 @@ +{ + "assignment_seed": 87, + "measurements": [ + { + "cached": { + "rank_calls": { + "block_core": { + "calls": 360, + "eliminations": 63 + }, + "fano": { + "calls": 30, + "eliminations": 2 + }, + "rank_product": { + "calls": 914, + "eliminations": 117 + }, + "rational": { + "calls": 100, + "eliminations": 88 + } + }, + "seconds": { + "block_core": 3.9520934589672834, + "complete_fano_audit": 0.05631933402037248, + "fano": 0.020035666995681822, + "rank_product": 0.2659540000022389, + "rational": 0.019999415962956846 + } + }, + "order": [ + "reference", + "cached" + ], + "reference": { + "rank_calls": { + "block_core": { + "calls": 764, + "eliminations": 63 + }, + "fano": { + "calls": 5532, + "eliminations": 2 + }, + "rank_product": { + "calls": 2869, + "eliminations": 117 + }, + "rational": { + "calls": 264, + "eliminations": 88 + } + }, + "seconds": { + "block_core": 4.770882459008135, + "complete_fano_audit": 0.05324716598261148, + "fano": 0.05275883403373882, + "rank_product": 0.323687499971129, + "rational": 0.018165000015869737 + } + } + } + ], + "medians": { + "block_core": { + "cached_median_seconds": 3.9520934589672834, + "reference_median_seconds": 4.770882459008135, + "speedup": 1.2071785519603597 + }, + "complete_fano_audit": { + "cached_median_seconds": 0.05631933402037248, + "reference_median_seconds": 0.05324716598261148, + "speedup": 0.9454509167908537 + }, + "fano": { + "cached_median_seconds": 0.020035666995681822, + "reference_median_seconds": 0.05275883403373882, + "speedup": 2.633245703530092 + }, + "rank_product": { + "cached_median_seconds": 0.2659540000022389, + "reference_median_seconds": 0.323687499971129, + "speedup": 1.2170807732480207 + }, + "rational": { + "cached_median_seconds": 0.019999415962956846, + "reference_median_seconds": 0.018165000015869737, + "speedup": 0.9082765241502634 + } + }, + "platform": "macOS-26.5.2-arm64-arm-64bit-Mach-O", + "python": "3.14.8 (main, Sep 30 2026, 17:55:09) [Clang 21.0.0 (clang-2100.1.1.101)]", + "receipt_sha256": "93acaade285fe35afc2a3ad87283c04c86d0a766d03e432dec738a60a8e52ca3", + "scope": "Exact verifier tooling; no new kappa.", + "status": "PASS_FINITE_BIT_TRANSITION_CACHE", + "tests": { + "cached": { + "tests_run": 53 + }, + "reference": { + "tests_run": 53 + } + } +} diff --git a/research/finite-bit-rank-cache-seed87/README.md b/research/finite-bit-rank-cache-seed87/README.md new file mode 100644 index 0000000000..eef75fd84e --- /dev/null +++ b/research/finite-bit-rank-cache-seed87/README.md @@ -0,0 +1,142 @@ +# Exact finite-bit transition caching + +Verification tooling. No new kappa or construction is claimed. + +The retained finite-bit checker already caches exact elimination results, but +still subtracts and hashes a rational matrix for every physical edge. The +opt-in [adapter](adapter.py) interns normalized frames once per call and uses +an integer pair to reuse an identical transition. Its nine-line replacement +leaves all input, scalar, endpoint and deficit checks in place. Every physical +edge still contributes its own charge, in its original position. + +Base commit: `680967accfd4311f3241dc154e1f434869747b43`. +Final upstream refresh: `ddb4371c16a5a5de9e363afa8c0d6d7c27429e3c`; +all 57 live inputs remain byte-identical to the research base. +The selected record at that commit is PR1094's conditional +`kappa = 836330098538459/500000000000000000`. +[SOURCES.json](SOURCES.json) pins 57 live inputs and two provenance files by +Git blob and SHA256. The original checker, frozen certificates and `upstream/` +are unchanged. Loading fails if the checker's pinned source bytes differ. + +## Why the cache preserves the check + +Validation first converts every frame to an immutable tuple of exact +`Fraction` entries. Python dictionary equality compares the complete tuple, +including entries, so equal IDs imply equal matrices. A hash collision does +not equate unequal keys. The key for an edge is its ordered source/sink ID +pair. On the first occurrence, the unchanged expression computes +`rank(sink - source)`. Every repeated pair has exactly the same difference +matrix, hence the same rational rank. Appending that rank for every original +edge preserves the complete edge-rank list, its sum and every returned field. + +Both dictionaries are local to one `inspect_candidate` call. A caller can +change a frame between calls and must receive a newly checked result. The +adapter caches no circuit validity or completed audit verdict. It uses the +original arithmetic, including the existing bounded elimination cache. + +There are at most F frame keys and E transition keys for F frames and E edges. +This adds O(F + E) references in the worst case. Workloads with few repeated +frames need not benefit. The measurements are finite runtime evidence, not +an asymptotic improvement or a formal proof of the multiplication theorem. + +## Reproduce + +From the repository root, with Python 3.12 and the standard library: + +```sh +python3.12 -B scripts/research_package.py --package research/finite-bit-rank-cache-seed87 +``` + +Expected result: `PASS_FINITE_BIT_TRANSITION_CACHE`. The command validates +source pins, compares complete reference/cached receipts, and runs 53 existing +tests under each engine. It does not write generated certificates. +The registered replay also passes with `PYTHONOPTIMIZE=2` inherited by its +driver. Child processes explicitly enable assertions, and directly launching a +worker with `-O` fails. This retains assertions used by historical dependencies. + +For the benchmark, run: + +```sh +python3.12 -B research/finite-bit-rank-cache-seed87/verify.py --pairs 9 +``` + +Each engine runs in a fresh subprocess. Pair order alternates, and each +fixture group starts with the inherited rank cache cleared. Timing includes +normalization, scalar validation, all endpoints, the complete physical edge +list and scoring. Fixture construction and process startup are excluded from +the reported group times. The complete Fano audit is also timed separately. +No wall-clock threshold controls acceptance. + +The fixed domain is all 15 Fano completion fixtures, all five existing +rank-product controls, both existing 64-dimensional block-core controls, and +12 rational-frame fixtures. The latter use seed 87, dimensions 2, 3, 4 and 8, +and banks of 1, 3 and 17 frames, with signed numerators -3 through 3 and +denominators 1 through 5. This is differential coverage, not a search for a +stronger bound. The stopping rule is at most nine benchmark pairs. + +Eleven controls reject bad endpoints, a wrong permutation, an omitted scalar +update, a float, a wrong dimension, repeated ports, a missing terminal, a zero +denominator, equality submitted as a strict deficit, and two source-byte +changes. A valid frame mutation changes the edge charges; restoring it recovers +the original receipt. Reference and cached engines must agree on the full +error class and message as well as accepted receipts. + +[BENCHMARK.json](BENCHMARK.json) records individual measurements, exact receipt +digest, rank-call counts and environment. Every complete receipt is compared +before it is reduced to a digest in that report. The existing test modules are +listed explicitly in `verify.py`; no test is selected by a performance result. + +Nine alternating fresh-process pairs on macOS arm64, CPython 3.12.15: + +| Workload | Reference median | Cached median | Speedup | +| --- | ---: | ---: | ---: | +| Both 64-dimensional block-core controls | 4.6681 s | 3.8311 s | 1.2185x | +| Five rank-product controls | 0.2614 s | 0.1885 s | 1.3864x | +| Fifteen Fano frame checks | 0.0396 s | 0.0201 s | 1.9678x | +| Complete Fano audit | 0.0724 s | 0.0536 s | 1.3503x | +| Twelve varied rational-frame controls | 0.0181 s | 0.0184 s | 0.9809x | + +The last workload is about 2% slower, so this is not a universal speedup. +For the Fano checks, rank-function calls fall from 5,532 to 30 while exact +elimination misses remain two. Block-core calls fall from 764 to 360 with +63 elimination misses in both engines. The benefit comes from avoiding repeated +matrix construction and hashing, not from omitting a distinct elimination. +Every pair produces the canonical full-receipt digest +`93acaade285fe35afc2a3ad87283c04c86d0a766d03e432dec738a60a8e52ca3`. +[PORTABILITY.json](PORTABILITY.json) records the same receipt and 53 tests per +engine on CPython 3.14.8. Python 3.10 syntax parsing passes; execution on 3.10 +and Linux was not tested. The benchmark was not CPU-pinned or isolated from +other host activity; individual samples remain in the report. + +## Credit and scope + +Douglas R. Colkitt authored the retained finite-bit contract, historical Fano, +rank-product and block-core work used here. Their original sources and notices +are preserved. This work is Sagar Thakrar's contribution, with substantial +OpenAI Codex assistance in profiling, implementation, checking and writing. +New work is Apache-2.0, the repository's license. No independent human review +is claimed. + +Nearest parallel work: [4RchYMing's PR808](https://github.com/CrocSwap/integer-mult-bounds/pull/808) +optimizes cyclic routing-state search; +[Richard Hoekstra's PR1234](https://github.com/CrocSwap/integer-mult-bounds/pull/1234) +optimizes rational span normalization and complements; CubeJerry's +[PR1459](https://github.com/CrocSwap/integer-mult-bounds/pull/1459) and +[PR1461](https://github.com/CrocSwap/integer-mult-bounds/pull/1461) optimize +rational containment. Their methods and targets are separate from this per-call +transition cache. Their source heads were inspected in the overlap check; +none is a dependency of this adapter. + +This does not replay the selected supplier, its native compiler, hosting, +precision, tape or analytic interface. All inherited conditional obligations +remain. The added argument proves why identical transitions can reuse a rank; +the finite replay checks implementation agreement on the declared fixtures. + +## Open next questions + +Should the retained checker adopt this cache? Review the replacement and repeat +the same workload benchmark on Linux first. Adoption would require maintainer +review and explicit migration of the six historical certificates that pin the +original checker. There is no justification here to change the selected +frontier or to optimize unrelated frame algorithms. [TASK.json](TASK.json) +records the same bounded follow-up. diff --git a/research/finite-bit-rank-cache-seed87/SOURCES.json b/research/finite-bit-rank-cache-seed87/SOURCES.json new file mode 100644 index 0000000000..7fe6989750 --- /dev/null +++ b/research/finite-bit-rank-cache-seed87/SOURCES.json @@ -0,0 +1,360 @@ +{ + "schema_version": 1, + "base_commit": "680967accfd4311f3241dc154e1f434869747b43", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "c05fafaa25ba95b2d5af86b1800427198e3d20eb", + "sha256": "89b5928bc92c81e2647b6d702a7ad85a6795b8f44e2eb267b2ff3145d8f2b2ce" + }, + { + "path": "docs/research/fano-completion-audit.md", + "usage": "input", + "git_blob": "820f070c55a1574b5b7147531495062434ec9157", + "sha256": "ebdf7452c0dc1810d3820263341c25541ad75b1b0d9f4668011309ef0ec969e2" + }, + { + "path": "scripts/audit_cancellation.py", + "usage": "input", + "git_blob": "bc3900f5903337d91a94f28d51429754c4c4b417", + "sha256": "508934ee4d9514a5519813603b6192a0d53103b6e30d65b8d53a1a774de244b6" + }, + { + "path": "scripts/audit_cyclic_topology.py", + "usage": "input", + "git_blob": "a6420a4ccf3066ba9f54cfb9f758cb6d9b9b3b90", + "sha256": "b20ece2cf1337e1808e35b602a0120c6aedaf602fa2315560726a149e9838c29" + }, + { + "path": "scripts/audit_fano_completion.py", + "usage": "input", + "git_blob": "56e3370aea0678ea6ee4228083fa570a9adb124e", + "sha256": "427c369eb2adec9214c5e804bb4413c5a1c4ecbe74ed81c4d65e1b11faa60ed0" + }, + { + "path": "scripts/audit_fused_block.py", + "usage": "input", + "git_blob": "c63869d22c6454cf6989bb6e70d41f0571eef985", + "sha256": "2afb83ca8e5f193ca8a4c242becf267ad1d9dc2578ba238b820e98d5185f6288" + }, + { + "path": "scripts/audit_joint_frames.py", + "usage": "input", + "git_blob": "913be4a1f0a651f3aaf7b4ed1901916918ba2cef", + "sha256": "3df8061392ce0ba42bbde8c02f2a30c8141145e70e9a48c18da73d3aafb14423" + }, + { + "path": "scripts/audit_rank_product_core.py", + "usage": "input", + "git_blob": "62e1863c128d371af5a07ced80e13740d05979c8", + "sha256": "1471f17e86d6c02d5c288116cc3a53544c881ded47a3500f70dac97b366e46a7" + }, + { + "path": "scripts/audit_subset_cores.py", + "usage": "input", + "git_blob": "4249c322ee806337ec9c907f917584da0b71abac", + "sha256": "ae38397693540a8cc26d416a6edcda271fd0fa2eb88566df690fb569e812f0a3" + }, + { + "path": "scripts/certify.py", + "usage": "input", + "git_blob": "a773311b726fd1ef98a056f6f76010e872d7908a", + "sha256": "2348d95008276c5d5764f7e028c3918e484582cd589bd4d9b82919161745e53e" + }, + { + "path": "scripts/exclusion_circuit.py", + "usage": "input", + "git_blob": "aaa99986c4b81c5d4fbe016fd216a4818940bb95", + "sha256": "b253f9d7318becda1c1f3b24e2287ed44a9c27fcea00cf9d531afb950d0457a0" + }, + { + "path": "scripts/experiments/block_core.py", + "usage": "input", + "git_blob": "971bf31caa06438cf116f96520d538ca71b4d108", + "sha256": "af94018e8f4b80219a8e9e104eae21e34b66fc670217d03ef54862b59c051fc9" + }, + { + "path": "scripts/experiments/cube_core_family.py", + "usage": "input", + "git_blob": "16f4d56790b2c5f710497b086a8bc8d48057d366", + "sha256": "e58f1f4067bda2d4838343f42ec2505316f006561f0702e869847d88b85413a8" + }, + { + "path": "scripts/experiments/fano_completion.py", + "usage": "input", + "git_blob": "86a0ec6e62fc9a371f03d0e87457a085c9e494f3", + "sha256": "6cade2a36b910bf7e68a872dc4fd3560837935cffe80f9526cd012a28b247738" + }, + { + "path": "scripts/experiments/fano_routing_witnesses.json", + "usage": "input", + "git_blob": "c4d04ad21c67f6242760b8f3f86289358b7cf2ca", + "sha256": "2017a4401c16ac58ccd7911b1d2128f1a93a98b108672db709e0c21cda4bb693" + }, + { + "path": "scripts/experiments/partial_routing.py", + "usage": "input", + "git_blob": "e0ab64dbbbefe9cc9b3dd6fb81508de09bc60b28", + "sha256": "dd67bf46aa70f1372d49c30c4fbbaff5664e27331a79ca3319251ceeec11ec00" + }, + { + "path": "scripts/experiments/positive_side_core.py", + "usage": "input", + "git_blob": "df3d6d565f2639482b959ecd26a5dffe27c8207f", + "sha256": "0d453ab7e869d2cf6a43d6865de82583edb390d3c75038271f0fc09e0f3828ba" + }, + { + "path": "scripts/experiments/rank_product_core.py", + "usage": "input", + "git_blob": "e5c093f467aa1edf1fea0e058ccc88806fbc09a1", + "sha256": "7a91c1188c5d42e864a5d2e42397b09c435b526ae4f4210c44bf615de488708e" + }, + { + "path": "scripts/experiments/shared_core.py", + "usage": "input", + "git_blob": "44be9424fc65f7b59eebdaea74de1d7f69b70898", + "sha256": "d3c59b61229956cb54ae1ef9145ed213abdf1ae743929de145a77c43656f01a8" + }, + { + "path": "scripts/experiments/signed_sparse_core.py", + "usage": "input", + "git_blob": "724ebd576383b81acfeabfbc6608b22b29196a6f", + "sha256": "21da8e1de5ab6ac8479183326c2000313d24b47cc5be2f46b4fe6ac3cd59779f" + }, + { + "path": "scripts/experiments/subset_core_family.py", + "usage": "input", + "git_blob": "007e35a943801d5b6f31c343bbbbd931eb6d4ba3", + "sha256": "373a45a8fb4294cdf72d510d54e16d21535227b085aefb008aa092b3ad26e4de" + }, + { + "path": "scripts/finite_bit_contract.py", + "usage": "input", + "git_blob": "3b58da79c478d43a6e9ceaebd7f42105eec098c4", + "sha256": "3cff26a332cb6056f656b824e3a523fb8937d15206ddcc4118b911ac8df1b2a7" + }, + { + "path": "scripts/incidence_rectangles.py", + "usage": "input", + "git_blob": "2368244337fe923452b7bbd33216a00421ace269", + "sha256": "5240fd33dcc3096f5685d10ca360186cad36b355a00d55686a4ea4449417d00e" + }, + { + "path": "scripts/paired_exclusion_circuit.py", + "usage": "input", + "git_blob": "36d1fa2c0235b9b307243a8735e38a3fbf957113", + "sha256": "8f05f04cf06217befd6d0ee0f2d7d0c5c5eb32cfab8c9a8ca7917fd6d620b7d2" + }, + { + "path": "scripts/paired_network.py", + "usage": "input", + "git_blob": "910449dd510c89ca24aa56904d225b86abfb3be7", + "sha256": "991223dc3c1374284c361ed017e42bf732dd971fa0bea2be2282cfb18257b3f7" + }, + { + "path": "scripts/prepare_layers.py", + "usage": "input", + "git_blob": "8e17b52f9573135426d7ba6865c8c9bc8da8639a", + "sha256": "a6e2adc612f264b1c0e51d18ce6315de9ae5e2ae2420aa22e99a22d8bf304947" + }, + { + "path": "scripts/rational_tensor.py", + "usage": "input", + "git_blob": "383bad4ac7546877717fce402fbb3650f8cfd796", + "sha256": "629b3f00a1aaab32fe908a73ca8f8412918209a300e6b1e5afe6325b9cfed3c3" + }, + { + "path": "scripts/routing_smt.py", + "usage": "input", + "git_blob": "21cf37b4a2c6df6cd05b6c3cde5f6ec2b40f113c", + "sha256": "25d2dfb09a34c0c0ecfdf870abe2d3883c95677189836dcce25421b9443e8a44" + }, + { + "path": "scripts/search_network.py", + "usage": "input", + "git_blob": "f03d5c1b2c81afd6c2f1d3ba9e17d4e7bcd31b9b", + "sha256": "3a4faa5037d9b8e7ca5828afac193a96b6966a8b114f14937921795b24ec4f6a" + }, + { + "path": "scripts/shared_point_circuit.py", + "usage": "input", + "git_blob": "8347a0bda63fbfb51b86c6c6d10a7bf541816308", + "sha256": "c9bb7a5df92d260a4e3ad532b53e26936730d7c93f7facfb0784957c1e81c8ba" + }, + { + "path": "scripts/shared_point_network.py", + "usage": "input", + "git_blob": "0ec7e75046fe714968c49178cd7f83e80e9f9d94", + "sha256": "a85e7f0d8c42d6a27e3846308571ca324a1824ac5c2d59e4daa5c7673c33c697" + }, + { + "path": "tests/test_block_core.py", + "usage": "input", + "git_blob": "decf262010fdfe973fb9c88d201647b02c665fd9", + "sha256": "1e037416aa8c16ef989d44fe601a2563c6330614ec41b975f014468774a616bc" + }, + { + "path": "tests/test_fano_completion.py", + "usage": "input", + "git_blob": "09829ffdc7b541fbae1a190e0c3af45e45b59524", + "sha256": "d9c5a40ac3952250ff9793e320e7a08b0562738f1cbb3ffc9bc4331ae16891d9" + }, + { + "path": "tests/test_finite_bit_contract.py", + "usage": "input", + "git_blob": "d26ed2e1eb74332927887fe1423f00feff14b769", + "sha256": "2e64760d4f080747a390ff256671958446366555dbfb449eb1bfa1b01e19468d" + }, + { + "path": "tests/test_positive_side_core.py", + "usage": "input", + "git_blob": "643a3020b9b6dbdf2230be7b9bb6c5a3ce2e637d", + "sha256": "46bd4173c6a3fd9295fc2682bf7f572161e95abc6c61e0859bb2f8eee7fb6319" + }, + { + "path": "tests/test_rank_product_core.py", + "usage": "input", + "git_blob": "d81d43afc2adc9148d1ee57f81de34963bfecfc2", + "sha256": "501c277c785a6fac39ab8f8c758ed12ffba7a6c0bda3fba957a105287224d7d6" + }, + { + "path": "tests/test_shared_core.py", + "usage": "input", + "git_blob": "02463b326f2a5676c913191ef26fe7015f4af1e8", + "sha256": "523398ca2caeba570f978d022ae443c67b2f9992996597bafa7c67b858c4afe7" + }, + { + "path": "tests/test_subset_core_family.py", + "usage": "input", + "git_blob": "b94d98d43352d6f13805a6f9adcaabaa9e3e08ce", + "sha256": "3d776e0d60aa226059a6dc6705ccef1b46f941d3aacd22fd60b5025fa7e45f90" + }, + { + "path": "upstream/LICENSE", + "usage": "input", + "git_blob": "261eeb9e9f8b2b4b0d119366dda99c6fd7d35c64", + "sha256": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4" + }, + { + "path": "upstream/README.md", + "usage": "input", + "git_blob": "c8cb3c3857907bf3465017b9f7ef1add4df5c29b", + "sha256": "8d1ceff898a4e0e681679f91c4def485820be9e99f04e4861f2ce601a364723e" + }, + { + "path": "upstream/build/figures/multiplication-flow.tex", + "usage": "input", + "git_blob": "f0297c9cb841ad74a7cee4b541e302073d913236", + "sha256": "3654d2728b0c98919d61760e1802804ed616546a747f9167a93e17bb8697f320" + }, + { + "path": "upstream/build/figures/proof-map.tex", + "usage": "input", + "git_blob": "a2d539e5a794eb8d679c6cad68c6b8d12b0fc880", + "sha256": "76d4deacf07bea355412abcfd798c7cbe6dcccef29a4a420a9e2a7b158f23848" + }, + { + "path": "upstream/build/main.tex", + "usage": "input", + "git_blob": "0b11a3feb14714253c1ca06ee561a31dd2fe8662", + "sha256": "42f0f506976bc2084374a71e97edc1549689a7accf35dda4db2a18af4f13c1aa" + }, + { + "path": "upstream/build/references.bib", + "usage": "input", + "git_blob": "bf01cae12597f2777199c8ee74ee9f6933a1b56e", + "sha256": "33cc2df13ccf85330849e8fb34d4ac7613b23f625787457a5b7b9aa6d7369476" + }, + { + "path": "upstream/build/sections/00-introduction.tex", + "usage": "input", + "git_blob": "aa9048eef857c3e694989f5bb5020109e6422502", + "sha256": "98721f03682ccf1cc7d0850b07adabaa2d8f3afe552e3861753eba9d284d0da0" + }, + { + "path": "upstream/build/sections/01-history.tex", + "usage": "input", + "git_blob": "7c6f033138f97315c80e64afb6cc446a1d590538", + "sha256": "798956c8150c31e3e2f5f29c47110d25ce619faad1374f4d3a0f15fa3ee33ead" + }, + { + "path": "upstream/build/sections/02-streams.tex", + "usage": "input", + "git_blob": "088fceea1867abc76271d7efe7532b779fee9039", + "sha256": "606c80db61cad13aa0c3b6060dc4b88dbbe7ac60cdd831aa93f28d908fd09dab" + }, + { + "path": "upstream/build/sections/03-motifs.tex", + "usage": "input", + "git_blob": "cdb0ba527aa8df5d57c151183fd3893c1a7e21ab", + "sha256": "ed76761194988a01af77ead0ea6469cb5dcd29690ab985a0b5a4006b0f2b69bb" + }, + { + "path": "upstream/build/sections/04-swap.tex", + "usage": "input", + "git_blob": "951e792b1768e6509561380b8bbfb1d1ccb64c08", + "sha256": "412b170ccaab38dba96e95e3cbfae09f4876a9818f8d278776a746b0f8044906" + }, + { + "path": "upstream/build/sections/05-layers.tex", + "usage": "input", + "git_blob": "5ce8b3c83c455f221bb84858a97230b0285644aa", + "sha256": "20cfc8d12099d4e4ed9e3e7eeb6162edd9b6e0e076f24693364cd24377252594" + }, + { + "path": "upstream/build/sections/06-transforms.tex", + "usage": "input", + "git_blob": "de073e9292d58573f7065a3cd4f214e0d05f3444", + "sha256": "924316e4bc905066281d8f9e8746a49d8829aeb393688608deb1e61c3c87853c" + }, + { + "path": "upstream/build/sections/07-resampling.tex", + "usage": "input", + "git_blob": "256243bf9416baefb82bf9203f80215b9ebe28f2", + "sha256": "8a6b91670f9163afb54892489fa2210c77fe1b058f0325ec7d18b44b94be6e2c" + }, + { + "path": "upstream/build/sections/08-assembly.tex", + "usage": "input", + "git_blob": "337810a1d9a58a2ecf14123420923c039ba322a6", + "sha256": "763d7945b1e1ec4ebae9b799bcefcc45fa9bae6e2ffad799868a9c3d513dbd4a" + }, + { + "path": "upstream/build/sections/09-exact-arithmetic.tex", + "usage": "input", + "git_blob": "4c7a1d63c912d081f70f5b166e9cab92d7774ee6", + "sha256": "5714e5d0656c78c6a1fde8d01fd11f1ba856a7ea94149b283bd9a50fdbf516c3" + }, + { + "path": "upstream/build/sections/10-transposition.tex", + "usage": "input", + "git_blob": "e69cc8276220edb8617a371ae9044a911fbc0767", + "sha256": "c14ad8d56112f6578678a58211bc8d63c3a4b60e55078ac73bc38f7348e713cb" + }, + { + "path": "upstream/build/sections/11-grouped-rectangles.tex", + "usage": "input", + "git_blob": "44439c716c6290cd6e512ffac91253443b37d3ab", + "sha256": "6525cd0a01980e56accfeaf06e9d875bc699197ba42c6e22b69435e352275174" + }, + { + "path": "upstream/formalization.yaml", + "usage": "input", + "git_blob": "e0584d4993df01ec08233ab344ebc1b1039bf7f7", + "sha256": "2dcbd0d6e6a22475f53d49bfdfcac9b6d2b470653c332a9f56522f5be166edb9" + }, + { + "path": "upstream/manifest.json", + "usage": "input", + "git_blob": "01c309e34d36cf3669c43d89c5dfb25cdc31b8af", + "sha256": "16ab13971694cabab09440c47ebf2fc0496a9d35fc3af33950fda3498f8e2392" + } + ] +} diff --git a/research/finite-bit-rank-cache-seed87/TASK.json b/research/finite-bit-rank-cache-seed87/TASK.json new file mode 100644 index 0000000000..915bb714d0 --- /dev/null +++ b/research/finite-bit-rank-cache-seed87/TASK.json @@ -0,0 +1,62 @@ +{ + "schema_version": 1, + "task_id": "replay-runtime", + "priority_revision": 2, + "base_commit": "680967accfd4311f3241dc154e1f434869747b43", + "original_card": { + "id": "replay-runtime", + "question": "Can one measured replay bottleneck be sped up without dropping coverage?", + "starting_points": [ + "scripts/run_isolated_tests.py", + "scripts/verify_replay_coverage.py", + "certificates/selected-result.json" + ], + "methods": [ + "Profile one isolated replay and optimize the measured bottleneck.", + "Design source-bound reuse with explicit dependency invalidation and negative controls." + ], + "acceptance_gate": "Report before/after wall time on the same fixture, retained checks and invalidation behavior.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the selected reproduction command and choose a single replay stage for profiling.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Measure one unchanged fixture, preserve check coverage, and test one optimization with invalidation controls.", + "bottleneck_link": "Faster trustworthy replays increase review throughput and let mechanism candidates be checked sooner.", + "allowed_variations": [ + "Profile one stage or design one source-bound cache boundary." + ], + "scope_change_triggers": [ + "Skipping coverage or comparing different fixtures to claim speedup." + ], + "overlap_terms": [ + "replay runtime", + "cache invalidation", + "isolated tests" + ] + }, + "scope_status": "refined", + "actual_scope": "Avoid repeated rational matrix subtraction and hashing for identical ordered frame pairs within one inspect_candidate call, preserving complete exact receipts.", + "scope_change_reason": "OS seed 87 assigns verification engineering; measured existing finite-bit fixtures identify repeated transition construction as the chosen bottleneck.", + "bottleneck_link": "This historical exact checker serves finite-bit candidate audits. Reducing duplicate transition work improves review throughput without changing supplier or theorem assumptions.", + "budget_minutes": 40, + "assignment_seed": 87, + "stop_rule": "One source-pinned optimization; implementation stops by 03:27 UTC and handoff by 03:37 UTC on 2026-10-14. At most nine fresh-process benchmark pairs, no search for a better bound.", + "outcome": "completed", + "evidence": "verify.py compares all complete receipts, eleven rejection controls and between-call mutation; 53 existing tests per engine. BENCHMARK.json records alternating fresh-process same-input timings.", + "author": "Sagar Thakrar (thakrarsagar)", + "ai_assistance": "Substantial OpenAI Codex assistance with profiling, code, verification, analysis and writing. No independent human review claimed.", + "open_questions": [ + { + "question": "Should the retained finite-bit checker adopt this local cache?", + "why_it_matters": "Adoption would make repeated-frame audits faster without the opt-in loader.", + "first_step": "Review the nine-line replacement and rerun the same workload benchmark on Linux before any source-pin migration.", + "blocked_by": "Maintainer review and explicit migration of the six historical certificates that pin the current checker. Performance is workload dependent." + } + ] +} diff --git a/research/finite-bit-rank-cache-seed87/VERIFY.json b/research/finite-bit-rank-cache-seed87/VERIFY.json new file mode 100644 index 0000000000..8d685ea429 --- /dev/null +++ b/research/finite-bit-rank-cache-seed87/VERIFY.json @@ -0,0 +1,76 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "docs/research/fano-completion-audit.md", + "scripts/audit_cancellation.py", + "scripts/audit_cyclic_topology.py", + "scripts/audit_fano_completion.py", + "scripts/audit_fused_block.py", + "scripts/audit_joint_frames.py", + "scripts/audit_rank_product_core.py", + "scripts/audit_subset_cores.py", + "scripts/certify.py", + "scripts/exclusion_circuit.py", + "scripts/experiments/block_core.py", + "scripts/experiments/cube_core_family.py", + "scripts/experiments/fano_completion.py", + "scripts/experiments/fano_routing_witnesses.json", + "scripts/experiments/partial_routing.py", + "scripts/experiments/positive_side_core.py", + "scripts/experiments/rank_product_core.py", + "scripts/experiments/shared_core.py", + "scripts/experiments/signed_sparse_core.py", + "scripts/experiments/subset_core_family.py", + "scripts/finite_bit_contract.py", + "scripts/incidence_rectangles.py", + "scripts/paired_exclusion_circuit.py", + "scripts/paired_network.py", + "scripts/prepare_layers.py", + "scripts/rational_tensor.py", + "scripts/routing_smt.py", + "scripts/search_network.py", + "scripts/shared_point_circuit.py", + "scripts/shared_point_network.py", + "tests/test_block_core.py", + "tests/test_fano_completion.py", + "tests/test_finite_bit_contract.py", + "tests/test_positive_side_core.py", + "tests/test_rank_product_core.py", + "tests/test_shared_core.py", + "tests/test_subset_core_family.py", + "upstream/LICENSE", + "upstream/README.md", + "upstream/build/figures/multiplication-flow.tex", + "upstream/build/figures/proof-map.tex", + "upstream/build/main.tex", + "upstream/build/references.bib", + "upstream/build/sections/00-introduction.tex", + "upstream/build/sections/01-history.tex", + "upstream/build/sections/02-streams.tex", + "upstream/build/sections/03-motifs.tex", + "upstream/build/sections/04-swap.tex", + "upstream/build/sections/05-layers.tex", + "upstream/build/sections/06-transforms.tex", + "upstream/build/sections/07-resampling.tex", + "upstream/build/sections/08-assembly.tex", + "upstream/build/sections/09-exact-arithmetic.tex", + "upstream/build/sections/10-transposition.tex", + "upstream/build/sections/11-grouped-rectangles.tex", + "upstream/formalization.yaml", + "upstream/manifest.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Complete differential receipts on 34 fixtures and the full Fano audit, eleven rejection controls, mutation isolation and 53 existing tests per engine." + } + ] +} diff --git a/research/finite-bit-rank-cache-seed87/adapter.py b/research/finite-bit-rank-cache-seed87/adapter.py new file mode 100644 index 0000000000..5ec85a8322 --- /dev/null +++ b/research/finite-bit-rank-cache-seed87/adapter.py @@ -0,0 +1,42 @@ +"""Opt-in repeated-transition cache for the pinned finite-bit checker. + +Sagar Thakrar, with substantial OpenAI Codex assistance. Apache-2.0. +The loaded checker and its mathematics are Douglas R. Colkitt's retained work. +""" +from hashlib import sha256 +from pathlib import Path +import sys +from types import ModuleType + +ROOT = Path(__file__).resolve().parents[2] +SOURCE = ROOT / 'scripts/finite_bit_contract.py' +SOURCE_SHA256 = '3cff26a332cb6056f656b824e3a523fb8937d15206ddcc4118b911ac8df1b2a7' +BEFORE = ' costs = tuple(rank(sub(frames[v],frames[u])) for u,v,_ in edges)' +AFTER = ''' frame_ids = {} + ids = [frame_ids.setdefault(frame, len(frame_ids)) for frame in frames] + ranks = {} + costs = [] + for u,v,_ in edges: + key = (ids[u],ids[v]) + if key not in ranks: + ranks[key] = rank(sub(frames[v],frames[u])) + costs.append(ranks[key])''' + + +def checked_source(source, cached): + if sha256(source).hexdigest() != SOURCE_SHA256: + raise ValueError('finite-bit checker source drift') + text = source.decode('utf-8') + if text.count(BEFORE) != 1: + raise ValueError('expected exactly one edge-rank expression') + return text.replace(BEFORE, AFTER) if cached else text + + +def load_checker(cached): + """Load a separate module; leave files and other imported modules unchanged.""" + sys.path.insert(0, str(ROOT / 'scripts')) + module = ModuleType('finite_bit_contract') + module.__file__ = str(SOURCE) + exec(compile(checked_source(SOURCE.read_bytes(), cached), str(SOURCE), 'exec'), + module.__dict__) + return module diff --git a/research/finite-bit-rank-cache-seed87/verify.py b/research/finite-bit-rank-cache-seed87/verify.py new file mode 100644 index 0000000000..2fa96cab0d --- /dev/null +++ b/research/finite-bit-rank-cache-seed87/verify.py @@ -0,0 +1,199 @@ +#!/usr/bin/env python3 +"""Complete differential replay and bounded same-input performance experiment. + +Sagar Thakrar, with substantial OpenAI Codex assistance. Apache-2.0. +""" +import argparse +from copy import deepcopy +from fractions import Fraction as Q +from hashlib import sha256 +import json +import os +from pathlib import Path +import platform +import random +import statistics +import subprocess +import sys +import time +import unittest + +from adapter import ROOT, SOURCE, checked_source, load_checker + +PACKAGE = Path(__file__).resolve().parent +TESTS = ('finite_bit_contract', 'fano_completion', 'rank_product_core', + 'block_core', 'shared_core', 'subset_core_family', 'positive_side_core') + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(',', ':')).encode() + + +def fixtures(checker): + from audit_joint_frames import add, eye, matrix + from audit_rank_product_core import controls + from experiments.block_core import check_block_pair, compile_block + from experiments.fano_completion import cases + from experiments.rank_product_core import compile_core + from audit_cyclic_topology import cyclic_seed + + groups = {'fano': [], 'rank_product': [], 'block_core': [], 'rational': []} + for name, program in cases(): + groups['fano'].append((name, checker.zero_frame_candidate(program['W'], program['gates']))) + for name, rows, vectors, form in controls(): + groups['rank_product'].append((name, compile_core(rows, vectors, form)[0])) + for matching in (None, [1, 0]): + candidate, _ = compile_block(check_block_pair([3, 3], eye(4), 2), matching) + groups['block_core'].append((str(matching), candidate)) + rng = random.Random(87) + for m in (2, 3, 4, 8): + for count in (1, 3, 17): + candidate = checker.zero_frame_candidate(4, cyclic_seed(4, star=True), m) + bank = [matrix([[Q(rng.randrange(-3, 4), rng.randrange(1, 6)) + for _ in range(m)] for _ in range(m)]) for _ in range(count)] + candidate['source_frames'] = [bank[i % count] for i in range(4)] + for w, out in enumerate(candidate['rho']): + candidate['sink_frames'][out] = add(candidate['source_frames'][w], eye(m)) + for index, gate in enumerate(candidate['gates']): + gate['frame'] = bank[index % count] + groups['rational'].append((f'm{m}-bank{count}', candidate)) + return groups + + +def negative_controls(checker): + from audit_cyclic_topology import swap_word + from audit_joint_frames import eye + candidate = checker.zero_frame_candidate(3, swap_word(0, 1)) + initial = checker.inspect_candidate(candidate, False) + candidate['gates'][1]['frame'] = eye(2) + changed = checker.inspect_candidate(candidate, False) + require(changed['edge_ranks'] != initial['edge_ranks'], 'stale between-call frame cache') + candidate['gates'][1]['frame'] = ((0, 0), (0, 0)) + require(checker.inspect_candidate(candidate, False) == initial, 'cache survives restoration') + controls = [] + mutations = ( + ('endpoint', lambda c: c['sink_frames'].__setitem__(2, ((0, 0), (0, 0)))), + ('permutation', lambda c: c['rho'].__setitem__(0, 0)), + ('scalar', lambda c: c['gates'][0]['xors'].clear()), + ('float', lambda c: c['gates'][0].__setitem__('frame', ((0.0, 0), (0, 0)))), + ('dimension', lambda c: c['gates'][0].__setitem__('frame', ((0,),))), + ('gate port', lambda c: c['gates'][0].__setitem__('roles', [0, 0])), + ('missing terminal', lambda c: c['source_frames'].pop()), + ('zero denominator', lambda c: c['gates'][0].__setitem__('frame', (('1/0', 0), (0, 0)))), + ) + for name, mutate in mutations: + bad = deepcopy(candidate) + mutate(bad) + try: + checker.inspect_candidate(bad, False) + except (ValueError, ZeroDivisionError) as error: + controls.append([name, type(error).__name__, str(error)]) + else: + raise ValueError('accepted corruption: ' + name) + try: + checker.inspect_candidate(candidate) + except ValueError as error: + controls.append(['strict deficit', type(error).__name__, str(error)]) + else: + raise ValueError('accepted equality control as strict deficit') + for suffix in (b'\n', b' # changed source'): + try: + checked_source(SOURCE.read_bytes() + suffix, True) + except ValueError: + controls.append(['source pin', 'ValueError', 'source drift rejected']) + else: + raise ValueError('accepted source drift') + return {'rejections': controls, 'mutation_before': initial, 'mutation_after': changed} + + +def worker(engine, tests=False): + require(sys.flags.optimize == 0, 'worker requires enabled Python assertions') + checker = load_checker(engine == 'cached') + # Install before importing callers so their normal imports use this engine. + sys.modules['finite_bit_contract'] = checker + if tests: + suite = unittest.TestSuite() + for name in TESTS: + suite.addTests(unittest.defaultTestLoader.discover(str(ROOT / 'tests'), + pattern='test_' + name + '.py')) + result = unittest.TextTestRunner(verbosity=1).run(suite) + require(result.wasSuccessful(), 'existing tests failed') + return {'tests_run': result.testsRun} + groups = fixtures(checker) + receipts, seconds, rank_calls = {}, {}, {} + original_rank = checker.rank + for group, candidates in groups.items(): + original_rank.cache_clear() + started = time.perf_counter() + receipts[group] = [[name, checker.inspect_candidate(c, False)] for name, c in candidates] + seconds[group] = time.perf_counter() - started + info = original_rank.cache_info() + rank_calls[group] = {'calls': info.hits + info.misses, 'eliminations': info.misses} + from audit_fano_completion import certificate + original_rank.cache_clear() + started = time.perf_counter() + receipts['complete_fano_audit'] = certificate() + seconds['complete_fano_audit'] = time.perf_counter() - started + receipts['controls'] = negative_controls(checker) + return {'receipts': receipts, 'seconds': seconds, 'rank_calls': rank_calls} + + +def child(engine, tests=False): + argv = [sys.executable, '-B', str(Path(__file__).resolve()), '--worker', engine] + if tests: + argv.append('--tests') + environment = dict(os.environ, PYTHONHASHSEED='0', PYTHONOPTIMIZE='0') + process = subprocess.run(argv, cwd=ROOT, env=environment, text=True, + capture_output=True, timeout=300) + require(process.returncode == 0, process.stderr or process.stdout) + return json.loads(process.stdout) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--worker', choices=('reference', 'cached')) + parser.add_argument('--tests', action='store_true') + parser.add_argument('--pairs', type=int, default=1) + args = parser.parse_args() + if args.worker: + print(json.dumps(worker(args.worker, args.tests), sort_keys=True)) + return + require(1 <= args.pairs <= 9, 'use one to nine fresh-process pairs') + sources = json.loads((PACKAGE / 'SOURCES.json').read_text()) + for row in sources['files']: + if row['usage'] == 'input': + require(sha256((ROOT / row['path']).read_bytes()).hexdigest() == row['sha256'], + 'source drift: ' + row['path']) + pairs, expected = [], None + for index in range(args.pairs): + order = ('reference', 'cached') if index % 2 == 0 else ('cached', 'reference') + pair = {engine: child(engine) for engine in order} + require(pair['reference']['receipts'] == pair['cached']['receipts'], 'full receipt mismatch') + digest = sha256(canonical(pair['reference']['receipts'])).hexdigest() + if expected is None: + expected = digest + require(expected == digest, 'receipt changed between runs') + pairs.append({'order': order, **{engine: {k: v for k, v in pair[engine].items() + if k != 'receipts'} for engine in order}}) + tests = {engine: child(engine, True) for engine in ('reference', 'cached')} + require(tests['reference'] == tests['cached'], 'test coverage mismatch') + ratios = {} + for group in pairs[0]['reference']['seconds']: + old = statistics.median(p['reference']['seconds'][group] for p in pairs) + new = statistics.median(p['cached']['seconds'][group] for p in pairs) + ratios[group] = {'reference_median_seconds': old, 'cached_median_seconds': new, + 'speedup': old / new} + print(json.dumps({'status': 'PASS_FINITE_BIT_TRANSITION_CACHE', 'assignment_seed': 87, + 'python': sys.version, 'platform': platform.platform(), + 'receipt_sha256': expected, 'tests': tests, 'measurements': pairs, + 'medians': ratios, 'scope': 'Exact verifier tooling; no new kappa.'}, + indent=2, sort_keys=True)) + + +if __name__ == '__main__': + main()