diff --git a/research/resident-scale-ribbon/ENGINEERING.md b/research/resident-scale-ribbon/ENGINEERING.md new file mode 100644 index 0000000000..67b800604a --- /dev/null +++ b/research/resident-scale-ribbon/ENGINEERING.md @@ -0,0 +1,47 @@ +# Verification and implementation bounds + +Playbook: autonomous local run. Exit predicate: one original, verified resident +SCALE transition saving, packaged for independent review. Stop after that step. +Build the Lever led to a retained physical compiler and deterministic verifier. +Prove It Works led to literal metered execution and full endpoint comparisons. + +The new call graph is acyclic. Compiler loops are bounded by W <= 64, D <= 64, +at most 24320 gates and 220000 emitted instructions. Each unit seek has a bound +from the fixed tape capacity. Tape storage is allocated once at construction, +with at most 131072 bits per tape. Transfer length is at most 8192 bits. The +scientific suite has 129 basis columns, 1364 legal pairs, 252 bounded +width/dimension cases and 24 full physical comparisons. The seven expected +rejections and three semantic controls have explicit finite domains. + +Rule 3, managed allocation deviation. Python lists, tuples and arbitrary-size +integers allocate during compilation and execution. Directly forbidding that +allocation conflicts with the supplied CPython replay interface. Scope is this +fixed finite compiler/verifier only. Explicit width/dimension, route and tape +capacities bound live payloads; one comparison fixture runs at a time. The +largest full owner fixture is 99072 bits. The runtime's internal allocations +are not separately instrumented. A lower-level fixed-storage executor is a +separate integration step, required before a uniform physical runtime claim. + +Rules 8/9, authenticated source loading deviation. The comparison compiler is +loaded from one hash-checked retained Python file by importlib. Its only +invoked scientific path is compile_route on the single 380-gate SCALE 2 +circuit and its fixed certificate. There is no arbitrary module selection, +network fetch or predecessor whole-word replay. Its original code is frozen. +Source compiler loops operate on the fixed authenticated row, width 64 and +finite heads. Replacing this adapter is unnecessary for the new construction; +an eventual standalone lower-level implementation can consume its literal +instruction output instead. + +New functions remain below sixty physical lines. Runtime guards validate +compiler capacities, tape boundaries, legal instructions and restored finite +control. The gate-count assertion is supplementary; every scientific check +and contract uses optimization-preserved exceptions. New code is warning-strict +and syntax-checked, and the complete verifier also runs under optimized Python. +No repository Python linter is installed in the available environment. Shared +diagnostics configuration and immutable source files are unchanged. + +The tariff counts logical tape reads, writes and unit moves. A read/XOR is one +read, and a conditional flip is a read plus write under the same finite-control +model as the predecessor. Python compilation, fixture construction, snapshots, +metadata hashing and host interpreter overhead are outside this operation bill. +The result is not a wall-clock measurement or an encoded-D machine compiler. diff --git a/research/resident-scale-ribbon/NOTICE b/research/resident-scale-ribbon/NOTICE new file mode 100644 index 0000000000..f2b4e739b8 --- /dev/null +++ b/research/resident-scale-ribbon/NOTICE @@ -0,0 +1,7 @@ +Resident SCALE 2 construction produced by Nick Petalas. +Apache-2.0. + +Retained PR6530 source bytes are by Ali Romman and their credited predecessors. +Their original notice is in inputs/PR6530-NOTICE. Original credit lines in +source files are unchanged. The new adjacent-swap resident compiler and its +traffic proof are distinguished from the retained interface and scalar circuit. diff --git a/research/resident-scale-ribbon/ORIGINS.json b/research/resident-scale-ribbon/ORIGINS.json new file mode 100644 index 0000000000..fea6f4f901 --- /dev/null +++ b/research/resident-scale-ribbon/ORIGINS.json @@ -0,0 +1,37 @@ +{ + "repository": "aliromman/integer-mult-bounds", + "commit": "fadaba3bb16a6965fa5e9c2c7af3a9df6ddf01bf", + "source_directory": "research/p104-exclusive-field-cache", + "files": [ + { + "path": "CERTIFICATES.json.gz", + "sha256": "87bbb8aa68a6f212e479ccfd70340ccb613782b3be6e8942112f4efbf3ca7698", + "git_blob": "13d8cef654794318d11e655a63ce95a78f0043a8", + "source_path": "inputs/CERTIFICATES.json.gz" + }, + { + "path": "CIRCUITS64.json.gz", + "sha256": "1652edd8c29d4cf6ca2ad6b771d9c5b0ba5a74cbcea999b1ee1f935a1a89255b", + "git_blob": "50ce55861aa769a23d60886418d4e9ec543a8cfb", + "source_path": "inputs/CIRCUITS64.json.gz" + }, + { + "path": "PR6530-PROOF.md", + "sha256": "8ec44a09040a88bd0e43b60ebb8c3f282d6bed63692c48e6d7aa7b4852af69ca", + "git_blob": "35698b776e1eb0532bf6a3b4b741c31003d49f10", + "source_path": "PROOF.md" + }, + { + "path": "cache.py", + "sha256": "c7ada185cb2337dec80e1ef8c60045b57d104a9e4a719bd7391b5566dcd37df4", + "git_blob": "19822f46079c3cb7890a402cdf272d9eb4ae755c", + "source_path": "inputs/cache.py" + }, + { + "path": "PR6530-NOTICE", + "source_path": "NOTICE", + "sha256": "e875893efa14fd80e3e86a0a900de652123492e95d2797edc54adf1ebeb3e83a", + "git_blob": "332a64b9e2282a6a3b01f8d474f8f08820edf3a6" + } + ] +} diff --git a/research/resident-scale-ribbon/PROOF.md b/research/resident-scale-ribbon/PROOF.md new file mode 100644 index 0000000000..78da335fbb --- /dev/null +++ b/research/resident-scale-ribbon/PROOF.md @@ -0,0 +1,147 @@ +# Resident doubling on one physical ribbon + +This scoped circuit construction and traffic proof was produced by Nick Petalas. +The construction answers the same-ribbon SCALE question in Ali Romman's PR6530. +It does not supply a new complete caller bill or a new kappa. + +## Contract + +Fix a record width W >= 2 and a positive payload dimension D. One resident +complex field occupies 2D consecutive W-bit two's-complement records on a +single ribbon, in the predecessor's interleaved real/imaginary order. Each +signed component x satisfies -2^(W-2) <= x < 2^(W-2), the exact-doubling +no-overflow condition. The other resident ribbon is arbitrary. Both evacuated +owner slots are zero. All ribbon heads and the clean finite-control bits begin +at zero. The owner head may be anywhere legal. + +The output doubles every component exactly, returns the active ribbon head +and control bits to zero, and leaves the other ribbon, all owner cells, the +owner head and the separate carry tape unchanged. The compiled schedule uses +one of the two available finite-control bits. It needs no new tape, clean +payload field, read from an evacuated owner, or field movement. + +The written construction applies to every finite W and D. The supplied emitter +admits 2 <= W <= 64 and 1 <= D <= 64 to bound its materialized instruction list. +Finite tests cover the explicitly reported domains, not every admitted input. + +## Bit map and exact inverse + +Write a record as bits b_0,...,b_(W-1), least significant first. Swap adjacent +positions (W-2,W-1), then (W-3,W-2), down to (0,1). This is the left cyclic +rotation + + (b_(W-1), b_0, b_1, ..., b_(W-2)). + +Each swap is the three CNOTs i->i+1, i+1->i, i->i+1. Finally apply CNOT +W-1->0. The resulting low bit is b_(W-1) XOR b_(W-2); every higher bit is +the previous lower bit. The no-overflow condition makes the top two input +bits equal. Consequently the new low bit is zero and this is exact signed +doubling. On arbitrary bit strings it remains an invertible linear map. +Reverse the full CNOT sequence to obtain its two-sided inverse. + +The retained source SCALE 2 circuit performs the same cyclic rotation by +successive swaps with position zero, followed by the same sign-clearing +CNOT, separately in its two records. The new schedule changes the rotation +factorization to neighboring swaps and puts both records on one ribbon. +The source circuit, its arithmetic contract and its previous two-ribbon +control-cache result retain their predecessor credit. The verifier compares +the new map, the literal retained source route and a separate logical gate +interpreter on all 129 basis columns, including the source carry coordinate. +This is a dependency check for the new construction, not a new predecessor +audit or a claim to its original result. + +For a CNOT c->t, read c into a zero control bit, seek t, read and conditionally +write t, seek c and read c again to clear the control bit. The target differs +from the control, so the second control read restores the control bit. The +operation is reversible for arbitrary data. All seeks expand to unit moves. +The schedule is fixed by W,D and the instruction pointer; no payload-dependent +head index, numeric cardinality oracle or hidden payload access is used. + +## Exact new traffic + +There are 3(W-1)+1 = 3W-2 CNOTs per record. Each costs three reads and one +write. For N = 2D records, reads are D(18W-12) and writes are D(6W-4). + +In the first record, the adjacent swaps cost 8(W-1) moves, with W-2 initial +moves and W-2 moves between successive swaps. The final long CNOT costs +3(W-1). Thus the first record costs 13W-15 moves and ends at W-1. Every +subsequent record costs 13W-14 moves, because its first control is W-1 +positions beyond the preceding exit. The final head return costs NW-1. +The total movement is N(14W-14)-2 = 28D(W-1)-2. + +Adding reads, writes and moves gives + + new(W,D) = D(52W-44)-2. + new(64,D) = 3284D-2. + +The predecessor's retained width-64 SCALE 2 route costs 9840D before its +staging transfers. The new resident circuit therefore saves 6556D+2 even +against that local term alone. This is an operation count, not wall time. + +## A complete comparison with identical entry and exit + +Use the actual selected word's adjacent events 10481..10483, with zero-based +indices: + + ADD 256 <- 256 - (1/2)257 + SCALE 257 <- 2*257 + ADD 257 <- 257 + (3/2)256 + +Both named fields can be resident before SCALE and are needed again by the +following ADD. For the comparison fixture, field 256 occupies bank zero, +field 257 bank one, and the owner head is at the end of field 256. This is +a legal entry. We do not claim a patched full predecessor policy. + +The old normalized path evicts both fields, executes the retained SCALE +staging/circuit, reacquires both fields into the same respective banks, and +returns the owner head to its entry. Try both eviction orders and both +acquisition orders. The other field's arbitrary data and all unrelated owner +cells are preserved. This supplies exactly the new path's physical endpoint. +The next ADD can bind its target/source tape arguments to those banks as in +PR6530. No physical bank swap is implied or free. + +Here is the complete affine calculation for all D >= 1. Let L=128D. From +the end of field i to the start of field j the distance is +abs((j-i-1)L+1). Its affine coefficients are 128*abs(j-i-1) and +1 when +j-i-1 >= 0, or -1 otherwise. A whole-field clean transfer, including ribbon +rewind, costs 1152D-3 in addition to this seek. It performs six accesses per +bit and three traversals of L-1 cells. + +The inherited SCALE staging costs its entrance seek plus +2688D-267, before the 9840D local circuit. To derive that staging term, +the source transfer reads/writes total 24WD. Its moves, excluding entrance +seek, are 3(2DW-1)+8(DW-1)+4(D-1)W = 18WD-11-4W. +This is the explicit increasing-record staging path, including all rewinds. +After reacquisition, returning from the end of field j to the end of field +256 costs abs(j-256)L. Every sign in these absolute values is fixed on +D >= 1, so these are affine proofs, rather than extrapolation from samples. + +For eviction/acquisition orders 01/01, 01/10, 10/01, 10/10 the complete +costs are respectively + + 17776D-280, 17776D-282, 17776D-278, 17776D-280. + +The best stated normalized flush path costs 17776D-282. The resident circuit +costs 3284D-2, saving 14492D-280, positive for every D >= 1. At D=1 the +complete comparison is 17494 versus 3282, a saving of 14212 operations. +This is a minimum over those four explicit normalization paths only. +The verifier executes all four paths at D=1,2,3 with two payloads each, +checks their full tapes and heads, and matches the affine bills exactly. + +## Limits and credit + +Classical adjacent transpositions, CNOT swaps, reversible finite control and +two's-complement arithmetic retain their usual credit. The new contribution +is their charged same-ribbon SCALE implementation under this exact exclusive +owner contract. Ali Romman supplies PR6530's interface, open question and +comparison policy, PR6527's staging and PR6513/6511's scalar/tape lineage. +Credit Nick Petalas for the retained scalar circuits, Sagar Thakrar / PR3241 +for metered tape work, DreamingOfClouds / PR6030 and all retained native, +owner, precision and compiler predecessors. Original source files and credit +lines are preserved in inputs. + +Only SCALE 2 is implemented here. The full caller policy is not reoptimized; +native and reset flushes retain their original obligations. Uniform encoded-D +control, native semantics, precision/stock admission, complete supplier funding +and outer transfer remain open. No new kappa, selected-frontier change, +independent human acceptance or formal proof-kernel result is claimed. diff --git a/research/resident-scale-ribbon/README.md b/research/resident-scale-ribbon/README.md new file mode 100644 index 0000000000..c37fc65b7c --- /dev/null +++ b/research/resident-scale-ribbon/README.md @@ -0,0 +1,86 @@ +# Resident SCALE 2 without a whole-cache flush + +This scoped circuit construction and written traffic proof was produced by +Nick Petalas. It answers Ali Romman's released same-ribbon question in +[PR6530](https://github.com/CrocSwap/integer-mult-bounds/pull/6530). + +A resident width-64 complex field can be doubled on its existing ribbon for +exactly **3284D-2** reads, writes and unit head moves. The other resident field, +both zero owner slots, the owner head and the carry tape remain unchanged. +There is no additional payload workspace. Signed components must satisfy the +retained exact-doubling no-overflow condition. + +The retained source local circuit costs 9840D before staging. A complete +comparison for fields 256/257, with identical entry and exit, reduces the best +of four explicit flush/scale/reacquire paths from 17776D-282 to 3284D-2. +The saving is **14492D-280** for every positive D. At D=1 it is 14212 operations. +This is an exact operation count under the predecessor's tape tariff, not a +wall-clock speedup or a new complete caller bill. + +The new schedule rotates each record through neighboring CNOT swaps, then +clears the duplicated sign bit. Its inverse reverses the same gates. +[PROOF.md](PROOF.md) proves the bit map, ownership, all-D count and the precise +comparison class. [ribbon.py](ribbon.py) emits and executes the physical route. +The implementation bounds W at 64 and D at 64; the written construction holds +for arbitrary finite W >= 2 and positive D. + +## Reproduce + +From the repository root, with CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/resident-scale-ribbon/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -W error -B research/resident-scale-ribbon/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/resident-scale-ribbon +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/resident-scale-ribbon --check-source-history +``` + +Both registered commands are read-only. The optional `--receipt /absolute/path` +writes a generated result bound to all fifteen package-file hashes. No receipt +is handwritten. Expected final line: `PASS_RESIDENT_SCALE_RIBBON`. + +The complete finite replay checks 129 source/new basis columns, 1364 exhaustive +legal small-width complex pairs with exact inverses, 252 arbitrary-bit +width/dimension roundtrips with exact traffic, and 24 full physical comparison +paths with all tape cells and heads checked. Seven invalid-domain/instruction +controls reject, and three semantic controls distinguish sign clearing, +rotation direction and the CNOT swap identity. The source's compiler is used +only to obtain this comparison circuit; its whole-word verifier and policy +optimizer are not run. No predecessor result is claimed as a new audit. + +The selected word is a declared source-pinned input. The exact three-event +window at indices 10481..10483 needs the two fields on both sides of SCALE. +This establishes a relevant legal local contract, not a globally spliced +replacement for the source policy. ORIGINS.json binds the retained external +source bytes and their original Git blobs at PR6530's exact head. Those +committed copies make replay independent of the unmerged source branch's +ancestry; full predecessor history is not claimed. + +## Limits + +Only SCALE 2 is supplied. The complete caller policy is not reoptimized. +Initial allocation, native/reset implementation, uniform encoded-D control, +numerical admission, stock, full supplier funding and outer transfer remain +open. A component improvement does not raise kappa or change the selected +frontier. The five selected framework assumptions remain. Independent human +and formal proof-kernel review are unclaimed. Lean, Docker and a selected +supplier cold replay are outside scope. + +## Open next questions + +The structured questions in [TASK.json](TASK.json) concern integrating this +exact edge into a complete certified policy, then one different SCALE +coefficient with its full transition charged. Neither is reserved here. + +## Credit + +Ali Romman supplies PR6530's exclusive-owner contract, released question and +comparison policy, PR6527's staging and PR6513/6511's physical scalar lineage. +Credit Nick Petalas for the retained scalar circuits, Sagar Thakrar / PR3241, +DreamingOfClouds / PR6030 and the retained native, owner, precision and compiler +authors. Classical adjacent swaps, CNOT identities and two's-complement +arithmetic retain their usual credit. Original source credit lines are retained +unchanged in inputs. This contribution is under Apache-2.0. + +The replay-runtime card is explicitly changed to physical operation count. +The first verified resident transition improvement ended the construction work. diff --git a/research/resident-scale-ribbon/SOURCES.json b/research/resident-scale-ribbon/SOURCES.json new file mode 100644 index 0000000000..120a707639 --- /dev/null +++ b/research/resident-scale-ribbon/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/p104-helper470-twin-rung-removal/WORD.json.gz", + "usage": "input", + "git_blob": "22f9ab02d1b73ea0aa4b07ce445a14cc2602c760", + "sha256": "7834725d9e34ee846a9ccc615221ea81e0201613938afa185d2eda0c9a6c232f" + } + ] +} diff --git a/research/resident-scale-ribbon/TASK.json b/research/resident-scale-ribbon/TASK.json new file mode 100644 index 0000000000..4da61b23da --- /dev/null +++ b/research/resident-scale-ribbon/TASK.json @@ -0,0 +1,67 @@ +{ + "schema_version": 1, + "task_id": "replay-runtime", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "replay-runtime", + "question": "Can one measured replay bottleneck be sped up without dropping coverage?", + "starting_points": [ + "scripts/run_isolated_tests.py", + "scripts/verify_replay_coverage.py", + "certificates/selected-result.json" + ], + "methods": [ + "Profile one isolated replay and optimize the measured bottleneck.", + "Design source-bound reuse with explicit dependency invalidation and negative controls." + ], + "acceptance_gate": "Report before/after wall time on the same fixture, retained checks and invalidation behavior.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "Measure one unchanged fixture, preserve check coverage, and test one optimization with invalidation controls.", + "bottleneck_link": "Faster trustworthy replays increase review throughput and let mechanism candidates be checked sooner.", + "allowed_variations": [ + "Profile one stage or design one source-bound cache boundary." + ], + "scope_change_triggers": [ + "Skipping coverage or comparing different fixtures to claim speedup." + ], + "overlap_terms": [ + "replay runtime", + "cache invalidation", + "isolated tests" + ] + }, + "scope_status": "changed", + "actual_scope": "Construct a resident single-ribbon SCALE 2 with a charged identical-endpoint physical comparison.", + "scope_change_reason": "The released PR6530 question concerns physical tape traffic rather than mathematical replay runtime. No wall-clock speedup is claimed.", + "bottleneck_link": "Removing an internal SCALE flush addresses scalar physical movement while retaining arbitrary exclusive owners; complete caller funding remains open.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified same-ribbon transition saving; leave other coefficients and whole-word integration open.", + "outcome": "completed", + "evidence": "PROOF.md, ribbon.py and verify.py; exact traffic 3284D-2, compared with four complete normalized flush paths.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can this resident SCALE 2 edge improve the complete PR6530 caller policy?", + "why_it_matters": "The local saving does not determine the globally optimal owner-head and bank schedule.", + "first_step": "Add this exact edge to the source state graph, preserve native/reset flushes and certify the complete signed physical bill.", + "blocked_by": "A new whole-word policy and complete physical replay are not supplied." + }, + { + "question": "Which other selected SCALE coefficients have a beneficial same-ribbon implementation?", + "why_it_matters": "The source includes division and signed coefficients with different fixed-width contracts.", + "first_step": "Choose one coefficient and emit its literal single-head circuit with a matched full transition.", + "blocked_by": "No extension beyond SCALE 2 was attempted after the first improvement." + } + ] +} diff --git a/research/resident-scale-ribbon/VERIFY.json b/research/resident-scale-ribbon/VERIFY.json new file mode 100644 index 0000000000..1946874838 --- /dev/null +++ b/research/resident-scale-ribbon/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p104-helper470-twin-rung-removal/WORD.json.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact map/basis, signed arithmetic/inverse, literal head traffic and identical-endpoint flush comparisons; seven rejection and three semantic controls." + }, + { + "argv": [ + "{python}", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same complete checks with optimization enabled." + } + ] +} diff --git a/research/resident-scale-ribbon/inputs/CERTIFICATES.json.gz b/research/resident-scale-ribbon/inputs/CERTIFICATES.json.gz new file mode 100644 index 0000000000..13d8cef654 Binary files /dev/null and b/research/resident-scale-ribbon/inputs/CERTIFICATES.json.gz differ diff --git a/research/resident-scale-ribbon/inputs/CIRCUITS64.json.gz b/research/resident-scale-ribbon/inputs/CIRCUITS64.json.gz new file mode 100644 index 0000000000..50ce55861a Binary files /dev/null and b/research/resident-scale-ribbon/inputs/CIRCUITS64.json.gz differ diff --git a/research/resident-scale-ribbon/inputs/PR6530-NOTICE b/research/resident-scale-ribbon/inputs/PR6530-NOTICE new file mode 100644 index 0000000000..332a64b9e2 --- /dev/null +++ b/research/resident-scale-ribbon/inputs/PR6530-NOTICE @@ -0,0 +1,9 @@ +Apache-2.0. Ali Romman with substantial OpenAI Codex assistance; no subagents. +The exact predecessor notices are in inputs/NOTICE-PR6527 and NOTICE-PR6513. +Credit PR6527's complete field-staging construction and baseline, PR6513's +physical control-cache routes, PR6511's full selected scalar circuits, Nick +Petalas's scalar and paired-negation work, Sagar Thakrar's PR3241 tape model, +DreamingOfClouds / PR6030 and all retained P104/native/compiler lineage. +Exclusive ownership, caching, batching and dynamic programming are established +methods. This package supplies the selected source-bound physical field-cache +construction and its full cost certificate, not the predecessor constructions. diff --git a/research/resident-scale-ribbon/inputs/PR6530-PROOF.md b/research/resident-scale-ribbon/inputs/PR6530-PROOF.md new file mode 100644 index 0000000000..35698b776e --- /dev/null +++ b/research/resident-scale-ribbon/inputs/PR6530-PROOF.md @@ -0,0 +1,112 @@ +# Exclusive field cache for the selected scalar caller + +## Contract and ownership + +Keep PR6527's field-major owner tape, two clean complex-field staging tapes, +one clean carry bit and two payload control bits. At width W=64 and positive +payload dimension D, each staging tape has L=2DW bits. Owner backing is +102272D bits and clean staging backing is 256D bits. There are four tapes. +The compiled controller names fields and physical banks. Those static names +and the instruction pointer are not additional payload arrays. As in the +predecessor, no uniform encoded-D controller is supplied. + +A live field has exactly one authoritative location: its owner slot or one +staging tape. If it is staged, its complete owner slot is zero. A free staging +tape is zero. Cache tags do not authorize a read from an evacuated owner slot. +All data-ribbon heads are at zero between local events, except the owner head, +whose last field position is retained and priced. The carry and two control +bits return to zero after every circuit and transfer. + +Acquisition moves a complete field from its owner slot to a free staging tape. +Eviction moves it back to its zero owner slot. Use PR6527's exact clean transfer: +four reads, two writes per bit, with unit traversal and complete control return. +This is reversible data movement, not a copy followed by unpriced erasure. + +An ADD/COPY needs the two distinct named fields. Keep any required resident +field in its current bank. Evict unneeded fields and acquire missing operands. +The physical circuit takes the target and source bank in that order; a bank +assignment changes the compiled tape names, not the data. Run all 2D component +circuits and rewind both staging heads. Retain both complete fields afterward. +The ADD restores its source. COPY keeps its original clean-target precondition. + +Before SCALE, flush both cached fields and execute the exact PR6527 SCALE +protocol. It returns empty staging tapes and a complete owner tape. Before +MOVE, INIT, CLEAR and final exit, flush both fields and return the owner head +to zero. The external operation's payload work is not executed or priced here. +Its complete owner layout, clean-workspace and origin-return contract remains +a premise. Physical reset and native implementations remain open. + +The invariant is inductive: acquisition and eviction move the sole value; +the scalar circuit changes only its target and restores source/carry; the +flush restores the complete owner state before any external work. Unrelated +owner cells are never changed. Thus the selected scalar actions and ownership +are preserved for arbitrary valid record inputs and any positive D. + +## Exact policy class + +The policy has two whole-field buffers, no prefetch and no field relabeling. +A required resident field is kept in its current bank. For a missing field, +try each free-bank assignment. Try every order of the required evictions and +acquisitions that keeps each acquisition destination clean. Each transfer +traverses its record in increasing order. No payload field is acquired unless +the current ADD/COPY needs it. Every SCALE and external boundary flushes. +The scalar event order, layout, local circuits and workspace are fixed. + +A state is the ordered pair of resident field labels and the last owner-head +field, or the origin. At most four states occur at each selected event layer. +The state graph includes every allowed action order. No pruning or heuristic +search is used. The optimum does not cover other circuits, a SCALE that remains +cached, arbitrary prefetch, other layouts or weighted operation tariffs. + +## Affine cost proof + +Let the owner head be at the end of field i. The distance to field j is +`abs((j-i-1)*2WD+1)`. Its sign is fixed for every D>=1. From origin, the distance +is `2WD*j`. A full-field transfer adds `3*(2DW-1)` moves and `12DW` reads/writes. +It therefore costs the seek plus `18WD-3` operations. This includes both tape +traversals, staging rewind, every data read/write and clean control return. + +For an ADD/COPY, the unchanged local circuits cost `2D*local_cost`, and the +record-to-record travel and final rewind cost `4*(2D-1)*W`. SCALE uses the +predecessor's complete exact movement formula, adds `24DW` transfer reads and +writes and `D*local_cost`, after all required evictions. A boundary adds every +eviction and the final owner-head return. Every edge is affine in D. + +The producer uses D=1,2 minima to propose affine potentials. The checker uses +the exact symbolic edge formulas. For each edge difference AD+B, it requires +A>=0 and A+B>=0, which proves the potential inequality for every D>=1. It also +checks all reachable states and an attaining symbolic path. These checks give +a lower bound for every permitted path and a path that attains it. Two sample +dimensions alone would not prove this result. + +The complete scalar cost is `800847760D - 5118198`. The freshly checked PR6527 +baseline is `1236161936D - 5196390`. The improvement is +`435314176D - 78192`, strictly positive for every D>=1. This is about 35 percent +of the complete predecessor scalar bill, with exactly the same workspace. +All 7936D unimplemented bit-reset requests remain separate. No native, +initial-layout, uniform-control, full supplier or outer cost is set to zero. + +## Evidence and limits + +An independent symbolic checker tracks field authority and live ownership +without calling the optimizer's transition function. It checks the complete +selected word, every acquisition/eviction and all external boundaries. A +second whole-word evaluator runs all actual scalar gates and compares every +owner record at every prefix with exact signed arithmetic. Its native calls +are explicit fresh-grid stubs and its INIT/CLEAR actions are explicit reset +stubs. It does not prove native semantics, native accuracy or physical reset. + +Literal physical windows cover every one of the 43 scalar templates at D=1,2, +zero/one/two cache hits, SCALE flushes and all external boundary types. They +start from complete valid cache/owner states of the source policy. Arbitrary +window payloads check exact bit-circuit equality and exclusive-owner cleanup; +arithmetic preconditions are checked by the complete scalar/grid-stub trace. +All physical payload access uses the unchanged metered Tape methods. Direct +snapshots are only fixture observations, outside the execution bill. + +Each instance has compiled fixed-width and fixed-dimension control. The +all-D statement is about the family of these physical schedules, not a +uniform multiplication algorithm. The complete physical native word, actual +reset, precision admission, full supplier funding, outer transfer, independent +human review and proof-kernel acceptance remain open. No new kappa or selected +frontier change follows from this scalar result. diff --git a/research/resident-scale-ribbon/inputs/cache.py b/research/resident-scale-ribbon/inputs/cache.py new file mode 100644 index 0000000000..19822f4607 --- /dev/null +++ b/research/resident-scale-ribbon/inputs/cache.py @@ -0,0 +1,213 @@ +# SPDX-License-Identifier: Apache-2.0 +# Ali Romman with substantial OpenAI Codex assistance. +"""Compile a two-bit control cache with exact local tape costs.""" + +from itertools import combinations, permutations + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def location(width, wire): + require(type(wire) is int and 0 <= wire <= 2 * width, "wire domain") + return divmod(wire, width) + + +def visit(width, heads, wire): + bank, offset = location(width, wire) + new = list(heads) + cost = abs(new[bank] - offset) + new[bank] = offset + return tuple(new), cost + + +def edges(width, state, gate): + """Enumerate the declared no-prefetch cache policy.""" + old, heads = state + required = set(gate[:-1]) + target = gate[-1] + require(len(gate) in (2, 3) and len(set(gate)) == len(gate), "gate domain") + for wire in gate: + location(width, wire) + must_keep = set(old) & required + optional = sorted(set(old) - required - {target}) + for size in range(min(len(optional), 2 - len(required)) + 1): + for subset in combinations(optional, size): + keep = must_keep | set(subset) + actions = tuple((0, w) for w in sorted(set(old) - keep)) + actions += tuple((1, w) for w in sorted(required - keep)) + for order in permutations(actions): + held = set(old) + end = heads + cost = 0 + for load, wire in order: + if load: + if len(held) == 2: + break + held.add(wire) + else: + held.remove(wire) + end, movement = visit(width, end, wire) + cost += movement + 1 + else: + require(required <= held and target not in held, "valid cache at write") + end, movement = visit(width, end, target) + yield (tuple(sorted(held)), end), cost + movement + 2, order + + +def terminals(width, state): + held, heads = state + for order in permutations(held): + end, cost = heads, 0 + for wire in order: + end, movement = visit(width, end, wire) + cost += movement + 1 + yield cost + sum(end), order + + +START = ((), (0, 0, 0)) + + +def optimize(width, gates): + """Return all layer potentials and one attaining path.""" + layers = [{START: 0}] + parents = [] + for gate in gates: + nxt, parent = {}, {} + for state, value in sorted(layers[-1].items()): + for end, cost, order in edges(width, state, gate): + total = value + cost + if end not in nxt or total < nxt[end]: + nxt[end] = total + parent[end] = (state, order) + require(bool(nxt) and len(nxt) <= 100000, "exact state budget; no truncation") + layers.append(nxt) + parents.append(parent) + total, state, finish = min((value + cost, state, order) + for state, value in layers[-1].items() + for cost, order in terminals(width, state)) + path = [] + for parent in reversed(parents): + state, order = parent[state] + path.append(order) + require(state == START, "path entrance") + return {"total": total, "layers": [[[list(s[0]), list(s[1]), d] + for s, d in sorted(layer.items())] for layer in layers], + "actions": list(reversed(path)), "finish": finish} + + +def check_certificate(width, gates, certificate): + """Check a feasible potential lower bound and an attaining route.""" + layers = [] + for rows in certificate["layers"]: + layer = {} + for cache, heads, value in rows: + state = (tuple(cache), tuple(heads)) + require(state not in layer and type(value) is int and value >= 0, "potential rows") + layer[state] = value + layers.append(layer) + require(len(layers) == len(gates) + 1 and layers[0] == {START: 0}, "potential entrance") + for i, gate in enumerate(gates): + reachable = set() + for state, value in layers[i].items(): + for end, cost, _ in edges(width, state, gate): + reachable.add(end) + require(end in layers[i + 1] and layers[i + 1][end] <= value + cost, + "edge potential inequality") + require(reachable == set(layers[i + 1]), "complete reachable layer") + total = certificate["total"] + require(type(total) is int and total >= 0, "total domain") + for state, value in layers[-1].items(): + for cost, _ in terminals(width, state): + require(total <= value + cost, "terminal potential inequality") + require(len(certificate["actions"]) == len(gates), "path length") + state, cost = START, 0 + for gate, actions in zip(gates, certificate["actions"]): + actions = tuple(map(tuple, actions)) + matches = [(end, charge) for end, charge, order in edges(width, state, gate) if order == actions] + require(len(matches) == 1, "legal path transition") + state, charge = matches[0] + cost += charge + finish = tuple(certificate["finish"]) + matches = [charge for charge, order in terminals(width, state) if order == finish] + require(len(matches) == 1 and cost + matches[0] == total, "attaining terminal") + return total + + +def compile_route(width, gates, certificate): + """Emit unit moves, XOR reads and local conditional writes.""" + check_certificate(width, gates, certificate) + heads = [0, 0, 0] + slots = [None, None] + route = [] + + def go(wire): + bank, offset = location(width, wire) + while heads[bank] != offset: + direction = 1 if heads[bank] < offset else -1 + route.append(("move", bank, direction)) + heads[bank] += direction + return bank + + def action(load, wire): + slot = slots.index(None) if load else slots.index(wire) + route.append(("xor", slot, go(wire))) + slots[slot] = wire if load else None + + for gate, actions in zip(gates, certificate["actions"]): + for load, wire in actions: + action(load, wire) + require(gate[-1] not in slots, "no cached target at write") + mask = sum(1 << slots.index(wire) for wire in gate[:-1]) + route.append(("flipmask", go(gate[-1]), mask)) + for wire in certificate["finish"]: + action(0, wire) + require(slots == [None, None], "empty exit cache") + for bank in range(3): + while heads[bank]: + route.append(("move", bank, -1)) + heads[bank] -= 1 + require(sum(counts(route).values()) == certificate["total"], "literal route bill") + return route + + +def counts(route): + result = dict(moves=0, reads=0, writes=0) + for op, first, second in route: + if op == "move": + require(first in (0, 1, 2) and second in (-1, 1), "move domain") + result["moves"] += 1 + elif op == "xor": + require(first in (0, 1) and second in (0, 1, 2), "read domain") + result["reads"] += 1 + elif op == "flipmask": + require(first in (0, 1, 2) and second in (1, 2, 3), "write domain") + result["reads"] += 1 + result["writes"] += 1 + else: + raise ValueError("unknown instruction") + return result + + +def run(route, tapes): + """Use only the predecessor's metered Tape methods for payload access.""" + require(len(tapes) == 3 and len({id(t) for t in tapes}) == 3, "distinct tapes") + require(all(t.head == 0 for t in tapes), "origin entrance") + scratch = [0, 0] + before = {name: sum(t.counts[name] for t in tapes) for name in ("moves", "reads", "writes")} + counts(route) + for op, first, second in route: + if op == "move": + tapes[first].move(second) + elif op == "xor": + scratch[first] ^= tapes[second].read() + else: + condition = all(scratch[j] for j in range(2) if second & (1 << j)) + tapes[first].write(tapes[first].read() ^ int(condition)) + require(scratch == [0, 0], "scratch return") + require(all(t.head == 0 for t in tapes), "head return") + observed = {name: sum(t.counts[name] for t in tapes) - value for name, value in before.items()} + require(observed == counts(route), "metered bill") + return observed diff --git a/research/resident-scale-ribbon/ribbon.py b/research/resident-scale-ribbon/ribbon.py new file mode 100644 index 0000000000..2cf0ac07bd --- /dev/null +++ b/research/resident-scale-ribbon/ribbon.py @@ -0,0 +1,162 @@ +"""A resident, single-ribbon reversible signed doubling circuit. + +The instruction grammar follows Ali Romman's PR6513/6530 tape interface. +The adjacent-swap schedule and resident SCALE compiler are new here. +""" + +MAX_WIDTH = 64 +MAX_DIMENSION = 64 + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def doubling_gates(width, dimension): + """Rotate each signed record left, then clear its duplicated sign bit.""" + require(type(width) is int and 2 <= width <= MAX_WIDTH, "width domain") + require(type(dimension) is int and 1 <= dimension <= MAX_DIMENSION, + "dimension domain") + gates = [] + for record in range(2 * dimension): + base = record * width + for bit in range(width - 2, -1, -1): + a, b = base + bit, base + bit + 1 + gates.extend(((a, b), (b, a), (a, b))) + gates.append((base + width - 1, base)) + assert len(gates) == 2 * dimension * (3 * width - 2) + return tuple(gates) + + +def compile_route(width, dimension, inverse=False): + """Emit unit moves and CNOTs using one restored finite-control bit.""" + gates = doubling_gates(width, dimension) + if inverse: + gates = tuple(reversed(gates)) + head, route = 0, [] + for control, target in gates: + for address, operation in ((control, "xor"), (target, "flipmask"), + (control, "xor")): + delta = address - head + route.extend(("move", 0, 1 if delta > 0 else -1) + for _ in range(abs(delta))) + head = address + route.append((operation, 0, 0 if operation == "xor" else 1)) + route.extend(("move", 0, -1) for _ in range(head)) + require(len(route) <= 220000, "compiled route capacity") + return tuple(route) + + +class Tape: + """Fixed-capacity binary tape; every payload access is metered.""" + + def __init__(self, bits, head=0): + require(1 <= len(bits) <= 131072 and all(b in (0, 1) for b in bits), + "binary tape capacity") + require(type(head) is int and 0 <= head < len(bits), "initial head") + self.bits = list(bits) + self.head = head + self.reads = self.writes = self.moves = 0 + + def read(self): + self.reads += 1 + return self.bits[self.head] + + def write(self, bit): + require(bit in (0, 1), "binary write") + self.writes += 1 + self.bits[self.head] = bit + + def move(self, direction): + require(direction in (-1, 1), "unit move") + require(0 <= self.head + direction < len(self.bits), "tape boundary") + self.head += direction + self.moves += 1 + + def traffic(self): + return self.reads, self.writes, self.moves + + +def seek(tape, address): + require(type(address) is int and 0 <= address < len(tape.bits), "seek domain") + delta = address - tape.head + for _ in range(abs(delta)): + tape.move(1 if delta > 0 else -1) + + +def execute(route, tapes): + """Two finite-control bits; neither the instruction pointer nor heads read data.""" + require(1 <= len(tapes) <= 3 and len({id(t) for t in tapes}) == len(tapes), + "distinct physical tapes") + require(len(route) <= 220000, "route capacity") + scratch = [0, 0] + for op, first, second in route: + if op == "move": + tapes[first].move(second) + elif op == "xor": + require(first in (0, 1), "control index") + scratch[first] ^= tapes[second].read() + elif op == "flipmask": + require(0 <= second <= 3, "control mask") + flag = all(scratch[j] for j in (0, 1) if second & (1 << j)) + tapes[first].write(tapes[first].read() ^ int(flag)) + else: + raise ValueError("instruction domain") + require(scratch == [0, 0], "control restoration") + + +def transfer(source, destination, length): + """PR6527/6530 clean transfer, including its restored control bit.""" + require(source is not destination and type(length) is int and 1 <= length <= 8192, + "transfer domain") + for bit in range(length): + control = source.read() + destination.write(destination.read() ^ control) + source.write(source.read() ^ control) + control ^= destination.read() + require(control == 0, "clean transfer destination") + if bit + 1 < length: + source.move(1) + destination.move(1) + + +def staged_scale(owner, ribbons, carry, target, width, dimension, route): + """Unchanged PR6527 SCALE staging, used only as the comparison path.""" + start = target * 2 * dimension * width + for returning in (False, True): + seek(owner, start) + for record in range(dimension): + for component in (0, 1): + seek(owner, start + (2 * record + component) * width) + seek(ribbons[component], record * width) + pair = (ribbons[component], owner) if returning else (owner, ribbons[component]) + transfer(*pair, width) + for ribbon in ribbons: + seek(ribbon, 0) + if not returning: + for record in range(dimension): + for ribbon in ribbons: + seek(ribbon, record * width) + execute(route, [*ribbons, carry]) + for ribbon in ribbons: + seek(ribbon, 0) + + +def normalized_baseline(owner, ribbons, carry, fields, target, width, + dimension, route, evict_order, acquire_order): + """Flush, source SCALE, reacquire the same banks, restore the owner head.""" + require(len(fields) == 2 and len(set(fields)) == 2 and target in fields, + "resident field contract") + entry_head = owner.head + length = 2 * dimension * width + for bank in evict_order: + seek(owner, fields[bank] * length) + transfer(ribbons[bank], owner, length) + seek(ribbons[bank], 0) + staged_scale(owner, ribbons, carry, target, width, dimension, route) + for bank in acquire_order: + seek(owner, fields[bank] * length) + transfer(owner, ribbons[bank], length) + seek(ribbons[bank], 0) + seek(owner, entry_head) diff --git a/research/resident-scale-ribbon/verify.py b/research/resident-scale-ribbon/verify.py new file mode 100644 index 0000000000..8943ced38e --- /dev/null +++ b/research/resident-scale-ribbon/verify.py @@ -0,0 +1,239 @@ +#!/usr/bin/env python3 +"""Finite exact corroboration for the resident SCALE circuit and traffic proof.""" + +import argparse +import gzip +import hashlib +import importlib.util +import itertools +import json +from pathlib import Path + +from ribbon import (Tape, compile_route, doubling_gates, execute, + normalized_baseline, require) + +HERE = Path(__file__).resolve().parent +PACKAGE_FILES = ("README.md", "PROOF.md", "ENGINEERING.md", "NOTICE", "TASK.json", + "VERIFY.json", "SOURCES.json", "ORIGINS.json", "ribbon.py", "verify.py", + "inputs/cache.py", "inputs/CIRCUITS64.json.gz", + "inputs/CERTIFICATES.json.gz", "inputs/PR6530-PROOF.md", + "inputs/PR6530-NOTICE") + + +def sources(): + manifest = json.loads((HERE / "SOURCES.json").read_text()) + for row in manifest["files"]: + if row["usage"] == "input": + raw = (HERE.parent.parent / row["path"]).read_bytes() + require(hashlib.sha256(raw).hexdigest() == row["sha256"], "selected word pin") + word = json.loads(gzip.decompress(raw))["program"] + require(word[10481:10484] == [["ADD", 256, 257, "-1/2", 306], + ["SCALE", 257, "2", 306], + ["ADD", 257, 256, "3/2", 306]], + "selected resident window") + origins = json.loads((HERE / "ORIGINS.json").read_text()) + require(len(origins["files"]) == 5, "source inventory") + for row in origins["files"]: + raw = (HERE / "inputs" / row["path"]).read_bytes() + require(hashlib.sha256(raw).hexdigest() == row["sha256"], "source hash") + blob = b"blob " + str(len(raw)).encode() + b"\0" + raw + require(hashlib.sha1(blob).hexdigest() == row["git_blob"], "source blob") + gates = json.loads(gzip.decompress((HERE / "inputs/CIRCUITS64.json.gz").read_bytes())) + certs = json.loads(gzip.decompress((HERE / "inputs/CERTIFICATES.json.gz").read_bytes())) + selected = [i for i, row in enumerate(gates) if row[:2] == ["SCALE", "2"]] + require(len(selected) == 1, "unique source circuit") + index = selected[0] + spec = importlib.util.spec_from_file_location("retained_cache", HERE / "inputs/cache.py") + cache = importlib.util.module_from_spec(spec) + spec.loader.exec_module(cache) + route = cache.compile_route(64, gates[index][2], certs[index]) + require(certs[index]["total"] == 9840, "source local tariff") + return tuple(route), gates[index][2] + + +def bits(value, width): + return [(value >> bit) & 1 for bit in range(width)] + + +def signed(records, width): + result = [] + for offset in range(0, len(records), width): + value = sum(records[offset + bit] << bit for bit in range(width)) + result.append(value - (1 << width) if value >> (width - 1) else value) + return result + + +def gate_oracle(gates, payload): + answer = payload.copy() + for gate in gates: + answer[gate[-1]] ^= int(all(answer[wire] for wire in gate[:-1])) + return answer + + +def basis_checks(source_route, gates): + candidate = compile_route(64, 1) + for column in range(129): + payload = [int(column == bit) for bit in range(129)] + old = [Tape(payload[:64]), Tape(payload[64:128]), Tape(payload[128:])] + execute(source_route, old) + new = Tape(payload[:128]) + execute(candidate, [new]) + require(new.bits + payload[128:] == gate_oracle(gates, payload), "new basis map") + require([b for tape in old for b in tape.bits] == new.bits + payload[128:], + "retained source map") + require(all(t.head == 0 for t in old) and new.head == 0, "basis heads") + return 129 + + +def arithmetic_checks(): + count = 0 + for width in range(2, 7): + bound = 1 << (width - 2) + route = compile_route(width, 1) + inverse = compile_route(width, 1, inverse=True) + for real, imag in itertools.product(range(-bound, bound), repeat=2): + payload = bits(real, width) + bits(imag, width) + tape = Tape(payload) + execute(route, [tape]) + require(signed(tape.bits, width) == [2 * real, 2 * imag], "signed doubling") + execute(inverse, [tape]) + require(tape.bits == payload and tape.head == 0, "signed inverse") + count += 1 + return count + + +def general_checks(): + count = 0 + for width in range(2, 65): + for dimension in (1, 2, 3, 4): + payload = [int((bit * 7 + bit // 3) % 11 < 5) + for bit in range(2 * dimension * width)] + tape = Tape(payload) + execute(compile_route(width, dimension), [tape]) + require(tape.traffic() == (dimension * (18 * width - 12), + dimension * (6 * width - 4), + 28 * dimension * (width - 1) - 2), + "exact general traffic") + execute(compile_route(width, dimension, inverse=True), [tape]) + require(tape.bits == payload and tape.head == 0, "arbitrary-bit inverse") + count += 1 + return count + + +def baseline_formula(evictions, acquisitions): + """Each affine pair represents A*D+B, with width fixed at 64.""" + fields, head, a, b = (256, 257), 256, 0, 0 + for bank in evictions: + delta = fields[bank] - head - 1 + a += 128 * abs(delta) + 1152 + b += (1 if delta >= 0 else -1) - 3 + head = fields[bank] + delta = 257 - head - 1 + a += 128 * abs(delta) + 2688 + 9840 + b += (1 if delta >= 0 else -1) - 267 + head = 257 + for bank in acquisitions: + delta = fields[bank] - head - 1 + a += 128 * abs(delta) + 1152 + b += (1 if delta >= 0 else -1) - 3 + head = fields[bank] + a += 128 * abs(head - 256) + return a, b + + +def fixture(dimension, variant): + length = 128 * dimension + values = [(13 * j - 17 + variant, 29 * j + 11 - variant) + for j in range(dimension)] + target = [b for pair in values for v in pair for b in bits(v, 64)] + other = [int((j * 7 + variant) % 13 < 6) for j in range(length)] + owner_bits = [int((j * 3 + variant) % 17 < 8) for j in range(258 * length)] + owner_bits[256 * length:258 * length] = [0] * (2 * length) + return owner_bits, other, target, values + + +def physical_checks(source_route): + rows = [] + for evictions, acquisitions in itertools.product(((0, 1), (1, 0)), repeat=2): + a, b = baseline_formula(evictions, acquisitions) + for dimension, variant in itertools.product((1, 2, 3), (0, 1)): + owner_bits, other, target, values = fixture(dimension, variant) + head = 257 * 128 * dimension - 1 + owner = Tape(owner_bits, head) + ribbons, carry = [Tape(other), Tape(target)], Tape([0]) + normalized_baseline(owner, ribbons, carry, (256, 257), 257, 64, + dimension, source_route, evictions, acquisitions) + total = sum(sum(t.traffic()) for t in [owner, *ribbons, carry]) + require(total == a * dimension + b, "complete baseline affine bill") + expected = [2 * v for pair in values for v in pair] + require(signed(ribbons[1].bits, 64) == expected, "complete baseline output") + require(owner.bits == owner_bits and ribbons[0].bits == other and + carry.bits == [0] and owner.head == head and + all(t.head == 0 for t in [*ribbons, carry]), "complete baseline state") + new_owner, new_other = Tape(owner_bits, head), Tape(other) + candidate = Tape(target) + execute(compile_route(64, dimension), [candidate]) + require(candidate.bits == ribbons[1].bits and candidate.head == 0, + "normalized endpoint equality") + require(new_owner.bits == owner_bits and new_other.bits == other and + new_owner.traffic() == new_other.traffic() == (0, 0, 0), + "spectator preservation") + rows.append({"dimension": dimension, "variant": variant, + "evictions": evictions, "acquisitions": acquisitions, + "baseline": total, "candidate": sum(candidate.traffic())}) + return rows + + +def controls(): + trials = [lambda: compile_route(1, 1), lambda: compile_route(65, 1), + lambda: compile_route(64, 0), lambda: compile_route(64, 65), + lambda: execute((("bad", 0, 0),), [Tape([0])]), + lambda: execute((("xor", 0, 0),), [Tape([1])]), + lambda: execute((("move", 0, -1),), [Tape([0])])] + for trial in trials: + try: + trial() + except ValueError: + continue + raise ValueError("negative control accepted") + # The negative boundary distinguishes the final sign-clearing CNOT. + width, payload = 4, bits(-4, 4) + bits(0, 4) + tape = Tape(payload) + route = compile_route(width, 1) + execute(route, [tape]) + require(signed(tape.bits, width) == [-8, 0], "signed boundary positive control") + gates = doubling_gates(width, 1) + omitted = gates[:9] + gates[10:] + require(gate_oracle(omitted, payload) != tape.bits, "omitted sign clear") + reversed_rotation = [(a, b) for a, b in reversed(gates[:9])] + list(gates[9:]) + require(gate_oracle(reversed_rotation, payload) != tape.bits, + "reversed rotation discriminator") + require(gate_oracle(((0, 1), (1, 0), (0, 1)), [0, 1]) == [1, 0], + "swap orientation control") + return len(trials) + 3 + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument("--receipt", type=Path) + args = parser.parse_args() + source_route, gates = sources() + result = {"claim_type": "scoped circuit construction and written traffic proof", + "basis_columns": basis_checks(source_route, gates), + "signed_pairs": arithmetic_checks(), + "width_dimension_roundtrips": general_checks(), + "physical_comparisons": physical_checks(source_route), + "controls": controls(), "new_all_D_cost": [3284, -2], + "baseline_all_D_paths": [baseline_formula(a, b) + for a, b in itertools.product(((0, 1), (1, 0)), repeat=2)]} + result["package_sha256"] = { + name: hashlib.sha256((HERE / name).read_bytes()).hexdigest() + for name in PACKAGE_FILES} + if args.receipt: + args.receipt.write_text(json.dumps(result, indent=2) + "\n") + print(json.dumps(result, sort_keys=True)) + print("PASS_RESIDENT_SCALE_RIBBON") + + +if __name__ == "__main__": + main()