diff --git a/research/complex-signed-digit/CLAIM.md b/research/complex-signed-digit/CLAIM.md new file mode 100644 index 0000000000..ae283cbd11 --- /dev/null +++ b/research/complex-signed-digit/CLAIM.md @@ -0,0 +1,43 @@ +# Sprint claim + +- Track: complex supplier. OS assignment seed: **36**, drawn with + `secrets.randbelow(100)` on 2026-10-13. +- Base: `66849e1475c930fd7732b1a0067ffee7e1e95f60`. +- Selected result: #626 with #543, conditional + `kappa = 51110230636731/31250000000000000`. +- Object: signed-digit preparation of non-unit dyadic additions in the selected + JP8 emitted scalar programs. Seed 36 selects JP8, index `36 % 2` in the ordered + candidate list `[jp8, ck]`; both orientations of that provider are in scope. +- Method: exact non-adjacent signed digits, explicit source copies, doublings, + signed source accumulation, halvings, target accumulation and scratch clear. + Compare complete cost and actual intermediate coefficients with the pinned + binary-Horner invoice. Accept only strictly cheaper numerator circuits. +- Deliverable: bounded finite circuit improvement or scoped negative result, + executable exact checker, source pins, negative controls, and a cost receipt. +- Expected finish: 2026-10-13 05:16 UTC. Final quarter reserved for verification + and submission. + +Three candidates were inspected: coordinate-total factory resynthesis, single +K-triangle read relocation, and signed-digit coefficient preparation. #681 +already resynthesizes a factory; #687 exhausts a read-relocation neighborhood. +The third is chosen. #696 improves copy and unit-coefficient handling while +retaining binary Horner for non-unit numerators; this claim concerns numerator +recoding and will measure its incremental effect separately. #411 introduced +paid dyadic lowering in the earlier supplier lineage. None of these pending +PRs is an implementation dependency. + +No pinned coordination issue exists. This local claim substitutes for an issue +comment. Live PR metadata was checked immediately before creating this file. +No selected certificate, source construction, global invoice, or `upstream/` +file will be changed. New kappa, full theorem formalization, and runtime +performance are outside the claim. + +## Completed result + +Submitted [PR #723](https://github.com/CrocSwap/integer-mult-bounds/pull/723). +The exact finite recipe saves 3,276 real-component primitives per JP8 +orientation, with 250 changed additions each. Both 716-column scalar +projections and nine negative controls pass. The recomputed forward envelope +increases slightly, while the 64/101-bit local bounds remain unchanged. +The selected-record check passes. No new kappa is claimed. See EXPECTED.json +and VALIDATION.md for the exact evidence, final overlap check and limits. diff --git a/research/complex-signed-digit/EXPECTED.json b/research/complex-signed-digit/EXPECTED.json new file mode 100644 index 0000000000..30493f0b5c --- /dev/null +++ b/research/complex-signed-digit/EXPECTED.json @@ -0,0 +1,50 @@ +{ + "status": "PASS_COMPLEX_SIGNED_DIGIT", + "provider": "jp8", + "assignment_seed": 36, + "programs": { + "forward": { + "events": 27909, + "scalar_macros": 22693, + "scalar_projection_columns": 716, + "distinct_signed_coefficients": 439, + "changed_additions": 250, + "changed_with_scratch_overshoot": 100, + "real_primitives_before": 257232, + "real_primitives_after": 253956, + "saved_real_primitives": 3276, + "prefix_l1_before": "4536094588619580433782972610869617/281474976710656", + "prefix_l1_after": "567011840215747740443164774152233/35184372088832", + "prefix_bits_before": 64, + "prefix_bits_after": 64, + "charged_local_payload_bits": 192, + "paid_profile": {"1": 2512, "2": 400, "3": 448, "4": 160, "5": 70, "6": 8, "8": 8}, + "changed_recipe_sha256": "df20effd3ea4af19ab29097ab493bd35d79c82956b99c753cd60b89641fe613a", + "coefficient_census_sha256": "544b272fc59cfcdc21e4dac39b9a9d2b9abd94b96ba913fc5de50975e3446535" + }, + "backward": { + "events": 27909, + "scalar_macros": 22693, + "scalar_projection_columns": 716, + "distinct_signed_coefficients": 439, + "changed_additions": 250, + "changed_with_scratch_overshoot": 100, + "real_primitives_before": 257280, + "real_primitives_after": 254004, + "saved_real_primitives": 3276, + "prefix_l1_before": "16753412757380464429924108070201913461/8388608", + "prefix_l1_after": "16753412757380464429924108070201913461/8388608", + "prefix_bits_before": 101, + "prefix_bits_after": 101, + "charged_local_payload_bits": 192, + "paid_profile": {"1": 2512, "2": 400, "3": 448, "4": 160, "5": 70, "6": 8, "8": 8}, + "changed_recipe_sha256": "3de925ea4c6bfeac0e7a81b3647defd0199066ed1df93e1a40013db3d61a711c", + "coefficient_census_sha256": "118f38bcbcd005fae2438743e3e23932a5a4478731a6c038b94182a3258a4128" + } + }, + "negative_controls": [ + "wrong_signed_digit", "missing_initial_clear", "missing_final_clear", + "missing_target_accumulation", "missing_halving", "nondyadic", "zero", + "undercharged_scratch", "target_excursion" + ] +} diff --git a/research/complex-signed-digit/README.md b/research/complex-signed-digit/README.md new file mode 100644 index 0000000000..72b386d3b4 --- /dev/null +++ b/research/complex-signed-digit/README.md @@ -0,0 +1,187 @@ +# Signed-digit preparation in the selected JP8 supplier + +**Finite local circuit improvement / research note. No new kappa.** + +Signed-digit numerator preparation saves **3,276 real-component primitives in +each orientation** of the selected JP8 supplier. It changes 250 additions per +orientation. Every source read, doubling, signed accumulation, halving and +scratch clear is charged. The original initial clear and leading source add +are retained. + +| JP8 orientation | Original real primitives | With numerator recoding | Saved | +| --- | ---: | ---: | ---: | +| Forward | 257,232 | 253,956 | 3,276 | +| Backward | 257,280 | 254,004 | 3,276 | + +These are scalar primitive counts, not measured runtimes or total recursive +costs. The paid child profile remains +`{1:2512, 2:400, 3:448, 4:160, 5:70, 6:8, 8:8}`. +The source/helper count, scalar macro word, frames, adapters, phases and +restoration boundaries are unchanged. The selected conditional result remains +`kappa = 51110230636731/31250000000000000` from #626 with #543. + +## Reproduce + +From the repository root, with Python 3.11 or later and the standard library: + +```sh +python3 -I -B research/complex-signed-digit/verify.py +``` + +Expected: + +```text +PASS_COMPLEX_SIGNED_DIGIT jp8 additions=250+250 real_saved=3276+3276 columns=716 controls=9 +``` + +The command is offline and writes no files. It checks all input byte and Git +blob pins, also checks decompressed payload hashes, replays the circuits with +an exact rational interpreter, reconstructs the 716-column scalar projection +in both orientations, recounts costs and intermediate envelopes, and compares +the complete result with [EXPECTED.json](EXPECTED.json). +`--report` performs the same calculations and controls and prints the receipt +without comparing it to EXPECTED.json. + +The executable recipe is [lowering.py](lowering.py). For every scalar add +`t += q*s`, `circuit(q)` returns a literal real primitive list over distinct +registers `t`, `s`, and private `w`. Apply that list to both real components, +in the original event's frame. Other scalar and non-scalar events stay intact. +The receipt hashes the ordered list of changed event indices, exact rational +coefficients and primitive lists, separately for each orientation. + +## Cost and boundary argument + +Write a nonzero dyadic coefficient as `q = sign * a / 2^k`, with positive +integer `a`. The original circuit costs + +`3 + floor(log2(a)) + popcount(a) + k` + +real primitives per component. The three fixed operations are initial scratch +clear, signed target accumulation, and final scratch clear. Binary numerator +preparation accounts for every doubling and source add. The proposed circuit +uses most-significant-first digits in `{-1,0,1}` and costs + +`3 + (digit_length - 1) + nonzero_digits + k`. + +It uses signed digits only when this complete cost is strictly smaller; +otherwise it emits the original binary circuit. This comparison includes an +extra leading digit when recoding introduces one. No minimal-circuit or global +optimality claim is made. + +The recoding step chooses `d=0` for even `a`, `d=1` for `a=1 mod 4`, and +`d=-1` for `a=3 mod 4`, then replaces `a` by `(a-d)/2`. Each step preserves +the represented integer and decreases it until zero. Reading the resulting +digits backwards and applying `w <- 2w + d*s` therefore produces `a*s`. +The `k` halvings produce `abs(q)*s`, the single final signed accumulation +produces `t+q*s`, and clearing `w` removes the private value. The initial +clear makes the circuit independent of arbitrary incoming scratch. The +source is never written. + +All operations before target accumulation affect only scratch, at the +existing scalar event's frame. Thus the replacement has the same complete +three-register boundary map. Substitution through the ordered program +preserves every scalar boundary on arbitrary correlated input, including +dirty helper restoration. It inserts no frame change, child call, source +adapter, centre copy, or residual wrapper. It uses the same private coefficient +stream as binary Horner. The exact three-column interpreter checks this +identity for every coefficient that occurs, with explicit private input. + +## Intermediate magnitudes must be repriced + +Signed recoding sometimes reaches `a+1` before subtracting the source. The +exact maximum scratch coefficient for the signed-digit numerator is `a+1` +when `a=3 mod 4`, and `a` otherwise. To prove it, write `a=2m+d`. The +most-significant-first execution computes `m`, doubles it, then adds `d`, +so `M(a)=max(M(m),2m,a)`, with `M(1)=1`. Induction gives the stated bound; +every intermediate coefficient is nonnegative. Halving cannot increase it. +Binary circuits retained by the cost comparison have maximum `a`. + +The checker interprets all primitive prefixes to obtain the actual maximum, +then multiplies it by the source's exact rational L1 envelope at that event. +Macro-boundary envelopes use `env[t] + abs(q)*env[s]` in both versions. This +uses the exact same-source correlation inside coefficient preparation; it +does not replace subtraction with an unsigned accumulation. The syntax check +rejects any extra target excursion that would invalidate this argument. + +There are 100 changed macros with scratch overshoot per orientation. The +forward maximum increases at zero-based event 27551, +`L353 += (-34078711/4)*L355`, frame 1: + +| Envelope | Exact value | +| --- | --- | +| Original forward | `4536094588619580433782972610869617/281474976710656` | +| New forward | `567011840215747740443164774152233/35184372088832` | +| Backward, both circuits | `16753412757380464429924108070201913461/8388608` | + +The forward inflation factor is exactly `34078712/34078711`. Its bit bound +stays 64; backward stays 101. Both fit the retained 192-bit local allowance. +The old exact forward prefix receipt must be updated if this lowering is +integrated. This package does not overwrite that receipt. + +## Completed coverage and limits + +This is deterministic synthesis over the two pinned JP8 programs, not a +random or open-ended search. Assignment seed 36 selects JP8 as recorded in +[CLAIM.md](CLAIM.md). The domain is all 27,909 events per orientation, including +22,693 scalar events and 439 distinct signed addition coefficients. The +stopping rule is completion of both programs; all were processed. Exactly +188 distinct signed coefficients per orientation receive cheaper circuits. +The largest absolute coefficient is 67,108,862. The per-component saving is +at most 22 primitives per changed macro. + +Nine controls reject a wrong signed digit, omitted initial or final clear, +omitted target accumulation, omitted halving, nondyadic and zero coefficients, +an undercharged scratch peak, and an endpoint-neutral target excursion. +The full scalar projection check is an additional exact finite check. It +does not independently replay Clifford amplitudes, geometry, or physical +hosting. Those operations are inherited and unchanged. + +No selected emitter, global invoice, certificate, or `upstream/` file is +modified. This does not supply new owner maps or a revised asymptotic +recurrence. All-size compilation, common-label and mutable-basis realization, +pooled hosting, residual normalization, rounded arithmetic and precision, +tape/exact recovery, analytic transfer and the bit H1-H5 assumptions remain. +Finite replay is not a formal proof of the full multiplication theorem. + +## Provenance and concurrent work + +Exact base: `66849e1475c930fd7732b1a0067ffee7e1e95f60`. +The selected #626 source head is `660de893d27bb7abd1d5b01b1640207528a5c851`, +with #622 at `f69477f4f6d3c7eb1f740b166881bffed4ffa9f6`. +[SOURCES.json](SOURCES.json) pins every consumed repository input by SHA-256 +and Git blob, with additional decompressed payload pins for gzip artifacts. +The retained compressed inputs are immutable sources; no recompression is +used as a mathematical comparison. + +Credit to Jeremy Kothe and the Claude Code contributors for #622's supplier, +Chafik Boukhalfa for #626's packaging and owner repair, icekylinx for the +#425/#433/#531 scalar-emission lineage, DreamingOfClouds for the native and +emitted verification lineage, Dugongue for the scalar and rank-sector work, +and eumemic for the selected #543 bit supplier and earlier #411 dyadic +lowering. Their original notices remain in the source packages. + +Concurrent [#696](https://github.com/CrocSwap/integer-mult-bounds/pull/696), +head `5a3f983715027c4fd83f50bc9001d4b18463bed1`, removes the initial +clear/add pair in favor of a copy and specializes unit coefficients. It +retains binary digits for non-unit numerators. This contribution retains +that original pair and all unit circuits to isolate the additional +numerator-recoding saving. Copy initialization would reduce binary and +signed-digit costs equally, so the 3,276-primitives difference per orientation +persists under composition, but this package does not implement or certify +that combined package. #681 changes a factory macro word; #687 examines a +K-triangle frame neighborhood. None is an implementation dependency. + +Concurrent [#722](https://github.com/CrocSwap/integer-mult-bounds/pull/722), +by @ellipsi2 at `a0766ab0fab379e1997fadc3ca157578d57986c1`, arrived between +the final overlap snapshot and submission. It shares binary-Horner preparation +across forward cleanup runs, changing private-work clearing to block boundaries. +This contribution recodes individual numerators and preserves clearing after +every macro. It also saves work backward, where #722 reports no eligible runs. +No combined saving is claimed without a composed recount. #722 is credited +related work and is not imported or independently verified here. + +Prepared for **Sagar Thakrar, @thakrarsagar**, with substantial **OpenAI Codex +assistance** in research, code, proof analysis, verification and writing. +A separately delegated Codex worker independently checked the cost census +and prefix calculation. That is AI-assisted cross-checking, not independent +human review. New material is under the repository's Apache-2.0 license. diff --git a/research/complex-signed-digit/SOURCES.json b/research/complex-signed-digit/SOURCES.json new file mode 100644 index 0000000000..b94ab4cf64 --- /dev/null +++ b/research/complex-signed-digit/SOURCES.json @@ -0,0 +1,31 @@ +{ + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "reviewed_source_heads": { + "622": "f69477f4f6d3c7eb1f740b166881bffed4ffa9f6", + "626": "660de893d27bb7abd1d5b01b1640207528a5c851" + }, + "files": { + "research/community-k492-audit/pr626/replay/mixed-global/base/providers/jp8/INDEPENDENT-LOCAL-REPLAY.json": { + "sha256": "cb2f99ed351925dd35434b73de16f4085884fe81a35a69e1c7ce2d5e96cb975b", + "git_blob": "19a4edfa2091d4cf38db49d7a780d29232badb49" + }, + "research/complex-k492-owner-repair/code/hpe_emit_local.py": { + "sha256": "7e4a6fbc38c8228157b6311457d1496bf460291393043932d2c365f004f77805", + "git_blob": "534fdc71f7641c704575efc038363d7eb206b2df" + }, + "research/community-k492-audit/pr626/replay/mixed-global/base/providers/jp8/LOCAL-PROGRAMS.json.gz": { + "sha256": "fa0c196f65bd6ec1424fdf7d789f6972075c7bb02bf43f573ea85eafab31be98", + "payload_sha256": "efe45ce7fb025a6f53cc9eb54e951ac2211a5ed927e689a049e4f68ca680654b", + "git_blob": "e22169a1633638213a5c63425a1919c7185f4c43" + }, + "research/community-k492-audit/pr626/replay/mixed-global/base/providers/jp8/CANONICAL-WORD.json.gz": { + "sha256": "7a3fec1022d3b2b1bd986302a327735ec521d17b043f4a5acb96253a56f6193c", + "payload_sha256": "fb4a8d14ed2a8048698bea6ae16f86163a1aa6c80f2eb622222eee5cdbce9b3b", + "git_blob": "7fd7cd1fefbb8b0e12397b355d9f6e227813bd58" + }, + "research/community-k492-audit/pr626/replay/mixed-global/base/providers/jp8/LOCAL-CHECKS.json": { + "sha256": "0fad744aa863eedb288a9f87b1c23225a36b316b6275cc3b1bcedd42afe28a67", + "git_blob": "0d84d903086993330ddcd871e66b15854f0c3ccd" + } + } +} diff --git a/research/complex-signed-digit/VALIDATION.md b/research/complex-signed-digit/VALIDATION.md new file mode 100644 index 0000000000..4c26f67c9c --- /dev/null +++ b/research/complex-signed-digit/VALIDATION.md @@ -0,0 +1,52 @@ +# Validation receipt + +2026-10-13, macOS arm64, Python 3.14.8. Base and refreshed `origin/main` both +equal `66849e1475c930fd7732b1a0067ffee7e1e95f60`. + +- `python3 -I -B research/complex-signed-digit/verify.py`: PASS. +- `python3 -I -O -B research/complex-signed-digit/verify.py`: PASS, including + all nine controls with assertions disabled. +- `make selected-record-check`: PASS for the selected record, exact kappa, + original source inventory and proof supplements. +- `git diff --cached --check`: PASS. +- In-memory CLI corruption checks replaced the pinned program bytes and + reduced the expected forward cost by two. They failed with `source drift` + and `committed receipt mismatch`, respectively. No source file was changed. + +A separately delegated Codex worker independently recounted both orientations +and obtained the same costs and exact prefix fractions. Its review identified +the need to reject temporary writes outside scratch; the checker now enforces +that restriction and tests an endpoint-neutral target excursion. This was +AI-assisted review, with no independent human-review claim. + +The final overlap review at 04:48:49 UTC covered 540 open PRs through #721. +No pinned coordination issue existed. Relevant refreshed heads were: + +- #696, `5a3f983715027c4fd83f50bc9001d4b18463bed1`: copy and unit lowering, + unchanged since initial inspection. The present saving isolates numerator + recoding and does not count its improvement. +- #681, `fdc2e4f3c6825530b02143b30deab5de10209479`: expanded to fourteen raw + factory windows since initial inspection. Its macro changes remain distinct + from recoding coefficients of the unchanged selected JP8 word. +- #687, `82bbb9c3ac34540f196410d137ebc59d9c2c43a9`: finite K-triangle + read-relocation neighborhood, unchanged. +- #717, `07f4671a838088b59c6356ab2b5ffe30038d4b1a`: construction-format + limits and invoice sensitivity. Its reported search classes do not recode + the private coefficient stream. + +These pending contributions are credited context, not source dependencies. +The metadata refresh found no duplicate signed-digit JP8 contribution. + +The post-submission head check found concurrent #722 at +`a0766ab0fab379e1997fadc3ca157578d57986c1`. Its body and file inventory were +inspected. It shares preparation across forward cleanup blocks and keeps +binary Horner; this result preserves each macro boundary, recodes numerators, +and also improves backward. README.md and the PR description credit this +distinct contribution. No additive saving or implementation dependency is +claimed. The source and mathematical checks above are unaffected. + +The full regenerating `make verify`, selected cold replay, global hosting and +assembly, Linux CI and Lean were not run. This package adds a local circuit +and an exact finite check; it does not modify the selected construction. +The inherited all-size, physical, precision/tape and analytic obligations +listed in README.md remain unresolved by this work. diff --git a/research/complex-signed-digit/lowering.py b/research/complex-signed-digit/lowering.py new file mode 100644 index 0000000000..9af13ff83f --- /dev/null +++ b/research/complex-signed-digit/lowering.py @@ -0,0 +1,40 @@ +"""Paid signed-digit coefficient circuits. Apache-2.0; OpenAI Codex assistance.""" + +from fractions import Fraction + + +def numerator_digits(n): + """Most significant first non-adjacent digits of a positive integer.""" + if type(n) is not int or n <= 0: + raise ValueError("positive integer numerator required") + digits = [] + while n: + digit = 2 - n % 4 if n % 2 else 0 + digits.append(digit) + n = (n - digit) // 2 + return digits[::-1] + + +def circuit(q, signed=True): + """Lower t += q*s, with distinct t,s,w and arbitrary initial private w. + + Each tuple is one real primitive. Both real components execute this word. + The original clear/leading-add initialization is retained for attribution. + """ + q = Fraction(q) + if not q or q.denominator & (q.denominator - 1): + raise ValueError("nonzero dyadic coefficient required") + n = abs(q.numerator) + binary = [int(bit) for bit in bin(n)[2:]] + digits = numerator_digits(n) if signed else binary + if len(digits) + sum(d != 0 for d in digits) >= len(binary) + sum(binary): + digits = binary + ops = [("clear", "w")] + for i, digit in enumerate(digits): + if i: + ops.append(("double", "w")) + if digit: + ops.append(("add" if digit == 1 else "sub", "w", "s")) + ops.extend([("half", "w")] * (q.denominator.bit_length() - 1)) + ops.extend([("add" if q > 0 else "sub", "t", "w"), ("clear", "w")]) + return ops diff --git a/research/complex-signed-digit/verify.py b/research/complex-signed-digit/verify.py new file mode 100644 index 0000000000..4d191a1da8 --- /dev/null +++ b/research/complex-signed-digit/verify.py @@ -0,0 +1,231 @@ +"""Exact finite JP8 numerator-recoding check. Apache-2.0, Codex assisted.""" + +import ast +from collections import Counter +from fractions import Fraction as Q +from functools import lru_cache +import gzip +import hashlib +import json +from pathlib import Path +import sys + +sys.path.insert(0, str(Path(__file__).resolve().parent)) +from lowering import circuit + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +PROVIDER = "research/community-k492-audit/pr626/replay/mixed-global/base/providers/jp8/" + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def digest(value): + return hashlib.sha256(json.dumps(value, sort_keys=True, separators=(",", ":")).encode()).hexdigest() + + +def load_sources(): + sources = json.loads((HERE / "SOURCES.json").read_text()) + data = {} + for name, pin in sources["files"].items(): + raw = (ROOT / name).read_bytes() + require(hashlib.sha256(raw).hexdigest() == pin["sha256"], "source drift: " + name) + blob = b"blob " + str(len(raw)).encode() + b"\0" + raw + require(hashlib.sha1(blob).hexdigest() == pin["git_blob"], "blob drift: " + name) + if name.endswith(".gz"): + raw = gzip.decompress(raw) + require(hashlib.sha256(raw).hexdigest() == pin["payload_sha256"], "payload drift") + data[name] = raw + return data + + +def execute(ops): + """Independent three-column interpreter; no digit identities assumed.""" + rows = {r: [Q(i == j) for j in range(3)] for i, r in enumerate(("t", "s", "w"))} + scratch_peak = Q(0) + for op in ops: + tag, target, *rest = op + if tag == "clear": + rows[target] = [Q(0)] * 3 + elif tag in ("double", "half"): + rows[target] = [x * (2 if tag == "double" else Q(1, 2)) for x in rows[target]] + elif tag in ("add", "sub"): + sign = 1 if tag == "add" else -1 + rows[target] = [x + sign*y for x, y in zip(rows[target], rows[rest[0]])] + else: + raise ValueError("unknown primitive") + scratch_peak = max(scratch_peak, sum(map(abs, rows["w"]))) + return rows, scratch_peak + + +def validate_circuit(q, ops): + require(ops[0] == ("clear", "w") and ops[-1] == ("clear", "w"), "private boundary") + require(ops[-2] == ("add" if q > 0 else "sub", "t", "w"), "target boundary") + require(all(op in (("double", "w"), ("half", "w"), ("add", "w", "s"), ("sub", "w", "s")) + for op in ops[1:-2]), "coefficient preparation touches an external register") + rows, peak = execute(ops) + require(rows == {"t": [Q(1), q, Q(0)], "s": [Q(0), Q(1), Q(0)], "w": [Q(0)]*3}, + "coefficient boundary or private erasure failed") + require(peak <= abs(q.numerator) + 1, "scratch peak exceeds numerator plus one") + return peak + + +@lru_cache(None) +def checked(q): + old, new = circuit(q, False), circuit(q) + old_peak = validate_circuit(q, old) + new_peak = validate_circuit(q, new) + require(old_peak == abs(q.numerator), "reference scratch bound") + require(len(new) <= len(old), "cost regression") + return old, new, old_peak, new_peak + + +def add_row(target, source, q): + result = dict(target) + for key, value in source.items(): + value = result.get(key, Q(0)) + q*value + if value: + result[key] = value + else: + result.pop(key, None) + return result + + +def replay(events, orientation, native_bound, canonical, original_checks, prior): + n, v = 2*canonical["v"] + canonical["R"], canonical["v"] + state = {("L", r): {r: Q(1)} for r in range(n)} + envelope = {r: Q(1) for r in state} + peaks = [Q(1), Q(1)] + counts = [0, 0] + paid, coefficients = Counter(), Counter() + changed = overshoots = macros = 0 + recipe = [] + for index, event in enumerate(events): + if event[0] in ("climb", "center"): + paid[event[5] if event[0] == "climb" else event[4]] += 1 + elif event[0] == "scalar": + macros += 1 + op = event[1] + tag, target = op[0], tuple(op[1]) + old_count = new_count = native_bound(op) + if tag == "clear": + state[target], envelope[target] = {}, Q(0) + elif tag == "copy": + source = tuple(op[2]) + state[target], envelope[target] = dict(state[source]), envelope[source] + elif tag == "scale": + q = Q(op[2], op[3]) + state[target] = {r: q*x for r, x in state[target].items()} + envelope[target] *= abs(q) + elif tag == "add": + source, q = tuple(op[2]), Q(op[3], op[4]) + require(target != source, "aliased scalar operands") + old, new, old_peak, new_peak = checked(q) + require(len(old) == old_count, "native invoice mismatch") + new_count = len(new) + coefficients[str(q)] += 1 + for i, scratch in enumerate((old_peak, new_peak)): + peaks[i] = max(peaks[i], scratch*envelope[source]) + if new_count < old_count: + changed += 1 + overshoots += new_peak > old_peak + recipe.append([index, str(q), new]) + # The three-column primitive check supplies this exact macro map. + state[target] = add_row(state.get(target, {}), state[source], q) + envelope[target] = envelope.get(target, Q(0)) + abs(q)*envelope[source] + else: + raise ValueError("unknown scalar operation") + for i, count in enumerate((old_count, new_count)): + counts[i] += 2*count + peaks[i] = max(peaks[i], envelope[target]) + else: + require(event[0] in ("adapter", "residual_adapter", "phase"), "unknown event") + for r in range(n): + expected = {r: Q(1)} + if orientation == "forward" and v <= r < 2*v: + expected[r-v] = Q(1) + elif orientation == "backward" and r < v: + expected[v+r] = Q(-1) + require(state[("L", r)] == expected, "scalar projection column mismatch") + require(all(not row for r, row in state.items() if r[0] == "C"), "centre dirt remains") + require(counts[0] == original_checks["real_component_primitive_bound"], "original cost receipt") + require(macros == original_checks["scalar_macros"], "original macro receipt") + require(dict(paid) == {int(r): k for r, k in canonical["local_profile"].items()}, "paid profile") + bits = [x.numerator.bit_length() - x.denominator.bit_length() + 1 for x in peaks] + require(peaks[0] == Q(prior["prefix_l1_upper"]) and bits[0] == prior["prefix_bits_upper"], + "reference envelope receipt") + require(peaks[1] < 2**prior["charged_payload_bits"], "retained local payload exceeded") + return { + "events": len(events), "scalar_macros": macros, "scalar_projection_columns": n, + "distinct_signed_coefficients": len(coefficients), "changed_additions": changed, + "changed_with_scratch_overshoot": overshoots, + "real_primitives_before": counts[0], "real_primitives_after": counts[1], + "saved_real_primitives": counts[0] - counts[1], + "prefix_l1_before": str(peaks[0]), "prefix_l1_after": str(peaks[1]), + "prefix_bits_before": bits[0], "prefix_bits_after": bits[1], + "charged_local_payload_bits": prior["charged_payload_bits"], + "paid_profile": {str(k): z for k, z in sorted(paid.items())}, + "changed_recipe_sha256": digest(recipe), "coefficient_census_sha256": digest(coefficients), + } + + +def controls(): + def rejected(action): + try: + action() + except ValueError: + return + raise ValueError("negative control was accepted") + + q = Q(31, 8) + ops = circuit(q) + require(len(ops) < len(circuit(q, False)), "control witness must improve") + mutants = { + "wrong_signed_digit": [("add", *op[1:]) if op[0] == "sub" else op for op in ops], + "missing_initial_clear": ops[1:], + "missing_final_clear": ops[:-1], + "missing_target_accumulation": ops[:-2] + ops[-1:], + } + half = next(i for i, op in enumerate(ops) if op[0] == "half") + mutants["missing_halving"] = ops[:half] + ops[half+1:] + for mutant in mutants.values(): + rejected(lambda mutant=mutant: validate_circuit(q, mutant)) + rejected(lambda: circuit(Q(1, 3))) + rejected(lambda: circuit(0)) + rejected(lambda: require(validate_circuit(q, ops) <= 31, "undercharged scratch")) + # An endpoint-neutral target excursion must not bypass the scratch-only proof. + excursion = ops[:-2] + [("double", "t"), ("half", "t")] + ops[-2:] + rejected(lambda: validate_circuit(q, excursion)) + return list(mutants) + ["nondyadic", "zero", "undercharged_scratch", "target_excursion"] + + +def verify(): + data = load_sources() + emitter = "research/complex-k492-owner-repair/code/hpe_emit_local.py" + tree = ast.parse(data[emitter]) + node = next(n for n in tree.body if isinstance(n, ast.FunctionDef) and n.name == "primitive_bound") + scope = {"Q": Q} + exec(compile(ast.Module(body=[node], type_ignores=[]), emitter, "exec"), scope) + programs = json.loads(data[PROVIDER + "LOCAL-PROGRAMS.json.gz"]) + canonical = json.loads(data[PROVIDER + "CANONICAL-WORD.json.gz"]) + original = json.loads(data[PROVIDER + "LOCAL-CHECKS.json"]) + prior = json.loads(data[PROVIDER + "INDEPENDENT-LOCAL-REPLAY.json"]) + require(set(programs) == {"forward", "backward"}, "orientation inventory") + require((canonical["v"], canonical["R"], canonical["h"]) == (112, 492, 9), "source geometry") + results = {o: replay(programs[o], o, scope["primitive_bound"], canonical, original[o], prior["local"][o]) + for o in ("forward", "backward")} + return {"status": "PASS_COMPLEX_SIGNED_DIGIT", "provider": "jp8", "assignment_seed": 36, + "programs": results, "negative_controls": controls()} + + +if __name__ == "__main__": + require(sys.argv[1:] in ([], ["--report"]), "usage: verify.py [--report]") + receipt = verify() + if sys.argv[1:] == ["--report"]: + print(json.dumps(receipt, indent=2)) + else: + require(receipt == json.loads((HERE / "EXPECTED.json").read_text()), "committed receipt mismatch") + print("PASS_COMPLEX_SIGNED_DIGIT jp8 additions=250+250 real_saved=3276+3276 columns=716 controls=9")