From 3418cd0cc739ce1d4ce3160e3313b325d66ae937 Mon Sep 17 00:00:00 2001 From: zxv Date: Fri, 23 Oct 2026 09:05:22 -0400 Subject: [PATCH 1/2] Add compact universal certificates for dirty linear circuits --- docs/research/agent-procedure.md | 6 + .../research/universal-dirty-circuit-guide.md | 82 ++++ .../universal-dirty-certificates/PROOF.md | 191 +++++++++ .../universal-dirty-certificates/README.md | 133 +++++++ .../universal-dirty-certificates/SOURCES.json | 55 +++ .../universal-dirty-certificates/TASK.json | 107 +++++ .../VALIDATION.json | 95 +++++ .../universal-dirty-certificates/VERIFY.json | 36 ++ .../check_certificate.py | 198 +++++++++ .../examples/binary-echo3.certificate.json | 84 ++++ .../examples/binary-echo3.json | 77 ++++ .../examples/dirty-echo3.certificate.json | 84 ++++ .../examples/dirty-echo3.json | 76 ++++ .../examples/wrong-order.certificate.json | 15 + .../examples/wrong-order.json | 76 ++++ .../universal-dirty-certificates/fields.py | 140 +++++++ .../linear_words.py | 250 ++++++++++++ .../universal-dirty-certificates/verify.py | 376 ++++++++++++++++++ 18 files changed, 2081 insertions(+) create mode 100644 docs/research/universal-dirty-circuit-guide.md create mode 100644 research/universal-dirty-certificates/PROOF.md create mode 100644 research/universal-dirty-certificates/README.md create mode 100644 research/universal-dirty-certificates/SOURCES.json create mode 100644 research/universal-dirty-certificates/TASK.json create mode 100644 research/universal-dirty-certificates/VALIDATION.json create mode 100644 research/universal-dirty-certificates/VERIFY.json create mode 100644 research/universal-dirty-certificates/check_certificate.py create mode 100644 research/universal-dirty-certificates/examples/binary-echo3.certificate.json create mode 100644 research/universal-dirty-certificates/examples/binary-echo3.json create mode 100644 research/universal-dirty-certificates/examples/dirty-echo3.certificate.json create mode 100644 research/universal-dirty-certificates/examples/dirty-echo3.json create mode 100644 research/universal-dirty-certificates/examples/wrong-order.certificate.json create mode 100644 research/universal-dirty-certificates/examples/wrong-order.json create mode 100644 research/universal-dirty-certificates/fields.py create mode 100644 research/universal-dirty-certificates/linear_words.py create mode 100644 research/universal-dirty-certificates/verify.py diff --git a/docs/research/agent-procedure.md b/docs/research/agent-procedure.md index 27d7029ef3..9294c540bf 100644 --- a/docs/research/agent-procedure.md +++ b/docs/research/agent-procedure.md @@ -374,6 +374,12 @@ pins. Use exact arithmetic or certified bounds for acceptance; finite-field and floating-point searches can propose candidates but cannot certify a rational rank identity or universal theorem on their own. +For scalar linear programs with independent noncommuting unary operators, the +[universal dirty-circuit guide](universal-dirty-circuit-guide.md) offers compact +exact certificates for complete dirty endpoints and termwise tensor substitution. +Its grammar and independent-symbol hypotheses must match the actual caller; +native, inverse/group, nonlinear and physical cost obligations remain separate. + Run checks relevant to your change, with a positive fixture and meaningful failure controls when adding a verifier. State which obligations were **not** checked. Supplier adoption needs the applicable complete cold replay and source diff --git a/docs/research/universal-dirty-circuit-guide.md b/docs/research/universal-dirty-circuit-guide.md new file mode 100644 index 0000000000..0989fd6e51 --- /dev/null +++ b/docs/research/universal-dirty-circuit-guide.md @@ -0,0 +1,82 @@ +# Certify a dirty linear circuit for arbitrary operators + +Use [universal-dirty-certificates](../../research/universal-dirty-certificates/README.md) +for scalar linear register programs with unary operators requiring **no +relations between them**. A compact certificate can prove the complete endpoint +for all payload dimensions without expanding every operator word. + +## Minimal input + +```json +{ + "field": "Q", + "roles": 3, + "program": [ + {"op":"query", "src":0, "dst":1, "symbol":"A"}, + {"op":"query", "src":1, "dst":2, "symbol":"B"}, + {"op":"query", "src":0, "dst":1, "symbol":"A", "coefficient":-1}, + {"op":"query", "src":1, "dst":2, "symbol":"B", "coefficient":-1} + ], + "target": { + "identity": true, + "terms": [{"out":2, "in":0, "word":["B","A"]}] + } +} +``` + +All three initial registers are arbitrary. The target is the complete identity +plus `v2 += B A v0`; register 1 must return its dirty input. Words use matrix +product order: BA applies A first. An empty word means payload identity. +Coefficients default to one and are integers or rational strings, never floats. +`field` defaults to Q; `"Qi"` selects Gaussian rationals (for example +`"1/2-3/4i"` or `"i"`); a prime integer p selects F_p with invertible denominators. + +| Instruction | Meaning | +| --- | --- | +| `add`, `src`, `dst`, optional `coefficient` | `v_dst += c v_src` | +| `query`, `src`, `dst`, `symbol`, optional `coefficient` | `v_dst += c X_symbol v_src` | +| `apply`, `dst`, `symbol` | `v_dst = X_symbol v_dst` | +| `scale`, `dst`, `coefficient` | `v_dst = c v_dst` | +| `swap`, `src`, `dst` | Exchange the registers | + +In place reuse and self queries are supported. Every index denotes one role +with its own initial input. Retain borrowed fields and cleanup outputs. If the +reference also expands exponentially, give `reference` as another instruction +list instead of `target`. Exactly one is required. + +## Produce and check + +```sh +python3 -I -B research/universal-dirty-certificates/linear_words.py \ + /path/to/problem.json --output /tmp/new-certificate.json +python3 -I -B research/universal-dirty-certificates/check_certificate.py \ + /path/to/problem.json /tmp/new-certificate.json +``` + +A positive certificate proves the complete matrix-polynomial identity. The +checker verifies a closed subspace annihilating every final input projection; +it performs no search or elimination. Its compiler, shared field arithmetic and +Python remain trusted. Archive both JSON files with exact source pins and the +instruction adapter. + +A negative certificate identifies a nonzero word and offending input/output. +Use `--invertible` on the producer for unipotent counterexamples. Use `--matrices` +on the checker to print sparse operators, input payload and discrepancy. +These disprove the **independent-operator** identity. Symbols named `G` and +`G_inverse` acquire no inverse relation. + +## Scope of the bridge + +Universal acceptance permits termwise substitution `X_a=G_a^(tensor f)` for every +positive f. Scalars stay outside: `c X-I` becomes `c G^(tensor f)-I`. This does +not tensorize sums or admit physical implementations. See the +[proof and limits](../../research/universal-dirty-certificates/PROOF.md). + +For free-group native programs, use the existing +[free-word tensor audit](../../research/free-word-tensor-lift-audit/README.md). +For rectangular scratch and one-sided invariants, the existing +[dirty-phase audit](../../research/universal-dirty-phase-identities/README.md) +has a different contract. Nonlinear leaves, aliasing, rounding, native frames, +tapes, precision and the complete invoice still need their own arguments. + +Prepared for zxv with substantial OpenAI Codex assistance. Apache-2.0. diff --git a/research/universal-dirty-certificates/PROOF.md b/research/universal-dirty-certificates/PROOF.md new file mode 100644 index 0000000000..3a405e327a --- /dev/null +++ b/research/universal-dirty-certificates/PROOF.md @@ -0,0 +1,191 @@ +# Compact universal certificates for dirty linear circuits + +## Result and provenance + +Let K be a field, let r registers contain arbitrary independent vectors in one +K-vector space V, and let X_a be finitely many **independent unary operator +symbols**. A program uses scalar ADD, SCALE, SWAP, unary APPLY, and queries +`v_d += c X_a v_s`. Source and destination may coincide. Coefficients are +central elements of K. Retain every input and every returned register, +including borrowed dirty registers. There are no implicit zero inputs. + +**Bridge theorem.** A program with q unary occurrences has a coefficient +representation with exactly r+q states, independent of its expanded word count. +For two programs, put D=2r+q_left+q_right. Their complete endpoints are equal +under every K-linear operator substitution, in every dimension, if and only if +their difference has a certificate consisting of at most D reachable rows, +initial-span coordinates, closure coordinates, and zero final projections. +Such a certificate can be found with polynomially many exact field operations. +If the endpoints differ, the search finds a shortest nonzero coefficient word +w. Matrices of dimension |w|+1 with entries zero or one realize that coefficient +as an actual endpoint discrepancy, including the offending dirty input/output. + +The same procedure applied after substituting X_a=I+Y_a supplies a discrepancy +using **simultaneously upper triangular unipotent**, hence invertible, operators. +In either version |w| is at most the maximum unary dependency depth of the two +programs, and at most D-1. For a program compared with an explicit polynomial +target, replace q_right by the sum of its displayed term lengths. + +This is a project-specific compilation and certificate bridge to **classical** +weighted-automata equivalence and noncommutative polynomial identity testing. +No new general PIT algorithm, free-algebra separation theorem, or tensor +independence theorem is claimed. Primary references are Stefan Kiefer, +[Notes on Equivalence and Minimization of Weighted Automata, §§1–2 (2020)](https://arxiv.org/abs/2009.01217), +and Ran Raz and Amir Shpilka, +[Deterministic Polynomial Identity Testing in Non Commutative Models (2005)](https://www.cs.tau.ac.il/~shpilka/publications/RazShpilka_PIT.pdf). +The new artifact specializes these methods to the project's complete dirty +register contract, gives a compact compiler and separately transcribed checker, +and binds them to a real scheduler and constructive failure diagnostics. + +The existing [free-word tensor-lift audit](../free-word-tensor-lift-audit/README.md) +already proves a particular provider's lift with explicit reduced free-group +words. The [universal dirty-phase identities](../universal-dirty-phase-identities/README.md) +already replace numerical tests for their typed local identities. Neither result +is claimed here. This method avoids word expansion for its own independent-symbol, +equal-space linear grammar; it does **not** replace their relation-aware or +rectangular-block arguments. + +## 1. Register compilation without word expansion + +Create r leaf atoms x_0,...,x_(r-1). Maintain each register as a scalar linear +combination of atoms. Scalar instructions update these combinations directly. +For each unary occurrence on expression e, create one fresh atom z_j=X_a e +and record its label a and its scalar dependency row e. APPLY replaces its +register expression by z_j. A query adds c z_j to its destination expression. +Take e from the pre-instruction source, also for self queries. Thus the number +of atoms is exactly r+q. Their dependencies always point to earlier atoms. +No symbolic polynomial, fresh clean vector, or physical helper is created by +this representation: atoms are compiler records only. + +Write U for the final r register rows. For each symbol a, form the state matrix +T_a: row j is atom j's dependency row if its label is a, and zero otherwise. +Let V map each original leaf to its corresponding input coordinate and all +unary atoms to zero. Induction on the acyclic dependencies gives + + coefficient of word a1 ... ak in endpoint (o,i) + = (U T_a1 ... T_ak V)_(o,i). + +Words use ordinary matrix-product order: [B,A] denotes BA, which applies A +first. Empty words supply scalar multiples of the identity on payloads. +Subtract two programs by a direct sum of their state spaces, concatenate +their initial rows with a minus sign on the second, and stack their final maps. +Inputs remain shared *semantically* through V; the compiler's two copies of +the leaf indices do not introduce independent copies of the actual data. + +The compiler supports rational coefficients, Gaussian rationals Q(i), and prime fields. +The executable's finite fields are F_p for primes p<=2^31-1; a displayed +fraction is admitted only if its denominator is invertible. The written +argument applies over any field. There is no numerical tolerance. + +## 2. The certificate and its small checker + +Let B have b<=D rows in the difference representation. A positive certificate +gives paths identifying these reachable rows and scalar coordinates H,C_a such +that + + U = H B, B T_a = C_a B for every symbol a, B V = 0. + +These **finite equalities** are the whole acceptance condition. They imply +U T_w lies in the row span of B for every word w, by induction on word length. +Hence U T_w V=0 for all words. Free words are a basis of K< X_a >, 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/universal-dirty-certificates/README.md b/research/universal-dirty-certificates/README.md new file mode 100644 index 0000000000..be4e5981e5 --- /dev/null +++ b/research/universal-dirty-certificates/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/universal-dirty-certificates/SOURCES.json b/research/universal-dirty-certificates/SOURCES.json new file mode 100644 index 0000000000..78109486a4 --- /dev/null +++ b/research/universal-dirty-certificates/SOURCES.json @@ -0,0 +1,55 @@ +{ + "schema_version": 1, + "base_commit": "ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "docs/research/pr-intake-evidence/pr4470/PROOF-REVIEW.md", + "usage": "provenance", + "git_blob": "f4dc043b6d35cae2811c9bcc064e04877f9e0549", + "sha256": "5c111dd56beb53dc44ab727d96e1af03aaf50f3023d4342e2b0a89ede6cf585b" + }, + { + "path": "research/cyclic-dirty-commutator-audit/ECHO-PROOF.md", + "usage": "provenance", + "git_blob": "23bf89c55e5c4dd82b674d9269dedee34d77510b", + "sha256": "e98e459720d8013618853bb4836558cf8bb06a4a1be03fe0954a76f178ecf403" + }, + { + "path": "research/cyclic-dirty-commutator-audit/echo.py", + "usage": "input", + "git_blob": "76a31171368eb945815cc00dce931c6c7a88e836", + "sha256": "63d44c48801f51720a7cc994d6b5e2e857d1aa4fae4c6b83c0cca032b3d9e13b" + }, + { + "path": "research/free-word-tensor-lift-audit/README.md", + "usage": "provenance", + "git_blob": "e771a770b42ac458c39a02e34bb375325bf8024a", + "sha256": "dafb6521f3782544fad354b3f660e9d36a484c137d6bb1a1805cc5fc29a752a6" + }, + { + "path": "research/two-register-three-mix/README.md", + "usage": "provenance", + "git_blob": "593549db00fac1a10734868380eab28bcb584cc2", + "sha256": "3353fe948c75fbfc56841260db02d5e14aba966d157d3390fe3d4785e397af60" + }, + { + "path": "research/universal-dirty-phase-identities/README.md", + "usage": "provenance", + "git_blob": "fdebc9c89099f0f59b2b1cc4353bc33786529011", + "sha256": "3620ec8ae93b66af22d9dff045a339ff75160b4e6c334518a01768dd69e6a0ea" + } + ], + "attribution": "Classical weighted-automata equivalence and noncommutative PIT: Kiefer 2020 notes and Raz-Shpilka 2005. Register/certificate bridge and tools prepared for zxv with substantial OpenAI Codex assistance. The live echo scheduler is retained predecessor work prepared for androolloyd, following Chafik Boukhalfa/chafreaky PR628 and Ali Romman PR621. No predecessor source modified. See README and PROOF for the tensor/dirty-phase lineage and exact new scope." +} diff --git a/research/universal-dirty-certificates/TASK.json b/research/universal-dirty-certificates/TASK.json new file mode 100644 index 0000000000..736307ea56 --- /dev/null +++ b/research/universal-dirty-certificates/TASK.json @@ -0,0 +1,107 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 7, + "base_commit": "ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Inventory the gate-operand parity lemma (#3807) and certified endpoint arithmetic (#3857). Neither is a full multiplication proof. For #4100, audit the compact-switch statement and its hypotheses before formalizing it.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Compact exact universal-substitution certificates and explicit matrix counterexamples for complete dirty linear programs over Q, Q(i) or prime fields, including literal pinned echo scheduler adapters.", + "scope_change_reason": "The user explicitly requested a high-leverage reusable result rather than a kappa increase. This replaces a single Lean interface formalization with a written generic bridge, reusable certificate tools, and source-bound applications. No Lean or full theorem formalization is claimed.", + "bottleneck_link": "Repeated dirty-connector, cleanup and tensor-lift work needs universal operator identities. A small invariant-subspace certificate closes this algebraic obligation without exponential word expansion or extrapolating from small matrices.", + "budget_minutes": 60, + "stop_rule": "Stop after the compact compiler and closure theorem, a separate no-elimination checker, a real pinned scheduler adapter, explicit failure witnesses and bounded semantic controls. Do not expand to relation-aware or physical/native admission.", + "outcome": "completed", + "evidence": "PROOF.md; 210 source-echo identities; 120 explicit-word differential circuits; 180 literal matrix counterexamples; malformed certificate/input and characteristic controls; committed examples; exponential 2^64-support case using 130 states and 65 closure rows.", + "author": "zxv, with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance in derivation, implementation, documentation, source inspection and self-review. No subagents, proof assistant or independent human review.", + "open_questions": [ + { + "question": "Bind one more independent-symbol contributor program to this grammar.", + "why_it_matters": "A source adapter makes the reusable algebra bridge available at another actual caller.", + "first_step": "Translate the literal instructions and every returned role; compare against a pinned symbolic endpoint oracle.", + "blocked_by": "The actual operator relations and equal-space typing must fit the grammar." + }, + { + "question": "Can a relation-aware frontend retain compact proof certificates?", + "why_it_matters": "Native suppliers often depend on inverse or commutation relations absent from this independent-symbol model.", + "first_step": "Choose one relation model and prove a sound normalization interface before implementing it.", + "blocked_by": "No relation-aware normalization theorem or implementation is supplied." + }, + { + "question": "Can rational coefficient growth and path reconstruction be reduced on a larger real source?", + "why_it_matters": "Polynomial field-operation counts do not ensure practical replay of all large suppliers.", + "first_step": "Profile a literal larger adapter and preserve all existing closure equations and controls.", + "blocked_by": "A larger compatible pinned adapter is needed." + } + ] +} diff --git a/research/universal-dirty-certificates/VALIDATION.json b/research/universal-dirty-certificates/VALIDATION.json new file mode 100644 index 0000000000..7f05adf1a2 --- /dev/null +++ b/research/universal-dirty-certificates/VALIDATION.json @@ -0,0 +1,95 @@ +{ + "schema_version": 1, + "status": "author_checked_scoped_algebra", + "environment": { + "registered_python": "Python 3.12.8", + "host_python": "3.14.5 (main, May 10 2026, 10:21:34) [Clang 21.0.0 (clang-2100.0.123.102)]", + "platform": "macOS-26.5.1-arm64-arm-64bit-Mach-O" + }, + "canonical_base": "ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c", + "priority_revision": 7, + "command": [ + "python3.12", + "-B", + "scripts/research_package.py", + "--package", + "research/universal-dirty-certificates" + ], + "normal_and_optimized_reports": [ + { + "certificate_rejections": 15, + "committed_examples": 3, + "differential_cases": 120, + "echo_identities": 210, + "exponential_support": { + "basis_rows": 65, + "distinct_words": 18446744073709551616, + "seconds": 1.464981, + "states": 130 + }, + "finite_field_operations": 596, + "gaussian_field_controls": 51, + "input_rejections": 9, + "literal_counterexamples": 180, + "max_echo_basis_rows": 38, + "max_echo_states": 284, + "seconds": 10.473044, + "tensor_of_sum_rejections": 1 + }, + { + "certificate_rejections": 15, + "committed_examples": 3, + "differential_cases": 120, + "echo_identities": 210, + "exponential_support": { + "basis_rows": 65, + "distinct_words": 18446744073709551616, + "seconds": 1.41866, + "states": 130 + }, + "finite_field_operations": 596, + "gaussian_field_controls": 51, + "input_rejections": 9, + "literal_counterexamples": 180, + "max_echo_basis_rows": 38, + "max_echo_states": 284, + "seconds": 9.771688, + "tensor_of_sum_rejections": 1 + } + ], + "replay_log_sha256": "eda9a9b6b33f6b4a6b14d74d4b57b2982b90e2adbb075779f0db83fb3d685215", + "verified_source_sha256": { + "check_certificate.py": "09cba2605c62f8af0dc48cf60b4eab9f8711cba820e22698d0447833c1a16c37", + "examples/binary-echo3.certificate.json": "cd088d9d5c0a8378361341c99e25ae5654a6be0b20398c9757a76804df2ab66a", + "examples/binary-echo3.json": "a5199c1dc6236e346891c641b9402d8065c5bd29087c560e76fcdf2299cdfcf9", + "examples/dirty-echo3.certificate.json": "21444c604e17d0cbd707ffbecde10edb4bdff0bdc5a3ffb71819be04c3ac58c5", + "examples/dirty-echo3.json": "862281041cd5616a8785b526d0cee57a50aa7457a8cb64a0abff1133d6d60798", + "examples/wrong-order.certificate.json": "54850450cc231e4db2a1c4637fc3f7a49dfb694d9c64cfeb8faa8df91d529a79", + "examples/wrong-order.json": "137def9876c1195456a312b8c232d656ff063cc5caae645be6afc3d06709742c", + "fields.py": "0829ad6ed3775ba6e3d11cf04cfb3513ac763549b730aaed74958b1238e660d7", + "linear_words.py": "fe825cf7c886de61bb5ec5a02171c5a392a7bddc185280726f4c359b3f289584", + "verify.py": "2759a2e7514453012ed0e4ffc7017375dea973925672dc16f127d91790dcb6e5" + }, + "orientation": { + "status": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "command": "python3 -B scripts/research_selected_baseline.py", + "selected": "60403/20000000", + "scope": "Metadata/source closure only; full selected replay not run. Initial sparse omissions were resolved by materializing the selected 522-file binding closure." + }, + "coordination": { + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19145795", + "upstream_checked": "ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c", + "remote_snapshot": "2026-10-23T12:57:31Z", + "open_pr_records": 341, + "discussion_records": 4444, + "remote_pagination_complete": true, + "sparse_local_overlap": "Only 5 local notes in the sparse report; not complete. Complemented by full original working-tree source scans and git grep over all origin/main research README/PROOF and docs research files for weighted-automata/PIT terms. No matching generic checker found; no novelty guarantee." + }, + "trust_and_unrun": [ + "Written proof and exact Python certificates; no proof-assistant or independent human review.", + "Separate checker compiler; shared fields.py is trusted arithmetic.", + "No inverse/commutation/Clifford relation-aware decision procedure.", + "No rounded backend, native supplier, hosting, stock, fixed-tape, moment, outer or full multiplication replay." + ], + "earlier_runs": "The final registered transcript supersedes earlier prototype runs. Metadata scaffolding and sparse-orientation failures were corrected; no scientific predecessor was modified." +} diff --git a/research/universal-dirty-certificates/VERIFY.json b/research/universal-dirty-certificates/VERIFY.json new file mode 100644 index 0000000000..30348d9569 --- /dev/null +++ b/research/universal-dirty-certificates/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/cyclic-dirty-commutator-audit/echo.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 90, + "checks": "Universal complete dirty-echo certificates; explicit-word differential circuits; literal nilpotent/unipotent witnesses; characteristic, tensor and certificate rejection controls; 2^64 support stress case; committed examples." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 90, + "checks": "Same semantic coverage with Python assertions disabled." + } + ] +} diff --git a/research/universal-dirty-certificates/check_certificate.py b/research/universal-dirty-certificates/check_certificate.py new file mode 100644 index 0000000000..cdb1d3fe14 --- /dev/null +++ b/research/universal-dirty-certificates/check_certificate.py @@ -0,0 +1,198 @@ +"""Small proof checker: no search, Gaussian elimination, or producer import. + +The trusted surface includes this separately transcribed register compiler. +Prepared for zxv with substantial OpenAI Codex assistance. Apache-2.0. +""" +from fractions import Fraction as F +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 require(ok, reason): + if not ok: + raise ValueError(reason) + + +def combine(terms): + result = {} + for c, v in terms: + for i, x in v.items(): + result[i] = result.get(i, F(0))+c*x + return {i: x for i, x in result.items() if x} + + +def reconstruct(problem, shifted): + """Reconstruct a dense dependency table using immutable register versions.""" + n = problem["roles"] + require(type(n) is int and n > 0, "roles") + require(set(problem) <= {"field", "roles", "program", "reference", "target"}, "problem keys") + field = scalars(problem) + require(("target" in problem) != ("reference" in problem), "reference/target") + dependencies, labels, final = [], [], [] + + def scalar(x): + require(type(x) in (str, int), "coefficient type") + return field(x) + + def role(i): + require(type(i) is int and 0 <= i < n, "role index") + return i + + def leaf(i): + j = len(labels) + labels.append(None) + dependencies.append({}) + final.append(i) + return {j: field(1)} + + def unary(s, v): + require(type(s) is str and s, "symbol") + j = len(labels) + labels.append(s) + dependencies.append(v.copy()) + final.append(None) + return combine([(F(1), {j: field(1)}), (F(1), v)]) if shifted else {j: field(1)} + + def instructions(ops): + require(type(ops) is list, "instruction list") + registers = [leaf(i) for i in range(n)] + for op in ops: + require(type(op) is dict, "instruction") + k = op.get("op") + keys = {"add": {"op", "src", "dst", "coefficient"}, + "query": {"op", "src", "dst", "symbol", "coefficient"}, + "apply": {"op", "dst", "symbol"}, + "scale": {"op", "dst", "coefficient"}, + "swap": {"op", "src", "dst"}} + require(k in keys and set(op) <= keys[k], "instruction keys") + d = role(op["dst"]) + if k in ("add", "query", "swap"): + s = role(op["src"]) + if k == "swap": + registers[s], registers[d] = registers[d], registers[s] + elif k == "scale": + registers[d] = combine([(scalar(op["coefficient"]), registers[d])]) + elif k == "apply": + registers[d] = unary(op["symbol"], registers[d]) + else: + image = registers[s].copy() + if k == "query": + image = unary(op["symbol"], image) + registers[d] = combine([(F(1), registers[d]), (scalar(op.get("coefficient", 1)), image)]) + return registers + + left = instructions(problem["program"]) + if "reference" in problem: + right = instructions(problem["reference"]) + else: + t = problem["target"] + require(type(t) is dict and set(t) <= {"identity", "terms"}, "target") + require(type(t.get("identity", True)) is bool and type(t.get("terms", [])) is list, "target types") + leaves = [leaf(i) for i in range(n)] + right = [v.copy() if t.get("identity", True) else {} for v in leaves] + for term in t.get("terms", []): + require(type(term) is dict and set(term) <= {"out", "in", "word", "coefficient"}, "term keys") + i, j = role(term["out"]), role(term["in"]) + require(type(term["word"]) is list, "word") + image = leaves[j] + for a in term["word"][::-1]: + image = unary(a, image) + right[i] = combine([(F(1), right[i]), (scalar(term.get("coefficient", 1)), image)]) + roots = [combine([(F(1), x), (F(-1), y)]) for x, y in zip(left, right)] + + def transition(v, a): + return combine([(x, dependencies[i]) for i, x in v.items() if labels[i] == a]) + + def terminal(v): + return combine([(x, {final[i]: F(1)}) for i, x in v.items() if final[i] is not None]) + + return roots, transition, terminal, len(labels), sorted(set(labels)-{None}) + + +def check(problem, certificate): + require(certificate.get("schema") == "dirty-linear-certificate/v1", "certificate schema") + source_hash = hashlib.sha256(json.dumps(problem, sort_keys=True, separators=(",", ":")).encode()).hexdigest() + require(certificate.get("problem_sha256") == source_hash, "problem digest") + shifted = certificate.get("shifted") + require(type(shifted) is bool and type(certificate.get("equivalent")) is bool, "certificate flags") + roots, step, terminal, states, alphabet = reconstruct(problem, shifted) + field = scalars(problem) + require(certificate.get("states") == states, "state count") + + def path(output, word): + require(type(output) is int and 0 <= output < len(roots), "output role") + require(type(word) is list and all(a in alphabet for a in word), "path alphabet") + v = roots[output] + for a in word: + v = step(v, a) + return v + + if not certificate["equivalent"]: + out = terminal(path(certificate["output"], certificate["word"])) + j = certificate["input"] + require(type(j) is int and 0 <= j < len(roots), "input role") + require(type(certificate["coefficient"]) is str, "witness coefficient type") + require(out.get(j, field(0)) == field(certificate["coefficient"]) != 0, "nonzero coefficient") + require(certificate["matrix_dimension"] == len(certificate["word"])+1, "matrix dimension") + return "counterexample" + + paths = certificate["paths"] + require(type(paths) is list and len(paths) <= states, "basis size") + basis = [path(p["output"], p["word"]) for p in paths] + require(all(not terminal(v) for v in basis), "basis output is nonzero") + + def expand(c): + require(type(c) is dict, "coordinates must be a sparse object") + terms = [] + for j, x in c.items(): + require(type(j) is str and j.isascii() and j.isdecimal() and str(int(j)) == j, "coordinate key") + require(0 <= int(j) < len(basis) and type(x) is str, "coordinate range/type") + terms.append((field(x), basis[int(j)])) + return combine(terms) + + init = certificate["initial"] + require(type(init) is list and len(init) == len(roots), "initial coverage") + require(all(expand(c) == v for c, v in zip(init, roots)), "initial span") + closure = certificate["closure"] + require(type(closure) is dict and set(closure) == set(alphabet), "complete operator closure") + for a in alphabet: + rows = closure[a] + require(type(rows) is list and len(rows) == len(basis), "closure row coverage") + require(all(expand(c) == step(v, a) for c, v in zip(rows, basis)), "invariant closure") + return "universal-identity" + + +def main(): + p = argparse.ArgumentParser(description=__doc__) + p.add_argument("problem", type=Path) + p.add_argument("certificate", type=Path) + p.add_argument("--matrices", action="store_true", help="print sparse concrete counterexample matrices") + args = p.parse_args() + problem, certificate = json.loads(args.problem.read_text()), json.loads(args.certificate.read_text()) + verdict = check(problem, certificate) + if args.matrices: + require(verdict == "counterexample", "a positive certificate has no counterexample") + word = certificate["word"] + d = len(word)+1 + _, _, _, _, alphabet = reconstruct(problem, certificate["shifted"]) + matrices = {} + for a in alphabet: + triples = [[j, j, 1] for j in range(d)] if certificate["shifted"] else [] + triples += [[j, j+1, 1] for j, b in enumerate(word) if b == a] + matrices[a] = triples + print(json.dumps({"field": problem.get("field", "Q"), "dimension": d, + "operators_as_row_column_value": matrices, + "input_role": certificate["input"], "input_payload_basis": d-1, + "output_role": certificate["output"], "output_coordinate": 0, + "endpoint_discrepancy": certificate["coefficient"]}, indent=2, sort_keys=True)) + else: + print("PASS_DIRTY_LINEAR_CERTIFICATE", verdict) + + +if __name__ == "__main__": + main() diff --git a/research/universal-dirty-certificates/examples/binary-echo3.certificate.json b/research/universal-dirty-certificates/examples/binary-echo3.certificate.json new file mode 100644 index 0000000000..34996f4e42 --- /dev/null +++ b/research/universal-dirty-certificates/examples/binary-echo3.certificate.json @@ -0,0 +1,84 @@ +{ + "closure": { + "A0": [ + {}, + {}, + {}, + {}, + {}, + { + "0": "1" + } + ], + "A1": [ + {}, + {}, + {}, + {}, + { + "5": "1" + }, + {} + ], + "A2": [ + {}, + { + "4": "1" + }, + {}, + {}, + {}, + {} + ] + }, + "equivalent": true, + "initial": [ + { + "0": "1" + }, + { + "1": "1" + }, + { + "2": "1" + }, + { + "3": "1" + } + ], + "paths": [ + { + "output": 0, + "word": [] + }, + { + "output": 1, + "word": [] + }, + { + "output": 2, + "word": [] + }, + { + "output": 3, + "word": [] + }, + { + "output": 1, + "word": [ + "A2" + ] + }, + { + "output": 1, + "word": [ + "A2", + "A1" + ] + } + ], + "problem_sha256": "b2b6159a748c9b6181c62c4b0dedaa37cd63b6ebb099adf259ebaacdf1435348", + "schema": "dirty-linear-certificate/v1", + "shifted": false, + "states": 19 +} diff --git a/research/universal-dirty-certificates/examples/binary-echo3.json b/research/universal-dirty-certificates/examples/binary-echo3.json new file mode 100644 index 0000000000..8bb08f6465 --- /dev/null +++ b/research/universal-dirty-certificates/examples/binary-echo3.json @@ -0,0 +1,77 @@ +{ + "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": [ + "A2", + "A1", + "A0" + ], + "coefficient": 1 + } + ] + }, + "field": 2 +} diff --git a/research/universal-dirty-certificates/examples/dirty-echo3.certificate.json b/research/universal-dirty-certificates/examples/dirty-echo3.certificate.json new file mode 100644 index 0000000000..f19706f071 --- /dev/null +++ b/research/universal-dirty-certificates/examples/dirty-echo3.certificate.json @@ -0,0 +1,84 @@ +{ + "closure": { + "A0": [ + {}, + {}, + {}, + {}, + {}, + { + "0": "1" + } + ], + "A1": [ + {}, + {}, + {}, + {}, + { + "5": "1" + }, + {} + ], + "A2": [ + {}, + { + "4": "1" + }, + {}, + {}, + {}, + {} + ] + }, + "equivalent": true, + "initial": [ + { + "0": "1" + }, + { + "1": "1" + }, + { + "2": "1" + }, + { + "3": "1" + } + ], + "paths": [ + { + "output": 0, + "word": [] + }, + { + "output": 1, + "word": [] + }, + { + "output": 2, + "word": [] + }, + { + "output": 3, + "word": [] + }, + { + "output": 1, + "word": [ + "A2" + ] + }, + { + "output": 1, + "word": [ + "A2", + "A1" + ] + } + ], + "problem_sha256": "01dcf72f1c54c9abc3a8dfd59a0107ca3d26bfd53429e769d9c61ce1e8dadc4f", + "schema": "dirty-linear-certificate/v1", + "shifted": false, + "states": 19 +} diff --git a/research/universal-dirty-certificates/examples/dirty-echo3.json b/research/universal-dirty-certificates/examples/dirty-echo3.json new file mode 100644 index 0000000000..13c38bf647 --- /dev/null +++ b/research/universal-dirty-certificates/examples/dirty-echo3.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": [ + "A2", + "A1", + "A0" + ], + "coefficient": 1 + } + ] + } +} diff --git a/research/universal-dirty-certificates/examples/wrong-order.certificate.json b/research/universal-dirty-certificates/examples/wrong-order.certificate.json new file mode 100644 index 0000000000..20e3102d5a --- /dev/null +++ b/research/universal-dirty-certificates/examples/wrong-order.certificate.json @@ -0,0 +1,15 @@ +{ + "coefficient": "-1", + "equivalent": false, + "input": 0, + "matrix_dimension": 3, + "output": 1, + "problem_sha256": "d32cd250d576afa157b04f24b9583bec75b113fafddfc831a86079ce5e583ae9", + "schema": "dirty-linear-certificate/v1", + "shifted": true, + "states": 19, + "word": [ + "A0", + "A1" + ] +} diff --git a/research/universal-dirty-certificates/examples/wrong-order.json b/research/universal-dirty-certificates/examples/wrong-order.json new file mode 100644 index 0000000000..85482942f0 --- /dev/null +++ b/research/universal-dirty-certificates/examples/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 + } + ] + } +} diff --git a/research/universal-dirty-certificates/fields.py b/research/universal-dirty-certificates/fields.py new file mode 100644 index 0000000000..f1b6dc83e2 --- /dev/null +++ b/research/universal-dirty-certificates/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/universal-dirty-certificates/linear_words.py b/research/universal-dirty-certificates/linear_words.py new file mode 100644 index 0000000000..4a877e1ab9 --- /dev/null +++ b/research/universal-dirty-certificates/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/universal-dirty-certificates/verify.py b/research/universal-dirty-certificates/verify.py new file mode 100644 index 0000000000..abccca3c9e --- /dev/null +++ b/research/universal-dirty-certificates/verify.py @@ -0,0 +1,376 @@ +#!/usr/bin/env python3 +"""Bounded semantic validation; default execution is read-only. + +Prepared for zxv with substantial OpenAI Codex assistance. Apache-2.0. +""" +from copy import deepcopy +from fractions import Fraction as Q +import hashlib +import importlib.util +import itertools +import json +from pathlib import Path +import random +import sys +import time + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +import linear_words as producer +import check_certificate as checker + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def ident(d): + return [[Q(i == j) for j in range(d)] for i in range(d)] + + +def plus(a, b): + return [[x+y for x, y in zip(ra, rb)] for ra, rb in zip(a, b)] + + +def times(a, b): + return [[sum((a[i][k]*b[k][j] for k in range(len(b))), Q(0)) + for j in range(len(b[0]))] for i in range(len(a))] + + +def constant(c, a): + return [[c*x for x in row] for row in a] + + +def dense(problem, matrices): + """Literal full-column interpreter, unrelated to the atom representation.""" + n, d = problem["roles"], len(next(iter(matrices.values()), [[1]])) + scalar = producer.scalars(problem) if problem.get("field") == "Qi" else Q + zero = [[Q(0)]*d for _ in range(d)] + + def execute(ops): + rows = [[ident(d) if i == j else deepcopy(zero) for j in range(n)] for i in range(n)] + for op in ops: + k, dst = op["op"], op["dst"] + if k == "swap": + s = op["src"] + rows[s], rows[dst] = rows[dst], rows[s] + elif k == "scale": + rows[dst] = [constant(scalar(op["coefficient"]), b) for b in rows[dst]] + elif k == "apply": + rows[dst] = [times(matrices[op["symbol"]], b) for b in rows[dst]] + else: + source = deepcopy(rows[op["src"]]) + if k == "query": + source = [times(matrices[op["symbol"]], b) for b in source] + c = scalar(op.get("coefficient", 1)) + rows[dst] = [plus(x, constant(c, y)) for x, y in zip(rows[dst], source)] + return rows + + left = execute(problem["program"]) + if "reference" in problem: + right = execute(problem["reference"]) + else: + t = problem["target"] + right = [[ident(d) if t.get("identity", True) and i == j else deepcopy(zero) + for j in range(n)] for i in range(n)] + for term in t.get("terms", []): + v = ident(d) + for a in term["word"]: + v = times(v, matrices[a]) + i, j = term["out"], term["in"] + right[i][j] = plus(right[i][j], constant(scalar(term.get("coefficient", 1)), v)) + return [[plus(x, constant(-1, y)) for x, y in zip(a, b)] for a, b in zip(left, right)] + + +def witness_matrices(problem, certificate): + m = producer.compile_problem(problem) + word = certificate["word"] + d = len(word)+1 + out = {} + for a in m.edges: + matrix = ident(d) if certificate["shifted"] else [[Q(0)]*d for _ in range(d)] + for j, b in enumerate(word): + if a == b: + matrix[j][j+1] += 1 + out[a] = matrix + return out + + +def check_negative(problem, certificate): + need(checker.check(problem, certificate) == "counterexample", "coefficient checker") + residual = dense(problem, witness_matrices(problem, certificate)) + value = residual[certificate["output"]][certificate["input"]][0][-1] + field = producer.scalars(problem) + need(field(value) == field(certificate["coefficient"]) != 0, "literal matrix counterexample") + + +def explicit_polynomials(problem): + """Independent small-case word expansion: maps (word,input) to coefficients.""" + n = problem["roles"] + rows = [{((), i): Q(1)} for i in range(n)] + + def add(a, b, c=Q(1)): + r = a.copy() + for key, x in b.items(): + r[key] = r.get(key, Q(0))+c*x + return {k: x for k, x in r.items() if x} + + for op in problem["program"]: + k, d = op["op"], op["dst"] + if k == "swap": + s = op["src"] + rows[s], rows[d] = rows[d], rows[s] + elif k == "scale": + rows[d] = {key: Q(op["coefficient"])*x for key, x in rows[d].items() if Q(op["coefficient"])*x} + else: + source = rows[d if k == "apply" else op["src"]].copy() + if k in ("query", "apply"): + source = {((op["symbol"],)+word, i): x for (word, i), x in source.items()} + rows[d] = source if k == "apply" else add(rows[d], source, Q(op.get("coefficient", 1))) + return rows + + +def source_echo(): + path = HERE.parents[1]/"research/cyclic-dirty-commutator-audit/echo.py" + manifest = json.loads((HERE/"SOURCES.json").read_text()) + pin = next(f for f in manifest["files"] if f["path"].endswith("/echo.py")) + need(hashlib.sha256(path.read_bytes()).hexdigest() == pin["sha256"], "echo source pin") + spec = importlib.util.spec_from_file_location("pinned_echo", path) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +def echo_problem(source, count, fanout, sign=1): + scratch, calls = source.resources(count, fanout) + instructions = list(source.instructions(0, count, 0, 1, 2, fanout, sign)) + need(len(instructions) == calls, "source count") + return {"roles": 2+scratch, + "program": [{"op": "query", "src": s, "dst": t, "symbol": f"A{i}", "coefficient": q} + for s, t, i, q in instructions], + "target": {"identity": True, "terms": [{"out": 1, "in": 0, + "word": [f"A{i}" for i in reversed(range(count))], "coefficient": sign}]}} + + +def rejected(fn): + try: + fn() + except (ValueError, KeyError, TypeError, ZeroDivisionError): + return + raise ValueError("malformed control accepted") + + +def main(): + source = source_echo() + report = {"echo_identities": 0, "literal_counterexamples": 0, "differential_cases": 0, + "certificate_rejections": 0, "input_rejections": 0} + start = time.monotonic() + max_states = max_basis = 0 + for field in ("Q", "Qi", 2, 3, 5): + for n in (1, 2, 3, 5, 8, 12, 16): + for fanout in (2, 3, 8): + for sign in (-1, 1): + p = echo_problem(source, n, fanout, sign) + p["field"] = field + c = producer.decide(p) + need(c["equivalent"] and checker.check(p, c) == "universal-identity", "source echo identity") + max_states = max(max_states, c["states"]) + max_basis = max(max_basis, len(c["paths"])) + report["echo_identities"] += 1 + p = echo_problem(source, 3, 3) + mutations = [] + a = deepcopy(p); a["program"].pop(); mutations.append(a) + a = deepcopy(p); a["program"][1]["coefficient"] *= -1; mutations.append(a) + a = deepcopy(p); a["target"]["terms"][0]["word"].reverse(); mutations.append(a) + a = deepcopy(p); a["program"][0]["src"] = 1; mutations.append(a) + a = deepcopy(p); a["program"].append({"op": "scale", "dst": 2, "coefficient": 0}); mutations.append(a) + for field in ("Q", "Qi", 2, 3, 5): + for a in mutations: + a["field"] = field + for shift in (False, True): + c = producer.decide(a, shift) + # Negating a call changes nothing in characteristic two. + if field == 2 and a is mutations[1]: + need(c["equivalent"], "characteristic-two sign") + checker.check(a, c) + continue + need(not c["equivalent"], "bad echo accepted") + check_negative(a, c) + report["literal_counterexamples"] += 1 + + # Dense scalar evaluations cannot see a commutator. The formal checker can. + trap = {"roles": 1, "program": [], "target": {"terms": [ + {"out": 0, "in": 0, "word": ["X", "Y"]}, + {"out": 0, "in": 0, "word": ["Y", "X"], "coefficient": -1}]}} + for x, y in itertools.product(range(-2, 3), repeat=2): + need(dense(trap, {"X": [[Q(x)]], "Y": [[Q(y)]]}) == [[[[0]]]], "scalar blindness") + for shift in (False, True): + c = producer.decide(trap, shift) + need(len(c["word"]) == 2, "shortest commutator word") + check_negative(trap, c) + report["literal_counterexamples"] += 1 + bad = producer.decide(trap) + for key, value in (("coefficient", "0"), ("input", 1), ("matrix_dimension", 99), ("word", ["X"])): + wrong = deepcopy(bad); wrong[key] = value + rejected(lambda: checker.check(trap, wrong)) + report["certificate_rejections"] += 1 + + # Tensoring the named unary map H=G-I differs from substituting in G-I. + def kron(a, b): + return [[a[i][j]*b[k][l] for j in range(len(a)) for l in range(len(b))] + for i in range(len(a)) for k in range(len(b))] + g = [[Q(2), Q(0)], [Q(0), Q(3)]] + h = plus(g, constant(-1, ident(2))) + need(h == [[1, 0], [0, 2]], "one-column tensor trap premise") + need(kron(h, h) != plus(kron(g, g), constant(-1, ident(4))), "tensor-of-sum trap") + report["tensor_of_sum_rejections"] = 1 + + # Exact differential tests include self reads, rational signs, swaps, scales, + # zero maps, dead symbols, and correlated reuse. Expand only these small cases. + rng = random.Random(20261023) + for _ in range(120): + n = rng.randrange(1, 5) + ops = [] + for _ in range(9): + k, s, d = rng.choice(("add", "query", "apply", "scale", "swap")), rng.randrange(n), rng.randrange(n) + op = {"op": k, "dst": d} + if k in ("add", "query", "swap"): + op["src"] = s + if k in ("query", "apply"): + op["symbol"] = rng.choice(("X", "Y")) + if k in ("add", "query", "scale"): + op["coefficient"] = rng.choice(("0", "1/2", "-2", "3/2")) + ops.append(op) + a = {"roles": n, "program": ops} + rows = explicit_polynomials(a) + terms = [{"out": o, "in": i, "word": list(w), "coefficient": str(c)} + for o, row in enumerate(rows) for (w, i), c in row.items()] + a["target"] = {"identity": False, "terms": terms} + for shift in (False, True): + c = producer.decide(a, shift) + need(c["equivalent"], "word expansion mismatch") + checker.check(a, c) + # Force a known discrepancy, then compare shortest degree to expansion. + a["target"]["terms"].append({"out": 0, "in": 0, "word": ["X", "Y", "X"], "coefficient": 1}) + c = producer.decide(a) + need(not c["equivalent"] and len(c["word"]) == 3, "shortest witness mismatch") + check_negative(a, c) + report["literal_counterexamples"] += 1 + report["differential_cases"] += 1 + + c = producer.decide(p) + corruptions = [] + a = deepcopy(c); a["paths"].pop(); corruptions.append(a) + a = deepcopy(c); a["initial"].pop(); corruptions.append(a) + a = deepcopy(c); a["initial"][0] = {}; corruptions.append(a) + a = deepcopy(c); a["closure"].pop(next(iter(a["closure"]))); corruptions.append(a) + a = deepcopy(c); a["closure"][next(iter(a["closure"]))].pop(); corruptions.append(a) + a = deepcopy(c); a["problem_sha256"] = "0"*64; corruptions.append(a) + a = deepcopy(c); a["states"] += 1; corruptions.append(a) + a = deepcopy(c); a["shifted"] = 0; corruptions.append(a) + a = deepcopy(c); a["paths"][0]["word"] = ["unknown"]; corruptions.append(a) + # Replace one genuinely nonzero closure row by zero. + a = deepcopy(c) + symbol, row = next((s, i) for s, rows in a["closure"].items() for i, v in enumerate(rows) if v) + a["closure"][symbol][row] = {}; corruptions.append(a) + a = deepcopy(c); a["initial"][0] = {"99999": "1"}; corruptions.append(a) + for a in corruptions: + rejected(lambda: checker.check(p, a)) + report["certificate_rejections"] += 1 + # Omit every dirty-return requirement except the apparent target success. + # The earlier scale(0) mutation proves that such a weakening would miss dirt. + for modify in ( + lambda a: a.update(roles=True), + lambda a: a["program"][0].update(src=99), + lambda a: a["program"][0].update(coefficient=0.5), + lambda a: a["program"][0].update(op="inverse"), + lambda a: a["program"][0].update(symbol=""), + lambda a: a.update(reference=[]), + lambda a: a.update(field=4), + lambda a: a.update(field=True), + lambda a: (a.update(field=2), a["program"][0].update(coefficient="1/2")), + ): + a = deepcopy(p); modify(a) + rejected(lambda: producer.decide(a)) + report["input_rejections"] += 1 + + # A characteristic-dependent identity must not be silently certified over Q. + binary = {"roles": 2, "program": [{"op": "query", "src": 0, "dst": 1, "symbol": "X"}]*2, + "reference": []} + need(not producer.decide(binary)["equivalent"], "rational double query") + binary["field"] = 2 + checker.check(binary, producer.decide(binary)) + report["finite_field_operations"] = 0 + for prime in (2, 3, 5, 7, 11): + field = producer.scalars({"field": prime}) + for x, y in itertools.product(range(prime), repeat=2): + need(str(field(x)+field(y)) == str((x+y) % prime), "field addition") + need(str(field(x)*field(y)) == str(x*y % prime), "field product") + if y: + need(str(field(x)/field(y)) == str(x*pow(y, -1, prime) % prime), "field quotient") + report["finite_field_operations"] += 2+bool(y) + + gaussian = producer.scalars({"field": "Qi"}) + complex_problem = {"field": "Qi", "roles": 2, "program": [ + {"op": "scale", "dst": 0, "coefficient": "i"}, + {"op": "query", "src": 0, "dst": 1, "symbol": "X", "coefficient": "1/2+3/4i"}, + {"op": "scale", "dst": 0, "coefficient": "-i"}], + "target": {"terms": [{"out": 1, "in": 0, "word": ["X"], "coefficient": "-3/4+1/2i"}]}} + checker.check(complex_problem, producer.decide(complex_problem)) + need(gaussian("i")*gaussian("i") == -1, "Gaussian phase square") + for r, s in itertools.product(range(-2, 3), repeat=2): + z = gaussian.pair(Q(r, 2), Q(s, 3)) + need(gaussian(str(z)) == z, "Gaussian exact serialization") + if z: + need(z/z == 1, "Gaussian quotient") + complex_problem["target"]["terms"][0]["coefficient"] = "-3/4-1/2i" + for shift in (False, True): + check_negative(complex_problem, producer.decide(complex_problem, shift)) + report["literal_counterexamples"] += 1 + report["gaussian_field_controls"] = 51 + + # 2^64 distinct words per endpoint; never enumerate them. + k = 64 + ops = [{"op": "query", "src": 0, "dst": 0, "symbol": f"X{i}"} for i in range(k)] + stress = {"roles": 1, "program": ops, "reference": + [{"op": "scale", "dst": 0, "coefficient": 2}]+ops+ + [{"op": "scale", "dst": 0, "coefficient": "1/2"}]} + t = time.monotonic(); c = producer.decide(stress); checker.check(stress, c) + report["exponential_support"] = {"distinct_words": 2**k, "states": c["states"], + "basis_rows": len(c["paths"]), "seconds": round(time.monotonic()-t, 6)} + # Sharpness of the unipotent witness bound within the unipotent test class. + for degree in range(1, 9): + a = {"roles": 1, "program": [{"op": "query", "src": 0, "dst": 0, + "symbol": "X", "coefficient": -1} for _ in range(degree)], + "reference": [{"op": "scale", "dst": 0, "coefficient": 0}]} + c = producer.decide(a, True) + need(len(c["word"]) == degree, "sharp unipotent bound") + check_negative(a, c) + for dim in range(1, degree+1): + x = ident(dim) + for j in range(dim-1): + x[j][j+1] = 1 + need(all(not z for row in dense(a, {"X": x})[0][0] for z in row), "below degree vanishing") + report["literal_counterexamples"] += 1 + report["max_echo_states"] = max_states + report["max_echo_basis_rows"] = max_basis + report["seconds"] = round(time.monotonic()-start, 6) + names = ("dirty-echo3", "binary-echo3", "wrong-order") + expected = {name+suffix for name in names for suffix in (".json", ".certificate.json")} + need({p.name for p in (HERE/"examples").glob("*.json")} == expected, "committed example inventory") + for name in names: + path = HERE/"examples"/(name+".json") + example = json.loads(path.read_text()) + certificate = json.loads(path.with_suffix(".certificate.json").read_text()) + checker.check(example, certificate) + need(producer.decide(example, certificate["shifted"]) == certificate, "committed certificate drift") + if not certificate["equivalent"]: + check_negative(example, certificate) + report["committed_examples"] = len(names) + print(json.dumps(report, indent=2, sort_keys=True)) + print("PASS_UNIVERSAL_DIRTY_CERTIFICATES") + + +if __name__ == "__main__": + main() From 48976daa4dce59b4867ef046da72a370e389925d Mon Sep 17 00:00:00 2001 From: zxv Date: Fri, 23 Oct 2026 09:06:13 -0400 Subject: [PATCH 2/2] Retain the exact normal and optimized replay transcript --- .../universal-dirty-certificates/REPLAY.txt | 45 +++++++++++++++++++ .../VALIDATION.json | 3 +- 2 files changed, 47 insertions(+), 1 deletion(-) create mode 100644 research/universal-dirty-certificates/REPLAY.txt diff --git a/research/universal-dirty-certificates/REPLAY.txt b/research/universal-dirty-certificates/REPLAY.txt new file mode 100644 index 0000000000..fddf316753 --- /dev/null +++ b/research/universal-dirty-certificates/REPLAY.txt @@ -0,0 +1,45 @@ +CHECK Universal complete dirty-echo certificates; explicit-word differential circuits; literal nilpotent/unipotent witnesses; characteristic, tensor and certificate rejection controls; 2^64 support stress case; committed examples. +{ + "certificate_rejections": 15, + "committed_examples": 3, + "differential_cases": 120, + "echo_identities": 210, + "exponential_support": { + "basis_rows": 65, + "distinct_words": 18446744073709551616, + "seconds": 1.464981, + "states": 130 + }, + "finite_field_operations": 596, + "gaussian_field_controls": 51, + "input_rejections": 9, + "literal_counterexamples": 180, + "max_echo_basis_rows": 38, + "max_echo_states": 284, + "seconds": 10.473044, + "tensor_of_sum_rejections": 1 +} +PASS_UNIVERSAL_DIRTY_CERTIFICATES +CHECK Same semantic coverage with Python assertions disabled. +{ + "certificate_rejections": 15, + "committed_examples": 3, + "differential_cases": 120, + "echo_identities": 210, + "exponential_support": { + "basis_rows": 65, + "distinct_words": 18446744073709551616, + "seconds": 1.41866, + "states": 130 + }, + "finite_field_operations": 596, + "gaussian_field_controls": 51, + "input_rejections": 9, + "literal_counterexamples": 180, + "max_echo_basis_rows": 38, + "max_echo_states": 284, + "seconds": 9.771688, + "tensor_of_sum_rejections": 1 +} +PASS_UNIVERSAL_DIRTY_CERTIFICATES +PASS_REGISTERED_RESEARCH_PACKAGE research/universal-dirty-certificates outcome=completed diff --git a/research/universal-dirty-certificates/VALIDATION.json b/research/universal-dirty-certificates/VALIDATION.json index 7f05adf1a2..8ff2470dc0 100644 --- a/research/universal-dirty-certificates/VALIDATION.json +++ b/research/universal-dirty-certificates/VALIDATION.json @@ -91,5 +91,6 @@ "No inverse/commutation/Clifford relation-aware decision procedure.", "No rounded backend, native supplier, hosting, stock, fixed-tape, moment, outer or full multiplication replay." ], - "earlier_runs": "The final registered transcript supersedes earlier prototype runs. Metadata scaffolding and sparse-orientation failures were corrected; no scientific predecessor was modified." + "earlier_runs": "The final registered transcript supersedes earlier prototype runs. Metadata scaffolding and sparse-orientation failures were corrected; no scientific predecessor was modified.", + "replay_transcript": "REPLAY.txt" }