diff --git a/research/x4-precondition-seed22/CLAIM.md b/research/x4-precondition-seed22/CLAIM.md new file mode 100644 index 0000000000..0be6c44328 --- /dev/null +++ b/research/x4-precondition-seed22/CLAIM.md @@ -0,0 +1,12 @@ +# Local sprint claim + +- Track: Complex supplier; OS-random assignment seed: 22. +- Base commit: f567884aeb8851b6e794af1184119a3bfbe1e631. +- Started: 2026-10-13 09:13 UTC. Target finish: 09:53 UTC (11:53 Europe/Berlin); reserve final 10 minutes for review and handoff. +- Scope: exact dyadic 2x2 factorization of selected PR799 X4 zero-frame precondition blocks, including backward dual, precise primitive cost, source/frame guards, prefix precision accounting, and corruption controls. No new kappa claim; selected record unchanged. +- Method: finite block census; algebraic factorization plus independent exact matrix enumeration/replay. No extra helper or source access is free. +- Expected deliverable: focused standalone research package with reproduction script, exact result certificate, proof note and attribution; at most one PR. +- Coordination: GitHub pinnedIssues queried 2026-10-13 ~09:15 UTC: no pinned issues. Claim kept local per task instructions. 669 open PRs inspected by metadata, focused overlap checked against #750, #837, #840 and coefficient-sharing work. +- Three candidates, zero-based order: (0) common-target cleanup coefficient routes [closer to #830]; (1) selected X4 zero-frame precondition pair factorization [chosen]; (2) precision-constrained CK signed route search [closer to #860/#866]. +- Diversification: seed 22 selects complex supplier; seed modulo three selects candidate 1 in this order; validation/mutation traversal starts at pair 22 modulo pair count. +- Pre-submission refresh at 09:32 UTC: main is still the exact base; latest 100 open PRs through #880 screened, following the initial full 669-PR snapshot through #876. New #877-#880 address cyclic precision, bit boundaries, physical transform layouts and bit schedules, not these pair factors. No pinned coordination issue exists. No pending code is imported. diff --git a/research/x4-precondition-seed22/INDEPENDENT.json b/research/x4-precondition-seed22/INDEPENDENT.json new file mode 100644 index 0000000000..aadd5533e1 --- /dev/null +++ b/research/x4-precondition-seed22/INDEPENDENT.json @@ -0,0 +1,419 @@ +{ + "archive": { + "archive_sha256": "70dfdfcf2ff95352c6020ee9dfca6dca9032b33c10daed3f3dc574c014f4e2cb", + "distinct_registers": 112, + "member_sha256": { + "native/local/CANONICAL-WORD.json.gz": "f1c2ede9276d4447c5857d0e9d32adb52f987b8adb643b45bde2c172d88c6ee9", + "native/local/LOCAL-PROGRAMS.json.gz": "ce194f8465079db575a9ce17ccee1396fa4de0210e2817da2525f95f4f93ebde" + }, + "pair_count": 56, + "pairs": [ + [ + 119, + 169 + ], + [ + 139, + 112 + ], + [ + 193, + 204 + ], + [ + 199, + 188 + ], + [ + 122, + 174 + ], + [ + 203, + 182 + ], + [ + 123, + 175 + ], + [ + 202, + 183 + ], + [ + 191, + 206 + ], + [ + 201, + 184 + ], + [ + 121, + 173 + ], + [ + 137, + 114 + ], + [ + 150, + 129 + ], + [ + 143, + 124 + ], + [ + 189, + 215 + ], + [ + 168, + 212 + ], + [ + 131, + 152 + ], + [ + 167, + 213 + ], + [ + 151, + 130 + ], + [ + 214, + 166 + ], + [ + 136, + 219 + ], + [ + 197, + 210 + ], + [ + 147, + 157 + ], + [ + 144, + 160 + ], + [ + 221, + 134 + ], + [ + 145, + 161 + ], + [ + 135, + 220 + ], + [ + 162, + 146 + ], + [ + 140, + 170 + ], + [ + 113, + 118 + ], + [ + 198, + 205 + ], + [ + 187, + 194 + ], + [ + 172, + 142 + ], + [ + 186, + 195 + ], + [ + 141, + 171 + ], + [ + 196, + 185 + ], + [ + 178, + 207 + ], + [ + 200, + 192 + ], + [ + 138, + 120 + ], + [ + 115, + 179 + ], + [ + 209, + 176 + ], + [ + 116, + 180 + ], + [ + 177, + 208 + ], + [ + 181, + 117 + ], + [ + 217, + 154 + ], + [ + 165, + 127 + ], + [ + 218, + 153 + ], + [ + 164, + 126 + ], + [ + 156, + 128 + ], + [ + 163, + 125 + ], + [ + 216, + 155 + ], + [ + 211, + 190 + ], + [ + 158, + 132 + ], + [ + 223, + 148 + ], + [ + 222, + 149 + ], + [ + 159, + 133 + ] + ] + }, + "bfs": { + "frontier_sizes": [ + 1, + 10, + 69, + 370, + 1646 + ], + "original_gatewise_minimum_lengths": { + "backward": [ + 2, + 3, + 1 + ], + "forward": [ + 2, + 3, + 1 + ] + } + }, + "candidate_backward": { + "maximum_absolute_reduced_numerator": 2, + "maximum_reduced_denominator": 1, + "peak_row_l1": "2", + "prefix_matrices": [ + [ + "1", + "0", + "0", + "1" + ], + [ + "1", + "0", + "1", + "1" + ], + [ + "-1", + "0", + "1", + "1" + ], + [ + "-2", + "0", + "1", + "1" + ], + [ + "-1", + "1", + "1", + "1" + ] + ] + }, + "candidate_forward": { + "maximum_absolute_reduced_numerator": 1, + "maximum_reduced_denominator": 2, + "peak_row_l1": "2", + "prefix_matrices": [ + [ + "1", + "0", + "0", + "1" + ], + [ + "1", + "-1", + "0", + "1" + ], + [ + "-1", + "1", + "0", + "1" + ], + [ + "-1/2", + "1/2", + "0", + "1" + ], + [ + "-1/2", + "1/2", + "1/2", + "1/2" + ] + ] + }, + "exhaustive": { + "shortest_word_counts": { + "backward": 8, + "forward": 8 + }, + "words_examined_by_length": [ + 1, + 10, + 100, + 1000, + 10000 + ] + }, + "limitation": "No assertion of global-circuit optimality, global guard acceptance, or a new kappa bound.", + "minimum_primitive_counts": { + "forward": 4, + "inverse_transpose_backward": 4 + }, + "negative_controls_rejected": [ + "omitted NEG", + "wrong first ADD sign", + "false forward row-l1 guard <= 1" + ], + "original_rational_backward": { + "maximum_absolute_reduced_numerator": 2, + "maximum_reduced_denominator": 1, + "peak_row_l1": "2", + "prefix_matrices": [ + [ + "1", + "0", + "0", + "1" + ], + [ + "-2", + "0", + "0", + "1" + ], + [ + "-2", + "0", + "1", + "1" + ], + [ + "-1", + "1", + "1", + "1" + ] + ] + }, + "original_rational_forward": { + "maximum_absolute_reduced_numerator": 1, + "maximum_reduced_denominator": 2, + "peak_row_l1": "1", + "prefix_matrices": [ + [ + "1", + "0", + "0", + "1" + ], + [ + "-1/2", + "0", + "0", + "1" + ], + [ + "-1/2", + "1/2", + "0", + "1" + ], + [ + "-1/2", + "1/2", + "1/2", + "1/2" + ] + ] + }, + "scope": "isolated two-register pair; ADD(+/-1), NEG, HALF, DOUBLE; unit cost; no scratch or swap", + "status": "PASS" +} diff --git a/research/x4-precondition-seed22/PAIR-PROOF.md b/research/x4-precondition-seed22/PAIR-PROOF.md new file mode 100644 index 0000000000..c83af0fb1b --- /dev/null +++ b/research/x4-precondition-seed22/PAIR-PROOF.md @@ -0,0 +1,114 @@ +# Isolated X4 pair: algebra, primitive minimum, and local prefix guard + +This claim concerns exactly two scalar registers, with no scratch register, +no free permutation, and unit cost for each of the ten instructions +`x += y`, `x -= y`, `y += x`, `y -= x`, and `NEG`, `HALF`, `DOUBLE` on either +register. It does not establish optimality of the full PR799 circuit or any +new multiplication bound. Source: base `f567884aeb8851b6e794af1184119a3bfbe1e631`, +the two pinned `native/local` JSON members of +`research/community-frontier799-audit/integrated799-replay.tar.gz`. + +## Exact map and replacement + +For an input column `(u,v)`, the archived forward triple is + +``` +x *= -1/2; x += y/2; y -= x. +``` + +It produces `((-u+v)/2, (u+v)/2)`, hence + +``` +A = (1/2) [-1 1] A^(-T) = B = [-1 1]. + [ 1 1] [ 1 1] +``` + +The replacement forward primitive word is + +``` +x -= y; NEG x; HALF x; y -= x. +``` + +Its four intermediate states are `(u-v,v)`, `(-u+v,v)`, +`((-u+v)/2,v)`, and `((-u+v)/2,(u+v)/2)`. + +The letterwise inverse-transpose word, in the same chronological order, is + +``` +y += x; NEG x; DOUBLE x; x += y. +``` + +It produces `(u,u+v)`, `(-u,u+v)`, `(-2u,u+v)`, and `(-u+v,u+v)`. +The archived backward triple `x *= -2; y -= x/2; x += y` has this same map. +Indeed `(G_n ... G_1)^(-T) = G_n^(-T) ... G_1^(-T)`; this explains why +letterwise inverse transposition preserves chronological order here. + +## Four primitives are necessary + +The determinant of `A` is `-1/2`; that of `B` is `-2`. In the declared +alphabet, an ADD has determinant `1`, NEG has determinant `-1`, HALF has +determinant `1/2`, and DOUBLE has determinant `2`. Each target therefore +requires at least one NEG and at least one HALF or DOUBLE. These are two +distinct diagonal instructions. Starting from the identity, a word with +at most one ADD and arbitrarily many diagonal instructions has at most +three nonzero matrix entries. Both target matrices have four nonzero +entries, so each also requires at least two ADDs. The lower bound is four, +attained by the words above. The argument does not presume a finite search +cutoff, but its scope remains exactly this two-register alphabet. + +The independent checker cross-checks that argument in exact `Fraction` +arithmetic. BFS has first-seen frontier sizes `1,10,69,370,1646` at depths +0 through 4. Both targets first occur at depth 4. Independently enumerating +all `1+10+100+1000+10000 = 11111` words through length 4 finds exactly eight +shortest words for each target. There is no coefficient-size pruning. + +For comparison, compiling the three original rational instructions +independently costs at least `2+3+1 = 6` primitives per scalar pair, in +either direction. A signed half/double needs the corresponding scale +and NEG. A half-ADD needs at least one HALF to introduce a fraction, +at least one DOUBLE to restore determinant one, and at least one ADD; +`HALF source; ADD destination, source; DOUBLE source` attains three. +The last unit ADD costs one. BFS independently confirms these minima. +Thus the fused word saves two primitives per scalar pair against that +specific gatewise baseline. For 56 disjoint scalar pairs this is 112 +per orientation; applying the same words separately to real and imaginary +coordinates doubles both counts. This comparison is not a lower bound +for other whole-block implementations. + +## Prefix and fraction guard + +The guard here is the maximum absolute row sum of the matrix mapping the +two input registers to any intermediate state, including the input. + +| Map and word | Maximum row sum | Maximum reduced denominator | +|---|---:|---:| +| Original rational forward | 1 | 2 | +| Fused primitive forward | 2 | 2 | +| Original rational backward | 2 | 1 | +| Fused primitive backward | 2 | 1 | + +Every one of the eight shortest forward words has peak row sum 2 and +maximum denominator 2; every shortest backward word has peak row sum 2 +and integer matrix entries. Thus a four-instruction replacement cannot +retain a local forward row-sum guard of 1. For example `(u,v)=(1,-1)` +already gives `x=2` after the first replacement instruction. + +For arbitrary entry row vectors `u,v` with individual row sums at most +`M`, the displayed words have intermediate row sums at most `2M`. +If all entry coefficients have common denominator `D`, all forward +prefix denominators divide `2D`; all backward prefix denominators divide +`D`. These are local bounds; a global guard must be checked against the +actual entry state and all unchanged circuit phases. + +## Reproduction and source checks + +Run `python3 research/x4-precondition-seed22/independent_checker.py` from +the repository root (or run the script by absolute path). The checker +uses only the Python standard library and imports no integration code. +It verifies the archive SHA-256, both compressed member hashes, the exact +56 original pair triples, their 112 distinct registers, and the matching +first 168 scalar instructions in both archived programs. It then checks +the algebra, duality, exhaustive minima, all shortest-word local guards, +and three negative controls: missing NEG, wrong first ADD sign, and the +false forward prefix guard of 1. Its JSON result is `PASS` on the pinned +source; malformed or changed source data is rejected. diff --git a/research/x4-precondition-seed22/README.md b/research/x4-precondition-seed22/README.md new file mode 100644 index 0000000000..e1c3ec255f --- /dev/null +++ b/research/x4-precondition-seed22/README.md @@ -0,0 +1,159 @@ +# Four-primitive X4 precondition pairs (no new kappa) + +The 56 disjoint zero-frame target pairs at the start of the selected PR799 +X4 complex program each admit a four-primitive implementation, in both +orientations. This replaces the retained emitter's eleven primitives per +real component and saves **784 real-component primitives per orientation**. +Against optimal *separate* compilation of the three old macros in the stated +two-register alphabet (six primitives), fusion still saves **224** per orientation. + +This is a finite scalar circuit construction and a scoped optimality result. +It changes only this research package. The selected construction, certificates, +production emitter, paid recursive profile, and conditional +`kappa = 0.001661634653669567` remain unchanged. + +## Reproduce + +From the repository root, using only Python 3.9+ and its standard library: + +```sh +python3 -B research/x4-precondition-seed22/check.py +``` + +Expected final line: `PASS_X4_PRECONDITION_PACKAGE no_new_kappa`. +The command checks both exact certificates, the full forward/backward scalar +programs, the independent pair proof/search, and seven source/interface tests. +It writes no repository files. `-I -O` also works. The frozen source archive +already exists in the repository; there is no download or solver dependency. + +## Construction and accounting + +Writing the two original registers as `(x,y)`, the forward triple is +`x *= -1/2; x += y/2; y -= x`. It maps `(u,v)` to +`((-u+v)/2,(u+v)/2)`. Replace it with: + +```text +x -= y; NEG x; HALF x; y -= x. +``` + +The backward triple computes the inverse transpose: `(u,v) -> (-u+v,u+v)`. +Our integration replay uses: + +```text +x -= y; NEG x; DOUBLE y; y -= x. +``` + +The independent checker uses a different four-letter backward realization +obtained by letterwise inverse transposition, and verifies the same matrix. + +| Complete local scalar program | Retained Horner real primitives | Replacement | Saving | +|---|---:|---:|---:| +| Forward | 193,162 | 192,378 | 784 | +| Backward | 193,210 | 192,426 | 784 | + +Each ADD reads one other register and writes its target; each NEG/HALF/DOUBLE +is charged once. Both real components are counted. The replacement needs no +copy, new helper, coefficient scratch, frame change, restoration instruction, +or recursive child. Both live targets reach their original pair endpoint, so +the later compensation, adapters, centers, frame changes, wrappers, B word and +cleanup use exactly the same inputs. Each replacement interval uses exactly +its two native target registers. All 112 registers have entrance frame zero. + +The retained comparison is implemented literally, including every coefficient +work clear, signed accumulation and shift. Its count agrees with the archived +`LOCAL-CHECKS.json` in both orientations. The six-operation comparison uses +two operations for the signed scale, three for a half-add by target dilation, +and one unit add; the independent BFS proves each separate macro minimum. +No additivity with other pending lowering proposals is assumed. + +## Proof, completed search and verification scope + +[PAIR-PROOF.md](PAIR-PROOF.md) gives an elementary four-operation lower bound: +the negative dyadic determinant requires a NEG and a scale, and the dense +matrix requires at least two ADDs. Its scope is exactly two live registers, +unit-cost signed unit ADD, NEG, HALF and DOUBLE, without scratch or a free swap. +It is not a lower bound for other instruction sets or the full supplier. + +`independent_checker.py` uses a separately written dense Fraction-matrix engine, +imports no integration code, and verifies every word through length four in +the ten-instruction alphabet: **11,111 words**, no coefficient pruning, exactly +eight shortest words per orientation. A separate state-deduplicated BFS agrees. +Seed 22 was drawn from OS randomness; the exhaustive search itself is deterministic. +The stopping rule is length four, where explicit witnesses meet the analytic bound. + +`verify.py` independently expands the retained Horner macros and the replacement +into real primitives, then replays both complete local scalar projections with +exact sparse rational rows. It checks **737 formal columns per orientation**: +728 native registers (including arbitrary dirty helpers), eight independently +dirty center cells and one dirty coefficient-work cell. It verifies every pair's +native endpoints, the complete program endpoints, and final clearing of all +private cells. The fused pair does not use the work cell and can leave its old +dirt untouched; the unchanged suffix clears it before use. Pair-boundary equality +is asserted on native registers, not on that eliminated private scratch cell. + +All phase/event boundaries outside the first 168 scalar macros are retained. +The unchanged suffix is hashed. The retained paid profile is +`{1:2548,2:338,3:430,4:194,5:56,8:8}`. All 672 instruction-deletion/sign mutants +across 56 pairs and two orientations fail the exact pair identity. Separate +tests reject altered coefficients, nonzero entrance frames, overlapping or +missing pairs, changed source bytes and omission of a dirty-work clear. + +## Precision: local increase, unchanged complete scalar budgets + +Every shortest forward realization raises the isolated prefix row-l1 maximum +from **1 to 2**. This is an actual intermediate growth requirement, not a +rounding-free implementation claim. The backward isolated maximum stays 2. +The full literal primitive replays give: + +| Exact scalar prefix metric | Retained | Replacement | +|---|---:|---:| +| Forward maximum row-l1 | 525,312 | 525,312 | +| Backward maximum row-l1 | 5,338,828 | 5,338,828 | +| Forward maximum binary denominator exponent | 3 | 3 | +| Backward maximum binary denominator exponent | 19 | 19 | + +These metrics include private scalar rows and every primitive prefix. They +bound exact linear growth and exact grid representability in the scalar +projection. They do **not** evaluate physical phase/frame/recursive operations, +roundoff accumulation or the full inherited precision/tape theorem. Those +obligations, all-size compilation, common-label/mutable-source realization, +whole-call hosting and analytic transfer remain inherited. No full Lean +multiplication theorem, practical runtime improvement or new kappa is claimed. + +## Provenance and nearby work + +Base commit: `f567884aeb8851b6e794af1184119a3bfbe1e631`. +The selected record points to Jeremy Kothe's PR799, pinned at +`80e6463157cfc80b85af09e7e2f14748fe2dac60`, with Chafik Boukhalfa's PR741 +(`e516b1463606840a15f80aac1995d64ce0092e89`) and DreamingOfClouds' PR589 bit +supplier on eumemic's PR555. The consumed input is the **actual integrated X4 +replay**, not the historical 492-helper `evidence/local` copy retained inside +the package. Archive/member hashes and contextual source pins are in +[SOURCES.json](SOURCES.json); [RESULT.json](RESULT.json) records consumed payloads. +The entire source archive is an immutable input; generated result JSON is +compared structurally, independent of compressed container bytes. + +Credit icekylinx's PR425 target-butterfly/emitter lineage, Jeremy Kothe and the +X4/SW4 contributors, Chafik Boukhalfa, DreamingOfClouds, Rohan Arun, eumemic and +the predecessor notices retained in the repository. This work makes no +priority claim for the elementary butterfly or scale-commutation identities. + +Related pending work was checked at pinned heads: + +- [Sagar Thakrar's PR750](https://github.com/CrocSwap/integer-mult-bounds/pull/750), + `b6d6934092c063ab2575ebee00f48bbc7b1c9d82`: historical CK cleanup scale relocation. + This package synthesizes the selected X4 zero-frame three-macro blocks. +- [Gareth Davidson's PR837](https://github.com/CrocSwap/integer-mult-bounds/pull/837), + `0a2977195efc8fb2a918fbfb694ec8d294387f08`: within-macro Horner lowering, + following Sagar Thakrar's PR696/723 and Chris Pagolu's PR734. Our factorization + crosses three macro boundaries and does not import their pending implementation. +- [PR866](https://github.com/CrocSwap/integer-mult-bounds/pull/866), + `5ae580bf68516f1cbe3b2dd3cb646be55170288f`: exact fractional-grid audit motivating + an explicit check of intermediate denominators as well as endpoints. +- PR840 concerns native BIT query fusion; PR864 fixes the X4 scalar word while + optimizing frames. Neither analyzes this scalar pair factorization. + +Prepared by **Philipp (@mightyOil)** with substantial **OpenAI Codex assistance**, +including separately implemented AI-assisted pair verification and review. +This is not independent human peer review. New files are Apache-2.0 under the +repository license. No predecessor files, source archives or notices are edited. diff --git a/research/x4-precondition-seed22/RESULT.json b/research/x4-precondition-seed22/RESULT.json new file mode 100644 index 0000000000..a9a1deeab1 --- /dev/null +++ b/research/x4-precondition-seed22/RESULT.json @@ -0,0 +1,385 @@ +{ + "archive_sha256": "70dfdfcf2ff95352c6020ee9dfca6dca9032b33c10daed3f3dc574c014f4e2cb", + "assignment_seed": 22, + "base_commit": "f567884aeb8851b6e794af1184119a3bfbe1e631", + "new_kappa_claim": false, + "orientations": { + "backward": { + "dirty_private_columns": 9, + "formal_columns": 737, + "native_columns": 728, + "paid_profile": { + "1": 2548, + "2": 338, + "3": 430, + "4": 194, + "5": 56, + "8": 8 + }, + "precondition": { + "replacement": { + "exact_prefix_fraction_bits": 0, + "exact_prefix_row_l1": "2", + "per_component_opcodes": { + "add": 112, + "double": 56, + "neg": 56 + }, + "per_component_primitives": 224, + "real_component_primitives": 448 + }, + "retained": { + "exact_prefix_fraction_bits": 0, + "exact_prefix_row_l1": "2", + "per_component_opcodes": { + "add": 224, + "clear": 224, + "double": 56, + "half": 56, + "neg": 56 + }, + "per_component_primitives": 616, + "real_component_primitives": 1232 + } + }, + "private_cells_cleared": true, + "replacement": { + "exact_prefix_fraction_bits": 19, + "exact_prefix_row_l1": "5338828", + "per_component_opcodes": { + "add": 37959, + "clear": 36488, + "double": 6946, + "half": 14172, + "neg": 648 + }, + "per_component_primitives": 96213, + "real_component_primitives": 192426 + }, + "retained": { + "exact_prefix_fraction_bits": 19, + "exact_prefix_row_l1": "5338828", + "per_component_opcodes": { + "add": 38071, + "clear": 36712, + "double": 6946, + "half": 14228, + "neg": 648 + }, + "per_component_primitives": 96605, + "real_component_primitives": 193210 + }, + "saved_real_component_primitives": 784, + "unchanged_suffix_sha256": "509834b6273ba5b5e8eda0b337a399df4a1a260c197549c066f8538db26fb345" + }, + "forward": { + "dirty_private_columns": 9, + "formal_columns": 737, + "native_columns": 728, + "paid_profile": { + "1": 2548, + "2": 338, + "3": 430, + "4": 194, + "5": 56, + "8": 8 + }, + "precondition": { + "replacement": { + "exact_prefix_fraction_bits": 1, + "exact_prefix_row_l1": "2", + "per_component_opcodes": { + "add": 112, + "half": 56, + "neg": 56 + }, + "per_component_primitives": 224, + "real_component_primitives": 448 + }, + "retained": { + "exact_prefix_fraction_bits": 1, + "exact_prefix_row_l1": "1", + "per_component_opcodes": { + "add": 224, + "clear": 224, + "half": 112, + "neg": 56 + }, + "per_component_primitives": 616, + "real_component_primitives": 1232 + } + }, + "private_cells_cleared": true, + "replacement": { + "exact_prefix_fraction_bits": 3, + "exact_prefix_row_l1": "525312", + "per_component_opcodes": { + "add": 37943, + "clear": 36472, + "copy": 8, + "double": 6946, + "half": 14172, + "neg": 648 + }, + "per_component_primitives": 96189, + "real_component_primitives": 192378 + }, + "retained": { + "exact_prefix_fraction_bits": 3, + "exact_prefix_row_l1": "525312", + "per_component_opcodes": { + "add": 38055, + "clear": 36696, + "copy": 8, + "double": 6946, + "half": 14228, + "neg": 648 + }, + "per_component_primitives": 96581, + "real_component_primitives": 193162 + }, + "saved_real_component_primitives": 784, + "unchanged_suffix_sha256": "1765afbd06f4c2609f4238570e4ff335aa802790750b77991a82737520a2c170" + } + }, + "pair_count": 56, + "pairs": [ + [ + 119, + 169 + ], + [ + 139, + 112 + ], + [ + 193, + 204 + ], + [ + 199, + 188 + ], + [ + 122, + 174 + ], + [ + 203, + 182 + ], + [ + 123, + 175 + ], + [ + 202, + 183 + ], + [ + 191, + 206 + ], + [ + 201, + 184 + ], + [ + 121, + 173 + ], + [ + 137, + 114 + ], + [ + 150, + 129 + ], + [ + 143, + 124 + ], + [ + 189, + 215 + ], + [ + 168, + 212 + ], + [ + 131, + 152 + ], + [ + 167, + 213 + ], + [ + 151, + 130 + ], + [ + 214, + 166 + ], + [ + 136, + 219 + ], + [ + 197, + 210 + ], + [ + 147, + 157 + ], + [ + 144, + 160 + ], + [ + 221, + 134 + ], + [ + 145, + 161 + ], + [ + 135, + 220 + ], + [ + 162, + 146 + ], + [ + 140, + 170 + ], + [ + 113, + 118 + ], + [ + 198, + 205 + ], + [ + 187, + 194 + ], + [ + 172, + 142 + ], + [ + 186, + 195 + ], + [ + 141, + 171 + ], + [ + 196, + 185 + ], + [ + 178, + 207 + ], + [ + 200, + 192 + ], + [ + 138, + 120 + ], + [ + 115, + 179 + ], + [ + 209, + 176 + ], + [ + 116, + 180 + ], + [ + 177, + 208 + ], + [ + 181, + 117 + ], + [ + 217, + 154 + ], + [ + 165, + 127 + ], + [ + 218, + 153 + ], + [ + 164, + 126 + ], + [ + 156, + 128 + ], + [ + 163, + 125 + ], + [ + 216, + 155 + ], + [ + 211, + 190 + ], + [ + 158, + 132 + ], + [ + 223, + 148 + ], + [ + 222, + 149 + ], + [ + 159, + 133 + ] + ], + "payload_sha256": { + "native/local/CANONICAL-WORD.json.gz": "1c0e9da767d4418f70016af599e4a447a3f7777acabe930318459c0fbbd260aa", + "native/local/LOCAL-CHECKS.json": "bbde5cea7bfd5df3d3ee7dfada0ff9d165af43a4d1dec6a9597cbfd8f87cc3b2", + "native/local/LOCAL-PROGRAMS.json.gz": "223c2bb27ad68a4e9468c3ddaece1899d577b661190922fdd25f5976052c4cab" + }, + "per_pair_per_component": { + "fused": 4, + "gatewise_conjugation": 6, + "retained_horner": 11 + }, + "rejected_instruction_mutants": 672, + "saved_vs_gatewise_conjugation_real_primitives_per_orientation": 224, + "status": "PASS_X4_PRECONDITION_SEED22" +} diff --git a/research/x4-precondition-seed22/SOURCES.json b/research/x4-precondition-seed22/SOURCES.json new file mode 100644 index 0000000000..b6b0a0b5bf --- /dev/null +++ b/research/x4-precondition-seed22/SOURCES.json @@ -0,0 +1,24 @@ +{ + "attribution": "Philipp (@mightyOil), with substantial OpenAI Codex assistance. Predecessors credited in README.md; no independent human review.", + "base_commit": "f567884aeb8851b6e794af1184119a3bfbe1e631", + "immutable_input_sha256": { + "certificates/selected-result.json": "9873519224e2db72d6a8c926f51e3e75129671e467948c6f6b03744f8bcfc699", + "docs/research/community-frontier799-review.md": "bd91c10c67f2a873fd456b95cbb43f715a43dac0e0a66938737d591c6b754052", + "research/community-frontier799-audit/integrated799-replay.tar.gz": "70dfdfcf2ff95352c6020ee9dfca6dca9032b33c10daed3f3dc574c014f4e2cb", + "research/complex-sw4-frame8/local/hpe_emit_local.py": "7e4a6fbc38c8228157b6311457d1496bf460291393043932d2c365f004f77805", + "research/gauge44-frames-x/construction/jx/LOCAL-PINS-jx-X4.json": "95c5114c8e937c2737a1b9f9da97303f2e5e129d39e6dfcc4010e99bfdb9c974" + }, + "license": "Apache-2.0", + "read_only_overlap_heads": { + "750": "b6d6934092c063ab2575ebee00f48bbc7b1c9d82", + "837": "0a2977195efc8fb2a918fbfb694ec8d294387f08", + "840": "da2cd0dd2229e08b61b174a8835a2c2bb99d2230", + "864": "9b1a55f6d281ae5bd7d691977d38861fcd9bd015", + "866": "5ae580bf68516f1cbe3b2dd3cb646be55170288f" + }, + "selected_source_heads": { + "589": "a5afc8c6169ea61ba7c51dfd3cade02cc7b13b46", + "741": "e516b1463606840a15f80aac1995d64ce0092e89", + "799": "80e6463157cfc80b85af09e7e2f14748fe2dac60" + } +} diff --git a/research/x4-precondition-seed22/VALIDATION.md b/research/x4-precondition-seed22/VALIDATION.md new file mode 100644 index 0000000000..af90bdf276 --- /dev/null +++ b/research/x4-precondition-seed22/VALIDATION.md @@ -0,0 +1,53 @@ +# Validation — 2026-10-13 + +Base: `f567884aeb8851b6e794af1184119a3bfbe1e631`. macOS arm64. + +## Completed contribution checks + +- `python3 -B -I -O research/x4-precondition-seed22/check.py`: + **PASS**, CPython 3.14.7. Both exact certificates match; 737 columns in each + orientation, 672 instruction mutants, exhaustive pair search, seven tests. +- A minimal copy containing only this package and the five pinned source files + was placed under a directory containing spaces. The same `check.py`, invoked + by absolute script resolution with `/usr/bin/python3 -B -I`, **PASS**, CPython + 3.9.6. No installed third-party libraries were used. +- A separately delegated AI review confirmed the algebra and invoices, + ran all seven tests from `/private/tmp` with `-B -I -O`, and independently + regenerated `INDEPENDENT.json` with exact structural equality. No blocking + finding remained. This is not independent human review. +- Cross-certificate comparison: all 56 ordered register pairs agree between + the two implementations; per-macro minima `[2,3,1]` and 737-column inventory + agree with the integration receipt. +- `make selected-record-check`: **PASS**, existing selected + `1661634653669567/1000000000000000000` unchanged. +- `git diff --cached --check`: **PASS**. Only this new research directory is + staged. No `upstream/`, production code, source archive, selected certificate + or predecessor notice changes. + +## General repository suite — incomplete, not a pass + +One `make verify` ran on a fresh `git archive` export of the exact base, to keep +unrelated generated files out of this contribution. It ran from 09:25:28 to +09:36:21 UTC (10 minutes 53 seconds), then was deliberately interrupted to +keep the bounded sprint focused on verification and handoff. + +The six earlier groups completed: `verify-community`, `verify-producers`, +`verify-partial-gauge`, `verify-three-stage-cover`, `verify-paired-cube`, and +`verify-recycled-bit`. The selected-record check also passed at the start of +`verify-entrance-banks`. Interruption occurred while that target ran +`research/coordinated-frames-and-entrance-banks/verify.py`; it is **not** a +mathematical failure or a completed check. Exit status was 130. + +The captured log SHA-256 is +`ef90b5bf2cd4b02e6758f169e112e73f1eda33908ca5547a91a4b18f4ae75062`. +No complete repository-suite, selected cold-replay, full physical precision, +global admission, hosted CI or Lean pass is claimed. The new package has no +third-party dependency and its own checks all completed. + +## Final overlap screen + +At 09:32 UTC, main was still the exact base. The initial full snapshot covered +669 open PRs through #876; the latest 100 were refreshed through #880. +Pinned coordination issues remained empty. New #877–#880 do not concern +the selected X4 two-register precondition factors. Exact nearby source heads +and distinctions are in `SOURCES.json` and `README.md`. diff --git a/research/x4-precondition-seed22/check.py b/research/x4-precondition-seed22/check.py new file mode 100644 index 0000000000..f8d6471769 --- /dev/null +++ b/research/x4-precondition-seed22/check.py @@ -0,0 +1,39 @@ +#!/usr/bin/env python3 +"""One-command, offline reproduction of the standalone X4 pair package.""" +import hashlib +import json +from pathlib import Path +import subprocess +import sys + +HERE = Path(__file__).resolve().parent + + +def run(script, *args): + command = [sys.executable, "-B", "-I"] + if sys.flags.optimize: + command.append("-O") + result = subprocess.run(command + [str(HERE / script), *map(str, args)], + text=True, capture_output=True) + if result.returncode: + raise RuntimeError(script + " failed:\n" + result.stdout + result.stderr) + return result + + +def main(): + sources = json.loads((HERE / "SOURCES.json").read_text()) + for relative, expected in sources["immutable_input_sha256"].items(): + if hashlib.sha256((HERE.parents[1] / relative).read_bytes()).hexdigest() != expected: + raise ValueError("source binding differs: " + relative) + print(run("verify.py", "--check", HERE / "RESULT.json").stdout.strip(), flush=True) + independent = json.loads(run("independent_checker.py").stdout) + if independent != json.loads((HERE / "INDEPENDENT.json").read_text()): + raise ValueError("independent certificate differs") + print("PASS independent pair proof: minima=4/4 words=11111 gatewise=6/6", flush=True) + result = run("test_verify.py") + print(result.stderr.strip(), flush=True) + print("PASS_X4_PRECONDITION_PACKAGE no_new_kappa", flush=True) + + +if __name__ == "__main__": + main() diff --git a/research/x4-precondition-seed22/independent_checker.py b/research/x4-precondition-seed22/independent_checker.py new file mode 100644 index 0000000000..b66d423372 --- /dev/null +++ b/research/x4-precondition-seed22/independent_checker.py @@ -0,0 +1,228 @@ +#!/usr/bin/env python3 +"""Independent, standard-library-only exact check of the isolated X4 pair map. + +No imports from the integration verifier, no scratch register, no permutation, +and no weighted-cost or whole-circuit optimality claim. Every alphabet letter +costs one. Run from any directory; stdout is deterministic JSON. +""" + +from fractions import Fraction as Q +from hashlib import sha256 +from itertools import product +from pathlib import Path +import argparse +import gzip +import json +import tarfile + +IDENTITY = (Q(1), Q(0), Q(0), Q(1)) +FORWARD = (Q(-1, 2), Q(1, 2), Q(1, 2), Q(1, 2)) +BACKWARD = (Q(-1), Q(1), Q(1), Q(1)) + +# (kind, destination, source-or-None, exact multiplier) +ALPHABET = tuple( + [("ADD", i, 1 - i, Q(s)) for i in (0, 1) for s in (-1, 1)] + + [(name, i, None, scalar) + for name, scalar in (("NEG", Q(-1)), ("HALF", Q(1, 2)), ("DOUBLE", Q(2))) + for i in (0, 1)] +) +FORWARD_WORD = ( + ("ADD", 0, 1, Q(-1)), ("NEG", 0, None, Q(-1)), + ("HALF", 0, None, Q(1, 2)), ("ADD", 1, 0, Q(-1)), +) +# This word is the letterwise inverse transpose of FORWARD_WORD. The +# chronological order stays the same under the inverse-transpose operation. +BACKWARD_WORD = ( + ("ADD", 1, 0, Q(1)), ("NEG", 0, None, Q(-1)), + ("DOUBLE", 0, None, Q(2)), ("ADD", 0, 1, Q(1)), +) +ORIGINAL_FORWARD = ( + ("SCALE", 0, None, Q(-1, 2)), ("ADD", 0, 1, Q(1, 2)), + ("ADD", 1, 0, Q(-1)), +) +ORIGINAL_BACKWARD = ( + ("SCALE", 0, None, Q(-2)), ("ADD", 1, 0, Q(-1, 2)), + ("ADD", 0, 1, Q(1)), +) +ARCHIVE_SHA256 = "70dfdfcf2ff95352c6020ee9dfca6dca9032b33c10daed3f3dc574c014f4e2cb" +MEMBER_HASHES = { + "native/local/CANONICAL-WORD.json.gz": + "f1c2ede9276d4447c5857d0e9d32adb52f987b8adb643b45bde2c172d88c6ee9", + "native/local/LOCAL-PROGRAMS.json.gz": + "ce194f8465079db575a9ce17ccee1396fa4de0210e2817da2525f95f4f93ebde", +} + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def step(matrix, instruction): + kind, destination, source, scalar = instruction + result = list(matrix) + for column in range(2): + at = 2 * destination + column + result[at] = (matrix[at] + scalar * matrix[2 * source + column] + if kind == "ADD" else scalar * matrix[at]) + return tuple(result) + + +def trace(word): + matrices = [IDENTITY] + for instruction in word: + matrices.append(step(matrices[-1], instruction)) + return matrices + + +def inverse_transpose(matrix): + a, b, c, d = matrix + determinant = a * d - b * c + require(determinant != 0, "singular target") + return (d / determinant, -c / determinant, + -b / determinant, a / determinant) + + +def metrics(matrices): + return { + "peak_row_l1": str(max(max(abs(m[0]) + abs(m[1]), + abs(m[2]) + abs(m[3])) for m in matrices)), + "maximum_reduced_denominator": max(q.denominator for m in matrices for q in m), + "maximum_absolute_reduced_numerator": max(abs(q.numerator) for m in matrices for q in m), + "prefix_matrices": [[str(q) for q in m] for m in matrices], + } + + +def breadth_first(): + # Deduplication is sound because every continuation depends only on the + # current 2x2 matrix. Retain first-seen distance, not a coefficient cutoff. + distances = {IDENTITY: 0} + frontier = {IDENTITY} + sizes = [1] + for depth in range(1, 5): + following = set() + for matrix in frontier: + for letter in ALPHABET: + candidate = step(matrix, letter) + if candidate not in distances: + following.add(candidate) + distances.update({matrix: depth for matrix in following}) + sizes.append(len(following)) + frontier = following + require(sizes == [1, 10, 69, 370, 1646], "BFS frontier changed") + require(distances[FORWARD] == distances[BACKWARD] == 4, "minimum changed") + gatewise = {} + for name, word in (("forward", ORIGINAL_FORWARD), ("backward", ORIGINAL_BACKWARD)): + lengths = [distances[step(IDENTITY, letter)] for letter in word] + require(lengths == [2, 3, 1], "gatewise primitive minima changed") + gatewise[name] = lengths + return {"frontier_sizes": sizes, "original_gatewise_minimum_lengths": gatewise} + + +def exhaustive_words(): + # A separate full-word enumeration cross-checks the state-based BFS and + # examines *every* shortest realization's intermediate guard. + counts = {"forward": 0, "backward": 0} + targets = {FORWARD: "forward", BACKWARD: "backward"} + examined = [] + for depth in range(5): + total = 0 + for word in product(ALPHABET, repeat=depth): + total += 1 + matrices = trace(word) + name = targets.get(matrices[-1]) + if name: + require(depth == 4, "a circuit shorter than four exists") + counts[name] += 1 + measured = metrics(matrices) + require(measured["peak_row_l1"] == "2", "optimal guard changed") + require(measured["maximum_reduced_denominator"] == + (2 if name == "forward" else 1), "optimal fraction guard changed") + examined.append(total) + require(counts == {"forward": 8, "backward": 8}, "shortest word count changed") + return {"words_examined_by_length": examined, "shortest_word_counts": counts} + + +def check_archive(path): + require(sha256(path.read_bytes()).hexdigest() == ARCHIVE_SHA256, + "archive differs from pinned PR799 input") + objects = {} + with tarfile.open(path, "r:gz") as archive: + for name, expected_hash in MEMBER_HASHES.items(): + member = archive.extractfile(name) + require(member is not None, "missing archive member") + raw = member.read() + require(sha256(raw).hexdigest() == expected_hash, "archive member hash mismatch") + objects[name] = json.loads(gzip.decompress(raw)) + canonical = objects["native/local/CANONICAL-WORD.json.gz"] + programs = objects["native/local/LOCAL-PROGRAMS.json.gz"] + precondition = canonical["precondition"] + require(len(precondition) == 168, "precondition is not 56 triples") + pairs = [] + expected_forward = [["phase", "zero_frame_precondition"]] + expected_backward = [["phase", "zero_frame_precondition"]] + for offset in range(0, len(precondition), 3): + block = precondition[offset:offset + 3] + x, y = block[0][1], block[1][2] + require(block == [["scale", x, -1, 2, 0], + ["add", x, y, 1, 2, 0], + ["add", y, x, -1, 1, 0]], "unexpected pair shape") + pairs.append([x, y]) + expected_forward.extend([ + ["scalar", ["scale", ["L", x], -1, 2], 0], + ["scalar", ["add", ["L", x], ["L", y], 1, 2], 0], + ["scalar", ["add", ["L", y], ["L", x], -1, 1], 0], + ]) + expected_backward.extend([ + ["scalar", ["scale", ["L", x], 2, -1], 0], + ["scalar", ["add", ["L", y], ["L", x], -1, 2], 0], + ["scalar", ["add", ["L", x], ["L", y], 1, 1], 0], + ]) + require(len({register for pair in pairs for register in pair}) == 112, + "pairs overlap") + for direction, expected in (("forward", expected_forward), ("backward", expected_backward)): + require(programs[direction][:169] == expected, direction + " archived prefix differs") + return {"archive_sha256": ARCHIVE_SHA256, "member_sha256": MEMBER_HASHES, + "pair_count": len(pairs), "distinct_registers": 112, "pairs": pairs} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--archive", type=Path, default=Path(__file__).resolve().parents[1] + / "community-frontier799-audit" / "integrated799-replay.tar.gz") + args = parser.parse_args() + require(trace(ORIGINAL_FORWARD)[-1] == FORWARD, "original forward algebra fails") + require(trace(FORWARD_WORD)[-1] == FORWARD, "candidate forward algebra fails") + require(trace(ORIGINAL_BACKWARD)[-1] == BACKWARD, "original backward algebra fails") + require(trace(BACKWARD_WORD)[-1] == BACKWARD, "candidate backward algebra fails") + require(inverse_transpose(FORWARD) == BACKWARD, "duality identity fails") + for f, b in zip(FORWARD_WORD, BACKWARD_WORD): + require(inverse_transpose(step(IDENTITY, f)) == step(IDENTITY, b), + "letterwise inverse-transpose mismatch") + # Negative controls: deletion and a sign mutation must be detected by the + # matrix oracle. A false prefix bound of one must also be detected. + no_neg = FORWARD_WORD[:1] + FORWARD_WORD[2:] + wrong_sign = (("ADD", 0, 1, Q(1)),) + FORWARD_WORD[1:] + require(trace(no_neg)[-1] != FORWARD, "negative control: omitted NEG accepted") + require(trace(wrong_sign)[-1] != FORWARD, "negative control: wrong sign accepted") + require(metrics(trace(FORWARD_WORD))["peak_row_l1"] != "1", + "negative control: false norm guard accepted") + result = { + "status": "PASS", + "scope": "isolated two-register pair; ADD(+/-1), NEG, HALF, DOUBLE; unit cost; no scratch or swap", + "archive": check_archive(args.archive), + "minimum_primitive_counts": {"forward": 4, "inverse_transpose_backward": 4}, + "bfs": breadth_first(), + "exhaustive": exhaustive_words(), + "original_rational_forward": metrics(trace(ORIGINAL_FORWARD)), + "candidate_forward": metrics(trace(FORWARD_WORD)), + "original_rational_backward": metrics(trace(ORIGINAL_BACKWARD)), + "candidate_backward": metrics(trace(BACKWARD_WORD)), + "negative_controls_rejected": ["omitted NEG", "wrong first ADD sign", "false forward row-l1 guard <= 1"], + "limitation": "No assertion of global-circuit optimality, global guard acceptance, or a new kappa bound.", + } + print(json.dumps(result, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/x4-precondition-seed22/test_verify.py b/research/x4-precondition-seed22/test_verify.py new file mode 100644 index 0000000000..1db549976c --- /dev/null +++ b/research/x4-precondition-seed22/test_verify.py @@ -0,0 +1,88 @@ +#!/usr/bin/env python3 +"""Source-boundary and dirty-scratch controls, not performance tests.""" +import copy +import importlib.util +from pathlib import Path +import tempfile +import unittest + +HERE = Path(__file__).resolve().parent +spec = importlib.util.spec_from_file_location("x4_precondition", HERE / "verify.py") +v = importlib.util.module_from_spec(spec) +spec.loader.exec_module(v) + + +class Controls(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.word, cls.programs, cls.checks = v.load_inputs() + + def test_changed_coefficient(self): + word = copy.deepcopy(self.word) + word["precondition"][1][3] = -1 + with self.assertRaisesRegex(ValueError, "triple shape"): + v.pairs(word) + + def test_nonzero_frame(self): + word = copy.deepcopy(self.word) + word["start"][word["precondition"][0][1]] = 1 + with self.assertRaisesRegex(ValueError, "zero-frame"): + v.pairs(word) + + def test_overlapping_pair(self): + word = copy.deepcopy(self.word) + word["precondition"][3:6] = word["precondition"][:3] + with self.assertRaisesRegex(ValueError, "disjoint"): + v.pairs(word) + + def test_missing_pair(self): + word = copy.deepcopy(self.word) + del word["precondition"][:3] + with self.assertRaisesRegex(ValueError, "56 complete"): + v.pairs(word) + + def test_archive_corruption(self): + with tempfile.TemporaryDirectory() as tmp: + root = Path(tmp) + path = root / v.ARCHIVE + path.parent.mkdir(parents=True) + path.write_bytes(b"not the pinned archive") + with self.assertRaisesRegex(ValueError, "source archive digest"): + v.load_inputs(root) + + def test_dirty_coefficient_work_requires_first_clear(self): + program = v.lower(["add", ["L", 0], ["L", 1], 1, 2]) + good, bad = v.Replay(2), v.Replay(2) + for op in program: + good.apply(op) + for op in program[1:]: + bad.apply(op) + self.assertEqual(good.rows[("L", 0)], {0: v.Q(1), 1: v.Q(1, 2)}) + self.assertIn(10, bad.rows[("L", 0)]) # independent dirty W column + self.assertFalse(good.rows[v.WORK]) + + def test_six_operation_gatewise_comparison(self): + x, y = ("L", 0), ("L", 1) + candidates = { + False: [("neg", x), ("half", x), ("double", x), + ("add", x, y, 1), ("half", x), ("add", y, x, -1)], + True: [("neg", x), ("double", x), ("double", y), + ("add", y, x, -1), ("half", y), ("add", x, y, 1)], + } + for backward, gatewise in candidates.items(): + old, mid, new = v.Replay(2), v.Replay(2), v.Replay(2) + for macro in v.expected_macros(0, 1, backward): + for op in v.lower(macro): + old.apply(op) + for op in gatewise: + mid.apply(op) + for op in v.replacement(0, 1, backward): + new.apply(op) + self.assertEqual([old.count, mid.count, new.count], [11, 6, 4]) + for r in (x, y): + self.assertEqual(old.rows[r], mid.rows[r]) + self.assertEqual(old.rows[r], new.rows[r]) + + +if __name__ == "__main__": + unittest.main(verbosity=2) diff --git a/research/x4-precondition-seed22/verify.py b/research/x4-precondition-seed22/verify.py new file mode 100644 index 0000000000..ae89da5598 --- /dev/null +++ b/research/x4-precondition-seed22/verify.py @@ -0,0 +1,285 @@ +#!/usr/bin/env python3 +"""Exact, source-bound X4 precondition lowering; no changed kappa claim. + +Philipp (@mightyOil), with substantial OpenAI Codex assistance. Apache-2.0. +The retained X4 word/emitter and their contributors are credited in README.md. +""" +import argparse +from collections import Counter +from fractions import Fraction as Q +import gzip +import hashlib +import json +from pathlib import Path +import tarfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +ARCHIVE = "research/community-frontier799-audit/integrated799-replay.tar.gz" +ARCHIVE_SHA = "70dfdfcf2ff95352c6020ee9dfca6dca9032b33c10daed3f3dc574c014f4e2cb" +PAYLOADS = { + "native/local/CANONICAL-WORD.json.gz": "1c0e9da767d4418f70016af599e4a447a3f7777acabe930318459c0fbbd260aa", + "native/local/LOCAL-PROGRAMS.json.gz": "223c2bb27ad68a4e9468c3ddaece1899d577b661190922fdd25f5976052c4cab", + "native/local/LOCAL-CHECKS.json": "bbde5cea7bfd5df3d3ee7dfada0ff9d165af43a4d1dec6a9597cbfd8f87cc3b2", +} +PROFILE = {1: 2548, 2: 338, 3: 430, 4: 194, 5: 56, 8: 8} +WORK = ("W", 0) + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def digest(data): + return hashlib.sha256(data).hexdigest() + + +def canonical(data): + return json.dumps(data, sort_keys=True, separators=(",", ":")).encode() + + +def load_inputs(root=ROOT): + path = root / ARCHIVE + require(digest(path.read_bytes()) == ARCHIVE_SHA, "source archive digest") + result = [] + with tarfile.open(path, "r:gz") as archive: + for member, expected in PAYLOADS.items(): + payload = archive.extractfile(member).read() + if member.endswith(".gz"): + payload = gzip.decompress(payload) + require(digest(payload) == expected, "source payload digest: " + member) + result.append(json.loads(payload)) + return result + + +def pairs(word): + pre = word["precondition"] + require(len(pre) == 168, "56 complete precondition triples required") + result = [] + used = set() + for i in range(0, len(pre), 3): + a, b, c = pre[i:i + 3] + x, y = a[1], b[2] + require(pre[i:i + 3] == [ + ["scale", x, -1, 2, 0], ["add", x, y, 1, 2, 0], + ["add", y, x, -1, 1, 0]], "precondition triple shape") + require(x != y and x not in used and y not in used, "disjoint pair support") + require(word["start"][x] == word["start"][y] == 0, "zero-frame start") + require(word["v"] <= x < 2 * word["v"] and + word["v"] <= y < 2 * word["v"], "target-only support") + used.update((x, y)) + result.append((x, y)) + return result + + +def expected_macros(x, y, backward): + x, y = ["L", x], ["L", y] + if backward: + return [["scale", x, 2, -1], ["add", y, x, -1, 2], ["add", x, y, 1, 1]] + return [["scale", x, -1, 2], ["add", x, y, 1, 2], ["add", y, x, -1, 1]] + + +def replacement(x, y, backward): + x, y = ("L", x), ("L", y) + # Forward: x = (y-x)/2, y = (x_old+y_old)/2. + # Backward: inverse transpose, x = y_old-x_old, y = x_old+y_old. + return [("add", x, y, -1), ("neg", x), + ("double", y) if backward else ("half", x), ("add", y, x, -1)] + + +def lower(op): + """Literal implementation of retained hpe_emit_local.primitive_bound. + + Every macro explicitly clears its private coefficient register before/after + use. No work-cell initialization, copy, scale, or source read is free. + """ + tag, target = op[0], tuple(op[1]) + if tag == "clear": + return [("clear", target)] + if tag == "copy": + return [("copy", target, tuple(op[2]))] + q = Q(op[3], op[4]) if tag == "add" else Q(op[2], op[3]) + a, b = abs(q.numerator), q.denominator + require(a > 0 and b & (b - 1) == 0, "nonzero dyadic coefficient") + if tag == "scale": + require(a & (a - 1) == 0, "power-of-two scale") + k = a.bit_length() - b.bit_length() + return ([("neg", target)] if q < 0 else []) + [ + ("double" if k > 0 else "half", target)] * abs(k) + require(tag == "add", "known scalar macro") + source = tuple(op[2]) + require(source != WORK and target != WORK and source != target, "private work and distinct operands") + out = [("clear", WORK)] + for i, bit in enumerate(bin(a)[2:]): + if i: + out.append(("double", WORK)) + if bit == "1": + out.append(("add", WORK, source, 1)) + out.extend([("half", WORK)] * (b.bit_length() - 1)) + out.extend([("add", target, WORK, 1 if q > 0 else -1), ("clear", WORK)]) + return out + + +class Replay: + """All formal columns at once, sparse exact rational row arithmetic.""" + def __init__(self, n): + self.rows = {("L", r): {r: Q(1)} for r in range(n)} + # Nine independent dirty private columns: eight center cells and the + # Horner work cell. Their first clear/copy must actually erase the dirt. + self.rows.update({("C", i): {n + i: Q(1)} for i in range(8)}) + self.rows[WORK] = {n + 8: Q(1)} + self.count = 0 + self.peak_l1 = Q(1) + self.peak_fraction_bits = 0 + self.opcodes = Counter() + + def apply(self, op): + tag, t = op[:2] + row = self.rows.setdefault(t, {}) + if tag == "clear": + row = {} + elif tag == "copy": + row = self.rows.get(op[2], {}).copy() + elif tag in ("neg", "half", "double"): + q = {"neg": Q(-1), "half": Q(1, 2), "double": Q(2)}[tag] + row = {j: q * value for j, value in row.items()} + elif tag == "add": + require(t != op[2] and op[3] in (-1, 1), "signed unit addition") + for j, value in list(self.rows.get(op[2], {}).items()): + z = row.get(j, Q(0)) + op[3] * value + if z: + row[j] = z + else: + row.pop(j, None) + else: + raise ValueError("unknown primitive " + tag) + self.rows[t] = row + self.count += 1 + self.opcodes[tag] += 1 + self.peak_l1 = max(self.peak_l1, sum(map(abs, row.values()), Q(0))) + for value in row.values(): + d = value.denominator + require(d & (d - 1) == 0, "dyadic prefix") + self.peak_fraction_bits = max(self.peak_fraction_bits, d.bit_length() - 1) + + def endpoint(self, n, v, backward): + for r in range(n): + want = {r: Q(1)} + if backward and r < v: + want[r + v] = Q(-1) + if not backward and v <= r < 2 * v: + want[r - v] = Q(1) + require(self.rows[("L", r)] == want, "complete endpoint column row " + str(r)) + require(all(not row for r, row in self.rows.items() if r[0] != "L"), "all private cells cleared") + + def receipt(self): + return dict(real_component_primitives=2 * self.count, per_component_primitives=self.count, + exact_prefix_row_l1=str(self.peak_l1), exact_prefix_fraction_bits=self.peak_fraction_bits, + per_component_opcodes=dict(sorted(self.opcodes.items()))) + + +def run_orientation(word, program, checks, pair_list, backward): + require(digest(canonical(program)) == checks["sha256"], "program digest") + require(program[0] == ["phase", "zero_frame_precondition"], "precondition phase") + n, v = 2 * word["v"] + word["R"], word["v"] + old, new = Replay(n), Replay(n) + cursor = 1 + for x, y in pair_list: + expected = [["scalar", op, 0] for op in expected_macros(x, y, backward)] + require(program[cursor:cursor + 3] == expected, "emitted triple binding") + for _, macro, _ in expected: + for op in lower(macro): + old.apply(op) + for op in replacement(x, y, backward): + new.apply(op) + require(old.rows[("L", x)] == new.rows[("L", x)] and + old.rows[("L", y)] == new.rows[("L", y)], "pair endpoint mismatch") + cursor += 3 + pre = {"retained": old.receipt(), "replacement": new.receipt()} + paid = Counter() + # All later events, source reads, frames, adapters and wrappers are unchanged. + for event in program[cursor:]: + if event[0] == "scalar": + for op in lower(event[1]): + old.apply(op) + new.apply(op) + elif event[0] == "climb": + paid[event[5]] += 1 + elif event[0] == "center": + paid[event[4]] += 1 + old.endpoint(n, v, backward) + new.endpoint(n, v, backward) + require(dict(paid) == PROFILE, "paid profile") + require(old.count * 2 == checks["real_component_primitive_bound"], "retained complete primitive invoice") + require((old.count - new.count) * 2 == 784, "real-component primitive saving") + require(new.peak_l1 <= old.peak_l1 and new.peak_fraction_bits <= old.peak_fraction_bits, + "complete exact prefix budget must not increase") + return dict(retained=old.receipt(), replacement=new.receipt(), precondition=pre, + saved_real_component_primitives=784, formal_columns=n + 9, + native_columns=n, dirty_private_columns=9, + private_cells_cleared=True, paid_profile=PROFILE, + unchanged_suffix_sha256=digest(canonical(program[cursor:]))) + + +def controls(pair_list): + """Every pair, every instruction deletion and signed-add inversion, both ways.""" + rejected = 0 + for backward in (False, True): + # OS assignment seed 22 fixes mutation traversal, not a random proof. + ordered = pair_list[22:] + pair_list[:22] + for x, y in ordered: + program = replacement(x, y, backward) + ref = Replay(max(x, y) + 1) + for op in program: + ref.apply(op) + mutants = [program[:i] + program[i + 1:] for i in range(len(program))] + for i in (0, 3): + change = list(program[i]); change[3] *= -1 + mutants.append(program[:i] + [tuple(change)] + program[i + 1:]) + for mutant in mutants: + test = Replay(max(x, y) + 1) + for op in mutant: + test.apply(op) + require(any(test.rows[("L", r)] != ref.rows[("L", r)] for r in (x, y)), + "mutation did not fail the pair identity") + rejected += 1 + return rejected + + +def verify(): + word, programs, checks = load_inputs() + require(word["v"] == 112 and word["R"] == 504, "selected X4 dimensions") + require({int(k): v for k, v in word["local_profile"].items()} == PROFILE, "selected profile") + ps = pairs(word) + results = {} + for orientation in ("forward", "backward"): + results[orientation] = run_orientation(word, programs[orientation], checks[orientation], ps, + orientation == "backward") + return dict(status="PASS_X4_PRECONDITION_SEED22", assignment_seed=22, + base_commit="f567884aeb8851b6e794af1184119a3bfbe1e631", + archive_sha256=ARCHIVE_SHA, payload_sha256=PAYLOADS, pair_count=len(ps), + pairs=ps, orientations=results, rejected_instruction_mutants=controls(ps), + per_pair_per_component={"retained_horner": 11, "gatewise_conjugation": 6, + "fused": 4}, + saved_vs_gatewise_conjugation_real_primitives_per_orientation=224, + new_kappa_claim=False) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write", type=Path) + parser.add_argument("--check", type=Path) + args = parser.parse_args() + result = verify() + # JSON normalizes tuples and integer dictionary keys. + result = json.loads(json.dumps(result)) + if args.check: + require(result == json.loads(args.check.read_text()), "result certificate differs") + if args.write: + args.write.write_text(json.dumps(result, indent=2, sort_keys=True) + "\n") + print(result["status"], "pairs=56 columns=737x2 saved=784/784 controls=672 no_new_kappa") + + +if __name__ == "__main__": + main()