From c261298cb82ce518a13ca9b1d3361b14e250c8a2 Mon Sep 17 00:00:00 2001 From: nightangelflowerwin-ops Date: Tue, 13 Oct 2026 05:20:45 -0700 Subject: [PATCH 1/2] Admit source-bound X4 primitive refinement through complete selected accounting --- research/x4-primitive-admission/EXPECTED.json | 10 + .../x4-primitive-admission/FRESH-REPLAY.json | 190 ++++++++ research/x4-primitive-admission/PROOF.md | 67 +++ research/x4-primitive-admission/README.md | 77 ++++ research/x4-primitive-admission/SOURCES.json | 33 ++ research/x4-primitive-admission/VALIDATION.md | 45 ++ research/x4-primitive-admission/admit.py | 150 +++++++ research/x4-primitive-admission/lowering.py | 134 ++++++ .../x4-primitive-admission/test_controls.py | 88 ++++ .../vendor/pr865/README.md | 120 +++++ .../vendor/pr865/pr741-sw4-v1.json | 94 ++++ .../vendor/pr865/verify_replay_coverage.py | 151 +++++++ .../vendor/pr883/CLAIM.md | 12 + .../vendor/pr883/INDEPENDENT.json | 419 ++++++++++++++++++ .../vendor/pr883/PAIR-PROOF.md | 114 +++++ .../vendor/pr883/README.md | 159 +++++++ .../vendor/pr883/RESULT.json | 385 ++++++++++++++++ .../vendor/pr883/SOURCES.json | 24 + .../vendor/pr883/VALIDATION.md | 53 +++ .../vendor/pr883/check.py | 39 ++ .../vendor/pr883/independent_checker.py | 228 ++++++++++ .../vendor/pr883/test_verify.py | 88 ++++ .../vendor/pr883/verify.py | 285 ++++++++++++ 23 files changed, 2965 insertions(+) create mode 100644 research/x4-primitive-admission/EXPECTED.json create mode 100644 research/x4-primitive-admission/FRESH-REPLAY.json create mode 100644 research/x4-primitive-admission/PROOF.md create mode 100644 research/x4-primitive-admission/README.md create mode 100644 research/x4-primitive-admission/SOURCES.json create mode 100644 research/x4-primitive-admission/VALIDATION.md create mode 100644 research/x4-primitive-admission/admit.py create mode 100644 research/x4-primitive-admission/lowering.py create mode 100644 research/x4-primitive-admission/test_controls.py create mode 100644 research/x4-primitive-admission/vendor/pr865/README.md create mode 100644 research/x4-primitive-admission/vendor/pr865/pr741-sw4-v1.json create mode 100644 research/x4-primitive-admission/vendor/pr865/verify_replay_coverage.py create mode 100644 research/x4-primitive-admission/vendor/pr883/CLAIM.md create mode 100644 research/x4-primitive-admission/vendor/pr883/INDEPENDENT.json create mode 100644 research/x4-primitive-admission/vendor/pr883/PAIR-PROOF.md create mode 100644 research/x4-primitive-admission/vendor/pr883/README.md create mode 100644 research/x4-primitive-admission/vendor/pr883/RESULT.json create mode 100644 research/x4-primitive-admission/vendor/pr883/SOURCES.json create mode 100644 research/x4-primitive-admission/vendor/pr883/VALIDATION.md create mode 100644 research/x4-primitive-admission/vendor/pr883/check.py create mode 100644 research/x4-primitive-admission/vendor/pr883/independent_checker.py create mode 100644 research/x4-primitive-admission/vendor/pr883/test_verify.py create mode 100644 research/x4-primitive-admission/vendor/pr883/verify.py diff --git a/research/x4-primitive-admission/EXPECTED.json b/research/x4-primitive-admission/EXPECTED.json new file mode 100644 index 0000000000..7fc51e72ff --- /dev/null +++ b/research/x4-primitive-admission/EXPECTED.json @@ -0,0 +1,10 @@ +{ + "status": "PASS_X4_PRIMITIVE_GLOBAL_ADMISSION", + "base": "f567884aeb8851b6e794af1184119a3bfbe1e631", + "predecessor": "b31a870a3842b37f6ab97767c506ce91783632a2", + "kappa": "1661634653669567/1000000000000000000", + "saved_selected_real_component_primitives": 56448, + "saved_coefficient_work_operations": 36288, + "global_prefix_bits": 257, + "physical": 7682 +} diff --git a/research/x4-primitive-admission/FRESH-REPLAY.json b/research/x4-primitive-admission/FRESH-REPLAY.json new file mode 100644 index 0000000000..9512ea39ba --- /dev/null +++ b/research/x4-primitive-admission/FRESH-REPLAY.json @@ -0,0 +1,190 @@ +{ + "status": "PASS_FRESH_SELECTED_REPLAY_AND_PRIMITIVE_REFINEMENT", + "baseline_binding": { + "status": "PASS_REBUILT_PR589_PR799_COMPOSITION", + "kappa": "1661634653669567/1000000000000000000", + "decimal": "0.001661634653669567", + "ancestry": { + "status": "PASS_REBUILT_PR589_PR741_COMPOSITION", + "kappa": "1661202643272239/1000000000000000000", + "decimal": "0.001661202643272239", + "bit_input_sha256": "b9f0e5ca038abe837b0007c8fe006f366a6f02009244ac57705a8a200e2301f4", + "bit_result_sha256": "28795393651ef4fbbc6232eb2b32f7b39b91fbd5ea6d2315583f350714698055", + "complex_receipt_sha256": "68600c734560bb155037e3973f7fbfb2fd1cb678485f8ac128c0b1e1bb1840a0", + "complex_assembly_sha256": "35ccaac474236b2e244f02cc599fbe4ddee783713f37ea623842ecb8de31f209", + "scope": "Rebuilt finite suppliers and exact composition. All-size/compiler, common-label/mutable-source, whole-call hosting, precision/tape and analytic transfer hypotheses remain conditional; not a full Lean theorem." + }, + "package_manifest_sha256": "e1b7998c8f7cb24f8674d250d0510f2b5b351b2ed0b35f17a17e6bacf3d9824b", + "assembly_sha256": "a7ab72bc4a3a00bd2147ae30dcf67448d0dfd69ab57e8f27f5ef520d0a560d01", + "independent_sha256": "932930a48de3a0d2b68fb3d1272521b6a6692b7ead886dbda608823f49030d35", + "price_sha256": "04bff9778b12a8dd878e0bf304c163d93aea09f3b7b3ebc878dab66e23054dd9", + "scope": "Exact finite X4 scalar/frame/phase/owner/invoice/assembly checks, bound to rebuilt PR589 and SW4 ancestry. Inherited all-size/compiler, common-label/mutable-source, whole-call hosting, precision/tape and analytic assumptions remain; not a full Lean theorem.", + "reused_ancestry": true + }, + "guarded_public_result": { + "status": "PASS_COMPLETE_PR799_REPLAY_COVERAGE", + "kappa": "1661634653669567/1000000000000000000", + "decimal": "0.001661634653669567", + "coverage_contract": "pr741-sw4-v1", + "contract_sha256": "7acd5033bc78e3f473718269edaa267c2785d84fbe95ccf6815a33dcf58c2756", + "selected_binding": { + "status": "PASS_REBUILT_PR589_PR799_COMPOSITION", + "kappa": "1661634653669567/1000000000000000000", + "decimal": "0.001661634653669567", + "ancestry": { + "status": "PASS_REBUILT_PR589_PR741_COMPOSITION", + "kappa": "1661202643272239/1000000000000000000", + "decimal": "0.001661202643272239", + "bit_input_sha256": "b9f0e5ca038abe837b0007c8fe006f366a6f02009244ac57705a8a200e2301f4", + "bit_result_sha256": "28795393651ef4fbbc6232eb2b32f7b39b91fbd5ea6d2315583f350714698055", + "complex_receipt_sha256": "68600c734560bb155037e3973f7fbfb2fd1cb678485f8ac128c0b1e1bb1840a0", + "complex_assembly_sha256": "35ccaac474236b2e244f02cc599fbe4ddee783713f37ea623842ecb8de31f209", + "scope": "Rebuilt finite suppliers and exact composition. All-size/compiler, common-label/mutable-source, whole-call hosting, precision/tape and analytic transfer hypotheses remain conditional; not a full Lean theorem." + }, + "package_manifest_sha256": "e1b7998c8f7cb24f8674d250d0510f2b5b351b2ed0b35f17a17e6bacf3d9824b", + "assembly_sha256": "a7ab72bc4a3a00bd2147ae30dcf67448d0dfd69ab57e8f27f5ef520d0a560d01", + "independent_sha256": "932930a48de3a0d2b68fb3d1272521b6a6692b7ead886dbda608823f49030d35", + "price_sha256": "04bff9778b12a8dd878e0bf304c163d93aea09f3b7b3ebc878dab66e23054dd9", + "scope": "Exact finite X4 scalar/frame/phase/owner/invoice/assembly checks, bound to rebuilt PR589 and SW4 ancestry. Inherited all-size/compiler, common-label/mutable-source, whole-call hosting, precision/tape and analytic assumptions remain; not a full Lean theorem." + }, + "reused_ancestry": true, + "scope": "Required evidence presence, ordered stages and existing hash/mathematical bindings. Not execution authentication or a full multiplication proof." + }, + "refinement": { + "status": "PASS_X4_PRIMITIVE_GLOBAL_ADMISSION", + "base": "f567884aeb8851b6e794af1184119a3bfbe1e631", + "predecessor": "b31a870a3842b37f6ab97767c506ce91783632a2", + "kappa": "1661634653669567/1000000000000000000", + "saved_selected_real_component_primitives": 56448, + "saved_coefficient_work_operations": 36288, + "global_prefix_bits": 257, + "physical": 7682, + "lowering_sha256": "565fe81544f6d7e58bb17c12f37beae03a9397f66b0eae77e1ee6a4ee81743c9", + "invoice_sha256": "2751c2fd4e84aa90ecba0bfc30bc90d68f4b6a30e08b138df7834dce4613f4f1", + "assembly_sha256": "1372e5067c015b122b05d5dac551df96b66a923d81b7639b8305ceb73ba528b1", + "scope": "Fresh selected native/phase/wrapper/owner admission plus certified explicit primitive refinement and complete invoice/assembly. No new kappa; inherited all-size and analytic assumptions remain." + }, + "native_steps": [ + { + "step": "jx", + "exit_code": 0, + "seconds": 3.594 + }, + { + "step": "jx-control-C0_identity", + "exit_code": 0, + "seconds": 3.172 + }, + { + "step": "jx-control-C1_741_only", + "exit_code": 0, + "seconds": 2.562 + }, + { + "step": "jx-control-M1_one_pair_448", + "exit_code": 0, + "seconds": 3.047 + }, + { + "step": "jx-control-N1_drop_preread", + "exit_code": 0, + "seconds": 2.0 + }, + { + "step": "jx-control-N2_wrong_sign_preread", + "exit_code": 0, + "seconds": 3.718 + }, + { + "step": "jx-control-N3_plain_join_moved_reads", + "exit_code": 0, + "seconds": 3.656 + }, + { + "step": "jx-control-N4_raise_dim7_at_855", + "exit_code": 0, + "seconds": 2.563 + }, + { + "step": "layer-end-controls", + "exit_code": 0, + "seconds": 1201.297 + }, + { + "step": "native", + "exit_code": 0, + "seconds": 13.5 + }, + { + "step": "ledgers", + "exit_code": 0, + "seconds": 9.266 + }, + { + "step": "local-replay", + "exit_code": 0, + "seconds": 80.735 + }, + { + "step": "wrappers", + "exit_code": 0, + "seconds": 33.422 + }, + { + "step": "phases", + "exit_code": 0, + "seconds": 2041.469 + } + ], + "global_steps": [ + { + "name": "restore-parent", + "seconds": 10.266, + "exit_code": 0, + "log_sha256": "3aea2a4b68e7aaeadd9ffef649be0d25e2dff1535d9a61bffeaf6d92e55ba6a8" + }, + { + "name": "bind", + "seconds": 5.859, + "exit_code": 0, + "log_sha256": "78a081673d6b4fde10a86e6f767d53648b868d1f0cac2441d12951434ad7341b" + }, + { + "name": "emit", + "seconds": 31.0, + "exit_code": 0, + "log_sha256": "e2e13b5dd252e7209473f068993c91615705ba63614de998e233909ffa8f8b7d" + }, + { + "name": "audit", + "seconds": 116.906, + "exit_code": 0, + "log_sha256": "7f392b1834727b565c6f97e8c8cfba61e439db0742797d217913cfdb55f16117" + }, + { + "name": "invoice", + "seconds": 15.468, + "exit_code": 0, + "log_sha256": "06023deeec03cb062e55fc5c8fe2ad59efbfccd0a9af8836cf1356a0d16157dc" + }, + { + "name": "assembly", + "seconds": 2.282, + "exit_code": 0, + "log_sha256": "ab65a6031607ba15c7f9c8a70f2bc5a75f02492e7515eaa2a8b23e231c2fb6d3" + }, + { + "name": "admission-controls", + "seconds": 2.985, + "exit_code": 0, + "log_sha256": "34527ddfe1e53bec71dc5759eb9a26417be6d4e93e76cbf80575d9bafebd876b" + }, + { + "name": "bit-supplier-controls", + "seconds": 4.422, + "exit_code": 0, + "log_sha256": "c648542cd6dddbb154af7d02a41aaed1025603d9a4ab54f7c249d2b683e22249" + } + ], + "scope": "Fresh PR799 native/global replay with complete explicitly verified PR741 ancestry reuse; not a fresh bit or SW4 reconstruction." +} diff --git a/research/x4-primitive-admission/PROOF.md b/research/x4-primitive-admission/PROOF.md new file mode 100644 index 0000000000..606ee8b4dc --- /dev/null +++ b/research/x4-primitive-admission/PROOF.md @@ -0,0 +1,67 @@ +# Compiler refinement and admission argument + +This does not replace the recursive supplier or its logical word. It replaces +the primitive expansion of 56 disjoint, frame-zero target blocks. The literal +forward expansion has matrix `((-1/2,1/2),(1/2,1/2))`; the backward expansion +has matrix `((-1,1),(1,1))`, the inverse transpose. The independently implemented +two-row checker computes each emitted matrix from the instructions themselves. +It rejects a nonzero frame, a register outside the pair, a private scratch read, +an incorrect coefficient type, or an unequal endpoint. + +Both targets begin at the zero frame. Every primitive acts on those same targets +at that frame, with no recursive query or new carrier. At the end of each block, +all native registers therefore have exactly their retained values. The original +coefficient work can retain its entering dirt across the fused interval; the +unchanged suffix explicitly clears it before any read. Complete emitted scalar +replay checks that property with nine independent dirty private columns in +addition to all 728 native columns. Exact clearing is not an initialization +assumption. + +Each physical non-scalar event is retained literally and in order. The complete +source-bound native/frame/phase/wrapper receipts and controller audit are required +before refinement. Equality at each block boundary transports those operator +obligations to the primitive implementation: the changed block has no phase or +frame transition to readmit. This is a certified compiler refinement, rather +than a claim that the historical verifier natively parses the new primitive +format. That verifier checks the logical interface; this checker verifies the +concrete implementation and their relation. + +Original scalar bounds charge eleven primitives per component per pair. The +new literal expansions charge four. For 56 pairs and two real components this +is `56*2*(11-4)=784` per orientation. The original two ADD expansions use nine +coefficient-work operations per component per pair; the new block uses none. +That is 504 fewer operations in the predecessor's coefficient-work convention. +The original invoice has 72 complete calls, so its selected sums fall by 56,448 +and 36,288 respectively. Coefficient work is already included in the primitive +sum; the reductions are not added together. + +Logical macro, adapter, center, wrapper, child, stock, dispatch, owner, source +access, routing and old pervertex overcharge reserves are retained. The compiler +can expand a logical three-macro block jointly using the certified four-operation +word. All added primitive work is explicitly counted, and no new physical +frame adapter is required inside a frame-zero target block. Existing adapter +reserves cover the unchanged boundary/physical event interface. + +Complete emitted exact row-L1 and fractional-grid maxima agree with PR883's +retained whole-program comparison. The isolated forward pair temporarily grows +from 1 to 2, but the complete original absolute-envelope reserve already covers +the new exact maxima. Both final native values and the old logical prefix +contract remain valid at every block boundary. The refinement retains that +larger reserve and checks exact intermediate magnitude and denominator bounds; +it does not infer a rounded physical execution theorem from rational replay. + +The retained invoice function independently validates the original fresh +provider before its counts can be refined. The new lowering receipt and concrete +program digest are part of the generated provider contract. The full invoice +function then recomputes every selected call, parent/pervertex allowance, stock, +prefix, router, literal, mass, precision, tape, row and halving guard. A separate +candidate SPEC changes only the refined provider contract and local-count fields. +The unchanged assembly executes its conservative admission, exact moment +engines, bit surcharge/deficit checks, bootstrap, native correction and 47 strict +outer constraints. The recursive profile and final kappa are unchanged. + +All original source bytes remain immutable. PR865's source-versioned coverage +gate additionally rejects missing required evidence before the original binder. +These are finite operator/compiler/accounting checks under inherited all-size, +realization, hosting, precision/tape and analytic hypotheses, not a complete +integer multiplication theorem. diff --git a/research/x4-primitive-admission/README.md b/research/x4-primitive-admission/README.md new file mode 100644 index 0000000000..a453da1c19 --- /dev/null +++ b/research/x4-primitive-admission/README.md @@ -0,0 +1,77 @@ +# Admit PR883's explicit X4 primitive lowering + +Finite compiler refinement and complete accounting; no new kappa. + +Philipp's PR883 gives four-primitive implementations of the selected X4 word's +56 zero-frame precondition pairs. This package emits those literal instructions +inside a complete primitive program, preserves every physical frame, phase, +center and wrapper event, and binds the refinement to a complete selected replay. +An independent two-row matrix check validates every emitted pair. Complete +737-column scalar replay checks the emitted streams and all private clearing. + +The original macro ledger remains the logical proof interface. Its native +frame, phase, wrapper and whole-owner admission is valid because every changed +pair has the identical endpoint at frame zero, uses only the same two targets, +and introduces no recursive child or scratch register. All logical macros and +compiler adapter reserves remain charged. The new concrete implementation is +explicitly distinguished from the original macro ledger; see PROOF.md. + +The complete 72-call invoice saves **56,448 real-component primitives** and +**36,288 coefficient-work operations**. The latter uses the predecessor's +per-component accounting convention, not an additional saving to add to the +primitive bill. Physical stock remains 7682; the conservative prefix remains +257 of 512 bits. All finite guards and the unchanged exact assembly pass at +`1661634653669567/1000000000000000000`. No runtime measurement is claimed. + +## Reproduce + +Python 3.11+, standard library only for the lowering/admission package. A full +bit reconstruction additionally needs the predecessor's C++17/Boost toolchain. +Supply a complete selected PR799 replay and its actual PR741 ancestry directory: + +```sh +python -I -B research/x4-primitive-admission/admit.py \ + --replay /completed/frontier799/replay --ancestor /completed/frontier741 \ + --out /fresh/external/refined-admission +python -I -B research/x4-primitive-admission/test_controls.py \ + /fresh/external/refined-admission +``` + +If using the original public PR799 worker rather than PR865's guarded runner, +pass its work directory directly. The unchanged vendored PR865 coverage gate +checks all required ancestry stages/artifacts and selected-stage logs/results +before the mathematical binder. An existing or in-repository output is refused. +Native admission intentionally rejects disabled assertions. + +`lowering/PRIMITIVE-PROGRAMS.json.gz` is the emitted concrete implementation; +`LOWERING.json` retains its exact endpoint, prefix, paid-profile and source +bindings. `invoice/` holds the complete recomputation. `candidate-package/` +contains a separate copied assembly context and generated refinement contract. +`ASSEMBLY.json` and `RESULT.json` are published only after assembly succeeds. +Original source packages, selected records and defaults are never edited. + +Six emitted-prefix corruptions per orientation, immutable source drift and three +assembly controls must fail. The retained PR883 controls also reject all 672 +pair deletion/sign mutants. The original source package's independent pair +proof and seven source/interface controls were freshly reproduced separately. + +## Credit and scope + +PR883 at `b31a870a3842b37f6ab97767c506ce91783632a2` is by Philipp (@mightyOil). +Its exact original package is retained in `vendor/pr883`; no priority for the +factorization, gatewise comparison or optimality proof is claimed. PR865 supplies +the required-evidence gate, crediting Lucas (@ljste)'s PR838 and concurrent PR847. +Selected native/phase/controller/invoice/assembly sources retain Jeremy Kothe, +Chafik Boukhalfa, icekylinx, DreamingOfClouds, Rohan Arun, eumemic and predecessor +attribution. SOURCES.json pins the consumed sources and contexts. + +Overlap refresh through PR902 found ToikY's concurrent PR901, which changes +the following arbitrary-helper compensation and preserves this precondition. +Its candidate is not consumed; no combined saving or integration priority is +claimed. Main remains at the pinned f567884a context. + +Prepared for **nightangelflowerwin-ops** with substantial **OpenAI Codex +assistance** in integration, verification, mathematics and writing, Apache-2.0. +No independent human review, new exponent, measured speedup or full multiplication +theorem is claimed. All-size compilation, physical realization/hosting, +precision/tape and analytic transfer remain inherited assumptions. diff --git a/research/x4-primitive-admission/SOURCES.json b/research/x4-primitive-admission/SOURCES.json new file mode 100644 index 0000000000..eb4aa510e4 --- /dev/null +++ b/research/x4-primitive-admission/SOURCES.json @@ -0,0 +1,33 @@ +{ + "base": "f567884aeb8851b6e794af1184119a3bfbe1e631", + "pr883": "b31a870a3842b37f6ab97767c506ce91783632a2", + "repo_inputs": { + "research/gauge44-frames-x/code/invoice_allcold.py": "141bd2fd58bbfb5b8d0fc8f56f61c45586d5608a5af3487c6b883dd987f998ec", + "research/gauge44-frames-x/code/assemble.py": "4c270a996b380ab712f72b81173ab24f1c73203a33578f261bfbaa7e67d75aec", + "research/gauge44-frames-x/code/witness.py": "779c5172894b992131e85be1e592ed2a1aec8c287b872ff42007d36a7291e444", + "research/gauge44-frames-x/data/SPEC.json": "64817c60a4a2c1839bf12239cb1b7515a40bf8988229d81d4c9faa17b488c7d5", + "research/community-frontier799-audit/integrated799-replay.tar.gz": "70dfdfcf2ff95352c6020ee9dfca6dca9032b33c10daed3f3dc574c014f4e2cb", + "scripts/verify_frontier741_bindings.py": "eff455167e2fd0bc9a67d35241d0e69d8edc58f3a23e776dcfe8f500ca8e8d67", + "scripts/verify_frontier799_bindings.py": "43897b3c99212d6134870898a1840f32898aa1b3679b299e654901568ad7e19b", + "research/gauge44-frames-x/code/generated_identity.py": "c8af22719c0f3097a991a3f6ccac8f090afd2faba554745733d9ea88f2c25708" + }, + "vendor_inputs": { + "check.py": "67979352f3300d214832876ee0f1af7e5fe07bf6e388fbca1ef7fba6d1806b7e", + "CLAIM.md": "afb7cdebcbedb07eaa8efd0f0056eeccae87dcb08b93b36515633d4e31ea9f43", + "INDEPENDENT.json": "9b84910c051657c4e45b65bdd3aa2f73c2ff4b8e63d1be98da238b3ac7b38a54", + "independent_checker.py": "657fd7d8df0bce959ec0f9b754e4d09de533c717da2c9a7c70c5d79c7a2c7dfb", + "PAIR-PROOF.md": "0a60e63ce7100f80b110f248686b50b6e1864e21882d6a55aa3ef47e18d3ad71", + "README.md": "1f64ef77394ea397c4eea96248d413e22a86e7a46e132835b461e81130630151", + "RESULT.json": "b0259d424d0a33efc8bb312b209b5eeb0f64f6af122834e259341e013bcd1b85", + "SOURCES.json": "294002dd64abd75bf5fc70b2fd8f99bf5138426123929cbd3339aa67dcb371fa", + "test_verify.py": "c294bbc09931a1d7c0f954d210a176070348660b7bd04269600040d3d1a7aee6", + "VALIDATION.md": "c59ef9a6d5e4aa92452cb509b7563edf41a0d3d7eaaf7fee628b32945be19cd6", + "verify.py": "88d1f900bdeaa828384622abcca78aeaa9291406d8b155b191ad2a4ea247724f" + }, + "pr865": "7519ad89d7eb0e2f8c54f1424f5d9022eebda3f9", + "coverage_inputs": { + "pr741-sw4-v1.json": "7acd5033bc78e3f473718269edaa267c2785d84fbe95ccf6815a33dcf58c2756", + "README.md": "cae445bd3001732b488dd2e76f08ad47f02e762a8b903265f02502617cea6c07", + "verify_replay_coverage.py": "d603afac43702f953e54dda18f88dc826b19edd4f816e544205045399a51a87a" + } +} diff --git a/research/x4-primitive-admission/VALIDATION.md b/research/x4-primitive-admission/VALIDATION.md new file mode 100644 index 0000000000..268df7da54 --- /dev/null +++ b/research/x4-primitive-admission/VALIDATION.md @@ -0,0 +1,45 @@ +# Finite integration verification + +Windows CPython 3.11.9 at base f567884a. The original PR883 package was freshly +reproduced: complete 737-column scalar projections, 672 pair mutants, +independent 11,111-word matrix/BFS proof, and seven source/interface controls. + +A prototype then passed complete lowering/invoice/assembly against the earlier +source-bound fresh selected replay. The final implementation independently +checks every emitted pair matrix and mandates the unchanged vendored PR865 +coverage gate before admitting a baseline. It freezes the typed mathematical +result in EXPECTED.json, including the full selected primitive/work reductions. + +A new selected PR799 replay subsequently completed all native controls, ledgers, +scalar/frame/cone replay, wrappers, 2949 exact phase edges, owner emission/audit, +complete invoice, exact assembly, admission/bit controls and independent local +and price checks. It explicitly reused complete verified PR741 ancestry; no +fresh bit or SW4 reconstruction is claimed. The versioned coverage gate passed. +FRESH-REPLAY.json retains that binding and all native/global stage receipts. + +The final primitive refinement on that new replay passes the emitted complete +programs, independent pair matrices, full selected invoice and unchanged strict +assembly. Selected primitive work is 13,852,752, 56,448 below the retained bill. +Coefficient-work count is 6,834,184, reduced by 36,288 in the retained accounting +convention. Prefix remains 257/512 bits; physical stock remains 7682; kappa stays +1661634653669567/1000000000000000000. + +All sixteen new controls pass: missing instruction/pair, wrong sign, nonzero +frame, scratch read and Boolean coefficient in both orientations; immutable +source drift; undercharged complete invoice; failed precision guard; and omitted +lowering contract. The three assembly corruptions publish no assembly result. +The selected-record integrity checker passes. + +Relocation to another complete source clone, with an output directory containing +spaces, passes the full coverage, emitted lowering, invoice, assembly and frozen +typed-result comparison. This is a complete source-root relocation, not a claim +of minimal-root packaging. No network is used by the admission verifier. + +The unmodified earlier broad repository run stopped on eleven ten-second +subprocess timeouts in a historical test under Ubuntu WSL. It was not repeated +for this finite compiler refinement. No repository-wide, hosted-CI, physical +runtime or all-size theorem pass is claimed. + +Overlap refresh through PR902 leaves main at f567884a. Concurrent PR901 changes +the subsequent compensation, not these precondition blocks; its code and saving +are not consumed or added. Original PR883 and native-source credit are retained. diff --git a/research/x4-primitive-admission/admit.py b/research/x4-primitive-admission/admit.py new file mode 100644 index 0000000000..5f9acccf4e --- /dev/null +++ b/research/x4-primitive-admission/admit.py @@ -0,0 +1,150 @@ +"""Reissue the complete selected invoice for a certified primitive refinement. + +No mathematical source or selected record is edited. Original native/phase/ +wrapper/controller evidence is required and the unchanged assembly runs again. +Prepared with substantial OpenAI Codex assistance; Apache-2.0. +""" +import argparse +import copy +from fractions import Fraction +import importlib.util +from hashlib import sha256 +import json +import os +from pathlib import Path +import runpy +import shutil +import subprocess +import sys + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +sys.path.insert(0, str(HERE)) +from lowering import sources, read, emit, require, canonical + + +def dump(path, data): + path.write_bytes((json.dumps(data, indent=2) + '\n').encode()) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--replay', type=Path, required=True) + parser.add_argument('--ancestor', type=Path, required=True) + parser.add_argument('--out', type=Path, required=True) + args = parser.parse_args() + require(__debug__, 'Admission requires enabled assertions') + pins = sources() + expected = read(HERE / 'EXPECTED.json') + require(set(expected) == {'status', 'base', 'predecessor', 'kappa', + 'saved_selected_real_component_primitives', 'saved_coefficient_work_operations', + 'global_prefix_bits', 'physical'}, 'Frozen result field domain') + require(all(type(expected[k]) is int for k in ('saved_selected_real_component_primitives', + 'saved_coefficient_work_operations', 'global_prefix_bits', 'physical')), + 'Frozen result integer domain') + replay, out = args.replay.resolve(), args.out.resolve() + require(not out.exists() and not out.is_relative_to(ROOT), 'Fresh external output required') + # Use the unchanged PR865 gate in an explicitly configured source context. + # It checks complete coverage before calling the original mathematical binder. + sys.path.insert(0, str(ROOT / 'scripts')) + path = HERE / 'vendor/pr865/verify_replay_coverage.py' + module_spec = importlib.util.spec_from_file_location('x4_required_coverage', path) + coverage = importlib.util.module_from_spec(module_spec) + module_spec.loader.exec_module(coverage) + coverage.ROOT = ROOT + coverage.CONTRACT = HERE / 'vendor/pr865/pr741-sw4-v1.json' + guarded = coverage.check_selected(replay, args.ancestor.resolve()) + binding = guarded['selected_binding'] + require(binding['kappa'] == '1661634653669567/1000000000000000000', 'Pinned selected result') + out.mkdir(parents=True) + local = replay / 'native/local' + lowering = emit(local, out / 'lowering') + baseline = replay / 'global/global' + original_invoice = read(baseline / 'audit/PREFIX-AND-INVOICE.json') + source = ROOT / 'research/gauge44-frames-x' + multicold = ROOT / 'research/complex-k492-owner-repair/vendor/multicold' + os.environ.update(WITNESS_SPEC=str(source / 'data/SPEC.json'), + GAIN_PR564_SOURCE=str(multicold)) + for key in ('WITNESS_DISCOVER', 'WITNESS_RECORD', 'PYTHONOPTIMIZE'): + os.environ.pop(key, None) + ns = runpy.run_path(str(source / 'code/invoice_allcold.py'), run_name='x4_invoice_refinement') + run = ns['run'] + original_recount = run.__globals__['recount_provider'] + lowering_hash = sha256(canonical(lowering)).hexdigest() + + def refined_recount(directory, registry): + provider = original_recount(directory, registry) + # Original physical admission covers identical macro semantics. The + # concrete lowering relation is independently required here, before any + # numerical reduction is accepted into the complete invoice. + for name, digest in lowering['source_artifacts'].items(): + require(sha256((directory / name).read_bytes()).hexdigest() == digest, + 'Provider differs from audited lowering: ' + name) + for orientation, row in provider['local'].items(): + proof = lowering['orientations'][orientation] + require(row['real_component_primitives'] == proof['audit']['retained']['real_component_primitives'], 'Retained primitive count') + row['real_component_primitives'] = proof['emitted']['real_component_primitives'] + row['coefficient_work_primitive_count'] -= proof['coefficient_work_operations_removed'] + require(row['coefficient_work_primitive_count'] >= 0, 'Coefficient bill') + # Retain the larger inherited absolute-envelope bound. PR883's + # complete primitive replay separately checks exact prefix growth. + require(Fraction(row['prefix_l1']) >= Fraction(proof['emitted']['exact_prefix_row_l1']), + 'Conservative magnitude reserve') + require(proof['emitted']['exact_prefix_fraction_bits'] <= + proof['audit']['retained']['exact_prefix_fraction_bits'], + 'Retained fractional grid reserve') + provider['local_primitive_bound'] = max(z['real_component_primitives'] for z in provider['local'].values()) + provider['local_adapters'] * provider['compiler'] + provider['primitive_lowering'] = dict(receipt_sha256=lowering_hash, + program_content_sha256=lowering['primitive_program_content_sha256']) + return provider + + run.__globals__['recount_provider'] = refined_recount + vendor = multicold / 'vendor/pr558/vendor/pr552/complex-global/vendor531' + invoice = run(baseline / 'base', baseline / 'hosted', baseline / 'audit', out / 'invoice', + vendor / 'evidence/audit/PREFIX-AND-INVOICE.json') + require(original_invoice['selected_real_component_primitives'] - invoice['selected_real_component_primitives'] == 72 * 784, + 'Complete selected primitive saving') + require(invoice['global_prefix_bits'] == original_invoice['global_prefix_bits'] and invoice['physical'] == original_invoice['physical'], + 'Inherited prefix/stock must be retained') + require(all(invoice['strict_checks'].values()), 'Finite inequalities') + # Produce a separate candidate contract. Recompute and freeze only the + # fields whose certified primitive implementation changed. + candidate = out / 'candidate-package' + shutil.copytree(source, candidate) + spec = read(candidate / 'data/SPEC.json') + for pid, provider in invoice['providers'].items(): + desc = spec['providers'][pid] + desc['complete_contract'] = {k: v for k, v in provider.items() if k != 'artifacts'} + for orientation, row in provider['local'].items(): + desc['expected_local'][orientation] = {k: row[k] for k in ('events', 'macros', 'real_component_primitives', 'prefix_l1', 'coefficient_work_primitive_count')} + dump(candidate / 'data/SPEC.json', spec) + assembly_input = out / 'assembly-input' + (assembly_input / 'audit').mkdir(parents=True) + (assembly_input / 'hosted').mkdir() + shutil.copyfile(baseline / 'hosted/HOSTED.json', assembly_input / 'hosted/HOSTED.json') + shutil.copyfile(baseline / 'audit/OWNERS-AND-PROFILE.json', assembly_input / 'audit/OWNERS-AND-PROFILE.json') + shutil.copyfile(out / 'invoice/PREFIX-AND-INVOICE.json', assembly_input / 'audit/PREFIX-AND-INVOICE.json') + environment = dict(os.environ, WITNESS_SPEC=str(candidate / 'data/SPEC.json'), PYTHONDONTWRITEBYTECODE='1') + with (out / 'assembly.log').open('w', encoding='utf-8') as log: + result = subprocess.run([sys.executable, '-B', str(candidate / 'code/assemble.py'), + str(multicold), str(assembly_input), str(out / 'ASSEMBLY.json')], + env=environment, stdout=log, stderr=subprocess.STDOUT) + require(result.returncode == 0, 'Refined assembly failed: ' + (out / 'assembly.log').read_text()[-3000:]) + assembly = read(out / 'ASSEMBLY.json') + require(assembly['kappa'] == binding['kappa'], 'Unexpected exponent change') + summary = dict(status='PASS_X4_PRIMITIVE_GLOBAL_ADMISSION', base=pins['base'], predecessor=pins['pr883'], + kappa=assembly['kappa'], saved_selected_real_component_primitives=72*784, + saved_coefficient_work_operations=original_invoice['selected_coefficient_work_primitive_count']-invoice['selected_coefficient_work_primitive_count'], + global_prefix_bits=invoice['global_prefix_bits'], physical=invoice['physical'], + lowering_sha256=lowering_hash, invoice_sha256=sha256((out/'invoice/PREFIX-AND-INVOICE.json').read_bytes()).hexdigest(), + assembly_sha256=sha256((out/'ASSEMBLY.json').read_bytes()).hexdigest(), + scope='Fresh selected native/phase/wrapper/owner admission plus certified explicit primitive refinement and complete invoice/assembly. No new kappa; inherited all-size and analytic assumptions remain.') + require(canonical({k: summary[k] for k in expected}) == canonical(expected), + 'Refined mathematical result differs from frozen expectation') + require(sources() == pins, 'Consumed source bytes changed during admission') + dump(out / 'RESULT.json', summary) + print(summary['status'], 'saved=56448', 'kappa=' + assembly['kappa']) + + +if __name__ == '__main__': + main() diff --git a/research/x4-primitive-admission/lowering.py b/research/x4-primitive-admission/lowering.py new file mode 100644 index 0000000000..995e77a2a3 --- /dev/null +++ b/research/x4-primitive-admission/lowering.py @@ -0,0 +1,134 @@ +"""Concrete source-bound X4 primitive lowering, following Philipp's PR883. + +Prepared for nightangelflowerwin-ops with substantial OpenAI Codex assistance. +Apache-2.0. Original sources and attribution are retained in vendor/pr883. +""" +import gzip +from fractions import Fraction as Q +from hashlib import sha256 +import importlib.util +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def read(path): + data = Path(path).read_bytes() + return json.loads(gzip.decompress(data) if str(path).endswith('.gz') else data) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(',', ':'), allow_nan=False).encode() + + +def sources(): + pins = read(HERE / 'SOURCES.json') + for name, digest in pins['repo_inputs'].items(): + require(sha256((ROOT / name).read_bytes()).hexdigest() == digest, 'Repository source drift: ' + name) + for name, digest in pins['vendor_inputs'].items(): + require(sha256((HERE / 'vendor/pr883' / name).read_bytes()).hexdigest() == digest, 'PR883 source drift: ' + name) + for name, digest in pins['coverage_inputs'].items(): + require(sha256((HERE / 'vendor/pr865' / name).read_bytes()).hexdigest() == digest, 'PR865 source drift: ' + name) + return pins + + +def predecessor(): + spec = importlib.util.spec_from_file_location('p883_lowering', HERE / 'vendor/pr883/verify.py') + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +def check_prefix(stream, pairs, backward): + """Independent two-row matrix check of every emitted physical block.""" + require(stream[0] == ['phase', 'zero_frame_precondition'], 'Primitive entrance phase') + for index, (x, y) in enumerate(pairs): + registers = {('L', x): 0, ('L', y): 1} + rows = [[Q(1), Q(0)], [Q(0), Q(1)]] + for event in stream[1 + 4*index:1 + 4*(index+1)]: + require(len(event) == 3 and event[0] == 'primitive' and type(event[2]) is int and event[2] == 0, + 'Primitive zero-frame block') + op = event[1] + require(tuple(op[1]) in registers, 'Primitive target escapes pair') + target = registers[tuple(op[1])] + if op[0] == 'add': + require(len(op) == 4 and tuple(op[2]) in registers and tuple(op[1]) != tuple(op[2]) and + type(op[3]) is int and op[3] in (-1, 1), 'Primitive signed source') + source = registers[tuple(op[2])] + rows[target] = [a + op[3]*b for a, b in zip(rows[target], rows[source])] + else: + require(len(op) == 2 and op[0] in ('neg', 'half', 'double'), 'Primitive two-register alphabet') + factor = {'neg': Q(-1), 'half': Q(1, 2), 'double': Q(2)}[op[0]] + rows[target] = [factor*a for a in rows[target]] + expected = [[Q(-1), Q(1)], [Q(1), Q(1)]] if backward else [[Q(-1,2),Q(1,2)],[Q(1,2),Q(1,2)]] + require(rows == expected, 'Primitive pair matrix differs') + + +def emit(directory, out): + """Expand the actual fresh provider; retain every non-scalar event literally.""" + sources() + module = predecessor() + expected_word, expected_programs, expected_checks = module.load_inputs(ROOT) + word = read(directory / 'CANONICAL-WORD.json.gz') + programs = read(directory / 'LOCAL-PROGRAMS.json.gz') + checks = read(directory / 'LOCAL-CHECKS.json') + require(canonical(word) == canonical(expected_word), 'Fresh X4 word differs from source') + require(canonical(programs) == canonical(expected_programs), 'Fresh logical program differs from source') + require(canonical(checks) == canonical(expected_checks), 'Fresh logical invoice differs from source') + pairs = module.pairs(word) + receipt, streams = {}, {} + for orientation in ('forward', 'backward'): + backward = orientation == 'backward' + audit = module.run_orientation(word, programs[orientation], checks[orientation], pairs, backward) + events = programs[orientation] + stream = [events[0]] + # A fused block still has three logical macros for conservative compiler + # reserves; this concrete expansion implements their joint endpoint. + for x, y in pairs: + stream.extend([['primitive', list(op), 0] for op in module.replacement(x, y, backward)]) + cursor = 1 + 3 * len(pairs) + for event in events[cursor:]: + if event[0] == 'scalar': + stream.extend([['primitive', list(op), event[2]] for op in module.lower(event[1])]) + else: + stream.append(event) + # Replay the emitted instructions themselves, not just the builder's + # audited recipe. Physical non-scalar operators remain hash-bound to + # the freshly checked source word, phase and wrapper receipts. + replay = module.Replay(2 * word['v'] + word['R']) + check_prefix(stream, pairs, backward) + for event in stream: + if event[0] == 'primitive': + op = event[1] + op = tuple(tuple(x) if isinstance(x, list) else x for x in op) + replay.apply(op) + replay.endpoint(2 * word['v'] + word['R'], word['v'], backward) + require(replay.count * 2 == audit['replacement']['real_component_primitives'], 'Emitted primitive bill') + require(replay.receipt() == audit['replacement'], 'Emitted full prefix/clearing audit') + require([e for e in stream if e[0] != 'primitive'] == + [e for e in events if e[0] != 'scalar'], 'Physical event stream changed') + streams[orientation] = stream + receipt[orientation] = dict(audit=audit, emitted= replay.receipt(), + stream_sha256=sha256(canonical(stream)).hexdigest(), + logical_macros_retained=checks[orientation]['scalar_macros'], + coefficient_work_operations_removed=504) + out.mkdir() + data = canonical(streams) + (out / 'PRIMITIVE-PROGRAMS.json.gz').write_bytes(gzip.compress(data, mtime=0)) + result = dict(status='PASS_SOURCE_BOUND_X4_PRIMITIVE_LOWERING', orientations=receipt, + source_artifacts={name: sha256((directory / name).read_bytes()).hexdigest() + for name in ('CANONICAL-WORD.json.gz', 'LOCAL-PROGRAMS.json.gz', 'LOCAL-CHECKS.json', + 'INDEPENDENT-LOCAL-REPLAY.json', 'CLIFFORD-RECIPES.json', + 'CLIFFORD-REVIEW.json', 'RESIDUAL-ADAPTERS.json', 'WRAPPER-CHECKS.json')}, + primitive_program_content_sha256=sha256(data).hexdigest(), + pair_count=len(pairs), pair_instruction_controls=module.controls(pairs), + scope='Explicit primitive compiler refinement; physical word/phase/wrapper stream unchanged. No new recursive profile or kappa.') + (out / 'LOWERING.json').write_bytes((json.dumps(result, indent=2) + '\n').encode()) + return result diff --git a/research/x4-primitive-admission/test_controls.py b/research/x4-primitive-admission/test_controls.py new file mode 100644 index 0000000000..af4dc9a647 --- /dev/null +++ b/research/x4-primitive-admission/test_controls.py @@ -0,0 +1,88 @@ +"""Adverse controls for the concrete emitted prefix and source boundary.""" +from copy import deepcopy +import json +import os +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +from lowering import read, require, sources, predecessor, check_prefix + + +def main(output): + sources() + module = predecessor() + word, _, _ = module.load_inputs(HERE.parents[1]) + pairs = module.pairs(word) + streams = read(output / 'lowering/PRIMITIVE-PROGRAMS.json.gz') + rejected = [] + for orientation, stream in streams.items(): + backward = orientation == 'backward' + check_prefix(stream, pairs, backward) + mutations = [] + changed = deepcopy(stream); del changed[1] + mutations.append(('missing_instruction', changed)) + changed = deepcopy(stream); changed[1][1][3] *= -1 + mutations.append(('wrong_sign', changed)) + changed = deepcopy(stream); changed[1][2] = 1 + mutations.append(('nonzero_frame', changed)) + changed = deepcopy(stream); changed[1][1][2] = ['W', 0] + mutations.append(('scratch_source', changed)) + changed = deepcopy(stream); changed[1][1][3] = True + mutations.append(('boolean_coefficient', changed)) + changed = deepcopy(stream); del changed[1:5] + mutations.append(('missing_pair', changed)) + for name, changed in mutations: + try: + check_prefix(changed, pairs, backward) + except (ValueError, IndexError, TypeError) as error: + rejected.append(orientation + ':' + name) + else: + raise ValueError('Primitive corruption accepted: ' + name) + # Source preflight rejects even whitespace-only changes in immutable inputs. + path = HERE / 'vendor/pr883/PAIR-PROOF.md' + original = path.read_bytes() + try: + path.write_bytes(original + b' ') + try: + sources() + except ValueError: + rejected.append('source_drift') + else: + raise ValueError('Source drift accepted') + finally: + path.write_bytes(original) + original_invoice = read(output / 'invoice/PREFIX-AND-INVOICE.json') + with tempfile.TemporaryDirectory(prefix='x4-invoice-controls-') as tmp: + parent = Path(tmp) + env = dict(os.environ, WITNESS_SPEC=str(output/'candidate-package/data/SPEC.json'), + PYTHONDONTWRITEBYTECODE='1') + env.pop('PYTHONOPTIMIZE', None) + mutations = [] + changed = deepcopy(original_invoice); changed['selected_real_component_primitives'] -= 1 + mutations.append(('undercharged_complete_invoice', changed)) + changed = deepcopy(original_invoice); changed['strict_checks']['precision'] = False + mutations.append(('failed_precision_admission', changed)) + changed = deepcopy(original_invoice); del changed['providers']['gauge44']['primitive_lowering'] + mutations.append(('omitted_lowering_contract', changed)) + for name, changed in mutations: + case = parent/name + shutil.copytree(output/'assembly-input', case) + (case/'audit/PREFIX-AND-INVOICE.json').write_bytes((json.dumps(changed)+'\n').encode()) + result = subprocess.run([sys.executable,'-B',str(output/'candidate-package/code/assemble.py'), + str(HERE.parents[1]/'research/complex-k492-owner-repair/vendor/multicold'), + str(case),str(case/'ASSEMBLY.json')], env=env, capture_output=True, text=True) + require(result.returncode != 0 and 'AssertionError' in result.stderr, + 'Assembly corruption accepted or wrong failure: '+name+' '+result.stderr[-500:]) + require(not (case/'ASSEMBLY.json').exists(), 'Failed admission published a result') + rejected.append(name) + require(len(rejected) == 16, 'Control coverage') + print('PASS_X4_PRIMITIVE_ADMISSION_CONTROLS', json.dumps(rejected)) + + +if __name__ == '__main__': + main(Path(sys.argv[1]).resolve()) diff --git a/research/x4-primitive-admission/vendor/pr865/README.md b/research/x4-primitive-admission/vendor/pr865/README.md new file mode 100644 index 0000000000..0db0a6d264 --- /dev/null +++ b/research/x4-primitive-admission/vendor/pr865/README.md @@ -0,0 +1,120 @@ +# Enforce PR838's coverage contract in the selected replay + +Lucas (@ljste)'s PR838 showed that the PR741 composition binding accepted +omitted ancestry stages and artifacts. This follow-up tests the complete +selected PR799 binding on actual archive files and enforces a versioned +coverage contract in the standard Makefile replay paths. + +The pristine archived PR799 and historical PR741 replays pass. Removing +`ancestor/complex/local/CLIFFORD-REVIEW.json` and its receipt inventory entry +still makes the original **complete PR799 binding** return +`PASS_REBUILT_PR589_PR799_COMPOSITION`. The new check rejects that witness. +This is an evidence-admission defect, not a disproved scalar identity or +counterexample to the multiplication theorem. + +## Implementation + +`certificates/replay-coverage/pr741-sw4-v1.json` defines the exact ordered +22-stage sequence and all 44 required artifacts, separately from the candidate +receipt. The producer, manifest and spec are SHA-256 pinned. Stage names and +the 34 explicit artifact declarations are independently compared with the +producer AST; the remaining ten local output names are explicit in the +source-bound contract. The current X4 consumer and producer scripts have +their own version pins. A new producer requires a reviewed contract version. + +`scripts/verify_replay_coverage.py` checks exact inventory and stage sequence, +execution-record equality, strict integer exit codes, containment and existing +hash bindings, then runs every original mathematical binding check. For PR799 +it also checks top-level execution logs, the stored ancestry binding and result, +and existence of all named native logs. Native stage records have no log +digests; this check does not pretend otherwise. + +`scripts/verify_frontier_complete.py` executes the unchanged historical cold +runner inside `work/replay/` and only then atomically publishes the public +`work/RESULT.json`, alongside `COVERAGE.json`. An explicitly reused ancestor must +pass coverage **before** any new native/global work starts. Both standard +`make frontier741-verify` and `make frontier799-verify` now invoke this runner; +`make verify` consequently enforces coverage on its historical PR741 stage. +Both existing cold-replay CI workflows also enforce this gate, with triggers +for contract/entrypoint changes and corrected nested artifact upload paths. +The old runners and binding scripts remain byte-identical because the selected +record pins them as reviewed proof supplements. Direct old-script invocations +retain their historical semantics; they are not the strengthened entrypoint. + +The existing PR799 regression fixture uses ordinary copies instead of symlinks +so the same input bytes are tested without requiring Windows symlink privileges. + +## Reproduce + +Standard library, Python 3.11+; no solver or network: + +```sh +python -I -B research/required-replay-coverage/verify.py +python -I -B research/required-replay-coverage/check_package.py +python -B -m unittest discover -s tests -p 'test_replay_coverage.py' -v +python -B -m unittest discover -s tests -p 'test_frontier7*bindings.py' -v +``` + +The deterministic receipt records the old/current outcome for every mutation. +Expected: `PASS_REQUIRED_REPLAY_COVERAGE 112 original PR799 accepts; 118 enforced rejections; valid historical and selected replays accepted`. +The matrix covers all 22 stage replacements, all 44 single inventory omissions, +all 42 otherwise-deletable ancestor artifacts, empty inventory, inconsistent +execution order, six additional type/hash/admission controls and two missing +selected logs. A public current-binding CLI witness is reproduced, the new +CLI rejects it, and incomplete ancestor reuse is rejected before launch. +Contract tests reject unknown versions, producer drift and escaping paths. + +Check an existing complete historical PR799 replay, or the `replay/` directory +of a completed strengthened run: + +```sh +python -I -B scripts/verify_replay_coverage.py --frontier 799 \ + --work /absolute/path/to/replay --ancestor /absolute/path/to/ancestor +``` + +Omit `--ancestor` only when its recorded reuse flag is false and the complete +ancestor is inside the replay's `ancestor/` directory. The explicit path avoids +guessing a relocated reuse directory from old logs. A fresh run can use: + +```sh +python -B scripts/verify_frontier_complete.py --frontier 799 \ + --work /fresh/outside/repository/path --ancestor /complete/source-bound/ancestor +``` + +Without an ancestor argument, the original runner rebuilds it from scratch. +Coverage adds linear work in the artifact bytes plus small fixed manifest/AST +checks; it does not weaken, skip or replace original verification stages. + +## Sources, credit and limits + +Base: `f567884aeb8851b6e794af1184119a3bfbe1e631`. +PR838: `2a50020bb9564229874cbfbdc112e17b235bacfc`. +Input archives and historical checkers are pinned in SOURCES.json. The contract +was derived from the pinned producer and complete archive, not a mutable +candidate's self-declared inventory. The omission-domain design follows PR838; +its original audit is credited and not superseded or described as repaired in +place. No original PR838 source is edited or imported without attribution. + +Credit Douglas Colkitt's reviewed checkers and retained replay; Chafik +Boukhalfa's PR741 construction; PR799's X4 construction; DreamingOfClouds' +PR589 transport on eumemic's PR555 supplier; all original predecessor notices. +Prepared for **nightangelflowerwin-ops** with substantial **OpenAI Codex** +assistance in implementation, testing and writing. Apache-2.0. No independent +human review is claimed. Concurrent PR841 addresses proof-pointer binding, +not these stage/artifact omissions. + +Concurrent **PR847**, Chinmay (@chinmayarvind23), head +`72b8406b96ea2e0f37bb5143f594e12d4817c92a`, arrived during validation with +the basic public Make/CI coverage integration and a separately published +success record. That design is explicitly credited; no priority for it is +claimed. This independent implementation adds version-pinned producer and +consumer contracts, full current PR799 reachability evidence, checks on the +selected replay's own logs/result, strict exit metadata, offline source-drift +controls and a fresh native/global replay. The older bindings and selected +proof pins remain unchanged in both approaches. No PR847 code is imported. + +Presence and hash consistency do not authenticate execution or independently +re-prove every mathematical artifact. Inherited all-size/compiler, common-label, +mutable-source, hosting, precision/tape and analytic conditions remain. +No kappa, selected record, construction source or `upstream/` byte is changed. +Validation, including any incomplete repository-wide run, is recorded separately. diff --git a/research/x4-primitive-admission/vendor/pr865/pr741-sw4-v1.json b/research/x4-primitive-admission/vendor/pr865/pr741-sw4-v1.json new file mode 100644 index 0000000000..1acec5f34c --- /dev/null +++ b/research/x4-primitive-admission/vendor/pr865/pr741-sw4-v1.json @@ -0,0 +1,94 @@ +{ + "schema": "integer-mult-replay-coverage-v1", + "id": "pr741-sw4-v1", + "producer": "research/complex-sw4-frame8/verify.py", + "producer_sha256": "7706065e3d2934ea493910638b40e6285348d337507e0fb695d8d1e536926637", + "manifest_sha256": "b9b39c206fcd2613382b0dcbda23a371e8781d1bedaf8e2f8e7df1e79dc1fa89", + "spec_sha256": "7fc2bd2e3c0ac13729c1fa1f0f327a4eb7c72373ba58e5ed3954b30e23c803be", + "stages": [ + "ancestral558-fresh", + "gauge44-exact-construction", + "notri56-construction", + "notri-control-g44", + "layered66-construction", + "p6n-cold72-construction", + "four-promotions", + "promotion-controls", + "sw4-read-exchanges", + "eight-B-frame-construction", + "all728-columns-native", + "both-native-ledgers", + "independent-native-controls", + "residual-wrappers", + "all-native-phase-edges", + "independent-scalar-frames-cones", + "inherited-cold-controls", + "eight-frame-controls", + "owner-construction-controls", + "strict-global-admission", + "independent-literal-map-moment", + "independent-two-engine-outer47" + ], + "artifacts": [ + "ANCESTRAL-LINK.json", + "FRAME-CONTROLS.json", + "INDEPENDENT-LOCAL.json", + "INDEPENDENT-MAP.json", + "INDEPENDENT-PRICE.json", + "OWNER-CONSTRUCTION-CONTROLS.json", + "PROMO-CONTROLS.json", + "RECONSTRUCTED-OWNERS.json.gz", + "RESULT.json", + "STAGES.json", + "cold-controls/COLD-END-CONTROLS.json", + "frames/BUILD.json", + "frames/FULL-WORD.json.gz", + "gauge44/STEPS.json", + "global-replay/ADMISSION-CONTROLS.json", + "global-replay/ASSEMBLY.json", + "global-replay/BIT-SUPPLIER-CONTROLS.json", + "global-replay/REPLAY.json", + "global-replay/STAGES.json", + "global-replay/global/audit/ASYNC-AUDIT.json", + "global-replay/global/audit/OWNERS-AND-PROFILE.json", + "global-replay/global/audit/PREFIX-AND-INVOICE.json", + "layered66/STEPS.json", + "layered66/controls/COLD-END-CONTROLS.json", + "layered66/swap/PIVOT-SWAP.json", + "local/CANONICAL-WORD.json.gz", + "local/CLIFFORD-RECIPES.json", + "local/CLIFFORD-REVIEW.json", + "local/FULL-WORD.json.gz", + "local/INDEPENDENT-LOCAL-REPLAY.json", + "local/LOCAL-CHECKS.json", + "local/LOCAL-PROGRAMS.json.gz", + "local/RESIDUAL-ADAPTERS.json", + "local/SCALAR-FRAME-AUDIT.json", + "local/WRAPPER-CHECKS.json", + "notri-control/STEPS.json", + "notri56/STEPS.json", + "notri56/cold44/CONSTRUCTION.json", + "p6n/STEPS.json", + "p6n/controls/COLD-END-CONTROLS.json", + "p6n/p6n/FULL-WORD.json.gz", + "promoted/FULL-WORD.json.gz", + "sw4/BUILD.json", + "sw4/FULL-WORD.json.gz" + ], + "selected": { + "id": "pr799-x4-v1", + "source_sha256": { + "scripts/verify_frontier799.py": "19fe1b32079095160dc00fe2f7df75e0fcbc82cff37f7159b755c8a63bd5ce99", + "scripts/verify_frontier799_bindings.py": "43897b3c99212d6134870898a1840f32898aa1b3679b299e654901568ad7e19b", + "research/gauge44-frames-x/construction/jx/reproduce_jx.py": "5c7afebb4eb7fcdeb7e971cfbc457cf071850e2da21c3c71295efdd453c2399c", + "research/gauge44-frames-x/verify_global.py": "16bd5e54598592e92e210f99065348c5df261b8350fdc688072ce053d15b088a" + }, + "stages": [ + "manifest", + "native", + "global", + "independent-local", + "independent-price" + ] + } +} diff --git a/research/x4-primitive-admission/vendor/pr865/verify_replay_coverage.py b/research/x4-primitive-admission/vendor/pr865/verify_replay_coverage.py new file mode 100644 index 0000000000..59e1fdaf66 --- /dev/null +++ b/research/x4-primitive-admission/vendor/pr865/verify_replay_coverage.py @@ -0,0 +1,151 @@ +#!/usr/bin/env python3 +"""Versioned evidence coverage, supplementary to immutable frontier bindings. + +Credit Lucas (@ljste), PR838, for the ancestor-coverage audit. Prepared for +nightangelflowerwin-ops with substantial OpenAI Codex assistance. Apache-2.0. +""" +import argparse +import ast +from hashlib import sha256 +import json +from pathlib import Path, PurePosixPath +import sys + +sys.path.insert(0, str(Path(__file__).resolve().parent)) +ROOT = Path(__file__).resolve().parents[1] +CONTRACT = ROOT / 'certificates/replay-coverage/pr741-sw4-v1.json' + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def read(path): + return json.loads(Path(path).read_bytes()) + + +def digest(path): + return sha256(Path(path).read_bytes()).hexdigest() + + +def artifact_path(directory, name): + require(type(name) is str and name and '\\' not in name, 'Invalid evidence path') + relative = PurePosixPath(name) + require(not relative.is_absolute() and '..' not in relative.parts and + relative.as_posix() == name and ':' not in name, 'Invalid evidence path') + path = (directory / name).resolve() + require(path.is_relative_to(directory.resolve()), 'Evidence escapes replay directory') + return path + + +def contract(): + value = read(CONTRACT) + require(value['schema'] == 'integer-mult-replay-coverage-v1' and + value['id'] == 'pr741-sw4-v1', 'Unsupported replay coverage version') + producer = ROOT / value['producer'] + require(value['producer'] == 'research/complex-sw4-frame8/verify.py' and + digest(producer) == value['producer_sha256'], 'Coverage producer version differs') + require(digest(producer.parent / 'MANIFEST.json') == value['manifest_sha256'] and + digest(producer.parent / 'data/SPEC.json') == value['spec_sha256'], 'Coverage package version differs') + tree = ast.parse(producer.read_bytes()) + calls = [n.value for n in tree.body if isinstance(n, ast.Expr) and + isinstance(n.value, ast.Call) and isinstance(n.value.func, ast.Name) and n.value.func.id == 'run'] + require([ast.literal_eval(call.args[0]) for call in calls] == value['stages'], 'Contract stages differ from producer') + lists = [n.value for n in tree.body if isinstance(n, ast.Assign) and + any(isinstance(t, ast.Name) and t.id == 'files' for t in n.targets)] + require(len(lists) == 1, 'Producer artifact declaration differs') + fixed = ast.literal_eval(lists[0]) + require(type(value['artifacts']) is list and len(value['artifacts']) == 44 and + len(set(value['artifacts'])) == 44 and set(fixed) <= set(value['artifacts']), 'Contract artifact inventory differs') + dynamic = set(value['artifacts']) - set(fixed) + require(len(fixed) == 34 and len(dynamic) == 10 and + all(name.startswith('local/') for name in dynamic), 'Contract local artifact inventory differs') + for name in value['stages']: + require(type(name) is str and '/' not in name and '\\' not in name and ':' not in name, 'Invalid stage name') + return value + + +def check_ancestor(bit, complex_dir): + """Require source-versioned complete coverage, then all original checks.""" + value = contract() + receipt = read(complex_dir / 'RECEIPT.json') + stages = receipt['stages'] + require(type(stages) is list and [s['name'] for s in stages] == value['stages'], 'Required ancestry stage sequence differs') + require(all(type(s['exit_code']) is int and s['exit_code'] == 0 for s in stages), 'Required ancestry stage failed') + artifacts = receipt['artifacts'] + require(type(artifacts) is dict and set(artifacts) == set(value['artifacts']), 'Required ancestry artifact inventory differs') + require(read(complex_dir / 'STAGES.json') == stages, 'Ancestry execution record differs from receipt') + for name, expected in artifacts.items(): + require(type(expected) is str and digest(artifact_path(complex_dir, name)) == expected, 'Required ancestry artifact hash differs: ' + name) + for stage in stages: + require(type(stage['log_sha256']) is str and + digest(artifact_path(complex_dir, stage['name'] + '.log')) == stage['log_sha256'], 'Required ancestry log differs') + from verify_frontier741_bindings import check + return check(bit, complex_dir) + + +def check_selected(work, ancestor=None): + """Enforce coverage in the complete selected PR799 replay, without reuse guesses.""" + ancestry_record = read(work / 'ANCESTRY.json') + require(type(ancestry_record['reused']) is bool, 'Invalid ancestry reuse flag') + require(ancestor is not None or ancestry_record['reused'] is False, + 'Explicit ancestor path required for reused evidence') + parent = ancestor if ancestor is not None else work / 'ancestor' + ancestry = check_ancestor(parent / 'bit', parent / 'complex') + selected = contract()['selected'] + require(selected['id'] == 'pr799-x4-v1', 'Unsupported selected coverage version') + for name, expected_hash in selected['source_sha256'].items(): + require(digest(artifact_path(ROOT, name)) == expected_hash, 'Selected coverage producer version differs: ' + name) + require(ancestry_record['binding'] == ancestry, 'Ancestry receipt binding differs') + expected = ([] if ancestry_record['reused'] else ['ancestor']) + selected['stages'] + stages = read(work / 'STEPS.json') + require(type(stages) is list and [s['name'] for s in stages] == expected and + all(type(s['exit_code']) is int and s['exit_code'] == 0 for s in stages), 'Required selected stage sequence differs') + for stage in stages: + require(digest(artifact_path(work, stage['name'] + '.log')) == stage['log_sha256'], 'Selected stage log differs') + # The original binding independently validates the named native stages. + # Also require each corresponding native log to exist. Native STEPS.json + # does not contain log digests, so no authentication claim is made here. + for stage in read(work / 'native/STEPS.json'): + require(type(stage['exit_code']) is int and stage['exit_code'] == 0, 'Required native stage failed') + require(artifact_path(work / 'native', stage['step'] + '.log').is_file(), 'Required native stage log missing') + from verify_frontier799_bindings import check + result = check(parent, work / 'native', work / 'global', + work / 'INDEPENDENT-LOCAL.json', work / 'INDEPENDENT-PRICE.json') + recorded = read(work / 'RESULT.json') + require(recorded['status'] == result['status'] and recorded['kappa'] == result['kappa'] and + recorded['ancestry'] == result['ancestry'] and + recorded['reused_ancestry'] is ancestry_record['reused'], 'Selected result binding differs') + return dict(status='PASS_COMPLETE_PR799_REPLAY_COVERAGE', kappa=result['kappa'], + decimal=result['decimal'], + coverage_contract=value_id(), contract_sha256=digest(CONTRACT), + selected_binding=result, reused_ancestry=ancestry_record['reused'], + scope='Required evidence presence, ordered stages and existing hash/mathematical bindings. Not execution authentication or a full multiplication proof.') + + +def value_id(): + return 'pr741-sw4-v1' + + +def main(): + p = argparse.ArgumentParser(description=__doc__) + p.add_argument('--frontier', choices=['741', '799'], required=True) + p.add_argument('--work', type=Path, required=True) + p.add_argument('--ancestor', type=Path) + p.add_argument('--out', type=Path) + a = p.parse_args() + if a.frontier == '741': + require(a.ancestor is None, 'Ancestor flag is only for PR799') + result = check_ancestor(a.work / 'bit', a.work / 'complex') + result = dict(status='PASS_COMPLETE_PR741_REPLAY_COVERAGE', binding=result, + coverage_contract=value_id(), contract_sha256=digest(CONTRACT)) + else: + result = check_selected(a.work, a.ancestor) + if a.out: + a.out.write_text(json.dumps(result, indent=2) + '\n', encoding='utf-8') + print(result['status']) + + +if __name__ == '__main__': + main() diff --git a/research/x4-primitive-admission/vendor/pr883/CLAIM.md b/research/x4-primitive-admission/vendor/pr883/CLAIM.md new file mode 100644 index 0000000000..0be6c44328 --- /dev/null +++ b/research/x4-primitive-admission/vendor/pr883/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-primitive-admission/vendor/pr883/INDEPENDENT.json b/research/x4-primitive-admission/vendor/pr883/INDEPENDENT.json new file mode 100644 index 0000000000..aadd5533e1 --- /dev/null +++ b/research/x4-primitive-admission/vendor/pr883/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-primitive-admission/vendor/pr883/PAIR-PROOF.md b/research/x4-primitive-admission/vendor/pr883/PAIR-PROOF.md new file mode 100644 index 0000000000..c83af0fb1b --- /dev/null +++ b/research/x4-primitive-admission/vendor/pr883/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-primitive-admission/vendor/pr883/README.md b/research/x4-primitive-admission/vendor/pr883/README.md new file mode 100644 index 0000000000..e1c3ec255f --- /dev/null +++ b/research/x4-primitive-admission/vendor/pr883/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-primitive-admission/vendor/pr883/RESULT.json b/research/x4-primitive-admission/vendor/pr883/RESULT.json new file mode 100644 index 0000000000..a9a1deeab1 --- /dev/null +++ b/research/x4-primitive-admission/vendor/pr883/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-primitive-admission/vendor/pr883/SOURCES.json b/research/x4-primitive-admission/vendor/pr883/SOURCES.json new file mode 100644 index 0000000000..b6b0a0b5bf --- /dev/null +++ b/research/x4-primitive-admission/vendor/pr883/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-primitive-admission/vendor/pr883/VALIDATION.md b/research/x4-primitive-admission/vendor/pr883/VALIDATION.md new file mode 100644 index 0000000000..af90bdf276 --- /dev/null +++ b/research/x4-primitive-admission/vendor/pr883/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-primitive-admission/vendor/pr883/check.py b/research/x4-primitive-admission/vendor/pr883/check.py new file mode 100644 index 0000000000..f8d6471769 --- /dev/null +++ b/research/x4-primitive-admission/vendor/pr883/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-primitive-admission/vendor/pr883/independent_checker.py b/research/x4-primitive-admission/vendor/pr883/independent_checker.py new file mode 100644 index 0000000000..b66d423372 --- /dev/null +++ b/research/x4-primitive-admission/vendor/pr883/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-primitive-admission/vendor/pr883/test_verify.py b/research/x4-primitive-admission/vendor/pr883/test_verify.py new file mode 100644 index 0000000000..1db549976c --- /dev/null +++ b/research/x4-primitive-admission/vendor/pr883/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-primitive-admission/vendor/pr883/verify.py b/research/x4-primitive-admission/vendor/pr883/verify.py new file mode 100644 index 0000000000..ae89da5598 --- /dev/null +++ b/research/x4-primitive-admission/vendor/pr883/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() From 1f0cd934f83ddf2f14f20275ecca072c5b85a7b9 Mon Sep 17 00:00:00 2001 From: nightangelflowerwin-ops Date: Tue, 13 Oct 2026 05:22:01 -0700 Subject: [PATCH 2/2] Record user-selected integration scope and overlap --- research/x4-primitive-admission/CLAIM.md | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) create mode 100644 research/x4-primitive-admission/CLAIM.md diff --git a/research/x4-primitive-admission/CLAIM.md b/research/x4-primitive-admission/CLAIM.md new file mode 100644 index 0000000000..cc884340fd --- /dev/null +++ b/research/x4-primitive-admission/CLAIM.md @@ -0,0 +1,17 @@ +# User-selected PR883 integration + +The user explicitly selected follow-ups to PR883, PR890, PR853, PR882 and PR889. +This is the first contribution in that goal. No random track or new topology +is inferred. The local object is PR883's 56 zero-frame target-pair expansions; +the method is concrete primitive emission, separate exact block verification, +source-bound native/phase/wrapper/owner transport, complete invoice and assembly. + +Stopping rule: freshly reproduce the original package, verify the full selected +native/global baseline with complete ancestry coverage, pass explicit lowering +and complete accounting, reject prefix/invoice corruptions, check relocation, +then submit with preserved sources/credit and no unilateral selected change. + +This adds integration and accounting evidence, not a priority claim for the +factorization, pair optimum or compiler primitive alphabet. Concurrent PR901 +changes the later compensation and is neither imported nor added to this bill. +Main remains pinned at f567884a; the final PR883 head is verified before publication.