From bddf5ba853f1b798d021454362e53338c819f150 Mon Sep 17 00:00:00 2001 From: mightyOil <82899331+mightyOil@users.noreply.github.com> Date: Wed, 14 Oct 2026 00:12:03 +0200 Subject: [PATCH] research: close restored 2+3-cycle boundary gap at ten primitives --- .github/workflows/restored-cycle-gap.yml | 31 ++ research/restored-cycle-gap/EXPECTED.json | 139 ++++++++ research/restored-cycle-gap/NOTICE.md | 25 ++ research/restored-cycle-gap/PINS.json | 54 +++ research/restored-cycle-gap/README.md | 211 +++++++++++ research/restored-cycle-gap/SOURCES.json | 48 +++ research/restored-cycle-gap/TASK.json | 67 ++++ research/restored-cycle-gap/VALIDATION.md | 38 ++ research/restored-cycle-gap/VERIFY.json | 27 ++ research/restored-cycle-gap/packed.cpp | 117 +++++++ .../references/PR1216-NOTICE.md | 33 ++ .../references/PR1216-PROOF.md | 186 ++++++++++ .../references/PR1216-independent.cpp.txt | 90 +++++ research/restored-cycle-gap/ternary.cpp | 130 +++++++ research/restored-cycle-gap/test_package.py | 96 +++++ research/restored-cycle-gap/verify.py | 331 ++++++++++++++++++ 16 files changed, 1623 insertions(+) create mode 100644 .github/workflows/restored-cycle-gap.yml create mode 100644 research/restored-cycle-gap/EXPECTED.json create mode 100644 research/restored-cycle-gap/NOTICE.md create mode 100644 research/restored-cycle-gap/PINS.json create mode 100644 research/restored-cycle-gap/README.md create mode 100644 research/restored-cycle-gap/SOURCES.json create mode 100644 research/restored-cycle-gap/TASK.json create mode 100644 research/restored-cycle-gap/VALIDATION.md create mode 100644 research/restored-cycle-gap/VERIFY.json create mode 100644 research/restored-cycle-gap/packed.cpp create mode 100644 research/restored-cycle-gap/references/PR1216-NOTICE.md create mode 100644 research/restored-cycle-gap/references/PR1216-PROOF.md create mode 100644 research/restored-cycle-gap/references/PR1216-independent.cpp.txt create mode 100644 research/restored-cycle-gap/ternary.cpp create mode 100644 research/restored-cycle-gap/test_package.py create mode 100644 research/restored-cycle-gap/verify.py diff --git a/.github/workflows/restored-cycle-gap.yml b/.github/workflows/restored-cycle-gap.yml new file mode 100644 index 0000000000..6665f2535f --- /dev/null +++ b/.github/workflows/restored-cycle-gap.yml @@ -0,0 +1,31 @@ +name: Restored cycle gap native replay +on: + pull_request: + paths: + - 'research/restored-cycle-gap/**' + - 'research/complex-swap-runs-seed37/EXPECTED.json' + - 'research/community-k492-audit/pr626/replay/mixed-global/base/providers/ck/LOCAL-PROGRAMS.json.gz' + - 'research/community-k492-audit/pr626/replay/mixed-global/base/providers/ck/LOCAL-CHECKS.json' + - 'research/community-k492-audit/pr626/replay/mixed-global/base/providers/jp8/LOCAL-PROGRAMS.json.gz' + - 'research/community-k492-audit/pr626/replay/mixed-global/base/providers/jp8/LOCAL-CHECKS.json' + - '.github/workflows/restored-cycle-gap.yml' + workflow_dispatch: +permissions: + contents: read +jobs: + exact-gap: + runs-on: ubuntu-24.04 + timeout-minutes: 15 + steps: + - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 + with: + persist-credentials: false + - uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97 + with: + python-version: '3.12' + - name: Full independently represented native exclusion and controls + run: python -I -O -B research/restored-cycle-gap/verify.py + - name: Read-only relocation and deliberate rejection controls + run: python -I -O -B research/restored-cycle-gap/test_package.py + - name: Inputs unchanged + run: git diff --exit-code diff --git a/research/restored-cycle-gap/EXPECTED.json b/research/restored-cycle-gap/EXPECTED.json new file mode 100644 index 0000000000..88a758348b --- /dev/null +++ b/research/restored-cycle-gap/EXPECTED.json @@ -0,0 +1,139 @@ +{ + "exact": { + "disposable_control_length": 8, + "donor_extensions": [ + 0, + 1, + 2, + 8, + 49 + ], + "exact_minimum": 10, + "omission_controls": 10, + "witness_length": 10, + "write_bound_at_nine": { + "cycles": 2, + "moved": 5, + "written_donors_at_most": 1 + } + }, + "finite_exclusion": { + "dense_controls": [ + { + "minimum": 0, + "permutation": "01", + "states": 48 + }, + { + "minimum": 4, + "permutation": "10", + "states": 48 + }, + { + "minimum": 0, + "permutation": "012", + "states": 11232 + }, + { + "minimum": 4, + "permutation": "021", + "states": 11232 + }, + { + "minimum": 4, + "permutation": "102", + "states": 11232 + }, + { + "minimum": 6, + "permutation": "120", + "states": 11232 + }, + { + "minimum": 6, + "permutation": "201", + "states": 11232 + }, + { + "minimum": 4, + "permutation": "210", + "states": 11232 + } + ], + "distance_nine_control": { + "direct_hits": 0, + "generators": 28, + "layers": [ + 1, + 28, + 486, + 6272, + 62885 + ], + "middle_hits": 1000, + "minimum_through_nine": 9, + "n": 4, + "permutation": "123a", + "states": 69672, + "transitions": 1950816 + }, + "invalid_native_inputs_rejected": 10, + "target": { + "canonical_ball_sha256": "a943ba6bc12d9da2d57ea31edb27455804adaea1280c1fd226af4c4915f210d0", + "direct_hits": 0, + "generators": 66, + "layers": [ + 1, + 66, + 2655, + 83270, + 2213925 + ], + "middle_hits": 0, + "minimum_through_nine": null, + "n": 6, + "permutation": "103425", + "states": 2299917, + "transitions": 151794522 + } + }, + "format": "restored-cycle-gap-v1", + "historical_invoice": { + "ck/backward": { + "boundaries": 42, + "census_sha256": "36b5a2c3deec1d24fe47ea3dcbc6a8b99e897fce5a16a920e13312f32716e1a9", + "disposable_component_cost": 224, + "restored_component_minimum": 252, + "separate_complex_components_extra": 56, + "two_cycles": 28, + "two_plus_three_cycles": 14 + }, + "ck/forward": { + "boundaries": 42, + "census_sha256": "36b5a2c3deec1d24fe47ea3dcbc6a8b99e897fce5a16a920e13312f32716e1a9", + "disposable_component_cost": 224, + "restored_component_minimum": 252, + "separate_complex_components_extra": 56, + "two_cycles": 28, + "two_plus_three_cycles": 14 + }, + "jp8/backward": { + "boundaries": 42, + "census_sha256": "1702dd8067fd6f1b0e081c37e853700847baf73e2172bc9e07b502120c847660", + "disposable_component_cost": 224, + "restored_component_minimum": 252, + "separate_complex_components_extra": 56, + "two_cycles": 28, + "two_plus_three_cycles": 14 + }, + "jp8/forward": { + "boundaries": 42, + "census_sha256": "1702dd8067fd6f1b0e081c37e853700847baf73e2172bc9e07b502120c847660", + "disposable_component_cost": 224, + "restored_component_minimum": 252, + "separate_complex_components_extra": 56, + "two_cycles": 28, + "two_plus_three_cycles": 14 + } + } +} diff --git a/research/restored-cycle-gap/NOTICE.md b/research/restored-cycle-gap/NOTICE.md new file mode 100644 index 0000000000..0ab468259b --- /dev/null +++ b/research/restored-cycle-gap/NOTICE.md @@ -0,0 +1,25 @@ +# Attribution + +New contribution for Philipp / mightyOil, with substantial OpenAI Codex +GPT-6 Astra assistance in research, proofs, implementation, checks and prose. +Apache-2.0, under the repository license. No independent human review claimed. + +Ross Richardson's PR1216 supplies the restored-donor model, read-only +specialization, modular quotient, exact upper witnesses, and the explicitly +open nine-versus-ten problem. Its PROOF.md, NOTICE.md and independent.cpp are +retained verbatim in references/ with exact Git-blob and SHA256 pins. +packed.cpp adapts that C++ implementation; verify.py's swap recognition and +boundary census adapt the corresponding PR1216 verifier. Their origin is +disclosed even though the source is not imported at runtime. The original +PR1216 verifier commit, path, Git blob and SHA256 are recorded in PINS.json. + +The new cycle-sensitive write lemma and exhaustive middle-gate exclusion +close that specific gap. Ternary.cpp is newly written; independence refers +to separately represented finite implementations, not to human authorship. + +Credit ToikY's actual PR969 boundary construction, Ross Richardson's PR1145, +Sagar Thakrar's PR696 lowering, faw01's PR839 clean-work contract, Jeremy +Kothe's PR622, Chafik Boukhalfa's PR626, icekylinx and all retained lineage +notices. PR1095's disposable-workspace model is distinct. Selected PR1094 +and earlier Rohan Arun, Jeremy Kothe, Hao Yan and bit-supplier contributions +are context only; no selected record or predecessor package is modified. diff --git a/research/restored-cycle-gap/PINS.json b/research/restored-cycle-gap/PINS.json new file mode 100644 index 0000000000..ea231c9f21 --- /dev/null +++ b/research/restored-cycle-gap/PINS.json @@ -0,0 +1,54 @@ +{ + "base_commit": "bce54fb3f895cbe5cd4c0eb477c3afeed100190f", + "predecessor_head": "2cbf4084e141ba24ee3417ff014fdc7ca83b6c66", + "live_inputs": { + "research/complex-swap-runs-seed37/EXPECTED.json": { + "sha256": "b1d3b19f360c611802f105382e969f26e15bdbf57dae19264e412554805e43d5", + "git_blob": "995ec843dfa40a024390b309082377cf70695a8e" + }, + "research/community-k492-audit/pr626/replay/mixed-global/base/providers/ck/LOCAL-PROGRAMS.json.gz": { + "sha256": "b5da54e049cc127a1065190a647cb71cac0c6ba03d9ccdb71719f4fcbfa886f3", + "git_blob": "61ef73c1f958e0d26f3e7a3a82bc3826b7098c93" + }, + "research/community-k492-audit/pr626/replay/mixed-global/base/providers/ck/LOCAL-CHECKS.json": { + "sha256": "059c4e59142bdf5c19dc7c0afebcddfec28e6e60cbc7299b8bdcc624afbc0cbe", + "git_blob": "d2b8854114b19b88e14d2af0dd84ad79e9eedbaa" + }, + "research/community-k492-audit/pr626/replay/mixed-global/base/providers/jp8/LOCAL-PROGRAMS.json.gz": { + "sha256": "fa0c196f65bd6ec1424fdf7d789f6972075c7bb02bf43f573ea85eafab31be98", + "git_blob": "e22169a1633638213a5c63425a1919c7185f4c43" + }, + "research/community-k492-audit/pr626/replay/mixed-global/base/providers/jp8/LOCAL-CHECKS.json": { + "sha256": "0fad744aa863eedb288a9f87b1c23225a36b316b6275cc3b1bcedd42afe28a67", + "git_blob": "0d84d903086993330ddcd871e66b15854f0c3ccd" + } + }, + "package": { + "ternary.cpp": { + "sha256": "f6f64206c2269a21f571cc2de64c64fb73b5cee9af89de9347d5e38b0dcaa41f", + "git_blob": "97757bcc42940fe3c3399e14afb16fec75b033fe" + }, + "packed.cpp": { + "sha256": "8ca8361756b87eabbe79bb438324ab20941b8c4ff2967be4f7a444feb9ea9232", + "git_blob": "c61013136cccb4e79d593f730c32d957a55613f3" + }, + "references/PR1216-PROOF.md": { + "sha256": "7808f30e28508e327f68fafdc0a1be58c779d892482d3713c767fd7c0d21e4b0", + "git_blob": "a78b1f09f31f5d2d29652ddde795598e41789b72" + }, + "references/PR1216-NOTICE.md": { + "sha256": "ea949bc4d13815896770c159d9231fe76901f3a798f13741123722ffc503b9f3", + "git_blob": "a29278ba18b01e2e8584b4e8ec5ba999bcc75ff9" + }, + "references/PR1216-independent.cpp.txt": { + "sha256": "e6c22ca6da54620933f98c33aef4f9644049a39b2b5178b69b8aaa6ffe1c78bd", + "git_blob": "f8c3f46feb83e064ee4c59c6e6af2e3cf93c535c" + } + }, + "adapted_verifier": { + "commit": "2cbf4084e141ba24ee3417ff014fdc7ca83b6c66", + "path": "research/complex-restored-borrowed-boundaries/verify.py", + "git_blob": "85527a5c1700c3ac28d593e80ba84113d8ba3f77", + "sha256": "25f4fc02c1e64abb9f88c83e3069160d4b1ca8e8cd67ee4934fa62ea60fbb4dd" + } +} diff --git a/research/restored-cycle-gap/README.md b/research/restored-cycle-gap/README.md new file mode 100644 index 0000000000..332a5de8a5 --- /dev/null +++ b/research/restored-cycle-gap/README.md @@ -0,0 +1,211 @@ +# A disjoint 2+3-cycle costs exactly ten with restored dirty donors + +**Scoped negative result / exact recursive boundary price; no new kappa.** +The unresolved nine-versus-ten gap in Ross Richardson's +[PR1216](https://github.com/CrocSwap/integer-mult-bounds/pull/1216) and +[PR1145](https://github.com/CrocSwap/integer-mult-bounds/pull/1145) closes at +**ten primitives**, even with any finite number of borrowed registers whose +arbitrary incoming values must all be restored. The ten-step witness is the +predecessor's direct sum of a four-step swap and six-step three-cycle. + +The new ingredient is a cycle-sensitive write lemma, followed by a complete +six-register radius-four / one-middle-gate / radius-four exclusion over F3. +The fresh ternary-row checker and the separately represented, adapted PR1216 +bit-packed checker agree on every one of **2,299,917 matrices and distances**. +Each checks all **151,794,522** possible middle transitions; none connects the +two balls for the target. This is a finite certificate tied to a written +unbounded-donor reduction, not a failed heuristic search or a proof-assistant +verification. + +## Exact model and proof + +All registers contain arbitrary independent real inputs. The complete target +is `(x0,x1,x2,x3,x4) -> (x1,x0,x3,x4,x2)` and identity on all donors. The priced +alphabet is distinct-register ADD/SUB, unary NEG/DOUBLE/HALVE, COPY and CLEAR. +There are no free renamings, signs, input promises, initialization, or discarded +registers. Every primitive targets one row; every prefix is a linear map. +The result also covers inverse cycle direction and relabelled coordinates. + +COPY to a distinct target and CLEAR are singular, so an invertible completed +map cannot contain them. Self-COPY is redundant. Every remaining prefix is +invertible over the dyadic rationals. A moved coordinate is written at least +once, and a written restored donor at least twice: its first write changes its +initial basis row by a nonzero invertible-prefix row or a nonidentity scale. +Without a later write it cannot return to that initial row. + +**Cycle-write lemma.** If a nontrivial target cycle had every coordinate +written exactly once, consider the first write to any coordinate `i` of that +cycle. Since it is the only write to `i`, it must produce the final basis row +`e_p(i)`. But coordinate `p(i)` belongs to that cycle and is still untouched, +so its row is also `e_p(i)`. Two equal rows contradict prefix invertibility. +Hence a permutation moving `m` coordinates in `c` nontrivial cycles requires +at least `m+c` writes to moved coordinates. Consequently a length-`L` word +can write to at most `floor((L-m-c)/2)` restored donors. This improves PR1216's +`floor((L-m)/2)` count without restricting mixed intermediate rows. + +At `L=9, m=5, c=2`, at most **one** donor is written. Any other donor is read +only: specialize its independent input to zero and delete its zero-source +ADD/SUBs. The universal identity continues to hold and length cannot increase. +This is an existence reduction for a lower bound, never free initialization +in an actual construction. The reduced word embeds into six registers. + +Reduce `Z[1/2]` modulo three: ADD/SUB remain row additions, while NEG, DOUBLE +and HALVE all become row negation. These 66 distinct invertible elementary +gates form an inverse-closed generating set `G`. A dyadic word of at most nine +steps would give such a modular word of at most nine steps. Modular existence +would not, by itself, supply a rational upper witness. + +Let `B` be the complete ball of radius four about identity in this generating +set, and `P` the target six-by-six permutation matrix. A word of length at +most nine exists exactly when either `A P` is in `B`, or `g A P` is in `B`, +for some `A in B`, `g in G`. For the nontrivial direction, write +`P = U h V`, with `U,V` of length at most four and `h` one gate; take +`A=U^-1`, `g=h^-1`. Conversely a hit gives `P=A^-1 g^-1 (gAP)`. +The direct intersection also accounts for empty middle gates/lengths at most +eight. Every lower depth is included; no determinant, write-pattern or +symmetry pruning is used in the finite scan. + +Both engines independently enumerate the layers +`1, 66, 2655, 83270, 2213925`, then check every state and every middle gate. +Both intersections are empty. The dyadic nine-step word is therefore +impossible with any finite number of restored donors. The exact ten-step +word below establishes the matching upper bound: + +```text +x0 += x1; x1 -= x0; x0 += x1; x1 = -x1; +x4 -= x3; x2 -= x4; x3 += x4; x4 += x2; x2 -= x4; x2 += x3. +``` + +All incoming donor coordinates are untouched in this word. The rational +replay checks every independent column and its literal inverse. + +## Historical boundary application and full cost boundary + +The unchanged historical PR969 CK/JP8 words are freshly decoded in all four +provider/orientation cases. The adapted exact two-by-two swap recognizer +reproduces all **168** pinned boundary records, including event intervals, +frames, swap positions, permutations and cycle lists. Each orientation has +28 two-cycles and 14 disjoint two-plus-three cycles. Thus in the unrestricted +scalar boundary model the exact independently restored component bill is + +```text +28*4 + 14*10 = 252, +``` + +versus 224 with the predecessor's disposable coefficient-work register. +Separate real/imaginary lowering costs **56 extra real primitives per +orientation**, sharpening PR1216's lower bound of 28. The older 238 lower +bill becomes an exact 252 local minimum. This does not assert physical +attainability of that minimum under additional frame/routing restrictions; +those restrictions can only raise it. Exact four-step swap minimality remains +PR1216's result, also corroborated by the complete small-group oracle here. + +For a caller with indivisible boundaries, write its full recurrence as + +```text +T(n) = sum_j T_j(n_j) + + P(n) + S(n) + A(n) + R(n) + H(n) + D(n) + + q(n) [4 b2(n) + 10 b23(n)]. +``` + +Here each child call is complete in its actual direction; `P` prices factor +and coefficient preparation, `S` source access/copies, `A` frame adapters, +`R` all other restoration, `H` data/program transport and head return, and +`D` controller/dispatch. `q` is the cost of one full scalar primitive at the +actual row length/precision, with separate component lowering when required. +No output multiplicity divides a full-row cost. All arbitrary borrowed +coordinates are included in the local endpoint, so no donor restoration is +left unpaid. Comparing this restricted replacement with disposable work +changes only the boundary term from `4b2+8b23` to `4b2+10b23`; differences in +the other terms must be charged separately. The source-dependent native +compiler, precision and tape obligations are not discharged by this formula. + +The intended boundary-saving mechanism fails under this exact interface. +It eliminates no supplier work row: other operations still need coefficient +work. No paid recursive profile, current selected supplier, moment or kappa +changes. Joint synthesis with adjacent scalar runs, clean or disposable +workspace, other primitives and joint complex-component arithmetic remain +outside this result. The selected PR1094 certificate/construction/review were +read for orientation, not recomputed or modified. + +## Reproduce and controls + +Python 3.12 and a C++17 compiler (`c++`, clang++ or g++ with `__int128`): + +```sh +python3.12 -I -O -B research/restored-cycle-gap/verify.py +python3.12 -I -O -B research/restored-cycle-gap/test_package.py +``` + +The first command prints `PASS_RESTORED_CYCLE_GAP exact_minimum=10`, the two +coverage counts and `historical_component_bill=252 no_new_kappa`. +It compiles both engines into temporary storage, compares the full canonical +matrix/distance byte streams (not just their hashes), recomputes the receipt +and checks it field for field against [EXPECTED.json](EXPECTED.json). +The exact source files are authenticated before execution. `--record NEW_PATH` +exports a fresh receipt and refuses to overwrite an existing file. + +The dense Python oracle independently visits **all GL(2,3) and GL(3,3)**, +checking every small-ball matrix/distance and all eight permutation endpoints. +An essential positive control is the signed four-cycle +`(x0,x1,x2,x3)->(x1,x2,x3,-x0)`: both native engines find zero direct hits and +**1,000 middle-gate hits**, giving exact modular distance nine; its explicit +nine-ADD/SUB rational word is independently checked. Removing the new middle +scan would falsely exclude this control. Ten omissions from the ten-step +witness, disposable-donor destruction, illegal read-only specialization, +nonunit quotient denominators and invalid native target inputs are rejected. + +Package tests include optimized read-only relocation with a complete native +replay, three on-disk source corruptions and a receipt corruption rejected +after another complete replay. The optional registered package command runs +only `--quick`, which explicitly does **not** replay the lower bound; the +dedicated native workflow runs both complete commands above. No generic quick +pass, hash alone, or inherited receipt is presented as full exclusion evidence. + +## Provenance and scope selection + +OS-random seed **54**, recursive-interface track. Exact base +`bce54fb3f895cbe5cd4c0eb477c3afeed100190f`. Three candidates were considered: +sign-asymmetric PR1088 prices (already immediate from balanced sign counts), +cyclic output frames (close to concurrent PR1287), and this explicit PR1216 +gap. The changed card premise is disclosed in [TASK.json](TASK.json): this +is a boundary obstruction, not a new consecutive-call cancellation. The new +cycle lemma changes the previously unsearched donor dimension at length nine; +the work does not merely repeat the closed eight-step search. + +PR1216 is pinned at `2cbf4084e141ba24ee3417ff014fdc7ca83b6c66`; its proof, +notice and original bit-packed source are retained byte-for-byte under +`references/`. Live input and adaptation hashes are in [PINS.json](PINS.json). +PR1145 is `fd4d5ffc448361297e717aa30eafed578caf8e61`; ToikY's actual PR969 +head is `d1ee3f46a6167ea54913e070af3161c71a99e1f2`. The older PR971 narrative +misidentification is not repeated. New finite coverage is exhaustive through +the stated nine-step bound, with no stochastic pruning or timeout-based +conclusion; seed54 diversifies the object, not the mathematical enumeration. + +## Open next questions + +- Can joint synthesis across one named adjacent scalar run and its boundary + beat the sum of independently restored boundary prices? This would change + the indivisible-boundary hypothesis. First extract that exact complete map + and optimistic invoice from a pinned supplier; all intermediate frames and + source-access costs are blockers before claiming a saving. +- Does the cycle-sensitive write bound help another concrete restored + permutation gap? First derive its finite donor cap and memory budget. A + larger finite search is justified only if an actual boundary or interface + decision depends on it; no unrestricted stabilization theorem is claimed. + +## Credit and limitations + +Ross Richardson retains credit for PR1216's restored-donor model, read-only +specialization, modular reduction, exact witnesses and PR1145's independent +representations. `packed.cpp` and the boundary recognizer are adaptations; +`ternary.cpp` is freshly written. Both are AI-assisted, not independent human +review. ToikY (PR969), Sagar Thakrar (PR696), faw01 (PR839), Jeremy Kothe +(PR622), Chafik Boukhalfa (PR626), icekylinx and the retained lineage keep their +source attribution. PR1095 concerns a distinct disposable-workspace class. +Prepared for **Philipp / mightyOil** with substantial **OpenAI Codex GPT-6 +Astra assistance** in mathematics, implementation, verification and prose. +New work is Apache-2.0; original notices are retained. No formal multiplication +theorem, current full supplier cold replay, physical compiler/hosting, +rounding theorem, outer analytic transfer, remote CI success or independent +human review is claimed. diff --git a/research/restored-cycle-gap/SOURCES.json b/research/restored-cycle-gap/SOURCES.json new file mode 100644 index 0000000000..39740c4279 --- /dev/null +++ b/research/restored-cycle-gap/SOURCES.json @@ -0,0 +1,48 @@ +{ + "schema_version": 1, + "base_commit": "bce54fb3f895cbe5cd4c0eb477c3afeed100190f", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "c05fafaa25ba95b2d5af86b1800427198e3d20eb", + "sha256": "89b5928bc92c81e2647b6d702a7ad85a6795b8f44e2eb267b2ff3145d8f2b2ce" + }, + { + "path": "research/complex-swap-runs-seed37/EXPECTED.json", + "usage": "input", + "sha256": "b1d3b19f360c611802f105382e969f26e15bdbf57dae19264e412554805e43d5", + "git_blob": "995ec843dfa40a024390b309082377cf70695a8e" + }, + { + "path": "research/community-k492-audit/pr626/replay/mixed-global/base/providers/ck/LOCAL-PROGRAMS.json.gz", + "usage": "input", + "sha256": "b5da54e049cc127a1065190a647cb71cac0c6ba03d9ccdb71719f4fcbfa886f3", + "git_blob": "61ef73c1f958e0d26f3e7a3a82bc3826b7098c93" + }, + { + "path": "research/community-k492-audit/pr626/replay/mixed-global/base/providers/ck/LOCAL-CHECKS.json", + "usage": "input", + "sha256": "059c4e59142bdf5c19dc7c0afebcddfec28e6e60cbc7299b8bdcc624afbc0cbe", + "git_blob": "d2b8854114b19b88e14d2af0dd84ad79e9eedbaa" + }, + { + "path": "research/community-k492-audit/pr626/replay/mixed-global/base/providers/jp8/LOCAL-PROGRAMS.json.gz", + "usage": "input", + "sha256": "fa0c196f65bd6ec1424fdf7d789f6972075c7bb02bf43f573ea85eafab31be98", + "git_blob": "e22169a1633638213a5c63425a1919c7185f4c43" + }, + { + "path": "research/community-k492-audit/pr626/replay/mixed-global/base/providers/jp8/LOCAL-CHECKS.json", + "usage": "input", + "sha256": "0fad744aa863eedb288a9f87b1c23225a36b316b6275cc3b1bcedd42afe28a67", + "git_blob": "0d84d903086993330ddcd871e66b15854f0c3ccd" + } + ] +} diff --git a/research/restored-cycle-gap/TASK.json b/research/restored-cycle-gap/TASK.json new file mode 100644 index 0000000000..aa3097f57f --- /dev/null +++ b/research/restored-cycle-gap/TASK.json @@ -0,0 +1,67 @@ +{ + "schema_version": 1, + "task_id": "persistent-boundary", + "priority_revision": 2, + "base_commit": "bce54fb3f895cbe5cd4c0eb477c3afeed100190f", + "original_card": { + "id": "persistent-boundary", + "question": "Can a specified pair of consecutive calls eliminate a restoration that the next call reconstructs?", + "starting_points": [ + "research/heterogeneous-owner-assembly/README.md", + "certificates/selected-result.json" + ], + "methods": [ + "Write typed entry/exit contracts and a contracting multitype recurrence.", + "Derive a lower bound for the compulsory transitions of one proposed typed interface." + ], + "acceptance_gate": "Show actual eliminated work and legal composition; changing a scalar recurrence into a matrix is insufficient.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Find a concrete consecutive-call boundary in the selected review and list its entry/exit obligations.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Specify two call types and one operation actually removed by composition; derive the normalized recurrence.", + "bottleneck_link": "Eliminating compulsory boundary work can lower recursive cost beyond packing gains.", + "allowed_variations": [ + "A two-type pilot or one explicit deferred restoration." + ], + "scope_change_triggers": [ + "Rewriting the old scalar recurrence as a matrix without eliminating work." + ], + "overlap_terms": [ + "persistent boundary", + "deferred restoration", + "multitype" + ] + }, + "scope_status": "changed", + "actual_scope": "Close PR1216 exact nine-versus-ten restored disjoint 2+3-cycle gap using cycle-sensitive write bound and complete six-register modular exclusion.", + "scope_change_reason": "The assigned recursive-interface track permits scoped negative results. Consecutive-call and cyclic-output proposals overlap current work; this explicit open boundary gap changes the previous unbounded-donor reduction and answers a concrete restoration-cost question.", + "bottleneck_link": "Negative local restoration mechanism screen. Under this boundary alphabet restored borrowing cannot match the disposable coefficient-work price, so this does not improve a selected recursive profile.", + "budget_minutes": 40, + "stop_rule": "Complete the two independent radius-four/middle/radius-four scans and exact upper witness; no parameter widening or longer search after closing this gap.", + "outcome": "negative-result", + "evidence": "README proof; EXPECTED exact receipt; full native replay; signed-cycle distance-nine control; historical 168-boundary source recount.", + "author": "Philipp / mightyOil", + "ai_assistance": "Substantial OpenAI Codex GPT-6 Astra assistance in proof, code, verification and prose; no independent human review.", + "open_questions": [ + { + "question": "Can a named boundary and adjacent scalar run be synthesized jointly below the separate price?", + "why_it_matters": "It would change the indivisible-boundary premise excluded here.", + "first_step": "Extract one pinned exact combined map and its optimistic complete bill.", + "blocked_by": "Source/frame access, physical hosting and precision costs need admission." + }, + { + "question": "Can the cycle-write lemma reduce a second concrete donor-cap gap?", + "why_it_matters": "It can remove an unbounded-storage obstacle without restricting intermediate rows.", + "first_step": "Identify an actual boundary and derive its finite donor cap and memory estimate.", + "blocked_by": "A named useful target and tractable complete coverage are required." + } + ], + "assignment_seed": 54 +} diff --git a/research/restored-cycle-gap/VALIDATION.md b/research/restored-cycle-gap/VALIDATION.md new file mode 100644 index 0000000000..d889201302 --- /dev/null +++ b/research/restored-cycle-gap/VALIDATION.md @@ -0,0 +1,38 @@ +# Executed validation + +Local host: macOS arm64, Apple clang 21.0.0 (C++17), CPython 3.12.13 and +3.14.7. New material only; predecessor and upstream inputs unchanged. + +- CPython 3.12.13, assertions disabled: complete native exclusion, exact upper + word, signed distance-nine positive control, complete dense GL(2,3)/GL(3,3) + oracle, all input controls and fresh 168-boundary recount passed. Rebuilt + EXPECTED.json after all checks, including the retained predecessor hashes. +- Five package test groups pass on CPython 3.12.13 in 40.675 seconds, including + full read-only relocated replay, three source-corruption rejections and a + receipt corruption rejected after another full native replay. +- CPython 3.14.7 complete optimized replay agrees field for field with the + committed receipt. Different Python versions do not make the underlying + native implementations independent; the separate representations do. +- Registered Python 3.12 quick replay and source/metadata pins pass. This quick + command explicitly omits the native exclusion; it is not the full result. +- Selected-record integrity passes. Five selected-record tests pass. Twenty + repository research tests pass with one expected skip. Whitespace checks pass. + +Both native engines enumerate all 2,299,917 six-register matrices/minimum +radius-four distances; the full 20,699,253-byte canonical streams agree. +Each tests all 151,794,522 middle transitions with zero hits, plus the direct +intersection. The four-register signed-cycle control has 1,000 middle hits +and minimum nine; the direct intersection has zero hits. The target canonical +ball SHA256 is `a943ba6bc12d9da2d57ea31edb27455804adaea1280c1fd226af4c4915f210d0`. +The hash summarizes the full byte comparison and is not a substitute for it. + +Source-bound contextual checks: selected base/main +`bce54fb3f895cbe5cd4c0eb477c3afeed100190f` remained current at the final fetch; +PR1216 and PR1145 heads were unchanged. Final overlap snapshot covered 794 +open PRs through #1300 and the available Discussion claims; no overlapping +nine-versus-ten result was found. The scoped coordinator written review found +no blocker, but did not independently execute the full exclusion. + +No Linux/hosted CI success, selected supplier cold replay, physical compiler, +rounding/precision theorem, Lean result or independent human review is claimed. +The dedicated native workflow is newly supplied; its remote status is separate. diff --git a/research/restored-cycle-gap/VERIFY.json b/research/restored-cycle-gap/VERIFY.json new file mode 100644 index 0000000000..d0bb830130 --- /dev/null +++ b/research/restored-cycle-gap/VERIFY.json @@ -0,0 +1,27 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/complex-swap-runs-seed37/EXPECTED.json", + "research/community-k492-audit/pr626/replay/mixed-global/base/providers/ck/LOCAL-PROGRAMS.json.gz", + "research/community-k492-audit/pr626/replay/mixed-global/base/providers/ck/LOCAL-CHECKS.json", + "research/community-k492-audit/pr626/replay/mixed-global/base/providers/jp8/LOCAL-PROGRAMS.json.gz", + "research/community-k492-audit/pr626/replay/mixed-global/base/providers/jp8/LOCAL-CHECKS.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py", + "--quick" + ], + "timeout_seconds": 120, + "checks": "Source pins, exact ten-step rational witness/inverse/controls, full 168 historical boundary recount. Explicitly excludes native lower-bound replay; full native replay uses dedicated restored-cycle-gap workflow." + } + ] +} diff --git a/research/restored-cycle-gap/packed.cpp b/research/restored-cycle-gap/packed.cpp new file mode 100644 index 0000000000..c61013136c --- /dev/null +++ b/research/restored-cycle-gap/packed.cpp @@ -0,0 +1,117 @@ +// Ross Richardson / OpenAI Codex, adapted by Philipp / mightyOil with Codex. +// Apache-2.0. PR1216's bit-packed BFS, extended with an independent middle-gate +// meet and explicit target permutation. No ternary row tables are imported. +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +using Key = unsigned __int128; +struct Hash { + std::size_t operator()(Key k) const { + auto lo=static_cast(k), hi=static_cast(k>>64); + return std::hash{}(lo ^ (hi*0x9e3779b97f4a7c15ULL)); + } +}; +int coefficient(Key key,int n,int row,int column) { + return (key >> (2*(row*n+column))) & 3; +} +Key change(Key key,int n,int target,int source,int sign) { + Key result=key; + for(int column=0;column6) throw std::runtime_error("dimension 2..6 required"); + std::string permutation(argv[2]); + if(int(permutation.size())!=n) throw std::runtime_error("permutation length"); + std::vector p(n),negative(n),seen(n); + for(int i=0;i='a' && permutation[i]<='f'; + p[i]=permutation[i]-(negative[i]?'a':'0'); + if(p[i]<0 || p[i]>=n || seen[p[i]]++) throw std::runtime_error("permutation"); + } + Key identity=0; + for(int i=0;i distance; + distance.reserve(n==6?2500000:600000); + distance.emplace(identity,0); + std::vector queue{identity}; + std::array layers{1,0,0,0,0}; + for(std::size_t cursor=0;cursor=0;--s) for(int t=n-1;t>=0;--t) for(int sign:{1,-1}) { + if(s==t && sign==1) continue; + Key next=change(state,n,t,s,sign); + if(distance.emplace(next,depth+1).second) {queue.push_back(next);++layers[depth+1];} + } + } + std::uint64_t transitions=0,direct_hits=0,middle_hits=0; + int minimum=99; + for(Key state:queue) { + // Explicit multiplication A P: old column c goes to column p[c]. + Key transformed=0; + for(int r=0;rsecond)); + } + for(int s=n-1;s>=0;--s) for(int t=n-1;t>=0;--t) for(int sign:{1,-1}) { + if(s==t && sign==1) continue; + ++transitions; + found=distance.find(change(transformed,n,t,s,sign)); + if(found!=distance.end()) { + ++middle_hits; minimum=std::min(minimum,int(distance.at(state))+1+int(found->second)); + } + } + } + std::vector> ordered; + ordered.reserve(distance.size()); + for(const auto& entry:distance) { + std::uint64_t ternary=0,place=1; + for(int r=0;r>(8*i))&255)); + ball.put(char(entry.second)); + } + ball.close(); if(!ball) throw std::runtime_error("ball write"); + std::ofstream out(argv[4]); + if(!out) throw std::runtime_error("report open"); + out<<"{\"n\":"< distance; + distance.reserve(n == 6 ? 2500000 : 100000); + distance.emplace(identity, 0); + std::vector queue{identity}; + for (std::size_t cursor = 0; cursor < queue.size(); ++cursor) { + Key state = queue[cursor]; + int depth = distance.at(state); + if (depth == 4) continue; + // Deliberately use a different generator order from the Python BFS. + for (int s = n - 1; s >= 0; --s) { + for (int t = n - 1; t >= 0; --t) { + for (int sign : {1, -1}) { + if (s == t && sign == 1) continue; + Key next = change(state, n, t, s, sign); + if (distance.emplace(next, depth + 1).second) queue.push_back(next); + } + } + } + } + std::vector> ordered; + ordered.reserve(distance.size()); + for (const auto &entry : distance) { + std::uint64_t ternary = 0, place = 1; + for (int r = 0; r < n; ++r) for (int c = 0; c < n; ++c) { + ternary += place * coefficient(entry.first, n, r, c); + place *= 3; + } + ordered.emplace_back(ternary, entry.second); + } + std::sort(ordered.begin(), ordered.end()); + std::ofstream output(argv[2], std::ios::binary); + if (!output) throw std::runtime_error("output open"); + for (const auto &entry : ordered) { + for (int i = 0; i < 8; ++i) output.put(char((entry.first >> (8 * i)) & 255)); + output.put(char(entry.second)); + } + output.close(); + if (!output) throw std::runtime_error("output write"); + std::cout << "PASS_INDEPENDENT_BALL n=" << n << " states=" << ordered.size() << '\n'; + return 0; + } catch (const std::exception &error) { + std::cerr << error.what() << '\n'; + return 1; + } +} diff --git a/research/restored-cycle-gap/ternary.cpp b/research/restored-cycle-gap/ternary.cpp new file mode 100644 index 0000000000..97757bcc42 --- /dev/null +++ b/research/restored-cycle-gap/ternary.cpp @@ -0,0 +1,130 @@ +// Philipp / mightyOil, substantial OpenAI Codex assistance. Apache-2.0. +// Fresh ternary-row implementation of the standard radius4 / middle / radius4 test. +#include +#include +#include +#include +#include +#include +#include +#include +#include +using Key = std::uint64_t; +struct Gate { int target, source, sign; }; + +int main(int argc, char** argv) { + try { + if (argc != 5) throw std::runtime_error("usage: ternary N PERM BALL REPORT"); + const int n = std::stoi(argv[1]); + if (n < 2 || n > 6) throw std::runtime_error("dimension 2..6 required"); + const std::string permutation(argv[2]); + if (int(permutation.size()) != n) throw std::runtime_error("permutation length"); + // Digits denote +e_j; a..f denote -e_j (used by the distance-nine control). + std::vector p(n), sign(n, 1), inverse(n, -1); + for (int i = 0; i < n; ++i) { + sign[i] = permutation[i] >= 'a' && permutation[i] <= 'f' ? -1 : 1; + p[i] = permutation[i] - (sign[i] == -1 ? 'a' : '0'); + if (p[i] < 0 || p[i] >= n || inverse[p[i]] != -1) throw std::runtime_error("permutation"); + inverse[p[i]] = i; + } + int row_base = 1; + for (int i = 0; i < n; ++i) row_base *= 3; + std::vector place(n, 1); + for (int i = 1; i < n; ++i) place[i] = place[i-1] * row_base; + std::vector negative(row_base), right_permuted(row_base); + std::vector plus(row_base * row_base), minus(row_base * row_base); + for (int a = 0; a < row_base; ++a) { + std::vector digits(n); + int residual = a; + for (int c = 0; c < n; ++c) { digits[c] = residual % 3; residual /= 3; } + int digit_place = 1; + for (int c = 0; c < n; ++c) { + negative[a] += ((3-digits[c]) % 3) * digit_place; + right_permuted[a] += ((3 + sign[inverse[c]]*digits[inverse[c]]) % 3) * digit_place; + digit_place *= 3; + } + for (int b = 0; b < row_base; ++b) { + int other = b, radix = 1; + for (int c = 0; c < n; ++c) { + plus[a*row_base+b] += ((digits[c] + other%3) % 3) * radix; + minus[a*row_base+b] += ((digits[c] - other%3 + 3) % 3) * radix; + other /= 3; radix *= 3; + } + } + } + std::vector gates; + for (int t = 0; t < n; ++t) { + gates.push_back({t, t, 0}); + for (int s = 0; s < n; ++s) if (t != s) + for (int sign : {1, -1}) gates.push_back({t, s, sign}); + } + auto change = [&](Key state, Gate gate) { + const int a = state / place[gate.target] % row_base; + const int b = state / place[gate.source] % row_base; + const int replacement = gate.target == gate.source ? negative[a] + : (gate.sign == 1 ? plus[a*row_base+b] : minus[a*row_base+b]); + return state - Key(a)*place[gate.target] + Key(replacement)*place[gate.target]; + }; + Key identity = 0; + int basis = 1; + for (int i = 0; i < n; ++i) { identity += Key(basis)*place[i]; basis *= 3; } + std::unordered_map distance; + distance.reserve(n == 6 ? 2500000 : 600000); + distance.emplace(identity, 0); + std::vector queue{identity}; + std::array layers{1,0,0,0,0}; + for (std::size_t cursor = 0; cursor < queue.size(); ++cursor) { + const Key state = queue[cursor]; + const int depth = distance.at(state); + if (depth == 4) continue; + for (const Gate gate : gates) { + const Key next = change(state, gate); + if (distance.emplace(next, depth+1).second) { + queue.push_back(next); ++layers[depth+1]; + } + } + } + std::uint64_t transitions = 0, direct_hits = 0, middle_hits = 0; + int minimum = 99; + for (Key state : queue) { + Key transformed = 0; + for (int r = 0; r < n; ++r) + transformed += Key(right_permuted[state/place[r]%row_base]) * place[r]; + auto found = distance.find(transformed); + if (found != distance.end()) { + ++direct_hits; + minimum = std::min(minimum, int(distance.at(state)) + int(found->second)); + } + for (Gate gate : gates) { + ++transitions; + found = distance.find(change(transformed, gate)); + if (found != distance.end()) { + ++middle_hits; + minimum = std::min(minimum, int(distance.at(state)) + 1 + int(found->second)); + } + } + } + std::vector> ordered(distance.begin(), distance.end()); + std::sort(ordered.begin(), ordered.end()); + std::ofstream ball(argv[3], std::ios::binary); + if (!ball) throw std::runtime_error("ball open"); + for (auto entry : ordered) { + for (int i = 0; i < 8; ++i) ball.put(char((entry.first >> (8*i)) & 255)); + ball.put(char(entry.second)); + } + ball.close(); if (!ball) throw std::runtime_error("ball write"); + std::ofstream out(argv[4]); + if (!out) throw std::runtime_error("report open"); + out << "{\"n\":" << n << ",\"permutation\":\"" << permutation << "\",\"layers\":["; + for (int i=0;i<5;++i) out << (i ? "," : "") << layers[i]; + out << "],\"states\":" << queue.size() << ",\"generators\":" << gates.size() + << ",\"transitions\":" << transitions << ",\"direct_hits\":" << direct_hits + << ",\"middle_hits\":" << middle_hits << ",\"minimum_through_nine\":"; + if (minimum == 99) out << "null"; else out << minimum; + out << "}\n"; out.close(); if (!out) throw std::runtime_error("report write"); + std::cout << "PASS_TERNARY n=" << n << " states=" << queue.size() << " transitions=" << transitions << '\n'; + return 0; + } catch (const std::exception& error) { + std::cerr << error.what() << '\n'; return 1; + } +} diff --git a/research/restored-cycle-gap/test_package.py b/research/restored-cycle-gap/test_package.py new file mode 100644 index 0000000000..5efaaa59da --- /dev/null +++ b/research/restored-cycle-gap/test_package.py @@ -0,0 +1,96 @@ +"""Meaningful algebra, source-integrity, and optimized relocation controls.""" +import copy +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +import unittest + +sys.path.insert(0, str(Path(__file__).resolve().parent)) +import verify as v + + +class PackageTests(unittest.TestCase): + def test_exact_inverse_and_all_omissions(self): + self.assertEqual(v.exact_checks()["omission_controls"], 10) + + def test_cycle_write_count_not_just_total_moved(self): + permutation = {i: v.PERMUTATION[i] for i in range(6)} + self.assertEqual(sorted(map(len, v.cycles_of(permutation))), [2, 3]) + moved = sum(i != j for i, j in permutation.items()) + self.assertEqual((9-moved-len(v.cycles_of(permutation)))//2, 1) + # A permutation requires more than one write on each nontrivial cycle: + # if every cycle coordinate is written once, the earliest final write + # duplicates the still-untouched row at its destination basis index. + checked = 0 + for n in range(2, 7): + for p in __import__("itertools").permutations(range(n)): + for cycle in v.cycles_of(dict(enumerate(p))): + for first in cycle: + rows = list(v.identity(n)) + rows[first] = rows[p[first]] + self.assertEqual(rows[first], rows[p[first]]) + self.assertNotEqual(first, p[first]) + checked += 1 + self.assertGreater(checked, 4000) + + def test_cost_boundary_and_admission(self): + for receipt in v.invoice().values(): + self.assertEqual(receipt["restored_component_minimum"], 28*4+14*10) + self.assertEqual(receipt["separate_complex_components_extra"], 2*(252-224)) + with self.assertRaises(ValueError): + v.inverse([("copy", 0, 1)]) + + def test_recognizer_detects_bad_swap(self): + provider = v.ROOT / (v.PROVIDERS + "ck/LOCAL-PROGRAMS.json.gz") + events = v.read(provider)["forward"] + blocks = v.boundary_census(events) + first = blocks[0]["swap_starts"][0] + self.assertIsNotNone(v.recognize(events, first, first+4)) + broken = copy.deepcopy(events[first:first+4]) + broken[-1][1][2] *= -1 + self.assertIsNone(v.recognize(broken, 0, 4)) + + def test_relocation_and_on_disk_controls(self): + # The full command is intentionally run once in a read-only relocated + # input tree, independently of the preceding normal package replay. + with tempfile.TemporaryDirectory(prefix="restored-gap-test-") as temporary: + root = Path(temporary) + package = root / "research/restored-cycle-gap" + shutil.copytree(v.HERE, package, ignore=shutil.ignore_patterns("__pycache__")) + for name in v.read(v.HERE / "PINS.json")["live_inputs"]: + target = root / name + target.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(v.ROOT / name, target) + for path in root.rglob("*"): + if path.is_file(): + path.chmod(0o444) + command = [sys.executable, "-I", "-O", "-B", str(package / "verify.py")] + completed = subprocess.run(command, cwd=root, capture_output=True, timeout=480) + self.assertEqual(completed.returncode, 0, completed.stderr.decode()) + self.assertIn(b"PASS_RESTORED_CYCLE_GAP", completed.stdout) + for name in ("ternary.cpp", "packed.cpp", "references/PR1216-PROOF.md"): + path = package / name + original = path.read_bytes() + path.chmod(0o644) + path.write_bytes(original + b"\ncorruption\n") + failed = subprocess.run(command + ["--quick"], cwd=root, capture_output=True, timeout=30) + self.assertNotEqual(failed.returncode, 0) + self.assertIn(b"source SHA256", failed.stderr) + path.write_bytes(original) + path.chmod(0o444) + # Receipt drift must be detected after a real complete replay. + path = package / "EXPECTED.json" + path.chmod(0o644) + bad = json.loads(path.read_text()) + bad["finite_exclusion"]["distance_nine_control"]["middle_hits"] = 0 + path.write_text(json.dumps(bad)) + failed = subprocess.run(command, cwd=root, capture_output=True, timeout=480) + self.assertNotEqual(failed.returncode, 0) + self.assertIn(b"receipt drift", failed.stderr) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/restored-cycle-gap/verify.py b/research/restored-cycle-gap/verify.py new file mode 100644 index 0000000000..a60288f33f --- /dev/null +++ b/research/restored-cycle-gap/verify.py @@ -0,0 +1,331 @@ +"""Exact restored-cycle gap. Stdlib plus explicitly required C++17 compiler. +Philipp / mightyOil, substantial OpenAI Codex assistance. Apache-2.0. +Boundary recognizer adapted from credited Ross Richardson PR1216. +""" +import argparse +from collections import Counter, deque +from fractions import Fraction as F +import gzip +import hashlib +import itertools +import json +from pathlib import Path +import shutil +import struct +import subprocess +import tempfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +PROVIDERS = "research/community-k492-audit/pr626/replay/mixed-global/base/providers/" +PREVIOUS = "research/complex-swap-runs-seed37/EXPECTED.json" + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":")).encode() + + +def read(path): + raw = Path(path).read_bytes() + return json.loads(gzip.decompress(raw) if str(path).endswith(".gz") else raw) + + +def pins(): + manifest = read(HERE / "PINS.json") + for section, base in (("package", HERE), ("live_inputs", ROOT)): + for name, pin in manifest[section].items(): + raw = (base / name).read_bytes() + require(hashlib.sha256(raw).hexdigest() == pin["sha256"], "source SHA256: " + name) + require(hashlib.sha1(b"blob " + str(len(raw)).encode() + b"\0" + raw).hexdigest() + == pin["git_blob"], "source Git blob: " + name) + return manifest + + +def identity(n): + return tuple(tuple(int(i == j) for j in range(n)) for i in range(n)) + + +def execute(word, n): + rows = [list(map(F, row)) for row in identity(n)] + for kind, t, s in word: + if kind == "copy": + rows[t] = list(rows[s]) + elif kind == "clear": + rows[t] = [F(0)] * n + elif kind == "scale": + rows[t] = [s * x for x in rows[t]] + else: + require(kind in ("add", "sub") and t != s, "invalid ADD/SUB") + rows[t] = [a + (1 if kind == "add" else -1)*b for a, b in zip(rows[t], rows[s])] + return tuple(tuple(row) for row in rows) + + +def inverse(word): + result = [] + for kind, t, s in reversed(word): + require(kind not in ("copy", "clear"), "singular word has no declared inverse") + result.append(("sub" if kind == "add" else "add" if kind == "sub" else "scale", + t, 1/s if kind == "scale" else s)) + return result + + +TWO = [("add", 0, 1), ("sub", 1, 0), ("add", 0, 1), ("scale", 1, F(-1))] +THREE = [("sub", 4, 3), ("sub", 2, 4), ("add", 3, 4), + ("add", 4, 2), ("sub", 2, 4), ("add", 2, 3)] +TEN = TWO + THREE +PERMUTATION = (1, 0, 3, 4, 2, 5) + + +def exact_checks(): + target = tuple(identity(6)[i] for i in PERMUTATION) + require(execute(TEN, 6) == target, "ten-word exact endpoint") + require(execute(TEN + inverse(TEN), 6) == identity(6), "ten-word literal inverse") + for i in range(10): + require(execute(TEN[:i] + TEN[i+1:], 6) != target, "undetected omitted gate") + for n in (5, 7, 13, 54): + expected = tuple(identity(n)[i] for i in (1, 0, 3, 4, 2, *range(5, n))) + require(execute(TEN, n) == expected, "dirty-donor extension") + disposable = [("copy", 5, 0), ("copy", 0, 1), ("copy", 1, 5), + ("copy", 5, 2), ("copy", 2, 3), ("copy", 3, 4), + ("copy", 4, 5), ("clear", 5, None)] + result = execute(disposable, 6) + require(result[:5] == target[:5] and result[5] != target[5], "disposable/restored distinction") + contaminated = execute([("add", 0, 5)] + TEN, 6) + require(contaminated != target, "read-only donor is not freely zero") + require(tuple(row[:5] for row in contaminated) == tuple(row[:5] for row in target), + "read-only specialization") + require((9 - 5)//2 == 2 and (9 - (5 + 2))//2 == 1, "donor bound improvement") + for a in range(-7, 8): + for depth in range(6): + q = F(a, 2**depth) + require(q.numerator * pow(q.denominator, -1, 3) % 3 == a * pow(2, depth, 3) % 3, + "dyadic reduction") + for denominator, modulus in ((2, 2), (3, 3)): + try: + pow(denominator, -1, modulus) + except ValueError: + pass + else: + raise ValueError("nonunit denominator accepted") + return {"exact_minimum": 10, "witness_length": 10, "omission_controls": 10, + "donor_extensions": [0, 1, 2, 8, 49], "disposable_control_length": 8, + "write_bound_at_nine": {"moved": 5, "cycles": 2, "written_donors_at_most": 1}} + + +def dense_group(n): + """Third representation: dense coefficient tuples, complete GL(n,3) BFS.""" + start = identity(n) + distance, queue = {start: 0}, deque([start]) + while queue: + state = queue.popleft() + for t in range(n): + rows = list(state) + rows[t] = tuple(-x % 3 for x in state[t]) + candidates = [tuple(rows)] + for s in range(n): + if s != t: + for sign in (-1, 1): + rows[t] = tuple((a+sign*b) % 3 for a, b in zip(state[t], state[s])) + candidates.append(tuple(rows)) + for new in candidates: + if new not in distance: + distance[new] = distance[state] + 1 + queue.append(new) + return distance + + +def ball_records(distance): + records = [] + for state, depth in distance.items(): + if depth > 4: + continue + key, place = 0, 1 + for row in state: + for value in row: + key += value*place + place *= 3 + records.append((key, depth)) + return b"".join(struct.pack(" 0 + and middle_control["minimum_through_nine"] == 9, "essential middle-gate control") + ball, target = native_case(engines, directory, 6, "103425") + require(target == {"n": 6, "permutation": "103425", "layers": [1, 66, 2655, 83270, 2213925], + "states": 2299917, "generators": 66, "transitions": 151794522, + "direct_hits": 0, "middle_hits": 0, "minimum_through_nine": None}, "target census") + target["canonical_ball_sha256"] = hashlib.sha256(ball).hexdigest() + return {"target": target, "dense_controls": small, "distance_nine_control": middle_control, + "invalid_native_inputs_rejected": 10} + + +def recognize(events, start, end): + """Exact 2x2 recognition, adapted from Ross Richardson's PR1216.""" + if start + 4 > end: + return None + block = events[start:start+4] + if any(event[0] != "scalar" for event in block): + return None + ops = [event[1] for event in block] + if [op[0] for op in ops] != ["add", "add", "add", "scale"]: + return None + a, b = tuple(ops[0][1]), tuple(ops[0][2]) + if a == b or a[0] != "L" or b[0] != "L": + return None + rows = {a: [F(1), F(0)], b: [F(0), F(1)]} + for op in ops: + target = tuple(op[1]) + if target not in rows: + return None + if op[0] == "add": + source = tuple(op[2]) + if source not in rows or source == target: + return None + rows[target] = [x + F(*op[3:5])*y for x, y in zip(rows[target], rows[source])] + else: + rows[target] = [F(*op[2:4])*x for x in rows[target]] + return (a, b) if rows[a] == [0, 1] and rows[b] == [1, 0] else None + + +def cycles_of(mapping): + pending = {a for a, b in mapping.items() if a != b} + result = [] + while pending: + first = min(pending) + cycle, cursor = [first], mapping[first] + while cursor != first: + require(cursor in pending and cursor not in cycle, "invalid cycle") + cycle.append(cursor) + cursor = mapping[cursor] + pending.difference_update(cycle) + result.append(cycle) + return result + + +def boundary_census(events): + result, cursor = [], 0 + while cursor < len(events): + if events[cursor][0] != "scalar": + cursor += 1 + continue + start, frame = cursor, events[cursor][2] + while cursor < len(events) and events[cursor][0] == "scalar" and events[cursor][2] == frame: + cursor += 1 + end, position, starts, mapping = cursor, start, [], {} + while position < end: + pair = recognize(events, position, end) + if pair is None: + position += 1 + continue + a, b = pair + mapping.setdefault(a, a) + mapping.setdefault(b, b) + mapping[a], mapping[b] = mapping[b], mapping[a] + starts.append(position) + position += 4 + if starts: + result.append({"start": start, "end": end, "frame": frame, "swap_starts": starts, + "permutation": [[list(a), list(b)] for a, b in sorted(mapping.items())], + "cycles": [[list(a) for a in cycle] for cycle in cycles_of(mapping)]}) + return result + + +def invoice(): + prior, result = read(ROOT / PREVIOUS), {} + for provider in ("ck", "jp8"): + programs = read(ROOT / (PROVIDERS + provider + "/LOCAL-PROGRAMS.json.gz")) + checks = read(ROOT / (PROVIDERS + provider + "/LOCAL-CHECKS.json")) + for direction in ("forward", "backward"): + key, events = provider + "/" + direction, programs[direction] + require(hashlib.sha256(canonical(events)).hexdigest() == checks[direction]["sha256"], "event source digest") + blocks = boundary_census(events) + require(blocks == prior["candidate_blocks"][key], "complete historical boundary census") + types = Counter(tuple(sorted(map(len, block["cycles"]))) for block in blocks) + require(types == {(2,): 28, (2, 3): 14}, "historical cycle profile") + result[key] = {"boundaries": len(blocks), "two_cycles": 28, "two_plus_three_cycles": 14, + "disposable_component_cost": 224, "restored_component_minimum": 252, + "separate_complex_components_extra": 56, + "census_sha256": hashlib.sha256(canonical(blocks)).hexdigest()} + return result + + +def main(): + ap = argparse.ArgumentParser(description=__doc__) + ap.add_argument("--record", type=Path) + ap.add_argument("--quick", action="store_true", help="no native lower-bound replay") + args = ap.parse_args() + pins() + result = {"format": "restored-cycle-gap-v1", "exact": exact_checks(), "historical_invoice": invoice()} + if args.quick: + print("PASS_RESTORED_CYCLE_QUICK exact_upper=10 historical_boundaries=168 full_lower_bound_not_replayed") + return + with tempfile.TemporaryDirectory(prefix="restored-cycle-gap-") as directory: + result["finite_exclusion"] = native_checks(Path(directory)) + if args.record: + with args.record.open("x") as stream: + stream.write(json.dumps(result, indent=2, sort_keys=True) + "\n") + else: + require(result == read(HERE / "EXPECTED.json"), "receipt drift") + print("PASS_RESTORED_CYCLE_GAP exact_minimum=10 arbitrary_dirty_donors states=2299917 middle_tests=151794522 historical_component_bill=252 no_new_kappa") + + +if __name__ == "__main__": + main()