diff --git a/research/frontier1094-recipes-exact-seed76/CASES.json b/research/frontier1094-recipes-exact-seed76/CASES.json new file mode 100644 index 0000000000..e508b1224d --- /dev/null +++ b/research/frontier1094-recipes-exact-seed76/CASES.json @@ -0,0 +1,69 @@ +{ + "archive": { + "path": "research/community-frontier1094-audit/selected-replay.tar.gz", + "sha256": "f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6", + "pinned_by": "docs/research/community-batch1099-integration.json" + }, + "prefix": "candidate/strict/", + "certificate": "research/community-frontier1094-audit/ASSEMBLY.json", + "certificate_sha256": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045", + "selected_record": "certificates/selected-result.json", + "checkpoint_dir": "certificates/checkpoints", + "members": { + "assembly": "ASSEMBLY.json", + "template": "global/hosted/GLOBAL-TEMPLATE.json.gz", + "owner_audit": "global/audit/OWNERS-AND-PROFILE.json", + "canonical_word": "global/base/providers/gauge44/CANONICAL-WORD.json.gz", + "recipes": "global/base/providers/gauge44/CLIFFORD-RECIPES.json", + "review": "global/base/providers/gauge44/CLIFFORD-REVIEW.json", + "local_programs": "global/base/providers/gauge44/LOCAL-PROGRAMS.json.gz" + }, + "source_artifact_keys": { + "canonical_word": "providers/gauge44/CANONICAL-WORD.json.gz", + "recipes": "providers/gauge44/CLIFFORD-RECIPES.json", + "review": "providers/gauge44/CLIFFORD-REVIEW.json", + "local_programs": "providers/gauge44/LOCAL-PROGRAMS.json.gz" + }, + "twin_prefix": "global8/base/providers/gauge44/", + "decoys": { + "recipes": "global/base/split-centres/CLIFFORD-RECIPES.json", + "canonical_word": "global/base/split-centres/CANONICAL-WORD.json.gz" + }, + "slot_pins": { + "path": "research/gauge44-slots-t16/construction/slots/SLOT-PINS-k8.json", + "sha256": "55dd229684febecb80638eff9c6b3986623e8539c6c956753b350209c3e0efe2", + "listed_in": "research/community-frontier1094-audit/SELECTED-SOURCE.json" + }, + "selected_source": { + "path": "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "sha256": "79b3de5db3dbcb9829789ba58e9e45758926031e2a7d80667a08429d369be53b" + }, + "fixtures": { + "lean_exact": { + "path": "research/hyperplane-end-lean/HyperplaneEnd/Exact.lean", + "sha256": "eebf3a3982af7ab9be45777b272a6aaa523206fa7667ceb6df63ad6589fd8183" + }, + "pr1415": { + "path": "research/hpe-lean-semantic-binding/RESULT.json", + "sha256": "9c0b3f39d9ef68ed8484f29fd9cb5d57e931580a882157afb593fb28839cbfdf" + }, + "pr702": { + "path": "research/cold-wrapper-amplitude-audit/EXPECTED.json", + "sha256": "64d9a891148c84bb6e5454ac6a02399a2abb3e553ee62f2719f8ed061eb8a501" + } + }, + "expected": { + "R": 480, + "h": 9, + "v": 112, + "frames": 1004, + "frame_dims": {"0": 1, "1": 120, "2": 168, "3": 168, "4": 73, "5": 27, "6": 168, "7": 152, "8": 126, "9": 1}, + "children": 2896, + "child_ranks": {"1": 1928, "2": 380, "3": 408, "4": 124, "5": 40, "8": 16}, + "descending_children": 8, + "adapters": 224, + "port_weights": {"3": 77, "7": 35}, + "events_per_orientation": {"climb": 3486, "center": 8, "adapter": 1090}, + "review_status": "PASS_NEW_WORD_EXACT_LOCAL_PHASE_RECIPES" + } +} diff --git a/research/frontier1094-recipes-exact-seed76/README.md b/research/frontier1094-recipes-exact-seed76/README.md new file mode 100644 index 0000000000..4a4747e0c3 --- /dev/null +++ b/research/frontier1094-recipes-exact-seed76/README.md @@ -0,0 +1,212 @@ +# Independent phase-exact check of the selected frontier1094 word's Clifford recipes + +**Independent verification: no new κ, and no existing check is changed.** + +- Track: 75–84 (independent verification), assignment seed 76, drawn with the OS CSPRNG via Python `secrets`. +- Card: `independent-moment`, with the scope **refined** in [TASK.json](TASK.json). The scope is one selected assembly premise, checked by a genuinely independent exact implementation. +- Base: `0b1cccf8`. The selected record frontier1094 is unchanged. + +## The claim checked + +Lemma G's `RecipesExact` premise (`research/e8-lemma-g-lean/LemmaG/Stream.lean:110-112`) says that every relabel `A → B` of the stream executes `T_B ∘ T_A⁻¹`, where `T_F` is the canonical frame operator of frame `F`. Every climb that the selected complex profile prices as a rank-r child relies on it: the stored recipe `L ∘ (C_[r] ⊗ I) ∘ R` must implement `T_new ∘ T_old⁻¹` exactly. + +For the selected word, this package checks every stored record on all 512 columns of ℂ^(2^9), global phase included: + +- **2,896 child recipes.** Each satisfies `L ∘ F_r ∘ R ∘ T_old = T_new`. This is the same as `L F_r R = T_new T_old⁻¹`, because `T_old` is invertible. +- **224 endpoint adapters.** Each satisfies its defining identity, which is Lemma G's H6: + - source: `M ∘ C_q = T_start`; + - target: `M ∘ F_9 ∘ C_q⁻¹ = T_final`. + +**Result: all 2,896 children and all 224 adapters are exact** (`PASS_FRONTIER1094_RECIPES_EXACT`). + +### What was checked before, and what is new + +- **The producer's own check is complete, but not independent.** `phases_full.py`/`lower_child` (icekylinx) asserts two things for each recipe: equality of the signed Z4 Pauli tableau, and of column 0. Together these pin the Clifford operator exactly, global phase included. But that check ran in the producer's own code, on in-memory operators, at generation time. +- **The Lemma G package's checkers ran on other words.** `e8-lemma-g-lean` (DreamingOfClouds) ran producer-independent, all-512-column checks of these premises on four other words: #484's `lg_instances` I-tr for H2, and `code/check_adapters.py` for #433's data-adapter identities (H6). It did not run them on the selected gauge44 word. +- **Seed80** (`research/complex-frame-distance-seed80`, woklerx) checks the ranks of the same 1,004 frames and 2,896 edges, and makes no phase claim. +- **Our #1262** rebuilt the selected rank ledger independently, without phases. + +**What is new.** For the **selected** word, the stored, byte-bound `CLIFFORD-RECIPES.json` is now re-decoded and checked against `T_B T_A⁻¹` and H6. The check uses a kernel written from scratch and calibrated against the Lean literals and published digests. It is a second, independent implementation of a check the producer already passed, not the closing of a known gap. + +## Binding ([verify.py](verify.py) `load`, checks B1–B12) + +- **The archive.** The selected record and the frontier1094 certificate `ASSEMBLY.json` (1122cb3a…) bind the capsule `selected-replay.tar.gz` (f1da8061…), which batch1099's integration record pins. +- **Exact bytes only.** The checker parses exactly the bytes it hashed. Members are resolved by full path under `candidate/strict/`, never by basename. +- **The certificate chain.** The certificate gives the template (9c4c5142…) and the owner audit (30bafff0…). The owner audit's `source_artifacts` give the raw digests of the gauge44 provider's four files: + + | File | Raw sha256 | + |---|---| + | `CANONICAL-WORD.json.gz` | 16bc0ebb… | + | `CLIFFORD-RECIPES.json` | d0768f21… | + | `CLIFFORD-REVIEW.json` | cb0e10a8… | + | `LOCAL-PROGRAMS.json.gz` | 241fde27… | + +- **The template.** Its gauge44 provider names the same recipes, word and programs, the same ports and centres, and (R, h, v) = (480, 9, 112). +- **SLOT-PINS-k8.** It is listed in the selected source manifest and pins the same recipes, programs and word. +- **Two digests for one word.** 16bc0ebb is the gz-byte digest; the word's payload digest is 4ddb29fb. Each comparison uses the right one. +- **The producer's review** is checked for consistency only, never used as evidence. +- **Canonical encodings** are checked. +- **The global8 twin** is byte-identical. This is informational and never read. +- **Decoys are rejected.** The `split-centres` recipe and word files share the gauge44 files' basenames, so a lookup by basename would pick them up; only the digest binding rejects them. + +## Inventory (checks I1–I7) + +- **Frames.** There are 1,004 independent row lists. Frame 0 is empty and frame 1 is the full frame. +- **Children.** + - The 2,896 child records are exactly the word's directed edges, which include both centre directions, sorted. + - Ranks: 1928 at rank 1, 380 at rank 2, 408 at rank 3, 124 at rank 4, 40 at rank 5 and 16 at rank 8. + - All spans are nested. The only descending records are the 8 centre reversals `(f, 0)`. +- **Relabel coverage.** The climb and centre events of **both** emitted orientations (3,486 climbs and 8 centres each) name exactly these 2,896 keys, with matching ranks. So every climb and centre relabel of the programs has exactly one record. +- **Adapters.** + - The 224 endpoint adapters are ordered (port, source/target). + - Each adapter's `q` is the word's port mask, of weight 3 or 7. + - Source frames are `[q]`; target frames have dimension 8. + - The program's adapter events point to the same frames. +- **Monomials.** All 6,016 monomial records are well formed: fields, ranges, symmetric `Q`, diagonal parity and an invertible `G`. + +## Operator semantics ([clifford.py](clifford.py), written from scratch) + +The kernel imports only the standard library. It was written from the specification: +- the gate definitions of `HyperplaneEnd/Clifford.lean` and `Exact.lean`; +- the producer's code, read only as a specification and never imported. + +**Conventions.** +- Bit i of a basis index is axis i. +- F2 matrices are lists of row bitmasks. +- A circuit is a gate list; the first gate is applied first. + +**Gates.** +- `P(G)` maps |x⟩ ↦ |Gx⟩. +- `X(b)` maps |x⟩ ↦ |x⊕b⟩. +- `D(Q, α)` maps |x⟩ ↦ i^{Σα_i x_i + 2Σ_{i frontier1094 certificate -> capsule -> owner audit/template -> gauge44 CANONICAL-WORD, CLIFFORD-RECIPES, CLIFFORD-REVIEW, LOCAL-PROGRAMS and SLOT-PINS-k8; inventory (2,896 child records = directed edges incl. both centre directions = climb/centre relabel keys of both orientations; ranks, nesting; 224 endpoint adapters; 6,016 monomials well formed); kernel calibration against the Exact.lean literals, #1415's operator digests and #702's 14 frame kernels; every child L F_r R T_old = T_new and every adapter identity exact on all 512 columns with global phase (packed Gaussian integers, beta = 2K+2); 12 semantic mutation controls rejected; RESULT.json byte-identical." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "-m", + "unittest", + "discover", + "-s", + "{package}", + "-p", + "test_package.py" + ], + "timeout_seconds": 300, + "checks": "Standard-library-only imports; projective and column-0-only comparators shown to accept phase and input-character errors that the exact comparator rejects; radix guard, measured digit bound on the 16-gate identities and a collision at beta = 2K; 12 semantic controls; rank-class phase mutants; mutated child and adapter records rejected by evaluate(); receipts list each pair once; I5/I6/I7 and fixture-pin negatives; decoy recipes/word, flipped recipe byte, duplicate key, flipped archive byte and unsafe members rejected; calibration reproduced." + } + ] +} diff --git a/research/frontier1094-recipes-exact-seed76/clifford.py b/research/frontier1094-recipes-exact-seed76/clifford.py new file mode 100644 index 0000000000..6f1e6a38fe --- /dev/null +++ b/research/frontier1094-recipes-exact-seed76/clifford.py @@ -0,0 +1,266 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Independent exact Clifford kernel on C^(2^9) (standard library only; imports no repository code). + +Conventions (README section "Operator semantics"; cross-checked against HyperplaneEnd/Exact.lean, +Clifford.lean and the published #1415 / #702 operator digests): +- a basis index is an int x; bit i of x is axis i (least significant bit = axis 0); +- an F2 matrix is a list of 9 row bitmasks, (Gx)_i = parity(G[i] & x); +- a circuit is a list of gates, the first gate applied first; +- gates: ('P', G) |x> -> |Gx>; ('X', b) |x> -> |x ^ b>; ('D', Q, a) |x> -> i^q(x) |x> with + q(x) = sum_{i in x} a_i + 2 sum_{i> i) & 1) << j for j in range(N_AXES)) for i in range(N_AXES)] + + +def apply_rows(rows, x): + return sum(parity(r & x) << i for i, r in enumerate(rows)) + + +def f2_inverse(rows): + a = [r | (1 << (N_AXES + i)) for i, r in enumerate(rows)] + for j in range(N_AXES): + k = next((i for i in range(j, N_AXES) if (a[i] >> j) & 1), None) + if k is None: + raise ValueError('singular F2 matrix') + a[j], a[k] = a[k], a[j] + for i in range(N_AXES): + if i != j and (a[i] >> j) & 1: + a[i] ^= a[j] + return [r >> N_AXES for r in a] + + +def basis_extend(U): + out = [] + for x in list(U) + [1 << i for i in range(N_AXES)]: + if f2_rank(out + [x]) > len(out): + out.append(x) + return out + + +def fourier(r, sign=1): + """F_r: sqrt(X) (sign = +1) on axes 0..r-1.""" + return [('C', 1 << i, sign) for i in range(r)] + + +def adjoint(circuit): + out = [] + for g in reversed(circuit): + if g[0] == 'P': + out.append(('P', f2_inverse(g[1]))) + elif g[0] == 'D': + out.append(('D', g[1], [(-x) % 4 for x in g[2]])) + elif g[0] == 'C': + out.append(('C', g[1], -g[2])) + elif g[0] == 'PH': + out.append(('PH', (-g[1]) % 4)) + elif g[0] == 'X': + out.append(g) + else: + raise ValueError('unknown gate %r' % (g,)) + return out + + +def frame_parts(U): + """G (columns = extended basis), its inverse, the Z4 form Q = I + Gi^T Gi and its diagonal.""" + r = len(U) + ext = basis_extend(U) + if len(ext) != N_AXES or ext[:r] != list(U): + raise ValueError('frame rows are not independent') + G = transpose(ext) + Gi = f2_inverse(G) + c = transpose(Gi) + Q = [(1 << i) ^ sum(parity(c[i] & c[j]) << j for j in range(N_AXES)) for i in range(N_AXES)] + a = [(Q[i] >> i) & 1 for i in range(N_AXES)] + return G, Gi, Q, a + + +def canonical_frame(U, shortcuts=True): + """T_U = K^-1 F_r K with K = [P(G), D(Q, a)] (the frame's rows used exactly as stored).""" + r = len(U) + if shortcuts and r == 0: + return [] + if shortcuts and r == N_AXES: + return fourier(N_AXES) + G, Gi, Q, a = frame_parts(U) + K = [('P', G), ('D', Q, a)] + return adjoint(K) + fourier(r) + K + + +def monomial(m, order='DPXPH'): + """[D(Q, a), P(G), X(offset), PH(phase)] for a serialized record; order='PDXPH' is a control only.""" + Q, a, G, b, p = m['quadratic_rows'], m['linear_Z4'], m['matrix_rows'], m['offset'], m['phase'] + if order == 'PDXPH': + return [('P', G), ('D', Q, a), ('X', b), ('PH', p)] + if order != 'DPXPH': + raise ValueError(order) + return [('D', Q, a), ('P', G), ('X', b), ('PH', p)] + + +def well_formed(m): + if not isinstance(m, dict) or set(m) != {'linear_Z4', 'matrix_rows', 'offset', 'phase', 'quadratic_rows'}: + return False + Q, a, G = m['quadratic_rows'], m['linear_Z4'], m['matrix_rows'] + if not all(isinstance(x, list) and len(x) == N_AXES and all(type(e) is int for e in x) for x in (Q, a, G)): + return False + if not (all(0 <= e < DIM for e in Q + G) and all(0 <= e < 4 for e in a)): + return False + if not (type(m['offset']) is int and 0 <= m['offset'] < DIM and type(m['phase']) is int and 0 <= m['phase'] < 4): + return False + if not all(((Q[i] >> j) & 1) == ((Q[j] >> i) & 1) for i in range(N_AXES) for j in range(N_AXES)): + return False + if not all(a[i] % 2 == (Q[i] >> i) & 1 for i in range(N_AXES)): + return False + return f2_rank(G) == N_AXES + + +def c_gates(circuit): + return sum(1 for g in circuit if g[0] == 'C') + + +def _z4_phase(Q, a, x): + lin = sum(a[i] for i in range(N_AXES) if (x >> i) & 1) + quad = sum(parity((Q[i] >> (i + 1)) & (x >> (i + 1))) for i in range(N_AXES) if (x >> i) & 1) + return (lin + 2 * quad) % 4 + + +_UNITS = ((1, 0), (0, 1), (-1, 0), (0, -1)) + + +def run(circuit, beta): + """Evaluate the circuit on the packed identity: row y holds sum_x N[y, x] * 2^(beta x), real and imaginary + parts separately, with N = 2^k times the operator matrix. Exact Python integers; no masking or carry.""" + re = [1 << (beta * y) for y in range(DIM)] + im = [0] * DIM + for g in circuit: + kind = g[0] + if kind == 'P': + table = [apply_rows(g[1], x) for x in range(DIM)] + if len(set(table)) != DIM: + raise ValueError('P is not a bijection') + r2, i2 = [0] * DIM, [0] * DIM + for x in range(DIM): + r2[table[x]] = re[x] + i2[table[x]] = im[x] + re, im = r2, i2 + elif kind == 'X': + b = g[1] + re = [re[x ^ b] for x in range(DIM)] + im = [im[x ^ b] for x in range(DIM)] + elif kind in ('D', 'PH'): + r2, i2 = [0] * DIM, [0] * DIM + for x in range(DIM): + k = _z4_phase(g[1], g[2], x) if kind == 'D' else g[1] + a, b = re[x], im[x] + if k == 0: + r2[x], i2[x] = a, b + elif k == 1: + r2[x], i2[x] = -b, a + elif k == 2: + r2[x], i2[x] = -a, -b + else: + r2[x], i2[x] = b, -a + re, im = r2, i2 + elif kind == 'C': + q, s = g[1], g[2] + if s not in (1, -1) or not 0 < q < DIM: + raise ValueError('bad C gate') + r2, i2 = [0] * DIM, [0] * DIM + for x in range(DIM): + a, b = re[x], im[x] + c, d = re[x ^ q], im[x ^ q] + if s == 1: # (1+i)(a+bi) + (1-i)(c+di) + r2[x], i2[x] = a - b + c + d, a + b - c + d + else: # (1-i)(a+bi) + (1+i)(c+di) + r2[x], i2[x] = a + b + c - d, b - a + c + d + re, im = r2, i2 + else: + raise ValueError('unknown gate %r' % (g,)) + return re, im + + +def radix(K): + """beta = 2K + 2: with |numerator components| <= 4^k after k C gates (each C at most quadruples the + largest component; P, X, D, PH permute or negate), scaled differences satisfy |d| <= 2 * 4^K < 2^beta.""" + return 2 * K + 2 + + +def equal(side1, k1, side2, k2, beta): + """Exact equality of the two operators (global phase included): scaled packed rows must coincide.""" + K = max(k1, k2) + if beta < radix(K): + raise ValueError('radix too small for a sound packed comparison') + s1, s2 = K - k1, K - k2 + (r1, i1), (r2, i2) = side1, side2 + return all((r1[y] << s1) == (r2[y] << s2) and (i1[y] << s1) == (i2[y] << s2) for y in range(DIM)) + + +def same_operator(c1, c2): + """Run both circuits at the sound radix and compare exactly.""" + k1, k2 = c_gates(c1), c_gates(c2) + beta = radix(max(k1, k2)) + return equal(run(c1, beta), k1, run(c2, beta), k2, beta) + + +def columns(side, beta): + """Decode packed rows into {x: {y: (re, im)}} numerators (balanced digits; valid when every scaled digit + is below 2^(beta-1) in absolute value).""" + B, half = 1 << beta, 1 << (beta - 1) + out = {} + for y in range(DIM): + digits = [] + for v in side[0][y], side[1][y]: + ds = [] + for _ in range(DIM): + d = v & (B - 1) + if d >= half: + d -= B + ds.append(d) + v = (v - d) >> beta + if v != 0: + raise ValueError('packed row does not decode') + digits.append(ds) + for x in range(DIM): + if digits[0][x] or digits[1][x]: + out.setdefault(x, {})[y] = (digits[0][x], digits[1][x]) + return out + + +def lean_syntax(circuit): + """The circuit in HyperplaneEnd/Exact.lean gate syntax, for structural comparison with its literals.""" + out = [] + for g in circuit: + if g[0] == 'P': + out.append(('pm', list(g[1]), f2_inverse(g[1]))) + elif g[0] == 'D': + out.append(('dg', list(g[1]), list(g[2]))) + elif g[0] == 'C': + out.append(('cg', g[1], g[2] == 1)) + elif g[0] == 'X': + out.append(('xg', g[1])) + else: + out.append(('ph', g[1])) + return out diff --git a/research/frontier1094-recipes-exact-seed76/test_package.py b/research/frontier1094-recipes-exact-seed76/test_package.py new file mode 100644 index 0000000000..d3a2a50786 --- /dev/null +++ b/research/frontier1094-recipes-exact-seed76/test_package.py @@ -0,0 +1,251 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Controls for the independent RecipesExact check (about 20 s). + +Run: python3 -I -B -m unittest discover -s research/frontier1094-recipes-exact-seed76 -p test_package.py -v +""" +import ast +import io +import json +import sys +import tarfile +import tempfile +import unittest +from pathlib import Path + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +import clifford as C # noqa: E402 +import verify as V # noqa: E402 + +DATA, BINDING = V.load() +CHILDREN, ADAPTERS, _ = V.inventory(DATA) +WORD = DATA['word'] +FRAMES = WORD['frames'] +BY_KEY = {(c['old'], c['new']): c for c in CHILDREN} +RESULT = json.loads((HERE / 'RESULT.json').read_text()) + + +class Independence(unittest.TestCase): + def test_kernel_and_verifier_import_only_the_standard_library(self): + allowed = {'argparse', 'gzip', 'hashlib', 'io', 'json', 're', 'sys', 'tarfile', 'time', 'collections', + 'pathlib', 'clifford'} + for name in ('verify.py', 'clifford.py'): + tree = ast.parse((HERE / name).read_text()) + mods = {a.name.split('.')[0] for n in ast.walk(tree) if isinstance(n, ast.Import) for a in n.names} + mods |= {n.module.split('.')[0] for n in ast.walk(tree) if isinstance(n, ast.ImportFrom)} + self.assertLessEqual(mods, allowed, name) + names = {n.id for n in ast.walk(tree) if isinstance(n, ast.Name)} + self.assertFalse(names & set(V.FORBIDDEN), name) + + +class Comparator(unittest.TestCase): + def test_k1_a_projective_comparator_would_accept_a_global_phase_error(self): + c = BY_KEY[(0, 174)] + bad = V._mutate(c, ('left', 'phase'), lambda p: (p + 1) % 4) + c1, c2 = V.child_circuits(bad, FRAMES) + self.assertFalse(C.same_operator(c1, c2)) # the exact comparator rejects it + k1, k2 = C.c_gates(c1), C.c_gates(c2) + beta = C.radix(max(k1, k2)) + s1, s2 = C.run(c1, beta), C.run(c2, beta) + rotated = C.run(c2 + [('PH', 1)], beta) # side2 times i + self.assertTrue(C.equal(s1, k1, rotated, k2, beta)) # equal up to the unit i: projectively equal + + def test_k2_a_column0_comparator_would_accept_an_input_character_error(self): + c = BY_KEY[(0, 2)] + bad = V._mutate(c, ('right', 'linear_Z4'), lambda a: a[:5] + [(a[5] + 2) % 4] + a[6:]) + c1, c2 = V.child_circuits(bad, FRAMES) + self.assertFalse(C.same_operator(c1, c2)) + k = max(C.c_gates(c1), C.c_gates(c2)) + beta = C.radix(k) + col1 = C.columns(C.run(c1, beta), beta) + col2 = C.columns(C.run(c2, beta), beta) + sc1, sc2 = 1 << (k - C.c_gates(c1)), 1 << (k - C.c_gates(c2)) + scale = lambda col, s: {y: (re * s, im * s) for y, (re, im) in col.items()} # noqa: E731 + self.assertEqual(scale(col1[0], sc1), scale(col2[0], sc2)) # column 0 alone cannot see it + self.assertNotEqual(scale(col1[32], sc1), scale(col2[32], sc2)) # column e5 does + + def test_k3_radix_guard(self): + s = C.run([], 4) + with self.assertRaises(ValueError): + C.equal(s, 1, s, 1, 3) + + def test_digit_bound_on_the_largest_identities(self): + # the lemma behind beta = 2K + 2: after k C gates every numerator component is at most 4^k, so the scaled + # digit difference of the two sides is at most 2 * 4^K < 2^(2K+2); check the bound on the K = 16 centre children + for key in ((415, 0), (418, 0)): + c1, c2 = V.child_circuits(BY_KEY[key], FRAMES) + k = C.c_gates(c1) + self.assertEqual(k, 16) + beta = C.radix(k) + biggest = max(max(abs(re), abs(im)) for col in C.columns(C.run(c1, beta), beta).values() for re, im in col.values()) + self.assertLessEqual(biggest, 4 ** k) + + def test_radix_2k_would_be_unsound(self): + # at beta = 2K a digit difference of 4^K is allowed by the bound, and (4^K, -1) packs to zero: a collision + K = 3 + B = 1 << (2 * K) + self.assertEqual(4 ** K * B ** 0 + (-1) * B ** 1, 0) + self.assertLessEqual(4 ** K, 2 * 4 ** K) + # at beta = 2K + 2 the same digits cannot cancel + B2 = 1 << C.radix(K) + self.assertNotEqual(4 ** K - B2, 0) + self.assertLess(2 * 4 ** K, B2) + + +class Semantics(unittest.TestCase): + def test_all_semantic_controls_reject(self): + out = V.semantic_controls(CHILDREN, ADAPTERS, WORD) + self.assertEqual(out, RESULT['controls']) + self.assertEqual(len(out), 12) + + def test_rank_off_by_one_is_rejected_structurally_and_by_the_evaluator(self): + c = dict(BY_KEY[(0, 174)], rank=2) + bad = {'children': [c if (x['old'], x['new']) == (0, 174) else x for x in CHILDREN], + 'endpoint_adapters': ADAPTERS} + with self.assertRaisesRegex(V.Reject, 'I3 child rank'): + V.inventory(dict(DATA, recipes=bad)) + self.assertFalse(C.same_operator(*V.child_circuits(c, FRAMES))) + + def test_swapped_matrix_rows_and_adapter_phase_are_rejected(self): + c = V._mutate(BY_KEY[(0, 415)], ('left', 'matrix_rows'), lambda G: [G[1], G[0]] + G[2:]) + self.assertFalse(C.same_operator(*V.child_circuits(c, FRAMES))) + x = V._mutate(ADAPTERS[1], ('left', 'phase'), lambda p: (p + 1) % 4) + self.assertFalse(C.same_operator(*V.adapter_circuits(x, WORD))) + + def test_every_rank_class_has_a_rejected_phase_mutant(self): + seen = set() + for c in CHILDREN: + if c['rank'] in seen: + continue + seen.add(c['rank']) + bad = V._mutate(c, ('left', 'phase'), lambda p: (p + 1) % 4) + self.assertTrue(C.same_operator(*V.child_circuits(c, FRAMES)), c['rank']) + self.assertFalse(C.same_operator(*V.child_circuits(bad, FRAMES)), c['rank']) + self.assertEqual(seen, {1, 2, 3, 4, 5, 8}) + + +class Binding(unittest.TestCase): + def test_d1_decoy_recipes_rejected(self): + with self.assertRaisesRegex(V.Reject, 'B6 provider file digest: recipes'): + V.load(member_overrides={'recipes': V.CASES['decoys']['recipes']}) + + def test_d2_decoy_word_rejected(self): + with self.assertRaisesRegex(V.Reject, 'B6 provider file digest: canonical_word'): + V.load(member_overrides={'canonical_word': V.CASES['decoys']['canonical_word']}) + + def test_d3_one_phase_digit_changed_in_the_recipe_bytes(self): + raw = V.canonical_bytes(DATA['recipes']) + i = raw.index(b'"phase":0') + flipped = raw[:i] + b'"phase":1' + raw[i + 9:] + with self.assertRaisesRegex(V.Reject, 'B6 provider file digest: recipes'): + V.load(byte_overrides={'recipes': flipped}) + + def test_d4_duplicate_json_key(self): + with self.assertRaisesRegex(V.Reject, 'duplicate JSON key'): + V.strict_loads(b'{"a":1,"a":2}') + + def _archive(self, mutate): + raw = (V.ROOT / V.CASES['archive']['path']).read_bytes() + return mutate(raw) + + def test_archive_byte_flip(self): + with tempfile.TemporaryDirectory() as d: + raw = self._archive(lambda b: b[:-1] + bytes([b[-1] ^ 1])) + p = Path(d) / 'a.tar.gz' + p.write_bytes(raw) + with self.assertRaisesRegex(V.Reject, 'B1 archive digest'): + V.load(archive_path=p) + + def test_unsafe_archive_members(self): + for name in ('../escape', 'dup'): + buf = io.BytesIO() + with tarfile.open(fileobj=buf, mode='w') as tar: + for n in ([name] if name != 'dup' else ['dup', 'dup']): + info = tarfile.TarInfo(n) + info.size = 0 + tar.addfile(info, io.BytesIO(b'')) + buf.seek(0) + with tarfile.open(fileobj=buf, mode='r') as tar: + with self.assertRaisesRegex(V.Reject, 'B2'): + V.safe_members(tar) + + def test_binding_is_recorded(self): + self.assertEqual(BINDING, RESULT['binding']) + self.assertTrue(BINDING['global8_twin_byte_identical']) + + +class Coverage(unittest.TestCase): + def test_result_covers_every_record_and_column(self): + ev = RESULT['evaluation'] + self.assertEqual((ev['children'], ev['adapters'], ev['columns']), (2896, 224, 512)) + self.assertTrue(ev['global_phase_included']) + self.assertEqual(sum(ev['K_histogram'].values()), 2896) + + def test_subset_counts_one_child_and_one_port(self): + out = V.evaluate(CHILDREN, ADAPTERS, WORD, subset='pair=0:174,ports=5') + self.assertEqual((out['children'], out['adapters']), (1, 2)) + + def test_evaluator_rejects_a_mutated_child_record(self): + bad = [V._mutate(c, ('right', 'linear_Z4'), lambda a: a[:5] + [(a[5] + 2) % 4] + a[6:]) + if (c['old'], c['new']) == (0, 174) else c for c in CHILDREN] + with self.assertRaisesRegex(V.Reject, 'E child 0:174'): + V.evaluate(bad, ADAPTERS, WORD, subset='pair=0:174,adapters=none') + + def test_evaluator_rejects_a_mutated_adapter_record(self): + bad = [V._mutate(x, ('left', 'phase'), lambda p: (p + 1) % 4) if (x['port'], x['role']) == (3, 'target') else x + for x in ADAPTERS] + with self.assertRaisesRegex(V.Reject, 'E adapter 3 target'): + V.evaluate(CHILDREN, bad, WORD, subset='children=none,ports=3') + + def test_receipts_list_each_selected_pair_once(self): + with tempfile.TemporaryDirectory() as d: + path = Path(d) / 'r.jsonl' + V.evaluate(CHILDREN, ADAPTERS, WORD, subset='dim=1..2,adapters=none', receipts=path) + lines = [json.loads(x) for x in path.read_text().splitlines()] + pairs = [tuple(pq) for x in lines if x['kind'] == 'children' for pq in x['pairs']] + expect = [(c['old'], c['new']) for c in CHILDREN if 1 <= len(FRAMES[c['new']]) <= 2] + self.assertEqual(sorted(pairs), sorted(expect)) + self.assertEqual(len(pairs), len(set(pairs))) + + +class Inventory(unittest.TestCase): + def _programs(self, mutate): + progs = json.loads(json.dumps(DATA['programs'])) + mutate(progs) + return dict(DATA, programs=progs) + + def test_i5_a_dropped_climb_event_is_rejected(self): + def drop(progs): + i = next(n for n, e in enumerate(progs['forward']) if e[0] == 'climb') + del progs['forward'][i] + with self.assertRaisesRegex(V.Reject, 'I5'): + V.inventory(self._programs(drop)) + + def test_i6_a_moved_adapter_frame_is_rejected(self): + def move(progs): + i = next(n for n, e in enumerate(progs['forward']) if e[0] == 'adapter' and e[1] == 'old_to_new' and e[2] == 0) + progs['forward'][i] = progs['forward'][i][:3] + [progs['forward'][i][3] + 1] + with self.assertRaisesRegex(V.Reject, 'I6'): + V.inventory(self._programs(move)) + + def test_i7_an_asymmetric_q_is_rejected(self): + recipes = json.loads(json.dumps(DATA['recipes'])) + Q = recipes['children'][0]['left']['quadratic_rows'] + Q[0] ^= 1 << 5 # Q_05 set without Q_50 + with self.assertRaisesRegex(V.Reject, 'I7'): + V.inventory(dict(DATA, recipes=recipes)) + + def test_calibration_runs_and_a_wrong_fixture_pin_is_rejected(self): + out = V.calibrate(FRAMES) + self.assertEqual(out, RESULT['calibration']) + saved = V.CASES['fixtures']['pr702']['sha256'] + try: + V.CASES['fixtures']['pr702']['sha256'] = '0' * 64 + with self.assertRaisesRegex(V.Reject, 'FX3 #702 EXPECTED pinned'): + V.calibrate(FRAMES) + finally: + V.CASES['fixtures']['pr702']['sha256'] = saved + + +if __name__ == '__main__': + unittest.main() diff --git a/research/frontier1094-recipes-exact-seed76/verify.py b/research/frontier1094-recipes-exact-seed76/verify.py new file mode 100644 index 0000000000..8775d15e74 --- /dev/null +++ b/research/frontier1094-recipes-exact-seed76/verify.py @@ -0,0 +1,624 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Independent phase-exact check of the selected frontier1094 word's stored Clifford recipes (no new kappa). + +Usage: python3 -I -B research/frontier1094-recipes-exact-seed76/verify.py [--write] [--subset SPEC] [--receipts PATH] + +Lemma G's RecipesExact premise (research/e8-lemma-g-lean/LemmaG/Stream.lean:110-112) says every relabel of +the stream executes T_B o T_A^-1. For the selected gauge44 provider this script checks, with a kernel written +from scratch (clifford.py, standard library only; no producer code is imported): + + B the byte binding: selected record -> frontier1094 certificate -> capsule -> owner audit / template -> + CANONICAL-WORD, CLIFFORD-RECIPES, CLIFFORD-REVIEW, LOCAL-PROGRAMS (and SLOT-PINS-k8); + I the inventory: the 2,896 child records are exactly the word's directed edges (with both centre + directions) and exactly the climb and centre relabel keys of both emitted orientations; ranks, nesting, + and the 224 endpoint adapters with their ports and frames; every monomial record well formed; + FX calibration of the kernel against independent published values: the Lean literals of + HyperplaneEnd/Exact.lean (gate lists and the rank-7 pair identities), the #1415 operator digests and + the #702 frame-kernel digests, plus hand values and basis-dependence checks; + E every child: L o F_r o R o T_old = T_new, and every endpoint adapter: M o C_q = T_start (source) and + M o F_9 o C_q^-1 = T_final (target), exactly on all 512 columns of C^(2^9), global phase included, + by packed exact Gaussian-integer evaluation at the sound radix beta = 2K + 2; + C semantic mutation controls on a fixed sample (each must be rejected), and a positive basis control. + +Expected last line: PASS_FRONTIER1094_RECIPES_EXACT (PARTIAL_FRONTIER1094_RECIPES_EXACT for --subset). +""" +import argparse +import gzip +import hashlib +import io +import json +import re +import sys +import tarfile +import time +from collections import Counter +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +sys.path.insert(0, str(HERE)) +import clifford as C # noqa: E402 + +CASES = json.loads((HERE / 'CASES.json').read_text()) +FORBIDDEN = ('clifford_exact', 'lower_child', 'phases_full', 'sparse_state', 'fast_state', 'lg_phys') + + +class Reject(Exception): + """A check failed; the argument is the label of the check.""" + + +def need(ok, label): + if not ok: + raise Reject(label) + + +def sha(data): + return hashlib.sha256(data).hexdigest() + + +def strict_loads(data): + def hook(pairs): + out = {} + for k, v in pairs: + if k in out: + raise Reject('P duplicate JSON key: ' + k) + out[k] = v + return out + return json.loads(data, object_pairs_hook=hook) + + +def canonical_bytes(obj): + return json.dumps(obj, sort_keys=True, separators=(',', ':')).encode() + + +def find_pin(obj, key, value): + if isinstance(obj, dict): + return any((k == key and v == value) or find_pin(v, key, value) for k, v in obj.items()) + if isinstance(obj, list): + return any(find_pin(v, key, value) for v in obj) + return False + + +def safe_members(tar): + names = Counter() + for info in tar.getmembers(): + names[info.name] += 1 + need(info.isreg() or info.isdir(), 'B2 archive members are regular files') + need(not info.name.startswith('/') and '..' not in Path(info.name).parts, 'B2 archive member paths') + need(all(n == 1 for n in names.values()), 'B2 archive member names are unique') + return {info.name: info for info in tar.getmembers()} + + +# ------------------------------------------------------------------------------------------------ binding +def load(archive_path=None, member_overrides=None, byte_overrides=None): + """Check the byte binding (B1-B12) and return the decoded inputs. The keyword arguments exist only for the + packaging controls in test_package.py (decoy members, flipped bytes).""" + arc = CASES['archive'] + raw = (Path(archive_path) if archive_path else ROOT / arc['path']).read_bytes() + need(sha(raw) == arc['sha256'], 'B1 archive digest') + need(find_pin(json.loads((ROOT / arc['pinned_by']).read_text()), arc['path'], arc['sha256']), 'B1 archive pin') + members = dict(CASES['members'], **(member_overrides or {})) + with tarfile.open(fileobj=io.BytesIO(raw), mode='r:gz') as tar: # parse exactly the hashed bytes + index = safe_members(tar) + + def member(path): + full = CASES['prefix'] + path + need(full in index, 'B2 archive member present: ' + path) + return tar.extractfile(index[full]).read() + got = {k: member(p) for k, p in members.items()} + twin = {k: member(CASES['twin_prefix'] + Path(p).name) for k, p in CASES['members'].items() + if p.startswith('global/base/providers/gauge44/')} + got.update(byte_overrides or {}) + # B3 certificate and record + repo_asm = (ROOT / CASES['certificate']).read_bytes() + need(repo_asm == got['assembly'] and sha(repo_asm) == CASES['certificate_sha256'], 'B3 certificate') + # only the selected record, or the frontier1094 checkpoint once the frontier moves on + records = [ROOT / CASES['selected_record'], ROOT / CASES['checkpoint_dir'] / 'frontier1094.json'] + named = False + for f in records: + try: + rec = json.loads(f.read_text()) if f.is_file() else {} + except ValueError: + rec = {} + rec = rec if isinstance(rec, dict) else {} + named = named or (rec.get('certificate') == CASES['certificate'] and rec.get('certificate_sha256') == sha(repo_asm)) + need(named, 'B3 a selected or checkpoint record names the certificate') + asm = strict_loads(got['assembly']) + # B4 template, B5 owner audit + template_raw = gzip.decompress(got['template']) + need(sha(template_raw) == asm['template_sha256'], 'B4 template digest') + need(sha(got['owner_audit']) == asm['input_sha256']['owner_audit'], 'B5 owner audit digest') + audit = strict_loads(got['owner_audit']) + need(audit['template_sha256'] == asm['template_sha256'], 'B5 owner audit template') + # B6 raw-byte digests of the provider files, from the owner audit + for key, art in CASES['source_artifact_keys'].items(): + need(sha(got[key]) == audit['source_artifacts'][art], 'B6 provider file digest: ' + key) + word_raw = gzip.decompress(got['canonical_word']) + programs_raw = gzip.decompress(got['local_programs']) + word, recipes = strict_loads(word_raw), strict_loads(got['recipes']) + programs, review = strict_loads(programs_raw), strict_loads(got['review']) + template = strict_loads(template_raw) + # B7 the template's gauge44 provider binds the same files and word parameters + t = template['local_providers']['gauge44'] + need(t['exact_local_clifford_recipe_sha256'] == sha(got['recipes']), 'B7 template binds the recipes') + need(t['canonical_word_sha256'] == sha(got['canonical_word']), 'B7 template binds the word') + need(t['local_programs_sha256'] == sha(got['local_programs']) and t['local_programs'] == programs, 'B7 template binds the programs') + need(t['ports'] == word['ports'] and t['centers'] == word['centers'], 'B7 template ports and centres') + exp = CASES['expected'] + need((t['R'], t['h'], t['v']) == (word['R'], word['h'], word['v']) == (exp['R'], exp['h'], exp['v']), 'B7 word parameters') + # B8 SLOT-PINS (repository file listed in the selected source manifest) + ss, sp = CASES['selected_source'], CASES['slot_pins'] + ss_raw = (ROOT / ss['path']).read_bytes() + need(sha(ss_raw) == ss['sha256'] and find_pin(json.loads((ROOT / arc['pinned_by']).read_text()), ss['path'], ss['sha256']), + 'B8 selected source manifest pinned') + sp_raw = (ROOT / sp['path']).read_bytes() + need(sha(sp_raw) == sp['sha256'] and find_pin(strict_loads(ss_raw), sp['path'], sp['sha256']), + 'B8 SLOT-PINS pinned by path in the source manifest') + pins = strict_loads(sp_raw) + need(pins['canonical_sha256'] == sha(word_raw), 'B8 SLOT-PINS word payload digest') # payload, not gz bytes (B9) + need(pins['clifford_recipes_sha256'] == sha(got['recipes']), 'B8 SLOT-PINS recipes digest') + need(all(pins['program_sha256'][o] == sha(json.dumps(programs[o], separators=(',', ':')).encode()) + for o in ('forward', 'backward')), 'B8 SLOT-PINS program digests') + # B10 the producer's review: consistency only, never evidence + need(review['status'] == exp['review_status'] and review['recipe_sha256'] == sha(got['recipes']) + and review['canonical_word_sha256'] == sha(got['canonical_word']), 'B10 review binds the same files') + # B11 canonical encodings + need(got['recipes'] == canonical_bytes(recipes) and word_raw == canonical_bytes(word), 'B11 canonical encodings') + binding = dict(record_or_checkpoint='certificates/selected-result.json or certificates/checkpoints/frontier1094.json', + certificate=CASES['certificate'], certificate_sha256=sha(repo_asm), archive=arc['path'], + archive_sha256=arc['sha256'], template_sha256=asm['template_sha256'], + owner_audit_sha256=asm['input_sha256']['owner_audit'], + recipes_sha256=sha(got['recipes']), canonical_word_gz_sha256=sha(got['canonical_word']), + canonical_word_payload_sha256=sha(word_raw), local_programs_gz_sha256=sha(got['local_programs']), + review_sha256=sha(got['review']), slot_pins_sha256=sp['sha256'], + global8_twin_byte_identical=all(twin[k] == got[k] for k in twin)) # B12, informational + return dict(word=word, recipes=recipes, programs=programs, review=review), binding + + +# ------------------------------------------------------------------------------------------------ inventory +def is_int(x): + return type(x) is int + + +def nested(small, large): + return C.f2_rank(list(large)) == C.f2_rank(list(large) + list(small)) + + +def inventory(data): + """I1-I7. Returns (children, adapters, counts).""" + word, recipes, programs = data['word'], data['recipes'], data['programs'] + exp = CASES['expected'] + frames, v = word['frames'], word['v'] + # I1 frames + need(len(frames) == exp['frames'], 'I1 frame count') + need(all(isinstance(U, list) and all(is_int(x) and 0 < x < C.DIM for x in U) and C.f2_rank(U) == len(U) + for U in frames), 'I1 frames are independent row lists') + need(frames[0] == [] and frames[1] == [1 << i for i in reversed(range(C.N_AXES))], 'I1 empty and full frames') + dims = Counter(str(len(U)) for U in frames) + need(dict(dims) == exp['frame_dims'], 'I1 frame dimensions') + centres = word['center_frames'] + need(all(len(frames[f]) == 8 for f in centres), 'I1 centre frames have dimension 8') + # I2 children = directed edges (+ both centre directions) + edges = [tuple(e) for e in word['edges']] + E = set(edges) | {(f, 0) for f in centres} | {(0, f) for f in centres} + need(len(edges) == len(set(edges)) and set(edges) == E and len(E) == exp['children'], 'I2 edge inventory') + children = recipes['children'] + need(set(recipes) == {'children', 'endpoint_adapters'}, 'I2 recipe file keys') + need([(c['old'], c['new']) for c in children] == sorted(E), 'I2 one record per edge, sorted') + # I3 each child + ranks = Counter() + descending = 0 + for c in children: + need(set(c) == {'left', 'new', 'old', 'rank', 'right'} and isinstance(c['right'], dict), 'I3 child keys') + a, b, r = c['old'], c['new'], c['rank'] + need(is_int(r) and r >= 1 and r == abs(len(frames[a]) - len(frames[b])), 'I3 child rank') + small, large = (frames[a], frames[b]) if len(frames[a]) < len(frames[b]) else (frames[b], frames[a]) + need(nested(small, large), 'I3 nested spans') + if len(frames[a]) > len(frames[b]): + descending += 1 + need(b == 0 and a in centres, 'I3 only centre reversals descend') + ranks[str(r)] += 1 + need(dict(ranks) == exp['child_ranks'] and descending == exp['descending_children'], 'I3 rank histogram') + # I4 endpoint adapters + adapters = recipes['endpoint_adapters'] + need([(x['port'], x['role']) for x in adapters] == [(p, r) for p in range(v) for r in ('source', 'target')], + 'I4 adapter order') + for x in adapters: + need(set(x) == {'frame', 'left', 'port', 'rank', 'right', 'role'} and x['rank'] == 0 and x['right'] is None, + 'I4 adapter keys') + p = x['port'] + if x['role'] == 'source': + need(x['frame'] == word['start'][p] and frames[x['frame']] == [word['ports'][p]], 'I4 source frame') + else: + need(x['frame'] == word['final'][v + p] and len(frames[x['frame']]) == 8, 'I4 target frame') + need(dict(Counter(str(bin(q).count('1')) for q in word['ports'])) == exp['port_weights'], 'I4 port weights') + # I5 / I6 program events + keys = set() + for o in ('forward', 'backward'): + ev = Counter() + okeys = set() + for e in programs[o]: + if e[0] == 'climb': + key = (e[3], e[4]) + need(key in E and e[5] == abs(len(frames[e[3]]) - len(frames[e[4]])), 'I5 climb key and rank') + okeys.add(key) + ev['climb'] += 1 + elif e[0] == 'center': + f = centres[e[1]] + need((e[2], e[3]) == ((f, 0) if o == 'forward' else (0, f)) and e[4] == 8, 'I5 centre key') + okeys.add((e[2], e[3])) + ev['center'] += 1 + elif e[0] == 'adapter': + _, way, r, f = e + if way == 'old_to_new': + need(f == (word['start'][r] if r < v else 0), 'I6 entry adapter frame') + else: + need(way == 'new_to_old' and f == (word['final'][r] if v <= r < 2 * v else 1), 'I6 exit adapter frame') + ev['adapter'] += 1 + need(dict(ev) == exp['events_per_orientation'], 'I5 event counts: ' + o) + keys |= okeys + need(keys == E, 'I5 relabel keys of both orientations = the record inventory') + need(all(word['final'][p] == 1 for p in range(v)), 'I6 every source port ends in the full frame') + # I7 monomials + monos = [c[s] for c in children for s in ('left', 'right')] + [x['left'] for x in adapters] + need(all(C.well_formed(m) for m in monos), 'I7 monomial records well formed') + return children, adapters, dict(child_ranks=dict(sorted(ranks.items())), descending=descending, monomials=len(monos), + relabel_keys=len(keys), frames=len(frames)) + + +# ------------------------------------------------------------------------------------------------ calibration +def lean_fixtures(): + fx = CASES['fixtures']['lean_exact'] + raw = (ROOT / fx['path']).read_bytes() + need(sha(raw) == fx['sha256'], 'FX1 Exact.lean pinned') + text = raw.decode() + num = r'\[([\d,\s]*)\]' + + def ints(s): + return [int(x) for x in re.findall(r'\d+', s)] + + def gates(name): + m = re.search(r'^def %s : List Gate :=\n(.*?)\n\n' % name, text, re.S | re.M) + need(m is not None, 'FX1 literal present: ' + name) + out = [] + for g in re.finditer(r'\.(dg|pm)\s*' + num + r'\s*' + num + r'|\.cg\s+(\d+)\s+(true|false)|\.(xg|ph)\s+(\d+)', m.group(1)): + if g.group(1): + out.append((g.group(1), ints(g.group(2)), ints(g.group(3)))) + elif g.group(4): + out.append(('cg', int(g.group(4)), g.group(5) == 'true')) + else: + out.append((g.group(6), int(g.group(7)))) + return out + mono = r'⟨' + num + r',\s*' + num + r',\s*' + num + r',\s*(\d+),\s*(\d+)⟩' + pairs = [] + for k in (1, 2, 3): + m = re.search(r'def pair%d : Pair := ⟨' % k + num + r',\s*' + num + r',\s*' + mono + r',\s*' + mono + r'⟩', text) + need(m is not None, 'FX1 pair literal %d' % k) + g = m.groups() + + def as_mono(i): + return dict(quadratic_rows=ints(g[i]), linear_Z4=ints(g[i + 1]), matrix_rows=ints(g[i + 2]), + offset=int(g[i + 3]), phase=int(g[i + 4])) + pairs.append(dict(E=ints(g[0]), U=ints(g[1]), L=as_mono(2), R=as_mono(7), + fE=gates('fE%d' % k), fU=gates('fU%d' % k), wL=gates('wL%d' % k), wR=gates('wR%d' % k))) + return pairs + + +def matrix_digest_1415(circuit): + """#1415's operator digest: per column x, reduce by 2 while all numerators are even, hash + [e, [[y, re, im] ...]] lines (hpe-lean-semantic-binding/verify.py).""" + k = C.c_gates(circuit) + beta = C.radix(k) + cols = C.columns(C.run(circuit, beta), beta) + h, dens, nonzero = hashlib.sha256(), set(), 0 + for x in range(C.DIM): + col, e = dict(cols.get(x, {})), k + while e > 0 and all(re_ % 2 == 0 and im % 2 == 0 for re_, im in col.values()): + col = {y: (re_ // 2, im // 2) for y, (re_, im) in col.items()} + e -= 1 + dens.add(e) + nonzero += len(col) + h.update((json.dumps([e, [[y, col[y][0], col[y][1]] for y in sorted(col)]], sort_keys=True, separators=(',', ':')) + '\n').encode()) + return h.hexdigest(), sorted(dens), nonzero + + +def kernel_digest_702(circuit): + """#702's frame-kernel digest: numerators over 2^k, unreduced, column by column (cold-wrapper-amplitude-audit).""" + k = C.c_gates(circuit) + beta = C.radix(k) + cols = C.columns(C.run(circuit, beta), beta) + body = [[[y, cols[x][y][0], cols[x][y][1]] for y in sorted(cols.get(x, {}))] for x in range(C.DIM)] + return sha(json.dumps(body, sort_keys=True, separators=(',', ':')).encode()), k + + +def calibrate(frames): + out = {} + # FX1 Lean literals: gate lists and the three rank-7 pair identities (Exact.lean check1-3) + pairs = lean_fixtures() + for k, p in enumerate(pairs, 1): + need(C.lean_syntax(C.canonical_frame(p['E'])) == p['fE'], 'FX1 canon(E%d) = fE%d' % (k, k)) + need(C.lean_syntax(C.canonical_frame(p['U'])) == p['fU'], 'FX1 canon(U%d) = fU%d' % (k, k)) + need(C.lean_syntax(C.monomial(p['L'])) == p['wL'] and C.lean_syntax(C.monomial(p['R'])) == p['wR'], + 'FX1 monomials %d' % k) + need(C.same_operator(C.canonical_frame(p['E']) + C.monomial(p['R']) + C.fourier(7) + C.monomial(p['L']), + C.canonical_frame(p['U'])), 'FX1 pair %d identity' % k) + out['lean_exact'] = '3 pairs: canon gate lists, monomial gate lists and rank-7 identities equal the Exact.lean literals' + # FX2 #1415 operator digests of T_U o T_E^-1 (exercises the adjoint) + fx = CASES['fixtures']['pr1415'] + raw = (ROOT / fx['path']).read_bytes() + need(sha(raw) == fx['sha256'], 'FX2 #1415 RESULT pinned') + for k, (f, p) in enumerate(zip(strict_loads(raw)['factorizations'], pairs), 1): + need(f['entrance'] == p['E'] and f['terminal'] == p['U'], 'FX2 pair frames %d' % k) + digest, dens, nonzero = matrix_digest_1415(C.adjoint(C.canonical_frame(p['E'])) + C.canonical_frame(p['U'])) + need(digest == f['left']['matrix_sha256'] and dens == f['left']['denominator_exponents'] + and nonzero == f['left']['nonzero_entries'], 'FX2 #1415 digest %d' % k) + out['pr1415'] = '3 operator digests of T_U o T_E^-1 reproduced' + # FX3 #702 frame kernels: all 14 are frames of this word + fx = CASES['fixtures']['pr702'] + raw = (ROOT / fx['path']).read_bytes() + need(sha(raw) == fx['sha256'], 'FX3 #702 EXPECTED pinned') + index = {tuple(U): i for i, U in enumerate(frames)} + found = [] + for ident in strict_loads(raw)['identities']: + U = ident['frame'] + need(tuple(U) in index, 'FX3 #702 frame is a word frame') + digest, k = kernel_digest_702(C.canonical_frame(U)) + need(digest == ident['kernel_sha256'] and (1 << k) == ident['amplitude_denominator'], 'FX3 #702 kernel digest') + found.append(index[tuple(U)]) + out['pr702'] = '%d frame kernels reproduced (word frames %s)' % (len(found), sorted(found)) + # FX5 hand values; FX6 shortcut agreement; FX7 basis dependence + cols = C.columns(C.run(C.canonical_frame(frames[2]), C.radix(1)), C.radix(1)) + need(frames[2] == [30] and cols[0] == {0: (1, 1), 30: (-1, -1)} and cols[1] == {1: (1, 1), 31: (-1, -1)}, 'FX5 T([30])') + need(C.same_operator(C.canonical_frame(frames[1], shortcuts=False), C.fourier(9)) + and C.same_operator(C.canonical_frame(frames[0], shortcuts=False), []), 'FX6 shortcuts agree') + for f in (174, 415): + U = frames[f] + need(C.same_operator(C.canonical_frame(list(reversed(U))), C.canonical_frame(U)), 'FX7 reordered rows: same T') + need(not C.same_operator(C.canonical_frame([U[0] ^ U[1]] + U[1:]), C.canonical_frame(U)), 'FX7 other basis: other T') + out['hand_and_structure'] = 'hand values, shortcut agreement and basis dependence' + return out + + +# ------------------------------------------------------------------------------------------------ evaluation +def child_circuits(c, frames, variant=None): + """side1 = T_old + R + F_r + L (first applied first), side2 = T_new; variant selects a mutation control.""" + a, b, r = c['old'], c['new'], c['rank'] + L, R = c['left'], c['right'] + Fr = C.fourier(r) + order = 'DPXPH' + if variant == 'one_gate': + Fr = [('C', (1 << r) - 1, 1)] + elif variant == 'fourier_sign': + Fr = [('C', 1, -1)] + Fr[1:] + elif variant == 'swap_wrappers': + L, R = R, L + elif variant == 'direction': + a, b = b, a + elif variant == 'gate_order': + order = 'PDXPH' + return C.canonical_frame(frames[a]) + C.monomial(R, order) + Fr + C.monomial(L, order), C.canonical_frame(frames[b]) + + +def adapter_circuits(x, word, variant=None): + p, role, frames = x['port'], x['role'], word['frames'] + q = word['ports'][(p + 1) % word['v']] if variant == 'port' else word['ports'][p] + if variant == 'role': + role = 'target' if role == 'source' else 'source' + order = 'PDXPH' if variant == 'gate_order' else 'DPXPH' + sign = -1 if variant == 'fourier_sign' else 1 + M = C.monomial(x['left'], order) + T = C.canonical_frame(frames[x['frame']]) + if role == 'source': + return [('C', q, sign)] + M, T + return [('C', q, -sign)] + C.fourier(9) + M, T + + +def check_pair(c1, c2): + return C.same_operator(c1, c2) + + +def evaluate(children, adapters, word, subset=None, receipts=None): + """Every child and adapter identity, exact on all 512 columns. Returns counts and the K histogram.""" + frames = word['frames'] + sel_c, sel_a = subset_filter(subset, children, adapters, frames) + groups = {} + for c in sel_c: + groups.setdefault(c['new'], []).append(c) + order = sorted(groups, key=lambda b: (len(frames[b]), b)) + Ks = Counter() + chain = hashlib.sha256(b'').hexdigest() + lines = [] + + def emit(obj): + nonlocal chain + line = canonical_bytes(dict(obj, prev=chain)) + chain = sha(line) + lines.append(line) + emit(dict(kind='header', schema=1, checker_sha256=sha((HERE / 'verify.py').read_bytes()), + kernel_sha256=sha((HERE / 'clifford.py').read_bytes()), radix_rule='beta=2K+2', subset=subset)) + t0 = time.process_time() + done_c = 0 + for b in order: + grp = groups[b] + k2 = C.c_gates(C.canonical_frame(frames[b])) + Kmax = max(max(len(frames[c['old']]) + c['rank'], k2) for c in grp) + beta = C.radix(Kmax) + side2 = C.run(C.canonical_frame(frames[b]), beta) + for c in grp: + c1, _ = child_circuits(c, frames) + k1 = C.c_gates(c1) + need(C.equal(C.run(c1, beta), k1, side2, k2, beta), 'E child %d:%d' % (c['old'], c['new'])) + Ks[max(k1, k2)] += 1 + done_c += 1 + emit(dict(kind='children', new=b, dim_new=len(frames[b]), K=Kmax, beta=beta, + pairs=[[c['old'], c['new']] for c in grp], status='EXACT')) + done_a = 0 + for x in sel_a: + c1, c2 = adapter_circuits(x, word) + need(check_pair(c1, c2), 'E adapter %d %s' % (x['port'], x['role'])) + done_a += 1 + emit(dict(kind='adapter', port=x['port'], role=x['role'], frame=x['frame'], status='EXACT')) + if subset is None: + emit(dict(kind='complete', children=done_c, adapters=done_a)) + if receipts: + Path(receipts).write_bytes(b'\n'.join(lines) + b'\n') + return dict(children=done_c, adapters=done_a, K_histogram={str(k): n for k, n in sorted(Ks.items())}, + receipts_sha256=sha(b'\n'.join(lines) + b'\n'), cpu_seconds=round(time.process_time() - t0, 1)) + + +def subset_filter(spec, children, adapters, frames): + if spec is None: + return children, adapters + sc, sa = list(children), list(adapters) + for term in spec.split(','): + key, _, val = term.partition('=') + if key == 'dim': + lo, _, hi = val.partition('..') + lo, hi = int(lo), int(hi or lo) + sc = [c for c in sc if lo <= len(frames[c['new']]) <= hi] + elif key == 'rank': + sc = [c for c in sc if c['rank'] == int(val)] + elif key == 'pair': + a, b = map(int, val.split(':')) + sc = [c for c in sc if (c['old'], c['new']) == (a, b)] + elif key == 'ports': + lo, _, hi = val.partition('-') + sa = [x for x in sa if int(lo) <= x['port'] <= int(hi or lo)] + elif key == 'children' and val == 'none': + sc = [] + elif key == 'adapters' and val == 'none': + sa = [] + else: + raise SystemExit('unknown subset term: ' + term) + return sc, sa + + +# ------------------------------------------------------------------------------------------------ controls +SAMPLE_CHILDREN = ((0, 2), (0, 174), (37, 1), (0, 415), (415, 0)) +SAMPLE_ADAPTERS = (0, 1) + + +def _mutate(rec, path, fn): + out = json.loads(json.dumps(rec)) + obj = out + for k in path[:-1]: + obj = obj[k] + obj[path[-1]] = fn(obj[path[-1]]) + return out + + +def semantic_controls(children, adapters, word): + """Each mutation must be rejected on every sample record it applies to; the reordered-rows frame is a + positive control that must pass. Returns {control: 'rejected k/k'}.""" + frames = word['frames'] + by_key = {(c['old'], c['new']): c for c in children} + sample_c = [by_key[k] for k in SAMPLE_CHILDREN] + sample_a = [adapters[i] for i in SAMPLE_ADAPTERS] + for c in sample_c: + need(check_pair(*child_circuits(c, frames)), 'C sample child passes unmutated') + for x in sample_a: + need(check_pair(*adapter_circuits(x, word)), 'C sample adapter passes unmutated') + + def cz(Q): + Q = list(Q) + Q[6] ^= 1 << 7 + Q[7] ^= 1 << 6 + return Q + record_mutations = { + 'global_phase': (('left', 'phase'), lambda p: (p + 1) % 4), + 'input_character': (('right', 'linear_Z4'), lambda a: a[:5] + [(a[5] + 2) % 4] + a[6:]), + 'cz_cross_term': (('left', 'quadratic_rows'), cz), + 'translation': (('right', 'offset'), lambda b: b ^ 256), + } + out = {} + for name, (path, fn) in record_mutations.items(): + rej = 0 + for c in sample_c: + rej += not check_pair(*child_circuits(_mutate(c, path, fn), frames)) + apath = ('left', path[1]) # adapters carry only a left monomial + for x in sample_a: + rej += not check_pair(*adapter_circuits(_mutate(x, apath, fn), word)) + need(rej == len(sample_c) + len(sample_a), 'C control not rejected: ' + name) + out[name] = 'rejected %d/%d' % (rej, rej) + for variant in ('swap_wrappers', 'direction', 'gate_order', 'fourier_sign', 'one_gate'): + cands = [c for c in sample_c if variant != 'one_gate' or c['rank'] >= 2] + rej = sum(not check_pair(*child_circuits(c, frames, variant)) for c in cands) + if variant == 'fourier_sign': # C_q sign flip on the adapters (the target then reads T_f C_q^-1 F_9^-1) + rej += sum(not check_pair(*adapter_circuits(x, word, variant)) for x in sample_a) + cands = cands + sample_a + # gate_order is children only: for every endpoint adapter q(Gx) = q(x), so evaluating D after P is the + # same operator (counted in gate_order_equivalent_adapters below); the order is pinned by the children + # controls and by FX1's comparison with the Lean Mono.gates literals + need(rej == len(cands), 'C control not rejected: ' + variant) + out[variant] = 'rejected %d/%d' % (rej, rej) + for variant in ('port', 'role'): + rej = sum(not check_pair(*adapter_circuits(x, word, variant)) for x in sample_a) + need(rej == len(sample_a), 'C control not rejected: adapter ' + variant) + out['adapter_' + variant] = 'rejected %d/%d' % (rej, rej) + # frame basis: same span, other basis -> rejected; same rows reordered -> passes (positive control) + rej = passed = 0 + for key in ((0, 174), (0, 415)): + c = by_key[key] + U = frames[c['new']] + alt = list(frames) + alt[c['new']] = [U[0] ^ U[1]] + U[1:] + rej += not check_pair(*child_circuits(c, alt)) + alt[c['new']] = list(reversed(U)) + passed += check_pair(*child_circuits(c, alt)) + need(rej == 2 and passed == 2, 'C frame basis control') + out['frame_basis'] = 'rejected 2/2; reordered rows pass 2/2' + return out + + +def gate_order_equivalent_adapters(adapters): + """How many endpoint monomials are unchanged when D is evaluated after P (a structural fact, not a control).""" + return sum(C.same_operator(C.monomial(x['left']), C.monomial(x['left'], 'PDXPH')) for x in adapters) + + +# ------------------------------------------------------------------------------------------------ main +def main(): + ap = argparse.ArgumentParser(description=__doc__.split('\n\n')[0]) + ap.add_argument('--write', action='store_true') + ap.add_argument('--subset', default=None) + ap.add_argument('--receipts', default=None) + a = ap.parse_args() + if a.write and a.subset: + raise SystemExit('--write needs a full run') + need(not any(m.split('.')[0] in FORBIDDEN for m in sys.modules), 'independence: no producer module loaded') + data, binding = load() + children, adapters, counts = inventory(data) + calibration = calibrate(data['word']['frames']) + controls = semantic_controls(children, adapters, data['word']) + ev = evaluate(children, adapters, data['word'], subset=a.subset, receipts=a.receipts) + need(not any(m.split('.')[0] in FORBIDDEN for m in sys.modules), 'independence: no producer module loaded') + if a.subset is not None: + print('children %d adapters %d (%.1f s CPU)' % (ev['children'], ev['adapters'], ev['cpu_seconds'])) + print('PARTIAL_FRONTIER1094_RECIPES_EXACT subset=%s' % a.subset) + return + exp = CASES['expected'] + need(ev['children'] == exp['children'] and ev['adapters'] == exp['adapters'], 'E full coverage') + ev.pop('cpu_seconds') + counts['gate_order_equivalent_adapters'] = '%d of %d' % (gate_order_equivalent_adapters(adapters), len(adapters)) + result = dict(status='PASS_FRONTIER1094_RECIPES_EXACT', binding=binding, inventory=counts, calibration=calibration, + controls=controls, evaluation=dict(ev, columns=C.DIM, global_phase_included=True, + comparator='exact packed Gaussian integers, scaled to a common 2^K', + radix_rule='beta = 2K + 2'), + scope='Record level: every child record and endpoint adapter of the gauge44 CLIFFORD-RECIPES.json equals ' + 'T_new T_old^-1 (climb and centre relabels) or satisfies Lemma G H6; not the 36 residual wrapper ' + 'recipes, the identity adapters, the executor bridge, a Lean proof or a new kappa') + text = json.dumps(result, indent=1, sort_keys=True) + '\n' + target = HERE / 'RESULT.json' + if a.write: + target.write_text(text) + else: + need(target.read_text() == text, 'RESULT.json reproduced byte for byte') + print('children %d adapters %d columns %d K %s' % (ev['children'], ev['adapters'], C.DIM, ev['K_histogram'])) + print('PASS_FRONTIER1094_RECIPES_EXACT') + + +if __name__ == '__main__': + try: + main() + except Reject as exc: + raise SystemExit('FAIL ' + str(exc))