From c28a38863964fb4e50704d59cb24840d5cd9949b Mon Sep 17 00:00:00 2001 From: woklerx <338878655+woklerx@users.noreply.github.com> Date: Tue, 13 Oct 2026 11:03:46 -0700 Subject: [PATCH] Speed up exact PR968 frame-pair enumeration without losing coverage --- .../BENCHMARK.json | 30 + .../CERTIFICATE.json | 694 ++++++++++++++++++ .../CLAIM.json | 28 + .../NOTICE.md | 18 + .../PR-BODY.md | 19 + .../PROOF.md | 54 ++ .../README.md | 49 ++ .../SOURCES.json | 8 + .../VALIDATION.md | 38 + .../fast.py | 44 ++ .../verify.py | 163 ++++ 11 files changed, 1145 insertions(+) create mode 100644 research/frame-pair-enumeration-fast-seed93/BENCHMARK.json create mode 100644 research/frame-pair-enumeration-fast-seed93/CERTIFICATE.json create mode 100644 research/frame-pair-enumeration-fast-seed93/CLAIM.json create mode 100644 research/frame-pair-enumeration-fast-seed93/NOTICE.md create mode 100644 research/frame-pair-enumeration-fast-seed93/PR-BODY.md create mode 100644 research/frame-pair-enumeration-fast-seed93/PROOF.md create mode 100644 research/frame-pair-enumeration-fast-seed93/README.md create mode 100644 research/frame-pair-enumeration-fast-seed93/SOURCES.json create mode 100644 research/frame-pair-enumeration-fast-seed93/VALIDATION.md create mode 100644 research/frame-pair-enumeration-fast-seed93/fast.py create mode 100644 research/frame-pair-enumeration-fast-seed93/verify.py diff --git a/research/frame-pair-enumeration-fast-seed93/BENCHMARK.json b/research/frame-pair-enumeration-fast-seed93/BENCHMARK.json new file mode 100644 index 0000000000..3660f1779d --- /dev/null +++ b/research/frame-pair-enumeration-fast-seed93/BENCHMARK.json @@ -0,0 +1,30 @@ +{ + "D_E_H_seconds": { + "candidate": 5.198546000057831, + "reference": 15.417732400004752, + "speedup": 2.965777815534043 + }, + "frames": 1260, + "median_seconds": { + "candidate": 1.3762801000848413, + "reference": 6.287578799994662 + }, + "median_speedup": 4.568531361898688, + "ordered_stream_sha256": "6d62428028c9e0c7b9c2402b4dd6362f0a4f343e643e5f632f70bf280d095275", + "platform": "Windows-11-10.0.26300-SP0", + "python": "3.14.5", + "repetitions": 3, + "seconds": { + "candidate": [ + 1.263736700057052, + 1.3762801000848413, + 1.4193533000070602 + ], + "reference": [ + 6.202400000067428, + 6.287578799994662, + 6.495049900026061 + ] + }, + "timing_scope": "Enumeration kernel only; unchanged downstream costs measured separately; no timing threshold determines correctness." +} diff --git a/research/frame-pair-enumeration-fast-seed93/CERTIFICATE.json b/research/frame-pair-enumeration-fast-seed93/CERTIFICATE.json new file mode 100644 index 0000000000..abad9120ea --- /dev/null +++ b/research/frame-pair-enumeration-fast-seed93/CERTIFICATE.json @@ -0,0 +1,694 @@ +{ + "base_commit": "abdc6a7002abdbcd9e21bfc5e1a795784deacfdf", + "coverage": { + "chain": { + "0": { + "cost": 72, + "exact": true, + "kind": "coordinate frame, 0 of its lines punctured", + "live": 120, + "live_rank": 8, + "lower_bound": 72, + "punctured": [], + "ratio": "3/5" + }, + "1": { + "cost": 71, + "exact": true, + "kind": "coordinate frame, 1 of its lines punctured", + "live": 119, + "live_rank": 8, + "lower_bound": 71, + "punctured": [ + 0 + ], + "ratio": "71/119" + }, + "2": { + "cost": 70, + "exact": true, + "kind": "coordinate frame, 2 of its lines punctured", + "live": 118, + "live_rank": 8, + "lower_bound": 70, + "punctured": [ + 0, + 1 + ], + "ratio": "35/59" + }, + "3": { + "cost": 69, + "exact": true, + "kind": "coordinate frame, 3 of its lines punctured", + "live": 117, + "live_rank": 8, + "lower_bound": 69, + "punctured": [ + 0, + 1, + 26 + ], + "ratio": "23/39" + }, + "4": { + "cost": 68, + "exact": true, + "kind": "coordinate frame, 4 of its lines punctured", + "live": 116, + "live_rank": 8, + "lower_bound": 68, + "punctured": [ + 0, + 1, + 26, + 27 + ], + "ratio": "17/29" + }, + "5": { + "cost": 67, + "exact": true, + "kind": "coordinate frame, 5 of its lines punctured", + "live": 115, + "live_rank": 8, + "lower_bound": 67, + "punctured": [ + 0, + 1, + 26, + 27, + 44 + ], + "ratio": "67/115" + }, + "6": { + "cost": 66, + "exact": true, + "kind": "coordinate frame, 6 of its lines punctured", + "live": 114, + "live_rank": 8, + "lower_bound": 66, + "punctured": [ + 0, + 1, + 26, + 27, + 44, + 45 + ], + "ratio": "11/19" + }, + "7": { + "cost": 65, + "exact": true, + "kind": "coordinate frame, 7 of its lines punctured", + "live": 113, + "live_rank": 8, + "lower_bound": 65, + "punctured": [ + 0, + 1, + 26, + 27, + 44, + 45, + 54 + ], + "ratio": "65/113" + }, + "8": { + "cost": 64, + "exact": true, + "kind": "coordinate frame, 8 of its lines punctured", + "live": 112, + "live_rank": 8, + "lower_bound": 64, + "punctured": [ + 0, + 1, + 26, + 27, + 44, + 45, + 54, + 55 + ], + "ratio": "4/7" + }, + "9": { + "cost": 63, + "exact": true, + "kind": "frame pair, 1 partner lines + 0 extra lines punctured", + "live": 111, + "live_rank": 8, + "lower_bound": 63, + "punctured": [ + 0, + 1, + 26, + 27, + 44, + 45, + 54, + 55, + 77 + ], + "ratio": "21/37" + }, + "10": { + "cost": 62, + "exact": true, + "kind": "frame pair, 2 partner lines + 0 extra lines punctured", + "live": 110, + "live_rank": 8, + "lower_bound": 62, + "punctured": [ + 0, + 1, + 26, + 27, + 44, + 45, + 54, + 55, + 77, + 107 + ], + "ratio": "31/55" + }, + "11": { + "cost": 61, + "exact": true, + "kind": "frame pair, 3 partner lines + 0 extra lines punctured", + "live": 109, + "live_rank": 8, + "lower_bound": 61, + "punctured": [ + 0, + 1, + 26, + 27, + 40, + 44, + 45, + 54, + 55, + 77, + 107 + ], + "ratio": "61/109" + }, + "12": { + "cost": 60, + "exact": true, + "kind": "frame pair, 4 partner lines + 0 extra lines punctured", + "live": 108, + "live_rank": 8, + "lower_bound": 60, + "punctured": [ + 0, + 1, + 26, + 27, + 40, + 44, + 45, + 52, + 54, + 55, + 77, + 107 + ], + "ratio": "5/9" + }, + "13": { + "cost": 59, + "exact": true, + "kind": "frame pair, 5 partner lines + 0 extra lines punctured", + "live": 107, + "live_rank": 8, + "lower_bound": 59, + "punctured": [ + 0, + 1, + 2, + 26, + 27, + 40, + 44, + 45, + 52, + 54, + 55, + 77, + 107 + ], + "ratio": "59/107" + }, + "14": { + "cost": 58, + "exact": true, + "kind": "frame pair, 6 partner lines + 0 extra lines punctured", + "live": 106, + "live_rank": 8, + "lower_bound": 58, + "punctured": [ + 0, + 1, + 2, + 18, + 26, + 27, + 40, + 44, + 45, + 52, + 54, + 55, + 77, + 107 + ], + "ratio": "29/53" + }, + "15": { + "cost": 57, + "exact": true, + "kind": "frame pair, 7 partner lines + 0 extra lines punctured", + "live": 105, + "live_rank": 8, + "lower_bound": 57, + "punctured": [ + 0, + 1, + 2, + 18, + 26, + 27, + 40, + 44, + 45, + 52, + 54, + 55, + 77, + 86, + 107 + ], + "ratio": "19/35" + }, + "16": { + "cost": 56, + "exact": true, + "kind": "frame pair, 8 partner lines + 0 extra lines punctured", + "live": 104, + "live_rank": 8, + "lower_bound": 56, + "punctured": [ + 0, + 1, + 2, + 18, + 26, + 27, + 40, + 44, + 45, + 52, + 54, + 55, + 77, + 86, + 107, + 112 + ], + "ratio": "7/13" + }, + "17": { + "cost": 56, + "exact": true, + "kind": "frame pair, 8 partner lines + 1 extra lines punctured", + "live": 103, + "live_rank": 8, + "lower_bound": 56, + "punctured": [ + 0, + 1, + 2, + 3, + 18, + 26, + 27, + 40, + 44, + 45, + 52, + 54, + 55, + 77, + 86, + 107, + 112 + ], + "ratio": "56/103" + }, + "18": { + "cost": 56, + "exact": true, + "kind": "frame pair, 8 partner lines + 2 extra lines punctured", + "live": 102, + "live_rank": 8, + "lower_bound": 56, + "punctured": [ + 0, + 1, + 2, + 3, + 4, + 18, + 26, + 27, + 40, + 44, + 45, + 52, + 54, + 55, + 77, + 86, + 107, + 112 + ], + "ratio": "28/51" + }, + "19": { + "cost": 56, + "exact": true, + "kind": "frame pair, 8 partner lines + 3 extra lines punctured", + "live": 101, + "live_rank": 8, + "lower_bound": 56, + "punctured": [ + 0, + 1, + 2, + 3, + 4, + 5, + 18, + 26, + 27, + 40, + 44, + 45, + 52, + 54, + 55, + 77, + 86, + 107, + 112 + ], + "ratio": "56/101" + }, + "20": { + "cost": 56, + "exact": true, + "kind": "frame pair, 8 partner lines + 4 extra lines punctured", + "live": 100, + "live_rank": 8, + "lower_bound": 56, + "punctured": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 18, + 26, + 27, + 40, + 44, + 45, + 52, + 54, + 55, + 77, + 86, + 107, + 112 + ], + "ratio": "14/25" + }, + "21": { + "cost": 56, + "exact": true, + "kind": "frame pair, 8 partner lines + 5 extra lines punctured", + "live": 99, + "live_rank": 8, + "lower_bound": 56, + "punctured": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 18, + 26, + 27, + 40, + 44, + 45, + 52, + 54, + 55, + 77, + 86, + 107, + 112 + ], + "ratio": "56/99" + }, + "22": { + "cost": 56, + "exact": true, + "kind": "frame pair, 8 partner lines + 6 extra lines punctured", + "live": 98, + "live_rank": 8, + "lower_bound": 56, + "punctured": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 18, + 26, + 27, + 40, + 44, + 45, + 52, + 54, + 55, + 77, + 86, + 107, + 112 + ], + "ratio": "4/7" + }, + "23": { + "cost": 56, + "exact": true, + "kind": "frame pair, 8 partner lines + 7 extra lines punctured", + "live": 97, + "live_rank": 8, + "lower_bound": 56, + "punctured": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 18, + 26, + 27, + 40, + 44, + 45, + 52, + 54, + 55, + 77, + 86, + 107, + 112 + ], + "ratio": "56/97" + }, + "24": { + "cost": 56, + "exact": true, + "kind": "frame pair, 8 partner lines + 8 extra lines punctured", + "live": 96, + "live_rank": 8, + "lower_bound": 56, + "punctured": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 18, + 26, + 27, + 40, + 44, + 45, + 52, + 54, + 55, + 77, + 86, + 107, + 112 + ], + "ratio": "7/12" + } + }, + "decoder_rank_checks": 7168, + "enumerations": 2520, + "example": { + "F1": [ + 2, + 18, + 40, + 52, + 77, + 86, + 107, + 112 + ], + "pairs": [ + [ + 0, + 77 + ], + [ + 1, + 107 + ], + [ + 26, + 40 + ], + [ + 44, + 52 + ], + [ + 2, + 27 + ], + [ + 18, + 45 + ], + [ + 86, + 54 + ], + [ + 112, + 55 + ] + ] + }, + "frames": 1260, + "histogram": [ + [ + 0, + 364 + ], + [ + 8, + 896 + ] + ], + "log": [ + "PASS D.frames | 1260 frames inside P112 (disjoint from the coordinate frame)", + "PASS D.census | solutions per frame: {0: 364, 8: 896}", + "PASS D.types | relative position (common F0-neighbours of F1 pairs) -> admissible: {'(True, ((0, 4), (2, 24)))': 896, '(False, ((0, 8), (2, 16), (4, 4)))': 336, '(False, ((0, 16), (4, 12)))': 28}", + "PASS D.exact-56 | 7168 frame-pair decoders built; every one satisfies A^T B = 2I and has eight cost-7 terms on its P104 (cst 56)", + "PASS D.full-exactness-crosscheck | one decoder rechecked entrywise: D T^T = 2G on all 104 x 104 live pairs", + "PASS E.chain | p=0..24: exact decoders with cst = max(72-p, 56) at every p (attaining the theorem)", + "PASS E.best-ratio | minimum copy ratio along the chain is 56/104 = 7/13 at p = 16 (P112: 64/112 = 4/7)", + "PASS H.mutated-decoder | adding a frame root to one column vector breaks D T^T = 2G", + "PASS H.self-line-live | restoring one self-line raises exactly one term to 8: cst 57 at p = 15", + "PASS H.even-pairs | coordinate (even, alpha = beta) decoder on the same P104 costs 64", + "PASS H.inadmissible | 364 frames of the two other relative types have no solution", + "PASS H.swapped-partners | swapping two column partners breaks duality or the odd pairing", + "PASS H.pi7-sharp | puncturing a 25-line codim-2 violator set leaves a root support with a 7-dim label span" + ], + "ordered_solution_stream_sha256": "20abf2679c4d08c2ec3de0b1aa8b703410eea38507e837ff4b92eaede3b6bd69", + "rank_stream_sha256": "92beaa1f5d8ed2ee9be473af43335844f60ea3fa36260d2475f6b7853b55e2b6", + "term_rank_checks": 57344, + "types": [ + [ + "(False, ((0, 16), (4, 12)))", + 28 + ], + [ + "(False, ((0, 8), (2, 16), (4, 4)))", + 336 + ], + [ + "(True, ((0, 4), (2, 24)))", + 896 + ] + ] + }, + "negative_controls": [ + "drop solution", + "reverse solution order", + "duplicate solution", + "swap partner", + "short frame", + "duplicate frame entry", + "overlapping frames", + "source byte mutation", + "missing source binding", + "source rejects nonintegral root pairing under optimized caller" + ], + "seed": 93, + "source_pins": { + "base_commit": "abdc6a7002abdbcd9e21bfc5e1a795784deacfdf", + "files": { + "research/complex-frame-pair-decoders/verify.py": "bdf7ee497dc04dfc634ee5b7848f6a2b39b0169668fb1a60a9715111dbd15395" + }, + "hash_convention": "SHA256 after CRLF to LF normalization; all other bytes retained", + "predecessor": "themilkman216 PR968, Apache-2.0; exact source split order and checks retained" + }, + "status": "PASS_FRAME_PAIR_FAST_S93" +} diff --git a/research/frame-pair-enumeration-fast-seed93/CLAIM.json b/research/frame-pair-enumeration-fast-seed93/CLAIM.json new file mode 100644 index 0000000000..fcd796f85a --- /dev/null +++ b/research/frame-pair-enumeration-fast-seed93/CLAIM.json @@ -0,0 +1,28 @@ +{ + "round": 19, + "batch_round": 9, + "seed": 93, + "track": "verification engineering", + "base_commit": "abdc6a7002abdbcd9e21bfc5e1a795784deacfdf", + "assignment": "Preassigned independent OS-random seed; no reroll", + "claim": "Replace repeated list neighborhood scans in PR968 frame-pair split enumeration with exact eight-bit masks, preserving all ordered results and downstream checks.", + "candidates": [ + "Chosen: full frame-pair split enumeration, exact ordered equivalence and bounded before/after measurement", + "Rejected: replacing bin(x).count with bit_count alone is too narrow a standalone contribution", + "Rejected: general dependency-DAG memoization overlaps existing PR1044 tooling" + ], + "coordination": "No pinned sprint issue at initial live issue check; claim recorded locally before implementation", + "coverage": "All1260 pinned second frames and256 splits each; all ordered solutions; unchanged D/E/H downstream checks", + "stopping_rule": "One fixed complete input, three alternating kernel benchmark pairs, one full paired scoped replay; no search expansion", + "live_overlap": [ + {"pr": 968, "relation": "Inherited algorithm and checks, original author credited"}, + {"pr": 1071, "relation": "Independent geometry and delivery lower bounds, not this enumeration representation"}, + {"pr": 1077, "relation": "Coefficient-field extension, not this performance result"}, + {"pr": 1075, "relation": "Different bounded quadratic-code replay kernel"}, + {"pr": 778, "relation": "Different single-intersection Gram replay kernel"}, + {"pr": 824, "relation": "Different stage-pair audit kernel"}, + {"pr": 1044, "relation": "General dependency-DAG tooling; not repeated here"} + ], + "selected": "PR942, conditional kappa1661960547713947/1000000000000000000, source ASSEMBLY and review followed", + "scope": "Optional exact enumeration tool; no new mathematical theorem, circuit, supplier adoption, selected change or kappa" +} diff --git a/research/frame-pair-enumeration-fast-seed93/NOTICE.md b/research/frame-pair-enumeration-fast-seed93/NOTICE.md new file mode 100644 index 0000000000..e43dad9df5 --- /dev/null +++ b/research/frame-pair-enumeration-fast-seed93/NOTICE.md @@ -0,0 +1,18 @@ +# Attribution and license + +This new package is Apache-2.0, following the repository license. +Prepared for @woklerx with substantial OpenAI Codex assistance in the +algorithm, proof, implementation, review and writing. Agent cross-review +is not independent human review. + +themilkman216's PR968 (`research/complex-frame-pair-decoders`) supplies the +original exact frame-pair search, E8 data and every inherited D/E/H check. +The new mask enumerator is an explicitly credited representation-level +rewrite of that search. Its ordered outputs are compared to the pinned +reference. Source files remain unchanged; no source license is replaced. + +JosieElliston's parallel PR1071 adds independent geometry and delivery +bounds for frame-pair centers. PR1077 extends the coefficient-field proof. +Neither is a dependency of this performance result, and no such mathematical +finding is claimed here. PR1075, PR778 and PR824 concern different exact +replay kernels. PR1044's dependency-DAG work is a separate optimization. diff --git a/research/frame-pair-enumeration-fast-seed93/PR-BODY.md b/research/frame-pair-enumeration-fast-seed93/PR-BODY.md new file mode 100644 index 0000000000..7d0bee88c0 --- /dev/null +++ b/research/frame-pair-enumeration-fast-seed93/PR-BODY.md @@ -0,0 +1,19 @@ +PR968 repeatedly scans eight-element neighborhood lists during its complete +frame-pair split census. An exact mask representation preserves the full +ordered solution stream and makes this kernel 4.57x faster in three paired +trials. A separate D/E/H replay is 2.97x faster on the recorded Windows run; +this is not a whole-repository timing claim. + +Both paths retain all 1,260 frames, 7,168 decoders, 57,344 term-rank checks, +25 attainment cases and six inherited controls. Ten additional controls +check source binding, malformed inputs, stream tampering and preservation +of source assertions under an optimized caller. The complete canonical +receipt matches; benchmark timing is excluded from mathematical equality. + +Reproduce: `python -I -O -B research/frame-pair-enumeration-fast-seed93/verify.py`. +Only this new package is added. Sections A/B/C/F/G, native suppliers and +the full theorem are outside this replay. No new kappa is claimed. + +Credit themilkman216's PR968 enumeration and proof checks; parallel PR1071 +and PR1077 address different mathematical questions. Prepared for @woklerx +with substantial OpenAI Codex assistance. Apache-2.0. diff --git a/research/frame-pair-enumeration-fast-seed93/PROOF.md b/research/frame-pair-enumeration-fast-seed93/PROOF.md new file mode 100644 index 0000000000..488320e96d --- /dev/null +++ b/research/frame-pair-enumeration-fast-seed93/PROOF.md @@ -0,0 +1,54 @@ +# Exact order-preserving enumeration + +The reference is themilkman216's PR968 `frame_pair_solutions`. We change +its representation of eight-element neighborhoods, not its search domain, +acceptance condition, multiplicity, or output ordering. Both ordered frames +must have eight distinct members and be disjoint. The consumed inner-product +matrix is the source's exact integer matrix on all 120 root lines. + +For a fixed selected subset S of the first frame, a second-frame member g +is a permitted partner of f in S exactly when its nonzero neighbors inside +S are the singleton {f}. Encoding those neighbors as an eight-bit integer +turns this condition into `hit != 0 and hit & (hit-1) == 0`. The sole bit +identifies f. Iterating g in its original frame order appends precisely the +reference partner list in precisely its original order. The outer subsets +still run from 0 through 255, and the same Cartesian product runs over f in +the original first-frame order. The injectivity check is retained. + +For each first choice, T is the complement of the chosen second-frame +members. A remaining first-frame member f is a permitted partner of g in T +exactly when its nonzero neighbors in T equal {g}. The reverse-neighborhood +mask tests this identical condition. Iterating remaining f in frame order +preserves every second partner list and therefore the second Cartesian +product's order. We retain its injectivity check and construct the same +ordered concatenation of pairs. Empty selected sets use the same empty +Cartesian-product convention. Thus every returned list, including empty +outputs, agrees exactly with the reference, not only up to permutation. + +The two adjacency directions are computed separately, so this equivalence +does not silently assume symmetry. Entries are tested for nonzeroness exactly +as in the reference. No sign, coefficient, rank, or downstream duality check +is replaced by a Boolean approximation. Masks only represent membership. + +The benchmark includes every one of the 1,260 second frames at the pinned +source, including all 364 without solutions. Both implementations return +the same complete ordered stream, containing 7,168 decoders. In the larger +replay, only the enumeration function is substituted. PR968 sections D, E +and H retain their source code: all 57,344 term-rank checks, all decoder +duality checks, the entrywise example, the 25 attaining puncture cases and +all six inherited controls run in both paths. The default checker compares +the complete proof-relevant output, including order-sensitive stream hashes, +rank-check inputs/results, every log line, all chain fields and census data. + +Source assertions are explicitly compiled with optimization level zero, +including when the wrapper runs under `python -O`; an actual nonintegral +pairing input checks this assertion boundary. Missing/changed source pins, +solution omission, duplication, reordering and partner mutation are rejected. +The receipt is compared canonically, with timings kept outside mathematical +equality. A fast machine or a timing fluctuation cannot change acceptance. + +This is a scoped enumeration optimization. Sections A/B/C/F/G, full supplier +verification and the multiplication theorem are not claimed as replayed here. +The source E8 matrix initialization and frame construction still run. No +finite census alone proves the universal decoder floor; PR968's proof and +classification premises are unchanged. diff --git a/research/frame-pair-enumeration-fast-seed93/README.md b/research/frame-pair-enumeration-fast-seed93/README.md new file mode 100644 index 0000000000..39c72a3333 --- /dev/null +++ b/research/frame-pair-enumeration-fast-seed93/README.md @@ -0,0 +1,49 @@ +# Faster exact frame-pair enumeration + +Precomputed eight-bit neighborhoods accelerate PR968's complete frame-split +search while preserving every ordered solution and its existing exact checks. +On the recorded Windows CPython run, the enumeration median is **4.57x faster**; +the larger D/E/H replay is **2.97x faster** in a separate single paired timing. +Timings depend on the machine and load; correctness has no timing threshold. +See [BENCHMARK.json](BENCHMARK.json) for all three alternating kernel trials, +environment details, raw seconds and the broader timing. + +The complete input has 1,260 second frames, 896 with eight solutions and +364 without solutions, yielding 7,168 exact decoders. The default verifier +runs both the pinned reference and candidate through unchanged source +sections D/E/H. It compares complete ordered solution streams, 57,344 exact +term ranks, every source check/log line, all 25 attainment cases and six +inherited rejection controls. Ten additional package controls pass, including +checking that source assertions survive an optimized caller. + +```sh +python -I -O -B research/frame-pair-enumeration-fast-seed93/verify.py +``` + +Expected: + +```text +PASS_FRAME_PAIR_FAST_S93 frames=1260 decoders=7168 term_ranks=57344 chain=25 inherited_controls=6 package_controls=10 +``` + +Python 3.10+ and the standard library suffice. `--benchmark` reruns three +alternating kernel trials and replaces only the local timing artifact; +`--record` deliberately regenerates the exact certificate. Default execution +does not rewrite either artifact. It compiles the pinned source in memory +with its assertions enabled, without editing the predecessor package. + +[PROOF.md](PROOF.md) gives the order-preservation argument. +[SOURCES.json](SOURCES.json) binds the exact consumed source after declared +CRLF normalization. [CERTIFICATE.json](CERTIFICATE.json) records all canonical +proof-relevant fields. The original selected construction is unchanged. + +This is an optional research wrapper, not installation into the upstream +verifier or a measured whole-repository speedup. We did not replay sections +A/B/C/F/G, native suppliers, hosted CI or the all-size multiplication theorem. +All PR968 mathematical assumptions and all selected supplier obligations +remain. No new circuit, lower bound or kappa is claimed. + +Prepared for @woklerx with substantial OpenAI Codex assistance. Apache-2.0. +Credit themilkman216 for PR968's exact enumeration and all inherited +geometric/rank checks. See [NOTICE.md](NOTICE.md), [CLAIM.json](CLAIM.json) +and [VALIDATION.md](VALIDATION.md). diff --git a/research/frame-pair-enumeration-fast-seed93/SOURCES.json b/research/frame-pair-enumeration-fast-seed93/SOURCES.json new file mode 100644 index 0000000000..724455078e --- /dev/null +++ b/research/frame-pair-enumeration-fast-seed93/SOURCES.json @@ -0,0 +1,8 @@ +{ + "base_commit": "abdc6a7002abdbcd9e21bfc5e1a795784deacfdf", + "files": { + "research/complex-frame-pair-decoders/verify.py": "bdf7ee497dc04dfc634ee5b7848f6a2b39b0169668fb1a60a9715111dbd15395" + }, + "hash_convention": "SHA256 after CRLF to LF normalization; all other bytes retained", + "predecessor": "themilkman216 PR968, Apache-2.0; exact source split order and checks retained" +} diff --git a/research/frame-pair-enumeration-fast-seed93/VALIDATION.md b/research/frame-pair-enumeration-fast-seed93/VALIDATION.md new file mode 100644 index 0000000000..7a66c96411 --- /dev/null +++ b/research/frame-pair-enumeration-fast-seed93/VALIDATION.md @@ -0,0 +1,38 @@ +# Validation + +The first bounded pilot matched all ordered solutions and measured a3.58x +enumeration gain and2.20x section-D gain. The final implementation also +precomputes reverse neighborhoods and does not assume matrix symmetry. +The initial package-control fixture mistakenly chose an inadmissible first +frame; it failed explicitly before receipt recording. The control now selects +the first admissible reference frame and checks that it has eight solutions. +The first saved-receipt comparison exposed integer versus string JSON-key +sorting in the chain dictionary. Canonicalization now converts keys to JSON +strings before sorting; the existing receipt is replayed without regeneration. + +Final isolated optimized recording and benchmark passed: + +```text +python -I -O -B research/frame-pair-enumeration-fast-seed93/verify.py --record --benchmark +PASS_FRAME_PAIR_FAST_S93 frames=1260 decoders=7168 term_ranks=57344 chain=25 inherited_controls=6 package_controls=10 +``` + +The three kernel trials alternate execution order, compare complete ordered +stream digests each time, and use identical frame inputs. BENCHMARK.json +contains raw timings and environment details. D/E/H timing includes full +source checks and instrumentation, but excludes module loading and final +canonical serialization; the kernel timing excludes frame generation and +hash computation. These scopes are explicit, not whole-command timings. + +No native toolchain, hosted CI or full repository suite was run. The package +does not edit a generator, selected construction or predecessor source, so +its scoped exact replay is the relevant check. Publication and acceptance +remain separate from these local results. + +After the key-normalization correction, default isolated optimized replay +passed against the existing certificate without regeneration. The repository's +`python -I -B scripts/verify_selected_result.py` passed with exact unchanged +kappa1661960547713947/1000000000000000000. A separate agent compared the mask +algorithm and all D/E/H coverage to the pinned reference and found no additional +ordering, mathematical or benchmark issue. This is agent review, not human +peer review. diff --git a/research/frame-pair-enumeration-fast-seed93/fast.py b/research/frame-pair-enumeration-fast-seed93/fast.py new file mode 100644 index 0000000000..cba829092c --- /dev/null +++ b/research/frame-pair-enumeration-fast-seed93/fast.py @@ -0,0 +1,44 @@ +"""Order-preserving mask enumeration of PR968's eight-by-eight frame splits. + +Prepared for @woklerx with substantial OpenAI Codex assistance. Apache-2.0. +The exact search and output order are inherited from themilkman216's PR968. +""" +from itertools import product + + +def frame_pair_solutions(F0, F1, ip): + if len(F0) != 8 or len(F1) != 8 or len(set(F0 + F1)) != 16: + raise ValueError('two disjoint ordered eight-element frames required') + neighbors = [sum(bool(ip[g][f]) << j for j, f in enumerate(F0)) for g in F1] + reverse_neighbors = [sum(bool(ip[f][g]) << j for j, g in enumerate(F1)) for f in F0] + output = [] + for selected in range(256): + left = [j for j in range(8) if selected >> j & 1] + partners = [[] for _ in range(8)] + for g, adjacent in enumerate(neighbors): + hit = adjacent & selected + if hit and hit & (hit - 1) == 0: + partners[hit.bit_length() - 1].append(g) + if any(not partners[f] for f in left): + continue + for choice in product(*(partners[f] for f in left)): + # Retain the reference's injectivity guard even though singleton + # neighborhoods already partition these first-partner lists. + if len(set(choice)) != len(left): + continue + chosen = sum(1 << g for g in choice) + right = [g for g in range(8) if not chosen >> g & 1] + remainder = [f for f in range(8) if not selected >> f & 1] + second = [[] for _ in range(8)] + for f in remainder: + hit = reverse_neighbors[f] & (255 ^ chosen) + if hit and hit & (hit - 1) == 0: + second[hit.bit_length() - 1].append(f) + if any(not second[g] for g in right): + continue + for choice2 in product(*(second[g] for g in right)): + if len(set(choice2)) != len(right): + continue + output.append([(F0[f], F1[g]) for f, g in zip(left, choice)] + + [(F1[g], F0[f]) for g, f in zip(right, choice2)]) + return output diff --git a/research/frame-pair-enumeration-fast-seed93/verify.py b/research/frame-pair-enumeration-fast-seed93/verify.py new file mode 100644 index 0000000000..3a778d993c --- /dev/null +++ b/research/frame-pair-enumeration-fast-seed93/verify.py @@ -0,0 +1,163 @@ +"""Replay the complete PR968 D/E/H coverage with both exact enumerators. + +Prepared for @woklerx with substantial OpenAI Codex assistance. Apache-2.0. +""" +import argparse +import contextlib +import copy +import hashlib +import importlib.util +import io +import json +from pathlib import Path +import platform +import statistics +import time +import types + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +REL = 'research/complex-frame-pair-decoders/verify.py' +BASE = 'abdc6a7002abdbcd9e21bfc5e1a795784deacfdf' +spec = importlib.util.spec_from_file_location('mask_enumerator', HERE/'fast.py') +fast = importlib.util.module_from_spec(spec); spec.loader.exec_module(fast) + + +def need(ok, why): + if not ok: raise ValueError(why) + + +def canonical(obj): + # JSON object keys are strings. Normalize runtime integer keys before + # sorting, so saved and live chain dictionaries use the same order. + return json.dumps(json.loads(json.dumps(obj, allow_nan=False)), + sort_keys=True, separators=(',', ':'), allow_nan=False) + + +def digest(obj): return hashlib.sha256(canonical(obj).encode()).hexdigest() + + +def check_pins(pins): + need(pins['base_commit'] == BASE and set(pins['files']) == {REL}, 'source inventory') + for rel, expected in pins['files'].items(): + raw = (ROOT/rel).read_bytes().replace(b'\r\n', b'\n') + need(hashlib.sha256(raw).hexdigest() == expected, 'source digest') + + +def source(): + # PR968 relies on assertions. Explicit optimize=0 preserves them even if + # this wrapper is launched with -O; no predecessor file is changed. + module = types.ModuleType('pinned_pr968') + module.__file__ = str(ROOT/REL) + exec(compile((ROOT/REL).read_bytes(), str(ROOT/REL), 'exec', optimize=0), module.__dict__) + return module + + +def scoped_replay(use_fast): + m = source() + reference = m.frame_pair_solutions + stream = [] + rank_records = [] + original_pair = m.pair_decoder + def enumerate_pairs(a, b): + result = fast.frame_pair_solutions(a, b, m.IP) if use_fast else reference(a, b) + stream.append([a, b, result]) + return result + def pair_check(pairs, live): + answer = original_pair(pairs, live) + rank_records.append([pairs, live, answer]) + return answer + m.frame_pair_solutions = enumerate_pairs + m.pair_decoder = pair_check + capture = io.StringIO() + start = time.perf_counter() + with contextlib.redirect_stdout(capture): + frames, example, hist, kinds = m.section_d() + chain = m.section_e(frames, example) + m.section_h(example, frames, hist) + elapsed = time.perf_counter() - start + need(not m.FAILS, 'predecessor checks failed: '+str(m.FAILS)) + need(len(frames) == 1260 and len(stream) == 2520 and len(rank_records) == 7168, + 'complete D and H enumeration/rank coverage') + receipt = {'frames': len(frames), 'enumerations': len(stream), 'decoder_rank_checks': len(rank_records), + 'term_rank_checks': sum(len(record[2][1]) for record in rank_records), + 'ordered_solution_stream_sha256': digest(stream), 'rank_stream_sha256': digest(rank_records), + 'histogram': sorted(hist.items()), 'types': sorted((str(k), v) for k,v in kinds.items()), + 'example': example, 'chain': chain, 'log': capture.getvalue().splitlines()} + return receipt, elapsed + + +def controls(): + m = source(); a = list(m.FRAME0) + frame = next(list(f) for f in m.frames_in(m.P112) if m.frame_pair_solutions(a,list(f))) + expected = m.frame_pair_solutions(a, frame) + need(len(expected) == 8, 'control fixture must be admissible') + passed = [] + def rejected(name, fn): + try: fn() + except ValueError: passed.append(name) + else: raise ValueError('control accepted: '+name) + for name, changed in [('drop solution', expected[:-1]), ('reverse solution order', expected[::-1]), + ('duplicate solution', expected + expected[:1])]: + rejected(name, lambda changed=changed: need(changed == expected, 'full ordered stream mismatch')) + changed = copy.deepcopy(expected); changed[0][0] = (changed[0][0][0], changed[0][1][1]) + rejected('swap partner', lambda: need(changed == expected, 'partner mismatch')) + for name, left, right in [('short frame', a[:-1], frame), ('duplicate frame entry', a, frame[:-1]+frame[:1]), + ('overlapping frames', a, a)]: + rejected(name, lambda left=left,right=right: fast.frame_pair_solutions(left,right,m.IP)) + pins = json.loads((HERE/'SOURCES.json').read_text()) + changed = copy.deepcopy(pins); changed['files'][REL] = '0'*64 + rejected('source byte mutation', lambda: check_pins(changed)) + changed = copy.deepcopy(pins); changed['files'] = {} + rejected('missing source binding', lambda: check_pins(changed)) + # Exercise an actual predecessor assertion under this caller's flags. + try: m.ip((1,), (1,)) + except AssertionError: passed.append('source rejects nonintegral root pairing under optimized caller') + else: raise ValueError('source assertions were disabled') + return passed + + +def benchmark(): + m = source(); frames = m.frames_in(m.P112) + timings = {'reference': [], 'candidate': []}; output_hash = None + for repetition in range(3): + # Alternate to reduce fixed-order warmup bias; every run consumes the + # identical ordered 1260-frame input, including 364 empty outputs. + order = ('reference','candidate') if repetition % 2 == 0 else ('candidate','reference') + for kind in order: + start = time.perf_counter() + if kind == 'reference': outputs = [m.frame_pair_solutions(m.FRAME0,list(f)) for f in frames] + else: outputs = [fast.frame_pair_solutions(m.FRAME0,list(f),m.IP) for f in frames] + timings[kind].append(time.perf_counter()-start) + h = digest(outputs) + if output_hash is None: output_hash = h + need(h == output_hash, 'benchmark changed complete ordered stream') + medians = {k:statistics.median(v) for k,v in timings.items()} + return {'python': platform.python_version(), 'platform': platform.platform(), 'frames': len(frames), + 'repetitions': 3, 'seconds': timings, 'median_seconds': medians, + 'median_speedup': medians['reference']/medians['candidate'], 'ordered_stream_sha256': output_hash, + 'timing_scope': 'Enumeration kernel only; unchanged downstream costs measured separately; no timing threshold determines correctness.'} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--record', action='store_true') + parser.add_argument('--benchmark', action='store_true') + args = parser.parse_args() + need(canonical({1:'a',2:'b',10:'c'}) == canonical({'1':'a','2':'b','10':'c'}), + 'JSON key normalization') + pins = json.loads((HERE/'SOURCES.json').read_text()); check_pins(pins) + before, bt = scoped_replay(False); after, at = scoped_replay(True) + need(canonical(before) == canonical(after), 'complete D/E/H proof-relevant receipt mismatch') + receipt = {'status':'PASS_FRAME_PAIR_FAST_S93', 'base_commit':BASE, 'seed':93, + 'source_pins':pins, 'coverage':after, 'negative_controls':controls()} + if args.record: (HERE/'CERTIFICATE.json').write_text(json.dumps(receipt,indent=2,sort_keys=True)+'\n') + else: need(canonical(receipt) == canonical(json.loads((HERE/'CERTIFICATE.json').read_text())), 'saved certificate mismatch') + if args.benchmark: + bench = benchmark(); bench['D_E_H_seconds'] = {'reference':bt,'candidate':at,'speedup':bt/at} + (HERE/'BENCHMARK.json').write_text(json.dumps(bench,indent=2,sort_keys=True)+'\n') + print('BENCHMARK enumeration median speedup',bench['median_speedup'],'D/E/H',bt/at) + print('PASS_FRAME_PAIR_FAST_S93 frames=1260 decoders=7168 term_ranks=57344 chain=25 inherited_controls=6 package_controls='+str(len(receipt['negative_controls']))) + + +if __name__ == '__main__': main()