diff --git a/research/inverse-dirty-certificates/PROOF.md b/research/inverse-dirty-certificates/PROOF.md new file mode 100644 index 0000000000..d2433c24ca --- /dev/null +++ b/research/inverse-dirty-certificates/PROOF.md @@ -0,0 +1,246 @@ +# Compact certificates with actual inverse calls + +This is a scoped written proof for the register grammar below. The implementation +and finite tests corroborate it; there is no proof-assistant or independent human +verification claim. The contribution answers the inverse-frontend question in +[zxv's PR5235](https://github.com/CrocSwap/integer-mult-bounds/pull/5235), pinned at +`48976daa4dce59b4867ef046da72a370e389925d`. That package supplies the +independent-operator register bridge, invariant certificates and unipotent +witness method. Here inverse occurrences denote the **actual inverse of the +same generator**, and therefore need a different, cyclic realization and a +sound passage from formal series to arbitrary invertible substitutions. + +Recognizable rational series, the Magnus substitution and weighted-automata +equivalence are classical. See Stefan Kiefer, +[Notes on Equivalence and Minimization of Weighted Automata](https://arxiv.org/abs/2009.01217), +and Retakh, Reutenauer and Vaintrob, +[Noncommutative rational functions and Farber's invariants of boundary links](https://arxiv.org/abs/math/0004112), +Remark 2.3 and Proposition 2.4, which recall the Magnus embedding and the +Schutzenberger/Fliess characterization. We claim a project-specific interface, +explicit state bound and executable certificate bridge, not a new general +automata/PIT algorithm or a new Magnus theorem. The argument below is +self-contained and does not require the injectivity theorem for the group +algebra embedding. + +## 1. Grammar and statement + +Fix a field K, a finite alphabet of independently chosen invertible operators +G_a on a common finite-dimensional K-vector space, and r >= 1 named registers. +All r initial vectors are independent; no dirty helper is assumed zero. +A program is a finite sequence of: + +1. scalar linear assignment to a register, with all sources read before the + assignment, including when the destination is also a source; +2. `dst <- G_a^s dst`, where s is +1 or -1; +3. `dst <- dst + c G_a^s src`, with the old source and destination, also when + `src == dst`. + +All scalar coefficients lie in K. Compare two such programs on the same +ordered roles and alphabet, returning **every** final register. Let q be the +total number of unary occurrences in both programs, including queries, inverse +occurrences, and queries with coefficient zero. Put D = r + q. + +**Theorem.** There are effectively constructed scalar matrices +U in K^(r x D), V in K^(D x r), and T_a in K^(D x D) such that: + +- the complete endpoint difference, expanded at G_a = I + Y_a, has coefficient + matrix U T_a1 ... T_ak V at every word a1...ak, including k=0; +- the programs have equal complete endpoints for every payload dimension and + every invertible substitution if and only if all these coefficients vanish; +- equality has a finite certificate consisting of at most D path rows, their + initial-span coordinates and transition-closure coordinates; +- failure has a nonzero coefficient word of length k < D and an explicit + simultaneous unipotent substitution in dimension k+1 <= D witnessing it. + +The search below finds a shortest nonzero coefficient word. The independent +certificate checker certifies its nonzeroness, **not shortestness**. It does +not claim a least-dimensional witness among arbitrary invertible matrices. + +The executable supports K=Q and prime fields F_p with p <= 2^31-1. Rational +input denominators must be nonzero in F_p. The written theorem holds over any +field. There are no commutation, involution, Clifford, adjoint or other +relations; a failure need not persist after imposing such extra relations. +Only inverses of named generators are in the grammar, not inverses of arbitrary +operator sums or matrices of operators. + +## 2. One atom per unary occurrence + +Create r leaf atoms x_i. Maintain each register as a scalar row in the atom +list. Each linear instruction updates that row. Each unary occurrence with +pre-instruction source row e creates a fresh atom z_j = G_a^s (e z). +An apply instruction replaces the destination by z_j; a query adds c z_j to +the old destination. Even a self-source query takes e before the update. + +Compile the two programs with separate mutable register tables but the same r +leaf atoms. Append all unary atoms from both sides to one list. Their source +rows use earlier atoms only. Thus there are exactly D atoms. U is the +left-minus-right matrix of all final role expressions; it retains each input +role and each output role independently. An atom is an algebraic compiler +record, not a clean physical register or a free allocation. + +Work in noncommutative formal series K<> and put G_a=1+Y_a. Its inverse +is the formal geometric series, well-defined over every characteristic. For a +forward occurrence and an inverse occurrence, respectively, the defining +equations are + + z_j = e z + Y_a e z, + z_j = e z - Y_a z_j. + +The second equation follows by multiplying z_j=(1+Y_a)^(-1)e z by 1+Y_a. +It is the inverse-aware step: a negative diagonal feedback term, not a new +independent operator label and not a truncated polynomial expansion. + +Let E have row e at every unary atom and zero leaf rows. Let V0 embed the r +input roles at the leaf rows. For each a, let A_a have row e at a forward +a-occurrence, row -unit_j at an inverse a-occurrence, and zero elsewhere. +Then, with scalar matrices commuting entrywise with the series letters, + + z = E z + V0 x + sum_a Y_a A_a z. + +E is strictly lower triangular. Consequently H=(I-E)^(-1) is the finite +scalar matrix I+E+...+E^(D-1). Set V=H V0 and T_a=H A_a. The equations become + + z = V x + sum_a Y_a T_a z. + +This system has a unique formal solution: each coefficient of positive length +is determined by shorter coefficients. Iterating gives exactly + + [a1 ... ak](U z) = U T_a1 ... T_ak V. + +Word order is matrix-product order: `[B,A]` means BA and applies A first. +The inverse feedback means T_a need not be nilpotent. Infinite nonzero tails +are allowed even though D is finite. + +The producer uses the equivalent triangular recurrences + + V_j = e V, + (T_b)_j = e T_b + 1_(b=a) e (forward), + (T_b)_j = e T_b - 1_(b=a) unit_j (inverse), + +where e only reads earlier rows. The checker instead reconstructs E,A_a and +the triangular inverse H. These are separately transcribed compilers. + +## 3. Finite closure certificates + +A positive certificate provides b <= D path rows B_l=U_o T_w and scalar +coordinate matrices L and C_a satisfying + + U = L B, B T_a = C_a B for every a, B V = 0. + +These finite equations imply U T_w V=0 for every word by induction. +Independence, minimality and reachability of B are unnecessary for soundness; +the supplied paths merely specify B compactly and bind it to the program. + +Conversely, if every coefficient is zero, the reachable space +R=span{U_o T_w} has dimension at most D, is transition-stable and annihilates V. +Choose a basis from reachable path rows. Its initial and closure coordinates +give the displayed certificate. A basis of paths shorter than D exists: +R_k, the span of paths of length at most k, cannot stop increasing and later +increase again, since R_(k+1)=R_k+sum_a R_k T_a. If R_0=0, everything is zero; +otherwise at most D-1 strict increases are possible. + +Breadth-first search tests output projections of accepted independent path +rows and appends their independent successors. Rejected dependent rows add no +possible earlier distinguishing length: their expression uses accepted rows +of no greater length, whose successors span their successors. Hence a first +nonzero projection occurs at a shortest coefficient word, of length < D. +Exact elimination is in the producer only. The checker rebuilds the path rows +and verifies the displayed equations, or verifies one claimed nonzero +coefficient on failure. No acceptance check relies on Python `assert`. + +With alphabet size s, dense production takes polynomially many field +operations (O(s D^3) for reachable-space search and coordinates, plus parsing +and compilation). Coordinate storage is O(s D^2+rD), with at most O(D^2) +path letters. The simple checker may rebuild each path from scratch, costing +O(D^4+sD^3) field operations. These are arithmetic bounds, not bounds on +rational coefficient bit lengths or a practical scaling guarantee. + +## 4. Why zero series implies every invertible substitution + +Formal series cannot be evaluated directly at arbitrary matrices by summing an +infinite series. The following argument supplies the missing step. + +Fix any dimension n and any tuple of invertible matrices M_a over K. Introduce +one central indeterminate t and substitute + + G_a(t) = I + t(M_a-I). + +Each G_a(t) has determinant with constant term 1, so is invertible over K(t) +and its inverse has a well-defined expansion in K[[t]]. The program endpoint +is therefore a matrix of rational functions regular at t=0. Its formal +expansion is precisely the specialization Y_a -> t(M_a-I) of the series from +Section 2: in each degree there are only finitely many words, so substitution +is legitimate. + +If the noncommutative endpoint series is zero, this matrix has identically +zero power series at t=0. A rational function regular at zero with zero formal +expansion is zero in K(t): multiply by its denominator, whose constant term is +nonzero. Finally every inverse occurrence is regular at t=1, since +det G_a(1)=det M_a != 0. Evaluating the zero rational endpoint at t=1 proves +equality for this arbitrary invertible tuple M_a. This is valid over finite +fields as well; it uses a formal indeterminate, not sampling field elements. + +Thus a finite closure certificate proves the complete universal invertible +endpoint claim, without assuming convergence, generic numerical invertibility +or an infinite-field polynomial identity heuristic. + +## 5. Nonzero series gives an explicit invertible witness + +Suppose c=(U T_a1 ... T_ak V)_(o,i) is nonzero. On the basis e_0,...,e_k let + + N_a = sum_(j=0 to k-1, a_(j+1)=a) E_(j,j+1), + G_a = I + N_a. + +All N_a share the same strictly upper-triangular flag. All products of more +than k such matrices vanish, and each inverse G_a^(-1) is the finite sum +I-N_a+N_a^2-...+(-N_a)^k. Therefore the formal-series substitution now really +is a finite calculation, also for programs containing inverse calls. + +In matrix entry (0,k), shorter words give zero, longer words give zero, and a +word of length k gives one exactly when its labels are a1,...,ak in order. +The literal endpoint difference in block (o,i), entry (0,k), equals c. +Use input e_k in role i and zero vectors in other roles to exhibit a concrete +failure. The universal check had kept all roles independent; this choice of +one witness input imposes no clean-state assumption on the theorem. +For k=0 take dimension one and all G_a=I. + +This proves the converse in Section 1 and the constructive dimension bound. +The literal matrix oracle computes inverses by Gaussian elimination and +executes the original instructions; it does not reuse T_a or the producer. + +## 6. Boundaries and discriminating examples + +The dirty-sandwich example has roles x,h,y, all arbitrary. It temporarily +changes h to h+A x, adds B h to y, restores h, and subtracts B h. Its complete +endpoint is (x,h,y+B A x). The reference program temporarily applies A to x, +queries B x into y, and applies A^(-1) to x. Both full endpoints agree. +Deleting any one of the eight left-side instructions yields a detectable +failure in each tested field. This example certifies the stated algebraic +boundary; it is not a proposed faster physical implementation or a new echo +construction. + +A false commutator identity B^(-1)A^(-1)BA=I has a nonzero degree-two +coefficient. Scalar/one-dimensional substitutions cannot reveal that error; +the certificate's unipotent witness does. Self-source queries, omitted helper +returns and wrong inverse signs have distinct rejecting fixtures. + +The family G^(-1)(I-G)^d expands to (-Y)^d/(1+Y), so its first coefficient +occurs at degree d and its tail continues indefinitely. The replay checks +coefficients beyond the program's number of unary occurrences. In F_p, +G^p-I=Y^p supplies a characteristic-sensitive delayed witness. + +The stress example computes (A+B)^64 x, which has 2^64 distinct noncommutative +words, on both sides, and inserts a C^(-1),C cancellation on one side. +The complete two-role comparison uses D=260 states and no expanded words. +The helper is explicitly overwritten on both sides in this stress program; +the separate dirty-sandwich example tests actual helper restoration. + +For a termwise tensor substitution choose the new generators G_a^(tensor f) +and their actual inverses. The theorem then applies at the enlarged payload +dimension. Scalar coefficients stay scalar; no tensor power of a sum or of +the whole register-role matrix is taken. This is only an algebraic interface +lemma. Native realizations, phases, rounding, rectangular typing, precision, +stock, hosting, fixed-tape cost, complete paid invoices and supplier admission +are not proved here. No selected frontier or kappa changes. + +Prepared by Krzysztof Wójt with substantial OpenAI Codex assistance. Apache-2.0. diff --git a/research/inverse-dirty-certificates/README.md b/research/inverse-dirty-certificates/README.md new file mode 100644 index 0000000000..1f895da660 --- /dev/null +++ b/research/inverse-dirty-certificates/README.md @@ -0,0 +1,151 @@ +# Compact certificates for dirty circuits with actual inverse calls + +A name such as `A_inverse` is an independent symbol unless the verifier +implements its relation to `A`. This package closes that specific gap in +[zxv's PR5235](https://github.com/CrocSwap/integer-mult-bounds/pull/5235), exact +head `48976daa4dce59b4867ef046da72a370e389925d`. + +For two linear register programs with r independent input roles and q total +unary occurrences, **D=r+q states** suffice to certify equality of **every +returned role** under all invertible operator substitutions and all payload +dimensions. Forward and inverse occurrences share the same generator. A failed +identity yields explicit unipotent matrices and an input in dimension at most +D. No expansion of reduced words or infinite series is needed. + +The [written proof](PROOF.md) constructs a finite feedback realization at +`G=I+Y`, proves the passage to arbitrary invertible matrices using a central +indeterminate, and gives sound/complete closure certificates. These are a new +repository interface and implementation of classical rational-series ideas, +not a new general weighted-automata or Magnus theorem. This is author-checked +scoped algebra, not supplier admission or a new kappa. + +## Interface and use + +Programs are JSON with `field: 0` for Q or a prime p <= 2^31-1 for F_p, an +ordered list of `roles`, named `operators`, and `left`/`right` instruction lists. +Every role starts as a separate arbitrary vector and every role is compared at +exit. Scalar coefficients are integers or exact fraction strings; denominators +must be invertible in the selected field. See the three [examples](examples). + +| Instruction | Exact semantics | +|---|---| +| `linear`, `dst`, `terms: [[role,c], ...]` | Replace dst by the scalar sum, reading all old values. | +| `apply`, `dst`, `operator`, `direction: 1` or `-1` | Apply G or its actual inverse to dst. | +| `query`, `dst`, `src`, `operator`, `direction`, `coefficient` | Add c G^direction(src) to dst, reading the old source even when src=dst. | + +The [dirty-sandwich example](examples/dirty-sandwich.json) compares two complete +programs with endpoint `(x,h,y+B A x)` and restores arbitrary dirty h. The +[wrong-order example](examples/wrong-order.json) produces a three-dimensional +counterexample; its [literal matrices and input](examples/wrong-order.witness.json) +make the noncommutation failure directly inspectable. The +[binary inverse-tail example](examples/binary-inverse-tail.json) needs a +degree-five coefficient and has a genuinely infinite formal tail. + +Generate and check a certificate from the repository root: + +```sh +python3.12 -B research/inverse-dirty-certificates/certify.py \ + research/inverse-dirty-certificates/examples/dirty-sandwich.json \ + --output /tmp/dirty-sandwich-certificate.json +python3.12 -B research/inverse-dirty-certificates/check_certificate.py \ + research/inverse-dirty-certificates/examples/dirty-sandwich.json \ + /tmp/dirty-sandwich-certificate.json +``` + +For a false identity, `certify.py` also accepts `--witness /tmp/witness.json`, +which writes the actual invertible matrices, all initial role vectors and the +endpoint discrepancy. A valid negative certificate is successfully checked +with verdict `different`; CLI exit success means valid evidence, not equality. + +`check_certificate.py` imports neither `algebra.py` nor the producer. It +reconstructs the feedback equations separately and performs no elimination or +search. It shares only strict syntax and exact field arithmetic. The literal +free-group and matrix oracles are a separate implementation in `oracles.py`. +All were prepared in the same assisted research session; this is not an +independent scientific review claim. + +## Evidence and scope + +The deterministic replay checks: + +- 504 signed-word cancellation/deletion cases over Q, F2 and F5; +- 160 scalar/apply/query differential programs against literal reduced words; +- 64 dirty-boundary, order, self-source and characteristic controls; +- 36 delayed/infinite-tail cases, including positive-characteristic witnesses; +- 324 literal invertible-matrix substitutions of the full dirty boundary; +- 16 malformed/false certificate rejections and 15 invalid-program rejections; +- three committed example certificates and two explicit matrix witnesses. + +The `(A+B)^64` stress endpoint contains **2^64 distinct words** before +comparison. Its inverse-aware certificate uses **260 states and 64 invariant +rows**. It overwrites a helper identically on both sides; actual dirty-helper +restoration is checked separately. This is a compact-representation example, +not a claim about performance on every existing supplier. + +The proof permits arbitrary fields. This executable supports Q and prime +fields only. Inverse calls are exact square linear operations. Extra operator +relations, rectangular types, nonlinear or rounded leaves, native realization, +phase conventions, precision, stock, hosting, tapes and the complete paid/outer +bill remain outside scope. A negative result for independently invertible +generators may disappear under additional relations. The checker does not +certify shortestness of a failure word or a minimum matrix dimension. + +Normal and optimized registered replays, source/history checks and the +Git-free export are recorded in [VALIDATION.json](VALIDATION.json). Finite tests +corroborate the universal written proof; no Lean or independent human review is +claimed. No selected record or predecessor source is changed. + +## Reproduce + +Python 3.12, standard library only. From the repository root: + +```sh +python3.12 -B scripts/research_package.py --package research/inverse-dirty-certificates --check-only +python3.12 scripts/research_package.py --package research/inverse-dirty-certificates +python3.12 -W error -B research/inverse-dirty-certificates/verify.py +python3.12 -W error -O -B research/inverse-dirty-certificates/verify.py +``` + +One direct replay took about 16 seconds on the recorded host. Default replay +does not write package files. `--write-examples` is an explicit regeneration +mode; `--quick` is a development smoke test and is not the registered replay. +The direct verifier is standalone and works in a Git-free package export. +The registered runner additionally validates the pinned Git provenance. + +## Open next questions + +1. Bind one existing inverse-bearing native word to this grammar while + preserving every input and returned helper. Compare against its existing + reduced-word oracle at an exact source head. The remaining blocker is the + adapter's source/type/phase contract; this package does not infer it. +2. Add one other explicitly named relation model, such as commuting pairs. + Start with a normalization theorem and a noncommuting rejection fixture. + Quotienting the present transition matrices without a new proof is unsound. +3. Reduce checker path recomputation on a larger real adapter. Compare identical + closure equations and complete endpoints before changing representation; + exact rational coefficient growth remains an unmeasured scaling constraint. + +These are released questions, not claims on further work. Details and the scope +change from the generic formal-interface card are in [TASK.json](TASK.json). + +## Credit + +Prepared by **Krzysztof Wójt (@krzysztofwojt)** with substantial **OpenAI Codex +assistance**, including a separately delegated exact-oracle implementation. +Apache-2.0. Classical sources are cited in [PROOF.md](PROOF.md). + +Credit **zxv's PR5235** for the compact independent-operator register bridge, +invariant certificates, unipotent witnesses and the explicit inverse-frontend +question. Its dirty-echo lineage (**androolloyd**, **Chafik Boukhalfa/chafreaky +#628**, **Ali Romman #621**), **Cinna Davis #4100/#4088**, **ToikY**'s free-word +tensor audit, **Sagar Thakrar #3687**, **roger-sato #3693**, and the dirty-phase +audit following **Charles Bethin #1278** retain their results and attribution. +No predecessor source code or archived artifact is copied or modified. + +The fresh main base is `ff3cc58e370d0f678e529246f8c73e8094e18fcf`, priority +revision 7. [SOURCES.json](SOURCES.json) distinguishes ancestor provenance from +the contextual pending predecessor, which is not a replay dependency. +The [canonical claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/5236#discussioncomment-19147346) +records live overlap and status. The checked corpus and targeted searches are +evidence of due diligence, not coverage of unpublished work or arbitrary +historical diffs. diff --git a/research/inverse-dirty-certificates/SOURCES.json b/research/inverse-dirty-certificates/SOURCES.json new file mode 100644 index 0000000000..1d06ebac6c --- /dev/null +++ b/research/inverse-dirty-certificates/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "contextual_predecessors": [ + { + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5235", + "author": "zxv, with substantial OpenAI Codex assistance", + "head": "48976daa4dce59b4867ef046da72a370e389925d", + "scope": "Independent-operator compact certificates and the explicit open inverse-frontend question; context only, no source code copied and no replay import.", + "readme_path": "research/universal-dirty-certificates/README.md", + "readme_sha256": "fb8d94a58b6c0448aa893e65f263b9d71639b1aa79cd10f054d0dc740a570dca", + "proof_path": "research/universal-dirty-certificates/PROOF.md", + "proof_sha256": "ef4cfcfd65b1dde1f11eedace0ed90a1b47a2cc100daaf778fbecbff3ec685a7" + } + ], + "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" + } + ] +} diff --git a/research/inverse-dirty-certificates/TASK.json b/research/inverse-dirty-certificates/TASK.json new file mode 100644 index 0000000000..07ffb0c668 --- /dev/null +++ b/research/inverse-dirty-certificates/TASK.json @@ -0,0 +1,107 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 7, + "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "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": "Construct and prove a compact r+q-state inverse-aware frontend for complete dirty linear register programs, with exact closure certificates and finite invertible counterexamples.", + "scope_change_reason": "Take the explicitly open inverse-relation frontend in PR5235/Discussion5236 instead of a generic formalization or the picker suggested recursive-interface cards. Supply a normalization theorem and executable bridge; no Lean or endpoint arithmetic audit is claimed.", + "bottleneck_link": "The independent-symbol frontend cannot certify identities requiring an operator and its actual inverse. A sound compact inverse-aware bridge removes this algebraic certification gap without expanding reduced words; actual native adapters and physical invoices remain separate.", + "budget_minutes": 240, + "stop_rule": "Stop at the first proved and corroborated inverse-aware interface or a precise obstruction; do not expand to commutation/Clifford models, supplier optimization or a new kappa. At most 240 minutes including publication.", + "outcome": "completed", + "evidence": "PROOF.md supplies the universal all-dimension argument. verify.py checks two feedback compilers, exact literal reduced-word and matrix oracles, complete dirty boundaries, infinite tails, certificate/syntax rejection controls and a 2^64-word stress endpoint. VALIDATION.json records replays and publication checks.", + "author": "Krzysztof Wójt", + "ai_assistance": "Substantial OpenAI Codex assistance for mathematical development, implementation, testing and writing. A Luna worker separately implemented the bounded literal group-word and matrix test oracles. Same-session checks are not independent human or proof-kernel review.", + "open_questions": [ + { + "question": "Can an actual inverse-bearing native word be bound literally to this complete-register grammar?", + "why_it_matters": "A source-bound adapter could make the compact certificate useful to an existing supplier audit.", + "first_step": "Choose one exact source head, retain every dirty input and returned helper, and compare against its existing reduced-word oracle.", + "blocked_by": "Source transcription, common square payload typing, and the native operator/phase contract are not inferred by this frontend." + }, + { + "question": "Can one named extra relation model such as commuting pairs receive a sound compact frontend?", + "why_it_matters": "An independent-invertible failure may disappear under extra native relations.", + "first_step": "Prove a normalization theorem and test a noncommuting rejection fixture before quotienting any state transitions.", + "blocked_by": "The inverse-only rational-series argument does not establish other relations." + }, + { + "question": "Can checker path recomputation be reduced on a larger real adapter without changing the certificate equations?", + "why_it_matters": "The reference checker is polynomial but repeated paths and rational bit growth may dominate practical replay.", + "first_step": "Profile one pinned adapter and cache only source-bound path prefixes while comparing every closure equation.", + "blocked_by": "A representative large inverse-aware adapter and coefficient-growth measurements remain absent." + } + ] +} diff --git a/research/inverse-dirty-certificates/VALIDATION.json b/research/inverse-dirty-certificates/VALIDATION.json new file mode 100644 index 0000000000..ea049d2b93 --- /dev/null +++ b/research/inverse-dirty-certificates/VALIDATION.json @@ -0,0 +1,74 @@ +{ + "schema_version": 1, + "evidence_status": "author-checked scoped proof and finite exact corroboration", + "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "priority_revision": 7, + "environment": { + "python": "CPython 3.12.12", + "platform": "macOS 26.5.2 arm64", + "dependencies": "Python standard library only", + "representative_direct_replay_wall_seconds": 16.02 + }, + "replays": [ + { + "command": "python3.12 -W error -B research/inverse-dirty-certificates/verify.py", + "status": "PASS_INVERSE_DIRTY_CERTIFICATES" + }, + { + "command": "python3.12 -W error -O -B research/inverse-dirty-certificates/verify.py", + "status": "PASS_INVERSE_DIRTY_CERTIFICATES" + }, + { + "command": "python3.12 -B scripts/research_package.py --package research/inverse-dirty-certificates", + "status": "PASS_REGISTERED_RESEARCH_PACKAGE; both declared modes passed" + } + ], + "exact_counts": { + "inverse_word_cases": 504, + "differential_programs": {"total": 160, "equal": 88, "different": 72}, + "boundary_cases": 64, + "inverse_tail_cases": 36, + "literal_matrix_cases": 324, + "certificate_rejections": 16, + "syntax_rejections": 15, + "committed_program_certificate_pairs": 3, + "committed_explicit_matrix_witnesses": 2, + "stress": {"endpoint_words": "18446744073709551616", "states": 260, "invariant_rows": 64} + }, + "publication_checks": { + "status": "passed", + "committed_bytes": "PASS_RESEARCH_COMMIT_BYTES; all 21 package files", + "declared_source_history": "PASS; base ff3cc58e370d0f678e529246f8c73e8094e18fcf is an ancestor; pending PR5235 is contextual only, not a Git replay dependency", + "export_integrity": "PASS_RESEARCH_EXPORT; 21 regular files", + "export_replay": "Both normal and optimized direct replays pass with PATH=/nonexistent and read-only exported files; all 21 payload hashes unchanged", + "cli_control": "wrong-order certificate and literal matrix witness regenerate through the command-line producer, and the separate checker verifies the negative certificate", + "scope": "Source availability and byte transport are separate from the written mathematical proof. No hosted or independent scientific acceptance is inferred." + }, + "overlap": { + "preclaim": { + "open_prs": 317, + "discussion_records": 4503, + "local_notes": 7091, + "complete_remote_pagination": true, + "discussion_snapshot_utc": "2026-10-23T14:06:48Z" + }, + "presubmission": { + "open_prs": 323, + "discussion_records": 4526, + "local_head_notes": 7091, + "complete_remote_pagination": true, + "discussion_snapshot_utc": "2026-10-23T14:34:13Z", + "canonical_main_unchanged": true, + "predecessor_head_unchanged": true + }, + "scope": "Live PR bodies/claims and all-main package notes plus targeted historical PR searches; no claim of unpublished-work or arbitrary-diff coverage. Donor-excluded topics and recent account claims were excluded." + }, + "limitations": [ + "The universal theorem is a written proof, not inferred from the finite tests.", + "The independently transcribed compiler/checker and delegated exact oracles were prepared in the same assisted session; no independent human or proof-kernel review.", + "Only named-generator inverse relations; other algebraic relations may invalidate a negative witness for a more constrained model.", + "No actual native supplier adapter, phase/rounding/type proof, precision/stock/tape/hosting budget, new kappa or selected-frontier change.", + "The checker certifies a nonzero coefficient, not shortestness or minimum arbitrary matrix dimension.", + "Polynomial field-operation bounds do not bound rational coefficient bit growth." + ] +} diff --git a/research/inverse-dirty-certificates/VERIFY.json b/research/inverse-dirty-certificates/VERIFY.json new file mode 100644 index 0000000000..f9b7579ad2 --- /dev/null +++ b/research/inverse-dirty-certificates/VERIFY.json @@ -0,0 +1,25 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact inverse-aware feedback certificates, literal reduced-word and matrix oracles, complete dirty boundaries, infinite tails, rejecting controls and 2^64-word stress." + }, + { + "argv": ["{python}", "-W", "error", "-O", "-B", "{package}/verify.py"], + "timeout_seconds": 120, + "checks": "The same complete replay with assertions disabled." + } + ] +} diff --git a/research/inverse-dirty-certificates/algebra.py b/research/inverse-dirty-certificates/algebra.py new file mode 100644 index 0000000000..a9e9c8d6f1 --- /dev/null +++ b/research/inverse-dirty-certificates/algebra.py @@ -0,0 +1,153 @@ +"""Compact feedback realization and exact reachable-space search. + +This is the producer implementation; check_certificate.py does not import it. +Prepared for Krzysztof Wójt with OpenAI Codex assistance. Apache-2.0. +""" + +from collections import deque + +from syntax import fingerprint, validate + + +def add_scaled(dst, src, scalar, field): + if scalar: + for j, value in enumerate(src): + if value: + dst[j] = field.add(dst[j], field.mul(scalar, value)) + + +def row_times(row, matrix, field): + result = [field.zero] * len(matrix[0]) + for scalar, source in zip(row, matrix): + add_scaled(result, source, scalar, field) + return result + + +def compile_program(program): + """Return U,T,V with coefficients U T_word V after G=I+Y. + + Both sides share the original leaf atoms. Each unary occurrence creates + exactly one further atom, including inverse and zero-coefficient queries. + """ + f = validate(program) + roles = program["roles"] + r = len(roles) + q = sum(ins["op"] != "linear" for side in ("left", "right") for ins in program[side]) + d = r + q + atoms = [] + finals = [] + for side in ("left", "right"): + regs = {name: [f.one if j == i else f.zero for j in range(d)] + for i, name in enumerate(roles)} + for ins in program[side]: + dst = ins["dst"] + if ins["op"] == "linear": + result = [f.zero] * d + for name, coefficient in ins["terms"]: + add_scaled(result, regs[name], f.parse(coefficient), f) + regs[dst] = result + continue + source = dst if ins["op"] == "apply" else ins["src"] + dependency = regs[source][:] + j = r + len(atoms) + atoms.append((ins["operator"], ins["direction"], dependency)) + if ins["op"] == "apply": + regs[dst] = [f.one if k == j else f.zero for k in range(d)] + else: + result = regs[dst][:] + result[j] = f.add(result[j], f.parse(ins["coefficient"])) + regs[dst] = result + finals.append([regs[name] for name in roles]) + u = [[f.sub(x, y) for x, y in zip(a, b)] for a, b in zip(*finals)] + v = [[f.one if i == j else f.zero for j in range(r)] for i in range(d)] + transitions = {a: [[f.zero] * d for _ in range(d)] for a in program["operators"]} + for j, (symbol, direction, dependency) in enumerate(atoms, r): + v[j] = row_times(dependency[:j], v[:j], f) + for a, matrix in transitions.items(): + matrix[j] = row_times(dependency[:j], matrix[:j], f) + if a == symbol: + if direction == 1: + add_scaled(matrix[j], dependency, f.one, f) + else: + matrix[j][j] = f.sub(matrix[j][j], f.one) + return {"field": f, "dimension": d, "U": u, "T": transitions, "V": v} + + +class ReachableBasis: + """Echelon rows with exact coordinates in the original path rows.""" + + def __init__(self, field): + self.field = field + self.rows = [] + self.echelon = [] + + def reduce(self, row): + f = self.field + residual = row[:] + coefficients = [f.zero] * len(self.rows) + for pivot, normalized, coordinates in self.echelon: + scalar = residual[pivot] + if scalar: + add_scaled(residual, normalized, f.neg(scalar), f) + add_scaled(coefficients, coordinates, scalar, f) + return residual, coefficients + + def append(self, row): + f = self.field + residual, removed = self.reduce(row) + pivot = next((j for j, x in enumerate(residual) if x), None) + if pivot is None: + return False + scale = residual[pivot] + normalized = [f.div(x, scale) for x in residual] + coordinates = [f.div(f.neg(x), scale) for x in removed] + [f.div(f.one, scale)] + self.rows.append(row[:]) + self.echelon.append((pivot, normalized, coordinates)) + return True + + def coordinates(self, row): + remainder, coefficients = self.reduce(row) + if any(remainder): + raise ValueError("row is outside the claimed span") + return coefficients + + +def produce(program): + model = compile_program(program) + f, u, t, v = (model[k] for k in ("field", "U", "T", "V")) + basis = ReachableBasis(f) + paths = [] + queue = deque() + for output, row in enumerate(u): + if basis.append(row): + path = {"output": output, "word": []} + paths.append(path) + queue.append((row, path)) + while queue: + row, path = queue.popleft() + projected = row_times(row, v, f) + if any(projected): + i = next(i for i, value in enumerate(projected) if value) + return { + "schema": "inverse-dirty-certificate/v1", + "program_sha256": fingerprint(program), + "verdict": "different", + "output": path["output"], "input": i, "word": path["word"], + "coefficient": f.dump(projected[i]), + } + for symbol, matrix in t.items(): + successor = row_times(row, matrix, f) + if basis.append(successor): + successor_path = {"output": path["output"], "word": path["word"] + [symbol]} + paths.append(successor_path) + queue.append((successor, successor_path)) + encode = lambda rows: [[f.dump(x) for x in row] for row in rows] + return { + "schema": "inverse-dirty-certificate/v1", + "program_sha256": fingerprint(program), + "verdict": "equal", + "paths": paths, + "initial": encode([basis.coordinates(row) for row in u]), + "closure": {a: encode([basis.coordinates(row_times(b, matrix, f)) + for b in basis.rows]) for a, matrix in t.items()}, + } diff --git a/research/inverse-dirty-certificates/certify.py b/research/inverse-dirty-certificates/certify.py new file mode 100644 index 0000000000..0c9ec8ed3b --- /dev/null +++ b/research/inverse-dirty-certificates/certify.py @@ -0,0 +1,51 @@ +"""Produce an exact inverse-aware certificate, without expanding group words. + +Prepared for Krzysztof Wójt with OpenAI Codex assistance. Apache-2.0. +""" + +import argparse +import json +from pathlib import Path + +from algebra import compile_program, produce +from fields import Field +from oracles import apply_witness, unipotent_operators + + +def explicit_witness(program, certificate): + if certificate["verdict"] != "different": + raise ValueError("an equal endpoint has no distinguishing witness") + f = Field(program["field"]) + word = certificate["word"] + n = len(word) + 1 + operators = unipotent_operators(program, word) + encode = lambda row: [f.dump(x) for x in row] + inputs = {role: encode([f.one if i == certificate["input"] and j == n-1 else f.zero + for j in range(n)]) for i, role in enumerate(program["roles"])} + differences = apply_witness(program, word, program["roles"][certificate["input"]]) + return {"schema": "inverse-dirty-witness/v1", "program_sha256": certificate["program_sha256"], + "field": program["field"], "dimension": n, + "operators": {a: [encode(row) for row in matrix] for a, matrix in operators.items()}, + "inputs": inputs, + "endpoint_difference": {role: encode(row) for role, row in zip(program["roles"], differences)}} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("program", type=Path) + parser.add_argument("--output", type=Path, required=True) + parser.add_argument("--witness", type=Path, help="also export literal matrices and inputs on failure") + args = parser.parse_args() + program = json.loads(args.program.read_text(encoding="utf-8")) + certificate = produce(program) + witness = explicit_witness(program, certificate) if args.witness else None + args.output.write_text(json.dumps(certificate, indent=2) + "\n", encoding="utf-8") + if args.witness: + args.witness.write_text(json.dumps(witness, indent=2) + "\n", encoding="utf-8") + print(json.dumps({"verdict": certificate["verdict"], + "states": compile_program(program)["dimension"], + "certificate": str(args.output)}, sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/inverse-dirty-certificates/check_certificate.py b/research/inverse-dirty-certificates/check_certificate.py new file mode 100644 index 0000000000..1117bf61f8 --- /dev/null +++ b/research/inverse-dirty-certificates/check_certificate.py @@ -0,0 +1,163 @@ +"""Check finite equations with a separate feedback compiler and no elimination. + +Imports only shared syntax/exact arithmetic, never the producer. A verified +failure word proves difference, not that its length is minimal. +Prepared for Krzysztof Wójt with OpenAI Codex assistance. Apache-2.0. +""" + +import argparse +import json +from pathlib import Path + +from syntax import exact_keys, fingerprint, validate + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def reconstruct(program): + """Build sparse constant/unary equations, then forward-solve I-E. + + This deliberately differs from the producer's per-row recurrence. + """ + f = validate(program) + roles, alphabet = program["roles"], program["operators"] + r = len(roles) + definitions = [None] * r + endpoints = [] + + def combine(pairs): + result = {} + for scalar, expression in pairs: + for j, value in expression.items(): + result[j] = f.add(result.get(j, f.zero), f.mul(scalar, value)) + if not result[j]: + del result[j] + return result + + for side in ("left", "right"): + registers = {name: {i: f.one} for i, name in enumerate(roles)} + for operation in program[side]: + destination = operation["dst"] + if operation["op"] == "linear": + registers[destination] = combine( + (f.parse(c), registers[name]) for name, c in operation["terms"]) + continue + source = operation.get("src", destination) + index = len(definitions) + definitions.append((registers[source].copy(), operation["operator"], operation["direction"])) + if operation["op"] == "apply": + registers[destination] = {index: f.one} + else: + registers[destination] = combine([ + (f.one, registers[destination]), + (f.parse(operation["coefficient"]), {index: f.one})]) + endpoints.append([registers[name] for name in roles]) + d = len(definitions) + # H = (I-E)^-1, obtained by an exact triangular solve; no matrix inverse. + h = [[f.one if i == j else f.zero for j in range(d)] for i in range(d)] + for i in range(r, d): + dependency, _, _ = definitions[i] + for j, coefficient in dependency.items(): + require(j < i, "noncausal constant dependency") + for k in range(d): + h[i][k] = f.add(h[i][k], f.mul(coefficient, h[j][k])) + transitions = {a: [[f.zero] * d for _ in range(d)] for a in alphabet} + for j in range(r, d): + dependency, a, sign = definitions[j] + unary = dependency if sign == 1 else {j: f.neg(f.one)} + for i in range(d): + if h[i][j]: + for k, coefficient in unary.items(): + transitions[a][i][k] = f.add(transitions[a][i][k], f.mul(h[i][j], coefficient)) + u = [] + for left, right in zip(*endpoints): + delta = combine([(f.one, left), (f.neg(f.one), right)]) + u.append([delta.get(j, f.zero) for j in range(d)]) + return f, u, transitions, [row[:r] for row in h] + + +def multiply(row, matrix, f, columns): + answer = [f.zero] * columns + for i, coefficient in enumerate(row): + if coefficient: + for j in range(columns): + if matrix[i][j]: + answer[j] = f.add(answer[j], f.mul(coefficient, matrix[i][j])) + return answer + + +def index(value, size): + require(type(value) is int and 0 <= value < size, "index outside declared boundary") + return value + + +def check(program, certificate): + f, u, t, v = reconstruct(program) + r, d = len(u), len(v) + require(isinstance(certificate, dict), "certificate must be an object") + require(certificate.get("schema") == "inverse-dirty-certificate/v1", "unknown certificate schema") + require(certificate.get("program_sha256") == fingerprint(program), "certificate belongs to another program") + + def path_row(output, word): + row = u[index(output, r)][:] + require(isinstance(word, list) and len(word) < d, "path exceeds the state bound") + for symbol in word: + require(isinstance(symbol, str) and symbol in t, "unknown path symbol") + row = multiply(row, t[symbol], f, d) + return row + + verdict = certificate.get("verdict") + common = {"schema", "program_sha256", "verdict"} + if verdict == "different": + exact_keys(certificate, common | {"output", "input", "word", "coefficient"}) + row = path_row(certificate["output"], certificate["word"]) + value = multiply(row, v, f, r)[index(certificate["input"], r)] + require(value != f.zero and value == f.parse(certificate["coefficient"]), "invalid distinguishing coefficient") + return {"verdict": "different", "states": d, "witness_dimension": len(certificate["word"]) + 1} + require(verdict == "equal", "unknown verdict") + exact_keys(certificate, common | {"paths", "initial", "closure"}) + paths = certificate["paths"] + require(isinstance(paths, list) and len(paths) <= d, "too many basis rows") + rows = [] + for path in paths: + exact_keys(path, {"output", "word"}) + rows.append(path_row(path["output"], path["word"])) + b = len(rows) + + def scalar_matrix(value, height, width): + require(isinstance(value, list) and len(value) == height, "coordinate matrix height") + result = [] + for row in value: + require(isinstance(row, list) and len(row) == width, "coordinate matrix width") + result.append([f.parse(x) for x in row]) + return result + + initial = scalar_matrix(certificate["initial"], r, b) + exact_keys(certificate["closure"], set(t)) + for i in range(r): + require(multiply(initial[i], rows, f, d) == u[i], "initial rows not in certified span") + for row in rows: + require(not any(multiply(row, v, f, r)), "basis row has a nonzero input projection") + for symbol, transition in t.items(): + coordinates = scalar_matrix(certificate["closure"][symbol], b, b) + for i, row in enumerate(rows): + require(multiply(row, transition, f, d) == multiply(coordinates[i], rows, f, d), + "span is not transition-closed") + return {"verdict": "equal", "states": d, "invariant_rows": b} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("program", type=Path) + parser.add_argument("certificate", type=Path) + args = parser.parse_args() + program = json.loads(args.program.read_text(encoding="utf-8")) + certificate = json.loads(args.certificate.read_text(encoding="utf-8")) + print(json.dumps(check(program, certificate), sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/inverse-dirty-certificates/examples/binary-inverse-tail.certificate.json b/research/inverse-dirty-certificates/examples/binary-inverse-tail.certificate.json new file mode 100644 index 0000000000..2528c71789 --- /dev/null +++ b/research/inverse-dirty-certificates/examples/binary-inverse-tail.certificate.json @@ -0,0 +1,15 @@ +{ + "schema": "inverse-dirty-certificate/v1", + "program_sha256": "3ace807cbdf906d90574b9eff5ab195cc2021106508000e5754fafcddcf2b304", + "verdict": "different", + "output": 0, + "input": 0, + "word": [ + "A", + "A", + "A", + "A", + "A" + ], + "coefficient": "1" +} diff --git a/research/inverse-dirty-certificates/examples/binary-inverse-tail.json b/research/inverse-dirty-certificates/examples/binary-inverse-tail.json new file mode 100644 index 0000000000..66f88463bd --- /dev/null +++ b/research/inverse-dirty-certificates/examples/binary-inverse-tail.json @@ -0,0 +1,65 @@ +{ + "schema": "inverse-dirty-program/v1", + "field": 2, + "roles": [ + "x" + ], + "operators": [ + "A" + ], + "left": [ + { + "op": "query", + "dst": "x", + "src": "x", + "operator": "A", + "direction": 1, + "coefficient": -1 + }, + { + "op": "query", + "dst": "x", + "src": "x", + "operator": "A", + "direction": 1, + "coefficient": -1 + }, + { + "op": "query", + "dst": "x", + "src": "x", + "operator": "A", + "direction": 1, + "coefficient": -1 + }, + { + "op": "query", + "dst": "x", + "src": "x", + "operator": "A", + "direction": 1, + "coefficient": -1 + }, + { + "op": "query", + "dst": "x", + "src": "x", + "operator": "A", + "direction": 1, + "coefficient": -1 + }, + { + "op": "apply", + "dst": "x", + "operator": "A", + "direction": -1 + } + ], + "right": [ + { + "op": "linear", + "dst": "x", + "terms": [] + } + ] +} diff --git a/research/inverse-dirty-certificates/examples/binary-inverse-tail.witness.json b/research/inverse-dirty-certificates/examples/binary-inverse-tail.witness.json new file mode 100644 index 0000000000..b4c1c7ec48 --- /dev/null +++ b/research/inverse-dirty-certificates/examples/binary-inverse-tail.witness.json @@ -0,0 +1,78 @@ +{ + "schema": "inverse-dirty-witness/v1", + "program_sha256": "3ace807cbdf906d90574b9eff5ab195cc2021106508000e5754fafcddcf2b304", + "field": 2, + "dimension": 6, + "operators": { + "A": [ + [ + "1", + "1", + "0", + "0", + "0", + "0" + ], + [ + "0", + "1", + "1", + "0", + "0", + "0" + ], + [ + "0", + "0", + "1", + "1", + "0", + "0" + ], + [ + "0", + "0", + "0", + "1", + "1", + "0" + ], + [ + "0", + "0", + "0", + "0", + "1", + "1" + ], + [ + "0", + "0", + "0", + "0", + "0", + "1" + ] + ] + }, + "inputs": { + "x": [ + "0", + "0", + "0", + "0", + "0", + "1" + ] + }, + "endpoint_difference": { + "x": [ + "1", + "0", + "0", + "0", + "0", + "0" + ] + } +} diff --git a/research/inverse-dirty-certificates/examples/dirty-sandwich.certificate.json b/research/inverse-dirty-certificates/examples/dirty-sandwich.certificate.json new file mode 100644 index 0000000000..3024407195 --- /dev/null +++ b/research/inverse-dirty-certificates/examples/dirty-sandwich.certificate.json @@ -0,0 +1,99 @@ +{ + "schema": "inverse-dirty-certificate/v1", + "program_sha256": "611458abc84b59b9db9f54a2c8b912fe035af629a5026d43fa63bc55145cc06c", + "verdict": "equal", + "paths": [ + { + "output": 0, + "word": [] + }, + { + "output": 1, + "word": [] + }, + { + "output": 2, + "word": [] + }, + { + "output": 2, + "word": [ + "B" + ] + } + ], + "initial": [ + [ + "1", + "0", + "0", + "0" + ], + [ + "0", + "1", + "0", + "0" + ], + [ + "0", + "0", + "1", + "0" + ] + ], + "closure": { + "A": [ + [ + "-1", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0" + ] + ], + "B": [ + [ + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "1" + ], + [ + "0", + "0", + "0", + "0" + ] + ] + } +} diff --git a/research/inverse-dirty-certificates/examples/dirty-sandwich.json b/research/inverse-dirty-certificates/examples/dirty-sandwich.json new file mode 100644 index 0000000000..c1254508e7 --- /dev/null +++ b/research/inverse-dirty-certificates/examples/dirty-sandwich.json @@ -0,0 +1,105 @@ +{ + "schema": "inverse-dirty-program/v1", + "field": 0, + "roles": [ + "x", + "h", + "y" + ], + "operators": [ + "A", + "B" + ], + "left": [ + { + "op": "apply", + "dst": "h", + "operator": "A", + "direction": -1 + }, + { + "op": "linear", + "dst": "h", + "terms": [ + [ + "h", + 1 + ], + [ + "x", + 1 + ] + ] + }, + { + "op": "apply", + "dst": "h", + "operator": "A", + "direction": 1 + }, + { + "op": "query", + "dst": "y", + "src": "h", + "operator": "B", + "direction": 1, + "coefficient": 1 + }, + { + "op": "apply", + "dst": "h", + "operator": "A", + "direction": -1 + }, + { + "op": "linear", + "dst": "h", + "terms": [ + [ + "h", + 1 + ], + [ + "x", + -1 + ] + ] + }, + { + "op": "apply", + "dst": "h", + "operator": "A", + "direction": 1 + }, + { + "op": "query", + "dst": "y", + "src": "h", + "operator": "B", + "direction": 1, + "coefficient": -1 + } + ], + "right": [ + { + "op": "apply", + "dst": "x", + "operator": "A", + "direction": 1 + }, + { + "op": "query", + "dst": "y", + "src": "x", + "operator": "B", + "direction": 1, + "coefficient": 1 + }, + { + "op": "apply", + "dst": "x", + "operator": "A", + "direction": -1 + } + ] +} diff --git a/research/inverse-dirty-certificates/examples/wrong-order.certificate.json b/research/inverse-dirty-certificates/examples/wrong-order.certificate.json new file mode 100644 index 0000000000..0c5d8fd52d --- /dev/null +++ b/research/inverse-dirty-certificates/examples/wrong-order.certificate.json @@ -0,0 +1,12 @@ +{ + "schema": "inverse-dirty-certificate/v1", + "program_sha256": "8b51b293d203b16cdea4b90ebebb4b12ad41d3a072615d9e0ed266ba492107e5", + "verdict": "different", + "output": 0, + "input": 0, + "word": [ + "A", + "B" + ], + "coefficient": "-1" +} diff --git a/research/inverse-dirty-certificates/examples/wrong-order.json b/research/inverse-dirty-certificates/examples/wrong-order.json new file mode 100644 index 0000000000..3beca6f4b1 --- /dev/null +++ b/research/inverse-dirty-certificates/examples/wrong-order.json @@ -0,0 +1,38 @@ +{ + "schema": "inverse-dirty-program/v1", + "field": 0, + "roles": [ + "x" + ], + "operators": [ + "A", + "B" + ], + "left": [ + { + "op": "apply", + "dst": "x", + "operator": "A", + "direction": 1 + }, + { + "op": "apply", + "dst": "x", + "operator": "B", + "direction": 1 + }, + { + "op": "apply", + "dst": "x", + "operator": "A", + "direction": -1 + }, + { + "op": "apply", + "dst": "x", + "operator": "B", + "direction": -1 + } + ], + "right": [] +} diff --git a/research/inverse-dirty-certificates/examples/wrong-order.witness.json b/research/inverse-dirty-certificates/examples/wrong-order.witness.json new file mode 100644 index 0000000000..55ee5acdca --- /dev/null +++ b/research/inverse-dirty-certificates/examples/wrong-order.witness.json @@ -0,0 +1,56 @@ +{ + "schema": "inverse-dirty-witness/v1", + "program_sha256": "8b51b293d203b16cdea4b90ebebb4b12ad41d3a072615d9e0ed266ba492107e5", + "field": 0, + "dimension": 3, + "operators": { + "A": [ + [ + "1", + "1", + "0" + ], + [ + "0", + "1", + "0" + ], + [ + "0", + "0", + "1" + ] + ], + "B": [ + [ + "1", + "0", + "0" + ], + [ + "0", + "1", + "1" + ], + [ + "0", + "0", + "1" + ] + ] + }, + "inputs": { + "x": [ + "0", + "0", + "1" + ] + }, + "endpoint_difference": { + "x": [ + "-1", + "0", + "0" + ] + } +} diff --git a/research/inverse-dirty-certificates/fields.py b/research/inverse-dirty-certificates/fields.py new file mode 100644 index 0000000000..2442625a15 --- /dev/null +++ b/research/inverse-dirty-certificates/fields.py @@ -0,0 +1,67 @@ +"""Exact Q / prime-field arithmetic shared by the two implementations. + +Prepared for Krzysztof Wójt with OpenAI Codex assistance. Apache-2.0. +""" + +from fractions import Fraction +from functools import lru_cache +from math import isqrt + + +@lru_cache(maxsize=64) +def prime(p): + if p < 2 or p > 2**31 - 1: + return False + if p % 2 == 0: + return p == 2 + return all(p % d for d in range(3, isqrt(p) + 1, 2)) + + +class Field: + def __init__(self, characteristic=0): + if type(characteristic) is not int or ( + characteristic != 0 and not prime(characteristic) + ): + raise ValueError("field must be 0 (Q) or a prime at most 2^31-1") + self.characteristic = characteristic + self.zero = 0 if characteristic else Fraction(0) + self.one = 1 if characteristic else Fraction(1) + + def parse(self, value): + if type(value) not in (int, str, Fraction): + raise ValueError("scalar must be an integer or an exact fraction string") + try: + value = Fraction(value) + except (ValueError, ZeroDivisionError) as error: + raise ValueError("invalid exact scalar") from error + p = self.characteristic + if not p: + return value + if value.denominator % p == 0: + raise ValueError("scalar denominator is zero in the field") + return value.numerator * pow(value.denominator, -1, p) % p + + def add(self, x, y): + return (x + y) % self.characteristic if self.characteristic else x + y + + def sub(self, x, y): + return (x - y) % self.characteristic if self.characteristic else x - y + + def mul(self, x, y): + return (x * y) % self.characteristic if self.characteristic else x * y + + def neg(self, x): + return -x % self.characteristic if self.characteristic else -x + + def div(self, x, y): + if not y: + raise ValueError("division by zero") + if self.characteristic: + return x * pow(y, -1, self.characteristic) % self.characteristic + return x / y + + def dump(self, x): + return str(x) + + def is_zero(self, x): + return x == 0 diff --git a/research/inverse-dirty-certificates/oracles.py b/research/inverse-dirty-certificates/oracles.py new file mode 100644 index 0000000000..ad52010688 --- /dev/null +++ b/research/inverse-dirty-certificates/oracles.py @@ -0,0 +1,390 @@ +"""Independent exact endpoint oracles for inverse-dirty register programs. + +The free-group oracle expands operator words literally and is limited by its +support cap. The matrix oracle checks one supplied finite-dimensional operator +assignment; neither oracle compiles or validates certificates. Witness vectors +corroborate an endpoint calculation and do not establish shortestness. + +Prepared for Krzysztof Wójt with OpenAI Codex assistance. Apache-2.0. +""" + +from __future__ import annotations + +from typing import Any + +try: + from .fields import Field +except ImportError: # Also support running sibling research scripts directly. + from fields import Field + + +WordKey = tuple[int, tuple[int, ...]] + + +def _field(program: dict[str, Any]) -> Field: + return Field(program["field"]) + + +def _prepend(symbol: int, word: tuple[int, ...]) -> tuple[int, ...]: + """Prepend a newly applied generator and reduce the free-group word.""" + if word and word[0] == -symbol: + return word[1:] + return (symbol,) + word + + +def _add_word_term( + target: dict[WordKey, Any], + key: WordKey, + value: Any, + field: Field, +) -> None: + total = field.add(target.get(key, field.zero), value) + if field.is_zero(total): + target.pop(key, None) + else: + target[key] = total + + +def _word_endpoint_side( + program: dict[str, Any], instructions: list[dict[str, Any]], field: Field, support_cap: int +) -> list[dict[WordKey, Any]]: + roles = program["roles"] + operators = {name: index for index, name in enumerate(program["operators"], start=1)} + registers: list[dict[WordKey, Any]] = [ + {(index, ()): field.one} for index in range(len(roles)) + ] + role_index = {role: index for index, role in enumerate(roles)} + + def check_support() -> None: + count = sum(len(register) for register in registers) + if count > support_cap: + raise ValueError( + f"literal free-group support {count} exceeds support_cap={support_cap}" + ) + + check_support() + for instruction in instructions: + op = instruction["op"] + dst = role_index[instruction["dst"]] + if op == "linear": + updated: dict[WordKey, Any] = {} + for source_role, raw_coefficient in instruction["terms"]: + coefficient = field.parse(raw_coefficient) + for key, value in registers[role_index[source_role]].items(): + _add_word_term( + updated, key, field.mul(coefficient, value), field + ) + registers[dst] = updated + elif op == "apply": + symbol = operators[instruction["operator"]] * instruction["direction"] + updated = {} + for (input_index, word), value in registers[dst].items(): + updated[(input_index, _prepend(symbol, word))] = value + registers[dst] = updated + elif op == "query": + source = role_index[instruction["src"]] + symbol = operators[instruction["operator"]] * instruction["direction"] + coefficient = field.parse(instruction["coefficient"]) + updated = dict(registers[dst]) + for (input_index, word), value in registers[source].items(): + key = (input_index, _prepend(symbol, word)) + _add_word_term( + updated, key, field.mul(coefficient, value), field + ) + registers[dst] = updated + else: # The input contract says programs are already validated. + raise ValueError(f"unknown instruction op {op!r}") + check_support() + return registers + + +def reduced_word_endpoint( + program: dict[str, Any], support_cap: int = 100_000 +) -> list[dict[WordKey, Any]]: + """Return each left-minus-right role as an exact reduced free-group sum. + + Keys are ``(input_role_index, signed_generator_word)``. Generator indices + follow ``program["operators"]`` starting at 1. A positive symbol means the + named operator and a negative symbol its inverse. Every role starts as an + independent input register. Expansion is literal and raises ``ValueError`` + if the combined live support exceeds ``support_cap``. + """ + if support_cap < 0: + raise ValueError("support_cap must be nonnegative") + field = _field(program) + left = _word_endpoint_side(program, program["left"], field, support_cap) + right = _word_endpoint_side(program, program["right"], field, support_cap) + result: list[dict[WordKey, Any]] = [] + for left_role, right_role in zip(left, right): + difference = dict(left_role) + for key, value in right_role.items(): + _add_word_term(difference, key, field.neg(value), field) + result.append(difference) + if sum(len(register) for register in result) > support_cap: + raise ValueError( + f"literal free-group support exceeds support_cap={support_cap}" + ) + return result + + +def _parse_matrix(raw: list[list[Any]], field: Field, name: str) -> list[list[Any]]: + if not isinstance(raw, list) or any(not isinstance(row, list) for row in raw): + raise ValueError(f"operator {name!r} must be a square list matrix") + size = len(raw) + if any(len(row) != size for row in raw): + raise ValueError(f"operator {name!r} must be square") + return [[field.parse(value) for value in row] for row in raw] + + +def _inverse(matrix: list[list[Any]], field: Field) -> list[list[Any]]: + """Invert a square matrix by exact Gauss-Jordan elimination.""" + size = len(matrix) + augmented = [ + list(row) + + [field.one if row_index == column else field.zero for column in range(size)] + for row_index, row in enumerate(matrix) + ] + width = 2 * size + for column in range(size): + pivot = next( + (row for row in range(column, size) if not field.is_zero(augmented[row][column])), + None, + ) + if pivot is None: + raise ValueError("operator matrix is singular and cannot be inverted") + if pivot != column: + augmented[column], augmented[pivot] = augmented[pivot], augmented[column] + pivot_value = augmented[column][column] + augmented[column] = [field.div(value, pivot_value) for value in augmented[column]] + for row in range(size): + if row == column: + continue + factor = augmented[row][column] + if field.is_zero(factor): + continue + augmented[row] = [ + field.sub(augmented[row][entry], field.mul(factor, augmented[column][entry])) + for entry in range(width) + ] + return [row[size:] for row in augmented] + + +def _zero_matrix(size: int, field: Field) -> list[list[Any]]: + return [[field.zero for _ in range(size)] for _ in range(size)] + + +def _matrix_add_scaled( + left: list[list[Any]], right: list[list[Any]], coefficient: Any, field: Field +) -> list[list[Any]]: + return [ + [field.add(a, field.mul(coefficient, b)) for a, b in zip(left_row, right_row)] + for left_row, right_row in zip(left, right) + ] + + +def _matrix_scale( + matrix: list[list[Any]], coefficient: Any, field: Field +) -> list[list[Any]]: + return [[field.mul(coefficient, value) for value in row] for row in matrix] + + +def _matrix_multiply( + left: list[list[Any]], right: list[list[Any]], field: Field +) -> list[list[Any]]: + size = len(left) + return [ + [ + _dot(left[row], [right[index][column] for index in range(size)], field) + for column in range(size) + ] + for row in range(size) + ] + + +def _dot(left: list[Any], right: list[Any], field: Field) -> Any: + total = field.zero + for a, b in zip(left, right): + total = field.add(total, field.mul(a, b)) + return total + + +def _matrix_is_zero(matrix: list[list[Any]], field: Field) -> bool: + return all(field.is_zero(value) for row in matrix for value in row) + + +def _literal_endpoint_side( + program: dict[str, Any], + instructions: list[dict[str, Any]], + matrices: dict[str, list[list[Any]]], + inverse_cache: dict[str, list[list[Any]]], + size: int, + field: Field, +) -> list[dict[int, list[list[Any]]]]: + roles = program["roles"] + role_index = {role: index for index, role in enumerate(roles)} + identity = [ + [field.one if row == column else field.zero for column in range(size)] + for row in range(size) + ] + registers: list[dict[int, list[list[Any]]]] = [ + {index: [row[:] for row in identity]} for index in range(len(roles)) + ] + + for instruction in instructions: + op = instruction["op"] + dst = role_index[instruction["dst"]] + if op == "linear": + updated: dict[int, list[list[Any]]] = {} + for source_role, raw_coefficient in instruction["terms"]: + coefficient = field.parse(raw_coefficient) + for input_index, block in registers[role_index[source_role]].items(): + total = _matrix_add_scaled( + updated.get(input_index, _zero_matrix(size, field)), + block, + coefficient, + field, + ) + if _matrix_is_zero(total, field): + updated.pop(input_index, None) + else: + updated[input_index] = total + registers[dst] = updated + elif op == "apply": + name = instruction["operator"] + if instruction["direction"] == 1: + operator_matrix = matrices[name] + else: + if name not in inverse_cache: + inverse_cache[name] = _inverse(matrices[name], field) + operator_matrix = inverse_cache[name] + registers[dst] = { + input_index: _matrix_multiply(operator_matrix, block, field) + for input_index, block in registers[dst].items() + } + elif op == "query": + name = instruction["operator"] + if instruction["direction"] == 1: + operator_matrix = matrices[name] + else: + if name not in inverse_cache: + inverse_cache[name] = _inverse(matrices[name], field) + operator_matrix = inverse_cache[name] + coefficient = field.parse(instruction["coefficient"]) + updated = dict(registers[dst]) + for input_index, block in registers[role_index[instruction["src"]]].items(): + transformed = _matrix_multiply(operator_matrix, block, field) + total = _matrix_add_scaled( + updated.get(input_index, _zero_matrix(size, field)), + transformed, + coefficient, + field, + ) + if _matrix_is_zero(total, field): + updated.pop(input_index, None) + else: + updated[input_index] = total + registers[dst] = updated + else: # The input contract says programs are already validated. + raise ValueError(f"unknown instruction op {op!r}") + return registers + + +def literal_endpoint( + program: dict[str, Any], operators: dict[str, list[list[Any]]] +) -> list[list[list[list[Any]]]]: + """Return all exact left-minus-right matrix blocks for one operator choice. + + The result is indexed ``[output_role][input_role][row][column]``. Missing + blocks are returned as full zero matrices. If the program has no operators + and ``operators`` is empty, the otherwise-undetermined matrix dimension is + taken to be 1. Inverses use exact Gauss-Jordan elimination over the program + field; singular matrices raise ``ValueError``. + """ + field = _field(program) + matrices = { + name: _parse_matrix(raw, field, name) for name, raw in operators.items() + } + named_operators = program["operators"] + missing = [name for name in named_operators if name not in matrices] + if missing: + raise ValueError(f"missing matrices for named operators: {missing!r}") + + dimensions = {len(matrix) for matrix in matrices.values()} + if len(dimensions) > 1: + raise ValueError("all operator matrices must have the same dimension") + size = next(iter(dimensions), 1) + inverse_cache: dict[str, list[list[Any]]] = {} + left = _literal_endpoint_side( + program, program["left"], matrices, inverse_cache, size, field + ) + right = _literal_endpoint_side( + program, program["right"], matrices, inverse_cache, size, field + ) + zero = _zero_matrix(size, field) + minus_one = field.neg(field.one) + result: list[list[list[list[Any]]]] = [] + for left_blocks, right_blocks in zip(left, right): + output: list[list[list[Any]]] = [] + for input_index in range(len(program["roles"])): + output.append( + _matrix_add_scaled( + left_blocks.get(input_index, zero), + right_blocks.get(input_index, zero), + minus_one, + field, + ) + ) + result.append(output) + return result + + +def unipotent_operators( + program: dict[str, Any], word: list[str] +) -> dict[str, list[list[Any]]]: + """Build the standard upper-shift unipotent assignment for ``word``.""" + field = _field(program) + names = program["operators"] + unknown = [name for name in word if name not in names] + if unknown: + raise ValueError(f"word contains operators absent from the program: {unknown!r}") + size = len(word) + 1 + result: dict[str, list[list[Any]]] = {} + for name in names: + matrix = [ + [field.one if row == column else field.zero for column in range(size)] + for row in range(size) + ] + for index, symbol in enumerate(word): + if symbol == name: + matrix[index][index + 1] = field.one + result[name] = matrix + return result + + +def apply_witness( + program: dict[str, Any], word: list[str], input_role: str +) -> list[list[Any]]: + """Apply the unipotent endpoint difference to ``e_last`` in one role. + + This is a concrete witness calculation for corroboration only; it does not + prove a shortest witness or a universal endpoint distinction. + """ + if input_role not in program["roles"]: + raise ValueError(f"unknown input role {input_role!r}") + operators = unipotent_operators(program, word) + endpoint = literal_endpoint(program, operators) + input_index = program["roles"].index(input_role) + last_column = len(word) + return [ + [endpoint[output_index][input_index][row][last_column] + for row in range(last_column + 1)] + for output_index in range(len(program["roles"])) + ] + + +__all__ = [ + "reduced_word_endpoint", + "literal_endpoint", + "unipotent_operators", + "apply_witness", +] diff --git a/research/inverse-dirty-certificates/syntax.py b/research/inverse-dirty-certificates/syntax.py new file mode 100644 index 0000000000..5a91dd1921 --- /dev/null +++ b/research/inverse-dirty-certificates/syntax.py @@ -0,0 +1,71 @@ +"""Strict syntax and byte-independent binding, not an algebraic compiler. + +Prepared for Krzysztof Wójt with OpenAI Codex assistance. Apache-2.0. +""" + +import hashlib +import json + +from fields import Field + + +def exact_keys(obj, keys): + if not isinstance(obj, dict) or set(obj) != set(keys): + raise ValueError(f"expected exactly these keys: {sorted(keys)}") + + +def names(values, nonempty=False): + if not isinstance(values, list) or (nonempty and not values): + raise ValueError("expected a list of names") + if any(not isinstance(x, str) or not x for x in values): + raise ValueError("names must be nonempty strings") + if len(set(values)) != len(values): + raise ValueError("duplicate name") + + +def validate(program): + exact_keys(program, {"schema", "field", "roles", "operators", "left", "right"}) + if program["schema"] != "inverse-dirty-program/v1": + raise ValueError("unknown program schema") + field = Field(program["field"]) + names(program["roles"], nonempty=True) + names(program["operators"]) + roles, operators = set(program["roles"]), set(program["operators"]) + for side in ("left", "right"): + if not isinstance(program[side], list): + raise ValueError("instruction sequence must be a list") + for ins in program[side]: + if not isinstance(ins, dict): + raise ValueError("instruction must be an object") + op = ins.get("op") + if op == "linear": + exact_keys(ins, {"op", "dst", "terms"}) + if not isinstance(ins["terms"], list): + raise ValueError("linear terms must be a list") + for term in ins["terms"]: + if not isinstance(term, list) or len(term) != 2 or term[0] not in roles: + raise ValueError("invalid linear term or undeclared source") + field.parse(term[1]) + elif op in ("apply", "query"): + keys = {"op", "dst", "operator", "direction"} + if op == "query": + keys |= {"src", "coefficient"} + exact_keys(ins, keys) + if ins["operator"] not in operators: + raise ValueError("undeclared operator") + if type(ins["direction"]) is not int or ins["direction"] not in (-1, 1): + raise ValueError("direction must be exactly +1 or -1") + if op == "query": + if ins["src"] not in roles: + raise ValueError("undeclared query source") + field.parse(ins["coefficient"]) + else: + raise ValueError("unknown instruction") + if ins["dst"] not in roles: + raise ValueError("undeclared destination") + return field + + +def fingerprint(program): + payload = json.dumps(program, sort_keys=True, separators=(",", ":"), ensure_ascii=True) + return hashlib.sha256(payload.encode("ascii")).hexdigest() diff --git a/research/inverse-dirty-certificates/verify.py b/research/inverse-dirty-certificates/verify.py new file mode 100644 index 0000000000..6cc68d45f8 --- /dev/null +++ b/research/inverse-dirty-certificates/verify.py @@ -0,0 +1,313 @@ +#!/usr/bin/env python3 +"""Exact bounded corroboration; the universal statement is in PROOF.md. + +Default replay is read-only. --write-examples regenerates committed examples. +Prepared for Krzysztof Wójt with OpenAI Codex assistance. Apache-2.0. +""" + +import argparse +from copy import deepcopy +from itertools import product +import json +from pathlib import Path +import random + +from algebra import compile_program, produce, row_times +from check_certificate import check, reconstruct +from certify import explicit_witness +from fields import Field +from oracles import apply_witness, literal_endpoint, reduced_word_endpoint +from syntax import fingerprint, validate + +HERE = Path(__file__).resolve().parent + + +def require(condition, message): + if not condition: + raise RuntimeError(message) + + +def expect_reject(function, label): + try: + function() + except (ValueError, TypeError, KeyError): + return + raise RuntimeError(f"negative control accepted: {label}") + + +def apply(dst, operator, direction=1): + return {"op": "apply", "dst": dst, "operator": operator, "direction": direction} + + +def query(dst, src, operator, direction=1, coefficient=1): + return {"op": "query", "dst": dst, "src": src, "operator": operator, + "direction": direction, "coefficient": coefficient} + + +def linear(dst, terms): + return {"op": "linear", "dst": dst, "terms": [[name, c] for name, c in terms]} + + +def program(left, right=(), roles=("x",), operators=("A", "B"), field=0): + return {"schema": "inverse-dirty-program/v1", "field": field, + "roles": list(roles), "operators": list(operators), + "left": list(left), "right": list(right)} + + +def dirty_sandwich(field=0): + # h is arbitrary dirty. Both programs finish at (x,h,y+B A x). + left = [apply("h", "A", -1), linear("h", [("h", 1), ("x", 1)]), + apply("h", "A"), query("y", "h", "B"), apply("h", "A", -1), + linear("h", [("h", 1), ("x", -1)]), apply("h", "A"), + query("y", "h", "B", coefficient=-1)] + right = [apply("x", "A"), query("y", "x", "B"), apply("x", "A", -1)] + return program(left, right, roles=("x", "h", "y"), field=field) + + +def wrong_order(field=0): + return program([apply("x", "A"), apply("x", "B"), + apply("x", "A", -1), apply("x", "B", -1)], field=field) + + +def inverse_tail(degree, field=0): + # G^-1 (I-G)^degree has an infinite series starting at degree. + return program([query("x", "x", "A", coefficient=-1)] * degree + [apply("x", "A", -1)], + [linear("x", [])], operators=("A",), field=field) + + +def inspect(data, expected=None, literal=True): + model = compile_program(data) + f, u, t, v = reconstruct(data) + require(model["U"] == u and model["T"] == t and model["V"] == v, + "independent feedback compilers disagree") + certificate = produce(data) + summary = check(data, certificate) + if expected is not None: + require(certificate["verdict"] == expected, "unexpected universal verdict") + if literal: + endpoint = reduced_word_endpoint(data) + require((not any(endpoint)) == (certificate["verdict"] == "equal"), + "compact verdict disagrees with literal reduced group words") + if certificate["verdict"] == "different": + word = certificate["word"] + require(len(word) < model["dimension"], "distinguishing length exceeds state bound") + witness = apply_witness(data, word, data["roles"][certificate["input"]]) + require(witness[certificate["output"]][0] == f.parse(certificate["coefficient"]), + "literal invertible matrices do not realize the coefficient") + return certificate, summary + + +def inverse_word_cases(): + count = 0 + alphabet = [("A", 1), ("A", -1), ("B", 1), ("B", -1)] + for length in range(1, 4): + for word in product(alphabet, repeat=length): + instructions = [apply("x", a, sign) for a, sign in word] + inverse = [apply("x", a, -sign) for a, sign in reversed(word)] + for characteristic in (0, 2, 5): + p = program(instructions + inverse, roles=("x", "dirty"), field=characteristic) + inspect(p, "equal") + p["left"].pop() + inspect(p, "different") + count += 2 + return count + + +def differential_cases(): + rng = random.Random(20261023) + count = positives = 0 + for characteristic in (0, 2, 3, 7): + scalars = [-2, -1, 0, 1, 2, "1/5"] + for trial in range(40): + roles = ["x", "h", "y"] + steps = [] + for _ in range(8): + dst, src = rng.choice(roles), rng.choice(roles) + symbol, sign = rng.choice(["A", "B"]), rng.choice([-1, 1]) + kind = rng.randrange(3) + if kind == 0: + steps.append(apply(dst, symbol, sign)) + elif kind == 1: + steps.append(query(dst, src, symbol, sign, rng.choice(scalars))) + else: + steps.append(linear(dst, [(dst, rng.choice(scalars)), (src, rng.choice(scalars))])) + p = program(steps, deepcopy(steps), roles=roles, field=characteristic) + position = rng.randrange(len(steps) + 1) + dst, symbol = rng.choice(roles), rng.choice(["A", "B"]) + p["left"][position:position] = [apply(dst, symbol, -1), apply(dst, symbol)] + if trial % 2: + p["left"].append(query("y", "h", "A", -1, 1)) + certificate, _ = inspect(p) + positives += certificate["verdict"] == "equal" + count += 1 + return {"total": count, "equal": positives, "different": count - positives} + + +def boundary_cases(): + checked = 0 + for characteristic in (0, 2, 3, 5, 7): + good = dirty_sandwich(characteristic) + inspect(good, "equal") + for i in range(len(good["left"])): + bad = deepcopy(good) + bad["left"].pop(i) + inspect(bad, "different") + checked += 1 + inspect(wrong_order(characteristic), "different") + inspect(program([apply("h", "A")], roles=("x", "h"), field=characteristic), "different") + self_query = program([query("x", "x", "A", -1), apply("x", "A")], + [query("x", "x", "A")], field=characteristic) + inspect(self_query, "equal") + checked += 4 + inspect(program([], operators=()), "equal") + inspect(program([linear("x", [("x", 2)])], operators=()), "different") + inspect(program([query("x", "x", "A", coefficient=2)], field=0), "different") + inspect(program([query("x", "x", "A", coefficient=2)], field=2), "equal") + return checked + 4 + + +def shortest_and_infinite_tail_cases(): + count = 0 + for characteristic in (0, 2, 3, 5): + for degree in range(1, 9): + p = inverse_tail(degree, characteristic) + certificate, _ = inspect(p) + require(certificate["word"] == ["A"] * degree, "unexpected first inverse-tail coefficient") + model = compile_program(p) + f = model["field"] + row = model["U"][0] + for k in range(degree + 5): + coefficient = row_times(row, model["V"], f)[0] + expected = f.zero if k < degree else f.parse(-1 if k % 2 else 1) + require(coefficient == expected, "inverse series truncated or wrong feedback sign") + row = row_times(row, model["T"]["A"], f) + count += 1 + for p in (2, 3, 5, 7): + data = program([apply("x", "A")] * p, operators=("A",), field=p) + certificate, summary = inspect(data, "different") + require(len(certificate["word"]) == p and summary["witness_dimension"] == p + 1, + "positive-characteristic delayed witness lost") + count += 1 + return count + + +def matrix_cases(): + checked = 0 + for characteristic in (0, 2, 3, 5): + p = dirty_sandwich(characteristic) + for a, b, c, d in product(range(3), repeat=4): + operators = {"A": [[1 + a*b, a], [b, 1]], + "B": [[1, c], [d, 1 + c*d]]} + endpoint = literal_endpoint(p, operators) + require(all(not value for output in endpoint for block in output for row in block for value in row), + "dirty sandwich fails on exact invertible matrices") + checked += 1 + expect_reject(lambda: literal_endpoint(p, {"A": [[1, 0], [0, 0]], "B": [[1, 0], [0, 1]]}), + "singular actual inverse") + return checked + + +def certificate_rejections(): + p = dirty_sandwich() + good = produce(p) + failures = [] + bad = deepcopy(good); bad["program_sha256"] = "0" * 64; failures.append((p, bad, "binding")) + bad = deepcopy(good); bad["schema"] = "unknown"; failures.append((p, bad, "schema")) + bad = deepcopy(good); bad["initial"].pop(); failures.append((p, bad, "omitted return")) + bad = deepcopy(good); bad["closure"].pop("A"); failures.append((p, bad, "omitted generator")) + bad = deepcopy(good); bad["initial"][0][0] = "999"; failures.append((p, bad, "initial coordinates")) + bad = deepcopy(good); bad["closure"]["A"][0][0] = "999"; failures.append((p, bad, "closure coordinates")) + bad = deepcopy(good); bad["paths"][0]["word"] = ["absent"]; failures.append((p, bad, "unknown path")) + bad = deepcopy(good); bad["paths"][0]["output"] = 3; failures.append((p, bad, "outside role boundary")) + bad = deepcopy(good); bad["paths"][0]["output"] = True; failures.append((p, bad, "bool index")) + bad = deepcopy(good); bad["paths"][0]["word"] = ["A"] * 20; failures.append((p, bad, "path bound")) + bad = deepcopy(good); bad["unexpected"] = 1; failures.append((p, bad, "extra field")) + changed = deepcopy(p); changed["left"][0]["direction"] = 1; failures.append((changed, good, "changed inverse")) + negative = wrong_order() + different = produce(negative) + bad = deepcopy(different); bad["coefficient"] = "0"; failures.append((negative, bad, "zero witness")) + bad = deepcopy(different); bad["word"] = []; failures.append((negative, bad, "false scalar witness")) + bad = deepcopy(different); bad["word"] = list(reversed(bad["word"])); failures.append((negative, bad, "reversed word coefficient")) + scalar = program([linear("x", [("x", 2)])], operators=()) + forged = {"schema": "inverse-dirty-certificate/v1", "program_sha256": fingerprint(scalar), + "verdict": "equal", "paths": [{"output": 0, "word": []}], "initial": [["1"]], "closure": {}} + failures.append((scalar, forged, "nonzero projected invariant")) + for data, certificate, label in failures: + expect_reject(lambda: check(data, certificate), label) + return len(failures) + + +def syntax_rejections(): + good = dirty_sandwich() + cases = [] + for field in (1, 4, -1, True, 2**31): + bad = deepcopy(good); bad["field"] = field; cases.append(bad) + bad = deepcopy(good); bad["roles"] = ["x", "x", "y"]; cases.append(bad) + bad = deepcopy(good); bad["roles"] = []; cases.append(bad) + bad = deepcopy(good); bad["operators"] = ["A"]; cases.append(bad) + bad = deepcopy(good); bad["left"][0]["direction"] = True; cases.append(bad) + bad = deepcopy(good); bad["left"][0]["direction"] = 0; cases.append(bad) + bad = deepcopy(good); bad["left"][0]["dst"] = "hidden"; cases.append(bad) + bad = deepcopy(good); bad["left"][1]["terms"][0][1] = 1.5; cases.append(bad) + bad = deepcopy(good); bad["left"][1]["terms"][0][1] = True; cases.append(bad) + bad = deepcopy(good); bad["field"] = 2; bad["left"][1]["terms"][0][1] = "1/2"; cases.append(bad) + bad = deepcopy(good); bad["outputs"] = ["x"]; cases.append(bad) + for bad in cases: + expect_reject(lambda: validate(bad), "invalid program syntax") + return len(cases) + + +def stress_case(stages=64): + steps = [] + for _ in range(stages): + steps.extend([linear("h", [("x", 1)]), apply("x", "A"), query("x", "h", "B")]) + data = program(steps + [apply("x", "C", -1), apply("x", "C")], steps, + roles=("x", "h"), operators=("A", "B", "C")) + _, summary = inspect(data, "equal", literal=False) + summary["unexpanded_endpoint_words"] = str(2**stages) + return summary + + +def examples(write=False): + values = {"dirty-sandwich": dirty_sandwich(), "wrong-order": wrong_order(), + "binary-inverse-tail": inverse_tail(5, 2)} + directory = HERE / "examples" + if write: + directory.mkdir(exist_ok=True) + for name, data in values.items(): + certificate = produce(data) + artifacts = [(".json", data), (".certificate.json", certificate)] + if certificate["verdict"] == "different": + artifacts.append((".witness.json", explicit_witness(data, certificate))) + for suffix, value in artifacts: + path = directory / (name + suffix) + text = json.dumps(value, indent=2) + "\n" + if write: + path.write_text(text, encoding="utf-8") + else: + require(path.read_text(encoding="utf-8") == text, "committed example does not regenerate") + check(data, certificate) + return len(values) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write-examples", action="store_true") + parser.add_argument("--quick", action="store_true", help="development smoke only, not a full replay") + args = parser.parse_args() + result = {"examples": examples(args.write_examples), + "boundary_cases": boundary_cases(), + "certificate_rejections": certificate_rejections(), + "syntax_rejections": syntax_rejections()} + if not args.quick: + result.update(inverse_word_cases=inverse_word_cases(), + differential_cases=differential_cases(), + inverse_tail_cases=shortest_and_infinite_tail_cases(), + literal_matrix_cases=matrix_cases(), stress=stress_case()) + result["status"] = "PASS_INVERSE_DIRTY_CERTIFICATES" if not args.quick else "SMOKE_ONLY" + result["scope"] = "Exact finite corroboration of PROOF.md; no native/physical admission or new kappa." + print(json.dumps(result, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()