diff --git a/research/bit-clean-ancilla-registers/EXPECTED.json b/research/bit-clean-ancilla-registers/EXPECTED.json new file mode 100644 index 0000000000..3355cf768c --- /dev/null +++ b/research/bit-clean-ancilla-registers/EXPECTED.json @@ -0,0 +1,148 @@ +{ + "runs": { + "clean_n2_w2_s5": { + "aux_touching_terminals": 0, + "calls": 5, + "candidates": 0, + "clean": true, + "clean_only_terminals": 0, + "data_registers": 2, + "diagonal_terminals": 4384, + "projectors": 6, + "rank2_control": false, + "registers": 2, + "relation_options": 117, + "terminals_full_cube": 576, + "terminals_no_collision": 32, + "terminals_partial_cube": 3776, + "terminals_sha256": "b51006b7062260bf916ba4cd4a21744fd4833983a3dd660c955b3b83dcfe5a55", + "words": 7776 + }, + "clean_n3_w1_s3_positive": { + "aux_touching_terminals": 46965, + "calls": 3, + "candidates": 64, + "clean": true, + "clean_only_terminals": 46372, + "data_registers": 1, + "diagonal_terminals": 46976, + "projectors": 28, + "rank2_control": false, + "registers": 3, + "relation_options": 11, + "terminals_full_cube": 16576, + "terminals_no_collision": 4096, + "terminals_partial_cube": 26304, + "terminals_sha256": "3f10a45f89dd4082160940c4dab88d296ea8fe492f04e0d7ff88ca6a427027cd", + "words": 21952 + }, + "clean_n3_w2_s4": { + "aux_touching_terminals": 167876, + "calls": 4, + "candidates": 0, + "clean": true, + "clean_only_terminals": 163925, + "data_registers": 2, + "diagonal_terminals": 168660, + "projectors": 28, + "rank2_control": false, + "registers": 3, + "relation_options": 37, + "terminals_full_cube": 33348, + "terminals_no_collision": 4096, + "terminals_partial_cube": 131216, + "terminals_sha256": "f6d66e09ca099e797e081deaf7522e6789fe1b7f40765f2e01f5b95a4fe946cf", + "words": 614656 + }, + "clean_n3_w2_s5": { + "aux_touching_terminals": 4047060, + "calls": 5, + "candidates": 0, + "clean": true, + "clean_only_terminals": 4014687, + "data_registers": 2, + "diagonal_terminals": 4051444, + "projectors": 28, + "rank2_control": false, + "registers": 3, + "relation_options": 117, + "terminals_full_cube": 526468, + "terminals_no_collision": 32768, + "terminals_partial_cube": 3492208, + "terminals_sha256": "8d9c10d4934c43e32bf242e88325f5f0403cf947f186c1cc2b8dad1f52a70993", + "words": 17210368 + }, + "clean_n3_w2_s5_rank2_control": { + "aux_touching_terminals": 7185478, + "calls": 5, + "candidates": 134082, + "clean": true, + "clean_only_terminals": 7079088, + "data_registers": 2, + "diagonal_terminals": 7216069, + "projectors": 29, + "rank2_control": true, + "registers": 3, + "relation_options": 117, + "terminals_full_cube": 946964, + "terminals_no_collision": 59049, + "terminals_partial_cube": 6210056, + "terminals_sha256": "43c9933da98491ca4abecec076f77a6bbb5a35c3d964f00a7ca4e4dce8729fcf", + "words": 20511149 + }, + "clean_n3_w2_s6_positive": { + "aux_touching_terminals": 96603668, + "calls": 6, + "candidates": 310528, + "clean": true, + "clean_only_terminals": 96330582, + "data_registers": 2, + "diagonal_terminals": 96628564, + "projectors": 28, + "rank2_control": false, + "registers": 3, + "relation_options": 359, + "terminals_full_cube": 8397060, + "terminals_no_collision": 262144, + "terminals_partial_cube": 87969360, + "terminals_sha256": "cad21a34607e00909ec726918b3465fc8a2c3437f8007559c8486b9cafba1fcc", + "words": 481890304 + }, + "clean_n4_w2_s5": { + "aux_touching_terminals": 4012287072, + "calls": 5, + "candidates": 0, + "clean": true, + "clean_only_terminals": 4012108024, + "data_registers": 2, + "diagonal_terminals": 4012291456, + "projectors": 120, + "rank2_control": false, + "registers": 4, + "relation_options": 117, + "terminals_full_cube": 536949120, + "terminals_no_collision": 33554432, + "terminals_partial_cube": 3441787904, + "terminals_sha256": "c060adb19f8a08038d1bd0034b6c03628f79c699e35fe1fe692e84e118fef98b", + "words": 24883200000 + }, + "dirty_n3_w2_s5_regression": { + "aux_touching_terminals": 32373, + "calls": 5, + "candidates": 0, + "clean": false, + "clean_only_terminals": 0, + "data_registers": 2, + "diagonal_terminals": 36757, + "projectors": 28, + "rank2_control": false, + "registers": 3, + "relation_options": 117, + "terminals_full_cube": 4093, + "terminals_no_collision": 243, + "terminals_partial_cube": 32421, + "terminals_sha256": "081ab4c11a7bd5de896bb1a63066893159c2aaed50400c08772b70e18046f8b9", + "words": 17210368 + } + } +} diff --git a/research/bit-clean-ancilla-registers/README.md b/research/bit-clean-ancilla-registers/README.md new file mode 100644 index 0000000000..b3ba86e00a --- /dev/null +++ b/research/bit-clean-ancilla-registers/README.md @@ -0,0 +1,199 @@ +# Clean ancillas do not save in the two-register m = 3 bit model + +**Result (scoped; no new κ).** In the abelian bit model of +[PR #468](../bit-three-register-lower-bound/README.md), add one or two *clean* +auxiliary registers. A clean register starts at zero and must end at zero. +Two arbitrary invertible rational `3×3` data targets still need six nonzero +rank-one paid calls, and six suffice. + +The merged [dirty-auxiliary package](../bit-dirty-auxiliary-registers/README.md) +(PR #1882) proves six calls for any number of *dirty* auxiliaries, and it +excludes clean ones explicitly. Clean correctness is a strictly weaker +requirement: only the data columns of the endpoint are constrained. At five +calls with one clean ancilla, 4,014,687 of the 4,051,444 surviving terminals +exist only because the ancilla starts at zero. None of them gives two rank-three +targets. + +The proof has two parts: + +- **Written:** PR #468's low-span lemma survives clean ancillas (section 2). + With five calls, this leaves a frame relation lattice of rank at most one. +- **Exhaustive:** the PR #1882 engine, with its acceptance predicate relaxed to + data columns, then covers every word and every rank-≤1 collision pattern. + +The exhaustive part covers one and two clean ancillas only. Any number of clean +ancillas remains open (see Open next questions), because PR #1882's written +Lemma 1 needs the dirty hypothesis. + +Task card: `bit-new-register-model` (scope key `7084092dd726e7ba1f2f`). The +scope is refined: the changed hypothesis is the auxiliary-register *input* +convention, inside the larger register model that PR #1882 already opened. +Claim: [discussion #2073](https://github.com/CrocSwap/integer-mult-bounds/discussions/2073). + +## 1. Model + +As in PR #1882: `G=(Q^{3×3},+)`, written multiplicatively, and matrices over +`F₂[G]`. There are `n=W+k` scalar registers. Registers `0,…,W−1` hold data; +`W,…,n−1` are auxiliary. A paid call is + +$$ +D_N([A])=I+([A]-1)N,\qquad \operatorname{rank}_{\mathbb Q}A=1,\qquad +N=xy^T,\ y^Tx=1 . +$$ + +With the column-vector convention, `D_N([A])` maps `v` to `v+([A]−1)x(yᵀv)`, +so column `k` of a product is the image of input register `k`. A word with +endpoint `P` **succeeds with clean ancillas** when + +$$ +P e_w=[C_w]\,e_w\quad (w 4: + continue + mats = [P[p] for p in word] + frames = frames_with_relation(len(word), r, rng) + state = formal_product(mats, frames) + if require_clean_only and diagonal_endpoint(state) is not None: + continue + end = clean_endpoint(state, W) + assert end is not None, line + assert len(reps) == W, line + for w, rep in enumerate(reps): + expected = add(*[frames[j] for j in range(len(word)) if rep >> j & 1]) \ + if rep else [[Fraction(0)] * 3 for _ in range(3)] + assert end[w] == expected, line + assert flag == 0 and any(rank_q(end[w]) <= 2 for w in range(W)), line + checked += 1 + if checked == count: + break + return checked + + +def compare_symbolic(lines, n, W, s, words): + """Compare clean engine terminals with the symbolic implementation.""" + P = projectors(n) + options = cube_options(s) + by_word = {} + for line in lines: + flag, word, r, reps = parse_terminal(line) + by_word.setdefault(tuple(word), set()).add((r, tuple(reps))) + for word in words: + state = symbolic_product([P[p] for p in word]) + found = set() + for r in options: + reps = symbolic_terminals_clean(state, r, W) + if reps is not None: + found.add((r, tuple(reps))) + assert found == by_word.get(tuple(word), set()), word + return len(words) + + +def clean_only_control(seed=20261014): + """Two calls that are correct only because the auxiliary starts at zero. + + Registers (x0, x1, a). Call 1 reads x0 + a and writes x0 (frame A). + Call 2 reads a and writes x0 and a (frame B). With a = 0 the second call + sees zero, so the data columns are [A] e_0 and e_1; the auxiliary column + is not diagonal. The clean predicate accepts, the dirty one rejects. + """ + rng = random.Random(seed) + P = projectors(3) + + def proj(x, y): + return tuple(tuple(x[i] * y[k] for k in range(3)) for i in range(3)) + first, second = proj((1, 0, 0), (1, 0, 1)), proj((1, 0, 1), (0, 0, 1)) + assert first in P and second in P + A = outer(dirty.random_vector(rng), dirty.random_vector(rng)) + B = outer(dirty.random_vector(rng), dirty.random_vector(rng)) + state = formal_product([first, second], [A, B]) + zero = [[Fraction(0)] * 3 for _ in range(3)] + assert diagonal_endpoint(state) is None + assert clean_endpoint(state, 2) == [A, zero] + # writing the result into the auxiliary instead is rejected by both + leak = formal_product([proj((0, 0, 1), (1, 0, 1))], [A]) + assert clean_endpoint(leak, 2) is None + return True diff --git a/research/bit-clean-ancilla-registers/engine.cpp b/research/bit-clean-ancilla-registers/engine.cpp new file mode 100644 index 0000000000..f3f8015f17 --- /dev/null +++ b/research/bit-clean-ancilla-registers/engine.cpp @@ -0,0 +1,282 @@ +// Exhaustive exact check: abelian bit words with clean (zero-initialized) +// auxiliary registers. Adapted from research/bit-dirty-auxiliary-registers. +// +// Usage: engine N W S OUT [clean] [rank2-control] +// N scalar registers (2..4), the first W are data registers, the rest are +// auxiliaries. Without "clean" they are dirty: arbitrary input, any +// diagonal monomial endpoint. With "clean" they start at zero and must +// end at zero, so only the data columns of the endpoint are constrained: +// column w < W must be [C_w] e_w (column-vector convention); +// S number of paid calls (1..6); +// OUT file receiving one line per diagonal terminal. +// +// Every ordered word of S binary rank-one idempotents is expanded as +// P(t) = prod_j ((I+N_j) + t_j N_j) = sum_a M_a t^a, a in {0,1}^S. +// The physical relation lattice of the rational frames is assumed to have +// rank at most one (the frame span is at least S-1); see README section 4. +// Option R=0 covers every relation lattice without subset collisions; +// otherwise subset monomials a,b collide exactly when a-b = +-r for a +// cube vector r in {-1,0,1}^S. For each option the formal coefficients are +// grouped, a diagonal monomial endpoint is required, and every data target is +// tested for the rank-at-most-two obstruction c in Qr + span(e_i,e_j). +// A terminal that survives this test would be reported as a candidate. +// All arithmetic is over F2 bit masks and small integers. +// +// In clean mode the off-diagonal test is applied to data columns only (every +// row, including auxiliary rows) and the one-monomial test to data diagonal +// entries only. Auxiliary columns are unconstrained. +// +// The optional argument "rank2-control" adds the rank-two scalar +// idempotent E00+E11, which lies outside the model. It is a failure control: +// one such call multiplies both data registers by one frame. + +#include +#include +#include +#include +#include + +using Mat = uint32_t; // row i occupies bits [i*n, i*n+n) + +static int n, W, S; +static bool clean_mode = false; + +static inline int bit(Mat m, int i, int j) { return (m >> (i * n + j)) & 1u; } + +static Mat mul(Mat a, Mat b) { + Mat c = 0; + const Mat rowmask = (1u << n) - 1u; + for (int i = 0; i < n; ++i) { + Mat row = 0; + for (int k = 0; k < n; ++k) + if (bit(a, i, k)) row ^= (b >> (k * n)) & rowmask; + c |= row << (i * n); + } + return c; +} + +static Mat identity() { + Mat m = 0; + for (int i = 0; i < n; ++i) m |= 1u << (i * n + i); + return m; +} + +// Entries that must vanish: all off-diagonal entries (dirty), or the +// off-diagonal entries of the data columns only (clean). +static Mat offdiag_mask(int columns) { + Mat m = 0; + for (int i = 0; i < n; ++i) + for (int j = 0; j < columns; ++j) + if (i != j) m |= 1u << (i * n + j); + return m; +} + +// Rank over F2 of an n x n bit matrix. +static int rank2(Mat m) { + int rows[4]; + const Mat rowmask = (1u << n) - 1u; + for (int i = 0; i < n; ++i) rows[i] = (m >> (i * n)) & rowmask; + int r = 0; + for (int c = 0; c < n; ++c) { + int p = -1; + for (int i = r; i < n; ++i) + if ((rows[i] >> c) & 1) { p = i; break; } + if (p < 0) continue; + std::swap(rows[r], rows[p]); + for (int i = 0; i < n; ++i) + if (i != r && ((rows[i] >> c) & 1)) rows[i] ^= rows[r]; + ++r; + } + return r; +} + +struct Relation { + std::vector r; // entries in {-1,0,1}; empty means R = 0 + uint64_t paired = 0; // subsets a that have a partner a+r or a-r + std::vector partner; // partner[a] or -1 +}; + +static std::vector projectors; +static std::vector relations; +static Mat OFF, FULL_OFF, ID; +static FILE* out; +static unsigned long long words = 0, terminals = 0, candidates = 0; +static unsigned long long terminals_by_option_kind[3] = {0, 0, 0}; // none, support layer[8]; + +// c + lambda r has support of size <= 2 for some rational lambda. +// Only lambda in {-1,0,1} can lower the support below that of lambda = 0. +static bool rank_at_most_two(int c, const std::vector& r) { + for (int lam = -1; lam <= 1; ++lam) { + if (r.empty() && lam != 0) continue; + int support = 0; + for (int j = 0; j < S; ++j) { + int v = ((c >> j) & 1) + (r.empty() ? 0 : lam * r[j]); + if (v != 0) ++support; + } + if (support <= 2) return true; + } + return false; +} + +static void check_word(const std::vector& M) { + ++words; + const int A = 1 << S; + uint64_t bad = 0; + for (int a = 0; a < A; ++a) + if (M[a] & OFF) bad |= 1ull << a; + for (size_t ri = 0; ri < relations.size(); ++ri) { + const Relation& rel = relations[ri]; + if ((bad & ~rel.paired) != 0) continue; + // grouped coefficients; class representative is the smaller subset mask + bool ok = true; + for (int a = 0; a < A && ok; ++a) { + int b = rel.partner.empty() ? -1 : rel.partner[a]; + if (b >= 0 && b < a) continue; + Mat g = M[a] ^ (b >= 0 ? M[b] : 0u); + if (g & OFF) ok = false; + } + if (!ok) continue; + int rep[4]; + const int checked = clean_mode ? W : n; + for (int i = 0; i < checked && ok; ++i) { + int count = 0; + for (int a = 0; a < A; ++a) { + int b = rel.partner.empty() ? -1 : rel.partner[a]; + if (b >= 0 && b < a) continue; + int g = bit(M[a], i, i) ^ (b >= 0 ? bit(M[b], i, i) : 0); + if (g) { ++count; rep[i] = a; } + } + if (count != 1) ok = false; // the endpoint entry must be one monomial + } + if (!ok) continue; + ++terminals; + if (clean_mode) { + // Would this grouping also be a dirty terminal? + bool dirty_ok = true; + for (int a = 0; a < A && dirty_ok; ++a) { + int b = rel.partner.empty() ? -1 : rel.partner[a]; + if (b >= 0 && b < a) continue; + Mat g = M[a] ^ (b >= 0 ? M[b] : 0u); + if (g & FULL_OFF) dirty_ok = false; + } + for (int i = W; i < n && dirty_ok; ++i) { + int count = 0; + for (int a = 0; a < A; ++a) { + int b = rel.partner.empty() ? -1 : rel.partner[a]; + if (b >= 0 && b < a) continue; + count += bit(M[a], i, i) ^ (b >= 0 ? bit(M[b], i, i) : 0); + } + if (count != 1) dirty_ok = false; + } + if (!dirty_ok) ++clean_only_terminals; + } + int kind = rel.r.empty() ? 0 : 1; + if (kind) { + int sup = 0; + for (int v : rel.r) sup += v != 0; + if (sup == S) kind = 2; + } + ++terminals_by_option_kind[kind]; + bool aux = false; + for (int j = 0; j < S; ++j) { + Mat N = projectors[word[j]]; + for (int i = 0; i < n; ++i) + for (int k = 0; k < n; ++k) + if ((i >= W || k >= W) && bit(N, i, k)) aux = true; + } + if (aux) ++aux_touching_terminals; + bool survivor = true; + for (int w = 0; w < W; ++w) + if (rank_at_most_two(rep[w], rel.r)) survivor = false; + if (survivor) ++candidates; + std::fprintf(out, "%d", survivor ? 1 : 0); + for (int j = 0; j < S; ++j) std::fprintf(out, " %d", word[j]); + std::fprintf(out, " |"); + if (rel.r.empty()) std::fprintf(out, " 0"); + else for (int v : rel.r) std::fprintf(out, " %d", v); + std::fprintf(out, " |"); + for (int i = 0; i < checked; ++i) std::fprintf(out, " %d", rep[i]); + std::fprintf(out, "\n"); + } +} + +static void dfs(int depth) { + if (depth == S) { check_word(layer[S]); return; } + const std::vector& prev = layer[depth]; + std::vector& next = layer[depth + 1]; + for (size_t p = 0; p < projectors.size(); ++p) { + word[depth] = (int)p; + Mat N = projectors[p], IN = ID ^ N; + const int A = 1 << depth; + for (int a = 0; a < A; ++a) { + next[a] = mul(prev[a], IN); + next[a | (1 << depth)] = mul(prev[a], N); + } + dfs(depth + 1); + } +} + +int main(int argc, char** argv) { + if (argc < 5 || argc > 7) { + std::fprintf(stderr, "usage: engine N W S OUT [clean] [rank2-control]\n"); + return 2; + } + bool rank2_control = false; + for (int k = 5; k < argc; ++k) { + if (std::strcmp(argv[k], "clean") == 0) clean_mode = true; + else if (std::strcmp(argv[k], "rank2-control") == 0) rank2_control = true; + else return 2; + } + n = std::atoi(argv[1]); W = std::atoi(argv[2]); S = std::atoi(argv[3]); + if (n < 2 || n > 4 || W < 1 || W > n || S < 1 || S > 6) return 2; + out = std::fopen(argv[4], "w"); + if (!out) return 2; + ID = identity(); FULL_OFF = offdiag_mask(n); + OFF = clean_mode ? offdiag_mask(W) : FULL_OFF; + for (Mat m = 1; m < (1u << (n * n)); ++m) + if (mul(m, m) == m && rank2(m) == 1) projectors.push_back(m); + if (rank2_control) projectors.push_back((1u << 0) | (1u << (n + 1))); + // relation options: R = 0, then cube vectors up to sign with support >= 2 + relations.push_back(Relation()); + int total = 1; + for (int j = 0; j < S; ++j) total *= 3; + for (int code = 0; code < total; ++code) { + std::vector r(S); + int c = code, sup = 0, first = 0; + for (int j = 0; j < S; ++j) { r[j] = c % 3 - 1; c /= 3; } + for (int j = 0; j < S; ++j) if (r[j]) { ++sup; if (!first) first = r[j]; } + if (sup < 2 || first < 0) continue; // A_j = 0 excluded; sign normalized + Relation rel; rel.r = r; rel.partner.assign(1 << S, -1); + for (int a = 0; a < (1 << S); ++a) { + int b = 0; bool valid = true; + for (int j = 0; j < S; ++j) { + int v = ((a >> j) & 1) + r[j]; + if (v < 0 || v > 1) { valid = false; break; } + b |= v << j; + } + if (valid) { rel.partner[a] = b; rel.partner[b] = a; } + } + for (int a = 0; a < (1 << S); ++a) + if (rel.partner[a] >= 0) rel.paired |= 1ull << a; + relations.push_back(rel); + } + for (int d = 0; d <= S; ++d) layer[d].assign(1 << d, 0); + layer[0][0] = ID; + dfs(0); + std::fclose(out); + std::printf("{\"clean\": %s, \"rank2_control\": %s, \"registers\": %d, \"data_registers\": %d, " + "\"calls\": %d, \"projectors\": %zu, \"relation_options\": %zu, " + "\"words\": %llu, \"diagonal_terminals\": %llu, " + "\"terminals_no_collision\": %llu, \"terminals_partial_cube\": %llu, " + "\"terminals_full_cube\": %llu, \"aux_touching_terminals\": %llu, " + "\"clean_only_terminals\": %llu, \"candidates\": %llu}\n", + clean_mode ? "true" : "false", rank2_control ? "true" : "false", n, W, S, projectors.size(), + relations.size(), words, terminals, terminals_by_option_kind[0], + terminals_by_option_kind[1], terminals_by_option_kind[2], + aux_touching_terminals, clean_only_terminals, candidates); + return 0; +} diff --git a/research/bit-clean-ancilla-registers/verify.py b/research/bit-clean-ancilla-registers/verify.py new file mode 100644 index 0000000000..89e3c49b27 --- /dev/null +++ b/research/bit-clean-ancilla-registers/verify.py @@ -0,0 +1,206 @@ +"""Replay the clean-ancilla register check. + +Quick mode (about one minute) compiles the engine, checks that its dirty mode +reproduces the merged PR #1882 digest byte for byte, reruns the n=2 and n=3 +clean searches with positive and failure controls, and runs the symbolic, +physical-realization and clean-only controls. ``--full`` adds the clean +six-call positive control, the complete n=3, s=4 symbolic comparison and the +n=4 exhaustive clean search (about 2.5 hours). + +Terminal lines are streamed through SHA-256 rather than stored, because the +clean n=4 and s=6 runs emit tens of gigabytes. + +Usage: python3 -B research/bit-clean-ancilla-registers/verify.py + [--full] [--work-dir DIR] [--record PATH] +""" + +from hashlib import sha256 +from itertools import product +from pathlib import Path +from tempfile import TemporaryDirectory +import argparse +import json +import os +import platform +import subprocess +import sys +import time + +ROOT = Path(__file__).resolve().parent +sys.path.insert(0, str(ROOT)) +import controls # noqa: E402 + +DIRTY_EXPECTED = ROOT.parent / 'bit-dirty-auxiliary-registers' / 'EXPECTED.json' + +# name, (n, W, s), flags, keep all lines in memory +QUICK = [ + ('dirty_n3_w2_s5_regression', (3, 2, 5), [], False), + ('clean_n2_w2_s5', (2, 2, 5), ['clean'], True), + ('clean_n3_w2_s4', (3, 2, 4), ['clean'], True), + ('clean_n3_w2_s5', (3, 2, 5), ['clean'], True), + ('clean_n3_w1_s3_positive', (3, 1, 3), ['clean'], False), + ('clean_n3_w2_s5_rank2_control', (3, 2, 5), ['clean', 'rank2-control'], False), +] +FULL = [ + ('clean_n3_w2_s6_positive', (3, 2, 6), ['clean'], False), + ('clean_n4_w2_s5', (4, 2, 5), ['clean'], False), +] +SAMPLE_EVERY = 1000 + + +def run_engine(binary, args, flags, keep): + """Run the engine, streaming its terminal lines through SHA-256.""" + read_fd, write_fd = os.pipe() + command = [str(binary), *map(str, args), f'/dev/fd/{write_fd}', *flags] + start = time.time() + proc = subprocess.Popen(command, stdout=subprocess.PIPE, stderr=subprocess.PIPE, + pass_fds=(write_fd,), text=True) + os.close(write_fd) + h, lines, sample, count, flagged = sha256(), [], [], 0, 0 + with os.fdopen(read_fd, 'rb') as stream: + for raw in stream: + h.update(raw) + line = raw.decode().rstrip('\n') + flagged += line.startswith('1 ') + if keep: + lines.append(line) + elif count % SAMPLE_EVERY == 0: + sample.append(line) + count += 1 + out, err = proc.communicate() + if proc.returncode: + raise RuntimeError(f'engine failed: {command}\n{err}') + summary = json.loads(out) + assert summary['diagonal_terminals'] == count, (summary, count) + assert summary['candidates'] == flagged, (summary, flagged) + summary['terminals_sha256'] = h.hexdigest() + summary['seconds'] = round(time.time() - start, 1) + return summary, (lines if keep else sample) + + +def check_run(name, summary, expected): + if name not in expected['runs']: + # Only while first recording a new run; replays require every entry. + assert os.environ.get('CLEAN_ANCILLA_RECORDING') == '1', f'{name} missing from EXPECTED.json' + return + for key, value in expected['runs'][name].items(): + assert summary[key] == value, (name, key, summary[key], value) + + +def rejects(function, *args, **kwargs): + try: + function(*args, **kwargs) + except AssertionError: + return True + return False + + +def checker_controls(lines5): + """Tampered engine output must be rejected by the Python checks.""" + first = next(line for line in lines5 if line.startswith('0 ')) + flag, word, r, reps = controls.parse_terminal(first) + dropped = [line for line in lines5 if line != first] + altered = reps[:] + altered[0] ^= 1 << (len(word) - 1) + rewritten = ' '.join(['0', *map(str, word), '|', + *(map(str, r) if r else ['0']), '|', *map(str, altered)]) + flagged = '1' + first[1:] + # a dirty-only line (three representatives) is not a clean terminal record + padded = first + ' 0' + out = { + 'dropped_terminal_rejected': rejects(controls.compare_symbolic, dropped, 3, 2, 5, [tuple(word)]), + 'altered_representative_rejected': rejects(controls.realize_terminals, [rewritten], 3, 2, 1), + 'false_candidate_flag_rejected': rejects(controls.realize_terminals, [flagged], 3, 2, 1), + 'wrong_arity_rejected': rejects(controls.realize_terminals, [padded], 3, 2, 1), + } + assert all(out.values()), out + return out + + +def replay(directory, full): + expected = json.loads((ROOT / 'EXPECTED.json').read_text()) + dirty_expected = json.loads(DIRTY_EXPECTED.read_text())['runs']['n3_w2_s5'] + compiler = os.environ.get('CXX', 'c++') + binary = directory / 'engine' + subprocess.run([compiler, '-O3', '-std=c++17', str(ROOT / 'engine.cpp'), '-o', str(binary)], + check=True) + runs, lines = {}, {} + for name, args, flags, keep in QUICK + (FULL if full else []): + summary, kept = run_engine(binary, args, flags, keep) + check_run(name, summary, expected) + runs[name], lines[name] = summary, kept + + # The dirty mode is the merged PR #1882 engine, byte for byte on output. + regression = runs['dirty_n3_w2_s5_regression'] + for key, value in dirty_expected.items(): + assert regression[key] == value, ('PR1882 regression', key) + assert regression['clean_only_terminals'] == 0 + + # Semantic expectations, stated independently of the recorded digests. + shapes = {q[0]: q[1] for q in QUICK + FULL} + for name in ('clean_n2_w2_s5', 'clean_n3_w2_s4', 'clean_n3_w2_s5') + \ + (('clean_n4_w2_s5',) if full else ()): + n, w, s = shapes[name] + assert runs[name]['words'] == len(controls.projectors(n)) ** s + assert runs[name]['candidates'] == 0 + assert runs['clean_n2_w2_s5']['clean_only_terminals'] == 0 # no auxiliary + assert runs['clean_n3_w2_s5']['clean_only_terminals'] > 0 # relaxation is used + assert runs['clean_n3_w2_s5']['diagonal_terminals'] > regression['diagonal_terminals'] + assert runs['clean_n3_w1_s3_positive']['candidates'] > 0 + assert runs['clean_n3_w2_s5_rank2_control']['candidates'] > 0 + if full: + assert runs['clean_n3_w2_s6_positive']['candidates'] > 0 + assert runs['clean_n4_w2_s5']['clean_only_terminals'] > 0 + + result = {'runs': runs, + 'pr1882_formal_controls': controls.dirty.check_formal_controls(), + 'clean_only_control': controls.clean_only_control()} + lines5 = lines['clean_n3_w2_s5'] + result['realized_terminals_n3_s5'] = controls.realize_terminals(lines5[::5000], 3, 2, 300) + result['realized_clean_only_n3_s5'] = controls.realize_terminals( + lines5[1::997], 3, 2, 300, require_clean_only=True) + assert result['realized_terminals_n3_s5'] == 300 + assert result['realized_clean_only_n3_s5'] == 300 + if full: + sample4 = lines['clean_n4_w2_s5'] + result['realized_clean_only_n4_s5'] = controls.realize_terminals( + sample4, 4, 2, 300, require_clean_only=True) + assert result['realized_clean_only_n4_s5'] == 300 + + result['symbolic_words_n2_s5'] = controls.compare_symbolic( + lines['clean_n2_w2_s5'], 2, 2, 5, list(product(range(6), repeat=5))) + sample = [word for index, word in enumerate(product(range(28), repeat=5)) if index % 5000 == 0] + sample += sorted({tuple(controls.parse_terminal(line)[1]) for line in lines5[::20000]}) + result['symbolic_words_n3_s5_sample'] = controls.compare_symbolic(lines5, 3, 2, 5, sample) + words4 = list(product(range(28), repeat=4)) + result['symbolic_words_n3_s4'] = controls.compare_symbolic( + lines['clean_n3_w2_s4'], 3, 2, 4, words4 if full else words4[::31]) + result['checker_controls'] = checker_controls(lines5) + result['mode'] = 'full' if full else 'quick' + result['environment'] = {'python': platform.python_version(), 'platform': platform.platform(), + 'compiler': compiler} + result['status'] = 'PASS_CLEAN_ANCILLA_SIX_CALLS' + return result + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument('--full', action='store_true') + parser.add_argument('--work-dir', type=Path) + parser.add_argument('--record', type=Path) + args = parser.parse_args() + if args.work_dir: + args.work_dir.mkdir(parents=True, exist_ok=True) + result = replay(args.work_dir, args.full) + else: + with TemporaryDirectory() as tmp: + result = replay(Path(tmp), args.full) + text = json.dumps(result, indent=2, sort_keys=True) + '\n' + if args.record: + args.record.write_text(text) + print(text, end='') + print(result['status']) + + +if __name__ == '__main__': + main()