diff --git a/research/spd-dirty-circuit-witness/NOTICE.md b/research/spd-dirty-circuit-witness/NOTICE.md new file mode 100644 index 0000000000..2b9c6ba72e --- /dev/null +++ b/research/spd-dirty-circuit-witness/NOTICE.md @@ -0,0 +1,23 @@ +# Attribution and frozen source + +New proof, degree adapter, literal replay and checks: Ali Romman, with substantial +OpenAI Codex assistance. Apache-2.0. + +The two files in vendor and wrong-order.json are unchanged copies from +[PR #5235](https://github.com/CrocSwap/integer-mult-bounds/pull/5235), head +`48976daa4dce59b4867ef046da72a370e389925d`. The source is prepared for zxv with +substantial OpenAI Codex assistance, under Apache-2.0. This PR is pending and +is not part of our main base. SOURCES.json records each original path, Git blob +and SHA256, and binds the retained copies to an ancestor in this publication +history. The original proof and README are also retained in vendor. The replay +checks the copied runtime bytes; metadata checks bind all retained sources. References inside the unchanged +vendor files refer to the predecessor's proof, not to a claim of our authorship. + +Retain its weighted-automata/PIT credit to Stefan Kiefer and Ran Raz / Amir +Shpilka. The echo lineage credits androolloyd, Chafik Boukhalfa / chafreaky +[PR #628](https://github.com/CrocSwap/integer-mult-bounds/pull/628), and Ali Romman +[PR #621](https://github.com/CrocSwap/integer-mult-bounds/pull/621). +The source also retains Cinna Davis, ToikY, Sagar Thakrar, roger-sato, Charles +Bethin, Ross Richardson and the wider dirty-phase/tensor lineage. Their results +are not new results of this package. No identities are inferred from a PR's +submitter account. The source README and proof are pinned provenance. diff --git a/research/spd-dirty-circuit-witness/PROOF.md b/research/spd-dirty-circuit-witness/PROOF.md new file mode 100644 index 0000000000..b4af353647 --- /dev/null +++ b/research/spd-dirty-circuit-witness/PROOF.md @@ -0,0 +1,108 @@ +# Positive-definite separation of complete dirty circuits + +## Statement + +Use the complete linear register grammar from zxv's [PR #5235](https://github.com/CrocSwap/integer-mult-bounds/pull/5235), +head `48976daa4dce59b4867ef046da72a370e389925d`. All input and returned roles +are independent. Coefficients are central elements of Q or Q(i). Symbols have +no inverse, commutation, Clifford or other relations. Compare two finite +programs, or compare one program with an explicit polynomial endpoint. + +Let F be their matrix of noncommutative polynomial differences. If F is +nonzero, let D be the largest word degree with a nonzero coefficient in any +entry. For every rational 0 < e <= 1/4, there are real symmetric rational +matrices A_a of dimension D+1 such that: + +- every spectrum is contained in [1-2e,1]; +- each matrix is positive definite, has operator norm at most 1, and has + spectral condition number at most 1/(1-2e) <= 2; +- the literal complete endpoint difference is nonzero for one input role + equal to a coordinate vector and all other roles equal to zero. + +Thus identity on this class, in every payload dimension, is equivalent to +free-polynomial identity. Taking e arbitrarily small also gives witnesses +arbitrarily close to I in operator norm. This statement gives no lower bound +on numerical detectability. The nonzero discrepancy can be exponentially small. + +## Construction and proof + +Choose an entry (o,i) and a degree-D word w=a_1...a_D with coefficient c != 0. +Number the path vertices 0,...,D. Let S_a contain both symmetric entries +(j-1,j) and (j,j-1) exactly when a_j=a. All other entries are zero. Put + + A_a = (1-e)I + (e/2) S_a. + +Each S_a is real symmetric and has absolute row sum at most 2. For every real +vector x, the inequality 2|x_j x_k| <= x_j^2+x_k^2 gives +|x^T S_a x| <= 2||x||_2^2. The spectral interval for A_a is therefore +[1-2e,1]. The same statement applies on complex payload space. + +In a product of k <= D such matrices, a path from vertex 0 to vertex D must +make D steps. Each factor can stay at its vertex or move one edge. If k, so the +complete matrix polynomial is zero. Evaluation in End_K(V) preserves sums, +ordered products and scalar coefficients, proving universal substitution. +No independence or minimality of B is needed for soundness. + +Conversely, if the polynomial is zero, the reachable row space +span{U_o T_w} is finite-dimensional, stable under every T_a, and annihilated by +V. Choose a reachable basis. Its initial and closure coordinates give exactly +the displayed certificate. This proves completeness for the declared grammar. + +`linear_words.py` computes that basis by incremental exact elimination. +`check_certificate.py` imports no producer code and does no elimination or +search: it separately reconstructs the dependency representation, rebuilds +the path rows, and checks all three equations. Both share `fields.py`, which +is explicitly part of the trusted arithmetic surface. Neither is a proof +assistant kernel. Source transcription, Python and the arithmetic/compiler +implementations remain trusted; bounded differential tests address faults. + +There are at most D accepted basis rows and |alphabet|D successor tests. +A dense implementation needs O(|alphabet|D^3 + L D) field operations for a +length-L pair of programs, plus parsing the target. Coordinate storage has at +most O(|alphabet|D^2+rD) field elements. These are arithmetic bounds; exact +scalar sizes and dense/sparse constants affect runtime. The reference checker +may recompute path rows and is polynomial, rather than performance optimized. + +## 3. Shortest distinguishing words and literal counterexamples + +Initialize a FIFO queue with independent rows of U. For each queued row U_o T_w, +test its output projection, and enqueue independent successor rows U_o T_w T_a. +All path rows of length at most k are spanned by accepted path rows of length +at most k. This follows by induction, including every rejected dependent row: +its expression uses earlier rows with no greater length, whose successors +span its successors. FIFO order therefore finds a word of least length among +all nonzero coefficients. Dimension increases at most D times. In the acyclic +representation, a word longer than either program's unary dependency depth is +already zero. The checker validates nonzeroness, **not a minimality certificate**; +shortestness is a property of the proved search algorithm. + +Suppose coefficient c != 0 occurs in output o, input i, word w=a1...ak. +On a space with basis e_0,...,e_k set + + N_a = sum_{j: a_(j+1)=a} E_(j,j+1). + +Every factor advances exactly one coordinate. Thus a word u has matrix entry +(0,k) equal to one exactly when u=w, and zero otherwise. Longer words vanish; +shorter words cannot reach coordinate k. Consequently the actual endpoint +discrepancy on input role i with payload e_k has output-role-o coordinate e_0 +equal to c. All other roles can be zero in this concrete witness; they were +independent during the universal check. If k=0, use one-dimensional zero +operators and the empty-word coefficient. Matrices for symbols absent from +w are zero too. This proves finite-dimensional separation constructively. + +For invertible generators run the algorithm on Q(Y)=P(I+Y). Substitution +X->I+Y is a free-algebra automorphism, with inverse Y->X-I, over every field. +It preserves nonzeroness and does not increase degree. Apply the preceding +construction to Q, and evaluate the original circuit at X_a=I+N_a. These +matrices are unipotent with finite inverse I-N_a+N_a^2-...; they share one +triangular flag. This proves the invertible version without assuming that a +separately named inverse symbol denotes this inverse. + +The degree+1 bound is sharp for this **unipotent witness class**: P(X)=(I-X)^d +vanishes on every unipotent operator of dimension at most d, whereas the +(d+1)-dimensional Jordan witness is nonzero. This is not a claim that d+1 is +the least dimension of an arbitrary invertible counterexample. + +## 4. Tensor substitution and dirty boundaries + +If a positive certificate is accepted, substitute X_a=G_a^(tensor f) for any +chosen endomorphisms G_a and any positive integer f. Polynomial evaluation +gives the endpoint identity on the enlarged payload space. Scalar c remains +c times its identity. For example X-I becomes G^(tensor f)-I; it does not +become (G-I)^(tensor f), and cX does not become (cG)^(tensor f). +The *evaluated unary word* tensors multiplicatively; the whole linear sum +must still be evaluated term by term. The certificate never tensorizes a sum. + +Complete role coverage means a borrowed field must return its arbitrary +input functional. A target with `identity:true` supplies that requirement +automatically for every unspecified block. Losing dirt is a nonzero endpoint +residual even when the intended visible target increment is correct. +External source/target aliasing changes the independent-role contract and +requires a new problem transcription. Reusing a role inside the word is legal. + +A negative result disproves universality for **independent** operators. It +does not disprove an identity under commutation, inverse, involution, +Clifford, fixed-dimension, reachable-state or nonlinear leaf constraints. +Such constraints are not silently added. Physical native implementation, +precision, rounded restoration, hosting, stock, compiler uniformity and the +complete paid/outer invoice all remain separate obligations. + +## 5. Bound application + +The adapter imports the exact pinned `echo.py` from the credited multiway dirty +echo package and translates its emitted `(src,dst,factor,sign)` instructions +literally into queries. Its reference is identity on all roles plus +`target += sign A_(n-1)...A_0 source`. Source and every borrowed input are +retained. Each accepted finite schedule now has an inspectable universal +coefficient certificate, extending beyond its earlier fixed matrix controls. +The echo theorem and scheduler are predecessor work, not newly discovered. +The tested schedule range is in README.md; no finite range substitutes for +that predecessor's arbitrary-n written induction or rounded-leaf argument. + +Prepared for zxv with substantial OpenAI Codex assistance. Apache-2.0. diff --git a/research/spd-dirty-circuit-witness/vendor/UPSTREAM-README.md b/research/spd-dirty-circuit-witness/vendor/UPSTREAM-README.md new file mode 100644 index 0000000000..be4e5981e5 --- /dev/null +++ b/research/spd-dirty-circuit-witness/vendor/UPSTREAM-README.md @@ -0,0 +1,133 @@ +# Compact universal certificates for dirty linear circuits + +**A reusable algebraic bridge and exact checker; no new κ.** A linear register +program with r arbitrary inputs and q noncommuting unary calls compiles into +r+q coefficient states. Exact subspace closure certifies its complete endpoint +for **every operator substitution and payload dimension**, without expanding +its noncommutative words. Failure returns a distinguishing word, its dirty +input/output roles, and explicit finite matrix counterexamples. An optional +change of variables makes every counterexample generator invertible. + +This addresses the gap between small matrix experiments and universal recursive +substitution. The weighted-automata and noncommutative PIT algorithms are +classical and credited in [PROOF.md](PROOF.md). The contribution is the compact +register compiler, complete-boundary certificate contract, separate checker, +constructive diagnostics and source-bound application. No new general PIT +algorithm or first universal algebra check in this project is claimed. + +## Result and use + +The [bridge theorem](PROOF.md) gives a polynomial exact-field procedure and a +finite certificate of initial-span coverage, operator closure and zero final +projections. The checker performs no search or Gaussian elimination and imports +no producer code. A shortest nonzero coefficient word of length k produces an +explicit (k+1)-dimensional counterexample. With `--invertible`, all generators +are simultaneously triangular unipotent matrices. The checker validates the +discrepancy; shortestness follows from the search proof. + +The [one-page guide](../../docs/research/universal-dirty-circuit-guide.md) gives +the grammar and acceptance boundary. The tools use only the standard library: + +```sh +python3 -I -B research/universal-dirty-certificates/linear_words.py \ + research/universal-dirty-certificates/examples/dirty-echo3.json \ + --output /tmp/my-new-dirty-certificate.json +python3 -I -B research/universal-dirty-certificates/check_certificate.py \ + research/universal-dirty-certificates/examples/dirty-echo3.json \ + /tmp/my-new-dirty-certificate.json +``` + +Output paths must be new. Add `--matrices` to the checker to print sparse +concrete matrices for a negative certificate. API users can call +`linear_words.decide(problem, shifted=False)` and +`check_certificate.check(problem, certificate)`. + +The committed wrong-order fixture is rejected using `A0=I+E01`, `A1=I+E12`, +`A2=I` in dimension three. Source payload e2 and zero other inputs produce +target discrepancy −1 in coordinate zero. Every generator is invertible. +Scalar substitutions miss the analogous commutator failure. + +## Source-bound evidence + +The adapter translates the actual emitted instructions of the authenticated +`research/cyclic-dirty-commutator-audit/echo.py`. The reference is identity on +every role plus `y += sign A_(n-1)...A_0 x`. The echo construction, schedule and +arbitrary-n/rounded proofs are predecessor work. New certificates cover the +tested emitted schedules for arbitrary substituted linear maps; the rounded +backend and its cost theorem are not replayed. + +- 210 complete source-echo identities: 1,2,3,5,8,12,16 factors; fanouts 2,3,8; + both signs; Q, Q(i), F2, F3, F5. At most 284 states and 38 invariant rows. +- 120 differential circuits against separately implemented explicit-word + expansion, including self reads, rational coefficients, swaps and zero maps. + Each planted discrepancy has a literal full-column matrix replay. +- Cleanup, source, coefficient and order mutations; malformed certificates; + finite-field controls; scalar commutator blindness; the tensor-of-sum trap; + and the sharp unipotent-degree witness family. +- **2^64 distinct endpoint words** in one stress circuit: 130 states and 65 + certificate rows. Initial production/check took about 1.3 seconds on the + Python 3.14 host. This measurement does not predict arbitrary supplier replay. + +Committed examples contain problems and inspectable certificates. Default +verification is read-only and checks exact certificate reproduction. Environment +and measured replays appear in [VALIDATION.json](VALIDATION.json). + +```sh +python3 -B scripts/research_package.py --package research/universal-dirty-certificates --check-only +python3 -B scripts/research_package.py --package research/universal-dirty-certificates +``` + +Direct verification also supports `-I -O -B`. Generic CI targets Python 3.12; +local interpreter versions are recorded separately. No historical heavy suite, +native supplier replay or Lean build is required. + +## Limits and trust + +Supported fields are Q, Q(i), and F_p, prime p<=2^31-1; fractions need invertible +denominators. Every input/returned role is retained. Equal payload dimensions +and **independent** operator symbols are required. A negative verdict need not +survive additional inverse, commutation, Clifford or reachable-state constraints. +The existing relation-aware free-group tensor audit remains appropriate there. + +The proof is written mathematics with exact executable certificates, not a +proof-assistant formalization or independent human review. The checker has a +separately transcribed compiler and shares `fields.py` with the producer. These, +Python and source transcription are trusted; differential expansion and literal +matrix execution are additional checks, not independent reviewers. + +Universal acceptance permits termwise tensor substitution with scalar +coefficients fixed. It does not tensorize a sum. Affine constants, rectangular +types, nonlinear leaves, physical aliasing, native implementation, precision, +rounded restoration, stock, hosting, tapes and the complete paid/outer invoice +remain separate. No supplier admission or selected-frontier change is claimed. + +## Open next questions + +- Bind another contributor's independent-symbol program with a literal source + adapter and complete endpoint. Compare its certificate against an existing + symbolic replay. Types and generator relations must match first. +- Add a relation-aware frontend for one named inverse/commutation model, starting + with a sound normalization theorem and boundary controls. Independent symbols + are only a conservative test of a relation-constrained implementation. +- Profile rational coefficient growth and repeated path traversal on a larger + real adapter, preserving exactly the same closure equations. The arithmetic + bound does not guarantee scalable replay of every 632-role supplier. + +## Credit and coordination + +Prepared for **zxv** with substantial **OpenAI Codex assistance**; Apache-2.0. +Classical weighted-automata/PIT credit belongs to the cited authors. The echo +package is prepared for **androolloyd**, following **Chafik Boukhalfa / chafreaky +PR628**, **Ali Romman PR621** and the retained inverse/precision lineage. +**Cinna Davis PR4100/4088**, **ToikY's free-word tensor-lift audit**, **Sagar +Thakrar PR3687**, **roger-sato PR3693**, and the universal dirty-phase audit +following **Charles Bethin PR1278** retain their prior results and credit. +Ross Richardson's cut58 and the two-register short-mixing work retain their +distinct tensor-separation arguments. Only the small echo scheduler is imported. + +[SOURCES.json](SOURCES.json) pins the base, catalogue, selected record, live +scheduler and relevant provenance. [TASK.json](TASK.json) records the explicit +scope change and bounded obligations. The canonical +[claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19145795) +records overlap and publication status. Cache misses do not establish novelty; +unpublished work and arbitrary historical diffs remain outside the checked scope. diff --git a/research/spd-dirty-circuit-witness/vendor/fields.py b/research/spd-dirty-circuit-witness/vendor/fields.py new file mode 100644 index 0000000000..f1b6dc83e2 --- /dev/null +++ b/research/spd-dirty-circuit-witness/vendor/fields.py @@ -0,0 +1,140 @@ +"""Small exact scalar layer shared by producer and checker (part of their trust base). + +Prepared for zxv with substantial OpenAI Codex assistance. Apache-2.0. +""" +from fractions import Fraction +from math import isqrt +from functools import lru_cache +import re + + +class Gaussian: + """Q(i); input strings use a+bi with rational a,b, or just i/-i.""" + def __init__(self, value=0): + if isinstance(value, Gaussian): + self.real, self.imag = value.real, value.imag + elif type(value) is str and value.endswith("i"): + body = value[:-1] + rational = r"\d+(?:/\d+)?" + match = re.fullmatch(r"([+-]?"+rational+r")([+-](?:"+rational+r")?)", body) + if match: + self.real = Fraction(match[1]) + self.imag = Fraction(match[2]+"1" if match[2] in ("+", "-") else match[2]) + else: + if body in ("", "+", "-"): + body += "1" + self.real, self.imag = Fraction(0), Fraction(body) + else: + self.real, self.imag = Fraction(value), Fraction(0) + + @classmethod + def pair(cls, real, imag): + out = cls() + out.real, out.imag = real, imag + return out + + def __add__(self, other): + z = Gaussian(other) + return self.pair(self.real+z.real, self.imag+z.imag) + + __radd__ = __add__ + + def __mul__(self, other): + z = Gaussian(other) + return self.pair(self.real*z.real-self.imag*z.imag, self.real*z.imag+self.imag*z.real) + + __rmul__ = __mul__ + + def __neg__(self): + return self.pair(-self.real, -self.imag) + + def __sub__(self, other): + return self+-Gaussian(other) + + def __rsub__(self, other): + return Gaussian(other)+-self + + def __truediv__(self, other): + z = Gaussian(other) + norm = z.real*z.real+z.imag*z.imag + return self*self.pair(z.real/norm, -z.imag/norm) + + def __rtruediv__(self, other): + return Gaussian(other)/self + + def __eq__(self, other): + z = Gaussian(other) + return self.real == z.real and self.imag == z.imag + + def __bool__(self): + return bool(self.real or self.imag) + + def __str__(self): + if not self.imag: + return str(self.real) + return str(self.real)+("+" if self.imag >= 0 else "")+str(self.imag)+"i" + + __repr__ = __str__ + + +def scalars(problem): + p = problem.get("field", "Q") + if p == "Q": + return Fraction + if p == "Qi": + return Gaussian + if type(p) is not int: + raise ValueError("field must be Q, Qi or a prime at most 2^31-1") + return prime_scalars(p) + + +@lru_cache(maxsize=32) +def prime_scalars(p): + if not 2 <= p <= 2**31-1 or any(p % d == 0 for d in range(2, isqrt(p)+1)): + raise ValueError("field must be Q, Qi or a prime at most 2^31-1") + + class Prime: + def __init__(self, x=0): + if isinstance(x, Prime): + self.value = x.value + else: + q = Fraction(x) + self.value = q.numerator*pow(q.denominator, -1, p) % p + + def __add__(self, other): + return Prime(self.value+Prime(other).value) + + __radd__ = __add__ + + def __mul__(self, other): + return Prime(self.value*Prime(other).value) + + __rmul__ = __mul__ + + def __neg__(self): + return Prime(-self.value) + + def __sub__(self, other): + return self+-Prime(other) + + def __rsub__(self, other): + return Prime(other)+-self + + def __truediv__(self, other): + return Prime(self.value*pow(Prime(other).value, -1, p)) + + def __rtruediv__(self, other): + return Prime(other)/self + + def __eq__(self, other): + return self.value == Prime(other).value + + def __bool__(self): + return bool(self.value) + + def __str__(self): + return str(self.value) + + __repr__ = __str__ + + return Prime diff --git a/research/spd-dirty-circuit-witness/vendor/linear_words.py b/research/spd-dirty-circuit-witness/vendor/linear_words.py new file mode 100644 index 0000000000..4a877e1ab9 --- /dev/null +++ b/research/spd-dirty-circuit-witness/vendor/linear_words.py @@ -0,0 +1,250 @@ +"""Exact free-algebra certificates for complete dirty linear programs. + +Prepared for zxv with substantial OpenAI Codex assistance. Apache-2.0. +Reachable-space equivalence is classical; see PROOF.md for attribution. +""" +from collections import deque +from fractions import Fraction as Q +import argparse +import hashlib +import json +from pathlib import Path +import sys +sys.path.insert(0, str(Path(__file__).resolve().parent)) +from fields import scalars + + +def need(test, message): + if not test: + raise ValueError(message) + + +def number(value, scalar=Q): + need(type(value) in (int, str), "coefficient must be an integer or exact scalar string") + return scalar(value) + + +def index(value, n): + need(type(value) is int and 0 <= value < n, "role index out of range") + return value + + +def add(a, b, scale=Q(1)): + out = a.copy() + for j, x in b.items(): + out[j] = out.get(j, Q(0)) + scale*x + if not out[j]: + del out[j] + return out + + +def scaled(a, c): + return {j: c*x for j, x in a.items() if c*x} + + +def digest(problem): + return hashlib.sha256(json.dumps(problem, sort_keys=True, separators=(",", ":")).encode()).hexdigest() + + +class Machine: + def __init__(self, roles, scalar=Q): + self.roles = roles + self.scalar = scalar + self.states = roles + self.edges = {} + self.final = {i: i for i in range(roles)} + self.initial = [{i: scalar(1)} for i in range(roles)] + + def atom(self, symbol, row): + need(type(symbol) is str and bool(symbol), "nonempty operator symbol required") + j = self.states + self.states += 1 + self.edges.setdefault(symbol, {})[j] = row.copy() + return {j: self.scalar(1)} + + def step(self, row, symbol): + out = {} + edges = self.edges.get(symbol, {}) + for i, c in row.items(): + out = add(out, edges.get(i, {}), c) + return out + + def terminal(self, row): + out = {} + for i, c in row.items(): + if i in self.final: + j = self.final[i] + out[j] = out.get(j, Q(0)) + c + if not out[j]: + del out[j] + return out + + +def program_machine(roles, instructions, shifted=False, scalar=Q): + need(type(instructions) is list, "program must be a list") + m = Machine(roles, scalar) + rows = m.initial + for op in instructions: + need(type(op) is dict and type(op.get("op")) is str, "instruction object required") + kind = op["op"] + allowed = { + "add": {"op", "src", "dst", "coefficient"}, + "query": {"op", "src", "dst", "symbol", "coefficient"}, + "apply": {"op", "dst", "symbol"}, + "scale": {"op", "dst", "coefficient"}, + "swap": {"op", "src", "dst"}, + } + need(kind in allowed and not (op.keys()-allowed[kind]), "unknown instruction or key") + dst = index(op.get("dst"), roles) + if kind in ("add", "query", "swap"): + src = index(op.get("src"), roles) + if kind == "swap": + rows[src], rows[dst] = rows[dst], rows[src] + elif kind == "scale": + rows[dst] = scaled(rows[dst], number(op["coefficient"], scalar)) + elif kind == "add": + rows[dst] = add(rows[dst], rows[src], number(op.get("coefficient", 1), scalar)) + else: + old = rows[dst if kind == "apply" else src].copy() + atom = m.atom(op.get("symbol"), old) + image = add(old, atom) if shifted else atom + if kind == "apply": + rows[dst] = image + else: + rows[dst] = add(rows[dst], image, number(op.get("coefficient", 1), scalar)) + return m + + +def target_machine(roles, target, shifted=False, scalar=Q): + need(type(target) is dict and not (target.keys()-{"identity", "terms"}), "invalid target") + need(type(target.get("identity", True)) is bool, "identity must be Boolean") + need(type(target.get("terms", [])) is list, "terms must be a list") + m = Machine(roles, scalar) + out = [{i: scalar(1)} if target.get("identity", True) else {} for i in range(roles)] + for term in target.get("terms", []): + need(type(term) is dict and not (term.keys()-{"out", "in", "word", "coefficient"}), "invalid target term") + i, j = index(term.get("out"), roles), index(term.get("in"), roles) + word = term.get("word") + need(type(word) is list, "word must be an ordered symbol list") + row = {j: scalar(1)} + for a in reversed(word): + atom = m.atom(a, row) + row = add(row, atom) if shifted else atom + out[i] = add(out[i], row, number(term.get("coefficient", 1), scalar)) + m.initial = out + return m + + +def compile_problem(problem, shifted=False): + need(type(problem) is dict and not (problem.keys()-{"field", "roles", "program", "reference", "target"}), "invalid problem keys") + scalar = scalars(problem) + n = problem.get("roles") + need(type(n) is int and n > 0, "positive role count required") + need(("reference" in problem) != ("target" in problem), "provide exactly one reference or target") + a = program_machine(n, problem["program"], shifted, scalar) + b = (program_machine(n, problem["reference"], shifted, scalar) if "reference" in problem + else target_machine(n, problem["target"], shifted, scalar)) + m = Machine(n, scalar) + m.states = a.states+b.states + shift = lambda row: {j+a.states: x for j, x in row.items()} + m.initial = [add(x, shift(y), Q(-1)) for x, y in zip(a.initial, b.initial)] + m.final = dict(a.final) + m.final.update({j+a.states: v for j, v in b.final.items()}) + m.edges = {s: dict(rows) for s, rows in a.edges.items()} + for s, rows in b.edges.items(): + m.edges.setdefault(s, {}).update({j+a.states: shift(v) for j, v in rows.items()}) + return m + + +class Span: + """Incremental elimination with coordinates in the original reachable rows.""" + def __init__(self): + self.rows = [] + self.echelon = [] + + def reduce(self, row): + row = row.copy() + coords = {} + for pivot, basis, rep in self.echelon: + c = row.get(pivot, Q(0)) + if c: + row = add(row, basis, -c) + coords = add(coords, rep, c) + return row, coords + + def insert(self, row): + rest, coords = self.reduce(row) + if not rest: + return False + j = len(self.rows) + self.rows.append(row) + pivot = min(rest) + c = 1/rest[pivot] + rep = scaled(add({j: Q(1)}, coords, Q(-1)), c) + self.echelon.append((pivot, scaled(rest, c), rep)) + self.echelon.sort(key=lambda item: item[0]) + return True + + def coordinates(self, row): + rest, coords = self.reduce(row) + need(not rest, "internal invariant space is not closed") + return coords + + +def packed(row): + return {str(j): str(x) for j, x in sorted(row.items())} + + +def decide(problem, shifted=False): + m = compile_problem(problem, shifted) + alphabet = sorted(m.edges) + span, paths, queue = Span(), [], deque() + + def consider(row, output, word): + terminal = m.terminal(row) + if terminal: + j = min(terminal) + return {"schema": "dirty-linear-certificate/v1", "problem_sha256": digest(problem), + "equivalent": False, "shifted": shifted, "states": m.states, + "output": output, "input": j, "word": word, + "coefficient": str(terminal[j]), "matrix_dimension": len(word)+1} + if span.insert(row): + paths.append({"output": output, "word": word}) + queue.append(len(paths)-1) + return None + + for i, row in enumerate(m.initial): + bad = consider(row, i, []) + if bad: + return bad + while queue: + k = queue.popleft() + for a in alphabet: + p = paths[k] + bad = consider(m.step(span.rows[k], a), p["output"], p["word"]+[a]) + if bad: + return bad + return {"schema": "dirty-linear-certificate/v1", "problem_sha256": digest(problem), + "equivalent": True, "shifted": shifted, "states": m.states, + "paths": paths, "initial": [packed(span.coordinates(row)) for row in m.initial], + "closure": {a: [packed(span.coordinates(m.step(row, a))) for row in span.rows] + for a in alphabet}} + + +def main(): + ap = argparse.ArgumentParser(description=__doc__) + ap.add_argument("problem", type=Path) + ap.add_argument("--invertible", action="store_true", help="use X=I+Y to construct unipotent witnesses") + ap.add_argument("--output", type=Path, help="new certificate path; never overwritten") + args = ap.parse_args() + cert = decide(json.loads(args.problem.read_text()), args.invertible) + data = json.dumps(cert, indent=2, sort_keys=True)+"\n" + if args.output: + with args.output.open("x") as stream: + stream.write(data) + else: + print(data, end="") + + +if __name__ == "__main__": + main() diff --git a/research/spd-dirty-circuit-witness/verify.py b/research/spd-dirty-circuit-witness/verify.py new file mode 100644 index 0000000000..c302070078 --- /dev/null +++ b/research/spd-dirty-circuit-witness/verify.py @@ -0,0 +1,188 @@ +"""Exact differential and literal checks for the bounded-condition witness. + +Ali Romman, with substantial OpenAI Codex assistance. Apache-2.0. +""" +import argparse +from copy import deepcopy +from fractions import Fraction as Q +import hashlib +import json +from pathlib import Path +import random +import sys + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +from witness import produce +from literal import check, endpoint, action, require +from fields import scalars + + +def expanded(problem): + scalar = scalars(problem) + initial = [{(j, ()): scalar(1)} for j in range(problem['roles'])] + + def combine(a, b, c): + out = a.copy() + for key, x in b.items(): + out[key] = out.get(key, scalar(0))+c*x + return {key: x for key, x in out.items() if x} + + def run(ops): + rows = [row.copy() for row in initial] + for op in ops: + d, kind = op['dst'], op['op'] + if kind == 'swap': + s = op['src']; rows[d], rows[s] = rows[s], rows[d] + elif kind == 'scale': + rows[d] = combine({}, rows[d], scalar(op['coefficient'])) + else: + value = rows[d if kind == 'apply' else op['src']].copy() + if kind in ('apply', 'query'): + value = {(j, (op['symbol'],)+word): x for (j, word), x in value.items()} + rows[d] = value if kind == 'apply' else combine(rows[d], value, scalar(op.get('coefficient', 1))) + return rows + + left = run(problem['program']) + if 'reference' in problem: + right = run(problem['reference']) + else: + t = problem['target'] + right = [row.copy() if t.get('identity', True) else {} for row in initial] + for term in t.get('terms', []): + d = term['out'] + right[d] = combine(right[d], {(term['in'], tuple(term['word'])): scalar(term.get('coefficient', 1))}, scalar(1)) + return [combine(a, b, scalar(-1)) for a, b in zip(left, right)] + + +def reject(fn): + try: + fn() + except (ValueError, KeyError, TypeError): + return + raise ValueError('control accepted') + + +def fixtures(): + rng = random.Random(5260) + count = negative = positive = 0 + for field in ('Q', 'Qi'): + for size in range(1, 5): + for trial in range(30): + ops = [] + for _ in range(12): + kind = rng.choice(('add', 'query', 'scale', 'swap', 'apply')) + op = {'op': kind, 'dst': rng.randrange(size)} + if kind in ('add', 'query', 'swap'): op['src'] = rng.randrange(size) + if kind in ('query', 'apply'): op['symbol'] = rng.choice(('X', 'Y', 'Z')) + if kind in ('add', 'query', 'scale'): + op['coefficient'] = rng.choice(('0', '1', '-1', '2/3', '1+i') if field == 'Qi' else ('0', '1', '-1', '2/3')) + ops.append(op) + problem = {'roles': size, 'field': field, 'program': ops, + 'reference': ops if trial % 5 == 0 else []} + polynomial = expanded(problem) + degrees = [len(word) for row in polynomial for _, word in row] + cert = produce(problem) + require(cert['equivalent'] == (not degrees), 'equivalence differs from expansion') + if degrees: + require(len(cert['word']) == max(degrees), 'wrong top degree') + actual = polynomial[cert['output']][(cert['input'], tuple(cert['word']))] + require(str(actual) == cert['coefficient'], 'wrong top coefficient') + for epsilon in (Q(1, 4), Q(1, 64)): + check(problem, produce(problem, epsilon)) + negative += 1 + else: + positive += 1 + count += 1 + return {'differential_circuits': count, 'negative_circuits': negative, + 'equivalent_circuits': positive, 'literal_replays': 2*negative} + + +def controls(): + # A shortest constant witness fails at X=3I/4, but the degree-one path succeeds. + p = {'roles': 1, 'program': [{'op': 'apply', 'dst': 0, 'symbol': 'X'}], + 'target': {'identity': False, 'terms': [{'out': 0, 'in': 0, 'word': [], 'coefficient': '3/4'}]}} + c = produce(p) + require(c['word'] == ['X'] and check(p, c) == '1/8', 'highest-degree control') + require(endpoint(p, [[Q(1)]], [], Q(1, 4)) == [[Q(0)]], 'constant witness must fail') + for key, value in [('word', []), ('coefficient', '-1'), ('input', 1), ('output', 1), + ('epsilon', '0'), ('epsilon', '1/2'), ('dimension', 1), + ('spectral_interval', ['0', '1']), ('problem_sha256', '0'*64), + ('equivalent', True)]: + mutant = deepcopy(c); mutant[key] = value + reject(lambda: check(p, mutant)) + reject(lambda: produce(dict(p, field=2))) + reject(lambda: produce(p, 0)) + # A returned dirty helper can fail while the requested data role is unchanged. + dirty = {'roles': 2, 'program': [{'op': 'query', 'src': 1, 'dst': 1, 'symbol': 'X'}], 'reference': []} + d = produce(dirty); require((d['output'], d['input']) == (1, 1), 'dirty role omitted'); check(dirty, d) + # A commutator must not vanish under the symmetric path substitution. + comm = {'roles': 1, 'program': [], 'target': {'terms': [ + {'out': 0, 'in': 0, 'word': ['X', 'Y']}, + {'out': 0, 'in': 0, 'word': ['Y', 'X'], 'coefficient': -1}]}} + check(comm, produce(comm)) + return 15 + + +def stress(): + ops = [] + for _ in range(64): + ops.extend([{'op': 'scale', 'dst': 1, 'coefficient': 0}, + {'op': 'query', 'src': 0, 'dst': 1, 'symbol': 'X'}, + {'op': 'query', 'src': 0, 'dst': 1, 'symbol': 'Y'}, + {'op': 'swap', 'src': 0, 'dst': 1}]) + p = {'roles': 2, 'program': ops, 'target': {'identity': False}} + cert = produce(p) + require(len(cert['word']) == 64, 'stress degree') + difference = check(p, cert) + require(Q(difference) == Q(1, 8)**64, 'stress endpoint') + return {'expanded_top_words': 2**64, 'degree': 64, 'dimension': cert['dimension'], + 'states': cert['statistics']['states'], + 'maximum_layer_dimension': max(cert['statistics']['layer_dimensions']), + 'sum_layer_dimensions': sum(cert['statistics']['layer_dimensions']), + 'discrepancy': difference} + + +def spectral_checks(): + cases = 0 + for length in range(16): + word = ['X' if j % 3 else 'Y' for j in range(length)] + for epsilon in (Q(1, 4), Q(1, 64)): + for symbol in ('X', 'Y', 'Z'): + n = length+1 + columns = [action([Q(int(i == j)) for i in range(n)], symbol, word, epsilon) for j in range(n)] + require(all(columns[j][i] == columns[i][j] for i in range(n) for j in range(n)), 'not symmetric') + for i in range(n): + radius = sum(abs(columns[j][i]) for j in range(n) if j != i) + require(columns[i][i]-radius >= 1-2*epsilon and columns[i][i]+radius <= 1, 'spectral enclosure') + cases += 1 + return cases + + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument('--write', action='store_true') + ap.add_argument('--small', action='store_true') + args = ap.parse_args() + report = {'fixtures': fixtures(), 'controls': controls(), 'spectral_matrices': spectral_checks()} + if args.small: + print(json.dumps(report, sort_keys=True)); return + report['stress'] = stress() + example = json.loads((HERE/'wrong-order.json').read_text()) + cert = produce(example) + report['source_example'] = {'certificate': cert, 'discrepancy': check(example, cert)} + sources = json.loads((HERE/'SOURCES.json').read_text()) + for f in ('fields.py', 'linear_words.py', 'wrong-order.json'): + row = next(r for r in sources['files'] if r['path'].endswith('/'+f)) + require(hashlib.sha256(((HERE/'vendor'/f) if f.endswith('.py') else (HERE/f)).read_bytes()).hexdigest() == row['sha256'], 'vendor drift') + names = sorted(p for p in HERE.rglob('*') if p.is_file() and '__pycache__' not in p.parts and p.name != 'RESULT.json') + report['files'] = {p.relative_to(HERE).as_posix(): hashlib.sha256(p.read_bytes()).hexdigest() for p in names} + if args.write: + (HERE/'RESULT.json').write_text(json.dumps(report, indent=2, sort_keys=True)+'\n') + else: + require(report == json.loads((HERE/'RESULT.json').read_text()), 'receipt drift') + print('PASS_SPD_DIRTY_WITNESS ' + json.dumps({k: v for k, v in report.items() if k != 'files'}, sort_keys=True)) + + +if __name__ == '__main__': + main() diff --git a/research/spd-dirty-circuit-witness/witness.py b/research/spd-dirty-circuit-witness/witness.py new file mode 100644 index 0000000000..fbe2d22f2d --- /dev/null +++ b/research/spd-dirty-circuit-witness/witness.py @@ -0,0 +1,69 @@ +"""Construct well-conditioned counterexamples for dirty linear programs. + +Ali Romman, with substantial OpenAI Codex assistance. Apache-2.0. +The unchanged compiler in vendor is prepared for zxv; see NOTICE.md. +""" +import argparse +from fractions import Fraction as Q +import json +from pathlib import Path +import sys + +sys.path.insert(0, str(Path(__file__).resolve().parent / 'vendor')) +from linear_words import Span, compile_problem, digest, need + + +def top_coefficient(problem): + """Keep a separate reachable space for each exact word length.""" + need(problem.get('field', 'Q') in ('Q', 'Qi'), 'ordered witness requires Q or Qi') + machine = compile_problem(problem) + alphabet = sorted(machine.edges) + candidates = [(row, output, []) for output, row in enumerate(machine.initial)] + last = None + widths = [] + for degree in range(machine.states): + span = Span() + paths = [] + for row, output, word in candidates: + if span.insert(row): + paths.append((output, word)) + terminal = machine.terminal(row) + if terminal: + source = min(terminal) + last = {'output': output, 'input': source, 'word': word, + 'coefficient': str(terminal[source])} + widths.append(len(paths)) + if not paths: + break + candidates = [(machine.step(row, symbol), output, word + [symbol]) + for row, (output, word) in zip(span.rows, paths) + for symbol in alphabet] + need(all(not row for row, _, _ in candidates) or widths[-1] == 0, + 'coefficient machine is not acyclic') + return last, {'states': machine.states, 'layer_dimensions': widths, + 'alphabet': alphabet} + + +def produce(problem, epsilon=Q(1, 4)): + epsilon = Q(epsilon) + need(0 < epsilon <= Q(1, 4), 'epsilon must be in (0,1/4]') + top, stats = top_coefficient(problem) + result = {'schema': 'spd-dirty-witness/v1', 'problem_sha256': digest(problem), + 'equivalent': top is None, 'statistics': stats} + if top is not None: + result.update(top) + result.update({'epsilon': str(epsilon), 'dimension': len(top['word']) + 1, + 'spectral_interval': [str(1-2*epsilon), '1']}) + return result + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('problem', type=Path) + parser.add_argument('--epsilon', default='1/4') + args = parser.parse_args() + print(json.dumps(produce(json.loads(args.problem.read_text()), Q(args.epsilon)), indent=2)) + + +if __name__ == '__main__': + main() diff --git a/research/spd-dirty-circuit-witness/wrong-order.json b/research/spd-dirty-circuit-witness/wrong-order.json new file mode 100644 index 0000000000..85482942f0 --- /dev/null +++ b/research/spd-dirty-circuit-witness/wrong-order.json @@ -0,0 +1,76 @@ +{ + "roles": 4, + "program": [ + { + "op": "query", + "src": 0, + "dst": 2, + "symbol": "A0", + "coefficient": 1 + }, + { + "op": "query", + "src": 2, + "dst": 3, + "symbol": "A1", + "coefficient": 1 + }, + { + "op": "query", + "src": 3, + "dst": 1, + "symbol": "A2", + "coefficient": 1 + }, + { + "op": "query", + "src": 2, + "dst": 3, + "symbol": "A1", + "coefficient": -1 + }, + { + "op": "query", + "src": 0, + "dst": 2, + "symbol": "A0", + "coefficient": -1 + }, + { + "op": "query", + "src": 2, + "dst": 3, + "symbol": "A1", + "coefficient": 1 + }, + { + "op": "query", + "src": 3, + "dst": 1, + "symbol": "A2", + "coefficient": -1 + }, + { + "op": "query", + "src": 2, + "dst": 3, + "symbol": "A1", + "coefficient": -1 + } + ], + "target": { + "identity": true, + "terms": [ + { + "out": 1, + "in": 0, + "word": [ + "A0", + "A1", + "A2" + ], + "coefficient": 1 + } + ] + } +}