diff --git a/research/bit-dirty-auxiliary-registers/EXPECTED.json b/research/bit-dirty-auxiliary-registers/EXPECTED.json new file mode 100644 index 0000000000..37f65f17bc --- /dev/null +++ b/research/bit-dirty-auxiliary-registers/EXPECTED.json @@ -0,0 +1,116 @@ +{ + "runs": { + "n2_w2_s5": { + "aux_touching_terminals": 0, + "calls": 5, + "candidates": 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 + }, + "n3_w1_s3_positive": { + "aux_touching_terminals": 593, + "calls": 3, + "candidates": 1, + "data_registers": 1, + "diagonal_terminals": 604, + "projectors": 28, + "rank2_control": false, + "registers": 3, + "relation_options": 11, + "terminals_full_cube": 169, + "terminals_no_collision": 27, + "terminals_partial_cube": 408, + "terminals_sha256": "60e15b7d905aaa0a12921675231ea38c1af2c4dbc868dd89b73a6c9abdb5387c", + "words": 21952 + }, + "n3_w2_s4": { + "aux_touching_terminals": 3951, + "calls": 4, + "candidates": 0, + "data_registers": 2, + "diagonal_terminals": 4735, + "projectors": 28, + "rank2_control": false, + "registers": 3, + "relation_options": 37, + "terminals_full_cube": 757, + "terminals_no_collision": 81, + "terminals_partial_cube": 3897, + "terminals_sha256": "e9c77c42a08b89bced4363e4a2803c15539b6e1a2a075d29347dad57dfe09cbe", + "words": 614656 + }, + "n3_w2_s5": { + "aux_touching_terminals": 32373, + "calls": 5, + "candidates": 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 + }, + "n3_w2_s5_rank2_control": { + "aux_touching_terminals": 106390, + "calls": 5, + "candidates": 13067, + "data_registers": 2, + "diagonal_terminals": 136981, + "projectors": 29, + "rank2_control": true, + "registers": 3, + "relation_options": 117, + "terminals_full_cube": 16589, + "terminals_no_collision": 1024, + "terminals_partial_cube": 119368, + "terminals_sha256": "1b1d3403ff6ae9744498d3aceabe8b250dae24fa3b619a0048ab911970f08b42", + "words": 20511149 + }, + "n3_w2_s6_positive": { + "aux_touching_terminals": 273086, + "calls": 6, + "candidates": 4852, + "data_registers": 2, + "diagonal_terminals": 297982, + "projectors": 28, + "rank2_control": false, + "registers": 3, + "relation_options": 359, + "terminals_full_cube": 23725, + "terminals_no_collision": 729, + "terminals_partial_cube": 273528, + "terminals_sha256": "5bd97891305c2108ab793b39c411e8f70ec9c1448ca29bf3cb30d2df7be6fbad", + "words": 481890304 + }, + "n4_w2_s5": { + "aux_touching_terminals": 179048, + "calls": 5, + "candidates": 0, + "data_registers": 2, + "diagonal_terminals": 183432, + "projectors": 120, + "rank2_control": false, + "registers": 4, + "relation_options": 117, + "terminals_full_cube": 16860, + "terminals_no_collision": 1024, + "terminals_partial_cube": 165548, + "terminals_sha256": "1f9f1dcce7db37797d761c73f60e0dd8b8ee30e00c57c935e72bd45b09327a62", + "words": 24883200000 + } + } +} \ No newline at end of file diff --git a/research/bit-dirty-auxiliary-registers/README.md b/research/bit-dirty-auxiliary-registers/README.md new file mode 100644 index 0000000000..273bb963ee --- /dev/null +++ b/research/bit-dirty-auxiliary-registers/README.md @@ -0,0 +1,313 @@ +# Dirty auxiliary registers do not save in the two-register m = 3 bit model + +**Theorem.** In the abelian bit model of +[PR #468](../bit-three-register-lower-bound/README.md), add any number of +*dirty auxiliary* scalar registers: registers with arbitrary input that may end +at any diagonal monomial, in particular restored exactly. Two arbitrary +invertible rational `3×3` data targets still need six nonzero rank-one paid +calls. Six suffice. + +The general statement behind it holds for every address dimension `m`, every +number `W` of data registers and every number of auxiliary registers. Suppose a +word with nonzero rank-one frames reaches invertible data targets in fewer than +`mW` calls. Then its rational frame span `d` satisfies `m+1 ≤ d ≤ s−2`. +For `(m,W)=(3,2)` and `s ≤ 5`, no such `d` exists. + +This is a scoped lower bound for a formal register model. It does not change +κ or the selected record. It does not cover clean (zero-initialized) ancillas, +other paid primitives, or arbitrary free address maps between calls. Three data +registers with an auxiliary register remain open; see section 6. + +Task card: catalogue card `bit-new-register-model`, scope key +`7f5f4426ef796683c485`, drawn with seed `27c624ea8d72df2a037db8762e0bb8a6`. +The changed hypothesis is the register count: PR #468 and the open +[PR #720](https://github.com/CrocSwap/integer-mult-bounds/pull/720) state +results for exactly three scalar registers. Dirty auxiliaries are the variant +that PR #288 §1.3(b) records as deficit-neutral, so they are the economically +relevant extra registers in this model. No public claim was posted. + +## 1. Model + +Let `G=(Q^{m×m},+)`, written multiplicatively as `[A][B]=[A+B]`, and work in +`M_n(F₂[G])`. There are `n=W+k` scalar registers: data registers `0,…,W−1` and +auxiliary registers `W,…,n−1`. A paid call is + +$$ +D_N([A])=I+([A]-1)N,\qquad \operatorname{rank}_{\mathbb Q}A=1,\qquad +N=xy^T,\quad x,y\in\mathbb F_2^n,\quad y^Tx=1 . +$$ + +For `n=3` there are 28 such idempotents `N`; for `n=4` there are 120. Free +scalar mixings are absorbed into the choice of `N`, as in PR #468 §1. A word +`D_{N_1}([A_1])⋯D_{N_s}([A_s])` succeeds when + +$$ +\prod_{j=1}^{s}D_{N_j}([A_j])=\operatorname{diag}([C_0],\ldots,[C_{n-1}]), +\qquad C_0,\ldots,C_{W-1}\ \text{invertible}. \tag{1} +$$ + +Every formal coefficient must agree. The auxiliary endpoints +`C_W,…,C_{n−1}` are unconstrained; exact restoration is `C_i=0`. A dirty +auxiliary may hold any input, so (1) is an equality of whole matrices, not of +their action on a zero-initialized vector. No triangularity is imposed on the +data targets. + +Zero frames give identity factors and can be deleted. Splitting +`D_N([A])=D_N([A/2])D_N([A/2])` turns any shorter successful word into one of +any larger length. It therefore suffices to exclude exactly `s` nonzero calls. + +## 2. Disjoint subsets with at most one relation, for any register count + +**Lemma 1.** Let `A_1,…,A_k` lie in a torsion-free abelian group, and let +`N_1,…,N_k` be binary rank-one idempotents in `M_n(F₂)`, for any `n`. Suppose +the product of the factors `I+([A_j]−1)N_j` is a diagonal monomial matrix +`diag([C_0],…,[C_{n−1}])`. If the integral relation lattice of the `A_j` has +rank at most one, there are pairwise disjoint sets `S_0,…,S_{n−1}` with + +$$ +C_i=\sum_{j\in S_i}A_j\qquad(0\le i> (i * n + j)) & 1 for j in range(n)] for i in range(n)] + sq = [[sum(m[i][k] & m[k][j] for k in range(n)) & 1 for j in range(n)] + for i in range(n)] + if sq != m: + continue + rows = {tuple(r) for r in m if any(r)} + if len(rows) == 1: # rank one over F2: all nonzero rows equal + found.append(tuple(tuple(r) for r in m)) + return found + + +def cube_options(s): + """R = 0 followed by sign-normalized cube relations of support >= 2.""" + options = [None] + for code in range(3 ** s): + r, c = [], code + for _ in range(s): + r.append(c % 3 - 1) + c //= 3 + support = [v for v in r if v] + if len(support) >= 2 and support[0] > 0: + options.append(tuple(r)) + return options + + +def _reduce(vector, r): + """Canonical representative of an integer vector modulo Z r.""" + if r is None: + return tuple(vector) + pivot = next(j for j, v in enumerate(r) if v) + k = vector[pivot] * r[pivot] # |r_pivot| = 1, so the pivot entry becomes 0 + return tuple(v - k * rv for v, rv in zip(vector, r)) + + +def symbolic_product(word_matrices): + """Formal product with entries {Laurent exponent vector: 1} over F2.""" + n, s = len(word_matrices[0]), len(word_matrices) + zero = tuple([0] * s) + state = [[({zero: 1} if i == k else {}) for k in range(n)] for i in range(n)] + for j, N in enumerate(word_matrices): + e = tuple(1 if q == j else 0 for q in range(s)) + # factor = I + (t_j - 1) N = (I + N) + t_j N over F2 + factor = [[{} for _ in range(n)] for _ in range(n)] + for i in range(n): + for k in range(n): + coeff = {} + if (1 if i == k else 0) ^ N[i][k]: + coeff[zero] = 1 + if N[i][k]: + coeff[e] = 1 + factor[i][k] = coeff + new = [[{} for _ in range(n)] for _ in range(n)] + for i in range(n): + for k in range(n): + acc = {} + for m in range(n): + for ea, ca in state[i][m].items(): + for eb, cb in factor[m][k].items(): + key = tuple(x + y for x, y in zip(ea, eb)) + acc[key] = acc.get(key, 0) ^ (ca & cb) + new[i][k] = {key: 1 for key, v in acc.items() if v} + state = new + return state + + +def symbolic_terminals(state, r): + """Return the diagonal class representatives, or None if not terminal.""" + n = len(state) + reps = [] + for i in range(n): + for k in range(n): + acc = {} + for key in state[i][k]: + red = _reduce(key, r) + acc[red] = acc.get(red, []) + [key] + odd = [keys for keys in acc.values() if len(keys) % 2] + if i != k and odd: + return None + if i == k: + if len(odd) != 1: + return None + # engine convention: the smallest subset bit mask in the class + key = odd[0][0] + members = [key] if r is None else [ + tuple(x + c * y for x, y in zip(key, r)) for c in (-1, 0, 1)] + masks = [sum(b << q for q, b in enumerate(m)) for m in members + if all(b in (0, 1) for b in m)] + reps.append(min(masks)) + return reps + + +# ------------------------------------------------------ physical frames + + +def rank_q(rows): + """Exact rank of a rational matrix (list of rows).""" + m = [list(map(Fraction, row)) for row in rows] + rank, cols = 0, len(m[0]) if m else 0 + for c in range(cols): + pivot = next((i for i in range(rank, len(m)) if m[i][c] != 0), None) + if pivot is None: + continue + m[rank], m[pivot] = m[pivot], m[rank] + for i in range(len(m)): + if i != rank and m[i][c] != 0: + f = m[i][c] / m[rank][c] + m[i] = [a - f * b for a, b in zip(m[i], m[rank])] + rank += 1 + return rank + + +def frame_key(matrix): + return tuple(Fraction(x) for row in matrix for x in row) + + +def outer(u, v): + return [[Fraction(a) * Fraction(b) for b in v] for a in u] + + +def add(*mats): + return [[sum((m[i][j] for m in mats), Fraction(0)) for j in range(3)] for i in range(3)] + + +def scale(c, m): + return [[Fraction(c) * x for x in row] for row in m] + + +ZERO_KEY = frame_key([[0] * 3] * 3) + + +def formal_product(word_matrices, frames): + """Product of D_N([A]) = I + ([A]-1)N in M_n(F2[(Q^{3x3},+)]).""" + n = len(word_matrices[0]) + state = [[({ZERO_KEY} if i == k else set()) for k in range(n)] for i in range(n)] + for N, A in zip(word_matrices, frames): + a = frame_key(A) + factor = [[set() for _ in range(n)] for _ in range(n)] + for i in range(n): + for k in range(n): + entry = set() + if i == k: + entry ^= {ZERO_KEY} + if N[i][k]: + entry ^= {a} + entry ^= {ZERO_KEY} + factor[i][k] = entry + new = [[set() for _ in range(n)] for _ in range(n)] + for i in range(n): + for k in range(n): + acc = set() + for m in range(n): + for x in state[i][m]: + for y in factor[m][k]: + acc ^= {tuple(p + q for p, q in zip(x, y))} + new[i][k] = acc + state = new + return state + + +def diagonal_endpoint(state): + """Return the diagonal frames if the product is a diagonal monomial matrix.""" + n = len(state) + out = [] + for i in range(n): + for k in range(n): + if i != k and state[i][k]: + return None + if len(state[i][i]) != 1: + return None + key = next(iter(state[i][i])) + out.append([list(key[0:3]), list(key[3:6]), list(key[6:9])]) + return out + + +def random_vector(rng): + while True: + v = [Fraction(rng.randint(-5, 5), rng.randint(1, 4)) for _ in range(3)] + if any(v): + return v + + +def frames_with_relation(s, r, rng): + """Rank-one rational frames whose integral relation lattice is exactly Z r. + + Support frames share one left vector u: A_j = u v_j^T with sum r_j v_j = 0. + Requires a support of size at most four. Others are generic rank-one. + The exact relation lattice is checked by rational rank computations. + """ + for _ in range(100): + frames = [outer(random_vector(rng), random_vector(rng)) for _ in range(s)] + if r is not None: + support = [j for j in range(s) if r[j]] + u = random_vector(rng) + vs = {j: random_vector(rng) for j in support[:-1]} + last = support[-1] + vs[last] = [-sum(r[j] * vs[j][c] for j in support[:-1]) / r[last] + for c in range(3)] + if not any(vs[last]): + continue + for j in support: + frames[j] = outer(u, vs[j]) + flat = [[x for row in A for x in row] for A in frames] + expected_span = s - (0 if r is None else 1) + if rank_q(flat) != expected_span: + continue + if r is not None and any(sum(r[j] * flat[j][c] for j in range(s)) != 0 + for c in range(9)): + continue + return frames + raise RuntimeError('could not realize relation') + + +# ----------------------------------------------------------- controls + + +def six_call_construction(rng): + """Two invertible data targets in six calls, with an untouched auxiliary.""" + e = [[1 if i == k else 0 for k in range(3)] for i in range(3)] + E = [tuple(tuple(1 if (i == k == w) else 0 for k in range(3)) for i in range(3)) + for w in range(3)] + targets = [] + while len(targets) < 2: + C = [[Fraction(rng.randint(-4, 4)) for _ in range(3)] for _ in range(3)] + if rank_q(C) == 3: + targets.append(C) + word, frames = [], [] + for w, C in enumerate(targets): + for i in range(3): + column = [C[a][i] for a in range(3)] + word.append(E[w]) + frames.append(outer(column, e[i])) + return word, frames, targets + + +def check_formal_controls(seed=20261013): + rng = random.Random(seed) + result = {} + # 1. six-call positive construction with the auxiliary restored + word, frames, targets = six_call_construction(rng) + end = diagonal_endpoint(formal_product(word, frames)) + zero = [[Fraction(0)] * 3 for _ in range(3)] + assert end is not None and end[0] == targets[0] and end[1] == targets[1] + assert end[2] == zero + result['six_call_positive'] = True + # 2. its one-frame mutation is rejected + bad = [row[:] for row in frames[0]] + bad[0][0] += 1 + mutated = diagonal_endpoint(formal_product(word, [bad] + frames[1:])) + assert mutated is None or rank_q(mutated[0]) != 3 or mutated[0] != targets[0] + result['mutated_frame_changes_endpoint'] = True + # 3. a J block over all three registers with frames B, -B is the identity + J = tuple(tuple(1 for _ in range(3)) for _ in range(3)) + B = outer(random_vector(rng), random_vector(rng)) + word2 = word[:3] + [J, J] + word[3:] + frames2 = frames[:3] + [B, scale(-1, B)] + frames[3:] + end2 = diagonal_endpoint(formal_product(word2, frames2)) + assert end2 is not None and end2[:2] == targets and end2[2] == zero + # moving one J factor past a data call breaks diagonality + word3 = word[:2] + [J] + word[2:3] + [J] + word[3:] + frames3 = frames[:2] + [B] + frames[2:3] + [scale(-1, B)] + frames[3:] + assert diagonal_endpoint(formal_product(word3, frames3)) is None + result['j_block_identity_and_order_control'] = True + return result + + +def parse_terminal(line): + flag, rest = line.split(' ', 1) + word_part, rel_part, rep_part = rest.split('|') + word = list(map(int, word_part.split())) + rel = list(map(int, rel_part.split())) + reps = list(map(int, rep_part.split())) + return int(flag), word, (None if rel == [0] else tuple(rel)), reps + + +def realize_terminals(lines, n, count, seed=7): + """Realize engine terminals with physical frames and check them exactly. + + For each selected terminal the formal product of random frames having + exactly the stated relation lattice must be a diagonal monomial matrix, + the endpoint frames must be the class sums reported by the engine, and + some data target must have rank at most two. + """ + rng = random.Random(seed) + P = projectors(n) + checked = 0 + for line in lines: + flag, word, r, reps = parse_terminal(line) + if r is not None and sum(1 for v in r if v) > 4: + continue + mats = [P[p] for p in word] + frames = frames_with_relation(len(word), r, rng) + end = diagonal_endpoint(formal_product(mats, frames)) + assert end is not None, line + for i, 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[i] == expected, line + assert flag == 0 and any(rank_q(end[w]) <= 2 for w in range(2)), line + checked += 1 + if checked == count: + break + return checked + + +def compare_symbolic(lines, n, s, words): + """Compare engine terminals with the symbolic implementation on words.""" + 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(state, r) + if reps is not None: + found.add((r, tuple(reps))) + assert found == by_word.get(tuple(word), set()), word + return len(words) diff --git a/research/bit-dirty-auxiliary-registers/engine.cpp b/research/bit-dirty-auxiliary-registers/engine.cpp new file mode 100644 index 0000000000..fdfc3e21b8 --- /dev/null +++ b/research/bit-dirty-auxiliary-registers/engine.cpp @@ -0,0 +1,244 @@ +// Exhaustive exact check: abelian bit words with dirty auxiliary registers. +// +// Usage: engine N W S OUT [rank2-control] +// N scalar registers (2..4), the first W are data registers, the rest are +// dirty auxiliaries whose endpoint may be any diagonal monomial; +// 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. +// +// The optional fifth 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 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; +} + +static Mat offdiag_mask() { + Mat m = 0; + for (int i = 0; i < n; ++i) + for (int j = 0; j < n; ++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, 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]; + for (int i = 0; i < n && 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; + 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 < n; ++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 != 6) { + std::fprintf(stderr, "usage: engine N W S OUT [rank2-control]\n"); + return 2; + } + bool rank2_control = argc == 6; + if (rank2_control && std::strcmp(argv[5], "rank2-control") != 0) 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(); OFF = offdiag_mask(); + 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("{\"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, " + "\"candidates\": %llu}\n", + 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, candidates); + return 0; +} diff --git a/research/bit-dirty-auxiliary-registers/verify.py b/research/bit-dirty-auxiliary-registers/verify.py new file mode 100644 index 0000000000..2e948de525 --- /dev/null +++ b/research/bit-dirty-auxiliary-registers/verify.py @@ -0,0 +1,167 @@ +"""Replay the dirty-auxiliary register check. + +Quick mode (about one minute) compiles the engine, reruns the n=2 and n=3 +five-call searches with their positive and failure controls, and runs the +symbolic, physical-realization and formal-identity controls. ``--full`` adds +the six-call positive control, the complete n=3, s=4 symbolic comparison and +the n=4 exhaustive search (about 80 minutes). + +Usage: python3 -B research/bit-dirty-auxiliary-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 + +QUICK = [ + ('n2_w2_s5', (2, 2, 5), False), + ('n3_w2_s4', (3, 2, 4), False), + ('n3_w2_s5', (3, 2, 5), False), + ('n3_w1_s3_positive', (3, 1, 3), False), + ('n3_w2_s5_rank2_control', (3, 2, 5), True), +] +FULL = [ + ('n3_w2_s6_positive', (3, 2, 6), False), + ('n4_w2_s5', (4, 2, 5), False), +] + + +def digest(path): + h = sha256() + with path.open('rb') as f: + for block in iter(lambda: f.read(1 << 20), b''): + h.update(block) + return h.hexdigest() + + +def run_engine(binary, directory, name, args, rank2): + out = directory / f'{name}.txt' + command = [str(binary), *map(str, args), str(out)] + (['rank2-control'] if rank2 else []) + start = time.time() + result = subprocess.run(command, capture_output=True, text=True) + if result.returncode: + raise RuntimeError(f'engine failed: {command}\n{result.stderr}') + summary = json.loads(result.stdout) + summary['terminals_sha256'] = digest(out) + summary['seconds'] = round(time.time() - start, 1) + return summary, out + + +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('DIRTY_AUX_RECORDING') == '1', f'{name} missing from EXPECTED.json' + return + want = expected['runs'][name] + for key, value in want.items(): + assert summary[key] == value, (name, key, summary[key], value) + + +def rejects(function, *args): + try: + function(*args) + except AssertionError: + return True + return False + + +def checker_controls(lines5): + """Tampered engine output must be rejected by the Python checks.""" + flag, word, r, reps = controls.parse_terminal(lines5[0]) + dropped = [line for line in lines5 if line != lines5[0]] + 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' + lines5[0][1:] + out = { + 'dropped_terminal_rejected': rejects(controls.compare_symbolic, dropped, 3, 5, [tuple(word)]), + 'altered_representative_rejected': rejects(controls.realize_terminals, [rewritten], 3, 1), + 'false_candidate_flag_rejected': rejects(controls.realize_terminals, [flagged], 3, 1), + } + assert all(out.values()), out + return out + + +def replay(directory, full): + expected = json.loads((ROOT / 'EXPECTED.json').read_text()) + 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, files = {}, {} + for name, args, rank2 in QUICK + (FULL if full else []): + summary, path = run_engine(binary, directory, name, args, rank2) + check_run(name, summary, expected) + runs[name], files[name] = summary, path + + # Semantic expectations, stated independently of the recorded digests. + for name in ('n2_w2_s5', 'n3_w2_s4', 'n3_w2_s5') + (('n4_w2_s5',) if full else ()): + n, w, s = dict((q[0], q[1]) for q in QUICK + FULL)[name] + assert runs[name]['words'] == len(controls.projectors(n)) ** s + assert runs[name]['candidates'] == 0 + assert runs['n3_w2_s5']['aux_touching_terminals'] > 0 + assert runs['n3_w1_s3_positive']['candidates'] > 0 + assert runs['n3_w2_s5_rank2_control']['candidates'] > 0 + if full: + assert runs['n3_w2_s6_positive']['candidates'] > 0 + assert runs['n4_w2_s5']['aux_touching_terminals'] > 0 + + result = {'runs': runs, 'formal_controls': controls.check_formal_controls()} + lines5 = files['n3_w2_s5'].read_text().splitlines() + result['realized_terminals_n3_s5'] = controls.realize_terminals(lines5[::50], 3, 300) + assert result['realized_terminals_n3_s5'] == 300 + + lines = files['n2_w2_s5'].read_text().splitlines() + result['symbolic_words_n2_s5'] = controls.compare_symbolic( + lines, 2, 5, list(product(range(6), repeat=5))) + all5 = product(range(28), repeat=5) + sample = [word for index, word in enumerate(all5) if index % 500 == 0] + sample += sorted({tuple(controls.parse_terminal(line)[1]) for line in lines5[::20]}) + result['symbolic_words_n3_s5_sample'] = controls.compare_symbolic(lines5, 3, 5, sample) + lines4 = files['n3_w2_s4'].read_text().splitlines() + words4 = list(product(range(28), repeat=4)) + result['symbolic_words_n3_s4'] = controls.compare_symbolic( + lines4, 3, 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_DIRTY_AUXILIARY_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()