From 66ee36401536625714c9937e36bbe7ef115da05f Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Sat, 17 Oct 2026 11:34:53 +0100 Subject: [PATCH] feat(research): implement scalar layer with one clean carry --- research/rank7-one-carry-scalars/CHECKS.json | 61 +++ .../rank7-one-carry-scalars/ENGINEERING.md | 62 +++ research/rank7-one-carry-scalars/OVERLAP.json | 51 +++ research/rank7-one-carry-scalars/PROOF.md | 128 ++++++ research/rank7-one-carry-scalars/README.md | 93 +++++ research/rank7-one-carry-scalars/RESULT.json | 376 ++++++++++++++++++ research/rank7-one-carry-scalars/SOURCES.json | 198 +++++++++ research/rank7-one-carry-scalars/TASK.json | 93 +++++ research/rank7-one-carry-scalars/VERIFY.json | 63 +++ research/rank7-one-carry-scalars/bindings.py | 36 ++ research/rank7-one-carry-scalars/checks.py | 94 +++++ .../rank7-one-carry-scalars/decisions.tsv | 6 + research/rank7-one-carry-scalars/scalars.py | 181 +++++++++ .../rank7-one-carry-scalars/test_scalars.py | 141 +++++++ research/rank7-one-carry-scalars/verify.py | 122 ++++++ 15 files changed, 1705 insertions(+) create mode 100644 research/rank7-one-carry-scalars/CHECKS.json create mode 100644 research/rank7-one-carry-scalars/ENGINEERING.md create mode 100644 research/rank7-one-carry-scalars/OVERLAP.json create mode 100644 research/rank7-one-carry-scalars/PROOF.md create mode 100644 research/rank7-one-carry-scalars/README.md create mode 100644 research/rank7-one-carry-scalars/RESULT.json create mode 100644 research/rank7-one-carry-scalars/SOURCES.json create mode 100644 research/rank7-one-carry-scalars/TASK.json create mode 100644 research/rank7-one-carry-scalars/VERIFY.json create mode 100644 research/rank7-one-carry-scalars/bindings.py create mode 100644 research/rank7-one-carry-scalars/checks.py create mode 100644 research/rank7-one-carry-scalars/decisions.tsv create mode 100644 research/rank7-one-carry-scalars/scalars.py create mode 100644 research/rank7-one-carry-scalars/test_scalars.py create mode 100644 research/rank7-one-carry-scalars/verify.py diff --git a/research/rank7-one-carry-scalars/CHECKS.json b/research/rank7-one-carry-scalars/CHECKS.json new file mode 100644 index 0000000000..2ccd4f1e13 --- /dev/null +++ b/research/rank7-one-carry-scalars/CHECKS.json @@ -0,0 +1,61 @@ +{ + "status": "PASS_AUTHOR_CHECKED_LOCAL_COMPOSITION", + "environment": { + "python": "3.12.15", + "platform": "macOS 27.0.1 arm64", + "ruff": "0.17.1" + }, + "source_python_sha256": { + "bindings.py": "cca060f9b8bb33c92c19c8ea391dc5862293b008afaa445f49cfc83284532705", + "checks.py": "6190ac5c32e8eae3ff07dc1ad2a63e0997307fcaf12b59c9bd7ea997d28717fe", + "scalars.py": "9b49ce697507551c1eece96b8c327c5479fe61cbc9464827ad2b54149e4e840c", + "test_scalars.py": "10f6b44200f13f70bbe36b731bd53bd65bc87fdc58c6adcdfbd6daf7693b41b4", + "verify.py": "701dd0d3da88300074b02d37552f67b36359edcd255c675184c56cd8cad923dc" + }, + "commands": [ + { + "command": "TMPDIR=\"$RUN/tmp\" uv run --python 3.12 --no-project python -B scripts/research_package.py --package research/rank7-one-carry-scalars", + "result": "PASS_REGISTERED_RESEARCH_PACKAGE; both final stable-code commands passed" + }, + { + "command": "uv tool run ruff check --no-cache --select E9,F,B research/rank7-one-carry-scalars", + "result": "All checks passed" + }, + { + "command": "uv tool run ruff format --no-cache --check research/rank7-one-carry-scalars", + "result": "All files formatted" + }, + { + "command": "Python 3.12 compile() on every new .py with -W error; AST function length check", + "result": "5 sources compile; every function <=60 lines" + }, + { + "command": "python -O -W error -B research/rank7-one-carry-scalars/test_scalars.py", + "result": "12 behavioral groups pass" + }, + { + "command": "Direct verify.py --work \"$RUN/export-replay\" from a plain export of this package plus exactly its 30 declared inputs, with no .git; cmp export-result.json RESULT.json", + "result": "PASS; byte-identical deterministic receipt" + }, + { + "command": "Recompute all 32 SOURCE SHA256/Git blobs, declared-input set, recorded Python digests and four literal invoices", + "result": "PASS_32_SOURCE_PINS_INVOICE_AND_TESTED_CODE_DIGESTS" + } + ], + "review": { + "kind": "internal read-only review, not independent human review", + "resolved": [ + "Forward-only templates included via all-stream alphabet union", + "Signed powers cannot require stronger hidden divisibility", + "SCALE recipe must match the canonical guarded coefficient word", + "Width checked before input bit allocation" + ], + "remaining_findings": [] + }, + "limits": [ + "No full supplier, routing or native dirty-bank ownership proof", + "No independent implementation of retained native/capacity engine", + "No compiler/kernel formal proof", + "Hosted CI not claimed; inspect the PR checks" + ] +} diff --git a/research/rank7-one-carry-scalars/ENGINEERING.md b/research/rank7-one-carry-scalars/ENGINEERING.md new file mode 100644 index 0000000000..e11272c280 --- /dev/null +++ b/research/rank7-one-carry-scalars/ENGINEERING.md @@ -0,0 +1,62 @@ +# Engineering scope and checks + +Build the Lever shaped the deliverable: the literal generator, cold replay and +complete invoice are rerunnable artifacts. Prove It Works required execution of +the emitted Boolean gates, restored source/carry checks and fresh native bindings. +Power of Ten shaped the finite width, coefficient, gate and truth-column limits. +The autonomous-run exit predicate is one complete source-bound scalar composition +with a strict local logical-gate reduction and one clean carry, with the changed +exclusive-borrow premise explicit. No full supplier or kappa predicate is claimed. + +## Code inspection + +- Structured loops, exceptions and context-managed temporary directories; no + recursive call cycle. Native source is frozen and its engine remains inherited. +- Width 4..256 in the primitive, 23..256 for the full-layer tariff; shifts −12..8, + at most nine coefficient terms, at most 32 recipe units, at most 20,000 gates. + Right-shift k=2, the literal count is `2n−2` Toffolis and `4n−2` +CNOTs; n=1 uses one CNOT. There are n−1 MAJ and n−1 UMA blocks plus two top +CNOTs. Each block has one Toffoli and two CNOTs. The implementation retains +the standard literal gates rather than claiming a gate minimum. + +For exponent e>=0, add source bits `[0,W−e)` to target bits `[e,W)`. +Those wires represent `2^e S mod 2^W`; omitted low target bits stay fixed. +If e>=W the increment is zero. If W−e=1 use the one-CNOT case. +For a right shift k=−e, require k (T+S,S) -> (T+S,-T) -> (S,-T) -> (-T,S) modulo 2^W +``` + +Every adder returns its own carry. S needs no clean bits or numerical bound +beyond being a W-bit word, and is restored after the swap. The exact cost is +`6W−6` Toffolis and `15W−6` CNOTs. This costs more gates than PR3094's +carry-bank negation but permits the whole scalar layer to reuse a single +clean bit. Signed SCALE interpretation follows from the unchanged endpoint +and prefix guards, not from interpreting the temporary shears as signed values. + +## Complete source-bound invoice + +Cold replay authenticates the complete 30-file predecessor dependency set, +rebuilds both native programs, replays the complete native/capacity checks, +and rebinds all 9,992 scalar macros per orientation. The actual histogram +has 9,438 ADD and 554 SCALE macros. For both real components, the signed-power +ADD counts by exponent are: + +| Exponent | −3 | −2 | −1 | 0 | 1 | +|---|---:|---:|---:|---:|---:| +| Calls | 210 | 5,432 | 7,040 | 5,862 | 478 | + +SCALE additionally uses 924 negations, 222 HALF and 300 DOUBLE operations. +These counts are identical for the two providers and both orientations. +The dispatch hashes bind the chronology; no macro, frame, child or cleanup +operation is removed from the source stream. + +Summing the literal formulas gives, per provider/orientation and both real +components, for every supported W: + +| Implementation | CNOTs | Toffolis | +|---|---:|---:| +| PR3094 direct caller | `82274W−104534` | `77936W−119740` | +| One-carry caller | `91514W−9476` | `43588W−44544` | +| Old minus new | `−9240W−95058` | `34348W−75196` | + +The combined unweighted logical-gate saving is `25108W−170254`, strictly +positive throughout 23<=W<=256 (at W=23 it is 407,230). +At W=84, CNOTs increase by 871,218, Toffolis fall by 2,810,036, and the +combined saving is 1,938,818. Clean carry stock falls from 83 bits to one; +the two operand banks total 168 bits in both template layouts. The changed +SCALE borrowing obligation must still be implemented on actual native owners. +A weighted tariff or physical time need not track this unweighted sum. + +## Evidence and limits + +`RESULT.json` records fresh native dispatch bindings, circuit hashes and all +four invoices. The verifier exhausts all aligned signed sources and every +modular target for ADDs at W=4..7. For SCALE it exhausts every arbitrary +auxiliary bank and each target satisfying the inherited guards. Complete +output states and reversed gate lists are checked on 314,560 truth columns +across 124 circuits. A separate Boolean-list evaluator checks 1,550 larger-width +fixtures through W=256. The written argument supplies the width-uniform proof. +Meaningful malformed/sign/cleanup controls run separately under optimized Python. +The reused native engine is executed, not independently reimplemented. + +No recursive paid profile, moment, kappa, selected frontier, full native caller, +multitape routing bound or unconditional multiplication theorem is changed. diff --git a/research/rank7-one-carry-scalars/README.md b/research/rank7-one-carry-scalars/README.md new file mode 100644 index 0000000000..0a15051fa9 --- /dev/null +++ b/research/rank7-one-carry-scalars/README.md @@ -0,0 +1,93 @@ +# Complete scalar layer with one clean carry + +The complete PR3094 prelude/A scalar layer admits a one-clean-carry +implementation when each macro can exclusively borrow and restore a second +operand bank. At 64-bit input precision (`W=84`), all 9,992 macros per +provider/orientation use **82 fewer clean carry bits** and **1,938,818 fewer +unweighted logical Boolean gates**. Both providers and orientations give: + +| Both real components | CNOTs | Toffolis | Clean carry bits | +|---|---:|---:|---:| +| PR3094 direct caller | 6,806,482 | 6,426,884 | 83 | +| One-carry caller | 7,677,700 | 3,616,848 | 1 | + +CNOTs increase by 871,218; Toffolis decrease by 2,810,036. These are logical +circuit counts, not a runtime or kappa improvement. At every supported width +`23 <= W <= 256`, the combined saving is exactly `25108W−170254` gates. +The two W-bit operand banks are additional to the carry. For ADD, the source +is temporarily writable and restored; for SCALE, a disjoint arbitrary dirty +bank must be supplied and is restored. No native ownership assignment for +that SCALE bank is provided. This changes PR3094's gate-level read-only +source contract. + +The construction extends PR3081's credited MAJ/UMA wired half-ADD to every +signed-power ADD in the actual stream. Negation uses three modular shears +and a swap, avoiding a full clean carry bank even for negative SCALEs. +Other SCALE shifts retain their literal inherited circuits and guards. +The source bytes, frames, recursive children and cleanup contract stay frozen. + +[PROOF.md](PROOF.md) derives the identities, restoration and exact uniform +invoice. [RESULT.json](RESULT.json) records fresh native/capacity bindings, +all four dispatch hashes and circuit hashes. Cold replay passes 124 exhaustive +small circuits with 314,560 complete truth columns, their literal inverses, +and 1,550 fixtures evaluated with a separate Boolean-list interpreter. +Twelve behavioral groups cover sign/cleanup mutants, dirty carry, alignment, +overflow, source corruption and malformed ownership/width boundaries. +The inherited native engine is executed, not independently reimplemented. + +## Reproduce + +Python 3.12, standard library only. From the repository root, choose a fresh +external directory and run: + +```sh +RUN="$HOME/.cache/integer-mult-bounds-runs/one-carry-$(date -u +%Y%m%dT%H%M%SZ)" +mkdir -p "$RUN/tmp" +TMPDIR="$RUN/tmp" PYTHONPYCACHEPREFIX="$RUN/bytecode" \ + uv run --python 3.12 --no-project python -W error -B \ + research/rank7-one-carry-scalars/verify.py --work "$RUN/replay" \ + > "$RUN/result.json" +cmp "$RUN/result.json" research/rank7-one-carry-scalars/RESULT.json +TMPDIR="$RUN/tmp" PYTHONPYCACHEPREFIX="$RUN/test-bytecode" \ + uv run --python 3.12 --no-project python -O -W error -B \ + research/rank7-one-carry-scalars/test_scalars.py +TMPDIR="$RUN/tmp" uv run --python 3.12 --no-project python -B \ + scripts/research_package.py --package research/rank7-one-carry-scalars +``` + +Without `--work`, replay removes its temporary outputs beneath TMPDIR. +[SOURCES.json](SOURCES.json) authenticates all 30 live predecessor inputs +before import; [VERIFY.json](VERIFY.json) declares them for CI invalidation. +No predecessor is copied or edited. Direct replay needs the declared source +files but no Git/network; the generic provenance check needs Git history. +[ENGINEERING.md](ENGINEERING.md) records bounds and verification limits. + +## Open next questions + +Can one literal native SCALE event borrow an actual dirty W-bit bank with +exclusive access and return it before the next cut? Name the owner, lifetime, +entry format and complete movement cost before lowering that event. No physical +bank assignment or access tariff is established by the circuit template. + +Can the complete producer and consumer retain the one-carry saving? Price +residual adapters, frame/warp/climb operations, recursive children, stock, +routing and eventual cleanup on the same layout. [TASK.json](TASK.json) +records the obligation ledger and decision to stop at this scalar composition. +The recursive rank profile, moment, selected kappa and full supplier admission +remain unchanged; this is not a complete multiplication theorem. + +## Credit + +Nick Petalas contributed the complete scalar composition, dirty-bank negation, +source-bound invoice and proof. Cuccaro, Draper, Kutin and Moulton supply the +MAJ/UMA adder; PR3081 already realizes the local wired dyadic ADD, and PR3088 +shares its sign-fill across four physical ADDs. PR3094 supplies the complete +scalar guard/binding baseline and retained PR3090/3080 sources. No novelty +is claimed for those primitives, signed powers or elementary modular shears. + +The retained lineage includes PR3078/3076/3060/3056, dcharb78/PR3042, +Jeremy Kothe/PR3015, Marius-Paul Dumitrean/PR2979, Cinna Davis/PR2226, +DLamdata, eumemic, icekylinx, Tekalign and the credited native, geometry and +owner contributors. Original source notices remain at their pinned paths. +New work is Apache-2.0. Development and internal read-only review used substantial +automated assistance; no independent human or proof-kernel review is claimed. diff --git a/research/rank7-one-carry-scalars/RESULT.json b/research/rank7-one-carry-scalars/RESULT.json new file mode 100644 index 0000000000..dac24bf16c --- /dev/null +++ b/research/rank7-one-carry-scalars/RESULT.json @@ -0,0 +1,376 @@ +{ + "bit_checks": { + "array_fixtures": 1550, + "exhaustive_circuits": 124, + "truth_columns": 314560 + }, + "boundary": "Both operand banks exclusively writable during each macro; source and carry restored.", + "clean_carry_bits": 1, + "coefficient_scratch_bits": 0, + "data_width": 84, + "operand_bits": 168, + "prior_clean_carry_bits": 83, + "status": "PASS_ONE_CARRY_SCALARS_NO_NEW_KAPPA", + "streams": { + "base/backward": { + "dispatch_sha256": "6245ca3e273eb8bdfa8ab52215f78ddd225187c21651c0a80238f399e08d78c6", + "histogram": { + "add:-1:1": 1757, + "add:-1:2": 1672, + "add:-1:4": 1411, + "add:-1:8": 33, + "add:-2:1": 114, + "add:-3:2": 9, + "add:-3:4": 15, + "add:-3:8": 12, + "add:-5:8": 9, + "add:-7:8": 1, + "add:1:1": 1151, + "add:1:2": 1799, + "add:1:4": 1282, + "add:1:8": 36, + "add:2:1": 110, + "add:3:2": 5, + "add:3:4": 7, + "add:3:8": 11, + "add:5:8": 3, + "add:7:4": 1, + "scale:-1:1": 7, + "scale:-1:2": 2, + "scale:-2:1": 2, + "scale:1:-1": 274, + "scale:1:-2": 84, + "scale:1:1": 12, + "scale:1:2": 64, + "scale:2:-1": 93, + "scale:2:1": 16 + }, + "invoices": { + "148": { + "both_components": { + "ccx": 6406480, + "cx": 13534596 + }, + "templates_sha256": "684398127ffc58d327bef489e3a8b91b5c71716c725a54956b0a945a80670bb7" + }, + "23": { + "both_components": { + "ccx": 957980, + "cx": 2095346 + }, + "templates_sha256": "0f8804c3296289e816d594b0fd0c7b1fe7bb569c2924675b9115e1ba0f3a23c1" + }, + "24": { + "both_components": { + "ccx": 1001568, + "cx": 2186860 + }, + "templates_sha256": "5b028fcda41f200a4a95434e075390c7055d6b111ee01a3255d070e0047d1482" + }, + "256": { + "both_components": { + "ccx": 11113984, + "cx": 23418108 + }, + "templates_sha256": "cf1a73e34ae0636a4862d9af0b43acd676fa48e7b120cff87f732081a32dbe49" + }, + "64": { + "both_components": { + "ccx": 2745088, + "cx": 5847420 + }, + "templates_sha256": "607c35f8bc99f976d2b1c6061d2e96d8f30bec24861ef2cc6a3151faa32e5e91" + }, + "84": { + "both_components": { + "ccx": 3616848, + "cx": 7677700 + }, + "templates_sha256": "b545f45e68d9ba60cd226eb57a98e569d20ca475312ea8422b87a1dcbf3f7c71" + }, + "85": { + "both_components": { + "ccx": 3660436, + "cx": 7769214 + }, + "templates_sha256": "7be758979339f322a6c7529287a82c529039c7861e28c62374c37dcf3e431e8b" + } + }, + "macros": 9992, + "saving_at_84_bits": { + "ccx": 2810036, + "cx": -871218 + } + }, + "base/forward": { + "dispatch_sha256": "06cc0dd10a036a118f9c4b34ed1d94cf885658e876bfa8962be87ad5752d1266", + "histogram": { + "add:-1:1": 1151, + "add:-1:2": 1799, + "add:-1:4": 1282, + "add:-1:8": 36, + "add:-2:1": 110, + "add:-3:2": 5, + "add:-3:4": 7, + "add:-3:8": 11, + "add:-5:8": 3, + "add:-7:4": 1, + "add:1:1": 1757, + "add:1:2": 1672, + "add:1:4": 1411, + "add:1:8": 33, + "add:2:1": 114, + "add:3:2": 9, + "add:3:4": 15, + "add:3:8": 12, + "add:5:8": 9, + "add:7:8": 1, + "scale:-1:1": 274, + "scale:-1:2": 93, + "scale:-2:1": 84, + "scale:1:-1": 7, + "scale:1:-2": 2, + "scale:1:1": 12, + "scale:1:2": 16, + "scale:2:-1": 2, + "scale:2:1": 64 + }, + "invoices": { + "148": { + "both_components": { + "ccx": 6406480, + "cx": 13534596 + }, + "templates_sha256": "60952d9dde36fd264c6c43820c22dcf2e6b164d0b8deecc6a4a4f447c9427a3b" + }, + "23": { + "both_components": { + "ccx": 957980, + "cx": 2095346 + }, + "templates_sha256": "c8178f934f1574bb7e6cb5014412a4ddd84e708e7fc51f6657a742b07c975fcd" + }, + "24": { + "both_components": { + "ccx": 1001568, + "cx": 2186860 + }, + "templates_sha256": "c79f196171546233202ef58a4f7e9161ce5690765369e4e43bdcf60da068b0fe" + }, + "256": { + "both_components": { + "ccx": 11113984, + "cx": 23418108 + }, + "templates_sha256": "d40b9b7e723861ad763156942168e2c3d8a97e67a7f5d594e2d8278fa5b41644" + }, + "64": { + "both_components": { + "ccx": 2745088, + "cx": 5847420 + }, + "templates_sha256": "f6c43184829b7094192d66fddcbe79d172fe8a27115096a334670c3ff583aa21" + }, + "84": { + "both_components": { + "ccx": 3616848, + "cx": 7677700 + }, + "templates_sha256": "74d933bddf553eef8c9bd1f7b1d4f30b17201e3fe2c23627dfb967b6f7a1c7d1" + }, + "85": { + "both_components": { + "ccx": 3660436, + "cx": 7769214 + }, + "templates_sha256": "304f5cd62e46954939a09d5049d53eca4460b7c3282e68f44ed703aa22855c4b" + } + }, + "macros": 9992, + "saving_at_84_bits": { + "ccx": 2810036, + "cx": -871218 + } + }, + "extra/backward": { + "dispatch_sha256": "6245ca3e273eb8bdfa8ab52215f78ddd225187c21651c0a80238f399e08d78c6", + "histogram": { + "add:-1:1": 1757, + "add:-1:2": 1672, + "add:-1:4": 1411, + "add:-1:8": 33, + "add:-2:1": 114, + "add:-3:2": 9, + "add:-3:4": 15, + "add:-3:8": 12, + "add:-5:8": 9, + "add:-7:8": 1, + "add:1:1": 1151, + "add:1:2": 1799, + "add:1:4": 1282, + "add:1:8": 36, + "add:2:1": 110, + "add:3:2": 5, + "add:3:4": 7, + "add:3:8": 11, + "add:5:8": 3, + "add:7:4": 1, + "scale:-1:1": 7, + "scale:-1:2": 2, + "scale:-2:1": 2, + "scale:1:-1": 274, + "scale:1:-2": 84, + "scale:1:1": 12, + "scale:1:2": 64, + "scale:2:-1": 93, + "scale:2:1": 16 + }, + "invoices": { + "148": { + "both_components": { + "ccx": 6406480, + "cx": 13534596 + }, + "templates_sha256": "684398127ffc58d327bef489e3a8b91b5c71716c725a54956b0a945a80670bb7" + }, + "23": { + "both_components": { + "ccx": 957980, + "cx": 2095346 + }, + "templates_sha256": "0f8804c3296289e816d594b0fd0c7b1fe7bb569c2924675b9115e1ba0f3a23c1" + }, + "24": { + "both_components": { + "ccx": 1001568, + "cx": 2186860 + }, + "templates_sha256": "5b028fcda41f200a4a95434e075390c7055d6b111ee01a3255d070e0047d1482" + }, + "256": { + "both_components": { + "ccx": 11113984, + "cx": 23418108 + }, + "templates_sha256": "cf1a73e34ae0636a4862d9af0b43acd676fa48e7b120cff87f732081a32dbe49" + }, + "64": { + "both_components": { + "ccx": 2745088, + "cx": 5847420 + }, + "templates_sha256": "607c35f8bc99f976d2b1c6061d2e96d8f30bec24861ef2cc6a3151faa32e5e91" + }, + "84": { + "both_components": { + "ccx": 3616848, + "cx": 7677700 + }, + "templates_sha256": "b545f45e68d9ba60cd226eb57a98e569d20ca475312ea8422b87a1dcbf3f7c71" + }, + "85": { + "both_components": { + "ccx": 3660436, + "cx": 7769214 + }, + "templates_sha256": "7be758979339f322a6c7529287a82c529039c7861e28c62374c37dcf3e431e8b" + } + }, + "macros": 9992, + "saving_at_84_bits": { + "ccx": 2810036, + "cx": -871218 + } + }, + "extra/forward": { + "dispatch_sha256": "06cc0dd10a036a118f9c4b34ed1d94cf885658e876bfa8962be87ad5752d1266", + "histogram": { + "add:-1:1": 1151, + "add:-1:2": 1799, + "add:-1:4": 1282, + "add:-1:8": 36, + "add:-2:1": 110, + "add:-3:2": 5, + "add:-3:4": 7, + "add:-3:8": 11, + "add:-5:8": 3, + "add:-7:4": 1, + "add:1:1": 1757, + "add:1:2": 1672, + "add:1:4": 1411, + "add:1:8": 33, + "add:2:1": 114, + "add:3:2": 9, + "add:3:4": 15, + "add:3:8": 12, + "add:5:8": 9, + "add:7:8": 1, + "scale:-1:1": 274, + "scale:-1:2": 93, + "scale:-2:1": 84, + "scale:1:-1": 7, + "scale:1:-2": 2, + "scale:1:1": 12, + "scale:1:2": 16, + "scale:2:-1": 2, + "scale:2:1": 64 + }, + "invoices": { + "148": { + "both_components": { + "ccx": 6406480, + "cx": 13534596 + }, + "templates_sha256": "60952d9dde36fd264c6c43820c22dcf2e6b164d0b8deecc6a4a4f447c9427a3b" + }, + "23": { + "both_components": { + "ccx": 957980, + "cx": 2095346 + }, + "templates_sha256": "c8178f934f1574bb7e6cb5014412a4ddd84e708e7fc51f6657a742b07c975fcd" + }, + "24": { + "both_components": { + "ccx": 1001568, + "cx": 2186860 + }, + "templates_sha256": "c79f196171546233202ef58a4f7e9161ce5690765369e4e43bdcf60da068b0fe" + }, + "256": { + "both_components": { + "ccx": 11113984, + "cx": 23418108 + }, + "templates_sha256": "d40b9b7e723861ad763156942168e2c3d8a97e67a7f5d594e2d8278fa5b41644" + }, + "64": { + "both_components": { + "ccx": 2745088, + "cx": 5847420 + }, + "templates_sha256": "f6c43184829b7094192d66fddcbe79d172fe8a27115096a334670c3ff583aa21" + }, + "84": { + "both_components": { + "ccx": 3616848, + "cx": 7677700 + }, + "templates_sha256": "74d933bddf553eef8c9bd1f7b1d4f30b17201e3fe2c23627dfb967b6f7a1c7d1" + }, + "85": { + "both_components": { + "ccx": 3660436, + "cx": 7769214 + }, + "templates_sha256": "304f5cd62e46954939a09d5049d53eca4460b7c3282e68f44ed703aa22855c4b" + } + }, + "macros": 9992, + "saving_at_84_bits": { + "ccx": 2810036, + "cx": -871218 + } + } + } +} diff --git a/research/rank7-one-carry-scalars/SOURCES.json b/research/rank7-one-carry-scalars/SOURCES.json new file mode 100644 index 0000000000..9d06e50b5d --- /dev/null +++ b/research/rank7-one-carry-scalars/SOURCES.json @@ -0,0 +1,198 @@ +{ + "schema_version": 1, + "base_commit": "997e6a9ca7b4f95d50e366f61412fd640d72a88a", + "files": [ + { + "path": "research/rank7-boolean-scalar-caller/FROZEN.json", + "usage": "input", + "sha256": "370b7814ec0809d086e3cf1ebb809ef30336382dc2584344b6755a76398c23be", + "git_blob": "ccff43704aa2aedb4acebea1f40d100ae0864a00" + }, + { + "path": "research/rank7-boolean-scalar-caller/RESULT.json", + "usage": "input", + "sha256": "b2528a896b449c283d38caf1f64fc907cdbb43a7a653635dad5308551998e676", + "git_blob": "c74f88a5f884cff921a9e6f15389e1d864d79d5a" + }, + { + "path": "research/rank7-boolean-scalar-caller/bitadder.py", + "usage": "input", + "sha256": "47c96d1ec18f919f16f439b5e42df7a6d95dc6f1ba3f963422151285b511c277", + "git_blob": "ee3548bb2c6d7cf2ed330251731a0f19b3afe45c" + }, + { + "path": "research/rank7-boolean-scalar-caller/caller.py", + "usage": "input", + "sha256": "1a7779377a2f80fcabe5270db658e7dada05577e3a1bc28f92c534916bb2d52c", + "git_blob": "f64517a57ed21afbbd3c86184705f7731be25e9b" + }, + { + "path": "research/rank7-boolean-scalar-caller/replay.py", + "usage": "input", + "sha256": "08718e8dc2aaef0fa81070f3550daa42b2cdd637b96b3fcef5a43bd9df6db1ba", + "git_blob": "c49294839e727df6084714d331ccaacd32740709" + }, + { + "path": "research/rank7-boolean-scalar-caller/source/RESULT.json", + "usage": "input", + "sha256": "0b9e55f0b556cb381ba0c1750ffbe00c7bfa9040e80c823cdc7820fc03e028a5", + "git_blob": "bb43ba062e545efe0eb72a58ba5a93840de04386" + }, + { + "path": "research/rank7-boolean-scalar-caller/source/VENDOR.json", + "usage": "input", + "sha256": "ce841a6efd8243f8021486c7d47522495aa9b563785aa6e783b3281ef7f0006e", + "git_blob": "4c77565e2230b8a86772088111b7122c3235c182" + }, + { + "path": "research/rank7-boolean-scalar-caller/source/integer.py", + "usage": "input", + "sha256": "6c2c4d3858ca4ddfa71572fcb52386abff35684e092dba99245963c4286cbc21", + "git_blob": "ce3b7b1fb98aab4ab4bee07ec4c584304b45d5d3" + }, + { + "path": "research/rank7-boolean-scalar-caller/source/microstates.py", + "usage": "input", + "sha256": "09fac67bd1f375507230ee2af63c854df644eda040691f06773fca8fab4aa936", + "git_blob": "4f0450545c546fb791587d70069808b087faca17" + }, + { + "path": "research/rank7-boolean-scalar-caller/source/vendor/lowering/lower.py", + "usage": "input", + "sha256": "5c385a2c601f243d6c3f16b9f04b06a6aa41b8dfa5750e452e146730fcb7cda4", + "git_blob": "c0663f28e5da78c463e0d4769bfc364695760689" + }, + { + "path": "research/rank7-boolean-scalar-caller/source/vendor/native/RESULT.json", + "usage": "input", + "sha256": "df75bc56184d41eb07233832c38bde3cb72a9137fde1b923050a4891dbc8ade4", + "git_blob": "51687684972e028977289fa94aeb8a5be3075064" + }, + { + "path": "research/rank7-boolean-scalar-caller/source/vendor/native/format.py", + "usage": "input", + "sha256": "73d5d5273a0165bce36db00dc5c6431640b4f4b9016e32ad074ba12a33dcf9b9", + "git_blob": "d5a50b68da8ea5d3b16cf8633733d3edf5276c5e" + }, + { + "path": "research/rank7-boolean-scalar-caller/source/vendor/native/vendor/clifford.py", + "usage": "input", + "sha256": "d5e42ddabd141b7bfbd70fe13908f3c3a06aeccebeab90623596bfb1988b97fb", + "git_blob": "6f1e6a38febde7eb7a7341d317522e6650d84408" + }, + { + "path": "research/rank7-boolean-scalar-caller/source/vendor/native/vendor/parent/EDITS.json", + "usage": "input", + "sha256": "7bc3c686815fd45c267127d3d6abd6b2dddff046594f614a45baffb4ff470953", + "git_blob": "62ee496d238eccb865ab0b554083600510918091" + }, + { + "path": "research/rank7-boolean-scalar-caller/source/vendor/native/vendor/parent/VENDOR.json", + "usage": "input", + "sha256": "c7fbb6c9e203b129983b4ad4ff5ab7fbea1720c43fdd55679a169996fc568eb7", + "git_blob": "0ede22c4a1ea771c98257d02974acbc18a0bd53e" + }, + { + "path": "research/rank7-boolean-scalar-caller/source/vendor/native/vendor/parent/contract.py", + "usage": "input", + "sha256": "5f9823fe342f629312e28d8edf5bca02171ce574f1037bc980397ba6c88ba784", + "git_blob": "8b81fe8a760b23723fb6739f1e71165bd8ef7287" + }, + { + "path": "research/rank7-boolean-scalar-caller/source/vendor/native/vendor/parent/contractions.py", + "usage": "input", + "sha256": "f80d93148c4a2159f5066a4420d1681c2d13a1ad041bf022200f15857fe50e5c", + "git_blob": "d80ec18d8a0a3e8ac57541c97061e6638f7d879a" + }, + { + "path": "research/rank7-boolean-scalar-caller/source/vendor/native/vendor/parent/frames.py", + "usage": "input", + "sha256": "a4428fa0e19ab8f98bce5f75a2d6677b6296559670e1c70ddebab6b2d28d9200", + "git_blob": "48983e5558b4c321718b2d3412833445348a610e" + }, + { + "path": "research/rank7-boolean-scalar-caller/source/vendor/native/vendor/parent/replay_parent.py", + "usage": "input", + "sha256": "19e6703a7b73325b826c4c47b2140b7266e174727e797a7df9f40ef31024ea83", + "git_blob": "5514757ea31871733ccd9bdc5e88d31845c529ab" + }, + { + "path": "research/rank7-boolean-scalar-caller/source/vendor/native/vendor/parent/tariff.py", + "usage": "input", + "sha256": "618721d59891a3aad495692ebb943451f5df6700a60e57d7761009aec0644655", + "git_blob": "b1676fd2e85d65ca5bb42d97c775a06f2d0a4dbb" + }, + { + "path": "research/rank7-boolean-scalar-caller/source/vendor/native/vendor/parent/vendor/CREDITS.md", + "usage": "input", + "sha256": "8475f5e7c090e05196cfd6c2894516cbbedd5876f54193fea575d8064e23574e", + "git_blob": "85b68ae52e139e83a7ff2ef2870024d420881cb0" + }, + { + "path": "research/rank7-boolean-scalar-caller/source/vendor/native/vendor/parent/vendor/NOTICE", + "usage": "input", + "sha256": "c9731c9cca25ede32c2a1b3aef6d5b249973cb2ed5fb2494407bdca598763661", + "git_blob": "89c20926ea7f803718f751d95989d5a269908efd" + }, + { + "path": "research/rank7-boolean-scalar-caller/source/vendor/native/vendor/parent/vendor/PROFILE.json", + "usage": "input", + "sha256": "3245979197e965850eec803879f355a49738a60158cd7043fdc574e9fa810052", + "git_blob": "03cdf8fa947e2b04b7c92f5c51924be3a6a21c7b" + }, + { + "path": "research/rank7-boolean-scalar-caller/source/vendor/native/vendor/parent/vendor/WORD-base.json.gz", + "usage": "input", + "sha256": "7e98f6f2a6c9ce9e7e04b515bd8ce4a4a533ff05f01ea265be2a1a994695260e", + "git_blob": "2ee02e318c98281a71445b954feccd55c153827c" + }, + { + "path": "research/rank7-boolean-scalar-caller/source/vendor/native/vendor/parent/vendor/WORD-extra.json.gz", + "usage": "input", + "sha256": "1396410de482883416fc7f534062ab005b484056b035fdcfa3b5cc065536ba35", + "git_blob": "33ba5f34996a31edd197cb58eca575645575e529" + }, + { + "path": "research/rank7-boolean-scalar-caller/source/vendor/native/vendor/parent/vendor/native/NOTICE-PR2226.md", + "usage": "input", + "sha256": "6b6730303818f6edc2a253eb4d05471eee58f28b5815fb250c32ae376f774c8a", + "git_blob": "a14b299ef55c5581166988aa78baba329cebde04" + }, + { + "path": "research/rank7-boolean-scalar-caller/source/vendor/native/vendor/parent/vendor/native/PR2226-NOTICE.md", + "usage": "input", + "sha256": "f1d45d886926915531e3a59968abf0a4c974d7038f869848e71bd3a21b834422", + "git_blob": "5ea70357a04d083dba066fbc5c809a5736d8edd6" + }, + { + "path": "research/rank7-boolean-scalar-caller/source/vendor/native/vendor/parent/vendor/native/bw_emit.py", + "usage": "input", + "sha256": "99b59a6fa3feda86785e4225157dcb1a6169d256cec4f5e0acc9cea7a701df76", + "git_blob": "6d47f63ab7a533941b3881bbfd3ae4dac5f76932" + }, + { + "path": "research/rank7-boolean-scalar-caller/source/vendor/native/vendor/parent/vendor/native/bw_transport.py", + "usage": "input", + "sha256": "9818e08b819310b40f1441b89be8c4369584a5b3fa5dfe9b86b1df9a7f5d6a76", + "git_blob": "08248542b18864c94a5ac050c8669f68519838e1" + }, + { + "path": "research/rank7-boolean-scalar-caller/source/verify.py", + "usage": "input", + "sha256": "e4a33e3a437b6d8652503e56bfcb026f486d114fe51784de86a20b9b17ec6d4b", + "git_blob": "1abf24ad91b953a650abc15e2c40d4fe44f446e6" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] +} diff --git a/research/rank7-one-carry-scalars/TASK.json b/research/rank7-one-carry-scalars/TASK.json new file mode 100644 index 0000000000..af759c7c87 --- /dev/null +++ b/research/rank7-one-carry-scalars/TASK.json @@ -0,0 +1,93 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 6, + "base_commit": "997e6a9ca7b4f95d50e366f61412fd640d72a88a", + "original_card": { + "id": "independent-moment", + "question": "Does one changed supplier or assembly claim lack a source-bound independent check of a specific new implication?", + "starting_points": [ + "certificates/selected-result.json", + "research/rank7-joint-endframes/README.md", + "docs/research/research-family-status.md" + ], + "methods": [ + "Independently reconstruct a coordinated frame/circuit change and its single-change control, then derive the complete rank and physical ledger.", + "Implement certified moment inequalities through a different exact enclosure method." + ], + "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read #2979 joint rank-7 end-frame proposal and the revision-6 evidence status. Its claimed kappa is not selected. Compare coordinated changes with the losing single-change controls and locate the complete physical ledger; an aggregate moment alone does not validate the mechanism.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Prioritize a bounded independent audit of #2979: reconstruct one joint group and its single-lowering control, check the declared frames/chronology, then trace changed children, idle widths and cleanup buffers into the complete invoice and both supplier caps. Choose one still-missing implication after checking existing audits. Stop with exact unresolved dependencies if full admission exceeds the session; do not launch a new lowering census on an unvalidated premise or substitute extra root digits for mechanism checking.", + "bottleneck_link": "Independent pricing prevents unsupported frontier claims and can reveal genuine accounting slack.", + "allowed_variations": [ + "Reconstruct either a source ledger or a numeric enclosure with a different method." + ], + "scope_change_triggers": [ + "Importing the primary function and calling its output independent verification.", + "Promoting #2979 from merged source archive to validated supplier solely from author PASS receipts or aggregate pricing." + ], + "overlap_terms": [ + "independent moment", + "rank histogram", + "exact enclosure", + "2979", + "rank7 joint endframes", + "paired extraction", + "joint lowering" + ] + }, + "scope_status": "changed", + "scope_change_reason": "Live full-claim/root and joint-frame audits overlap the generic card. Follow the public PR3094 physical-caller/clean-stock handoff instead: compose the already credited PR3081 one-carry primitive across every actual scalar and remove the clean NEG bank. This is a local circuit/access-contract improvement, not independent moment verification.", + "actual_scope": "One-clean-carry conditional implementation of all 9992 prelude/A scalar macros in both pinned PR3076 providers/orientations, with complete changed gate invoice and dirty-bank restoration.", + "bottleneck_link": "Prices a complete local implementation layer of the changed supplier and replaces W-1 clean carries by one, at the cost of exclusive mutable operands and a dirty bank for SCALE. No recursive paid profile or kappa change.", + "author": "Nick Petalas", + "ai_assistance": "Substantial automated development and internal read-only review assistance; no independent human review claimed.", + "budget_minutes": 60, + "stop_rule": "Stop at the verified complete scalar composition or any missing alignment/return/strict local cost obligation. Do not expand into native bank assignment, child/frame/routing implementation or another scalar search.", + "outcome": "completed", + "evidence": "PROOF.md; RESULT.json; registered cold replay and 12 behavioral controls.", + "family_expansion_decision": { + "decision": "narrow", + "target": "Complete scalar composition only; no dependent implementation expansion.", + "why_this_step": "PR3094 leaves W-1 clean carry backing unresolved. This determines a strictly smaller local clean-stock requirement while charging every changed Boolean gate.", + "boundary": "Two disjoint W-bit operand banks exclusively writable inside the macro, arbitrary initial dirty auxiliary for SCALE, one initially-zero carry. Source and carry returned, target output retained.", + "proved": [ + "Modular scalar identities and full return", + "Exact conditional Boolean tariffs", + "Inherited literal scalar grids/ranges and dispatch bindings replayed" + ], + "constructive_upper_bounds": [ + "One clean carry plus two W-bit operand banks; explicit circuits" + ], + "unknown": [ + "Actual owner and exclusive access at every SCALE", + "Native residual adapters and child/frame interiors", + "Paid routing, stock production and later consumer/cleanup" + ], + "consumer_saving_limit": "No claim that the local saving survives physical access or later consumption. Unknowns remain charged obligations.", + "reopen_condition": "An actual native event with named bank owners, legal access lifetimes and complete movement/restoration allowance." + }, + "open_questions": [ + { + "question": "Can one native SCALE borrow and restore an actual dirty bank affordably?", + "why_it_matters": "The one-clean-carry template requires a writable second operand absent from a bare SCALE event.", + "first_step": "Name one SCALE dispatch, its bank owner and access lifetime, then charge movement and return.", + "blocked_by": "Physical ownership and routing are unproved." + }, + { + "question": "Does a complete producer and consumer retain the local saving?", + "why_it_matters": "A scalar tariff is not a supplier moment improvement.", + "first_step": "Combine one paid adapter/frame/child boundary with the same layout and eventual cleanup.", + "blocked_by": "Full native arithmetic, clean-stock backing and consumer bill." + } + ] +} diff --git a/research/rank7-one-carry-scalars/VERIFY.json b/research/rank7-one-carry-scalars/VERIFY.json new file mode 100644 index 0000000000..567c12b536 --- /dev/null +++ b/research/rank7-one-carry-scalars/VERIFY.json @@ -0,0 +1,63 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/rank7-boolean-scalar-caller/FROZEN.json", + "research/rank7-boolean-scalar-caller/RESULT.json", + "research/rank7-boolean-scalar-caller/bitadder.py", + "research/rank7-boolean-scalar-caller/caller.py", + "research/rank7-boolean-scalar-caller/replay.py", + "research/rank7-boolean-scalar-caller/source/RESULT.json", + "research/rank7-boolean-scalar-caller/source/VENDOR.json", + "research/rank7-boolean-scalar-caller/source/integer.py", + "research/rank7-boolean-scalar-caller/source/microstates.py", + "research/rank7-boolean-scalar-caller/source/vendor/lowering/lower.py", + "research/rank7-boolean-scalar-caller/source/vendor/native/RESULT.json", + "research/rank7-boolean-scalar-caller/source/vendor/native/format.py", + "research/rank7-boolean-scalar-caller/source/vendor/native/vendor/clifford.py", + "research/rank7-boolean-scalar-caller/source/vendor/native/vendor/parent/EDITS.json", + "research/rank7-boolean-scalar-caller/source/vendor/native/vendor/parent/VENDOR.json", + "research/rank7-boolean-scalar-caller/source/vendor/native/vendor/parent/contract.py", + "research/rank7-boolean-scalar-caller/source/vendor/native/vendor/parent/contractions.py", + "research/rank7-boolean-scalar-caller/source/vendor/native/vendor/parent/frames.py", + "research/rank7-boolean-scalar-caller/source/vendor/native/vendor/parent/replay_parent.py", + "research/rank7-boolean-scalar-caller/source/vendor/native/vendor/parent/tariff.py", + "research/rank7-boolean-scalar-caller/source/vendor/native/vendor/parent/vendor/CREDITS.md", + "research/rank7-boolean-scalar-caller/source/vendor/native/vendor/parent/vendor/NOTICE", + "research/rank7-boolean-scalar-caller/source/vendor/native/vendor/parent/vendor/PROFILE.json", + "research/rank7-boolean-scalar-caller/source/vendor/native/vendor/parent/vendor/WORD-base.json.gz", + "research/rank7-boolean-scalar-caller/source/vendor/native/vendor/parent/vendor/WORD-extra.json.gz", + "research/rank7-boolean-scalar-caller/source/vendor/native/vendor/parent/vendor/native/NOTICE-PR2226.md", + "research/rank7-boolean-scalar-caller/source/vendor/native/vendor/parent/vendor/native/PR2226-NOTICE.md", + "research/rank7-boolean-scalar-caller/source/vendor/native/vendor/parent/vendor/native/bw_emit.py", + "research/rank7-boolean-scalar-caller/source/vendor/native/vendor/parent/vendor/native/bw_transport.py", + "research/rank7-boolean-scalar-caller/source/verify.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Fresh native/capacity bindings, all 9992 scalar macros, complete exact invoices, 124 circuits/314560 truth columns and 1550 independent array fixtures." + }, + { + "argv": [ + "{python}", + "-O", + "-W", + "error", + "-B", + "{package}/test_scalars.py" + ], + "timeout_seconds": 60, + "checks": "12 behavioral groups: sign and cleanup mutants, source restoration/corruption, dirty carry, alignment/overflow and domain rejection." + } + ] +} diff --git a/research/rank7-one-carry-scalars/bindings.py b/research/rank7-one-carry-scalars/bindings.py new file mode 100644 index 0000000000..e8eb7a4534 --- /dev/null +++ b/research/rank7-one-carry-scalars/bindings.py @@ -0,0 +1,36 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Authenticate all predecessor bytes before importing their implementation.""" + +import hashlib +import json +import sys +from pathlib import Path + +from scalars import require + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +PARENT = ROOT / "research/rank7-boolean-scalar-caller" + + +def load(): + records = json.loads((PACKAGE / "SOURCES.json").read_text())["files"] + require(1 <= len(records) <= 64, "bounded complete dependency inventory") + for record in records: + if record["usage"] != "input": + continue + path = ROOT / record["path"] + require( + not path.is_symlink() and path.stat().st_size <= 8_000_000, "regular input" + ) + require( + hashlib.sha256(path.read_bytes()).hexdigest() == record["sha256"], + "source hash", + ) + sys.path.insert(0, str(PARENT)) + import bitadder + import caller + import replay + from source.vendor.lowering import lower + + return bitadder, caller, replay, lower diff --git a/research/rank7-one-carry-scalars/checks.py b/research/rank7-one-carry-scalars/checks.py new file mode 100644 index 0000000000..97c0d9ef8a --- /dev/null +++ b/research/rank7-one-carry-scalars/checks.py @@ -0,0 +1,94 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Exhaustive complete-boundary checks and a second literal gate interpreter.""" + +from fractions import Fraction as Q +import random + +import scalars as s + + +def packed(width, cases): + s.require(0 < len(cases) <= 65536, "bounded truth batch") + data = [bytearray((len(cases) + 7) // 8) for _ in range(2 * width + 1)] + for lane, (source, target, _) in enumerate(cases): + for bank, value in enumerate((target, source)): + for bit in range(width): + data[bank * width + bit][lane // 8] |= ((value >> bit) & 1) << ( + lane % 8 + ) + return [int.from_bytes(row, "little") for row in data] + + +def check_batch(width, gates, cases): + before = packed(width, cases) + after = s.apply(width, gates, before) + expected = packed(width, [(source, value, value) for source, _, value in cases]) + s.require(after == expected, "complete literal truth columns and clean return") + s.require(s.apply(width, list(reversed(gates)), after) == before, "literal inverse") + + +def array_apply(width, gates, source, target): + """Independent Boolean-list evaluator; no call to the packed interpreter.""" + wires = [bool((v >> i) & 1) for v in (target, source) for i in range(width)] + [ + False + ] + for gate in gates: + if len(gate) == 2: + wires[gate[1]] = wires[gate[1]] != wires[gate[0]] + elif wires[gate[0]] and wires[gate[1]]: + wires[gate[2]] = not wires[gate[2]] + return wires + + +def run(alphabet, build, guards): + s.require(1 <= len(alphabet) <= 32, "bounded scalar alphabet") + columns = circuits = fixtures = 0 + rng = random.Random(481516) + for width in range(4, 8): + limit = 1 << (width - 1) + for kind, a, b in alphabet: + q = Q(a, b) + cases = [] + for source in range(-limit, limit): + for target in range(-limit, limit): + if kind == "add": + if source % q.denominator: + continue + value = target + q * source + else: + try: + value = guards(width, kind, a, b, target, source) + except ValueError: + continue + cases.append((source, target, int(value))) + check_batch(width, build(width, kind, a, b), cases) + columns += len(cases) + circuits += 1 + for width in (23, 64, 84, 148, 256): + limit = 1 << (width - 1) + for kind, a, b in alphabet: + gates = build(width, kind, a, b) + for _ in range(10): + source = rng.randrange(-limit, limit) + target = rng.randrange(-limit // 4, limit // 4) + q = Q(a, b) + if kind == "add": + source = (source // (16 * q.denominator)) * q.denominator + else: + target = (target // 16) * 8 + value = guards(width, kind, a, b, target, source) + actual = array_apply(width, gates, source, target) + expected = [ + bool((v >> i) & 1) for v in (value, source) for i in range(width) + ] + [False] + s.require(actual == expected, "independent array endpoint and return") + s.require( + s.execute(width, gates, source, target) == value % (1 << width), + "interpreters agree", + ) + fixtures += 1 + return { + "truth_columns": columns, + "exhaustive_circuits": circuits, + "array_fixtures": fixtures, + } diff --git a/research/rank7-one-carry-scalars/decisions.tsv b/research/rank7-one-carry-scalars/decisions.tsv new file mode 100644 index 0000000000..dafbcb049d --- /dev/null +++ b/research/rank7-one-carry-scalars/decisions.tsv @@ -0,0 +1,6 @@ +timestamp phase decision reason evidence result +2026-10-17T10:23:42.093068+00:00 workspace reuse imb-research clean inventory and no cwd owners git status, ignored inventory, lsof fresh branch from 997e6a9 +2026-10-17T10:25:25.071637+00:00 scope one-carry complete scalar caller PR3094 still charges W-1 clean carries; PR3081 only local powers read live handoffs and overlap borrow/restore source; negate by modular shears +2026-10-17T10:31:08.592475+00:00 verification complete one-carry composition passes strict full local bill and clean stock win 4 native binds; 124 circuits; 314560 columns; 1550 array fixtures; 12 controls stop before native ownership/routing expansion +2026-10-17T10:32:42.848055+00:00 review use union of forward/backward alphabets and reject malformed recipes internal review found forward-only coefficients and constructor boundary gaps 124 circuits, 314560 columns, 1550 fixtures; 12 optimized groups pass all findings resolved; final registered replay in progress +2026-10-17T10:34:53.186308+00:00 publication retain final source, proof and receipts final stable registered and Git-free replay pass exact output equality; source pins and tested code digests pass ready to commit and publish; remove session scratch after publication diff --git a/research/rank7-one-carry-scalars/scalars.py b/research/rank7-one-carry-scalars/scalars.py new file mode 100644 index 0000000000..cd8e416165 --- /dev/null +++ b/research/rank7-one-carry-scalars/scalars.py @@ -0,0 +1,181 @@ +# SPDX-License-Identifier: Apache-2.0 +"""One-clean-carry scalar circuits with temporarily writable operands.""" + +from fractions import Fraction + +MAX_WIDTH = 256 +MAX_GATES = 20_000 + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def validate(width, gates): + require(type(width) is int and 4 <= width <= MAX_WIDTH, "bounded width") + require(len(gates) <= MAX_GATES, "bounded gate inventory") + for gate in gates: + require(len(gate) in (2, 3), "CX or CCX gate") + require(len(set(gate)) == len(gate), "distinct gate wires") + require( + all(type(i) is int and 0 <= i <= 2 * width for i in gate), + "two operand banks and one carry", + ) + + +def adder(source, target, carry): + """MAJ/UMA modulo 2**n; both operand banks may be written internally.""" + n = len(source) + require(1 <= n <= MAX_WIDTH and len(target) == n, "adder widths") + require(len({*source, *target, carry}) == 2 * n + 1, "disjoint wires") + require( + all( + type(i) is int and 0 <= i <= 2 * MAX_WIDTH + for i in (*source, *target, carry) + ), + "bounded integer wire names", + ) + if n == 1: + return [(source[0], target[0])] + gates = [] + for i in range(n - 1): + a, b, c = source[i], target[i], carry if i == 0 else source[i - 1] + gates.extend(((a, c), (a, b), (b, c, a))) + gates.extend(((source[-1], target[-1]), (source[-2], target[-1]))) + for i in reversed(range(n - 1)): + a, b, c = source[i], target[i], carry if i == 0 else source[i - 1] + gates.extend(((b, c, a), (a, c), (c, b))) + require(len(gates) == 6 * n - 4, "literal MAJ/UMA tariff") + return gates + + +def shifted(width, exponent): + validate(width, ()) + require(type(exponent) is int and -12 <= exponent <= 8, "bounded shift") + source, target = tuple(range(width, 2 * width)), tuple(range(width)) + if exponent >= width: + return [] + if exponent >= 0: + return adder(source[: width - exponent], target[exponent:], 2 * width) + k = -exponent + require(k < width, "right shift below width") + fill = [(source[-1], source[i]) for i in range(k)] + active = source[k:] + source[:k] + return fill + adder(active, target, 2 * width) + list(reversed(fill)) + + +def negate(width): + """Three modular shears and a swap: (T,S) -> (-T,S).""" + validate(width, ()) + target, source = tuple(range(width)), tuple(range(width, 2 * width)) + forward = adder(source, target, 2 * width) + backward = adder(target, source, 2 * width) + gates = forward + list(reversed(backward)) + forward + for t, s in zip(target, source, strict=True): + gates.extend(((t, s), (s, t), (t, s))) + return gates + + +def circuit(width, kind, a, b, recipe, powers): + validate(width, ()) + require(kind in ("add", "scale"), "scalar kind") + require(type(a) is int and type(b) is int and b != 0, "integer coefficient") + q = Fraction(a, b) + require( + abs(q.numerator) <= 255 + and q.denominator <= 4096 + and q.denominator.bit_count() == 1, + "bounded dyadic coefficient", + ) + require(len(recipe) <= 32, "bounded recipe") + require(len(powers) <= 9, "bounded signed powers") + gates = [] + if kind == "add": + require( + all( + sign in (-1, 1) and type(e) is int and -12 <= e <= 8 + for sign, e in powers + ), + "signed-power alphabet", + ) + require( + sum(Fraction(sign) * Fraction(2) ** e for sign, e in powers) + == Fraction(a, b), + "exact coefficient expansion", + ) + require( + all(e >= 1 - q.denominator.bit_length() for _, e in powers), + "powers use only coefficient denominator alignment", + ) + for sign, exponent in powers: + emitted = shifted(width, exponent) + gates.extend(emitted if sign > 0 else reversed(emitted)) + else: + require(not powers, "scale has no ADD powers") + gates = scale(width, recipe, q) + validate(width, gates) + return gates + + +def scale(width, recipe, coefficient): + require(abs(coefficient.numerator).bit_count() == 1, "power-of-two SCALE") + exponent = ( + abs(coefficient.numerator).bit_length() - coefficient.denominator.bit_length() + ) + expected = [("neg", 0)] if coefficient < 0 else [] + expected += [("double" if exponent > 0 else "half", 0)] * abs(exponent) + require(recipe == expected, "canonical guarded SCALE recipe") + gates, product = [], Fraction(1) + for instruction in recipe: + require(len(instruction) == 2 and instruction[1] == 0, "scale target bank") + name = instruction[0] + require(name in ("neg", "half", "double"), "scale-only recipe") + product *= -1 if name == "neg" else Fraction(1, 2) if name == "half" else 2 + if name == "neg": + gates.extend(negate(width)) + else: + shift = [] + for i in range(width - 1): + shift.extend(((i, i + 1), (i + 1, i), (i, i + 1))) + shift.append((width - 2, width - 1)) + gates.extend(shift if name == "half" else reversed(shift)) + require(product == coefficient, "exact SCALE recipe coefficient") + return gates + + +def apply(width, gates, wires): + """AND/XOR interpreter, also for bit-packed exhaustive truth columns.""" + validate(width, gates) + require(len(wires) == 2 * width + 1, "complete wire inventory") + require( + all(type(v) is int and 0 <= v and v.bit_length() <= 65536 for v in wires), + "bounded scalar or packed truth columns", + ) + result = list(wires) + for gate in gates: + control = result[gate[0]] + if len(gate) == 3: + control &= result[gate[1]] + result[gate[-1]] ^= control + return result + + +def execute(width, gates, source, target, *, carry=0): + validate(width, gates) + require(carry == 0, "clean carry entrance") + require(all(type(v) is int for v in (source, target)), "integer operands") + limit = 1 << (width - 1) + require(-limit <= source < limit and -limit <= target < limit, "signed operands") + wires = [(value >> i) & 1 for value in (target, source) for i in range(width)] + after = apply(width, gates, wires + [carry]) + require(after[width : 2 * width] == wires[width:], "source restored") + require(after[-1] == 0, "carry restored") + return sum(after[i] << i for i in range(width)) + + +def counts(gates): + return { + "cx": sum(len(g) == 2 for g in gates), + "ccx": sum(len(g) == 3 for g in gates), + } diff --git a/research/rank7-one-carry-scalars/test_scalars.py b/research/rank7-one-carry-scalars/test_scalars.py new file mode 100644 index 0000000000..2d7d253966 --- /dev/null +++ b/research/rank7-one-carry-scalars/test_scalars.py @@ -0,0 +1,141 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Behavioral failure controls for the complete one-carry scalar boundary.""" + +import hashlib +import json +import tempfile +import unittest +from pathlib import Path +from unittest.mock import patch +from fractions import Fraction as Q + +import bindings +import checks +import scalars as s +import verify + +BITS, CALLER, REPLAY, LOWER = bindings.load() +BUILD = verify.factory(BITS, LOWER) + + +class ScalarTests(unittest.TestCase): + def test_dirty_negation_and_inverse(self): + gates = BUILD(8, "scale", -1, 1) + for source in (-128, -7, 0, 127): + for target in (-128, -1, 0, 127): + self.assertEqual(s.execute(8, gates, source, target), -target % 256) + self.assertEqual(s.counts(gates), {"cx": 114, "ccx": 42}) + + def test_shift_tariffs_and_edge_cases(self): + for width in (4, 23, 84, 256): + for exponent in range(-3, 9): + gates = s.shifted(width, exponent) + n = width - max(0, exponent) + expected = ( + {"cx": 0, "ccx": 0} + if n <= 0 + else {"cx": 1, "ccx": 0} + if n == 1 + else {"cx": 4 * n - 2 + 2 * max(0, -exponent), "ccx": 2 * n - 2} + ) + self.assertEqual(s.counts(gates), expected) + source = -(1 << max(0, -exponent)) + observed = s.execute(width, gates, source, 0) + self.assertEqual( + observed, int(Q(source) * Q(2) ** exponent) % (1 << width) + ) + + def test_missing_sign_fill_rejects(self): + gates = BUILD(8, "add", 1, 8) + with self.assertRaises(ValueError): + checks.check_batch(8, gates[1:], [(-8, 0, -1)]) + + def test_missing_sign_cleanup_rejects(self): + gates = BUILD(8, "add", 1, 8) + with self.assertRaises(ValueError): + checks.check_batch(8, gates[:-1], [(-8, 0, -1)]) + + def test_missing_carry_cleanup_and_wrong_sign_reject(self): + gates = BUILD(4, "add", 1, 1) + cases = [(a, b, a + b) for a in range(-8, 8) for b in range(-8, 8)] + with self.assertRaises(ValueError): + checks.check_batch(4, gates[:-2], cases) + with self.assertRaises(ValueError): + checks.check_batch(4, gates, [(2, 3, 1)]) + + def test_negation_swap_is_necessary(self): + gates = BUILD(8, "scale", -1, 1) + with self.assertRaises(ValueError): + checks.check_batch(8, gates[:-24], [(37, -9, 9)]) + + def test_clean_carry_entrance(self): + with self.assertRaises(ValueError): + s.execute(8, BUILD(8, "add", 1, 1), 2, 3, carry=1) + + def test_original_alignment_and_signed_endpoint_guards(self): + for args in ( + (8, "add", 1, 2, 0, -7), + (8, "add", 1, 1, 127, 1), + (8, "scale", -1, 1, -128, 37), + ): + with self.assertRaises(ValueError): + CALLER.guards(*args) + self.assertEqual(s.execute(8, BUILD(8, "add", 1, 1), 1, 127), 128) + + def test_actual_internal_source_write_and_return(self): + gates = BUILD(8, "add", 1, 1) + self.assertTrue(any(8 <= gate[-1] < 16 for gate in gates)) + self.assertEqual(s.execute(8, gates, -19, 5), 242) + self.assertEqual(BUILD(8, "scale", 1, 1), []) + + def test_changed_source_rejects_before_import(self): + with tempfile.TemporaryDirectory(prefix="one-carry-hash-") as directory: + root = Path(directory) + (root / "input.py").write_text("changed source") + (root / "SOURCES.json").write_text( + json.dumps( + { + "files": [ + { + "path": "input.py", + "usage": "input", + "sha256": hashlib.sha256( + b"original source" + ).hexdigest(), + } + ] + } + ) + ) + with ( + patch.object(bindings, "PACKAGE", root), + patch.object(bindings, "ROOT", root), + ): + with self.assertRaisesRegex(ValueError, "source hash"): + bindings.load() + + def test_stronger_alignment_and_wrong_scale_recipe_reject(self): + with self.assertRaisesRegex(ValueError, "denominator alignment"): + s.circuit(8, "add", 1, 1, [], [(1, -1), (1, -1)]) + with self.assertRaisesRegex(ValueError, "guarded SCALE recipe"): + s.circuit(8, "scale", 2, 1, [], []) + with self.assertRaisesRegex(ValueError, "guarded SCALE recipe"): + s.circuit(8, "scale", 1, 1, [("half", 0), ("double", 0)], []) + + def test_boundary_validation(self): + for width in (3, 257): + with self.assertRaises(ValueError): + s.shifted(width, 0) + with self.assertRaises(ValueError): + s.shifted(4, -4) + for gates in ([(0, 0)], [(0, 17)], [(0, 1, 2, 3)]): + with self.assertRaises(ValueError): + s.validate(8, gates) + with self.assertRaises(ValueError): + s.adder((0, 1), (1, 2), 3) + with self.assertRaises(ValueError): + s.circuit(8, "add", 3, 2, [], [(1, 0)]) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/rank7-one-carry-scalars/verify.py b/research/rank7-one-carry-scalars/verify.py new file mode 100644 index 0000000000..f92625844c --- /dev/null +++ b/research/rank7-one-carry-scalars/verify.py @@ -0,0 +1,122 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Cold replay and full one-carry scalar invoice, with bounded truth checks.""" + +import argparse +import hashlib +import json +import tempfile +from pathlib import Path + +import bindings +import checks +import scalars as s + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":")).encode() + + +def factory(bits, lower): + def build(width, kind, a, b): + recipe = lower.certify(kind, a, b, policy="target_walk") + powers = bits.terms(a, b) if kind == "add" else [] + return s.circuit(width, kind, a, b, recipe, powers) + + return build + + +def aggregate(width, histogram, build): + s.require( + len(histogram) == 29 and sum(histogram.values()) == 9992, "complete histogram" + ) + total = {"cx": 0, "ccx": 0} + templates = {} + for key, count in sorted(histogram.items()): + kind, a, b = key.split(":") + gates = build(width, kind, int(a), int(b)) + templates[key] = gates + for name, n in s.counts(gates).items(): + total[name] += 2 * count * n + return { + "both_components": total, + "templates_sha256": hashlib.sha256(canonical(templates)).hexdigest(), + } + + +def run(work): + bits, caller, replay, lower = bindings.load() + parent = replay.run(work) + expected = json.loads((bindings.PARENT / "RESULT.json").read_text()) + expected.pop("bit_checks") + s.require(parent == expected, "fresh native/capacity and prior invoice binding") + build = factory(bits, lower) + streams, all_keys = {}, set() + for provider in ("base", "extra"): + for direction in ("forward", "backward"): + old = parent["providers"][provider][direction] + histogram = old["histogram"] + all_keys.update(histogram) + invoices = { + str(w): aggregate(w, histogram, build) + for w in (23, 24, 64, 84, 85, 148, 256) + } + current = invoices["84"]["both_components"] + baseline = old["both_components_at_84_bits"]["direct"] + saving = {g: baseline[g] - current[g] for g in baseline} + s.require(sum(saving.values()) > 0, "strict full scalar gate saving") + # All shifts are below 23: counts are affine throughout 23..256. + for w in (64, 84, 85, 148, 256): + for g in current: + lo = invoices["23"]["both_components"][g] + slope = invoices["24"]["both_components"][g] - lo + s.require( + invoices[str(w)]["both_components"][g] == lo + (w - 23) * slope, + "uniform tariff law", + ) + streams[f"{provider}/{direction}"] = { + "dispatch_sha256": old["dispatch_sha256"], + "macros": old["macros"], + "histogram": histogram, + "invoices": invoices, + "saving_at_84_bits": saving, + } + alphabet = [ + tuple([k, int(a), int(b)]) + for k, a, b in (key.split(":") for key in sorted(all_keys)) + ] + return { + "status": "PASS_ONE_CARRY_SCALARS_NO_NEW_KAPPA", + "data_width": 84, + "clean_carry_bits": 1, + "prior_clean_carry_bits": 83, + "operand_bits": 168, + "coefficient_scratch_bits": 0, + "boundary": "Both operand banks exclusively writable during each macro; source and carry restored.", + "streams": streams, + "bit_checks": checks.run(alphabet, build, caller.guards), + } + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--work", type=Path) + args = parser.parse_args() + if args.work: + work = args.work.expanduser().resolve() + s.require( + not work.exists() and not work.is_relative_to(bindings.ROOT), + "fresh external output", + ) + work.mkdir(parents=True) + result = run(work) + else: + with tempfile.TemporaryDirectory(prefix="one-carry-scalars-") as directory: + result = run(Path(directory)) + expected = bindings.PACKAGE / "RESULT.json" + if expected.exists(): + s.require(result == json.loads(expected.read_text()), "deterministic receipt") + print(json.dumps(result, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()