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..bb713d755b --- /dev/null +++ b/research/typed-actual-width-physical-h/README.md @@ -0,0 +1,95 @@ +# 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. + +## 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. 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()