diff --git a/research/pr5270-reference-audit/README.md b/research/pr5270-reference-audit/README.md new file mode 100644 index 0000000000..d868b0a64f --- /dev/null +++ b/research/pr5270-reference-audit/README.md @@ -0,0 +1,123 @@ +# PR5270's physical replay reference does not match its priced controller + +Author-checked independent audit for ahrazzle, prepared with substantial OpenAI +Codex assistance. Apache-2.0. Not yet independently reviewed; no selected-result change. + +At PR5270 head `df9e5037587ce0cfbd23c2a944515526b301e820`, the physical +listing and its `standard()` reference agree with each other, but that reference +is not the formal thinned controller whose invoice the package prices. +This is an exact finite counterexample to that binding, not an impossibility +theorem for coded suppliers. + +From this package directory, using the Python 3 standard library: + +```sh +python3 -B verify.py +``` + +Runtime here: about 0.12 seconds. `RESULT.json` records the result. +`SOURCES.json` authenticates unchanged source exports by SHA-256 and records +their canonical URLs and Git blob IDs. The two PR5270 blob IDs also agree with +the GitHub PR-files response; the retained controller blob is the PR's own +source-manifest pin. + +## The four-role counterexample + +Take p=2, pattern `T`, with thick stage set `{1,3}`. Specialize the central +letter to `q=1`, the two thick letters to `D1=D3=i`, and thin even letters to 1. +The retained formal Laurent-polynomial controller, followed by its retained +`thin()` function, gives + +```text +[-1 0 0 0] +[ 0 -1 0 0] +[ 0 0 i 0] +[ 0 0 0 i]. +``` + +The actual PR5270 listing's uncoded reference gives + +```text +[-i 0 0 1-i] +[ 0 -i 1-i 0] +[ 0 0 -1 0] +[ 0 -i 2-i -1]. +``` + +All entries above are exact Gaussian integers. The difference is not a rounding +effect or a missing global phase: several entries that should vanish are nonzero. + +A separate direct calculation of the actual reference on the fourth role input +`e3` gives `(1-i, 0, 0, -1)`, while the formal controller gives `i e3`. +On this eigenvector both the rank-eight D and the full rank-nine R have +eigenvalue i, so this counterexample does not rely on their separate rank mismatch. + +Three transcription differences are individually discriminated: + +1. In the forward loop, the source formal `bridge(dst,src,c)` updates the odd + role at `src` from the odd role at `dst`, with coefficient `-c`. The p19 + listing and its `standard()` reverse this direction. The final reverse sweep + already has the correct direction; blindly reversing every odd bridge is + not the repair. +2. The middle idle belongs to even stage 2 and becomes identity after thinning. + The listing applies `R` instead. The p19 invoice independently drops this + rank-zero call, while the listing applies 18 such nonidentity idles. +3. The p2 terminal idle covers stages `{3,4}`, of which only 3 is thick. Its + specialization is `R`, while the listing uses the unthinned interval length + and applies `R^2`. The same stage-count versus thick-stage-count mismatch + affects initial and terminal intervals at p19. + +The checker uses two differently represented computations. One executes only +the authenticated retained formal controller/thinning functions on sparse +Laurent polynomials and then specializes them exactly. The other interprets +the emitted listing with Gaussian-integer matrices. To bind the latter to the +actual physical source rather than merely our reading, it also executes the +retained `standard()` and Gaussian butterfly on the genuine 512-address vector +`v[x]=(-1)^bit_1(x)`. The central Q fixes this vector and the full R multiplies +it by i. Four basis-role inputs recover the complete displayed 4-by-4 matrix, +using exact arithmetic modulo 65537 with i=256. Every output address is checked. + +At p19 the same exact specialization has 351 differing matrix entries. +Correcting only the reference's bridge directions and idle thinning restores +agreement with the formal controller for both p2 and p19. Leaving any one of +the three p2 defects in place is rejected. These are consistency controls, not +supplier admission. + +## Remaining scope + +Even after these transcription repairs, a separate physical binding is needed. +The retained native backward endpoint in `coded-native-caller/PHYSICAL.md` has +diagonal factor D of rank eight. The p19 listing uses full rank-nine R because +its gauge commutes with R but not D. Its finite replay also reuses one +9-coordinate address block, whereas the invoice uses independent thick blocks +and maximum target rank153. This audit does not prove that substitution legal, +price any extra Q transformations, implement code gauges on independent blocks, +or establish the complete native helper/precision/compiler interface. We make +no claim that every possible correction loses. +In particular, the mismatch does not rule out a newly proved boundary +normalization and revised invoice for the altered word. + +The geometric tail change from 19/20 to 97/100 is not the immediate obstruction: +the general higher-moment theorem allows any rational limits below one that +satisfy the complete charged inequality. Likewise, a sufficiently larger +logarithmic compiler power can remove the *fixed-power* numerical cap once a +valid native unit is established. Neither arithmetic repair binds this altered +physical word to the claimed invoice. + +## Open next questions + +- First correct the bridge and idle transcription in a new successor package, + and compare the corrected path against the formal stage-labelled controller. +- Then bind one actual rank-eight native reverse invocation, its necessary + code changes and independent-block spectators to that path, charging every + additional Gaussian child. The present full-R gauge identity is insufficient. +- Only after that binding, recalculate the complete paid/target profiles and + use the generic tail/compiler theorem with newly certified constants. + +Credit: DaysSky for PR5270's listing and physical gauge work; Cayden Burkart / +SethBurkart123 for PR4940's formal coded controller; Dillon for PR4933's +physical normalizers; Dugongue / mdumitrean for PR4929's center-free producer; +Cinna Davis, Cao Yifan, zxv, Jacob Alan Sussman and the retained native, +controller, compiler and outer contributors for the predecessor construction. +The source exports retain their notices. This audit's addition is the exact +source-bound reference/invoice mismatch and its independent eigenvector check. diff --git a/research/pr5270-reference-audit/RESULT.json b/research/pr5270-reference-audit/RESULT.json new file mode 100644 index 0000000000..a873648b80 --- /dev/null +++ b/research/pr5270-reference-audit/RESULT.json @@ -0,0 +1,219 @@ +{ + "status": "PASS_SCOPED_PR5270_REFERENCE_INVOICE_COUNTEREXAMPLE", + "source_head": "df9e5037587ce0cfbd23c2a944515526b301e820", + "specialization": { + "q": "1", + "odd_stage_letters": "i", + "even_stage_letters": "1" + }, + "p2_formal_matrix_gaussian_pairs": [ + [ + [ + -1, + 0 + ], + [ + 0, + 0 + ], + [ + 0, + 0 + ], + [ + 0, + 0 + ] + ], + [ + [ + 0, + 0 + ], + [ + -1, + 0 + ], + [ + 0, + 0 + ], + [ + 0, + 0 + ] + ], + [ + [ + 0, + 0 + ], + [ + 0, + 0 + ], + [ + 0, + 1 + ], + [ + 0, + 0 + ] + ], + [ + [ + 0, + 0 + ], + [ + 0, + 0 + ], + [ + 0, + 0 + ], + [ + 0, + 1 + ] + ] + ], + "p2_source_reference_matrix_gaussian_pairs": [ + [ + [ + 0, + -1 + ], + [ + 0, + 0 + ], + [ + 0, + 0 + ], + [ + 1, + -1 + ] + ], + [ + [ + 0, + 0 + ], + [ + 0, + -1 + ], + [ + 1, + -1 + ], + [ + 0, + 0 + ] + ], + [ + [ + 0, + 0 + ], + [ + 0, + 0 + ], + [ + -1, + 0 + ], + [ + 0, + 0 + ] + ], + [ + [ + 0, + 0 + ], + [ + 0, + -1 + ], + [ + 2, + -1 + ], + [ + -1, + 0 + ] + ] + ], + "p2_retained_512_address_reference": "matches independent Gaussian-integer interpreter modulo 65537", + "p19_mismatched_matrix_entries": 351, + "p19_first_mismatches": [ + [ + 0, + 2 + ], + [ + 0, + 3 + ], + [ + 0, + 4 + ], + [ + 0, + 5 + ], + [ + 0, + 6 + ], + [ + 0, + 7 + ], + [ + 0, + 8 + ], + [ + 0, + 9 + ], + [ + 0, + 10 + ], + [ + 0, + 11 + ], + [ + 0, + 12 + ], + [ + 0, + 13 + ] + ], + "positive_controls": [ + "corrected p2 bridge direction and idle thinning", + "corrected p19 bridge direction and idle thinning" + ], + "rejected_controls": [ + "uncorrected p2 middle idle", + "uncorrected p2 terminal idle", + "uncorrected p2 odd-role bridge direction" + ], + "scope": "Source replay reference is not the formal thinned controller whose invoice is priced. No impossibility claim; no new kappa; no supplier repair admitted." +} diff --git a/research/pr5270-reference-audit/SOURCES.json b/research/pr5270-reference-audit/SOURCES.json new file mode 100644 index 0000000000..358a99b608 --- /dev/null +++ b/research/pr5270-reference-audit/SOURCES.json @@ -0,0 +1,28 @@ +{ + "repository": "DaysSky/integer-mult-bounds", + "pr": 5270, + "head": "df9e5037587ce0cfbd23c2a944515526b301e820", + "files": [ + { + "local_path": "vendor/p19_word.py", + "source_path": "research/coded-reverse-word-p19/p19_word.py", + "url": "https://github.com/DaysSky/integer-mult-bounds/blob/df9e5037587ce0cfbd23c2a944515526b301e820/research/coded-reverse-word-p19/p19_word.py", + "sha256": "305acd8258d6615a0d55533d8b876561311741e8e674da7e56123cc61ab28f29", + "git_blob": "6522cf370b5686e19b1eaf82ceea5ab13183e8c7" + }, + { + "local_path": "vendor/physical_gauge_lift.py", + "source_path": "research/coded-reverse-word-p19/physical_gauge_lift.py", + "url": "https://github.com/DaysSky/integer-mult-bounds/blob/df9e5037587ce0cfbd23c2a944515526b301e820/research/coded-reverse-word-p19/physical_gauge_lift.py", + "sha256": "8dc4cb463902a94cc1e6a9c86d780c96f115efb7afb66634637a3b57934c5156", + "git_blob": "c68b7ca2cd3b9ce3a67dfc715144110aa301279f" + }, + { + "local_path": "vendor/controller_verify.py", + "source_path": "research/coded-reverse-controller/verify.py", + "url": "https://github.com/DaysSky/integer-mult-bounds/blob/df9e5037587ce0cfbd23c2a944515526b301e820/research/coded-reverse-controller/verify.py", + "sha256": "05a898d3af329dc4665590b4ec4b2801e588843efe9618eec55b4028fd104b67", + "git_blob": "71f3d8929f28d7b4b854be7177ca8dfecf81ea5c" + } + ] +} diff --git a/research/pr5270-reference-audit/vendor/controller_verify.py b/research/pr5270-reference-audit/vendor/controller_verify.py new file mode 100644 index 0000000000..71f3d8929f --- /dev/null +++ b/research/pr5270-reference-audit/vendor/controller_verify.py @@ -0,0 +1,216 @@ +#!/usr/bin/env python3 +"""Checks for consuming the center-free coded native word (PR4929) in the query-thinned controller. + +Coded reverse stages carry the code A; every forward stage is a query-only shear that first mixes its +source by A^-1. Standard library only; reads existing repo files. Python 3.9+. +""" +import gzip, importlib.util, json, math, sys +from collections import Counter +from fractions import Fraction as Q +from pathlib import Path + +sys.dont_write_bytecode = True +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +sys.path[:0] = [str(ROOT/'research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/bit-compression/carrier-reuse/reference'), + str(ROOT/'research/kappa-rebuild/bit')] +import complex_controller_factor as C + +def need(ok, why): + if not ok: + raise SystemExit('FAIL: '+why) + print('PASS', why, flush=True) + +# ---- 1. the code A of PR4929 -------------------------------------------------------------- +NP = 112 +A = [[Q(x) for x in row] for row in json.load(open(ROOT/'research/native-center-free-code/CODE.json'))['A']] +I = [[Q(int(i == j)) for j in range(NP)] for i in range(NP)] +def mm(X, Y): return [[sum(X[i][k]*Y[k][j] for k in range(NP) if X[i][k]) for j in range(NP)] for i in range(NP)] +Ainv = [[I[i][j]+(A[i][j]-I[i][j])/13 for j in range(NP)] for i in range(NP)] +R = [[int(json.load(gzip.open(ROOT/'research/kappa-native-resume/causal-controller/sources/research/joint-query/certificate.json.gz'))['R_rows'][a].get(str(p), 0)) for p in range(NP)] for a in range(8)] +need(all(A[i][j] == A[j][i] for i in range(NP) for j in range(NP)) and all(A[i][i] == 0 for i in range(NP)), 'A symmetric with zero diagonal') +need(all(A[p][q] == I[p][q]-Q(sum(R[a][p]*R[a][q] for a in range(8)), 4) for p in range(NP) for q in range(NP)), 'A = I - R^T R / 4 for the joint-query packet') +need(mm([[A[i][j]-I[i][j] for j in range(NP)] for i in range(NP)], [[A[i][j]+13*I[i][j] for j in range(NP)] for i in range(NP)]) == [[Q(0)]*NP for _ in range(NP)], '(A-I)(A+13I)=0: modes 1 (104) and -13 (8)') +need(mm(A, Ainv) == I, 'A^-1 = I + (A-I)/13') + +# ---- 2. coded controller: exact diagonalization after thinning ------------------------------- +def controller(p, keep, coupling): + """C.controller with a per-stage coupling: forward lower-left coupling*Q^-1, reverse upper-right -coupling*Q.""" + n, stages = 2*p, 2*p+1 + zero = (0,)*(stages+1) + matrix = [[{zero: 1} if i == j else {} for j in range(n)] for i in range(n)] + idle = [] + term = lambda q, sel: (q,)+tuple(int(s in sel) for s in range(stages)) + def idle_call(pair, sel, kind): + retained = bool(keep >> len(idle) & 1) + idle.append(dict(kind=kind, pair=pair, retained=retained)) + if retained: + for role in (2*pair, 2*pair+1): + matrix[role] = [C.monomial_times(x, term(0, sel)) for x in matrix[role]] + def local(stage, pair, reverse): + x, y = 2*pair, 2*pair+1 + if reverse: x, y = y, x + coef = (-1 if reverse else 1)*coupling[stage] + matrix[y] = [C.plus(a, C.monomial_times(b, term(1 if reverse else -1, []), coef)) for a, b in zip(matrix[y], matrix[x])] + for role in (x, y): matrix[role] = [C.monomial_times(z, term(0, [stage])) for z in matrix[role]] + if stage % 2 and stage <= 2*p-3: idle_call((stage+1)//2, list(range(stage+1)), 'initial') + elif stage % 2 == 0 and 2 <= stage <= 2*p-2: idle_call(stage//2, [stage], 'middle') + elif stage == 2*p: + for j in range(p-1): idle_call(j, list(range(2*j+3, 2*p+1)), 'terminal') + def bridge(dst, src, c): + for d, s, cc in ((2*dst, 2*src, c), (2*src+1, 2*dst+1, -c)): + matrix[d] = [C.plus(a, b, cc) for a, b in zip(matrix[d], matrix[s])] + local(0, 0, False) + for j in range(p): + local(2*j+1, j, True) + if j < p-1: bridge(j, j+1, 1) + local(2*j+2, j, False) + if j < p-1: bridge(j, j+1, -1) + for j in reversed(range(p-1)): bridge(j+1, j, 1) + for j in range(p): matrix[2*j], matrix[2*j+1] = matrix[2*j+1], [C.monomial_times(x, zero, -1) for x in matrix[2*j]] + co = {} + for i, row in enumerate(matrix): + for j, poly in enumerate(row): + for key, v in poly.items(): co.setdefault(key, [[Q(0)]*n for _ in range(n)])[i][j] += v + return {k: m for k, m in co.items() if any(any(r) for r in m)}, idle + +def keep_of(p, pat): + _, idle = controller(p, 0, {s: 1 for s in range(2*p+1)}) + return sum(1 << i for i, r in enumerate(idle) if r['kind'] == 'middle' or (r['kind'] == 'initial' and pat[r['pair']-1] in 'IB') or (r['kind'] == 'terminal' and pat[r['pair']] in 'TB')) + +def thin(co, thick): + out = {} + for term, m in co.items(): + key = (term[0],)+tuple(x if s in thick else 0 for s, x in enumerate(term[1:])) + t = out.setdefault(key, [[Q(0)]*len(m) for _ in m]) + for i, row in enumerate(m): + for j, v in enumerate(row): t[i][j] += v + return {k: m for k, m in out.items() if any(any(r) for r in m)} + +C.scalar_program = lambda m: None # the dyadic boundary test is reported below as a denominator instead +def diagonalize(p, pat, coupling): + r = C.factor(thin(controller(p, keep_of(p, pat), coupling)[0], set(range(1, 2*p, 2)))) + if r is None: return None + return sorted(Counter(sum(t[1:]) for t in r['diagonal']).items()), sorted({q.denominator for m in (r['left'], r['right']) for row in m for q in row}) + +c = Q(-13) +for p, pat in [(3, 'IT'), (4, 'IIT'), (5, 'IITT'), (8, 'IIIITTT')]: + coded = {s: (c if s % 2 else 1/c) for s in range(2*p+1)} # reverse = A, forward (incl. both ends) = A^-1 + std = diagonalize(p, pat, {s: Q(1) for s in range(2*p+1)}) + cod = diagonalize(p, pat, coded) + need(std is not None and cod is not None and std[0] == cod[0] and std[1] == [1] and cod[1] == [1, 13], + 'p=%d %s: coded controller diagonalizes with the standard outputs %s; new boundary denominator 13' % (p, pat, cod[0] if cod else None)) +p, pat = 3, 'IT' +need(diagonalize(p, pat, {s: (c if s % 2 else Q(1)) for s in range(2*p+1)}) is None, 'control: coded reverse with uncoded forward stages does not diagonalize') +need(diagonalize(p, pat, {s: (c if (s % 2 or s in (0, 2*p)) else 1/c) for s in range(2*p+1)}) is None, 'control: coded (thick) forward end stages do not diagonalize') +need(diagonalize(p, pat, {s: (c if s % 2 else Q(1, 169)) for s in range(2*p+1)}) is None, 'control: wrong inverse code does not diagonalize') + +# ---- 3. explicit conjugation with the real 112 x 112 code (p=2, numeric Q and D_s) ----------- +def sparse(M): return [[(j, v) for j, v in enumerate(row) if v] for row in M] +SI, SA, SAi = sparse(I), sparse(A), sparse(Ainv) +def build(p, rev, fwd, Qv, Dv): + rows = {(r, q): {(r, q): Q(1)} for r in range(2*p) for q in range(NP)} + def addrow(dst, src, M, coef): + new = {} + for pp in range(NP): + acc = dict(rows[(dst, pp)]) + for q, mv in M[pp]: + for k, v in rows[(src, q)].items(): acc[k] = acc.get(k, 0)+coef*mv*v + new[pp] = {k: v for k, v in acc.items() if v} + rows.update({(dst, pp): new[pp] for pp in range(NP)}) + def scale(role, m): + for q in range(NP): + for k in rows[(role, q)]: rows[(role, q)][k] *= m + def local(stage, pair, reverse): + x, y = 2*pair, 2*pair+1 + if reverse: x, y = y, x; addrow(y, x, rev, -Qv) + else: addrow(y, x, fwd, 1/Qv) + if stage % 2: scale(x, Dv[stage]); scale(y, Dv[stage]) + def bridge(dst, src, cf): + for d, s, cc in ((2*dst, 2*src, cf), (2*src+1, 2*dst+1, -cf)): + for pp in range(NP): + acc = dict(rows[(d, pp)]) + for k, v in rows[(s, pp)].items(): acc[k] = acc.get(k, 0)+cc*v + rows[(d, pp)] = {k: v for k, v in acc.items() if v} + local(0, 0, False) + for j in range(p): + local(2*j+1, j, True) + if j < p-1: bridge(j, j+1, 1) + local(2*j+2, j, False) + if j < p-1: bridge(j, j+1, -1) + for j in reversed(range(p-1)): bridge(j+1, j, 1) + return rows +def mix(rows, p, roles, M, side): + out = {} + for (r, pp), rw in rows.items(): + if side == 'rows' and r in roles: + acc = {} + for q, mv in M[pp]: + for k, v in rows[(r, q)].items(): acc[k] = acc.get(k, 0)+mv*v + elif side == 'cols': + acc = {} + for (cc, q), v in rw.items(): + if cc in roles: + for k, mv in M[q]: acc[(cc, k)] = acc.get((cc, k), 0)+v*mv + else: acc[(cc, q)] = acc.get((cc, q), 0)+v + else: acc = rw + out[(r, pp)] = {k: v for k, v in acc.items() if v} + return out +p = 2; Dv = {s: Q(2*s+3) for s in range(2*p+1)} +std, cod = build(p, SI, SI, Q(2), Dv), build(p, SA, SAi, Q(2), Dv) +xr = set(range(0, 2*p, 2)) +need(mix(mix(std, p, xr, SA, 'rows'), p, xr, Ainv and sparse(Ainv), 'cols') == cod, 'p=2, 448x448: coded controller == (A on x-roles) * standard * (A^-1 on x-roles), exact') +need(mix(mix(std, p, xr, SA, 'rows'), p, xr, SA, 'cols') != cod, 'control: wrong conjugation rejected') + +# ---- 4. invoice and moment root ------------------------------------------------------------- +H = {4: 28, 7: 7, 8: 47, 9: 326} # helpers (unchanged by PR4929) +P_OLD = {1: 2237, 2: 388, 3: 494, 4: 147, 5: 36, 8: 8} # joint-helper-lattice local paid profile +P_NEW = {1: 2201, 2: 412, 3: 510, 4: 127, 5: 40} # PR4929 paid profile, both orientations +need(sum(r*n for r, n in P_OLD.items())-sum(r*n for r, n in P_NEW.items()) == 64, 'PR4929 removes exactly 64 rank mass per call') +def invoice(p, pat, thick, prof): + full = frozenset(range(2*p+1)); T, D = Counter(), Counter() + outs = [full, full] + for i, ch in enumerate(pat, 1): outs += [frozenset(range(0, 2*i+1)) if ch == 'I' else frozenset(range(2*i, 2*p+1))]*2 + for s in outs: T[1+8*len(s & thick)] += 112 + for i, ch in enumerate(pat, 1): + if ch == 'I': D[8*len(frozenset(range(0, 2*i)) & thick)] += 224 + else: D[8*len(frozenset(range(2*i+1, 2*p+1)) & thick)] += 224 + for j in range(1, p): D[8*len(frozenset([2*j]) & thick)] += 224 + for r, n in H.items(): T[r] += len(thick)*n + for r, n in prof.items(): D[r] += len(thick)*n + D[1] += 112*(2*p+1-len(thick)) + T.pop(0, None); D.pop(0, None) + return T, D +def root(T, D): + f = lambda cc: sum(n*r**(1-cc) for r, n in T.items())-sum(n*r**(1-cc) for r, n in D.items()) + lo, hi = 0.0, 0.05 + for _ in range(200): + mid = (lo+hi)/2 + if f(mid) > 0: lo = mid + else: hi = mid + return lo +pub = root(*invoice(16, 'I'*7+'T'*8, frozenset({0, 32} | set(range(1, 32, 2))), P_OLD)) +need(abs(pub-0.0030201659770) < 1e-12, 'model reproduces the published p16 raw root 0.0030201659770 (got %.13f)' % pub) +res = {p: root(*invoice(p, 'I'*((p-1)//2)+'T'*(p-1-(p-1)//2), frozenset(range(1, 2*p, 2)), P_NEW)) for p in (8, 19)} +print('coded controller raw complex root: p=8 %.6f, p=19 %.6f' % (res[8], res[19])) +need(res[19] > 0.0034*1.5, 'p=19 raw root is more than 1.5x the BIT cap 0.0034') +def guards(T, D, cc, u=0.2, cut=20, floor=21): + t = 1-cc; Tt = sum(n*r**t for r, n in T.items()); Pt = sum(n*r**t for r, n in D.items()) + return Pt/Tt, sum(n*r**(t+u) for r, n in D.items())/(cut**u*Tt), floor*sum(T.values())/(cut**cc*Tt) +a, g, d = guards(*invoice(19, 'I'*9+'T'*9, frozenset(range(1, 38, 2)), P_NEW), 0.0034) +need(a < 1-1e-9 and g < 0.97 and d < 0.97, 'p=19 tail guards at C=0.0034: alpha=%.8f gamma=%.4f delta=%.4f' % (a, g, d)) + +# ---- 5. the repo's strict outer ledger --------------------------------------------------------- +sys.path.insert(0, str(ROOT/'research/pr4359-p7-padding/dependencies/compiler-refill')) +spec = importlib.util.spec_from_file_location('ledger_mod', ROOT/'research/pr4359-p7-padding/dependencies/compiler-refill/endpoint.py') +L = importlib.util.module_from_spec(spec); spec.loader.exec_module(L) +gap, atom = Q(1, 1400000000), Q(1, 250) +def failing(kappa): + prm = {'kappa': kappa, 'tested_saving': kappa+7*gap, 'complex_uniform_saving': kappa+6*gap, 'b': kappa+5*gap, 'a': kappa+4*gap, + 'q': kappa+3*gap, 'bit_saving': Q(17, 5000), 'epsilon': 1-gap, 'beta': 1-3*gap, 'r0': gap/10, 'stop': gap, 'layout': gap, 'd': gap} + out = L.ledger(prm); out['functional_checks']['actual_new_BIT_stock_sublinear'] = prm['beta']*(1-atom) + return [k for part in ('strict_checks', 'functional_checks') for k, x in out[part].items() if x <= 0] +need(failing(Q(60403, 20000000)) == [], 'ledger passes at the selected kappa 0.00302015 (control)') +need(failing(Q(3324, 1000000)) == [] and failing(Q(33999, 10000000)) == [], 'ledger passes at 0.003324 (+10%) and 0.0033999') +need(failing(Q(34, 10000)) == ['actual_bit_above_effective'], 'at 0.0034 the only failing predicate is the BIT cap') +print('DONE: formal and arithmetic checks pass; physical admission of the adapter is NOT checked here') diff --git a/research/pr5270-reference-audit/vendor/p19_word.py b/research/pr5270-reference-audit/vendor/p19_word.py new file mode 100644 index 0000000000..6522cf370b --- /dev/null +++ b/research/pr5270-reference-audit/vendor/p19_word.py @@ -0,0 +1,242 @@ +#!/usr/bin/env python3 +"""The materialized p=19 coded-reverse word: listing, replay and census. + +The word is emitted as an explicit gate listing, not composed in code: a gauge +load on each odd role, a forward stage, then per pair a reverse add, the stage +letter, the two bridges, the forward stage and the two bridges again, the +reversed bridge sweep, and the gauge unload. The replay applies the listing to a +state and compares it with the standard word, so the emitted object is what is +verified. + +Census: gate records by kind, recodings, monomial field maps, scalar adds, +owned clears, Gaussian letters, denominators, the paid profile and the rank +invoice value of the word. +""" +import importlib.util, json +from collections import Counter +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +P, OWNERS, SIZE = 65537, 112, 512 +H = {4: 28, 7: 7, 8: 47, 9: 326} +P_NEW = {1: 2201, 2: 412, 3: 510, 4: 127, 5: 40} +P_OLD = {1: 2237, 2: 388, 3: 494, 4: 147, 5: 36, 8: 8} +MAPS, ADDS, CLEARS = 224, 896, 16 # per recoding: 112 K + 112 K^-1, 8 x (56 + 56) adds, 16 clears + +def need(ok, why): + if not ok: raise ValueError(why) + +def engine(): + spec = importlib.util.spec_from_file_location('lift', HERE/'physical_gauge_lift.py') + mod = importlib.util.module_from_spec(spec); spec.loader.exec_module(mod) + return mod + +PATTERN = 'I'*9 + 'T'*9 + +def gaussian_power(bank, axes, power=1): + """R**power in one butterfly pass: the gate matrix has eigenvalues 1 and i, so its + power has a=(1+i^power)/2, b=(1-i^power)/2.""" + ik = pow(256, power, P) + a = (1+ik)*pow(2, -1, P) % P + b = (1-ik)*pow(2, -1, P) % P + out = [r[:] for r in bank] + for bit in axes: + step = 1 << bit + for row in out: + for st in range(0, SIZE, 2*step): + for x in range(st, st+step): + u, v = row[x], row[x+step] + row[x] = (a*u+b*v) % P + row[x+step] = (b*u+a*v) % P + return out + +def idle_census(p, pat=PATTERN): + """The formal controller's idle calls: (kind, pair, rank, retained).""" + rows = [] + for stage in range(1, 2*p): + if stage % 2 and stage <= 2*p-3: + pair = (stage+1)//2 + rows.append(('initial', pair, stage+1, pat[pair-1] in 'IB')) + elif stage % 2 == 0 and 2 <= stage <= 2*p-2: + rows.append(('middle', stage//2, 1, True)) + for j in range(p-1): + rows.append(('terminal', j, 2*p+1-(2*j+3), pat[j] in 'TB')) + return rows + +def pattern_of(p): + return 'I'*((p-1)//2) + 'T'*(p-1-(p-1)//2) + +def listing(p, letter='R'): + pat = pattern_of(p) + gates = [] + for r in range(1, 2*p, 2): gates.append(('GAUGE_LOAD', r, 'C^-1')) + gates.append(('FORWARD', 0, 1, 'C^-1.Q^-1')) + for j in range(p): + gates.append(('REVERSE', 2*j, 2*j+1, 'Q.C')) + gates.append(('LETTER', 2*j, 2*j+1, letter)) + if j < p-1 and pat[j] in 'IB': + gates.append(('IDLE', 2*(j+1), 2*(j+1)+1, 2*j+2, 'initial')) + if j < p-1: + gates.append(('BRIDGE', 2*j, 2*j+2, 1)); gates.append(('BRIDGE', 2*j+1, 2*j+3, -1)) + gates.append(('FORWARD', 2*j, 2*j+1, 'C^-1.Q^-1')) + if j < p-1: + gates.append(('IDLE', 2*(j+1), 2*(j+1)+1, 1, 'middle')) + gates.append(('BRIDGE', 2*j, 2*j+2, -1)); gates.append(('BRIDGE', 2*j+1, 2*j+3, 1)) + for j in range(p-1): + if pat[j] in 'TB': + gates.append(('IDLE', 2*j, 2*j+1, 2*p+1-(2*j+3), 'terminal')) + for j in reversed(range(p-1)): + gates.append(('BRIDGE', 2*j+2, 2*j, 1)); gates.append(('BRIDGE', 2*j+1, 2*j+3, -1)) + for r in range(1, 2*p, 2): gates.append(('GAUGE_UNLOAD', r, 'C')) + for j in range(p): gates.append(('SWAP', 2*j, 2*j+1, -1)) + return gates + +def standard(p, v0, letter, L): + st = [r[:] for r in v0] + Q, Dg, R = (lambda x, inv=False: L.gaussian(x, [0], inv)), \ + (lambda x, inv=False: L.gaussian(x, range(1, 9), inv)), \ + (lambda x, inv=False: L.gaussian(x, range(9), inv)) + let = {'R': R, 'D': Dg}[letter] + st[1] = L.add(st[1], Q(st[0], True)) + for j in range(p): + a, b = 2*j, 2*j+1 + st[a] = L.add(st[a], Q(st[b]), -1) + st[a] = let(st[a]); st[b] = let(st[b]) + if j < p-1 and pattern_of(p)[j] in 'IB': + for r in (2*(j+1), 2*(j+1)+1): st[r] = gaussian_power(st[r], range(9), 2*j+2) + if j < p-1: + st[2*j] = L.add(st[2*j], st[2*j+2], 1); st[2*j+1] = L.add(st[2*j+1], st[2*j+3], -1) + st[b] = L.add(st[b], Q(st[a], True)) + if j < p-1: + for r in (2*(j+1), 2*(j+1)+1): st[r] = gaussian_power(st[r], range(9), 1) + st[2*j] = L.add(st[2*j], st[2*j+2], -1); st[2*j+1] = L.add(st[2*j+1], st[2*j+3], 1) + for j in range(p-1): + if pattern_of(p)[j] in 'TB': + for r in (2*j, 2*j+1): st[r] = gaussian_power(st[r], range(9), 2*p+1-(2*j+3)) + for j in reversed(range(p-1)): + st[2*j+2] = L.add(st[2*j+2], st[2*j], 1); st[2*j+1] = L.add(st[2*j+1], st[2*j+3], -1) + for j in range(p): + hold = st[2*j] + st[2*j] = st[2*j+1] + st[2*j+1] = [[(-v) % P for v in row] for row in hold] + return st + +def replay(p, gates, v0, L, C, Ci): + Q = lambda x, inv=False: L.gaussian(x, [0], inv) + let = {'R': (lambda x, inv=False: L.gaussian(x, range(9), inv)), + 'D': (lambda x, inv=False: L.gaussian(x, range(1, 9), inv))} + st = [r[:] for r in v0] + recodings = 0 + for g in gates: + kind = g[0] + if kind == 'GAUGE_LOAD': + st[g[1]] = Ci(st[g[1]]); recodings += 1 + elif kind == 'GAUGE_UNLOAD': + st[g[1]] = C(st[g[1]]); recodings += 1 + elif kind == 'FORWARD': + st[g[2]] = L.add(st[g[2]], Ci(Q(st[g[1]], True))); recodings += 1 + elif kind == 'REVERSE': + st[g[1]] = L.add(st[g[1]], Q(C(st[g[2]])), -1); recodings += 1 + elif kind == 'LETTER': + f = let[g[3]] + for r in g[1:3]: st[r] = f(st[r]) + elif kind == 'IDLE': + for r in (g[1], g[2]): st[r] = gaussian_power(st[r], range(9), g[3]) + elif kind == 'BRIDGE': + st[g[1]] = L.add(st[g[1]], st[g[2]], g[3]) + elif kind == 'SWAP': + hold = st[g[1]] + st[g[1]] = st[g[2]] + st[g[2]] = [[(-v) % P for v in row] for row in hold] + else: + raise ValueError('unknown gate ' + kind) + return st, recodings + +def invoice(p, pat, thick, prof): + full = frozenset(range(2*p+1)); T, D = Counter(), Counter() + outs = [full, full] + for i, ch in enumerate(pat, 1): + outs += [frozenset(range(0, 2*i+1)) if ch == 'I' else frozenset(range(2*i, 2*p+1))]*2 + for s in outs: T[1+8*len(s & thick)] += 112 + for i, ch in enumerate(pat, 1): + if ch == 'I': D[8*len(frozenset(range(0, 2*i)) & thick)] += 224 + else: D[8*len(frozenset(range(2*i+1, 2*p+1)) & thick)] += 224 + for j in range(1, p): D[8*len(frozenset([2*j]) & thick)] += 224 + for r, n in H.items(): T[r] += len(thick)*n + for r, n in prof.items(): D[r] += len(thick)*n + D[1] += 112*(2*p+1-len(thick)) + T.pop(0, None); D.pop(0, None) + return T, D + +def root(T, D): + f = lambda c: sum(n*r**(1-c) for r, n in T.items())-sum(n*r**(1-c) for r, n in D.items()) + lo, hi = 0.0, 0.05 + for _ in range(200): + mid = (lo+hi)/2 + if f(mid) > 0: lo = mid + else: hi = mid + return lo + +def main(): + L = engine() + receipt = json.loads((ROOT/'research/coded-native-caller/NORMALIZERS.json').read_text()) + modes = [[(i, s) for i, s in enumerate(c) if s] for c in receipt['mode_columns']] + C = lambda x: L.physical_code(x, receipt['ports'], modes, False) + Ci = lambda x: L.physical_code(x, receipt['ports'], modes, True) + + import random + rng = random.Random(5) + p = 2 + gates = listing(p) + kinds = Counter(g[0] for g in gates) + v0 = [[[rng.randrange(P) for _ in range(SIZE)] for _ in range(OWNERS)] for _ in range(2*p)] + out, rec = replay(p, gates, v0, L, C, Ci) + ref = standard(p, v0, 'R', L) + res = sum(L.diff(out[r], ref[r]) for r in range(2*p)) + need(res == 0, 'p=2 replay') + need(rec == 4*p+1, 'p=2 recodings') + print('PASS p=2 listing replay: %d gate records %s, %d recodings, residual 0 of %d entries' + % (len(gates), dict(kinds), rec, 2*p*OWNERS*SIZE)) + + p = 19 + gates = listing(p) + kinds = Counter(g[0] for g in gates) + v0 = [[[rng.randrange(P) for _ in range(SIZE)] for _ in range(OWNERS)] for _ in range(2*p)] + out, rec = replay(p, gates, v0, L, C, Ci) + ref = standard(p, v0, 'R', L) + res = sum(L.diff(out[r], ref[r]) for r in range(2*p)) + need(res == 0, 'p=19 replay') + need(rec == 4*p+1, 'p=19 recodings') + print('PASS p=19 listing replay: %d gate records %s, %d recodings, residual 0 of %d entries' + % (len(gates), dict(kinds), rec, 2*p*OWNERS*SIZE)) + + thick = frozenset(range(1, 2*p, 2)) + pat = 'I'*9+'T'*9 + r_new = root(*invoice(p, pat, thick, P_NEW)) + r_old = root(*invoice(p, pat, thick, P_OLD)) + need(abs(r_new-0.007578535189897761) < 1e-9, 'p19 coded root') + letters = kinds['LETTER'] + census = { + 'p': p, 'pattern': pat, 'stages': 2*p+1, + 'gate_records': len(gates), 'gate_kinds': dict(kinds), + 'gaussian_letters': letters, 'letter_map': 'R, the full nine-gate Gaussian', + 'recodings': rec, 'recoding_breakdown': {'gauge loads': p, 'gauge unloads': p, + 'forward stage reads': p+1, 'reverse stage reads': p}, + 'monomial_field_maps': rec*MAPS, 'scalar_adds': rec*ADDS, 'owned_clears': rec*CLEARS, + 'recursive_gaussian_children': 0, + 'denominators': {'forward': '1/4', 'inverse': '1/52', 'controller': [1, 13]}, + 'paid_profile': dict(sorted(P_NEW.items())), 'helper_profile': dict(sorted(H.items())), + 'productive_total': sum(invoice(p, pat, thick, P_NEW)[0].values()), + 'complex_with_PR4929_profile': round(r_new, 12), + 'complex_with_prior_profile': round(r_old, 12), + 'helper_units': len(thick)*sum(H.values()), 'helper_profile_inherited': dict(sorted(H.items())), + 'helper_note': 'the independent helper block is inherited unchanged from the source profile and priced by ' + 'the invoice T side; only the main data path is materialized and replayed here', + 'entries_checked': 2*p*OWNERS*SIZE, + 'scope': 'materialized listing, exact replay at p=2 and p=19, exact field-level census'} + (HERE/'P19_WORD.json').write_text(json.dumps(census, indent=2, sort_keys=True)+'\n') + print(json.dumps(census, sort_keys=True)) + +if __name__ == '__main__': + main() diff --git a/research/pr5270-reference-audit/vendor/physical_gauge_lift.py b/research/pr5270-reference-audit/vendor/physical_gauge_lift.py new file mode 100644 index 0000000000..c68b7ca2cd --- /dev/null +++ b/research/pr5270-reference-audit/vendor/physical_gauge_lift.py @@ -0,0 +1,310 @@ +#!/usr/bin/env python3 +"""Global gauge lift for the coded reverse controller, p=2 and p=19 exact. + +The recovered full_build.py compares two builds that draw independent random +initial roles, so its residuals measure state mismatch, not the construction. +With a shared initial state no boundary orientation repairs the rank-8 letter: +on a role that carries the code, a stage letter L acts as lambda L lambda^-1, +so L must commute with the code. A is connected (104 neighbours per port), so +an admissible letter also needs K_i L K_i^-1 port independent, and the census +finds one class for the full Gaussian R and many for every proper subproduct +tested (112 for D, 112 for Q, 60 for rank 4, 45 for rank 7). Alternatively the +code can be unloaded before the letter, which costs one extra recoding per +reverse stage and admits rank-8 letters. + +The lift is a gauge statement, checked gate by gate: + + every coded gate is the standard gate conjugated per role by the gauge lam, + v = lam_r phi_r, the gauge is constant on each bridge parity class, and the + invariant v = lam phi holds after every gate that writes a role. + + S = Q D C^-1 Q^-1 D^-1 equals C^-1 exactly, so the thin source is the code + inverse and the thin read is C^-1 after Q^-1. + +Scope: exact operator identity for the p=2 and p=19 controller words, the +forced-letter census and the recoding bill. Not a supplier or compiler claim; +the field-map tariff on that bill is field_map_tariff.py. +""" +import json, random +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +P, IMAG, OWNERS, SIZE = 65537, 256, 112, 512 +MONOMIAL_MAPS, SCALAR_ADDS, OWNED_CLEARS = 224, 896, 16 + +def need(ok, why): + if not ok: raise ValueError(why) + +def empty(): return [[0]*SIZE for _ in range(OWNERS)] +def add(x, y, s=1): return [[(a+s*b) % P for a, b in zip(xi, yi)] for xi, yi in zip(x, y)] +def gaussian(bank, axes, inverse=False): + a = (1+(-IMAG if inverse else IMAG))*pow(2, -1, P) % P + b = (1-(-IMAG if inverse else IMAG))*pow(2, -1, P) % P + out = [r[:] for r in bank] + for bit in axes: + step = 1 << bit + for row in out: + for st in range(0, SIZE, 2*step): + for x in range(st, st+step): + u, v = row[x], row[x+step] + row[x] = (a*u+b*v) % P + row[x+step] = (b*u+a*v) % P + return out +def signed_map(rec, x, inverse=False): + rows, mask = rec['G_rows'], rec['Z_mask'] + if inverse: + y = sum((((sum(((r >> bit) & 1) << j for j, r in enumerate(rows)) & x).bit_count() & 1) << bit) for bit in range(9)) + sign = 1-2*((mask & x).bit_count() & 1) + else: + y = sum((((r & x).bit_count() & 1) << bit) for bit, r in enumerate(rows)) + sign = 1-2*((mask & y).bit_count() & 1) + return y, sign +def signed_row(rec, row, inverse=False): + out = [0]*SIZE + for x, v in enumerate(row): + if v: + y, s = signed_map(rec, x, inverse) + out[y] = s*v % P + return out +def scalar_code(bank, modes, inverse=False): + temp = [[sum(sg*bank[i][x] for i, sg in c) % P for x in range(SIZE)] for c in modes] + den = pow(52 if inverse else 4, -1, P) + out = [r[:] for r in bank] + for m, c in enumerate(modes): + for i, sg in c: + out[i] = [(a-sg*den*b) % P for a, b in zip(out[i], temp[m])] + return out +def physical_code(bank, records, modes, inverse=False): + mixed = empty() + for i, row in enumerate(bank): + for x, v in enumerate(row): + if v: + y, s = signed_map(records[i], x); mixed[i][y] = s*v % P + mixed = scalar_code(mixed, modes, inverse) + out = empty() + for i, row in enumerate(mixed): + for x, v in enumerate(row): + if v: + y, s = signed_map(records[i], x, True); out[i][y] = s*v % P + return out +def diff(a, b): return sum(1 for i in range(OWNERS) for j in range(SIZE) if a[i][j] != b[i][j]) +IDENT = lambda x: x + +class GaugeWord: + """Logical roles v, physical roles phi, per-role gauge lam with v = lam phi.""" + + def __init__(self, p, v0, C, Ci, Q): + self.p, self.C, self.Ci, self.Q = p, C, Ci, Q + self.v = [r[:] for r in v0] + self.f = [r[:] for r in v0] + self.lam = [IDENT]*2*p + self.linv = [IDENT]*2*p + self.fails = [] + self.recodings = 0 + + def check(self, roles, tag): + for r in roles: + d = diff(self.lam[r](self.f[r]), self.v[r]) + if d: self.fails.append((tag, r, d)) + + def set_gauge(self, r, lam, linv, change): + self.f[r] = change(self.f[r]); self.lam[r] = lam; self.linv[r] = linv + self.recodings += 1 + self.check([r], 'gauge%d' % r) + + def fwd(self, j, order): + x, y = 2*j, 2*j+1 + self.v[y] = add(self.v[y], self.Q(self.v[x], True)) + src = self.f[x] + if self.lam[x] is not IDENT: src = self.lam[x](src); self.recodings += 1 + if order == 'inv-first': + src = self.Q(src, True) + if self.linv[y] is not IDENT: src = self.linv[y](src); self.recodings += 1 + else: + if self.linv[y] is not IDENT: src = self.linv[y](src); self.recodings += 1 + src = self.Q(src, True) + self.f[y] = add(self.f[y], src) + self.check([y], 'fwd%d' % j) + + def rev_add(self, j): + a, b = 2*j, 2*j+1 + self.v[a] = add(self.v[a], self.Q(self.v[b]), -1) + src = self.f[b] + if self.lam[b] is not IDENT: src = self.lam[b](src); self.recodings += 1 + src = self.Q(src) + if self.linv[a] is not IDENT: src = self.linv[a](src); self.recodings += 1 + self.f[a] = add(self.f[a], src, -1) + self.check([a], 'rev%d-add' % j) + + def rev_letter(self, j, letter): + for r in (2*j, 2*j+1): + self.v[r] = letter(self.v[r]) + self.f[r] = letter(self.f[r]) + self.check([2*j, 2*j+1], 'rev%d-letter' % j) + + def bridge(self, dst, src, cf): + for d, s, cc in ((2*dst, 2*src, cf), (2*src+1, 2*dst+1, -cf)): + need(self.lam[d] is self.lam[s] and self.linv[d] is self.linv[s], + 'gauge mismatch across bridge %d-%d' % (dst, src)) + self.v[d] = add(self.v[d], self.v[s], cc) + self.f[d] = add(self.f[d], self.f[s], cc) + self.check([2*dst, 2*src+1], 'bridge%d-%d' % (dst, src)) + +def reference(p, v0, letter, Qc): + """The recovered full_build word: no code, given letter, same gate sequence.""" + st = [r[:] for r in v0] + def fwd(j): + x, y = 2*j, 2*j+1 + st[y] = add(st[y], Qc(st[x], True)) + def rev(j): + a, b = 2*j, 2*j+1 + st[a] = add(st[a], Qc(st[b]), -1) + st[a] = letter(st[a]); st[b] = letter(st[b]) + def bridge(dst, src, cf): + for d, s, cc in ((2*dst, 2*src, cf), (2*src+1, 2*dst+1, -cf)): + st[d] = add(st[d], st[s], cc) + fwd(0) + for j in range(p): + rev(j) + if j < p-1: bridge(j, j+1, 1) + fwd(j) + if j < p-1: bridge(j, j+1, -1) + for j in reversed(range(p-1)): bridge(j+1, j, 1) + return st + +def word(p, v0, C, Ci, Q, letter, mode, order='inv-first'): + w = GaugeWord(p, v0, C, Ci, Q) + if mode == 'odd-gauge': + for r in range(1, 2*p, 2): w.set_gauge(r, C, Ci, Ci) + elif mode == 'even-gauge': + for r in range(0, 2*p, 2): w.set_gauge(r, C, Ci, Ci) + elif mode == 'coded-all': + for r in range(2*p): w.set_gauge(r, C, Ci, Ci) + coded = mode in ('odd-gauge', 'even-gauge', 'coded-all') + w.fwd(0, order if coded else 'inv-last') + for j in range(p): + if mode == 'transient': + w.set_gauge(2*j+1, C, Ci, Ci) + w.rev_add(j) + w.set_gauge(2*j+1, IDENT, IDENT, C) + w.rev_letter(j, letter) + else: + w.rev_add(j) + w.rev_letter(j, letter) + if j < p-1: w.bridge(j, j+1, 1) + w.fwd(j, order if coded else 'inv-last') + if j < p-1: w.bridge(j, j+1, -1) + for j in reversed(range(p-1)): w.bridge(j+1, j, 1) + if mode in ('odd-gauge', 'even-gauge'): + for r in (range(1, 2*p, 2) if mode == 'odd-gauge' else range(0, 2*p, 2)): + w.set_gauge(r, IDENT, IDENT, C) + return w + +def bill(w): + return {'recodings': w.recodings, 'monomial_field_maps': w.recodings*MONOMIAL_MAPS, + 'scalar_adds': w.recodings*SCALAR_ADDS, 'owned_clears': w.recodings*OWNED_CLEARS} + +def main(): + receipt = json.loads((ROOT/'research/coded-native-caller/NORMALIZERS.json').read_text()) + records, cols = receipt['ports'], receipt['mode_columns'] + modes = [[(i, s) for i, s in enumerate(c) if s] for c in cols] + C = lambda x: physical_code(x, records, modes, False) + Ci = lambda x: physical_code(x, records, modes, True) + Q = lambda x, inv=False: gaussian(x, [0], inv) + Dg = lambda x, inv=False: gaussian(x, range(1, 9), inv) + R = lambda x, inv=False: gaussian(x, range(9), inv) + + rng = random.Random(5) + def dense(): return [[rng.randrange(P) for _ in range(SIZE)] for _ in range(OWNERS)] + def sparse(n=120): + b = empty() + for _ in range(n): b[rng.randrange(OWNERS)][rng.randrange(SIZE)] = rng.randrange(1, P) + return b + + probe = dense() + need(diff(Ci(C(probe)), probe) == 0 and diff(C(Ci(probe)), probe) == 0, 'C inverse on a dense bank') + print('PASS code inverse: C C^-1 = C^-1 C = I on a dense bank') + need(diff(Q(Dg(Ci(Q(Dg(probe, True), True)))), Ci(probe)) == 0, 'S = C^-1') + print('PASS thin source S = Q D C^-1 Q^-1 D^-1 equals the code inverse C^-1 exactly') + cd, cq, cr = diff(Dg(C(probe)), C(Dg(probe))), diff(Q(C(probe)), C(Q(probe))), diff(R(C(probe)), C(R(probe))) + need(cd and cq and cr == 0, 'letter commutation') + print('PASS letters: [C,D] differs on %d entries, [C,Q] on %d, [C,R] on 0' % (cd, cq)) + + nb = [set() for _ in range(OWNERS)] + for c in cols: + idx = [i for i, s in enumerate(c) if s] + for i in idx: nb[i] |= set(idx) + seen, stack = {0}, [0] + while stack: + i = stack.pop() + for j in nb[i]: + if j not in seen: seen.add(j); stack.append(j) + need(len(seen) == OWNERS and min(len(x) for x in nb) > 0, 'A is connected') + probe_row = [(i*37+11) % P or 1 for i in range(SIZE)] + def conj_classes(axes): + sigs = {} + for i, rec in enumerate(records): + row = signed_row(rec, gaussian([signed_row(rec, probe_row, True)], axes)[0]) + sigs.setdefault(tuple(row), []).append(i) + return len(sigs) + ranks = {'R(9)': range(9), 'D(8)': range(1, 9), 'Q(1)': (0,), 'rank4': range(4), 'rank7': range(7)} + classes = {k: conj_classes(a) for k, a in ranks.items()} + need(classes['R(9)'] == 1 and all(v > 1 for k, v in classes.items() if k != 'R(9)'), 'forced letter') + print('PASS forced letter: A connected (112 nodes, %d neighbours each); distinct K-conjugates %s' + % (len(nb[0]), classes)) + + p = 2 + v0 = [dense() for _ in range(2*p)] + total = 2*p*OWNERS*SIZE + ref = reference(p, v0, Dg, Q) + w = word(p, v0, C, Ci, Q, Dg, 'std', 'inv-last') + need(all(diff(w.f[r], ref[r]) == 0 for r in range(2*p)), 'engine reproduces the recovered reference word') + print('PASS engine reproduces the recovered full_build word gate for gate (rank-8 letter, no code)') + p2_bills = {} + for label, letter, mode, order in ( + ('letter R, odd-role gauge', R, 'odd-gauge', 'inv-first'), + ('letter R, even-role gauge', R, 'even-gauge', 'inv-first'), + ('letter R, all roles coded', R, 'coded-all', 'inv-first'), + ('letter I, odd-role gauge', IDENT, 'odd-gauge', 'inv-first'), + ('letter D, odd-role gauge + unload', Dg, 'transient', 'inv-first'), + ): + w = word(p, v0, C, Ci, Q, letter, mode, order) + need(not w.fails, 'p=2 gate invariant: ' + label + ' ' + mode) + decoded = sum(diff(w.lam[r](w.f[r]), w.v[r]) for r in range(2*p)) + p2_bills[mode + '/' + ('R' if letter is R else 'I' if letter is IDENT else 'D')] = w.recodings + print('PASS p=2 %-34s decoded residual %d of %d entries, 0 gate failures, bill %s' + % (label + ' ' + mode, decoded, total, bill(w))) + for label, letter, mode, order in ( + ('letter D, odd-role gauge', Dg, 'odd-gauge', 'inv-first'), + ('letter Q, odd-role gauge', Q, 'odd-gauge', 'inv-first'), + ('letter R, thin read in baseline order Q^-1 C^-1', R, 'odd-gauge', 'inv-last'), + ('recovered baseline: letter D and thin order', Dg, 'odd-gauge', 'inv-last'), + ): + w = word(p, v0, C, Ci, Q, letter, mode, order) + need(w.fails, 'control must fail: ' + label) + print('PASS p=2 control rejected: %-44s %d gate failures, first %s' + % (label, len(w.fails), w.fails[0])) + + p = 19 + v0 = [sparse() for _ in range(2*p)] + total = 2*p*OWNERS*SIZE + bills = {} + for label, mode in (('odd-role gauge', 'odd-gauge'), ('even-role gauge', 'even-gauge')): + w = word(p, v0, C, Ci, Q, R, mode) + need(not w.fails, 'p=19 gate invariant: ' + label) + decoded = sum(diff(w.lam[r](w.f[r]), w.v[r]) for r in range(2*p)) + bills[mode] = w.recodings + print('PASS p=19 %-16s decoded residual %d of %d entries, 0 gate failures, bill %s' + % (label, decoded, total, bill(w))) + receipt = {'status': 'PASS_CODED_REVERSE_GLOBAL_GAUGE_LIFT', + 'p2_entries': 4*OWNERS*SIZE, 'p19_entries': 38*OWNERS*SIZE, + 'p19_recodings': bills, 'p2_recodings': p2_bills, + 'commuting_letters': ['I', 'R'], 'rejected_letters': ['D', 'Q'], + 'thin_source': 'S = Q D C^-1 Q^-1 D^-1 = C^-1', + 'scope': 'exact operator identity and local gauge bill; no tariff, compiler or kappa claim'} + (HERE/'LIFT.json').write_text(json.dumps(receipt, indent=2, sort_keys=True) + '\n') + print(json.dumps(receipt, sort_keys=True)) + +if __name__ == '__main__': + main() diff --git a/research/pr5270-reference-audit/verify.py b/research/pr5270-reference-audit/verify.py new file mode 100644 index 0000000000..14339c7763 --- /dev/null +++ b/research/pr5270-reference-audit/verify.py @@ -0,0 +1,198 @@ +#!/usr/bin/env python3 +"""Exact, scoped witness that PR5270's replay reference is not its thinned invoice. + +New audit: OpenAI Codex for ahrazzle. Apache-2.0. +Retained source files keep their original authorship and notices. +No full-supplier impossibility or new multiplication exponent is claimed. +""" +import ast +from collections import Counter +from fractions import Fraction +from hashlib import sha256 +import importlib.util +import json +from pathlib import Path +from types import SimpleNamespace + +HERE = Path(__file__).resolve().parent +ZERO, ONE, I = (0, 0), (1, 0), (0, 1) + +def need(ok, reason): + if not ok: + raise ValueError(reason) + +def add(a, b): + return (a[0]+b[0], a[1]+b[1]) + +def mul(a, b): + return (a[0]*b[0]-a[1]*b[1], a[0]*b[1]+a[1]*b[0]) + +def ipow(k): + return (ONE, I, (-1, 0), (0, -1))[k % 4] + +def exact_matrix(n): + return [[ONE if i == j else ZERO for j in range(n)] for i in range(n)] + +class Polynomial: + @staticmethod + def plus(a, b, coefficient=1): + out = dict(a) + for term, value in b.items(): + out[term] = out.get(term, 0)+coefficient*value + return {k: v for k, v in out.items() if v} + + @staticmethod + def monomial_times(a, term, coefficient=1): + return {tuple(x+y for x, y in zip(k, term)): coefficient*v + for k, v in a.items() if coefficient*v} + +def retained_functions(path, names, environment): + tree = ast.parse(path.read_bytes()) + selected = [n for n in tree.body if isinstance(n, ast.FunctionDef) and n.name in names] + need({n.name for n in selected} == set(names), 'missing retained function') + exec(compile(ast.Module(body=selected, type_ignores=[]), str(path), 'exec'), environment) + return environment + +def formal_matrix(p): + """Execute retained Laurent-polynomial controller, then its exact thinning. + + Evaluate q=1 and every retained odd stage letter at i. This is a valid + Gaussian eigenvalue specialization. No diagonalizer or numerical solver. + """ + env = retained_functions(HERE/'vendor/controller_verify.py', + ['controller', 'keep_of', 'thin'], + {'C': Polynomial, 'Q': Fraction}) + pat = 'I'*((p-1)//2)+'T'*(p-1-(p-1)//2) + raw, idles = env['controller'](p, env['keep_of'](p, pat), + {s: 1 for s in range(2*p+1)}) + thinned = env['thin'](raw, set(range(1, 2*p, 2))) + result = [[ZERO for _ in range(2*p)] for _ in range(2*p)] + for term, matrix in thinned.items(): + value = ipow(sum(term[1:])) + for i, row in enumerate(matrix): + for j, coefficient in enumerate(row): + need(coefficient.denominator == 1, 'integer specialization') + result[i][j] = add(result[i][j], mul((int(coefficient), 0), value)) + return result + +def listed_matrix(p, fix_middle=False, fix_outer=False, fix_bridges=False): + """Separate exact Gaussian-integer interpreter of the emitted reference. + + Boundary codes are omitted because this audits the standard() reference + to which the source claims the coded listing is gauge-equivalent. + """ + env = retained_functions(HERE/'vendor/p19_word.py', ['pattern_of', 'listing'], {}) + gates = env['listing'](p) + matrix = exact_matrix(2*p) + + def scaled(row, coefficient): + return [mul(x, coefficient) for x in row] + + def accumulate(dst, src, coefficient): + matrix[dst] = [add(x, y) for x, y in zip(matrix[dst], scaled(matrix[src], coefficient))] + + odd_bridges = 0 + for gate in gates: + kind = gate[0] + if kind in ('GAUGE_LOAD', 'GAUGE_UNLOAD'): + continue + if kind == 'FORWARD': + accumulate(gate[2], gate[1], ONE) + elif kind == 'REVERSE': + accumulate(gate[1], gate[2], (-1, 0)) + elif kind == 'LETTER': + need(gate[3] == 'R', 'changed letter') + for role in gate[1:3]: + matrix[role] = scaled(matrix[role], I) + elif kind == 'IDLE': + power = gate[3] + if gate[4] == 'middle' and fix_middle: + power = 0 + elif gate[4] in ('initial', 'terminal') and fix_outer: + # Both intervals start at an odd stage and have even length. + # Exactly half of their letters survive odd-stage thinning. + need(power % 2 == 0, 'expected even outer interval') + power //= 2 + for role in gate[1:3]: + matrix[role] = scaled(matrix[role], ipow(power)) + elif kind == 'BRIDGE': + dst, src = gate[1:3] + if dst % 2: + if fix_bridges and odd_bridges < 2*(p-1): + dst, src = src, dst + odd_bridges += 1 + accumulate(dst, src, (gate[3], 0)) + elif kind == 'SWAP': + matrix[gate[1]], matrix[gate[2]] = matrix[gate[2]], scaled(matrix[gate[1]], (-1, 0)) + else: + raise ValueError('unknown gate '+kind) + return matrix + +def native_reference_matrix(): + """Run the retained standard() itself on a genuine 512-address eigenvector. + + v[x]=(-1)^bit_1(x): central Q fixes v; full nine-axis R multiplies it by i. + Four basis-role inputs recover the full 4x4 role matrix. Arithmetic mod + 65537 is exact; i=256. This binds the independent interpreter to the actual + source reference, without running its random dense p19 experiment. + """ + spec = importlib.util.spec_from_file_location('retained_lift', HERE/'vendor/physical_gauge_lift.py') + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + env = retained_functions(HERE/'vendor/p19_word.py', + ['gaussian_power', 'pattern_of', 'standard'], {'P': 65537, 'SIZE': 512}) + prime = 65537 + vector = [1 if not x & 2 else prime-1 for x in range(512)] + need(module.gaussian([vector], [0]) == [vector], 'Q eigenvalue one') + need(module.gaussian([vector], range(9)) == [[256*x % prime for x in vector]], 'R eigenvalue i') + matrix = [[0]*4 for _ in range(4)] + for column in range(4): + initial = [[[0]*512] for _ in range(4)] + initial[column] = [vector] + out = env['standard'](2, initial, 'R', module) + for row in range(4): + coefficient = out[row][0][0] + need(out[row][0] == [coefficient*x % prime for x in vector], 'eigenvector subspace preserved') + matrix[row][column] = coefficient + return matrix + +def main(): + pins = json.loads((HERE/'SOURCES.json').read_text()) + for row in pins['files']: + need(sha256((HERE/row['local_path']).read_bytes()).hexdigest() == row['sha256'], + 'changed pinned source '+row['local_path']) + expected = formal_matrix(2) + actual = listed_matrix(2) + need(expected == [[(-1,0),ZERO,ZERO,ZERO], [ZERO,(-1,0),ZERO,ZERO], + [ZERO,ZERO,I,ZERO], [ZERO,ZERO,ZERO,I]], 'formal p2 diagonal') + need(actual == [[(0,-1),ZERO,ZERO,(1,-1)], [ZERO,(0,-1),(1,-1),ZERO], + [ZERO,ZERO,(-1,0),ZERO], [ZERO,(0,-1),(2,-1),(-1,0)]], 'literal p2 witness') + need(actual != expected, 'counterexample disappeared') + reduce_field = lambda m: [[(a+256*b) % 65537 for a,b in row] for row in m] + need(native_reference_matrix() == reduce_field(actual), 'retained source reference differs from independent interpreter') + # Reference-path consistency controls, not admission of a repaired supplier. + need(listed_matrix(2, True, True, True) == expected, 'corrected reference positive control') + need(listed_matrix(2, True, False, True) != expected, 'terminal-only defect not detected') + need(listed_matrix(2, False, True, True) != expected, 'middle-only defect not detected') + need(listed_matrix(2, True, True, False) != expected, 'bridge-only defect not detected') + expected19, actual19 = formal_matrix(19), listed_matrix(19) + need(actual19 != expected19, 'p19 mismatch absent') + need(listed_matrix(19, True, True, True) == expected19, 'p19 corrected reference positive control') + mismatches = [(i,j) for i in range(38) for j in range(38) if expected19[i][j] != actual19[i][j]] + output = { + 'status': 'PASS_SCOPED_PR5270_REFERENCE_INVOICE_COUNTEREXAMPLE', + 'source_head': pins['head'], + 'specialization': {'q': '1', 'odd_stage_letters': 'i', 'even_stage_letters': '1'}, + 'p2_formal_matrix_gaussian_pairs': expected, + 'p2_source_reference_matrix_gaussian_pairs': actual, + 'p2_retained_512_address_reference': 'matches independent Gaussian-integer interpreter modulo 65537', + 'p19_mismatched_matrix_entries': len(mismatches), + 'p19_first_mismatches': mismatches[:12], + 'positive_controls': ['corrected p2 bridge direction and idle thinning', 'corrected p19 bridge direction and idle thinning'], + 'rejected_controls': ['uncorrected p2 middle idle', 'uncorrected p2 terminal idle', 'uncorrected p2 odd-role bridge direction'], + 'scope': 'Source replay reference is not the formal thinned controller whose invoice is priced. No impossibility claim; no new kappa; no supplier repair admitted.' + } + print(json.dumps(output, indent=2)) + +if __name__ == '__main__': + main()