diff --git a/Makefile b/Makefile index 93315aeb71..fb74dd2247 100644 --- a/Makefile +++ b/Makefile @@ -618,3 +618,13 @@ phase-recipes-parallel-benchmark: frontier1042-verify: selected-record-check @work=$$(mktemp -d "$${TMPDIR:-/tmp}/integer-mult-frontier1042.XXXXXX"); \ python3 -B scripts/verify_frontier1042.py --work "$$work/replay" + +.PHONY: hpe-audit-fast-verify hpe-audit-fast-crosscheck-lec +hpe-audit-fast-verify: + python3 -I -B research/hpe-audit-fast-seed93/verify.py + cd research/hpe-audit-fast-seed93 && python3 -B -m unittest test_package -v + +# Opt-in, about 2 minutes: all 96 trials of the selected chain's lec-p6n step, each run by both audits. +hpe-audit-fast-crosscheck-lec: + @work=$$(mktemp -d "$${TMPDIR:-/tmp}/hpe-audit-fast.XXXXXX"); \ + python3 -B research/hpe-audit-fast-seed93/run_lec.py --archived p6n --pins LEC-REASON-PINS-STACK --out "$$work/lec-p6n" --mode crosscheck diff --git a/research/hpe-audit-fast-seed93/BENCHMARK-macos-arm64.json b/research/hpe-audit-fast-seed93/BENCHMARK-macos-arm64.json new file mode 100644 index 0000000000..3f365d72ff --- /dev/null +++ b/research/hpe-audit-fast-seed93/BENCHMARK-macos-arm64.json @@ -0,0 +1,58 @@ +{ + "machine": "macOS arm64 (Darwin 27), 3.12.3", + "base": "ba82555c64e1879e4b7decce28186f208fcb8262", + "inputs": "chain//FULL-WORD.json.gz from research/community-frontier1042-audit/selected-replay.tar.gz", + "steps": { + "p6n": { + "reference_seconds": 75.2, + "fast_seconds": 30.3, + "crosscheck_seconds": 99.9, + "speedup": 2.48, + "trials_crosschecked": 96, + "receipt_identical_to_reference": true, + "receipt_equals_archived_except_word_path": true + }, + "promo": { + "reference_seconds": 76.2, + "fast_seconds": 30.3, + "crosscheck_seconds": 101.0, + "speedup": 2.51, + "trials_crosschecked": 96, + "receipt_identical_to_reference": true, + "receipt_equals_archived_except_word_path": true + }, + "jx": { + "reference_seconds": 76.0, + "fast_seconds": 29.9, + "crosscheck_seconds": 99.9, + "speedup": 2.54, + "trials_crosschecked": 96, + "receipt_identical_to_reference": true, + "receipt_equals_archived_except_word_path": true + }, + "hyb": { + "reference_seconds": 75.4, + "fast_seconds": 29.7, + "crosscheck_seconds": 99.5, + "speedup": 2.54, + "trials_crosschecked": 96, + "receipt_identical_to_reference": true, + "receipt_equals_archived_except_word_path": true + }, + "frames": { + "reference_seconds": 76.4, + "fast_seconds": 29.8, + "crosscheck_seconds": 101.1, + "speedup": 2.56, + "trials_crosschecked": 96, + "receipt_identical_to_reference": true, + "receipt_equals_archived_except_word_path": true + } + }, + "total": { + "reference_seconds": 379.2, + "fast_seconds": 150.0, + "speedup": 2.53 + }, + "note": "Wall time, sequential single process runs; machine-dependent. Not a multiplication performance measurement." +} diff --git a/research/hpe-audit-fast-seed93/FUZZ-300-SEED93.json b/research/hpe-audit-fast-seed93/FUZZ-300-SEED93.json new file mode 100644 index 0000000000..301782bbd3 --- /dev/null +++ b/research/hpe-audit-fast-seed93/FUZZ-300-SEED93.json @@ -0,0 +1,44 @@ +{ + "fuzz": { + "outcomes": { + "AssertionError ('zero-frame compensation reads an entering helper'": 27, + "AssertionError ('zero-frame precondition/compensation touches a cold hyperp": 23, + "AssertionError ('zero-frame precondition/compensation touches an entering h": 1, + "AssertionError (('arbitrary-dirt endpoint'": 168, + "AssertionError (('nonmonotone'": 10, + "AssertionError ()": 6, + "TypeError ('both arguments should be Rational instances'": 12, + "pass": 53 + }, + "seed": 93, + "trials": 300 + }, + "honest": { + "frames": { + "canonical_sha256": "002179493fa941f5ce8170d49a8e2105d5b4ff11e7d8f2feea95107be0653d11", + "identical": true + }, + "hyb": { + "canonical_sha256": "21fee0f233479a0529ac332224484af0e84e10bc3148b150b807760c7207acd2", + "identical": true + }, + "jx": { + "canonical_sha256": "c8517f65ca84e2ef9dc6a7bdb0a8830d960cc771fff587b09cd9e5abcfb5ce6e", + "identical": true + }, + "p6n": { + "canonical_sha256": "1dc0cacd73f77aaff7ff8001ff6ef3029c5c36e36ae7678dde8e9222950fb149", + "identical": true + }, + "promo": { + "canonical_sha256": "c8517f65ca84e2ef9dc6a7bdb0a8830d960cc771fff587b09cd9e5abcfb5ce6e", + "identical": true + } + }, + "status": "PASS_HPE_AUDIT_FAST_EQUIVALENCE", + "timing_seconds": { + "fast": 44.9, + "note": "machine-dependent; not part of the equivalence claim", + "reference": 135.0 + } +} diff --git a/research/hpe-audit-fast-seed93/README.md b/research/hpe-audit-fast-seed93/README.md new file mode 100644 index 0000000000..8c60894f10 --- /dev/null +++ b/research/hpe-audit-fast-seed93/README.md @@ -0,0 +1,139 @@ +# Fast exact HPE transport audit for the layer-end controls + +**Status: tooling improvement (verification engineering). No new κ. No check is changed, removed or weakened; the selected result is unchanged.** + +- **Track and seed:** track 85–94 (verification engineering), assignment seed **93** from the OS CSPRNG (Python `secrets`). +- **Base commit:** `ba82555c64e1879e4b7decce28186f208fcb8262`. +- **Adds:** this directory and two Makefile targets. No existing file is modified. + +## What is slow + +In the selected #1042 replay, the `chain` stage takes 711 s. Of that, 530 s is spent in its five layer-end control steps (`lec-p6n`, `lec-promo`, `lec-jx`, `lec-hyb`, `lec-frames`). + +Each step runs the pinned `layer_end_controls_leaver.py`. That script calls PR635's `hpe_audit_and_transport.run` (sha256 `c9a05ff2…0aa3`) about 96 times: once on the honest word, then on each of 95 mutants, every one of which must be rejected at its pinned reason. + +The cost is in exact arithmetic. On one audit, profiling shows: + +| Share | Where | +|---|---| +| ~63% | `Fraction` operations in the row updates (endpoint replay in both orientations, plus the P and P⁻¹ state maps) | +| ~22% | `copy.deepcopy` of gates | + +## What changes + +`hpe_audit_fast.py` is the pinned file with four local changes. Its control flow, every assertion, every message and every output are kept. + +1. **Integer rows.** Each scalar row is stored as integer numerators over one positive row denominator, instead of a dict of `Fraction`s. + - Each gate coefficient is still built as `Fraction(a, b)`, in the same order as before. So the `assert target != source`, `assert q` and any `ZeroDivisionError` or `TypeError` are raised exactly as in the pinned file. + - Zero entries are never stored. That makes every truth test (`if x`, `P[g].get(h)`) and every zero-pattern unchanged. + - Rows are reduced by their content gcd only when a denominator exceeds 128 bits. + - The dirty-compensation table is still built from normalized `Fraction`s, sorted as before. + - The endpoint equality is evaluated entry by entry against the pinned expected `Fraction` matrix. +2. **Structural copies.** Gates are copied structurally instead of with `deepcopy`, and nested lists are never shared. Any shape other than a list of JSON scalars and integer lists falls back to `deepcopy`. +3. **Memoized frame bases.** `basis()` is memoized for tuples of integers, which is a pure function. Any other input takes the original uncached path. +4. **Shared coefficients.** `Fraction(a, b)` objects are shared for pairs of integers with b ≠ 0. They are immutable, so sharing cannot change any value. + +### How it is used + +`shim/hpe_audit_and_transport.py` stands in for the module. The **unchanged** controls script picks it up when `PR635_CODE` points at `shim/`, which is what `run_lec.py` sets. + +`run_lec.py` repeats the chain's invocation exactly: same portable wrapper, routing word, reason-pin file and environment. It hash-pins the controls script, the wrapper, the routing word, both pin files and the reference audit. It has three modes: + +- **`reference`:** the pinned audit, unchanged. +- **`fast`:** the fast audit only. +- **`crosscheck`:** every trial word is audited by **both** implementations. Any difference in outcome raises `RuntimeError`: exception type and arguments, output bytes, receipt without `seconds`, or printed output. It never raises `AssertionError`, so no `trial()` can absorb the mismatch. The reference result is what is returned, and each outcome is logged. + +This is opt-in. Nothing in `make frontier1042-verify` changes. It composes with #1059, which parallelises the calls without changing the audit. This package makes each call cheaper. + +## Evidence + +All measurements were taken on one machine (macOS arm64, Python 3.12.3), with the same inputs, extracted from the committed `selected-replay.tar.gz`. + +| Step | Reference | Fast | Speedup | Cross-check (96 trials) | +|---|---:|---:|---:|---| +| `lec-p6n` | 75.2 s | 30.3 s | 2.48× | identical (99.9 s) | +| `lec-promo` | 76.2 s | 30.3 s | 2.51× | identical (101.0 s) | +| `lec-jx` | 76.0 s | 29.9 s | 2.54× | identical (99.9 s) | +| `lec-hyb` | 75.4 s | 29.7 s | 2.54× | identical (99.5 s) | +| `lec-frames` | 76.4 s | 29.8 s | 2.56× | identical (101.1 s) | +| **total** | **379.2 s** | **150.0 s** | **2.53×** | **480/480 identical** | + +Each `crosscheck` row means: + +- all trial words gave identical outcomes and identical outputs under both audits; +- the resulting `COLD-END-CONTROLS.json` is byte-identical to the `reference` run's; +- it equals the maintainer's archived receipt for that step, apart from the word path. + +**Differential fuzz** (`verify.py`): + +- The five honest words give byte-identical canonical and full words, receipts and printed output. +- The recorded run `FUZZ-300-SEED93.json` has 300 mutants with seed 93, and all 300 are identical under both audits. Their outcomes: + + | Outcome | Count | + |---|---:| + | rejected at the arbitrary-dirt endpoint | 168 | + | accepted (the audit passes) | 53 | + | rejected because the compensation reads an entering helper | 27 | + | rejected because the precondition or compensation touches a cold helper | 23 | + | `TypeError` from a non-integer coefficient | 12 | + | rejected as `nonmonotone` | 10 | + | empty `assert q` | 6 | + | other | 1 | + + The total time was 135.0 s for the reference and 44.9 s for the fast audit. + +The mutations are: + +- coefficient changes, including non-dyadic values; +- edge values: 0, 3⁶⁰, −5⁵⁰, 2³⁰⁰, `'x'`, 1.5 and `None`. These exercise `ZeroDivisionError`, `TypeError`, the empty `assert q` and the 128-bit normalization; +- gate drops, swaps and duplicates; +- register changes; +- frame-vector bit flips. + +**Unit tests:** + +- 300 random gate programs give integer rows equal to the pinned `Fraction` rows; +- zero entries are dropped; +- `apply` raises the same errors on bad gates as the reference; +- copies never share nested lists; +- a deliberately wrong fast audit makes `crosscheck` raise `RuntimeError` (control). + +## Reproduce + +```sh +make hpe-audit-fast-verify # about 1-2 min: 5 honest words, 40 seeded mutants, 7 unit tests +make hpe-audit-fast-crosscheck-lec # about 2 min: all 96 lec-p6n trials under both audits +``` + +The first target prints: + +``` +PASS_HPE_AUDIT_FAST_EQUIVALENCE | honest 5/5 identical | fuzz 40 seed 93 identical | reference …s fast …s +``` + +Any single step can also be run directly: + +```sh +python3 -B research/hpe-audit-fast-seed93/run_lec.py --archived hyb --pins LEC-REASON-PINS-STACK --out /tmp/x/lec-hyb --mode fast +``` + +For `lec-frames`, pass `--pins LEC-REASON-PINS`. + +## Scope + +- **What the evidence is.** Equivalence is shown by: + - a line-by-line argument (the changes are local, and they preserve values, zero patterns and exception order); + - finite differential evidence: every trial of the five selected steps, plus a seeded fuzz. + + It is not a formal proof of equivalence for every possible input. That is why `crosscheck` exists: anyone who wants the pinned semantics on new words can run both audits. +- **What it does not change.** No pinned file, reason pin, receipt or selected record is changed. +- **About the timings.** They describe one machine. They are not measurements of multiplication performance. + +## Credit + +- **Audited code:** `hpe_audit_and_transport.py` was prepared for icekylinx with GPT-6 Astra assistance. It was adapted from icekylinx's PR425/433, DreamingOfClouds' PR484 `audit_gk.py` and Round19's transport, and shipped in PR635. Its Apache-2.0 header is kept in the derived file. +- **Controls:** the layer-end controls are DreamingOfClouds' and LayerReviewer's. The leaver variant and its not-applicable handling come from LeaverSAT and Q6Reviewer, in Jeremy Kothe's #1004/#1005 chain. +- **Related work:** #1059 (thakrarsagar) parallelises the T37 layer-end controls; this package is complementary to it. +- **Precedents:** #367 applied the same `Fraction`-to-integer technique to PR364's frame verifier, and #824 to the stage-pair audit. Neither touches this audit. + +Prepared by Wronskode (@Wronskode) with substantial AI assistance from Claude (Anthropic) via Claude Code. New material is Apache-2.0. diff --git a/research/hpe-audit-fast-seed93/hpe_audit_fast.py b/research/hpe-audit-fast-seed93/hpe_audit_fast.py new file mode 100644 index 0000000000..baca651653 --- /dev/null +++ b/research/hpe-audit-fast-seed93/hpe_audit_fast.py @@ -0,0 +1,405 @@ +"""Rebuild arbitrary-dirt compensation and transport a changed local word. + +FAST EXACT VARIANT (opt-in verification tooling, seed 93). Derived from PR635's +pinned code/hpe_audit_and_transport.py (sha256 c9a05ff2...0aa3). Control flow, +assertions, messages and outputs are those of the pinned file. Only two things +change: (1) scalar rows are exact integer numerators over one positive row +denominator instead of dicts of Fractions (zero entries are never stored, so +every truth test and equality is unchanged); (2) gate copies are structural +instead of copy.deepcopy, falling back to deepcopy for any non-JSON-scalar +shape. Prepared by Wronskode (@Wronskode) with substantial AI assistance from +Claude (Anthropic) via Claude Code. Apache-2.0. + +Original header follows. +Prepared for icekylinx with GPT-6 Astra assistance. Apache-2.0. +Adapted from PR425/433 (icekylinx), PR484's audit_gk.py +(DreamingOfClouds), and Round19's 112-port transport. This auditor does not +import a constructor, a nominated compensation table, or a global price. +Only the changed scalar word and its actual frame chains are checked here. +""" +import argparse +import copy +import gzip +import hashlib +import json +import time +from collections import Counter +from fractions import Fraction as Q +from math import gcd + +_SCALAR = (int, str, type(None)) +_NORMALIZE_BITS = 128 +from pathlib import Path + + +def read(path): + data = path.read_bytes() + return json.loads(gzip.decompress(data) if path.suffix == '.gz' else data) + + +def content_hash(path): + data = path.read_bytes() + return hashlib.sha256(gzip.decompress(data) if path.suffix == '.gz' else data).hexdigest() + + +_BASIS = {} +_Q = {} + + +def basis(vs): + """Memoized for tuples of ints; any other input takes the pinned uncached path.""" + if type(vs) is tuple and all(type(x) is int for x in vs): + out = _BASIS.get(vs) + if out is None: + out = _BASIS[vs] = _basis(vs) + return out + return _basis(vs) + + +def coefficient(a, b): + """Q(a, b), shared for int pairs (Fractions are immutable); errors are raised by Q itself.""" + if type(a) is int and type(b) is int and b: + q = _Q.get((a, b)) + if q is None: + q = _Q[a, b] = Q(a, b) + return q + return Q(a, b) + + +def _basis(vs): + pivots = {} + for x in vs: + for k in sorted(pivots, reverse=True): + if x >> k & 1: + x ^= pivots[k] + if x: + k = x.bit_length() - 1 + for j in pivots: + if pivots[j] >> k & 1: + pivots[j] ^= x + pivots[k] = x + return tuple(pivots[k] for k in sorted(pivots, reverse=True)) + + +def _copy(e): + """Value-equal copy of a gate; nested objects are never shared with the input.""" + if type(e) is not list: + return copy.deepcopy(e) + out = list(e) + for i, x in enumerate(out): + if type(x) is list: + if not all(type(y) is int for y in x): + return copy.deepcopy(e) + out[i] = list(x) + elif type(x) not in _SCALAR: + return copy.deepcopy(e) + return out + + +def rows_identity(n): + """Row r is [denominator, {column: numerator}] and represents {column: numerator/denominator}.""" + return [[1, {r: 1}] for r in range(n)] + + +def _normalize(row): + d, m = row + g = d + for x in m.values(): + g = gcd(g, x) + if g == 1: + return + row[0] = d // g + for j in m: + m[j] //= g + + +def row_fractions(row): + d, m = row + return {j: Q(x, d) for j, x in m.items()} + + +def apply(e, rows): + if e[0] == 'scale': + _, target, a, b, *_ = e + q = coefficient(a, b) + assert q + d, m = rows[target] + qn = q.numerator + rows[target] = row = [d*q.denominator, {j: qn*x for j, x in m.items()}] + else: + _, target, source, a, b, *_ = e + assert target != source + q = coefficient(a, b) + td, tm = rows[target] + sd, sm = rows[source] + den = q.denominator*sd + g = gcd(td, den) + lcm = td//g*den + ft, fs = lcm//td, q.numerator*(lcm//den) + if ft != 1: + for j in tm: + tm[j] *= ft + for j, x in list(sm.items()): + value = tm.get(j, 0) + fs*x + if value: + tm[j] = value + else: + tm.pop(j, None) + row = rows[target] + row[0] = lcm + if row[0].bit_length() > _NORMALIZE_BITS: + _normalize(row) + + +def rows_equal(rows, expected): + """rows (integer form) equals expected (dicts of Fractions), entry by entry.""" + if len(rows) != len(expected): + return False + for (d, m), x in zip(rows, expected): + if m.keys() != x.keys() or any(m[j] != x[j]*d for j in m): + return False + return True + + +def inverse(e): + e = _copy(e) + if e[0] == 'add': + e[3] *= -1 + else: + e[2], e[3] = e[3], e[2] + return e + + +def dual(e): + e = inverse(e) + if e[0] == 'add': + e[1], e[2] = e[2], e[1] + return e + + +def state_maps(prefix, n): + """P = exact state map of the prefix (precondition + compensation + A + cut + B), and P^-1 (rows as sparse dicts).""" + P = rows_identity(n) + for e in prefix: + apply(e, P) + Pinv = rows_identity(n) + for e in reversed(prefix): + apply(inverse(e), Pinv) + return P, Pinv + + +def cone_violations(P, Pinv, hpe, mapping, endB, final, frames): + """COLD-HPE / CONE PRE-CHECK. Necessary conditions for helper h (raw index) to end at U = final[h] under ANY + monotone common-frame cleanup of the end-of-B state P (frames only climb, every gate at a common frame): + row (J26-H dependency bound): every g in supp(row h of P^-1) has end-of-B frame <= U -- h is rebuilt from them; + column (dirt-column lemma): every g != h with P[g][h] != 0 has end-of-B frame <= U -- the column of P at h, + restricted to rows whose frame is not <= U, changes only by invertible row operations unless h is read at a + frame not <= U, so it can reach e_h only if it is already zero there. + Both are implied by the exact endpoint replay plus the frame checks below; here they fail FAST, with the reason.""" + inside = lambda a, b: basis(frames[a] + frames[b]) == frames[b] + viol = [] + for h in hpe: + U = final[mapping[h]] + viol += [('row', h, g) for g, x in sorted(Pinv[h][1].items()) if x and not inside(endB[mapping[g]], U)] + viol += [('column', h, g) for g in range(len(P)) if g != h and P[g][1].get(h) and not inside(endB[mapping[g]], U)] + return viol + + +def run(raw_path, routing_path, out): + start_time = time.monotonic() + word, routing = read(raw_path), read(routing_path) + v, h, helpers = word['report']['v'], word['report']['h'], word['report']['R'] + assert h == 9 and v == 112 and routing['v'] == v + n = 2*v + helpers + ident = lambda: [{r: Q(1)} for r in range(n)] + main = word['A'] + word['cut'] + word['B'] + assert all(not v <= e[2] < 2*v for e in word['A'] + word['B'] + if e[0] == 'add' and not v <= e[1] < 2*v) + matrix = rows_identity(n) + for e in main: + apply(e, matrix) + dirty = [[1, {}] for _ in range(n)] + for r in range(v, 2*v): + dirty[r] = [matrix[r][0], {j: x for j, x in matrix[r][1].items() if j >= 2*v}] + for e in word['precondition']: + apply(e, dirty) + compensation = [['add', r, j, -q.numerator, q.denominator, []] + for r in range(v, 2*v) for j, q in sorted(row_fractions(dirty[r]).items())] + entering = set(map(int, word.get('start_extra', {}))) + assert all(e[2] not in entering for e in compensation), 'zero-frame compensation reads an entering helper' + cleanup = [inverse(e) for e in reversed(word['A'] + word['B']) + if not v <= e[1] < 2*v] + if 'refactored_cleanup' in word: + # REFACTORED CLEANUP (cold low-frame ends): the cleanup is not the literal reversed inverse of A+B but another exact + # factorisation of the same inverse. Nothing about it is trusted: it may only touch non-target registers (T rows + # stay the compensated data accumulators), every gate is dyadic (checked below), and the arbitrary-dirt endpoint + # replay below must be exact in BOTH orientations for the full reordered program. Inherited words keep the literal + # assertion (the else branch), so their outputs are unchanged. + assert all(not v <= r < 2*v for e in word['cleanup'] for r in ([e[1]] + ([e[2]] if e[0] == 'add' else []))), 'refactored cleanup touches a target' + assert all(e[0] in ('add', 'scale') for e in word['cleanup']) + cleanup = word['cleanup'] + else: + assert [e[:-1] for e in cleanup] == [e[:-1] for e in word['cleanup']], 'cleanup is not the literal reversed inverse of A+B' + # HPE: hyperplane-ended helpers. 'early_cleanup' = [[cleanup index, frame vectors], ...] are cleanup gates executed + # right after B (before the final climbs) at the given frame; 'helper_final' = {helper: frame vectors} replaces FULL as + # that helper's terminal frame. The scalar program is the reordered one and is replayed exactly below, so a move that + # does not commute with the skipped cleanup prefix is rejected by the arbitrary-dirt endpoint assertion. + early = [(int(i), f) for i, f in word.get('early_cleanup', [])] + helper_final = {int(r): f for r, f in word.get('helper_final', {}).items()} + early_idx = [i for i, _ in early] + assert len(set(early_idx)) == len(early_idx) and all(0 <= i < len(cleanup) for i in early_idx) + assert all(2*v <= r < n for r in helper_final) + # COLD-HPE: a COLD helper (not in start_extra, entrance frame 0 = bottom) may also end at a proper subspace U. + # It is the E = bottom instance of #593's theorems: its wrappers are the (0, U) recipes R_{0,U}, L_{0,U} (checked + # exactly by hpe_adapters_local), emitted as residual_adapter events like an entering helper's. + cold_hpe = sorted(r for r in helper_final if r not in entering) + # COLD-HPE wrapper order: R_{0,U}^-1 is emitted with the entry adapters, after the zero-frame precondition and + # compensation, so (exactly as for an entering helper, asserted above) nothing before it may touch a cold-ended helper. + assert all(r not in set(cold_hpe) for e in word['precondition'] + compensation for r in ([e[1]] + ([e[2]] if e[0] == 'add' else []))), 'zero-frame precondition/compensation touches a cold hyperplane-ended helper before its wrapper' + # ENTERING helpers (start frame E != 0): their wrapper R_E^-1 precedes every gate on them, so the zero-frame precondition + # and compensation may not touch them either (mirrors hpe_emit_local's start-frame-0 rule here, at the scalar audit). + assert all(r not in entering for e in word['precondition'] + compensation for r in ([e[1]] + ([e[2]] if e[0] == 'add' else []))), 'zero-frame precondition/compensation touches an entering helper' + tail =[word['cleanup'][i][:-1] + [f] for i, f in early] + rest = [e for i, e in enumerate(word['cleanup']) if i not in set(early_idx)] + program = word['precondition'] + compensation + main + tail + rest + for backward in (False, True): + actual = rows_identity(n) + for e in program: + apply(dual(e) if backward else e, actual) + expected = ident() + for t in range(v): + expected[t if backward else v+t][v+t if backward else t] = Q(-1 if backward else 1) + assert rows_equal(actual, expected), ('arbitrary-dirt endpoint', backward) + # The native scalar compiler allows dyadic additions and signed binary scales. + for e in program: + q = Q(e[3], e[4]) if e[0] == 'add' else Q(e[2], e[3]) + assert q.denominator & (q.denominator-1) == 0 + if e[0] == 'scale': + a = abs(q.numerator) + assert a and a & (a-1) == 0 + + tau = lambda x: x ^ (43 if (x & 43).bit_count() % 2 else 0) + ports = routing['ports'] + assert len(set(ports)) == v and set(map(tau, word['ports'])) == set(ports) + mapping = {i: ports.index(tau(p)) for i, p in enumerate(word['ports'])} + mapping.update({v+i: v+mapping[i] for i in range(v)}) + mapping.update({r: r for r in range(2*v, n)}) + full = tuple(1 << i for i in range(h-1, -1, -1)) + frames, frame_ids = [(), full], {(): 0, full: 1} + + def fid(vectors): + frame = basis(vectors) + if frame not in frame_ids: + frame_ids[frame] = len(frames) + frames.append(frame) + return frame_ids[frame] + + def transform(e): + e = _copy(e) + e[1] = mapping[e[1]] + if e[0] == 'add': + e[2] = mapping[e[2]] + if e[-1] is not None: + e[-1] = fid([tau(x) for x in e[-1]]) + return e + + canonical = {key: [transform(e) for e in word[key]] + for key in ('A', 'B', 'cut', 'cleanup', 'precondition')} + canonical['compensation'] = [transform(e) for e in compensation] + if tail: + canonical['tail'] = [transform(e) for e in tail] # HPE (absent for inherited words: identical output) + canonical['cleanup'] = [transform(e) for e in rest] # HPE (full cleanup minus the early gates) + canonical['start'] = [fid([p]) for p in ports] + [0]*(v+helpers) + for r, frame in word.get('start_extra', {}).items(): + assert 2*v <= int(r) < n + canonical['start'][int(r)] = fid([tau(x) for x in frame]) + canonical['final'] = ([1]*v + + [fid(x for x in range(1, 1 << h) if (x & p).bit_count() % 2 == 0) for p in ports] + + [1]*helpers) + for r, frame in helper_final.items(): # HPE + canonical['final'][r] = fid([tau(x) for x in frame]) + canonical.update(h=h, v=v, R=helpers, ports=ports, frames=frames, + centers=[mapping[r] for r in word['centers']], + center_frames=[fid(tau(x) for x in frame) for frame in word['center_frames']]) + levels = {mapping[v+int(t)]-v: fid(tau(x) for x in frame) + for t, frame in word.get('target_levels', {}).items()} + canonical['target_levels'] = {str(t): f for t, f in levels.items()} + current, paid, edges = canonical['start'].copy(), Counter(), set() + + def climb(r, f): + old = current[r] + assert basis(frames[old] + frames[f]) == frames[f], ('nonmonotone', r, old, f) + if old != f: + degree = len(frames[f]) - len(frames[old]) + assert degree > 0 + paid[degree] += 1 + edges.add((old, f)) + current[r] = f + + for part in ('A', 'B'): + if part == 'B': + assert all(current[r] == f for r, f in zip(canonical['centers'], canonical['center_frames'])) + assert all(current[v+t] == levels.get(t, 0) for t in range(v)) + for r, frame in zip(canonical['centers'], canonical['center_frames']): + served = {levels.get(e[1]-v, 0) for e in canonical['cut'] if e[2] == r} + old = frame + for f in sorted(served, key=lambda f: -len(frames[f])): + assert basis(frames[old] + frames[f]) == frames[old] + if old != f: + paid[len(frames[old])-len(frames[f])] += 1 + edges.add((old, f)) + edges.add((f, old)) + old = f + for e in canonical[part]: + for r in [e[1]] + ([e[2]] if e[0] == 'add' else []): + climb(r, e[-1]) + if helper_final: # COLD-HPE / CONE PRE-CHECK at the end-of-B frames + P, Pinv = state_maps(word['precondition'] + compensation + main, n) + cone = cone_violations(P, Pinv, sorted(helper_final), mapping, current.copy(), canonical['final'], frames) + assert not cone, ('hpe cone pre-check (row / column)', cone[:8]) + for e in canonical.get('tail', []): # HPE: early cleanup gates at their common frame + for r in [e[1]] + ([e[2]] if e[0] == 'add' else []): + climb(r, e[-1]) + for r, f in enumerate(canonical['final']): + climb(r, f) + # HPE: the remaining cleanup runs at FULL, so it may touch only registers whose terminal frame is FULL; a + # hyperplane-ended helper is touched by nothing after its tail gates. + for e in canonical['cleanup']: + assert all(canonical['final'][r] == 1 for r in [e[1]] + ([e[2]] if e[0] == 'add' else [])), ('cleanup on non-FULL end', e) + assert all(len(frames[canonical['final'][r]]) < h for r in helper_final) + assert dict(paid) == {int(r): count for r, count in word['report']['local_profile'].items()}, 'paid local profile differs from the reported local_profile' + canonical['local_profile'] = dict(sorted(paid.items())) + canonical['edges'] = sorted(edges) + out.mkdir(parents=True, exist_ok=False) + payload = json.dumps(canonical, sort_keys=True, separators=(',', ':')).encode() + (out/'CANONICAL-WORD.json.gz').write_bytes(gzip.compress(payload, mtime=0)) + (out/'FULL-WORD.json.gz').write_bytes(gzip.compress(json.dumps(word, sort_keys=True, separators=(',', ':')).encode(), mtime=0)) + receipt = dict(status='PASS_CHANGED_WORD_ALL_COLUMNS_AND_NATIVE_FRAMES', + input_content_sha256=content_hash(raw_path), routing_content_sha256=content_hash(routing_path), + canonical_content_sha256=hashlib.sha256(payload).hexdigest(), + live_columns_each_orientation=n, helpers=helpers, + compensation_additions=len(compensation), scalar_operations=len(program), + center_rank_sum=sum(map(len, word['center_frames'])), + local_profile=dict(sorted(paid.items())), local_rank_mass=sum(r*z for r, z in paid.items()), + widths=[len(frames[canonical['final'][r]])-len(frames[canonical['start'][r]]) for r in range(2*v, n)], + frames=len(frames), directed_edges=len(edges), + tau=43, target_port_order_matches_baseline=True, + seconds=time.monotonic()-start_time, + scope='Fresh exact forward and inverse-transpose scalar replay on every arbitrary input; all native frame chains and dyadic primitives. Phase lowering, wrappers, global owners and global assembly are separate.') + if tail or helper_final: + receipt.update(hyperplane_ended_helpers=sorted(helper_final), early_cleanup_gates=len(tail)) + if cold_hpe: # COLD-HPE (absent for words without cold ends) + receipt.update(cold_hyperplane_ended_helpers=cold_hpe) + if 'refactored_cleanup' in word: # REFACTORED CLEANUP (absent for inherited words) + receipt.update(refactored_cleanup_gates=len(word['cleanup']), refactored_cleanup=word['refactored_cleanup']) + (out/'SCALAR-FRAME-AUDIT.json').write_text(json.dumps(receipt, indent=2)+'\n') + print(json.dumps({k: value for k, value in receipt.items() if k != 'widths'}, indent=2), flush=True) + + +if __name__ == '__main__': + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--raw', type=Path, required=True) + parser.add_argument('--routing', type=Path, required=True) + parser.add_argument('--out', type=Path, required=True) + args = parser.parse_args() + run(args.raw, args.routing, args.out) diff --git a/research/hpe-audit-fast-seed93/run_lec.py b/research/hpe-audit-fast-seed93/run_lec.py new file mode 100644 index 0000000000..1ec35b98ae --- /dev/null +++ b/research/hpe-audit-fast-seed93/run_lec.py @@ -0,0 +1,91 @@ +#!/usr/bin/env python3 +"""Run the unchanged leaver layer-end controls with the fast or cross-checked audit. + +Invokes research/gauge44-leaver8/construction/leaver/layer_end_controls_leaver.py +exactly as reproduce_leaver_chain.py does (same portable wrapper, routing word +and environment), except that PR635_CODE names this package's shim directory. +Prepared by Wronskode (@Wronskode) with substantial AI assistance from Claude +(Anthropic) via Claude Code. Apache-2.0. +""" +import argparse +import hashlib +import json +import os +import subprocess +import sys +import tarfile +import tempfile +import time +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +LEAVER = ROOT / 'research/gauge44-leaver8/construction/leaver' +CONTROLS = LEAVER / 'layer_end_controls_leaver.py' +MULTICOLD = ROOT / 'research/complex-k492-owner-repair/vendor/multicold' +ROUTING = MULTICOLD / 'vendor/pr558/vendor/pr552/complex-local/inputs/phase-baseline/CANONICAL-WORD.json.gz' +ARCHIVE = ROOT / 'research/community-frontier1042-audit/selected-replay.tar.gz' +PR635_CODE = ROOT / 'research/complex-sw4-frame8/vendor/pr635/research/complex-571-cold14-st2/code' +PINS = { + CONTROLS: '4ba676f1ea326b739a64c3477f64eeb295f8151514f78fa7e62b71e4373a6206', + MULTICOLD / 'code/run_portable.py': '322d29d43dbee8130cde15d4bf05396698b5e3dfe3735813899db91cc0ba7955', + ROUTING: 'e070ae2c78b4a1b644b418774af62b40d8d16e6ba89602f0474afb557d507c37', + PR635_CODE / 'hpe_audit_and_transport.py': 'c9a05ff291016b870b4fc925b317abd9c3a604c73ffc8920dfdbbeb475e20aa3', + LEAVER / 'LEC-REASON-PINS-k8.json': 'b07279e41ec9d8f89e8509081e1e7f2c8e8b062fd951b22608a03ac461982914', + LEAVER / 'LEC-REASON-PINS-STACK-k8.json': 'd87ed7b5869bed4a3d266f0ce5fc784cbe88340a625d22ab9f580fa00872df19', +} + + +def sha(p): + return hashlib.sha256(Path(p).read_bytes()).hexdigest() + + +def main(): + ap = argparse.ArgumentParser(description=__doc__) + src = ap.add_mutually_exclusive_group(required=True) + src.add_argument('--word', type=Path) + src.add_argument('--archived', choices=['p6n', 'promo', 'jx', 'hyb', 'frames'], + help='use this word from the committed selected replay and compare with its archived receipt') + ap.add_argument('--pins', required=True, choices=['LEC-REASON-PINS', 'LEC-REASON-PINS-STACK']) + ap.add_argument('--out', type=Path, required=True) + ap.add_argument('--mode', choices=['reference', 'fast', 'crosscheck'], default='fast') + a = ap.parse_args() + for path, digest in PINS.items(): + if sha(path) != digest: + sys.exit('pinned input changed: %s' % path.relative_to(ROOT)) + out = a.out.resolve() + if out.exists(): + sys.exit('output directory must not exist') + out.parent.mkdir(parents=True, exist_ok=True) + pins = LEAVER / ('%s-k8.json' % a.pins) + archived = None + if a.archived: + with tarfile.open(ARCHIVE) as tar: + data = tar.extractfile('chain/%s/FULL-WORD.json.gz' % a.archived).read() + archived = json.loads(tar.extractfile('chain/lec-%s/COLD-END-CONTROLS.json' % a.archived).read()) + a.word = Path(tempfile.mkdtemp()) / 'FULL-WORD.json.gz' + a.word.write_bytes(data) + env = dict(os.environ, PYTHONDONTWRITEBYTECODE='1', PYTHONUTF8='1', PYTHONINTMAXSTRDIGITS='0', + MULTICOLD_SOURCE=str(MULTICOLD), GAIN_PR564_SOURCE=str(MULTICOLD), LEC_REASON_PINS=str(pins), + PR635_CODE=str(PR635_CODE if a.mode == 'reference' else HERE / 'shim'), + HPE_AUDIT_MODE='fast' if a.mode == 'reference' else a.mode, + HPE_AUDIT_REFERENCE=str(PR635_CODE / 'hpe_audit_and_transport.py'), + HPE_AUDIT_CROSSCHECK_LOG=str(out.parent / (out.name + '.crosscheck.jsonl'))) + for k in ('PYTHONOPTIMIZE', 'XPARAM', 'EXTRAH', 'PAIRING_RANKS', 'DIAG', 'HYBBUDGET', 'SW4_PIN'): + env.pop(k, None) + cmd = [sys.executable, '-B', str(MULTICOLD / 'code/run_portable.py'), str(CONTROLS), + str(a.word.resolve()), str(ROUTING), str(out)] + t = time.monotonic() + rc = subprocess.call(cmd, env=env, stdout=sys.stdout, stderr=subprocess.STDOUT) + print('MODE %s exit %d seconds %.1f' % (a.mode, rc, time.monotonic() - t), flush=True) + if rc == 0 and archived is not None: + got = json.loads((out / 'COLD-END-CONTROLS.json').read_text()) + got.pop('word'), archived.pop('word') + if got != archived: + sys.exit('receipt differs from the archived maintainer receipt') + print('PASS receipt equals the archived lec-%s receipt (apart from the word path)' % a.archived) + sys.exit(rc) + + +if __name__ == '__main__': + main() diff --git a/research/hpe-audit-fast-seed93/shim/hpe_audit_and_transport.py b/research/hpe-audit-fast-seed93/shim/hpe_audit_and_transport.py new file mode 100644 index 0000000000..40d167a589 --- /dev/null +++ b/research/hpe-audit-fast-seed93/shim/hpe_audit_and_transport.py @@ -0,0 +1,80 @@ +"""Stand-in for PR635's hpe_audit_and_transport module (opt-in tooling, seed 93). + +HPE_AUDIT_MODE=fast run() is hpe_audit_fast.run. +HPE_AUDIT_MODE=crosscheck run() executes the pinned reference and the fast + variant on the same input and raises RuntimeError + (never AssertionError, so no caller can absorb it) + unless both give the same outcome and byte-identical + outputs; the reference result is then returned. +HPE_AUDIT_REFERENCE names the pinned reference file; its sha256 is checked. +Prepared by Wronskode (@Wronskode) with substantial AI assistance from Claude +(Anthropic) via Claude Code. Apache-2.0. +""" +import contextlib +import hashlib +import importlib.util +import io +import json +import os +import shutil +import sys +import tempfile +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parents[1] +REFERENCE_SHA256 = 'c9a05ff291016b870b4fc925b317abd9c3a604c73ffc8920dfdbbeb475e20aa3' +MODE = os.environ.get('HPE_AUDIT_MODE', 'fast') +if MODE not in ('fast', 'crosscheck'): + raise RuntimeError('HPE_AUDIT_MODE must be fast or crosscheck') + + +def _load(name, path): + spec = importlib.util.spec_from_file_location(name, path) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +_fast = _load('hpe_audit_fast', PACKAGE / 'hpe_audit_fast.py') +_reference = None +if MODE == 'crosscheck': + ref_path = Path(os.environ['HPE_AUDIT_REFERENCE']) + if hashlib.sha256(ref_path.read_bytes()).hexdigest() != REFERENCE_SHA256: + raise RuntimeError('reference audit is not the pinned PR635 file') + _reference = _load('hpe_audit_reference', ref_path) +CROSSCHECKS = [] + + +def _outcome(module, raw_path, routing_path, out): + stdout = io.StringIO() + try: + with contextlib.redirect_stdout(stdout): + module.run(raw_path, routing_path, out) + except Exception as exc: # compared, then re-raised by the caller + return exc, (type(exc).__name__, repr(exc.args)), None, None + files = {p.name: p.read_bytes() for p in sorted(out.iterdir())} + receipt = json.loads(files.pop('SCALAR-FRAME-AUDIT.json')) + receipt.pop('seconds') + printed = json.loads(stdout.getvalue()) + printed.pop('seconds') + return None, None, (files, receipt, printed), stdout.getvalue() + + +def run(raw_path, routing_path, out): + if MODE == 'fast': + return _fast.run(raw_path, routing_path, out) + scratch = Path(tempfile.mkdtemp()) + try: + f_exc, f_key, f_out, _ = _outcome(_fast, raw_path, routing_path, scratch / 'fast') + r_exc, r_key, r_out, r_text = _outcome(_reference, raw_path, routing_path, out) + finally: + shutil.rmtree(scratch, ignore_errors=True) + if f_key != r_key or f_out != r_out: + raise RuntimeError(('hpe audit crosscheck mismatch', str(raw_path), r_key, f_key)) + CROSSCHECKS.append(r_key) + with open(os.environ.get('HPE_AUDIT_CROSSCHECK_LOG', os.devnull), 'a') as log: + log.write(json.dumps(dict(outcome=r_key or 'PASS', input_sha256=hashlib.sha256( + Path(raw_path).read_bytes()).hexdigest())) + '\n') + if r_exc is not None: + raise r_exc + sys.stdout.write(r_text) diff --git a/research/hpe-audit-fast-seed93/test_package.py b/research/hpe-audit-fast-seed93/test_package.py new file mode 100644 index 0000000000..16478c0d12 --- /dev/null +++ b/research/hpe-audit-fast-seed93/test_package.py @@ -0,0 +1,116 @@ +"""Unit tests for the seed-93 fast exact HPE audit. Apache-2.0.""" +import importlib.util +import random +import subprocess +import sys +import unittest +from fractions import Fraction as Q +from pathlib import Path + +HERE = Path(__file__).resolve().parent + + +def load(name, path): + spec = importlib.util.spec_from_file_location(name, path) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +F = load('hpe_fast_test', HERE / 'hpe_audit_fast.py') +R = load('hpe_reference_test', HERE.parents[1] / 'research/complex-sw4-frame8/vendor/pr635/research/' + 'complex-571-cold14-st2/code/hpe_audit_and_transport.py') + + +class RowArithmetic(unittest.TestCase): + def test_random_programs_match_fraction_rows(self): + rng = random.Random(93) + for trial in range(300): + n = rng.randrange(2, 7) + ref = [{r: Q(1)} for r in range(n)] + fast = F.rows_identity(n) + for _ in range(rng.randrange(1, 60)): + if rng.random() < 0.2: + e = ['scale', rng.randrange(n), rng.choice([-4, -1, 1, 2, 3, 2 ** 70]), rng.choice([1, 2, 3, 5 ** 30])] + else: + t, s = rng.sample(range(n), 2) + e = ['add', t, s, rng.randrange(-5, 6), rng.choice([1, 2, 4, 3, 7 ** 25])] + R.apply(e, ref) + F.apply(e, fast) + self.assertTrue(F.rows_equal(fast, ref)) + self.assertEqual([F.row_fractions(r) for r in fast], ref) + + def test_zero_entries_are_never_stored(self): + rows = F.rows_identity(2) + F.apply(['add', 0, 1, 1, 1], rows) + F.apply(['add', 0, 1, -1, 1], rows) + self.assertEqual(rows[0][1], {0: 1}) + + def test_errors_are_the_reference_errors(self): + for e in (['scale', 0, 0, 1], ['add', 0, 0, 1, 1], ['add', 0, 1, 1, 0], ['add', 0, 1, 'x', 1]): + outcomes = [] + for module, rows in ((R, [{0: Q(1)}, {1: Q(1)}]), (F, F.rows_identity(2))): + try: + module.apply(e, rows) + outcomes.append(None) + except Exception as exc: + outcomes.append((type(exc), exc.args)) + self.assertEqual(outcomes[0], outcomes[1], e) + + +class Copies(unittest.TestCase): + def test_copy_never_shares_nested_lists(self): + e = ['add', 3, 4, 1, 2, [5, 6]] + c = F._copy(e) + self.assertEqual(c, e) + c[-1].append(7) + self.assertEqual(e[-1], [5, 6]) + + def test_unusual_shapes_fall_back_to_deepcopy(self): + e = ['add', 3, 4, 1, 2, [[5]]] + c = F._copy(e) + c[-1][0].append(1) + self.assertEqual(e[-1], [[5]]) + self.assertEqual(F.inverse(e), R.inverse(e)) + self.assertEqual(F.dual(['scale', 1, 2, 3, None]), R.dual(['scale', 1, 2, 3, None])) + + +class CrosscheckControl(unittest.TestCase): + def test_wrong_fast_audit_is_caught_not_absorbed(self): + import gzip, os, tarfile, tempfile + archive = HERE.parents[1] / 'research/community-frontier1042-audit/selected-replay.tar.gz' + with tarfile.open(archive) as tar: + data = tar.extractfile('chain/p6n/FULL-WORD.json.gz').read() + tmp = Path(tempfile.mkdtemp()) + word = tmp / 'w.json.gz' + word.write_bytes(data) + os.environ.update(HPE_AUDIT_MODE='crosscheck', HPE_AUDIT_REFERENCE=str( + HERE.parents[1] / 'research/complex-sw4-frame8/vendor/pr635/research/complex-571-cold14-st2/code/' + 'hpe_audit_and_transport.py')) + try: + shim = load('hpe_shim_test', HERE / 'shim/hpe_audit_and_transport.py') + finally: + os.environ.pop('HPE_AUDIT_MODE') + + class Wrong: + @staticmethod + def run(raw, routing, out): + raise AssertionError("'arbitrary-dirt endpoint'") + shim._fast = Wrong + with self.assertRaises(RuntimeError) as cm: + shim.run(word, R.Path(str(HERE.parents[1] / 'research/complex-k492-owner-repair/vendor/multicold/vendor/' + 'pr558/vendor/pr552/complex-local/inputs/phase-baseline/CANONICAL-WORD.json.gz')), + tmp / 'out') + self.assertIn('crosscheck mismatch', str(cm.exception)) + + +class Differential(unittest.TestCase): + def test_archived_words_and_small_fuzz(self): + r = subprocess.run([sys.executable, '-I', '-B', str(HERE / 'verify.py'), '--fuzz', '5', '--seed', '7'], + capture_output=True, text=True) + self.assertEqual(r.returncode, 0, r.stdout + r.stderr) + self.assertIn('PASS_HPE_AUDIT_FAST_EQUIVALENCE', r.stdout) + + +if __name__ == '__main__': + unittest.main() diff --git a/research/hpe-audit-fast-seed93/verify.py b/research/hpe-audit-fast-seed93/verify.py new file mode 100644 index 0000000000..a61254eb67 --- /dev/null +++ b/research/hpe-audit-fast-seed93/verify.py @@ -0,0 +1,155 @@ +#!/usr/bin/env python3 +"""Differential check: fast exact HPE audit versus PR635's pinned reference. + +Inputs are read from the committed selected PR1042 replay archive. For each of +the five words whose layer-end controls the selected chain runs (p6n, promo, +jx, hyb, frames), both implementations must give byte-identical output files, +an identical receipt (apart from elapsed seconds) and identical printed output. +A seeded fuzz then mutates those words (coefficients, including zero, negative, +non-dyadic, huge and non-integer values; gate drops, swaps and duplicates; +registers; frame vectors) and requires the same outcome: the same exception +type and arguments, or the same outputs. + +Prepared by Wronskode (@Wronskode) with substantial AI assistance from Claude +(Anthropic) via Claude Code. Apache-2.0. +""" +import argparse +import contextlib +import copy +import gzip +import hashlib +import importlib.util +import io +import json +import random +import shutil +import sys +import tarfile +import tempfile +import time +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +ARCHIVE = ROOT / 'research/community-frontier1042-audit/selected-replay.tar.gz' +REFERENCE = ROOT / 'research/complex-sw4-frame8/vendor/pr635/research/complex-571-cold14-st2/code/hpe_audit_and_transport.py' +ROUTING = ROOT / ('research/complex-k492-owner-repair/vendor/multicold/vendor/pr558/vendor/pr552/' + 'complex-local/inputs/phase-baseline/CANONICAL-WORD.json.gz') +PINS = { + REFERENCE: 'c9a05ff291016b870b4fc925b317abd9c3a604c73ffc8920dfdbbeb475e20aa3', + ROUTING: 'e070ae2c78b4a1b644b418774af62b40d8d16e6ba89602f0474afb557d507c37', +} +WORDS = ('p6n', 'promo', 'jx', 'hyb', 'frames') +SECTIONS = ('A', 'B', 'cut', 'precondition', 'cleanup') + + +def load(name, path): + spec = importlib.util.spec_from_file_location(name, path) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +def outcome(module, raw, out): + printed = io.StringIO() + t = time.perf_counter() + try: + with contextlib.redirect_stdout(printed): + module.run(raw, ROUTING, out) + except Exception as exc: + return ('raise', type(exc).__name__, repr(exc.args)), time.perf_counter() - t + dt = time.perf_counter() - t + files = {p.name: p.read_bytes() for p in sorted(out.iterdir())} + receipt = json.loads(files.pop('SCALAR-FRAME-AUDIT.json')) + receipt.pop('seconds') + text = json.loads(printed.getvalue()) + text.pop('seconds') + return ('pass', files, receipt, text), dt + + +def compare(ref, fast, word, tmp, tag): + raw = tmp / (tag + '.json.gz') + raw.write_bytes(gzip.compress(json.dumps(word).encode(), mtime=0)) + r, tr = outcome(ref, raw, tmp / (tag + '-ref')) + f, tf = outcome(fast, raw, tmp / (tag + '-fast')) + if r != f: + raise SystemExit('MISMATCH %s: reference %s / fast %s' % (tag, str(r)[:300], str(f)[:300])) + return r, tr, tf + + +def mutate(word, rng): + w = copy.deepcopy(word) + n = 2 * w['report']['v'] + w['report']['R'] + sec = rng.choice([s for s in SECTIONS if w[s]]) + i = rng.randrange(len(w[sec])) + g = w[sec][i] + kind = rng.choice(['coef', 'coef', 'coef', 'edge', 'drop', 'swap', 'dup', 'reg', 'frame']) + if kind == 'coef': + k = 3 if g[0] == 'add' else 2 + g[k + rng.randrange(2)] = rng.choice([-3, -2, -1, 1, 2, 3, 5, 7, 4, 1024, -1024]) + elif kind == 'edge': + k = 3 if g[0] == 'add' else 2 + g[k + rng.choice([0, 1])] = rng.choice([0, 3 ** 60, -(5 ** 50), 2 ** 300, 'x', 1.5, None]) + elif kind == 'drop': + del w[sec][i] + elif kind == 'swap' and len(w[sec]) > 1: + j = min(i + 1, len(w[sec]) - 1) if i + 1 < len(w[sec]) else i - 1 + w[sec][i], w[sec][j] = w[sec][j], w[sec][i] + elif kind == 'dup': + w[sec].insert(i, copy.deepcopy(g)) + elif kind == 'reg': + g[1 + (rng.randrange(2) if g[0] == 'add' else 0)] = rng.randrange(n) + elif kind == 'frame' and isinstance(g[-1], list) and g[-1]: + j = rng.randrange(len(g[-1])) + g[-1][j] ^= 1 << rng.randrange(9) + return w, '%s:%s[%d]' % (kind, sec, i) + + +def main(): + ap = argparse.ArgumentParser(description=__doc__) + ap.add_argument('--fuzz', type=int, default=40, help='mutants per run (spread over the five words)') + ap.add_argument('--seed', type=int, default=93) + ap.add_argument('--receipt', type=Path, help='write a JSON receipt here') + a = ap.parse_args() + for path, digest in PINS.items(): + if hashlib.sha256(path.read_bytes()).hexdigest() != digest: + raise SystemExit('pinned input changed: %s' % path.relative_to(ROOT)) + ref = load('hpe_reference', REFERENCE) + fast = load('hpe_fast', HERE / 'hpe_audit_fast.py') + words = {} + with tarfile.open(ARCHIVE) as tar: + for name in WORDS: + words[name] = json.loads(gzip.decompress(tar.extractfile('chain/%s/FULL-WORD.json.gz' % name).read())) + tmp = Path(tempfile.mkdtemp()) + receipt = dict(honest={}, fuzz=dict(seed=a.seed, trials=a.fuzz, outcomes={})) + try: + t_ref = t_fast = 0.0 + for name, word in words.items(): + r, tr, tf = compare(ref, fast, word, tmp, 'honest-' + name) + if r[0] != 'pass': + raise SystemExit('honest word %s rejected: %s' % (name, r)) + receipt['honest'][name] = dict(canonical_sha256=hashlib.sha256(r[1]['CANONICAL-WORD.json.gz']).hexdigest(), + identical=True) + t_ref, t_fast = t_ref + tr, t_fast + tf + rng = random.Random(a.seed) + counts = receipt['fuzz']['outcomes'] + for k in range(a.fuzz): + name = WORDS[k % len(WORDS)] + w, desc = mutate(words[name], rng) + r, tr, tf = compare(ref, fast, w, tmp, 'fuzz%d' % k) + key = r[0] if r[0] == 'pass' else '%s %s' % (r[1], r[2].split(',')[0][:60]) + counts[key] = counts.get(key, 0) + 1 + t_ref, t_fast = t_ref + tr, t_fast + tf + finally: + shutil.rmtree(tmp, ignore_errors=True) + receipt['status'] = 'PASS_HPE_AUDIT_FAST_EQUIVALENCE' + receipt['timing_seconds'] = dict(reference=round(t_ref, 1), fast=round(t_fast, 1), + note='machine-dependent; not part of the equivalence claim') + if a.receipt: + a.receipt.write_text(json.dumps(receipt, indent=1, sort_keys=True) + '\n') + print('%s | honest 5/5 identical | fuzz %d seed %d identical | reference %.1fs fast %.1fs' + % (receipt['status'], a.fuzz, a.seed, t_ref, t_fast)) + + +if __name__ == '__main__': + main()