From 381f5d6146488a20e29e79c2f2dd12630309e258 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 27 Oct 2026 19:36:03 +0000 Subject: [PATCH] feat(research): bypass unit-modulus quarter-carry work --- research/unit-modulus-carry-bypass/PROOF.md | 133 ++++++++++ research/unit-modulus-carry-bypass/README.md | 106 ++++++++ .../unit-modulus-carry-bypass/SOURCES.json | 54 +++++ research/unit-modulus-carry-bypass/TASK.json | 92 +++++++ .../unit-modulus-carry-bypass/VERIFY.json | 41 ++++ research/unit-modulus-carry-bypass/verify.py | 227 ++++++++++++++++++ research/unit-modulus-carry-bypass/wrapper.py | 41 ++++ 7 files changed, 694 insertions(+) create mode 100644 research/unit-modulus-carry-bypass/PROOF.md create mode 100644 research/unit-modulus-carry-bypass/README.md create mode 100644 research/unit-modulus-carry-bypass/SOURCES.json create mode 100644 research/unit-modulus-carry-bypass/TASK.json create mode 100644 research/unit-modulus-carry-bypass/VERIFY.json create mode 100644 research/unit-modulus-carry-bypass/verify.py create mode 100644 research/unit-modulus-carry-bypass/wrapper.py diff --git a/research/unit-modulus-carry-bypass/PROOF.md b/research/unit-modulus-carry-bypass/PROOF.md new file mode 100644 index 0000000000..7c0d3552ca --- /dev/null +++ b/research/unit-modulus-carry-bypass/PROOF.md @@ -0,0 +1,133 @@ +# The prefix and its uniform physical bounds + +This is a scoped construction in the nineteen-tape, seven-symbol machine +of the retained PR5849 quarter-carry leaf. One literal branch, write, unit +move, goto or halt costs one transition. Space is the sum of visited tape +interval lengths, including all nineteen initial head positions and erased +storage. These are the predecessor's currencies. + +## Declared interface and dependencies + +Let P,Q,S be positive canonical LSB-first binary descriptors. Q is odd. +Tape0 contains the complete original-owner Boolean stream of volume V=PQS. +Tape5 starts on the first Q bit. The valid supplied packet encodes k+16 in +five bits, with -16<=k<=12. All private and spectator contracts are exactly +those of the pinned source. The requested permutation is a rotation by +plus or minus k*4^-1 modulo Q in the Q coordinate, with all other state +restored. At Q=1 this is the identity, since there is only one coordinate. + +For odd Q>=3, cite the following nonunit conclusions from the section +"Physically supplied quarter code" of PR5849's retained PROOF.md: + +```text +T_old <= (1111/3)V, +W_old <= 24V. +``` + +These are used as predecessor results, not re-proved or independently +replayed. In particular the old offset producer, payload permutation, +restoration, and its analytic count remain that contribution. The two +source tables, interpreters and proof statements are bound in SOURCES.json. + +## A fixed seven-row table + +The following rows are prepended. All source destinations are increased by +seven, and the fallback goto targets seven plus the source entry. + +```text +0: move tape5 right +1: branch tape5: RIGHT -> 2, ZERO -> 4, ONE -> 4, other -> 6 +2: move tape5 left +3: halt +4: move tape5 left +5: goto relocated source entry +6: reject +``` + +This construction receives a source table and alphabet constants only. +It receives no runtime Q, packet, extent, payload or head position. +Selection occurs by a physical read on tape5. + +A canonical positive odd Q has first bit ONE. The next symbol is RIGHT +exactly when Q=1. In this case the executed rows are 0,1,2,3, costing +exactly four transitions. No tape is written. Tape5 moves one step right +and one step left, and every head therefore returns. The only visited +position beyond the nineteen initial positions is tape5's next position, +so W_new=20. Arbitrary payloads, descriptors and spectators are unchanged. +This proves the required endpoint for every P,S and valid packet at Q=1. + +For odd Q>=3, the next symbol is ZERO or ONE. The executed prefix rows are +0,1,4,5. These cost exactly four transitions and enter the retained program +in its original complete configuration, after relocation. Induction on +the old program's transitions proves that relocation preserves each tape +operation, branch choice, halt and rejection. Thus + +```text +T_new = T_old + 4 for Q>=3. +``` + +The prefix visits just the first two Q positions. The retained nonunit +descriptor producer already visits those positions: it checks tape5's first +ONE, moves right and reads the next bit before entering its general branch. +Thus the prefix adds no visited positions to a complete valid nonunit run, +and W_new=W_old there. + +## Improved complete bounds + +For Q>=3, V=PQS>=3, so the cited nonunit inequality gives + +```text +T_new <= (1111/3)V + 4 <= (1115/3)V, +W_new <= 24V. +``` + +For Q=1, V>=1, and the exact new counts give + +```text +T_new = 4 <= (1115/3)V, +W_new = 20 <= 24V. +``` + +Both directions therefore satisfy the displayed complete bounds for every +valid input. The transition coefficient decreases by exactly 289/3 from +the old tight uniform bound 468, and the sufficient visited-cell coefficient +decreases from 49 to 24. The new bounds need not be tight. Nonunit executions +pay four extra transitions; this is an improvement to the worst-case uniform +envelope over the whole interface, not a claim that each invocation is cheaper. + +The result preserves the successful-input contract. It does not promise +to diagnose invalid unused packets or private state in the unit branch. +Source-to-caller legality and the remaining G20 obligations in the README +are separate from this proof. + +## Implementation limits and verification choices + +The assembler transforms the pinned 31,873-row tables and rejects more than +100,000 input rows. Its loops are finite table traversals with at most seven +branch destinations per row. It neither interprets runtime descriptors nor +introduces a new runtime loop. Each changed function is under sixty lines. +Internal invariants use explicit checks that remain active under optimized +Python. The suffix checker independently reverses relocation before comparing +every row, rather than comparing the wrapper to a second call to itself. + +Managed Python allocation is a rule-3 deviation in the finite assembler and +verifier. Live allocations are bounded by the authenticated fixed table, +at most four payload bits for unit cases, 513 descriptor bits for prefix-only +cases, and 125 payload bits for complete compositions. Each simulated run +has at most 200,000 transitions. These verification limits do not restrict +the mathematical input domain. The retained interpreter owns any dynamic +simulation storage; no source runtime behavior is changed to satisfy them. + +Direct compilation of two authenticated interpreter sources and the local +wrapper is a rule-8 deviation. It prevents stale bytecode from replacing +the declared bytes, has three fixed module targets, checks fresh names, +and removes each temporary module entry on every exit. Negative-control +callbacks are a rule-9 deviation limited to six immediate checks with no +retained state. Follow-on changes to these bounds or targets require +revisiting the controls. The finite table, fixtures and execution caps +bound allocations and all loops. Warning-strict normal and optimized +registered replays check this scope. No static analyzer is configured for +this isolated package; diagnostics on the two new files are run if available. + +No predecessor verification suite, formal proof-kernel check or independent +human review is claimed. diff --git a/research/unit-modulus-carry-bypass/README.md b/research/unit-modulus-carry-bypass/README.md new file mode 100644 index 0000000000..f1cfe51d6d --- /dev/null +++ b/research/unit-modulus-carry-bypass/README.md @@ -0,0 +1,106 @@ +# A literal unit-modulus bypass for the G20 quarter-carry leaf + +**Scoped physical construction and written proof; no new kappa.** A fixed +seven-instruction prefix lowers the complete runtime quarter-carry leaf's +uniform bounds from **468V to 1115V/3 transitions** and from **49V to 24V +visited cells**, where V=PQS. The new bounds are sufficient upper bounds, +with no claim that they are optimal. + +For Q=1 the required rotation is the identity. The prefix physically reads +the next symbol of the canonical Q descriptor, restores its head and halts +in exactly four transitions. It visits exactly 20 cells under the retained +convention that all nineteen initial head positions count. For every odd +Q>=3 it restores the head and enters the original table after exactly four +additional transitions. Every retained instruction is unchanged apart from +the relocation of its finite program-counter destinations. + +The [proof](PROOF.md) combines this construction with Ali Romman's cited +nonunit bounds in [PR #5849](https://github.com/CrocSwap/integer-mult-bounds/pull/5849). +The predecessor's arithmetic, general carry implementation and all-route +envelope are dependencies, not results re-audited here. The delivered step +is the physical prefix and its improved uniform envelope. Earlier high-route +callers already skip high operations at Q=1, as documented by Sagar Thakrar +in [PR #3265](https://github.com/CrocSwap/integer-mult-bounds/pull/3265). +No priority for that general observation is claimed. + +The same valid interface is retained: positive canonical P,Q,S with Q odd, +the complete original-owner Boolean payload, a valid five-bit packet for +-16<=k<=12, the declared blank private tapes, and arbitrary spectators. +Both directions implement x -> x +/- k*4^-1 mod Q, preserve all descriptors +and spectators, restore every head, and return private storage blank. + +## Evidence and reproduction + +From the repository root, run these standard-library CPython 3.12 commands: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/unit-modulus-carry-bypass/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/unit-modulus-carry-bypass/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/unit-modulus-carry-bypass +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/unit-modulus-carry-bypass --check-source-history +``` + +The direct verifier prints a generated JSON receipt with status +`PASS_UNIT_MODULUS_CARRY_BYPASS`, hashes of its package and six declared +inputs, and these enumerated checks: + +- 1,972 unit-modulus executions cover both directions, every valid packet, + and every Boolean payload for shapes (1,1,1), (1,1,4) and (2,1,2). + All cells and heads agree with their entry state; the exact bill is 4 + transitions and 20 visited cells. A separate interpreter covers 58 of them. +- Eight descriptor-only prefix fixtures, including 513-bit Q, check the + exact four-transition return or four-transition fallback overhead with + occupied spectators, in both interpreters. +- Every fallback row in both 31,873-instruction source tables is compared + after independently undoing relocation. +- Six complete nonunit compositions in both interpreters cover Q=3,5,125 + and both directions, with a direct coordinate-gather oracle, full head + return and private erasure. The source's port9 fixture k=-3,Q=125 uses + residue 93. The new composition takes 16,694 transitions and visits 625 + cells in either direction. +- Six rejection controls cover each omitted descriptor-head return, an + altered fallback instruction, an understated transition bill, a wrong + tape count and an invalid entry state. + +The verifier writes no files. The source table, both interpreters and cited +source statements are pinned by Git blob and SHA-256 in [SOURCES.json](SOURCES.json). +The registered normal and optimized commands are in [VERIFY.json](VERIFY.json). +The finite checks corroborate the proof; they do not establish its unbounded +claims by extrapolation. + +## Limits + +Nonunit correctness and bounds are inherited from the exact retained #5849 +table and proof. This package does not repeat that predecessor's broad replay. +The Q=1 branch assumes valid descriptors and a valid packet; it does not +validate the unused payload, packet or private tapes. Invalid-input rejection +behavior is outside the successful-execution contract. + +This is a component improvement. The complete G20 caller has not been +installed or repriced with it. Low-cache packet formation and selection, +whole-T staging, low-type commit, physical ROW presentation, ancestor +stock/P3, and the full caller invoice remain open. All five framework +assumptions retain their status. There is no selected-frontier change, +new recursive saving, or complete multiplication theorem. + +## Open next questions + +Can a real low-cache row be joined to the supplied packet and this wrapped +leaf in one paid physical execution? Begin with the retained port9 witness +and include low-row selection, the homogeneous route, packet formation, +cache erasure and low-type commit. Whole-T staging and the actual ROW caller +map are the blockers. [TASK.json](TASK.json) records this question structurally. + +## Sources and credit + +Base canonical main is `19fdb086ea96af9a9f87936a2b888e10af4ed810`, priority +revision 8. The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19226097) +states this physical-leaf scope. + +This package was produced by Nick Petalas. Apache-2.0. Credit Ali Romman for +#5849's complete carry leaf, physical bounds, retained interpreters and source +envelope; David Arias for the literal machine and counter/stream macros; +JoyboyBrian for quarter arithmetic and affine owner reuse; Sagar Thakrar for +the earlier high-route Q=1 branch; Charles Bethin, Jose Manuel, Tekalign, +ToikY, and the retained tape/ROW/G20 contributors for the predecessor chain. +All retained source files and their original credit lines are unchanged. diff --git a/research/unit-modulus-carry-bypass/SOURCES.json b/research/unit-modulus-carry-bypass/SOURCES.json new file mode 100644 index 0000000000..473be1589f --- /dev/null +++ b/research/unit-modulus-carry-bypass/SOURCES.json @@ -0,0 +1,54 @@ +{ + "schema_version": 1, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/high-route-setup-invoice/README.md", + "usage": "input", + "git_blob": "fa28cf6792d57a8a07dff64b2837f321c2369a5d", + "sha256": "126f252765f99dbde98c57dadfac0fdae616de34409d84af3767b83ce96a5b9f" + }, + { + "path": "research/runtime-quarter-carry/PROOF.md", + "usage": "input", + "git_blob": "028a7777a3fc4a14dce28b555242c8e0a744b9a3", + "sha256": "bd51dd2ad2401fd68a4a5bfe1e4ae7009bc38f255badd6cecc4fbc7c6b905da6" + }, + { + "path": "research/runtime-quarter-carry/README.md", + "usage": "input", + "git_blob": "d3cfcbe49fc1416dc9799d55c56f7f033f7674dc", + "sha256": "d02d8dab32ca6dfda95666ee7c32720b2b90cf14ada7744e0ee1adb49ad1efe6" + }, + { + "path": "research/runtime-quarter-carry/TABLE.json.gz", + "usage": "input", + "git_blob": "f26183d28d8337863516eebfd5a48e2659b1eadc", + "sha256": "7222965c79faca34ad43af7e65dfb74e55b6fd0f7625658e82f9a580d5d20204" + }, + { + "path": "research/runtime-quarter-carry/inputs/independent.py", + "usage": "input", + "git_blob": "0d93b49039465369e79075c0ad93a3d389aa7678", + "sha256": "82ba16fae207f2141f986c7cc5788771b6a372a34b90cab67260bc4c7effc500" + }, + { + "path": "research/runtime-quarter-carry/inputs/machine.py", + "usage": "input", + "git_blob": "6ed03865cdb646d40573c132f841afbe335daba0", + "sha256": "04b7b76b9f06653d94d2158196cdd1bed7883dd1f59fcbc81a486e3ffb248681" + } + ] +} diff --git a/research/unit-modulus-carry-bypass/TASK.json b/research/unit-modulus-carry-bypass/TASK.json new file mode 100644 index 0000000000..ce5d19ac88 --- /dev/null +++ b/research/unit-modulus-carry-bypass/TASK.json @@ -0,0 +1,92 @@ +{ + "schema_version": 1, + "task_id": "bit-helper-contract", + "priority_revision": 8, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "original_card": { + "id": "bit-helper-contract", + "question": "Can a changed G20 helper path or independent-target split improve the complete BIT moment without losing its physical endpoint?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "research/g20-helper-split/README.md", + "research/g20-conjugation-admission/README.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "A full boundary contract and paid profile; unchanged scalar counts alone are insufficient. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "First read #5679/#5708 and their audits as pending component proposals. Choose one uncovered helper group/cut on an exact word; compare arbitrary-input native action, targets, owned storage, both orientations and full signed bill. Stop if the gain is only a scalar count or repaid by lost targets. Do not rerun the frozen #5609 common-frame domain without changing its hypothesis.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "G20", + "helper split", + "5679", + "5708", + "independent target" + ], + "existing_checks": [ + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "A fixed unit-modulus bypass for the literal PR5849 quarter-carry leaf, preserving its valid input/output interface and improving its uniform physical transition and visited-cell bounds.", + "scope_change_reason": "This is a physical leaf construction rather than a changed helper split or a complete BIT moment improvement. It addresses the implementation-cost part of the current BIT contract.", + "bottleneck_link": "The G20 caller still needs complete physical route costs. This reduces one declared carry-leaf bound while leaving low-cache production, whole-T staging, ROW presentation, stock/P3 and the full caller invoice open.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified original wrapper improvement; package it without optimizing the remaining nonunit program.", + "outcome": "completed", + "evidence": "PROOF.md gives the scoped construction and all-size bound; wrapper.py builds it; verify.py enumerates all declared controls and emits a hash-bound receipt.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can the supplied quarter-code packet be formed from a real low-cache row and composed with this wrapped leaf?", + "why_it_matters": "The packet producer remains outside the complete G20 carry-layer contract.", + "first_step": "Use the PR5849 port9 k=-3,Q=125 witness; include low-row selection, homogeneous route, packet formation and low-type commit in one paid physical execution.", + "blocked_by": "Whole-T staging and the actual ROW caller map remain unspecified at this leaf boundary." + } + ], + "coordination": { + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19226097", + "source": "PR #5849", + "source_author": "aliromman", + "upstream_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "checked_at": "2026-10-27T19:30:00Z" + }, + "verification_environment": { + "implementation": "CPython", + "python": "3.12.15", + "system": "Darwin", + "release": "27.0.0", + "machine": "arm64", + "dependencies": "standard library only" + } +} diff --git a/research/unit-modulus-carry-bypass/VERIFY.json b/research/unit-modulus-carry-bypass/VERIFY.json new file mode 100644 index 0000000000..ea3649ced6 --- /dev/null +++ b/research/unit-modulus-carry-bypass/VERIFY.json @@ -0,0 +1,41 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/high-route-setup-invoice/README.md", + "research/runtime-quarter-carry/PROOF.md", + "research/runtime-quarter-carry/README.md", + "research/runtime-quarter-carry/TABLE.json.gz", + "research/runtime-quarter-carry/inputs/independent.py", + "research/runtime-quarter-carry/inputs/machine.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact wrapper branches and tolls; all relocated fallback rows; 1972 complete unit executions; separate interpreter cases; six full nonunit composition fixtures; six negative controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same scientific checks with optimization enabled; all need checks remain active." + } + ] +} diff --git a/research/unit-modulus-carry-bypass/verify.py b/research/unit-modulus-carry-bypass/verify.py new file mode 100644 index 0000000000..8a26d5c2ad --- /dev/null +++ b/research/unit-modulus-carry-bypass/verify.py @@ -0,0 +1,227 @@ +"""Verify the wrapper, its interface, and complete composition fixtures. + +Produced by Nick Petalas. Apache-2.0. No predecessor verifier is invoked. +""" + +from copy import deepcopy +from fractions import Fraction +from hashlib import sha256 +from itertools import product +from pathlib import Path +import gzip +import json +import sys +import types + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +SOURCE = ROOT / "research/runtime-quarter-carry" + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def load(name, path): + """Compile authenticated source bytes directly, without bytecode caches.""" + module = types.ModuleType(name) + module.__file__ = str(path) + need(name not in sys.modules, "fresh module name") + sys.modules[name] = module + try: + exec(compile(path.read_bytes(), str(path), "exec"), module.__dict__) + finally: + sys.modules.pop(name, None) + return module + + +def authenticate(): + manifest = json.loads((PACKAGE / "SOURCES.json").read_text()) + inputs = [row for row in manifest["files"] if row["usage"] == "input"] + need(len(inputs) == 6, "complete input closure") + for row in inputs: + need(sha256((ROOT / row["path"]).read_bytes()).hexdigest() == row["sha256"], + "source bytes: " + row["path"]) + return {row["path"]: row["sha256"] for row in inputs} + + +def native_program(machine, table): + rows = [] + for row in table["instructions"]: + if row[0] == "branch": + row = (row[0], row[1], tuple(tuple(p) for p in row[2]), row[3]) + rows.append(tuple(row)) + return machine.Program(tuple(rows), table["tapes"], table["entry"]) + + +def bank_for(dense, shape, payload, code): + origins = [11 * tape - 61 for tape in range(19)] + bank = [({o - 5: dense.ONE, o: dense.MARK, o + 7: dense.ZERO}, o) + for o in origins] + bank[0] = dense.marked([dense.ONE if b else dense.ZERO for b in payload], origins[0]) + for tape, extent in zip((4, 5, 7), shape): + bank[tape] = dense.binary(extent, origins[tape]) + for tape in (2, 3, 8, 10, 11, 12, 13, 14, 15): + bank[tape] = ({}, origins[tape]) + packet = [dense.ONE if (code + 16) >> bit & 1 else dense.ZERO for bit in range(5)] + bank[16] = dense.marked(packet, origins[16]) + return bank + + +def native_run(machine, program, bank, cap): + result = machine.Machine(program, [machine.Tape(cells, head) for cells, head in bank]) + result.run(cap) + state = [(dict(tape.cells), tape.head) for tape in result.tapes] + spans = [max(visited or {tape.head}) - min(visited or {tape.head}) + 1 + for tape, visited in zip(result.tapes, result.visits)] + return state, result.steps, sum(spans) + + +def dense_run(dense, table, bank, cap): + tapes, steps = dense.execute(table, bank, cap) + return ([(t.snapshot(), t.head) for t in tapes], steps, + sum(t.high - t.low + 1 for t in tapes)) + + +def structural_check(original, wrapped): + """Undo relocation independently and compare every retained row.""" + need(len(wrapped["instructions"]) == len(original["instructions"]) + 7, + "exact seven-row prefix") + need(wrapped["instructions"][5] == ["goto", original["entry"] + 7], + "fallback enters original entry") + for before, after in zip(original["instructions"], wrapped["instructions"][7:]): + decoded = deepcopy(after) + if decoded[0] == "branch": + for pair in decoded[2]: + pair[1] -= 7 + decoded[3] -= 7 + elif decoded[0] == "goto": + decoded[1] -= 7 + need(decoded == before, "unaltered fallback instruction") + + +def unit_cases(machine, dense, tables, programs): + count = dense_count = 0 + for inverse in (False, True): + for code in range(-16, 13): + for p, s in ((1, 1), (1, 4), (2, 2)): + for bits in product((0, 1), repeat=p * s): + bank = bank_for(dense, (p, 1, s), bits, code) + result = native_run(machine, programs[inverse], bank, 5) + need(result == (bank, 4, 20), "unit branch preserves every cell and head") + if p == s == 1 and bits == (1,): + need(dense_run(dense, tables[inverse], bank, 5) == result, + "separate unit interpreter") + dense_count += 1 + count += 1 + return count, dense_count + + +def prefix_cases(machine, dense, wrapper): + stub = {"tapes": 19, "entry": 0, "instructions": [["halt"]]} + table = wrapper.wrap(stub, vars(machine)) + program = native_program(machine, table) + count = 0 + # Descriptor-only prefix tests allocate no Q-sized payload. + moduli = [1, 3, 5] + [(1 << bits) + 1 for bits in (3, 8, 31, 128, 512)] + for q in moduli: + bank = [({-7: dense.ONE, 0: dense.MARK, 9: dense.ZERO}, 0) for _ in range(19)] + bank[5] = dense.binary(q, -23) + result = native_run(machine, program, bank, 6) + need(result == (bank, 4 if q == 1 else 5, 20), "exact prefix toll and restoration") + need(dense_run(dense, table, bank, 6) == result, "separate prefix interpreter") + count += 1 + return count + + +def composition_cases(machine, dense, tables, programs): + rows = [] + for shape, code in (((1, 3, 1), 12), ((2, 5, 3), -16), ((1, 125, 1), -3)): + p, q, s = shape + payload = [int(index == 7 % (p * q * s)) for index in range(p * q * s)] + offset = code * pow(4, -1, q) % q + for inverse in (False, True): + bank = bank_for(dense, shape, payload, code) + sign = -1 if inverse else 1 + expected = [payload[(a * q + (x - sign * offset) % q) * s + z] + for a, x, z in product(range(p), range(q), range(s))] + target = deepcopy(bank) + target[0] = dense.marked([dense.ONE if bit else dense.ZERO for bit in expected], + bank[0][1] - 1) + result = native_run(machine, programs[inverse], bank, 200_000) + need(result[0] == target, "composed original-owner rotation and restoration") + need(dense_run(dense, tables[inverse], bank, 200_000) == result, + "separate complete composition interpreter") + need(3 * result[1] <= 1115 * len(payload), "new transition envelope") + need(result[2] <= 24 * len(payload), "new visited-cell envelope") + rows.append(dict(shape=list(shape), code=code, inverse=inverse, + steps=result[1], visited=result[2])) + return rows + + +def reject(action): + try: + action() + except (ValueError, RuntimeError): + return + raise ValueError("negative control was accepted") + + +def controls(machine, dense, tables, programs, wrapper, originals): + bank = bank_for(dense, (1, 1, 1), [1], -3) + for index in (2, 4): + bad = deepcopy(tables[False]) + bad["instructions"][index] = ["goto", index + 1] + q = 1 if index == 2 else 5 + fixture = bank if q == 1 else bank_for(dense, (1, q, 1), [1] + [0] * (q - 1), -3) + reject(lambda: need(native_run(machine, native_program(machine, bad), fixture, 100_000)[0][5][1] + == fixture[5][1], "omitted descriptor return")) + wrong = deepcopy(tables[False]) + wrong["instructions"][7] = ["halt"] + reject(lambda: structural_check(originals[False], wrong)) + reject(lambda: need(native_run(machine, programs[False], bank, 5)[1] <= 3, + "understated four-transition bill")) + reject(lambda: wrapper.wrap({"tapes": 18, "entry": 0, "instructions": [["halt"]]}, + vars(machine))) + reject(lambda: wrapper.wrap({"tapes": 19, "entry": 1, "instructions": [["halt"]]}, + vars(machine))) + return 6 + + +def run(): + input_hashes = authenticate() + machine = load("carry_bypass_retained_machine", SOURCE / "inputs/machine.py") + dense = load("carry_bypass_retained_dense", SOURCE / "inputs/independent.py") + wrapper = load("carry_bypass_wrapper", PACKAGE / "wrapper.py") + raw = (SOURCE / "TABLE.json.gz").read_bytes() + need(len(raw) < 1_000_000, "bounded compressed source table") + unpacked = gzip.decompress(raw) + need(len(unpacked) < 10_000_000, "bounded authenticated table payload") + source = json.loads(unpacked) + tables, programs, originals = {}, {}, {} + for inverse in (False, True): + original = source["quarter:" + str(inverse)] + originals[inverse] = original + tables[inverse] = wrapper.wrap(original, vars(machine)) + structural_check(original, tables[inverse]) + dense.validate(tables[inverse]) + programs[inverse] = native_program(machine, tables[inverse]) + units = unit_cases(machine, dense, tables, programs) + prefixes = prefix_cases(machine, dense, wrapper) + compositions = composition_cases(machine, dense, tables, programs) + negative = controls(machine, dense, tables, programs, wrapper, originals) + need(Fraction(1111, 3) + Fraction(4, 3) == Fraction(1115, 3) < 468, + "strict transition-bound improvement") + files = sorted(path for path in PACKAGE.iterdir() if path.is_file()) + return dict(status="PASS_UNIT_MODULUS_CARRY_BYPASS", unit_cases=units[0], + separate_unit_cases=units[1], prefix_cases=prefixes, + composition_cases=compositions, negative_controls=negative, + transitions_per_volume="1115/3", visited_per_volume=24, + input_sha256=input_hashes, + package_sha256={path.name: sha256(path.read_bytes()).hexdigest() for path in files}) + + +if __name__ == "__main__": + need(sys.argv[1:] == [], "no output or mutation options") + print(json.dumps(run(), indent=2, sort_keys=True)) diff --git a/research/unit-modulus-carry-bypass/wrapper.py b/research/unit-modulus-carry-bypass/wrapper.py new file mode 100644 index 0000000000..da585d6657 --- /dev/null +++ b/research/unit-modulus-carry-bypass/wrapper.py @@ -0,0 +1,41 @@ +"""Prepend a literal unit-modulus return to a fixed quarter-carry table. + +Produced by Nick Petalas. Apache-2.0. +The retained tape machine and quarter-carry table keep their source credit. +""" + +PREFIX_SIZE = 7 +MAX_INSTRUCTIONS = 100_000 + + +def wrap(program, symbols): + """Accept the pinned table ABI, without receiving any runtime values.""" + rows = program["instructions"] + if program["tapes"] != 19 or not 0 < len(rows) <= MAX_INSTRUCTIONS: + raise ValueError("bounded nineteen-tape input table required") + entry = program["entry"] + if type(entry) is not int or not 0 <= entry < len(rows): + raise ValueError("invalid retained entry") + zero, one, right = (symbols[name] for name in ("ZERO", "ONE", "RIGHT")) + prefix = [ + ["move", 5, 1], + ["branch", 5, [[right, 2], [zero, 4], [one, 4]], 6], + ["move", 5, -1], + ["halt"], + ["move", 5, -1], + ["goto", entry + PREFIX_SIZE], + ["reject", "canonical positive odd modulus required"], + ] + suffix = [] + for row in rows: + if row[0] == "branch": + suffix.append(["branch", row[1], + [[s, pc + PREFIX_SIZE] for s, pc in row[2]], + row[3] + PREFIX_SIZE]) + elif row[0] == "goto": + suffix.append(["goto", row[1] + PREFIX_SIZE]) + elif row[0] in ("move", "write", "halt", "reject"): + suffix.append(list(row)) + else: + raise ValueError("unsupported retained instruction") + return {"tapes": 19, "entry": 0, "instructions": prefix + suffix}