From 64bf3c4a09018278ff80d5788f6dce8bf31c4c90 Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Tue, 20 Oct 2026 02:34:20 +0000 Subject: [PATCH 1/2] Price one typed actual-width physical H and its toward-zero return. The matched-layout call equals the PR 3623 tensor on fifty small rounds and carries an exact read, write and gate bill. It does not reuse tapes across rounds or change kappa. Co-authored-by: unpaidmoon --- .../typed-actual-width-physical-h/PROOF.md | 121 ++++ .../typed-actual-width-physical-h/README.md | 81 +++ .../RECEIPT.json | 41 ++ .../SOURCES.json | 18 + .../typed-actual-width-physical-h/TASK.json | 72 +++ .../typed-actual-width-physical-h/VERIFY.json | 28 + .../frozen/pr3623-check_join.py | 388 ++++++++++++ .../physical_h.py | 595 ++++++++++++++++++ .../typed-actual-width-physical-h/verify.py | 178 ++++++ 9 files changed, 1522 insertions(+) create mode 100644 research/typed-actual-width-physical-h/PROOF.md create mode 100644 research/typed-actual-width-physical-h/README.md create mode 100644 research/typed-actual-width-physical-h/RECEIPT.json create mode 100644 research/typed-actual-width-physical-h/SOURCES.json create mode 100644 research/typed-actual-width-physical-h/TASK.json create mode 100644 research/typed-actual-width-physical-h/VERIFY.json create mode 100644 research/typed-actual-width-physical-h/frozen/pr3623-check_join.py create mode 100644 research/typed-actual-width-physical-h/physical_h.py create mode 100644 research/typed-actual-width-physical-h/verify.py diff --git a/research/typed-actual-width-physical-h/PROOF.md b/research/typed-actual-width-physical-h/PROOF.md new file mode 100644 index 0000000000..2072c8d541 --- /dev/null +++ b/research/typed-actual-width-physical-h/PROOF.md @@ -0,0 +1,121 @@ +# Typed actual-width H and toward-zero return + +This note prices one matched-layout normalized butterfly and its rounded +return. It does not apply the diagonal, reuse tapes across rounds, or change +a multiplication exponent. + +## Typed object + +Fix a layout parameter `K >= 1`, axis flags, length `ell >= 2`, and precision +`p >= 1`. Let the original and physical named-slot orders be the two orders in +PR #3623's `slots_for`. Write `M` for the number of records and `r = 2^ell` +for the coefficients in each record. A round `h` in that layout's round list +has selected address bits `beta_1, ..., beta_g` from the matched-extent rule: + +- on a common round, `g` equals the axis count and the bits are + `right + rho + t K`; +- on a prefix round, the bits are exactly the physical slots of height `h`. + +The packet width is `w = p + 2`. The work width is `W = p + g + 2`. Every +borrowed numerator is an integer in `[-2^p, 2^p]`, encoded as an MSB-first +two's-complement word of width `w`. The call reads those words in either the +original or the physical slot order and writes the rounded tensor in the +physical order. The root copy is LSB-first. The consumer copy is MSB-first. +Both copies, and the blanked work tape, finish with their heads at cell 0. +The borrowed source bytes are unchanged. The object rejects a second call. + +An old descriptor is not coerced. On the three short axes with `ell = 3` and +`K = 1`, round `h = 1` has selected bits `(3, 4, 5)`. The concealed bits +`(0, 1, 2)` raise `selected-bit descriptor`. + +## Butterfly and rounding + +Sign-extend each admitted word into width `W`. For each selected bit `beta`, +split the work image by that address bit, interleave the two halves so that +partners are adjacent, replace each adjacent pair `(a, b)` by `(a+b, a-b)`, +and merge the sum back onto the clear bit and the difference onto the set bit. +Component additions and subtractions are ripple circuits on width `W`. +Subtraction is invert-and-add-one. A final carry that leaves the signed +`W`-bit range aborts; the bound below says a successful admitted call does +not hit that abort. + +After `t` selected bits, every work numerator is a sum of `2^t` input +numerators with coefficients in `{±1}`. Its absolute value is therefore at +most `2^{p+t}`. At `t = g` this is at most `2^{p+g}`. Width `W = p+g+2` +represents every integer from `-2^{p+g+1}` through `2^{p+g+1}-1`, so the +whole work vector fits. + +`Q_p` then acts componentwise. Let `s` be the sign bit. Form the magnitude by +xoring every bit with `s` and adding `s`, drop the `g` low bits by keeping the +high `w` bits, then xor with `s` and add `s` again. For a nonnegative +magnitude this wiring is division by `2^g` rounded down. Restoring the sign +makes the result truncating division: nonnegative inputs use `floor(n/2^g)`, +and negative inputs use `-floor(|n|/2^g)`. That is not an arithmetic right +shift. In particular `-1` divided by `2` is `0` here and `-1` under an +arithmetic shift. The same witness appears in the two-record call below: +records `(0, 0)` and `(1, 0)` on the single selected bit become `(0, 0)` and +`(0, 0)` after rounding, whereas an arithmetic shift of the difference `-1` +would have left `-1`. + +The consumer word is that signed `w`-bit vector, MSB first. The root word is +its reversal. Decoding the reversal as an MSB word changes the integer `1`. +Reversing again recovers it. After rounding, every returned numerator still +lies in `[-2^p, 2^p]`, which fits in a `w = p+2` two's-complement word +because `2^p <= 2^{p+1}-1` and `-2^p >= -2^{p+1}`. + +The integer shadow of this schedule is exactly the unnormalized Hadamard on +the selected bits, followed by truncating division by `2^g`. Hadamard factors +on distinct bits commute, so the selected-bit order does not change the +integer result. PR #3623's explicit tensor `h_direct`, followed by its +toward-zero `truncate`, is the same map. The finite cubes compare those two +executables; they are controls for the wiring, not the only inputs covered +by the schedule. + +## Exact bill + +Write `C = 2 M r` for the number of real and imaginary components, and +`L = C W` for the work-tape length. A successful call performs exactly + +```text +reads = C w + 5 g L + L +writes = 2 L + 7 g L + 2 C w +gates = C (W - w) + C + 2 g M + (3/2) g C W + C (2 W + 2 w) +``` + +The summands are the layout read and sign-extended write, five sequential +work-length passes per selected bit (split, interleave, adjacent butterfly, +deinterleave, merge), the final `Q_p` read, the root and consumer writes, and +the final work-tape blank. The two extra writes per selected bit blank the +half tapes and the paired tape. Gates are one disk test and `W-w` sign-fanout +gates per component, two address tests per record per selected bit, `3W` +adder/inverter gates per butterfly component pair, and `2W+2w` magnitude and +resign gates per component. Head travel is data-independent and equals the +itinerary in `itinerary_moves`: every scan starts and ends at cell 0, and the +adjacent butterfly is the only pass that seeks backward inside a pair. + +For two records of one bit each, that adjacent pair costs 4 moves: step from +cell 0 to cell 1, return to cell 0, step to cell 1, and home. The whole +linear level on that shape costs 14 moves, because each of the five length-2 +scans costs 2 and the adjacent pair costs 4, while every one-cell half tape +costs 0. Both integers are checked. + +The two-record witness with `ell = 2`, one short axis, `K = 1`, `p = 4` and +one selected bit has `M = 2`, `r = 4`, `g = 1`, `W = 7`, `w = 6`, `C = 16` +and `L = 112`. The formulas give 768 reads, 1200 writes and 620 gates, and +the executed ledger matches those three integers. Its head travel is the +separate itinerary value 3890. + +## What this does not prove + +The diagonal factors `J_h` stay with PR #3617. This return is `Q_p H` in +physical slot order, not `J Q_p H` and not `Q_p H J`. Auxiliary tapes are +allocated per selected bit and blanked before the next bit; that is not a +fixed all-round stock. The initial framing of a production cube, descriptor +updates, previous-output reset, and a simultaneous buffer bound are still +open. No call uses the production band `ell >= 45812984491`. No selected +exponent changes. + +The checked `Q_p` range is every integer from `-2^{p+g}` through `2^{p+g}` +for `p = 4` and `0 <= g <= 6`, which covers every selected-bit width in the +cube suite. The wiring argument is not limited to those widths; the exhaustive +loop is. diff --git a/research/typed-actual-width-physical-h/README.md b/research/typed-actual-width-physical-h/README.md new file mode 100644 index 0000000000..9ec15c5fbb --- /dev/null +++ b/research/typed-actual-width-physical-h/README.md @@ -0,0 +1,81 @@ +# Typed actual-width physical H + +**A one-round rounded return for the matched twiddle layout. No new κ.** + +PR #3623 proves a matched chunk width `K = floor((d-1)^(1/500))` and joins +PR #3617's fixed diagonal to arithmetic-oracle butterflies. Its first open +question is a typed physical `H` and toward-zero `Q_p` on that same array. +This package supplies that call: MSB packet words in, physical-order rounded +tensor out, with an exact read/write/gate bill and a data-independent head +itinerary. It does not build the inter-round stock contract. + +## Result + +For each round of the ten small layouts used by PR #3623's cube checker, and +for both original and physical source orders, the tape program equals PR +#3623's explicit tensor followed by toward-zero division by `2^g`. The +borrowed source is unchanged, scratch and per-bit auxiliary tapes are +blanked, heads return to cell 0, and a second call is rejected. The old +descriptor `(0, 1, 2)` is rejected on the matched round whose bits are +`(3, 4, 5)`. A numerator `17` at `p = 4` is rejected before the butterfly. + +The bill depends only on the record count, coefficient count, selected-bit +count and precision. On the two-record witness it is 768 reads, 1200 writes +and 620 gates. Across the 50 calls the totals are 18,871,808 reads, +27,630,304 writes, 94,213,460 moves and 9,636,792 gates. [PROOF.md](PROOF.md) +derives the closed form. The cube comparisons are wiring controls for that +schedule, not a production-width execution. + +Arithmetic right shift is a different return: `-1` shifted by one bit stays +`-1`, while this `Q_p` returns `0`. Skipping the LSB-to-MSB bridge changes +the integer `1`. + +## Evidence + +The frozen tensor is byte-identical to `check_join.py` at PR #3623 head +`c5ab698bba8b35323e40ae3b132e78f26179d393` and at the handoff head +`328c40966b650f60b1d62cfb0b1d67b2b755eb62` (git blob +`421ae05f081ec37e4c5fa0b1b7e200a1578ab16d`). The current PR head only adds a +workflow commit after that scientific file. `Q_p` was also checked on every +integer in `[-2^{p+g}, 2^{p+g}]` for `p = 4` and `g = 0..6`. + +From the repository root, with Python 3.12 and the standard library: + +```sh +python3 -B research/typed-actual-width-physical-h/verify.py +python3 -B -O research/typed-actual-width-physical-h/verify.py +python3 -B scripts/research_package.py --package research/typed-actual-width-physical-h --check-only +python3 -B scripts/research_package.py --package research/typed-actual-width-physical-h +``` + +Both direct runs print `PASS_TYPED_ACTUAL_WIDTH_PHYSICAL_H` and match +[RECEIPT.json](RECEIPT.json). On this host each direct run took about 10 +seconds. The registered launcher was also run, as recorded in the PR. + +Not run: the selected cold replay, Lean, Docker, a production `ell`, the +PR #3617 diagonal, and any all-round tape reuse. + +## Open next questions + +1. Can one fixed collection of full-cube tapes carry every round, with + previous-output reset and a proved simultaneous-stock bound? The diagonal + pass is one-shot and this `H` allocates its auxiliary tapes per selected + bit. A useful first step is one two-round schedule on the `ell = 2` + witness with an explicit buffer list. The blocker is that no such shared + inventory is constructed here. +2. Can this return be placed under PR #3617's framed diagonal on one complete + cube without a fresh stage object per round? That would discharge the + fixed-`h` join, not the inter-round stock question. The blocker is the + one-shot full pass and the still-unpriced initial framing. +3. Does any of this change the retained outer movement bottleneck? No faster + exponent is claimed. Reopen that only with a paid movement change. The + blocker is the unchanged `169711/2000000000000` ordinary term. + +## Credit + +The matched layout, tensor and toward-zero truncation are Clear1nsight's PR +#3623, incorporating Sagar Thakrar's PR #3617 diagonal contract and the +PR #3493 / #3593 / #3599 / #3611 sources credited there. The handoff is +discussion #1166 comment 19016699. New tape schedule, bill and checks by +unpaidmoon, with substantial assistance from Grok 4.7 in Cursor. No +independent human or formal-kernel acceptance is claimed. Apache-2.0. diff --git a/research/typed-actual-width-physical-h/RECEIPT.json b/research/typed-actual-width-physical-h/RECEIPT.json new file mode 100644 index 0000000000..052d718fae --- /dev/null +++ b/research/typed-actual-width-physical-h/RECEIPT.json @@ -0,0 +1,41 @@ +{ + "pass_token": "PASS_TYPED_ACTUAL_WIDTH_PHYSICAL_H", + "calls": 50, + "selected_bit_widths": [ + 1, + 2, + 3, + 4 + ], + "totals": { + "read": 18871808, + "write": 27630304, + "move": 94213460, + "gate": 9636792 + }, + "digest_sha256": "9de82d583fb882cdaa6f238d764ef8e6b72ff757aa856a4983ad9a889229d176", + "controls": { + "negative_output": [ + [ + 0, + 0 + ], + [ + 0, + 0 + ] + ], + "negative_ledger": { + "read": 768, + "write": 1200, + "move": 3890, + "gate": 620 + }, + "arithmetic_shift_of_minus_one": -1, + "old_descriptor": "selected-bit descriptor", + "disk": "unit disk", + "adjacent_pair_moves": 4, + "linear_level_moves_m2_rw1": 14, + "q_range_failures": 0 + } +} diff --git a/research/typed-actual-width-physical-h/SOURCES.json b/research/typed-actual-width-physical-h/SOURCES.json new file mode 100644 index 0000000000..a604c6a640 --- /dev/null +++ b/research/typed-actual-width-physical-h/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "bb4bccbf42844d2801487450727c2f63e10d1d0f", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + } + ] +} diff --git a/research/typed-actual-width-physical-h/TASK.json b/research/typed-actual-width-physical-h/TASK.json new file mode 100644 index 0000000000..06a9ac3b48 --- /dev/null +++ b/research/typed-actual-width-physical-h/TASK.json @@ -0,0 +1,72 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 6, + "base_commit": "bb4bccbf42844d2801487450727c2f63e10d1d0f", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Can one exact all-size/compiler, precision, hosting or restoration implication be proved or falsified?", + "starting_points": [ + "certificates/selected-result.json", + "docs/audit.md" + ], + "methods": [ + "Prove one missing implication with explicit quantified hypotheses.", + "Find an exact counterexample at the claimed interface boundary." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the selected review scope and choose one exact all-size or precision implication.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write its quantified inputs and conclusion; find a missing hypothesis or construct a minimal exact adversarial instance.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": [ + "Choose one tape, precision, hosting or restoration lemma." + ], + "scope_change_triggers": [ + "Replacing a quantified obligation with another finite smoke test." + ], + "overlap_terms": [ + "uniform transfer", + "all-size", + "precision" + ] + }, + "scope_status": "changed", + "actual_scope": "Implement one typed actual-width physical H and toward-zero Q_p return on the PR3623 matched layout, and give its exact tape bill.", + "scope_change_reason": "The catalogue card asks for one quantified all-size, precision, hosting or restoration implication. This takes the released physical-H obligation from discussion 1166 comment 19016699, which is the first open question of PR 3623, rather than a new all-size compiler theorem. The schedule identity and closed bill are the implication; the finite cubes check the wiring.", + "bottleneck_link": "PR 3623 leaves H and Q_p unpriced, so the matched layer still cannot be charged as a caller. An exact one-round bill shows what that return costs and that an arithmetic shift or an old bit descriptor is a different return. It does not move the retained outer ordinary bottleneck.", + "budget_minutes": 60, + "stop_rule": "Stop after one round's typed return and its bill. Do not build inter-round stock, the diagonal, or a production-width root. Preserve the selected frontier.", + "outcome": "partial", + "evidence": "PROOF.md derives the work-width bound, the toward-zero wiring, and the read/write/gate formulas. verify.py matches PR3623 h_direct plus truncate on 50 calls, rejects the old descriptor, the out-of-disk numerator and a second call, and checks Q_p on the full p=4, g<=6 magnitude range. RECEIPT.json records the totals.", + "author": "unpaidmoon", + "ai_assistance": "Substantial assistance from Grok 4.7 in Cursor. No independent human or formal-kernel acceptance is claimed.", + "open_questions": [ + { + "question": "Can one fixed collection of full-cube tapes carry every round of this H, with previous-output reset and a simultaneous-stock bound?", + "why_it_matters": "Per-bit auxiliary tapes and a one-shot diagonal do not give the all-round Q term in PR 3623.", + "first_step": "Write a two-round schedule on the ell=2 witness and list every live buffer.", + "blocked_by": "No shared inventory is constructed in this package." + }, + { + "question": "Can this MSB return sit under PR 3617's framed diagonal on one cube without a fresh stage object per round?", + "why_it_matters": "That would discharge the fixed-h semantic join while leaving inter-round stock open.", + "first_step": "Feed one rounded packet from this return into the unchanged diagonal consumer and price the framing.", + "blocked_by": "The published full pass is one-shot, and initial framing is still unpriced." + }, + { + "question": "Can a paid movement change improve the retained outer ordinary bottleneck while keeping this return?", + "why_it_matters": "The matched K and this local H bill do not change the narrower 169711/2000000000000 movement term.", + "first_step": "Price a different movement or consumer with the same endpoints and the full transfer invoice.", + "blocked_by": "No improved outer movement construction is claimed here." + } + ] +} diff --git a/research/typed-actual-width-physical-h/VERIFY.json b/research/typed-actual-width-physical-h/VERIFY.json new file mode 100644 index 0000000000..cc3f2abba2 --- /dev/null +++ b/research/typed-actual-width-physical-h/VERIFY.json @@ -0,0 +1,28 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Fifty matched-layout calls equal the frozen tensor and the closed bill; old descriptor, disk, one-shot, bridge and toward-zero controls reject or disagree as stated." + }, + { + "argv": [ + "{python}", + "-B", + "-O", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same identity and failure controls with assertions disabled, so the result does not depend on assert statements." + } + ] +} diff --git a/research/typed-actual-width-physical-h/frozen/pr3623-check_join.py b/research/typed-actual-width-physical-h/frozen/pr3623-check_join.py new file mode 100644 index 0000000000..421ae05f08 --- /dev/null +++ b/research/typed-actual-width-physical-h/frozen/pr3623-check_join.py @@ -0,0 +1,388 @@ +"""Exact bounded checks for the changed outer layout; no physical root replay. + +New audit by Clear1nsight with substantial OpenAI assistance, Apache-2.0. +The two imported source modules remain byte-identical and separately credited. +""" + +from fractions import Fraction +from hashlib import sha1, sha256 +import importlib.util +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent + + +def need(condition, reason): + if not condition: + raise ValueError(reason) + + +def rejected(call, reason): + try: + call() + except ValueError as error: + need(str(error) == reason, "unexpected rejection reason: " + str(error)) + return reason + raise ValueError("missing rejection: " + reason) + + +def root_int(n, degree): + need(type(n) is int and n >= 0 and degree >= 1, "integer root domain") + if n < 2: + return n + x = 1 << ((n.bit_length() + degree - 1) // degree) + while True: + y = ((degree - 1) * x + n // pow(x, degree - 1)) // degree + if y >= x: + break + x = y + need(pow(x, degree) <= n < pow(x + 1, degree), "exact integer root") + return x + + +def integer_digest(n): + return sha256(n.to_bytes((n.bit_length() + 7) // 8 or 1, "big")).hexdigest() + + +def floors_and_cost(): + records = [] + for k in (2, 3): + d0 = pow(k, 500) + old = pow(d0, 40) + changed = pow(d0 + 1, 40) + cases = ((old - 1, k - 1, k - 1), (old, k, k - 1), + (changed - 1, k, k - 1), (changed, k, k)) + for p, expect_old, expect_new in cases: + d = root_int(p, 40) + need(root_int(d, 500) == expect_old, "old exact-K threshold") + need(root_int(d - 1, 500) == expect_new, "matched exact-K threshold") + for p, expected in ((6 * ((old + 5) // 6), k - 1), + (6 * ((changed + 5) // 6), k)): + need(p % 6 == 0, "actual precision multiple") + need(root_int(root_int(p, 40) - 1, 500) == expected, + "actual precision floor boundary") + records.append({"k": k, "old_threshold_bits": old.bit_length(), + "new_threshold_bits": changed.bit_length(), + "old_threshold_sha256": integer_digest(old), + "new_threshold_sha256": integer_digest(changed), + "actual_old_offset": (-old) % 6, + "actual_new_offset": (-changed) % 6}) + need(2 ** 39 > 12 * 41 ** 2, "record base inequality") + need(2 ** 39 * 41 ** 80 > 42 ** 80, "record monotonic ratio") + ell_min = (2 ** 39 + 11) // 12 + need(ell_min == 45812984491 and ell_min > 32, "actual caller versus executable cap") + tau = Fraction(99830289, 10 ** 8) + alpha = Fraction(99827101, 10 ** 8) + old_bottleneck = Fraction(1, 40 * 500) * (1 - tau) + new_layer_saving = (1 - alpha) / 40 + need(old_bottleneck == Fraction(169711, 2000000000000), "preserved outer ordinary bill") + need(new_layer_saving == Fraction(172899, 4000000000), "new layer exponent") + need(new_layer_saving > old_bottleneck, "outer bottleneck remains narrower") + return {"thresholds": records, "minimum_nontrivial_ell_lower_bound": ell_min, + "source_band_integer_checks": 2, + "exact_K_saving": str(old_bottleneck), "new_layer_saving": str(new_layer_saving)} + + +def slots_for(ell, flags, k): + need(ell >= 2 and flags and 1 <= k < ell, "layout domain") + original = tuple((i, h) for i, long in enumerate(flags) + for h in range(ell - (not long) - 1, -1, -1)) + b, q = (ell - 1) % k, (ell - 1) // k + prefix = [(i, ell - 1) for i, long in enumerate(flags) if long] + prefix += [(i, h) for h in range(b - 1, -1, -1) for i in range(len(flags))] + chunks = [(i, h) for j in range(q) for i in range(len(flags)) + for h in range(ell - 2 - j * k, ell - 2 - (j + 1) * k, -1)] + changed = tuple(prefix + chunks) + need(len(set(changed)) == len(original) and set(changed) == set(original), "layout bijection") + return original, changed + + +def bit_at(x, slots, named): + return (x >> (len(slots) - 1 - slots.index(named))) & 1 + + +def selected(slots, h): + return tuple(len(slots) - 1 - j for j, item in enumerate(slots) if item[1] == h) + + +def reorder(data, before, after): + need(set(before) == set(after), "permutation named domain") + output = [None] * len(data) + for x, row in enumerate(data): + y = 0 + for name in after: + y = 2 * y + bit_at(x, before, name) + output[y] = list(row) + need(all(row is not None for row in output), "complete permutation") + return output + + +def h_fast(data, bits): + result = [list(row) for row in data] + for bit in bits: + for x in range(len(result)): + if (x >> bit) & 1: + continue + y = x | (1 << bit) + left, right = result[x], result[y] + result[x] = [(a[0] + b[0], a[1] + b[1]) for a, b in zip(left, right)] + result[y] = [(a[0] - b[0], a[1] - b[1]) for a, b in zip(left, right)] + return result, 1 << len(bits) + + +def h_direct(data, bits): + """Independent explicit tensor matrix, before its 2^g denominator.""" + mask = sum(1 << bit for bit in bits) + result = [] + for x in range(len(data)): + row = [(0, 0) for _ in data[0]] + for choice in range(1 << len(bits)): + y = x & ~mask + for j, bit in enumerate(bits): + y |= ((choice >> j) & 1) << bit + sign = -1 if ((x & y & mask).bit_count() % 2) else 1 + row = [(a[0] + sign * b[0], a[1] + sign * b[1]) + for a, b in zip(row, data[y])] + result.append(row) + return result, 1 << len(bits) + + +def truncate(data, denominator): + def part(v): + return (1 if v >= 0 else -1) * (abs(v) // denominator) + return [[(part(a), part(b)) for a, b in row] for row in data] + + +def exponent(x, slots, ell, flags, h, opposite=False): + value = 0 + for i, long in enumerate(flags): + if h >= ell - (not long): + continue + branch = bit_at(x, slots, (i, h)) + low = sum((1 << v) * bit_at(x, slots, (i, v)) for v in range(h)) + value += branch * low + return ((1 if opposite else -1) * (1 << (ell - h)) * value) % (2 << ell) + + +def rotate(row, e): + r = len(row) + output = [None] * r + for j, (a, b) in enumerate(row): + quotient, destination = divmod(j + e, r) + sign = -1 if quotient % 2 else 1 + output[destination] = (sign * a, sign * b) + return output + + +def diagonal(data, slots, ell, flags, h, opposite=False): + return [rotate(row, exponent(x, slots, ell, flags, h, opposite)) + for x, row in enumerate(data)] + + +def reference_round(data, slots, ell, flags, h, opposite=False): + if opposite: + data = diagonal(data, slots, ell, flags, h, True) + raw, denominator = h_direct(data, selected(slots, h)) + if not opposite: + raw = diagonal(raw, slots, ell, flags, h) + return truncate(raw, denominator) + + +def caller_round(data, slots, ell, flags, k, h, opposite=False): + g, a = len(flags), sum(flags) + b, q = (ell - 1) % k, (ell - 1) // k + if b <= h < ell - 1: + j, rho = (ell - 2 - h) // k, (h - b) % k + left, right = a + g * b + j * g * k, (q - j - 1) * g * k + need(left + g * k + right == len(slots), "complete root extent") + bits = tuple(right + rho + t * k for t in range(g)) + need(set(bits) == set(selected(slots, h)), "literal root selected positions") + else: + bits = selected(slots, h) + if opposite: + data = diagonal(data, slots, ell, flags, h, True) + raw, denominator = h_fast(data, bits) + result = truncate(raw, denominator) + if not opposite: + result = diagonal(result, slots, ell, flags, h) + return result + + +def cube_checks(): + cases = ((2, (False,), 1), (2, (True,), 1), + (3, (False, False), 1), (3, (True, False), 1), + (3, (True, True), 1), (3, (False, False, False), 1), + (3, (True, False, True), 1), + (3, (False, False, False, False), 2), + (3, (True, False, False, False), 2), + (4, (True, False), 2)) + results = [] + for ell, flags, k in cases: + original, physical = slots_for(ell, flags, k) + m, r = 1 << len(original), 1 << ell + cube = [[((17 * x + 5 * j + 3) % 7 - 3, (11 * x + 7 * j + 2) % 7 - 3) + for j in range(r)] for x in range(m)] + levels = list(range(ell - 2, -1, -1)) + if any(flags): + levels.insert(0, ell - 1) + b, q = (ell - 1) % k, (ell - 1) // k + need(len(levels) == ell - 1 + int(any(flags)), "complete round count") + need(sum(b <= h < ell - 1 for h in levels) == q * k, "common root invocation count") + need(sum(len(selected(original, h)) for h in levels if h < b or h == ell - 1) + == sum(flags) + len(flags) * b, "prefix singleton inventory") + checked = 0 + for opposite in (False, True): + reference = cube + actual = reorder(cube, original, physical) + for h in reversed(levels) if opposite else levels: + reference = reference_round(reference, original, ell, flags, h, opposite) + actual = caller_round(actual, physical, ell, flags, k, h, opposite) + need(actual == reorder(reference, original, physical), "complete repaired round") + need(all(a * a + b0 * b0 <= 16 ** 2 for row in actual for a, b0 in row), + "complete-round disk return for p=4") + checked += 1 + results.append({"ell": ell, "long_axes": list(flags), "declared_layout_K": k, + "records": m, "coefficients": r, "complete_round_comparisons": checked, + "common_calls_each_direction": q * k, + "prefix_individual_sweeps_each_direction": sum(flags) + len(flags) * b}) + return results + + +def controls(): + ell, flags = 3, (False, False, False) + original, old = slots_for(ell, flags, 2) + _, new = slots_for(ell, flags, 1) + a = len(original) + need(a == 6 and 3 * 1 != a, "old descriptor extent must disagree") + impulse = [[(int(x == 0 and j == 0), 0) for j in range(1 << ell)] + for x in range(1 << a)] + # Scale by eight so the final truncation cannot hide the selected-bit error. + impulse[0][0] = (8, 0) + intended, den = h_fast(impulse, (0, 2, 4)) + concealed, bad_den = h_fast(impulse, (0, 1, 2)) + intended, concealed = truncate(intended, den), truncate(concealed, bad_den) + need(intended[2][0] == (0, 0) and concealed[2][0] == (1, 0), "wrong-root endpoint witness") + need(reorder(impulse, original, new) == impulse, "impulse origin invariant") + nonconstant = [[(x + j, 0) for j in range(1 << ell)] for x in range(1 << a)] + mapped = reorder(nonconstant, original, new) + need(reorder(mapped, old, original) != nonconstant, "old inverse layout control") + bad_offset, _ = h_fast(impulse, (1, 2, 3)) + good_offset, _ = h_fast(impulse, (0, 1, 2)) + need(bad_offset != good_offset, "offset control") + # Inverse order matters even though rounding commutes with the diagonal. + small_slots, _ = slots_for(2, (True,), 1) + one = [[(0, 0)] * 4 for _ in range(4)] + one[3][0] = (4, 0) + correct = reference_round(one, small_slots, 2, (True,), 1, True) + raw, d = h_fast(one, selected(small_slots, 1)) + wrong = diagonal(truncate(raw, d), small_slots, 2, (True,), 1, True) + need(correct != wrong, "inverse round order control") + need((-1) // 2 != -(1 // 2), "floor rounding is not odd") + need(truncate([[(-1, 1)]], 2) == [[(0, 0)]], "toward-zero control") + p = 4 + need(2 ** p > 2 ** ((p + 1) - 1) - 1, "p+1 misses positive disk endpoint") + need(-(2 ** (p + 1)) < -(2 ** p), "signed minimum outside caller disk") + return {"old_extent_bits": a, "wrong_active_extent_bits": 3, + "concealed_extent_witness_address": 2, + "correct_value": [0, 0], "wrong_value": [1, 0], + "rejected_failures": ["old chunk extent", "concealed extent wrong tensor", + "old inverse layout", "wrong offset", "inverse round order", + "floor rounding", "short signed format"]} + + +def load_frozen(name, filename, expected_blob): + path = HERE / filename + data = path.read_bytes() + blob = sha1(b"blob " + str(len(data)).encode() + b"\0" + data).hexdigest() + need(blob == expected_blob, "frozen source bytes: " + filename) + spec = importlib.util.spec_from_file_location(name, path) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module, {"path": filename, "git_blob": blob, "sha256": sha256(data).hexdigest()} + + +def actual_packet_boundary(): + producer, pp = load_frozen("audited_pr3593", "pr3593-controller.py", "2e72164d9429baeb1b18621f6f4b9576dbcc60a4") + consumer, cp = load_frozen("audited_pr3611", "pr3611-consumer.py", "d916056a4ae22d668ad3269ba881e4f518e982ab") + cap_controls = [rejected(lambda: producer.encode(33, 1, 0, (True,)), "bad ell"), + rejected(lambda: consumer.Consumer(33, 6), "allocation ell")] + ell, flags, k, h, p = 3, (False, False, False), 1, 1, 4 + original, physical = slots_for(ell, flags, k) + address = (1, 0, 0, 1, 0, 0) + x = int("".join(map(str, address)), 2) + r, w = 1 << ell, p + 2 + cube = [] + for index in range(1 << len(original)): + sign = -1 if bit_at(index, original, (0, h)) else 1 + cube.append([(sign * (j % 3 + 1), sign * (1 - j % 3)) for j in range(r)]) + raw, denominator = h_fast(reorder(cube, original, physical), selected(physical, h)) + complete_h = truncate(raw, denominator) + packet = complete_h[x] + need(any(a or b for a, b in packet), "nonzero complete-H packet") + before_packet = packet + receipts = [] + for opposite in (False, True): + descriptor = producer.encode(ell, k, h, flags, opposite) + ctrl = producer.Controller(descriptor, address) + ctrl.execute() + expected_e = exponent(x, physical, ell, flags, h, opposite) + actual_e = int("".join(map(str, ctrl.data["output"].cells)), 2) + need(actual_e == expected_e, "actual emitted matched-layout exponent") + prod_snapshot = ctrl.invoice() + prod_cost = (sum(sum(v.values()) for v in prod_snapshot["data"].values()) + + prod_snapshot["control_tape_actions"] + prod_snapshot["descriptor_actions"] + + sum(prod_snapshot["gates"].values())) + producer_bound = 5000 * (len(address) + ell + 1) ** 2 * (ell + k + h + len(flags) + 10) + need(prod_cost <= producer_bound, "actual producer tariff") + bits = [int(bit) for pair in packet for value in pair + for bit in format(value % (1 << w), "0%db" % w)] + source = consumer.Tape(["^"] + bits + ["$"]) + width = consumer.Tape(["^"] + ["1"] * w + ["$"]) + module = consumer.Consumer(ell, w) + borrowed = (ctrl.data["output"], ctrl.descriptor, width, source) + snapshots = [(list(t.cells), t.head) for t in borrowed] + observed_tapes = tuple(module.tapes.values()) + borrowed + counts_before = [sum(t.counts.values()) for t in observed_tapes] + result = module.run(*borrowed) + need([(list(t.cells), t.head) for t in borrowed] == snapshots, "actual borrow return") + output_bits = result.cells[1:1 + 2 * r * w] + values = [] + for j in range(0, len(output_bits), w): + v = int("".join(map(str, output_bits[j:j + w])), 2) + values.append(v - (1 << w) if v >> (w - 1) else v) + packet = list(zip(values[::2], values[1::2])) + need(packet == rotate(before_packet if not opposite else receipts[-1]["packet"], expected_e), + "actual packet endpoint") + need(all(not any(module.tapes[role].cells) and module.tapes[role].head == 0 + for role in ("prefix", "suffix", "word", "a", "b")), "actual private return") + consumer_cost = sum(module.invoice.values()) + observed_cost = sum(sum(t.counts.values()) - old for t, old in zip(observed_tapes, counts_before)) + observed_cost += sum(module.gates.values()) + need(consumer_cost == observed_cost, "independent shared-role action reconciliation") + need(consumer_cost <= 256 * (2 * r * w + ell + w + 1), "actual consumer tariff") + rearm_control = rejected(lambda: module.run(*borrowed), "one-shot consumer") + need([(list(t.cells), t.head) for t in borrowed] == snapshots, "one-shot rejection preserves borrows") + receipts.append({"opposite": opposite, "exponent": actual_e, "producer_tariff": prod_cost, + "producer_tariff_bound": producer_bound, "consumer_tariff": consumer_cost, + "consumer_actions_independently_reconciled": observed_cost, + "used_object_rejection": rearm_control, "packet": packet}) + need(packet == before_packet, "actual opposite packet return") + wrong = producer.Controller(producer.encode(ell, 2, h, flags), address) + wrong.execute() + wrong_e = int("".join(map(str, wrong.data["output"].cells)), 2) + need(wrong_e != receipts[0]["exponent"], "old-K actual header must differ") + return {"source_pins": [pp, cp], "arithmetic_H_only": True, + "whole_physical_root_or_diagonal_pass_executed": False, + "matched_layout_address": x, "wrong_K_exponent": wrong_e, "source_cap_rejections": cap_controls, + "actual_single_packet_calls": receipts} + + +def run(): + return {"scope": "source-relative matched outer layout; bounded arithmetic and two actual single-packet joins", + "floor_and_cost": floors_and_cost(), "complete_cube_checks": cube_checks(), + "controls": controls(), "actual_interface": actual_packet_boundary()} + + +if __name__ == "__main__": + print(json.dumps(run(), sort_keys=True, indent=2)) diff --git a/research/typed-actual-width-physical-h/physical_h.py b/research/typed-actual-width-physical-h/physical_h.py new file mode 100644 index 0000000000..1ff92d44bf --- /dev/null +++ b/research/typed-actual-width-physical-h/physical_h.py @@ -0,0 +1,595 @@ +"""Typed actual-width physical H and toward-zero rounded return. + +The machine below is the object under test. It is not the PR #3623 arithmetic +oracle. Successful calls are data-independent in every tape and gate count. +""" + +from __future__ import annotations + + +class Tape: + """Unit-seek bit tape. Counters start after presentation.""" + + def __init__(self, n): + if n < 0: + raise ValueError("tape length") + self.cells = [0] * n + self.head = 0 + self.read = 0 + self.write = 0 + self.move = 0 + + def seek(self, pos): + if not 0 <= pos <= len(self.cells): + raise ValueError("tape boundary") + self.move += abs(pos - self.head) + self.head = pos + + def read_bit(self): + if self.head >= len(self.cells): + raise ValueError("tape boundary") + self.read += 1 + return self.cells[self.head] + + def write_bit(self, bit): + if self.head >= len(self.cells) or bit not in (0, 1): + raise ValueError("tape boundary") + self.write += 1 + self.cells[self.head] = bit + + def scan_read(self, pos, n): + self.seek(pos) + out = [] + for i in range(n): + if i: + self.seek(pos + i) + out.append(self.read_bit()) + return out + + def scan_write(self, pos, bits): + self.seek(pos) + for i, bit in enumerate(bits): + if i: + self.seek(pos + i) + self.write_bit(bit) + + def poke(self, pos, bits): + for i, bit in enumerate(bits): + self.cells[pos + i] = bit + + +def bits_from_int(value, width): + if width < 1 or not isinstance(value, int): + raise ValueError("bit word") + if value < 0: + value = (1 << width) + value + if value < 0 or value >= 1 << width: + raise ValueError("bit word") + return [((value >> (width - 1 - i)) & 1) for i in range(width)] + + +def int_from_bits(bits): + width = len(bits) + value = 0 + for bit in bits: + value = (value << 1) | bit + if bits and bits[0]: + value -= 1 << width + return value + + +def add_bits(a, b, gates, cin=0): + width = len(a) + if len(b) != width or cin not in (0, 1): + raise ValueError("adder width") + carry = cin + out = [0] * width + for i in range(width - 1, -1, -1): + gates[0] += 1 + total = a[i] + b[i] + carry + out[i] = total & 1 + carry = total >> 1 + got = int_from_bits(out) + expect = int_from_bits(a) + int_from_bits(b) + cin + if got != expect: + raise ValueError("work width") + return out + + +def sub_bits(a, b, gates): + flipped = [1 - bit for bit in b] + gates[0] += len(b) + return add_bits(a, flipped, gates, cin=1) + + +def slots_for(ell, flags, k): + if not (ell >= 2 and flags and 1 <= k < ell): + raise ValueError("layout domain") + original = tuple((i, h) for i, long in enumerate(flags) + for h in range(ell - (not long) - 1, -1, -1)) + b, q = (ell - 1) % k, (ell - 1) // k + prefix = [(i, ell - 1) for i, long in enumerate(flags) if long] + prefix += [(i, h) for h in range(b - 1, -1, -1) for i in range(len(flags))] + chunks = [(i, h) for j in range(q) for i in range(len(flags)) + for h in range(ell - 2 - j * k, ell - 2 - (j + 1) * k, -1)] + changed = tuple(prefix + chunks) + if len(set(changed)) != len(original) or set(changed) != set(original): + raise ValueError("layout bijection") + return original, changed + + +def selected_bits(slots, h): + return tuple(len(slots) - 1 - j for j, item in enumerate(slots) if item[1] == h) + + +def bit_at(x, slots, named): + return (x >> (len(slots) - 1 - slots.index(named))) & 1 + + +def origin_of_target(before, after): + """original address x whose image is physical address y, matching reorder.""" + count = 1 << len(before) + origin = [None] * count + for x in range(count): + y = 0 + for name in after: + y = (y << 1) | bit_at(x, before, name) + origin[y] = x + if any(item is None for item in origin): + raise ValueError("layout bijection") + return tuple(origin) + + +def levels_for(ell, flags): + levels = list(range(ell - 2, -1, -1)) + if any(flags): + levels.insert(0, ell - 1) + return tuple(levels) + + +def trunc_pow2(value, g): + if g < 0: + raise ValueError("shift") + if value >= 0: + return value >> g + return -((-value) >> g) + + +def arithmetic_shift(value, g): + return value >> g + + +class TypedActualWidthH: + """One common or prefix round of matched-layout H, then Q_p. + + The borrowed cube is MSB-first two's complement of width w=p+2. + The root return is LSB-first. The consumer return is MSB-first. + Work width is W=p+g+2. Scratch is blanked. The object is one-shot. + """ + + def __init__(self, ell, flags, k, p): + flags = tuple(bool(item) for item in flags) + original, physical = slots_for(ell, flags, k) + self.ell = ell + self.flags = flags + self.k = k + self.p = p + if not isinstance(p, int) or p < 1: + raise ValueError("precision") + self.original = original + self.physical = physical + self.levels = levels_for(ell, flags) + self.w = p + 2 + self.used = False + + def matched_bits(self, h): + if h not in self.levels: + raise ValueError("round index") + axes = len(self.flags) + owned = sum(self.flags) + b, q = (self.ell - 1) % self.k, (self.ell - 1) // self.k + address_bits = len(self.physical) + if b <= h < self.ell - 1: + j, rho = (self.ell - 2 - h) // self.k, (h - b) % self.k + left = owned + axes * b + j * axes * self.k + right = (q - j - 1) * axes * self.k + if left + axes * self.k + right != address_bits: + raise ValueError("complete root extent") + bits = tuple(right + rho + t * self.k for t in range(axes)) + literal = selected_bits(self.physical, h) + if tuple(sorted(bits)) != tuple(sorted(literal)) or len(bits) != len(literal): + raise ValueError("literal root selected positions") + return bits + return selected_bits(self.physical, h) + + def require_bits(self, h, bits): + if tuple(bits) != self.matched_bits(h): + raise ValueError("selected-bit descriptor") + return self.matched_bits(h) + + def run(self, cube, h, source_order="physical"): + if self.used: + raise ValueError("one-shot physical H") + self.used = True + bits = self.matched_bits(h) + if source_order not in ("physical", "original"): + raise ValueError("source order") + g = len(bits) + width = self.w + work = self.p + g + 2 + records = 1 << len(self.physical) + coeffs = 1 << self.ell + if len(cube) != records: + raise ValueError("record count") + bound = 1 << self.p + for row in cube: + if len(row) != coeffs: + raise ValueError("coefficient count") + for real, imag in row: + if not isinstance(real, int) or not isinstance(imag, int): + raise ValueError("numerator") + if abs(real) > bound or abs(imag) > bound: + raise ValueError("unit disk") + source_slots = self.physical if source_order == "physical" else self.original + origin = origin_of_target(source_slots, self.physical) + sw = coeffs * 2 * width + source = Tape(records * sw) + scratch = Tape(records * coeffs * 2 * work) + root = Tape(records * sw) + consumer = Tape(records * sw) + gates = [0] + for x, row in enumerate(cube): + _present_record(source, x * sw, row, width) + invoice_before = (source.read, source.write, source.move) + self._layout(source, scratch, origin, records, coeffs, width, work, gates) + if (source.read, source.write, source.move) == invoice_before: + raise ValueError("layout was not charged") + for beta in bits: + self._butterfly(scratch, records, coeffs, work, beta, gates) + scratch.seek(0) + decoded = self._round_and_bridge( + scratch, root, consumer, records, coeffs, width, work, g, gates) + self._blank(scratch) + source.seek(0) + root.seek(0) + consumer.seek(0) + if source.cells != _presented_cells(cube, width): + raise ValueError("borrowed source") + if any(scratch.cells) or scratch.head or root.head or consumer.head or source.head: + raise ValueError("head return") + shadow = _integer_h(cube, origin, bits) + if decoded != shadow: + raise ValueError("rounded return") + ledger = { + "read": source.read + scratch.read + root.read + consumer.read, + "write": source.write + scratch.write + root.write + consumer.write, + "move": source.move + scratch.move + root.move + consumer.move, + "gate": gates[0], + } + return decoded, ledger, { + "records": records, + "coefficients": coeffs, + "selected_bits": bits, + "work_width": work, + "packet_width": width, + } + + def _layout(self, source, scratch, origin, records, coeffs, width, work, gates): + sw = coeffs * 2 * width + rw = coeffs * 2 * work + bound = 1 << self.p + for y in range(records): + packed = source.scan_read(origin[y] * sw, sw) + extended = [] + for index in range(coeffs * 2): + word = packed[index * width:(index + 1) * width] + value = int_from_bits(word) + gates[0] += 1 + if abs(value) > bound: + raise ValueError("unit disk") + sign = word[0] + extended.extend([sign] * (work - width)) + gates[0] += work - width + extended.extend(word) + scratch.scan_write(y * rw, extended) + source.seek(0) + scratch.seek(0) + + def _butterfly(self, scratch, records, coeffs, work, beta, gates): + """Move address bit beta to adjacent pairs, butterfly, and merge back. + + Every pass is a sequential scan. Partners are the records that differ + only in bit beta, written back as sum on the clear bit and difference + on the set bit. + """ + rw = coeffs * 2 * work + low = Tape((records // 2) * rw) + high = Tape((records // 2) * rw) + paired = Tape(records * rw) + low_n = high_n = 0 + for x in range(records): + record = scratch.scan_read(x * rw, rw) + gates[0] += 1 + if (x >> beta) & 1: + high.scan_write(high_n * rw, record) + high_n += 1 + else: + low.scan_write(low_n * rw, record) + low_n += 1 + if low_n != records // 2 or high_n != records // 2: + raise ValueError("address split") + scratch.seek(0) + low.seek(0) + high.seek(0) + for index in range(records // 2): + left = low.scan_read(index * rw, rw) + right = high.scan_read(index * rw, rw) + paired.scan_write((2 * index) * rw, left) + paired.scan_write((2 * index + 1) * rw, right) + low.seek(0) + high.seek(0) + paired.seek(0) + _adjacent_butterfly(paired, records, coeffs, work, gates) + paired.seek(0) + for index in range(records // 2): + left = paired.scan_read((2 * index) * rw, rw) + right = paired.scan_read((2 * index + 1) * rw, rw) + low.scan_write(index * rw, left) + high.scan_write(index * rw, right) + low.seek(0) + high.seek(0) + paired.seek(0) + low_n = high_n = 0 + for x in range(records): + gates[0] += 1 + if (x >> beta) & 1: + record = high.scan_read(high_n * rw, rw) + high_n += 1 + else: + record = low.scan_read(low_n * rw, rw) + low_n += 1 + scratch.scan_write(x * rw, record) + scratch.seek(0) + low.seek(0) + high.seek(0) + paired.seek(0) + for tape in (low, high, paired): + _blank_tape(tape) + if any(tape.cells) or tape.head: + raise ValueError("auxiliary return") + # Auxiliary invoices are part of this round. Fold them into scratch's + # counters so the caller ledger stays four tapes plus these locals. + for tape in (low, high, paired): + scratch.read += tape.read + scratch.write += tape.write + scratch.move += tape.move + + def _round_and_bridge(self, scratch, root, consumer, records, coeffs, width, work, g, gates): + decoded = [] + for record in range(records): + row = [] + for coeff in range(coeffs): + pair = [] + for part in range(2): + index = (record * coeffs + coeff) * 2 + part + word = scratch.scan_read(index * work, work) + signed = _q_component(word, g, width, gates) + root.scan_write(index * width, list(reversed(signed))) + consumer.scan_write(index * width, signed) + pair.append(int_from_bits(signed)) + row.append((pair[0], pair[1])) + decoded.append(row) + return decoded + + def _blank(self, scratch): + scratch.seek(0) + for pos in range(len(scratch.cells)): + if pos: + scratch.seek(pos) + scratch.write_bit(0) + scratch.seek(0) + + +def _present_record(tape, pos, row, width): + bits = [] + for real, imag in row: + bits.extend(bits_from_int(real, width)) + bits.extend(bits_from_int(imag, width)) + tape.poke(pos, bits) + + +def _presented_cells(cube, width): + bits = [] + for row in cube: + for real, imag in row: + bits.extend(bits_from_int(real, width)) + bits.extend(bits_from_int(imag, width)) + return bits + + +def _blank_tape(tape): + tape.seek(0) + for pos in range(len(tape.cells)): + if pos: + tape.seek(pos) + tape.write_bit(0) + tape.seek(0) + + +def _adjacent_butterfly(paired, records, coeffs, work, gates): + rw = coeffs * 2 * work + for index in range(records // 2): + left = 2 * index + right = left + 1 + rec_a = paired.scan_read(left * rw, rw) + rec_b = paired.scan_read(right * rw, rw) + out_a, out_b = _mix(rec_a, rec_b, coeffs, work, gates) + paired.scan_write(left * rw, out_a) + paired.scan_write(right * rw, out_b) + paired.seek(0) + + +def _mix(rec_a, rec_b, coeffs, work, gates): + out_a, out_b = [], [] + for index in range(coeffs * 2): + a = rec_a[index * work:(index + 1) * work] + b = rec_b[index * work:(index + 1) * work] + out_a.extend(add_bits(a, b, gates, cin=0)) + out_b.extend(sub_bits(a, b, gates)) + return out_a, out_b + + +def _q_component(word, g, width, gates): + sign = word[0] + magnitude = [bit ^ sign for bit in word] + gates[0] += len(word) + magnitude = add_bits(magnitude, [0] * len(word), gates, cin=sign) + if int_from_bits(magnitude) < 0: + raise ValueError("magnitude") + narrowed = magnitude[:width] + if int_from_bits(narrowed) != int_from_bits(magnitude) >> g: + raise ValueError("shift wiring") + signed = [bit ^ sign for bit in narrowed] + gates[0] += width + return add_bits(signed, [0] * width, gates, cin=sign) + + +def _integer_h(cube, origin, bits): + records = [list(cube[origin[y]]) for y in range(len(origin))] + for beta in bits: + half = 1 << beta + span = half << 1 + block = 0 + while block < len(records): + for offset in range(half): + left, right = block + offset, block + offset + half + mixed_l, mixed_r = [], [] + for (ar, ai), (br, bi) in zip(records[left], records[right]): + mixed_l.append((ar + br, ai + bi)) + mixed_r.append((ar - br, ai - bi)) + records[left], records[right] = mixed_l, mixed_r + block += span + denom = 1 << len(bits) + return [[(trunc_pow2(real, len(bits)), trunc_pow2(imag, len(bits))) + for real, imag in row] for row in records] + + +def closed_read_write_gate(records, coeffs, g, p): + """Data-independent read, write and gate totals for one successful call. + + Layout reads each source bit once and writes the sign-extended work image. + Each selected bit then uses five sequential work-length copies (split, + interleave, adjacent butterfly, deinterleave, merge) and blanks the two + half tapes plus the paired tape. Q_p reads the work image once and writes + the LSB root word and the MSB consumer word. The work tape is blanked + last. Gates are the sign fan-out, one disk test per component, two address + tests per record per selected bit, three width-W add/invert steps per + butterfly component pair, and the abs/resign pair. + """ + work = p + g + 2 + width = p + 2 + components = records * coeffs * 2 + work_bits = components * work + reads = components * width + g * 5 * work_bits + work_bits + writes = (work_bits + g * 7 * work_bits + + 2 * components * width + work_bits) + gates = (components * (work - width) + components + + g * 2 * records + + g * (components // 2) * 3 * work + + components * (2 * work + 2 * width)) + return {"read": reads, "write": writes, "gate": gates} + + +def itinerary_moves(records, coeffs, g, p, origin, betas): + """Head travel of the successful-call schedule. Ignores coefficient values.""" + work = p + g + 2 + width = p + 2 + sw = coeffs * 2 * width + rw = coeffs * 2 * work + moves = 0 + head_s = 0 + head_w = 0 + + def seek(head, pos): + return head, abs(pos - head) + + for y in range(records): + pos = origin[y] * sw + head_s, delta = seek(head_s, pos) + moves += delta + if sw > 1: + moves += sw - 1 + head_s = pos + sw - 1 + posw = y * rw + head_w, delta = seek(head_w, posw) + moves += delta + if rw > 1: + moves += rw - 1 + head_w = posw + rw - 1 + if len(betas) != g: + raise ValueError("selected-bit count") + moves += abs(0 - head_s) + moves += abs(0 - head_w) + for _beta in betas: + moves += _linear_level_moves(records, rw) + # Q_p sequential scans. Work, root and consumer each start at 0. + work_bits = records * rw + packet_bits = records * sw + moves += _scan_moves(work_bits) # read work + moves += _scan_moves(packet_bits) # write root + moves += _scan_moves(packet_bits) # write consumer + if work_bits: + moves += work_bits - 1 # rewind work from its last bit + if packet_bits: + moves += 2 * (packet_bits - 1) # rewind root and consumer + # Blank from 0 across the work tape and rewind. + moves += _scan_moves(work_bits) + if work_bits: + moves += work_bits - 1 + # Final source/root/consumer seeks are already at 0. Caller seeks source + # home at layout end. run() seeks source, root and consumer to 0 again. + return moves + + +def _scan_moves(n): + """Moves while scanning n contiguous bits starting at the current origin 0.""" + if n <= 1: + return 0 + return n - 1 + + +def _level_moves(records, rw, beta): + """In-place pair schedule plus the homing seek back to 0.""" + moves = 0 + head = 0 + half = 1 << beta + span = half << 1 + block = 0 + while block < records: + for offset in range(half): + for rec in (block + offset, block + offset + half, + block + offset, block + offset + half): + pos = rec * rw + moves += abs(pos - head) + head = pos + if rw > 1: + moves += rw - 1 + head = pos + rw - 1 + block += span + moves += abs(0 - head) + return moves + + +def _scan_and_home(n): + """Forward scan from cell 0, then rewind to 0.""" + if n <= 1: + return 0 + return 2 * (n - 1) + + +def _linear_level_moves(records, rw): + """Five sequential passes, one adjacent butterfly, and auxiliary blanking.""" + length = records * rw + half = length // 2 + adjacent = _level_moves(records, rw, 0) + return (5 * _scan_and_home(length) + 10 * _scan_and_home(half) + adjacent) diff --git a/research/typed-actual-width-physical-h/verify.py b/research/typed-actual-width-physical-h/verify.py new file mode 100644 index 0000000000..db936346f2 --- /dev/null +++ b/research/typed-actual-width-physical-h/verify.py @@ -0,0 +1,178 @@ +#!/usr/bin/env python3 +"""Replay the typed actual-width physical H against the frozen PR #3623 tensor.""" + +from hashlib import sha1, sha256 +import importlib.util +import json +from pathlib import Path + +import physical_h + +HERE = Path(__file__).resolve().parent +FROZEN = HERE / "frozen" / "pr3623-check_join.py" +FROZEN_SHA256 = "33f91624d60be8c7124ecc24be073f8a5a3759b671979b6a17a6e26538f4355e" +FROZEN_BLOB = "421ae05f081ec37e4c5fa0b1b7e200a1578ab16d" +RECEIPT_PATH = HERE / "RECEIPT.json" + +CASES = ( + (2, (False,), 1), + (2, (True,), 1), + (3, (False, False), 1), + (3, (True, False), 1), + (3, (True, True), 1), + (3, (False, False, False), 1), + (3, (True, False, True), 1), + (3, (False, False, False, False), 2), + (3, (True, False, False, False), 2), + (4, (True, False), 2), +) + + +def need(condition, reason): + if not condition: + raise ValueError(reason) + + +def rejected(call, reason): + try: + call() + except ValueError as error: + need(str(error) == reason, "unexpected rejection: " + str(error)) + return reason + raise ValueError("missing rejection: " + reason) + + +def load_frozen(): + data = FROZEN.read_bytes() + digest = sha256(data).hexdigest() + blob = sha1(b"blob " + str(len(data)).encode() + b"\0" + data).hexdigest() + need(digest == FROZEN_SHA256, "frozen sha256") + need(blob == FROZEN_BLOB, "frozen git blob") + spec = importlib.util.spec_from_file_location("pr3623_check_join", FROZEN) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +def cube_for(ell, original): + records = 1 << len(original) + coeffs = 1 << ell + return [[((17 * x + 5 * j + 3) % 7 - 3, (11 * x + 7 * j + 2) % 7 - 3) + for j in range(coeffs)] for x in range(records)] + + +def run_cases(frozen): + rows = [] + totals = {"read": 0, "write": 0, "move": 0, "gate": 0} + widths = set() + for ell, flags, k in CASES: + original, physical = physical_h.slots_for(ell, flags, k) + need((original, physical) == frozen.slots_for(ell, flags, k), "layout pin") + cube = cube_for(ell, original) + for order in ("physical", "original"): + source = cube if order == "original" else frozen.reorder(cube, original, physical) + for h in physical_h.levels_for(ell, flags): + machine = physical_h.TypedActualWidthH(ell, flags, k, 4) + decoded, ledger, info = machine.run(source, h, source_order=order) + bits = info["selected_bits"] + need(bits == machine.matched_bits(h), "descriptor") + physical_cube = source if order == "physical" else frozen.reorder( + source, original, physical) + raw, _den = frozen.h_direct(physical_cube, bits) + need(decoded == frozen.truncate(raw, _den), "tensor return") + closed = physical_h.closed_read_write_gate( + info["records"], info["coefficients"], len(bits), 4) + need({key: ledger[key] for key in closed} == closed, "read write gate bill") + slots = machine.original if order == "original" else machine.physical + origin = physical_h.origin_of_target(slots, machine.physical) + moves = physical_h.itinerary_moves( + info["records"], info["coefficients"], len(bits), 4, origin, bits) + need(ledger["move"] == moves, "head itinerary") + need(rejected(lambda: machine.run(source, h, source_order=order), + "one-shot physical H") == "one-shot physical H", "one-shot") + for key in totals: + totals[key] += ledger[key] + widths.add(len(bits)) + rows.append({ + "ell": ell, + "flags": list(flags), + "K": k, + "h": h, + "order": order, + "bits": list(bits), + "records": info["records"], + "ledger": ledger, + }) + return rows, totals, sorted(widths) + + +def negative_and_rejections(): + machine = physical_h.TypedActualWidthH(2, (False,), 1, 4) + h = machine.levels[0] + need(machine.matched_bits(h) == (0,), "single selected bit") + coeffs = 1 << 2 + cube = [[(0, 0) for _ in range(coeffs)] for _ in range(2)] + cube[1][0] = (1, 0) + decoded, ledger, _info = machine.run(cube, h, source_order="physical") + need(decoded[0][0] == (0, 0) and decoded[1][0] == (0, 0), "toward-zero witness") + need(physical_h.arithmetic_shift(-1, 1) == -1, "arithmetic shift stays negative") + need(physical_h.trunc_pow2(-1, 1) == 0, "toward zero clears the odd numerator") + signed = physical_h.bits_from_int(1, 6) + lsb, msb = list(reversed(signed)), list(signed) + need(physical_h.int_from_bits(msb) == 1, "msb consumer word") + need(physical_h.int_from_bits(lsb) != 1, "skipping the bridge changes the integer") + need(physical_h.int_from_bits(list(reversed(lsb))) == 1, "bridge restores the integer") + old = physical_h.TypedActualWidthH(3, (False, False, False), 1, 4) + descriptor = rejected(lambda: old.require_bits(1, (0, 1, 2)), "selected-bit descriptor") + disk_machine = physical_h.TypedActualWidthH(2, (False,), 1, 4) + bad = [[(0, 0) for _ in range(4)] for _ in range(2)] + bad[0][0] = (17, 0) + disk = rejected(lambda: disk_machine.run(bad, disk_machine.levels[0]), "unit disk") + need(physical_h._level_moves(2, 1, 0) == 4, "hand-checked adjacent pair") + need(physical_h._linear_level_moves(2, 1) == 14, "hand-checked linear level") + failures = 0 + for g in range(0, 7): + work = 4 + g + 2 + width = 6 + for value in range(-(1 << (4 + g)), (1 << (4 + g)) + 1): + gates = [0] + out = physical_h._q_component(physical_h.bits_from_int(value, work), g, width, gates) + if physical_h.int_from_bits(out) != physical_h.trunc_pow2(value, g): + failures += 1 + need(failures == 0, "Q_p range") + return { + "negative_output": [list(decoded[0][0]), list(decoded[1][0])], + "negative_ledger": ledger, + "arithmetic_shift_of_minus_one": -1, + "old_descriptor": descriptor, + "disk": disk, + "adjacent_pair_moves": 4, + "linear_level_moves_m2_rw1": 14, + "q_range_failures": failures, + } + + +def digest(rows): + payload = json.dumps(rows, sort_keys=True, separators=(",", ":")).encode() + return sha256(payload).hexdigest() + + +def main(): + frozen = load_frozen() + rows, totals, widths = run_cases(frozen) + controls = negative_and_rejections() + receipt = { + "pass_token": "PASS_TYPED_ACTUAL_WIDTH_PHYSICAL_H", + "calls": len(rows), + "selected_bit_widths": widths, + "totals": totals, + "digest_sha256": digest(rows), + "controls": controls, + } + expected = json.loads(RECEIPT_PATH.read_text(encoding="utf-8")) + need(receipt == expected, "receipt mismatch") + print("PASS_TYPED_ACTUAL_WIDTH_PHYSICAL_H") + + +if __name__ == "__main__": + main() From 83db51a76b57f3f70f566d96af4f5eb786d7b880 Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Tue, 20 Oct 2026 02:36:54 +0000 Subject: [PATCH 2/2] Note the parallel arithmetic H invoice beside this tape bill. PR #4123 answers the same handoff with add/sub and bit counts. This package prices the one-shot tape itinerary instead. Co-authored-by: unpaidmoon --- research/typed-actual-width-physical-h/README.md | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/research/typed-actual-width-physical-h/README.md b/research/typed-actual-width-physical-h/README.md index 9ec15c5fbb..bb713d755b 100644 --- a/research/typed-actual-width-physical-h/README.md +++ b/research/typed-actual-width-physical-h/README.md @@ -79,3 +79,17 @@ PR #3493 / #3593 / #3599 / #3611 sources credited there. The handoff is discussion #1166 comment 19016699. New tape schedule, bill and checks by unpaidmoon, with substantial assistance from Grok 4.7 in Cursor. No independent human or formal-kernel acceptance is claimed. Apache-2.0. + +## Relation to the parallel arithmetic invoice + +While this package was being checked, the same account posted a different +one-round answer to comment 19016699: discussion comment 19056745 and +upstream PR #4123 (`research/typed-actual-width-h`, head +`499427578245cbd3d2b07680945a94f6e927d020`). That invoice counts normalized +`H0` add/sub operations, truncations and bit touches, and proves a Euclidean +error below `sqrt(2) 2^{-p}`. This package does not repeat that count. It +prices the unnormalized butterfly as a one-shot tape program: sequential +split, interleave, adjacent butterfly, deinterleave and merge, then +toward-zero division by `2^g`, with a closed read/write/gate form and a +data-independent head itinerary. The two artifacts can be reviewed +separately. Neither prices inter-round stock or the PR #3617 diagonal.