diff --git a/.github/workflows/e8-coupled-retiming.yml b/.github/workflows/e8-coupled-retiming.yml new file mode 100644 index 0000000000..92f866dbb6 --- /dev/null +++ b/.github/workflows/e8-coupled-retiming.yml @@ -0,0 +1,29 @@ +name: E8 coupled retiming + +on: + pull_request: + paths: + - 'research/e8-coupled-retiming/**' + - '.github/workflows/e8-coupled-retiming.yml' + push: + paths: + - 'research/e8-coupled-retiming/**' + - '.github/workflows/e8-coupled-retiming.yml' + workflow_dispatch: + +permissions: + contents: read + +jobs: + verify: + runs-on: ubuntu-24.04 + timeout-minutes: 5 + steps: + - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7 + with: + persist-credentials: false + - uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97 # v7 + with: + python-version: '3.14' + - run: python3 -B research/e8-coupled-retiming/verify.py + - run: git diff --exit-code diff --git a/research/e8-coupled-retiming/NOTICE.md b/research/e8-coupled-retiming/NOTICE.md new file mode 100644 index 0000000000..8bbad70301 --- /dev/null +++ b/research/e8-coupled-retiming/NOTICE.md @@ -0,0 +1,78 @@ +# Attribution and scope of new work + +Jacob Sussman supplied the E8 label family, circuit, scatter, frame scheduler, +checkers, price routines, and general proof framework in +`jacobalansussman/wht-power-saving-lean`, commit +`9c94857bbaee886f8649edee0bc2d3c738f9555e`. + +`data/original.json.gz` is an unchanged copy from that commit. The new +certificate derives from that file. This package uses the repository's +[Apache-2.0 license](../../LICENSE). The source notices that apply to the +retained certificate are copied below. + +DaysSky's CrocSwap PR352 supplies the connection to the complex branch and the +exact coarse-moment convention used here. Its commit +`04b4c3c478b5bd8797d2663d89d8db4dfd0ad9f2`, source paths, and hashes are +recorded in `sources.json`. Prior frame-retiming contributions +include CrocSwap PR328 and PR350. No claim of priority for the general method is +made. + +The new work consists of four explicit frame changes, a deterministic +generator, independent scalar and frame checks, exact rational cost bounds, +and the short cost proof. OpenAI Codex and its research agents supplied +substantial assistance. New contributions are +offered under the repository's Apache-2.0 license. + +Attribution does not imply review or endorsement by the credited authors. + +## Upstream notice excerpts + +The following text is copied from the copyright header and sections 4 and 8 +of the [upstream NOTICE](https://github.com/jacobalansussman/wht-power-saving-lean/blob/9c94857bbaee886f8649edee0bc2d3c738f9555e/NOTICE). +References within these excerpts refer to that source repository. + +```text +Walsh-Hadamard power saving (wht-power-saving-lean) +Copyright 2026 Jacob Sussman + +Repository: https://github.com/jacobalansussman/wht-power-saving-lean + +4. How the new files were made. + Jacob Sussman made the new files on 2026-10-08, 2026-10-09 and 2026-10-10 + by directing a team of AI agents (Claude). The agents wrote the new Lean + files, the certificate data and the generator scripts. They made the + rebuild scripts under tools/rebuild/, in part by adapting programs of + CrocSwap/integer-mult-bounds (section 6): ten of the thirteen on + 2026-10-09, tidied for this repository on 2026-10-10, and three on + 2026-10-10. On 2026-10-10 they also wrote the search programs under + tools/e8/ and found with them the certificate of the fourth result + (section 8). See README.md, section 4. + +8. The certificate of the fourth result and the search programs. + tools/certificate/gcert1-e8-r783.json.gz, the Lean data modules + generated from it (Work/GCert/Data/Gen/E8*.lean, Work/GCert/Data/Gen/E8/ + and the modules of Work/GCert/Data/ with E8 or B2Ge8 in their names) and + the Python programs under tools/e8/ were made by the agents for this + repository on 2026-10-10 (section 4). The circuit in that certificate + is not the circuit of section 6, and no data file of + CrocSwap/integer-mult-bounds was loaded to make it. It uses three + devices that were published by others in pull requests to that + repository: + - the in-place pair, a + b and a - b formed on the two arrays that held + a and b: icekylinx (#184), carried in #191 and #193 (ikeboy); + - the re-use of a finished helper with a compensating read: jamesyc + (#124) and eumemic (#143); + - the late pairing rule, the choice of which finished helper a new + value takes: Chafik Boukhalfa (the account chafreaky), #200 and #233, + and pull request #2 of this repository. The search programs apply the + idea with a greedy rule of their own; his program, his pairs and his + certificate were not used. + No program of that repository is included in tools/e8/, imported or + run by it. The programs of tools/e8/ have not been compared statement + by statement with the programs of that repository, as those of + tools/rebuild/ were (section 6). The integer programme of + tools/e8/ is solved with the open-source solver HiGHS, called through + SciPy (scipy.optimize.milp), with NumPy; none of the three is included + here. The credits, with links, are in README.md ("Whose ideas the new + unit uses") and in RELATED-WORK.md, section 8. +``` diff --git a/research/e8-coupled-retiming/PROOF.md b/research/e8-coupled-retiming/PROOF.md new file mode 100644 index 0000000000..332d30c265 --- /dev/null +++ b/research/e8-coupled-retiming/PROOF.md @@ -0,0 +1,170 @@ +# Four E8 frame changes + +All gate and register indices below are zero-based indices in the original +certificate. Binary frames are given by integer bit masks. The new certificate +has uncompressed SHA-256 +`3191011e0cb189665c8e0a9b97137dbed50241a0704c8be01c11b1b5a9518fc2`. + +## Circuit changes + +1. Remove `helper388 -= source64` and `helper771 += source64` from A65. + Insert those two additions just before A187, at frame 285 with basis + `[196,56]`. No gate A66 through A186 touches any of these three registers. + Source 64 has label 56. +2. Remove `helper693 += source98` and `helper839 -= source98` from A100. + Insert those two additions just before A198, at frame 296 with basis + `[257,243,14]`. No gate A101 through A197 touches any of these three + registers. Source 98 has label 253, and `253 = 243 XOR 14`. +3. In B193, B916, and B917, replace frame 599, with basis + `F=[276,148,84,51,15]`, by `G=[256,128,64,39,20,15]`. + These gates add helper807 to helper766, distribute plus or minus half of + helper807 to targets149 and155, and add helper766 to helper807. +4. In B873 and B874, replace frame 585, with basis `[161,81,9,5,3]`, + by `[305,161,81,9,5,3]`. The first gate adds half of helper550 to target198 + and subtracts half of helper550 from target202. The second gate adds + helper521 to helper550. + +The first two changes move additions only across gates that touch disjoint +registers. Such scalar operations commute, for all initial register values. +Neither change crosses the scatter. The last two changes keep all scalar +operations and their order. Thus the complete scalar operator and the retained +totals at scatter stay the same. The verifier also compares the complete +1023-by-1023 rational scalar matrices. + +All paths remain nested. The verifier checks actual binary subspace inclusion, +not only dimensions. For the third change, `G=F+span(256)` has dimension six. +The identities + +``` +276 = 256 XOR 20 +148 = 128 XOR 20 +84 = 64 XOR 20 +51 = 39 XOR 20 +``` + +show that F is contained in G. The preceding helper frames are contained in F. +The next helper frames are + +``` +helper766: [256,128,64,37,20,13,2] +helper807: [256,128,64,38,20,14,1] +``` + +They contain G because `39=37 XOR 2=38 XOR 1` and +`15=13 XOR 2=14 XOR 1`. The final target frames also contain G: + +``` +target149: [256,128,64,32,18,8,6,1] +target155: [256,128,64,34,16,10,4,1] +``` + +For target149, use `39=32 XOR 6 XOR 1`, `20=18 XOR 6`, and +`15=8 XOR 6 XOR 1`. For target155, use `39=34 XOR 4 XOR 1`, +`20=16 XOR 4`, and `15=10 XOR 4 XOR 1`. + +For the fourth change, let `F=span(161,81,9,5,3)` and +`G=F+span(305)`. These frames have dimensions five and six. All preceding +frames are contained in F. The next frame of helper521 is +`span(257,145,81,48,9,5,3)`. The next frame of helper550 and both targets is +`span(304,160,80,8,4,2,1)`. Both contain F. They contain the added vector +because `305=257 XOR 48=304 XOR 1`. Thus both contain G, and the paths +remain nested. + +## Child ranks + +Each climb contributes a child whose rank is the increase in frame dimension. +The four changes affect disjoint sets of registers. Thus their histogram +differences add. + +| Change | Register | Old child ranks | New child ranks | +| --- | --- | --- | --- | +| 1 | source64 | 5,3 | 1,4,3 | +| 1 | helper388 | 1,1,2,2,3 | 2,2,2,3 | +| 1 | helper771 | 1,1,1,3,1,2 | 2,1,3,1,2 | +| 2 | source98 | 5,3 | 2,3,3 | +| 2 | helper693 | 1,2,1,5 | 3,1,5 | +| 2 | helper839 | 1,2,1,2,1,1,1 | 3,1,2,1,1,1 | +| 3 | helper766 and helper807, each | 3,2,2,1,1 | 3,3,1,1,1 | +| 3 | target149 and target155, each | 5,3 | 6,2 | +| 4 | target198 and target202, each | 5,2,1 | 6,1,1 | +| 4 | helper521 | 2,1,2,2,1,1 | 2,1,2,1,1,1,1 | +| 4 | helper550 | 2,1,2,2,2 | 2,1,3,1,2 | + +The combined invocation histogram difference is + +``` +rank: 1 2 3 4 5 6 +change: +2 -6 +4 +1 -6 +4 +``` + +Its rank mass is zero and its child count is minus one. Copy cost remains 72. +The five-stage histogram is five times the invocation histogram, plus 240 +children at each rank 4, 8, 16, and 20. Therefore its rank mass remains 56,715, +with dimension m=45, stock W=1263, and deficit mW-56715=120. + +## Strict cost inequality + +Let a be a saving, with 0 1 +M_candidate(876412559609473 / 10^18) < 1 +M_candidate(876412559609474 / 10^18) > 1. +``` + +The logarithm uses the atanh series with a positive geometric tail bound. +Arguments are reduced to [1,2]. The exponential uses a Taylor polynomial of degree 20 with +a geometric tail bound. All arithmetic in these enclosures is rational. +Decimals in the saved result are only displays of the proved margins. + +## Limits + +This proves the finite circuit and recursive-cost improvement under the +stated convention. The general frame-transfer and recursion theorems remain +dependencies. A complete scalar identity is not a proof of the tape compiler +or the integer-multiplication assembly. No global optimum or larger final +integer-multiplication saving is claimed. + +The local verifier checks the finite rational circuit, its frame paths, and +the stated moment. It does not run the upstream checkers or their Lean +representation checks for separate positive and negative parts and digit +limits. The disjoint operations in the first two changes commute in those +representations as well: each moved addition crosses only operations on other +registers. The last two changes leave the scalar operations in place. This +preserves the scalar computation from the pinned baseline; it does not replace +a build of new Lean data. diff --git a/research/e8-coupled-retiming/README.md b/research/e8-coupled-retiming/README.md new file mode 100644 index 0000000000..50593e7050 --- /dev/null +++ b/research/e8-coupled-retiming/README.md @@ -0,0 +1,80 @@ +# E8 complex cost from four coupled frame changes + +This package changes Jacob Sussman's E8 circuit at commit +`9c94857bbaee886f8649edee0bc2d3c738f9555e`. It gives a smaller recursive moment with +the same 783 helpers, copy cost 72, rank mass 56,715, and deficit 120. + +| Quantity | Original | Candidate | +| --- | ---: | ---: | +| Conditional complex saving under PR352's fallback convention | 876248285600677 / 10^18 | 876412559609473 / 10^18 | +| Children in one invocation | 3974 | 3973 | +| Children in five stages | 20830 | 20825 | +| Scalar additions, including scatter | 3876 | 3876 | + +The conditional saving increases by about 0.01875%. + +Four phase-A additions move to two later frames. Two sets of phase-B gates use +larger frames. The original frame table gains two entries. All scalar coefficients, +retained totals, and scatter coefficients stay the same. The complete rational +scalar operator also stays the same, including its dependence on every initial +helper value. + +[PROOF.md](PROOF.md) gives the exact edits and a strict cost inequality for every +saving between zero and one. It does not rely on the approximate moment root. + +## Reproduce + +From the repository root, run: + +```sh +python3 -B research/e8-coupled-retiming/verify.py +``` + +The script uses Python and its standard library. It checks source hashes, +rebuilds the candidate, checks every frame path, reconstructs the scalar source +map and histogram, and compares all 1,046,529 entries of the complete scalar maps. +A coefficient identity checks the +strict-concavity proof for the full saving interval. Exact rational bounds prove both +reported savings. In each case the next 10^-18 grid point fails. Four damaged +inputs must fail for their stated reasons. + +To write the candidate to another file, run: + +```sh +python3 -B research/e8-coupled-retiming/retime.py /tmp/e8-retimed.json.gz +``` + +The saved verification result is `verification.json`. Run the script to obtain +a fresh result; the script does not use that saved result as an input. + +## Scope + +This is a finite complex-circuit improvement. It does not change the selected +integer-multiplication result, the bit circuit, or its saving. + +The new certificate has not been compiled in Lean. The original certificate's +Lean data and theorem do not certify this changed file. A formal extension must +generate and compile new data. The general frame-transfer, helper cleanup, +recursive construction, and multiplication assembly remain inherited +dependencies. The complete scalar-map comparison does not prove those steps. +The script does not run the upstream checkers or their Lean representation +checks for separate positive and negative parts and digit limits. + +## Source and search + +The baseline is Sussman's `tools/certificate/gcert1-e8-r783.json.gz`. The exact +commit and original-data hash are in `sources.json`. The E8 complex +connection and fallback convention follow CrocSwap PR352 at +`04b4c3c478b5bd8797d2663d89d8db4dfd0ad9f2`. The exact reference paths and +hashes are recorded as mathematical provenance in `sources.json`; those files +are not imported or run. Earlier retiming +work includes Sussman's `tools/e8/sched.py` and CrocSwap PR328 and PR350. +This package supplies a new E8 witness; it does not claim to invent retiming. + +The candidate came from bounded searches over pairs of moves and common +intermediate frames. Frames came from existing stops and their joins or +intersections. A later search moved two more complete gates to one common +intermediate frame. These searches do not establish +global optimality. The search is not needed to reproduce or verify the witness. + +See [NOTICE.md](NOTICE.md) for attribution and AI assistance. diff --git a/research/e8-coupled-retiming/data/original.json.gz b/research/e8-coupled-retiming/data/original.json.gz new file mode 100644 index 0000000000..0bd0bacf74 Binary files /dev/null and b/research/e8-coupled-retiming/data/original.json.gz differ diff --git a/research/e8-coupled-retiming/data/retimed.json.gz b/research/e8-coupled-retiming/data/retimed.json.gz new file mode 100644 index 0000000000..efdb76ecf3 Binary files /dev/null and b/research/e8-coupled-retiming/data/retimed.json.gz differ diff --git a/research/e8-coupled-retiming/reconstruct.py b/research/e8-coupled-retiming/reconstruct.py new file mode 100644 index 0000000000..9cefd8ec9d --- /dev/null +++ b/research/e8-coupled-retiming/reconstruct.py @@ -0,0 +1,226 @@ +"""Check the E8 scalar map, frame paths, and recursive cost from one certificate. + +This file uses only the Python standard library. It imports no supplier code. +The checks do not prove the all-size tape compiler or the multiplication theorem. +""" + +import argparse +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 + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def add(row, source, coefficient): + for key, value in source.items(): + increment = coefficient * value + require(6 % increment.denominator == 0, "Scalar increment is not in sixths") + result = row.get(key, Q(0)) + increment + if result: + row[key] = result + else: + row.pop(key, None) + + +def elements(basis): + result = {0} + for vector in basis: + require(vector not in result, "Dependent frame basis") + result |= {x ^ vector for x in result} + return frozenset(result) + + +@lru_cache(None) +def logarithm(ratio): + def small(value): + t = (value - 1) / (value + 1) + total = Q(0) + power = t + terms = 80 + for j in range(terms): + total += 2 * power / (2 * j + 1) + power *= t * t + tail = 2 * power / ((2 * terms + 1) * (1 - t * t)) + return total, total + tail + + exponent = 0 + while ratio >= 2: + ratio /= 2 + exponent += 1 + lo, hi = small(ratio) + a, b = small(Q(2)) + return lo + exponent * a, hi + exponent * b + + +def exponential(value): + require(0 <= value < 1, "Exponential bound requires an argument below one") + total = term = Q(1) + for j in range(1, 21): + term *= value / j + total += term + tail = term * value / 21 / (1 - value / 22) + return total, total + tail + + +def moment(histogram, dimension, stock, saving, fallback=True): + lo = hi = Q(0) + terms = {rank: Q(count) for rank, count in histogram.items()} + if fallback: + terms[1] = terms.get(1, Q(0)) + Q( + 32 * dimension * dimension * sum(histogram.values()), 10**16 + ) + for rank, count in terms.items(): + a, b = logarithm(Q(dimension, rank)) + lower = exponential(saving * a)[0] + upper = exponential(saving * b)[1] + weight = count * rank / (dimension * stock) + lo += weight * lower + hi += weight * upper + return lo, hi + + +def reconstruct(c): + require(c["format"] == "gcert/1", "Certificate format") + h, v, helpers = c["h"], c["v"], c["R"] + require((h, v) == (9, 120), "This audit is for the E8 label family") + require(not c["ext"], "Exterior gauges are outside this audit") + ports = c["ports"] + require(len(ports) == v and set(ports) == {p for p in range(512) if p.bit_count() in (3, 7)}, "E8 ports") + require(c["frames"][0] == [] and c["frames"][1] == [1 << i for i in range(h - 1, -1, -1)], "Frame endpoints") + for basis in c["frames"]: + require(all(0 < vector < 512 for vector in basis), "Frame outside ambient space") + pivots = [vector.bit_length() - 1 for vector in basis] + require(pivots == sorted(set(pivots), reverse=True) and all( + not (vector >> pivot & 1) + for i, vector in enumerate(basis) for j, pivot in enumerate(pivots) if i != j + ), "Noncanonical frame basis") + spaces = [elements(f) for f in c["frames"]] + dimensions = [len(f) for f in c["frames"]] + require(len(set(spaces)) == len(spaces), "Duplicate frame spaces") + require(all(all(0 <= x < 512 for x in s) for s in spaces), "Frame outside ambient space") + total = 2 * v + helpers + require(len(c["start"]) == len(c["final"]) == total, "Endpoint count") + require(all(0 <= frame < len(spaces) for frame in c["start"] + c["final"]), "Endpoint frame index") + current = list(c["start"]) + rows = [{i: Q(1)} if i < v else {} for i in range(total)] + by_role = {kind: Counter() for kind in "xysc"} + allowed = {("x", "s"), ("s", "s"), ("s", "y"), ("x", "y"), ("x", "x")} + + def kind(register): + return "x" if register < v else "y" if register < 2 * v else "s" + + def climb(register, frame): + previous = current[register] + require(spaces[previous] <= spaces[frame], "A frame path is not nested") + if previous != frame: + by_role[kind(register)][dimensions[frame] - dimensions[previous]] += 1 + current[register] = frame + + for i, port in enumerate(ports): + require(spaces[current[i]] == {0, port}, "Source start") + require(spaces[c["final"][i]] == frozenset(range(512)), "Source final") + require(spaces[current[v + i]] == {0}, "Target start") + require(spaces[c["final"][v + i]] == {x for x in range(512) if (x & port).bit_count() % 2 == 0}, "Target final") + for i in range(2 * v, total): + require(spaces[current[i]] == {0} and len(spaces[c["final"][i]]) == 512, "Helper endpoints") + + def run(gates, phase): + for gate in gates: + require(gate[0] in ("in", "out") and len(gate) == (5 if gate[0] == "out" else 4), "Unsupported gate") + tag, frame, pivot, terms = gate[:4] + require(0 <= frame < len(spaces), "Gate frame index") + spectators = gate[4] if tag == "out" else [] + registers = [pivot] + [r for r, _, _ in terms] + spectators + require(len(set(registers)) == len(registers), "Aliased gate ports") + require(all(0 <= r < total for r in registers), "Register outside circuit") + require(phase == "B" or all(kind(r) != "y" for r in registers), "Early target operation") + for register in registers: + climb(register, frame) + for register, numerator, denominator in terms: + target, source = (pivot, register) if tag == "in" else (register, pivot) + require((kind(source), kind(target)) in allowed, "Unsupported scalar direction") + require(phase == "B" or (kind(source), kind(target)) in {("x", "s"), ("s", "s")}, "Unsupported phase-A scalar direction") + require(denominator > 0, "Coefficient denominator") + add(rows[target], rows[source], Q(numerator, denominator)) + + run(c["A"], "A") + retained = c["ret"] + require(sorted(k for k, _, _ in retained) == list(range(len(retained))), "Retained total indices") + totals = {} + for k, register, frame in retained: + require(2 * v <= register < total and current[register] == frame, "Retained total frame") + totals[k] = dict(rows[register]) + by_role["c"][dimensions[frame]] += 1 + require(all(spaces[current[v + i]] == {0} for i in range(v)), "Target moved before scatter") + require(len(c["scat"]["table"]) == v, "Scatter size") + for target, entries in enumerate(c["scat"]["table"]): + for k, numerator, denominator in entries: + require(k in totals and denominator > 0, "Scatter entry") + add(rows[v + target], totals[k], Q(numerator, denominator)) + run(c["B"], "B") + require(all(rows[i] == {i: Q(1)} and rows[v + i] == {i: Q(1)} for i in range(v)), "Clean-source scalar identity") + for i, frame in enumerate(c["final"]): + climb(i, frame) + recorded = {kind: {int(r): n for r, n in hist.items()} for kind, hist in c["blocks"].items()} + require(by_role == recorded, "Recorded histogram differs from actual paths") + invocation = sum(by_role.values(), Counter()) + copy_cost = sum(rank * count for rank, count in by_role["c"].items()) + require(copy_cost == c["cst"], "Copy cost") + mass = sum(rank * count for rank, count in invocation.items()) + require(mass == c["N"] == helpers * h + 2 * v * (h - 1) + copy_cost, "Telescoping rank identity") + histogram = Counter({rank: 5 * count for rank, count in invocation.items()}) + for rank in (h - 1, 2 * h - 2, 2 * h + 2, 4): + histogram[rank] += 2 * v + dimension, stock = 5 * h, 4 * v + helpers + deficit = dimension * stock - sum(rank * count for rank, count in histogram.items()) + require(deficit == 4 * v - 5 * copy_cost, "Five-stage deficit") + return { + "h": h, "v": v, "helpers": helpers, "frames": len(spaces), + "source_columns": v, "copy_cost": copy_cost, + "invocation_histogram": dict(sorted(invocation.items())), "invocation_mass": mass, + "m": dimension, "W": stock, "histogram": dict(sorted(histogram.items())), + "rank_mass": dimension * stock - deficit, "deficit": deficit, + "scope": "Exact scalar source columns and frame paths. The general dirty and frame transfer theorems remain dependencies. No tape compiler or Lean build is checked.", + } + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument("certificate", type=Path) + parser.add_argument("--saving", default="876248285600677/1000000000000000000") + parser.add_argument("--output", type=Path) + args = parser.parse_args() + blob = args.certificate.read_bytes() + raw = gzip.decompress(blob) if blob[:2] == b"\x1f\x8b" else blob + result = reconstruct(json.loads(raw)) + result["source_sha256"] = hashlib.sha256(raw).hexdigest() + saving = Q(args.saving) + lower, upper = moment(result["histogram"], result["m"], result["W"], saving) + following = moment(result["histogram"], result["m"], result["W"], saving + Q(1, 10**18)) + require(upper < 1, "Requested saving is not certified") + result["saving"] = str(saving) + scale = 2**256 + lo = lower - 1 + hi = upper - 1 + enclosed = [Q(lo.numerator * scale // lo.denominator, scale), + Q(-((-hi.numerator * scale) // hi.denominator), scale)] + result["moment_minus_one"] = list(map(str, enclosed)) + result["interval_method"] = "Exact rational log and exp bounds; outward rounding to 256 bits for the saved interval." + result["adjacent_grid_excluded"] = following[0] > 1 + result["moment_gap_decimal"] = float(1 - upper) + text = json.dumps(result, indent=2) + "\n" + if args.output: + args.output.write_text(text) + print(json.dumps({k: result[k] for k in ("source_sha256", "helpers", "copy_cost", "invocation_mass", "rank_mass", "deficit", "saving", "moment_gap_decimal", "adjacent_grid_excluded")}, indent=2)) + + +if __name__ == "__main__": + main() diff --git a/research/e8-coupled-retiming/retime.py b/research/e8-coupled-retiming/retime.py new file mode 100644 index 0000000000..db25baf196 --- /dev/null +++ b/research/e8-coupled-retiming/retime.py @@ -0,0 +1,102 @@ +"""Change E8 frame assignments and count the resulting blocks.""" + +from collections import Counter +from copy import deepcopy +import gzip +import hashlib +import json +from pathlib import Path +import sys + + +ROOT = Path(__file__).resolve().parent +SOURCE_SHA256 = "3594f19c4d01cf11fb930c5c61baeed399620acbc5b94096b16bcacb23997dd3" +# All positions refer to the original, zero-based phase-A gate list. +MOVES = ((65, 187, 64, (388, 771), 285), + (100, 198, 98, (693, 839), 296)) + + +def registers(gate): + return {gate[2]} | {term[0] for term in gate[3]} | set(gate[4] if gate[0] == "out" else []) + + +def build(source): + candidate = deepcopy(source) + additions = {} + for origin, destination, source_register, targets, frame in MOVES: + gate = candidate["A"][origin] + assert gate[0] == "out" and gate[2] == source_register and not gate[4] + selected = [term for term in gate[3] if term[0] in targets] + assert len(selected) == len(targets) + touched = {source_register, *targets} + # The moved additions commute with every gate they cross. + assert all(not (registers(g) & touched) for g in source["A"][origin + 1:destination]) + assert source["A"][destination][1] == frame + gate[3] = [term for term in gate[3] if term[0] not in targets] + additions[destination] = ["out", frame, source_register, selected, []] + candidate["A"] = [g for i, gate in enumerate(candidate["A"]) + for g in ([additions[i], gate] if i in additions else [gate])] + frame = len(candidate["frames"]) + assert frame == 946 + candidate["frames"].append([256, 128, 64, 39, 20, 15]) + for index in (193, 916, 917): + assert candidate["B"][index][1] == 599 + candidate["B"][index][1] = frame + frame = len(candidate["frames"]) + assert frame == 947 + assert candidate["frames"][585] == [161, 81, 9, 5, 3] + assert candidate["B"][873] == ["out", 585, 550, [[198, 1, 2], [202, -1, 2]], []] + assert candidate["B"][874] == ["in", 585, 550, [[521, 1, 1]]] + candidate["frames"].append([305, 161, 81, 9, 5, 3]) + for index in (873, 874): + candidate["B"][index][1] = frame + candidate["derived_from"] = ( + "Three frame changes from Sussman E8 at 9c94857b; see PROOF.md" + "; move B873 and B874 to one common rank-six frame" + ) + + current = list(candidate["start"]) + blocks = {role: Counter() for role in "xysc"} + v = candidate["v"] + + def climb(register, frame): + old = current[register] + if old != frame: + role = "x" if register < v else "y" if register < 2 * v else "s" + rank = len(candidate["frames"][frame]) - len(candidate["frames"][old]) + assert rank > 0 + blocks[role][rank] += 1 + current[register] = frame + + for phase in ("A", "B"): + if phase == "B": + for _, register, frame in candidate["ret"]: + assert current[register] == frame + blocks["c"][len(candidate["frames"][frame])] += 1 + for gate in candidate[phase]: + for register in registers(gate): + climb(register, gate[1]) + for register, frame in enumerate(candidate["final"]): + climb(register, frame) + candidate["blocks"] = {role: {str(r): count for r, count in sorted(hist.items())} + for role, hist in blocks.items()} + assert sum(r * n for hist in blocks.values() for r, n in hist.items()) == candidate["N"] + return candidate + + +def main(): + if sys.flags.optimize: + raise SystemExit("Assertions must remain enabled for generation") + raw = gzip.decompress((ROOT / "data/original.json.gz").read_bytes()) + assert hashlib.sha256(raw).hexdigest() == SOURCE_SHA256 + candidate = build(json.loads(raw)) + output = Path(sys.argv[1]) if len(sys.argv) > 1 else ROOT / "data/retimed.json.gz" + raw = json.dumps(candidate, separators=(",", ":")).encode() + with output.open("wb") as stream: + with gzip.GzipFile(filename="", mode="wb", fileobj=stream, mtime=0) as zipped: + zipped.write(raw) + print(hashlib.sha256(raw).hexdigest()) + + +if __name__ == "__main__": + main() diff --git a/research/e8-coupled-retiming/scalar_map_comparison.py b/research/e8-coupled-retiming/scalar_map_comparison.py new file mode 100644 index 0000000000..f814448cf7 --- /dev/null +++ b/research/e8-coupled-retiming/scalar_map_comparison.py @@ -0,0 +1,71 @@ +"""Compare every row of the complete rational scalar maps of two certificates.""" + +from fractions import Fraction +import gzip +import hashlib +import json +from pathlib import Path +import sys + + +def word(certificate): + additions = [] + for phase in ("A", "B"): + if phase == "B": + retained = {k: register for k, register, _ in certificate["ret"]} + for target, terms in enumerate(certificate["scat"]["table"]): + additions.extend((certificate["v"] + target, retained[k], Fraction(a, b)) for k, a, b in terms) + for gate in certificate[phase]: + tag, _, pivot, terms = gate[:4] + for register, a, b in terms: + target, source = (pivot, register) if tag == "in" else (register, pivot) + additions.append((target, source, Fraction(a, b))) + return additions + + +def row(additions, output): + result = {output: Fraction(1)} + for target, source, coefficient in reversed(additions): + value = result.get(target, 0) + if value: + result[source] = result.get(source, 0) + coefficient * value + if not result[source]: + del result[source] + return result + + +def compare(certificates): + """Compare the complete scalar maps, including all initial helper values.""" + a, b = certificates + assert all(a[key] == b[key] for key in ("h", "v", "R", "ports", "scat")) + n = 2 * a["v"] + a["R"] + words = [word(certificate) for certificate in certificates] + assert len(words[0]) == len(words[1]) + counts = [] + for output in range(n): + original, candidate = (row(additions, output) for additions in words) + assert original == candidate, output + counts.append(len(original)) + return { + "complete_scalar_maps_equal": True, + "rows": n, + "columns": n, + "nonzero_entries": sum(counts), + "elementary_additions": len(words[0]), + "scope": "Exact full rational scalar map, including arbitrary source, target, and helper initial values. Frame transforms and compiled cleanup are separate obligations." + } + + +def main(): + if sys.flags.optimize: + raise SystemExit("Assertions must remain enabled for verification") + assert len(sys.argv) == 3 + raws = [gzip.decompress(Path(path).read_bytes()) for path in sys.argv[1:]] + result = compare([json.loads(raw) for raw in raws]) + result["uncompressed_sha256"] = [hashlib.sha256(raw).hexdigest() for raw in raws] + result["source_files"] = sys.argv[1:] + print(json.dumps(result, indent=2)) + + +if __name__ == "__main__": + main() diff --git a/research/e8-coupled-retiming/sources.json b/research/e8-coupled-retiming/sources.json new file mode 100644 index 0000000000..68edc2307c --- /dev/null +++ b/research/e8-coupled-retiming/sources.json @@ -0,0 +1,26 @@ +{ + "repository": "https://github.com/jacobalansussman/wht-power-saving-lean", + "commit": "9c94857bbaee886f8649edee0bc2d3c738f9555e", + "mathematical_provenance": { + "repository": "https://github.com/DaysSky/integer-mult-bounds", + "pull_request": "https://github.com/CrocSwap/integer-mult-bounds/pull/352", + "commit": "04b4c3c478b5bd8797d2663d89d8db4dfd0ad9f2", + "scope": "Reference for the moment convention only. These files are not imported or run.", + "files": { + "research/w3-p10b-e8-complex/code/pricing/moment.py": "81cbc864e106418fc7854322746f72180cb8110ff39f74450a3b8d55a82c1482", + "research/w3-p10b-e8-complex/code/complex/certify_complex.py": "7e480b7761fa700944a7dca41ccbefd530203b5e9168b6b37fe879b7e6da57fa" + } + }, + "files": { + "data/original.json.gz": "4b92f00fc7454b9b15e6d71a3b05062792eacca0a0ca4efee46f87827d57c8aa" + }, + "upstream_notice": { + "path": "NOTICE", + "sha256": "557c9ad4660eebd14a00583736c4d12d2c45f3fc9bc148845f9f3efec72c9434", + "retained_sections": [ + "copyright header", + "4. How the new files were made.", + "8. The certificate of the fourth result and the search programs." + ] + } +} diff --git a/research/e8-coupled-retiming/verification.json b/research/e8-coupled-retiming/verification.json new file mode 100644 index 0000000000..76e59bff23 --- /dev/null +++ b/research/e8-coupled-retiming/verification.json @@ -0,0 +1,67 @@ +{ + "status": "PASS", + "source_commit": "9c94857bbaee886f8649edee0bc2d3c738f9555e", + "uncompressed_sha256": [ + "3594f19c4d01cf11fb930c5c61baeed399620acbc5b94096b16bcacb23997dd3", + "3191011e0cb189665c8e0a9b97137dbed50241a0704c8be01c11b1b5a9518fc2" + ], + "histogram_delta": { + "1": 2, + "2": -6, + "3": 4, + "4": 1, + "5": -6, + "6": 4 + }, + "histogram": { + "1": 2093, + "2": 598, + "3": 522, + "4": 141, + "5": 209, + "6": 335, + "7": 43, + "8": 24, + "9": 8 + }, + "positive_second_difference_weights": [ + 1, + 4, + 1, + 2, + 4 + ], + "baseline": { + "saving": "876248285600677/1000000000000000000", + "strict_upper_below_one": true, + "next_grid_lower_above_one": true, + "upper_gap_decimal": 8.291462013379377e-19 + }, + "candidate": { + "saving": "876412559609473/1000000000000000000", + "strict_upper_below_one": true, + "next_grid_lower_above_one": true, + "upper_gap_decimal": 2.5095997917841125e-19 + }, + "m": 45, + "W": 1263, + "helpers": 783, + "copy_cost": 72, + "rank_mass": 56715, + "deficit": 120, + "scalar_map_rows_and_columns": 1023, + "checks": [ + "frame_paths", + "clean_source_identity", + "complete_scalar_map", + "exact_moments", + "strict_concavity_identity" + ], + "rejected_controls": [ + "scatter sign", + "same-rank wrong subspace", + "copy undercharge", + "forbidden phase-A cancellation" + ], + "scope": "Finite E8 circuit and exact recursive moment. No new Lean build or full multiplication theorem is claimed." +} diff --git a/research/e8-coupled-retiming/verify.py b/research/e8-coupled-retiming/verify.py new file mode 100644 index 0000000000..10c56a738a --- /dev/null +++ b/research/e8-coupled-retiming/verify.py @@ -0,0 +1,110 @@ +"""Check the pinned E8 frame changes and their exact recursive cost.""" + +from collections import Counter +from copy import deepcopy +from fractions import Fraction as Q +import gzip +import hashlib +import json +from pathlib import Path +import sys + +sys.dont_write_bytecode = True +from reconstruct import moment, reconstruct +from retime import build +from scalar_map_comparison import compare + + +ROOT = Path(__file__).resolve().parent +OLD = Q(876248285600677, 10**18) +NEW = Q(876412559609473, 10**18) +GRID = Q(1, 10**18) + + +def digest(data): + return hashlib.sha256(data).hexdigest() + + +def check_bound(result, saving): + args = result["histogram"], result["m"], result["W"] + low, high = moment(*args, saving) + next_low, _ = moment(*args, saving + GRID) + assert high < 1 < next_low + return {"saving": str(saving), "strict_upper_below_one": True, + "next_grid_lower_above_one": True, "upper_gap_decimal": float(1 - high)} + + +def main(): + if sys.flags.optimize: + raise SystemExit("Assertions must remain enabled for verification") + pins = json.loads((ROOT / "sources.json").read_text()) + for path, expected in pins["files"].items(): + assert digest((ROOT / path).read_bytes()) == expected, path + raw = [gzip.decompress((ROOT / "data" / name).read_bytes()) + for name in ("original.json.gz", "retimed.json.gz")] + original, candidate = map(json.loads, raw) + assert digest(raw[0]) == "3594f19c4d01cf11fb930c5c61baeed399620acbc5b94096b16bcacb23997dd3" + assert digest(raw[1]) == "3191011e0cb189665c8e0a9b97137dbed50241a0704c8be01c11b1b5a9518fc2" + rebuilt = json.dumps(build(original), separators=(",", ":")).encode() + assert rebuilt == raw[1] + old, new = map(reconstruct, (original, candidate)) + delta = {r: new["invocation_histogram"].get(r, 0) - old["invocation_histogram"].get(r, 0) + for r in range(1, 10)} + delta = {r: count for r, count in delta.items() if count} + assert delta == {1: 2, 2: -6, 3: 4, 4: 1, 5: -6, 6: 4} + # These positive weights prove the cost sign for every exponent in (0, 1). + weights = [1, 4, 1, 2, 4] + coefficients = Counter() + for rank, weight in enumerate(weights, 1): + assert weight > 0 + coefficients[rank - 1] += weight + coefficients[rank] -= 2 * weight + coefficients[rank + 1] += weight + assert coefficients.pop(0) == 1 + assert dict(coefficients) == delta + assert sum(delta.values()) == -1 + for key in ("helpers", "copy_cost", "invocation_mass", "rank_mass", "deficit", "m", "W"): + assert old[key] == new[key], key + + # These damaged inputs test separate proof obligations. + controls = [] + bad = deepcopy(candidate) + bad["scat"]["table"][0][0][1] *= -1 + controls.append(("scatter sign", bad, "Clean-source scalar identity")) + bad = deepcopy(candidate) + bad["A"][0][1] = candidate["start"][1] + controls.append(("same-rank wrong subspace", bad, "A frame path is not nested")) + bad = deepcopy(candidate) + bad["cst"] -= 1 + controls.append(("copy undercharge", bad, "Copy cost")) + bad = deepcopy(candidate) + bad["A"] += [["out", 1, 0, [[1, 1, 1]], []], ["out", 1, 0, [[1, -1, 1]], []]] + controls.append(("forbidden phase-A cancellation", bad, "Unsupported phase-A scalar direction")) + rejected = [] + for name, broken, expected in controls: + try: + reconstruct(broken) + except ValueError as error: + assert str(error) == expected, (name, str(error)) + rejected.append(name) + else: + raise AssertionError("Damaged input accepted: " + name) + + scalar = compare((original, candidate)) + assert scalar["complete_scalar_maps_equal"] and scalar["rows"] == 1023 + result = {"status": "PASS", "source_commit": pins["commit"], + "uncompressed_sha256": list(map(digest, raw)), + "histogram_delta": delta, "histogram": new["invocation_histogram"], + "positive_second_difference_weights": weights, + "baseline": check_bound(old, OLD), "candidate": check_bound(new, NEW), + "m": new["m"], "W": new["W"], "helpers": new["helpers"], + "copy_cost": new["copy_cost"], "rank_mass": new["rank_mass"], "deficit": new["deficit"], + "scalar_map_rows_and_columns": scalar["rows"], + "checks": ["frame_paths", "clean_source_identity", "complete_scalar_map", "exact_moments", "strict_concavity_identity"], + "rejected_controls": rejected, + "scope": "Finite E8 circuit and exact recursive moment. No new Lean build or full multiplication theorem is claimed."} + print(json.dumps(result, indent=2)) + + +if __name__ == "__main__": + main()