From b7923ed3312a518534ae94be0cd16b6beb518619 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 27 Oct 2026 13:38:57 +0000 Subject: [PATCH] feat(research): bound exact identity tests by live sign width --- research/sign-frontier-identity/PROOF.md | 158 +++++++++++++++ research/sign-frontier-identity/README.md | 163 ++++++++++++++++ research/sign-frontier-identity/SOURCES.json | 30 +++ research/sign-frontier-identity/TASK.json | 111 +++++++++++ research/sign-frontier-identity/VERIFY.json | 37 ++++ research/sign-frontier-identity/solver.py | 144 ++++++++++++++ research/sign-frontier-identity/verify.py | 191 +++++++++++++++++++ 7 files changed, 834 insertions(+) create mode 100644 research/sign-frontier-identity/PROOF.md create mode 100644 research/sign-frontier-identity/README.md create mode 100644 research/sign-frontier-identity/SOURCES.json create mode 100644 research/sign-frontier-identity/TASK.json create mode 100644 research/sign-frontier-identity/VERIFY.json create mode 100644 research/sign-frontier-identity/solver.py create mode 100644 research/sign-frontier-identity/verify.py diff --git a/research/sign-frontier-identity/PROOF.md b/research/sign-frontier-identity/PROOF.md new file mode 100644 index 0000000000..2c971a4615 --- /dev/null +++ b/research/sign-frontier-identity/PROOF.md @@ -0,0 +1,158 @@ +# Complete dirty endpoints with bounded live signs + +This contribution was produced by Nick Petalas. Apache-2.0. + +## Statement and scope + +Consider a chronological word of L instructions on r independent roles. +The permitted instructions are rational ADD, signed QUERY, signed unary +APPLY and SWAP. An ADD is x_d <- x_d + c x_s. A QUERY is +x_d <- x_d + c z_j x_s. An APPLY is x_d <- z_j x_d. A SWAP exchanges +two roles. Here d != s, c is rational and each z_j independently belongs +to {+1,-1}. Repeated occurrences of a label use the same sign. All roles +have arbitrary initial values, and equality concerns their complete endpoint. + +After instruction t, let B_t consist of labels whose first occurrence is +at most t and whose last occurrence is greater than t. Set + + k = max_(0 <= t <= L) |B_t|, D = r^2+1. + +An instruction containing a sign only once does not put it in either +adjacent frontier. Such an instruction still branches over both signs. + +**Theorem.** Identity of the complete word at every sign assignment is +decidable deterministically using at most + + L * 2^(k+1) * D + +candidate prefix updates and O(L * 2^(k+1) * D^3) rational arithmetic +operations. At each cut it retains at most 2^k * D actual prefix matrices. +If the word is not the identity, it returns an actual sign assignment +and hence a complete-endpoint counterexample. Rational bit complexity +is 2^k times a polynomial in the ordinary input size. In particular, +fixed r and bounded k give a polynomial-time exact test independently +of the total number n of sign labels. + +The same test compares two words by appending the inverse of the second +to the first. The parameter k is measured on that concatenation, not +separately on each word. This qualification can matter substantially. + +## Homogeneous prefix invariant + +Let P be a complete r-by-r prefix matrix and define + + h(P) = (vec(P),1) in Q^D. + +For every live assignment a on B_t, retain a set S_(t,a) of actual +prefix matrices together with their actual sign histories. Its invariant is + + span { h(P) : P in S_(t,a) } + = span { h(P_t(e)) : e is any prefix assignment restricting to a }. + +The right-hand set ranges over assignments to every label already seen, +including forgotten labels. At t=0 there is only h(I), so the invariant +holds. A basis needs at most D representatives; selection by exact +incremental Gaussian elimination can keep actual members of the set. +The normalized elimination rows are auxiliary data, never fake executions. + +For a fixed next sign, left multiplication by the instruction matrix A +induces a linear map on homogeneous vectors, + + (vec(P),u) -> (vec(AP),u). + +If the next sign is new, branch each representative with both choices. +If its label is live, its value is already specified by a. Constant +instructions do not branch. Apply the linear map to every representative. +Then restrict the sign key to B_(t+1), merging keys for labels that have +just reached their last occurrence. Taking the span of this union and +selecting a basis preserves exactly the displayed invariant. Forgotten +signs have no future occurrence, so this merger loses no future correlation. +No bound on the number of their possible histories is assumed. + +At the last cut the frontier is empty. Define the linear map + + F(vec(P),u) = vec(P) - u vec(I). + +Every complete endpoint equals I exactly when F vanishes on the final +span. It suffices to check its retained basis. Each retained vector is +h(P) for an actual assignment, so any failing basis member supplies an +actual counterexample. A differing column supplies a dirty input on which +the endpoints differ. This proves both decision and witness correctness. + +The homogeneous coordinate is necessary for this implementation. Ordinary +linear span cannot distinguish the set {I} from {I,-I}. For example, +applying the same sign once to each of the five roles has endpoint zI. +Keeping only a nonhomogeneous basis can discard the negative endpoint. +The supplied semantic control requires the negative assignment to survive. + +## Cost and exact arithmetic + +There are at most 2^k keys before an instruction, and each has at most D +representatives. Each representative has at most two successors. Thus +there are at most 2^(k+1)D candidate updates per instruction, including +a sign occurring only once. Left multiplication costs O(r^3) operations +even for a general dense instruction matrix. The supplied elementary +updates cost only O(r). Incremental echelon reduction of a D-vector +against at most D stored rows costs O(D^2). These bounds give the theorem. +Only the previous and next layers, their elimination rows and their +actual witnesses need remain live. Besides input and schedule storage, +the space is O(2^k D^2) rationals and O(2^k D n) witness bits. + +For completeness, this is also a bit-complexity claim, not just a unit-cost +field count. Let b bound the bit length of any input numerator or +denominator. Clear each instruction's denominators first. The product +of these denominators has O(Lb) bits, and products of r-by-r integer +matrices have entry length O(L(b+log(r+1))). Hence every actual prefix +has a polynomial-size rational representation. The homogeneous coordinate +has the same bound after clearing row denominators. Elimination entries +are ratios of minors of at most D such rows. The determinant expansion +bounds their bit lengths by a polynomial in D,L,b. Exact rational +arithmetic and independence tests therefore have polynomial bit cost. +Witnesses are n-bit assignments. Label indices themselves remain part +of the input encoding; sparse large indices can be renamed in order of +first occurrence before this mathematical algorithm. + +## Native interpretation and comparison + +This is the commuting-sign subclass specified in PR #5716, Section 1. +For the diagonal generator Z_j e_x=(-1)^(x_j)e_x, its f-fold tensor power +acts on an address tuple by the scalar + + z_j = (-1)^(x_j^(1)+...+x_j^(f)). + +Every sign assignment is realized at f=1. It is also realized for every +positive f by using its binary address in the first tensor factor and +zero addresses in the remaining factors. Instructions preserve addresses, +so their complete endpoint is block diagonal with the scalar endpoints +just tested. The theorem therefore decides equality at every positive +tensor width in this exact subclass. This application uses the stated +sign semantics; it does not check another contributor's compiler. + +ADD and QUERY are inverted by negating c; APPLY and SWAP are involutions. +Reverse the instruction order to invert a word. If P and Q are the two +endpoints, first executing the first word and then the inverse second word +has endpoint Q^(-1)P. It is I if and only if P=Q, on every sign assignment. +No zero role, erased output, independent resampling of repeated signs or +unpaid physical operation is introduced by this mathematical reduction. + +## What is new here + +PR #5716 explicitly asks for a useful restricted class with a tractable +complete-endpoint identity test. The contribution is the live-sign +restriction, the displayed source-grammar bound and the executable +counterexample-preserving test. It is a scoped answer to that question, +not a new general weighted-automaton equivalence principle or a claim +of priority for parameterized dynamic programming. + +Reachable-span bases and retaining concrete witnesses are classical. +See Stefan Kiefer, [Notes on Equivalence and Minimization of Weighted +Automata](https://arxiv.org/abs/2009.01217), Section 2, especially +Propositions 2.1 and 2.2, and the Schutzenberger/Tzeng lineage cited there. +The adaptation here conditions the span on currently live signs, forgets +them only after their final occurrence and homogenizes complete matrices +to test an affine equality. The proof above is self-contained. + +No small k is proved for the selected P104 caller, the CNF hardness +construction or general native affine/quadratic operators. Noncommuting +address maps and rounded arithmetic are excluded. There is no new kappa, +physical tariff, supplier admission or complete multiplication theorem. diff --git a/research/sign-frontier-identity/README.md b/research/sign-frontier-identity/README.md new file mode 100644 index 0000000000..c4db4d1195 --- /dev/null +++ b/research/sign-frontier-identity/README.md @@ -0,0 +1,163 @@ +# Exact dirty-endpoint tests with bounded live signs + +This contribution was produced by Nick Petalas. Apache-2.0. + +## Result + +Scoped written mathematical proof with exact finite corroboration. For a word +of L rational ADD, signed QUERY, signed APPLY and SWAP instructions on r +arbitrary dirty roles, let k be the maximum number of signs that have appeared +but will appear again. Complete identity at every assignment is decidable in + + O(L * 2^(k+1) * (r^2+1)^3) + +rational operations, with at most 2^k(r^2+1) retained actual prefix matrices. +Bit complexity is 2^k times a polynomial in the ordinary input size. A failed +identity returns an actual sign assignment. Repeated signs remain correlated, +and every input and returned role participates in the endpoint. + +In the commuting diagonal-sign native subclass, this decides equality at every +positive tensor width. Two words can be compared by appending the inverse of +the second to the first; k is measured on the concatenation. No small k is +asserted for the selected caller or the general hardness construction. + +[PROOF.md](PROOF.md) gives the theorem, homogeneous span invariant, field and +bit bounds, native interpretation and exact limitations. The algorithm is + +```text +for each instruction + branch new signs; preserve every live sign + transform actual prefix matrices within each live-sign assignment + forget signs at their last use; retain a homogeneous span basis +check every final representative against the complete identity +``` + +The extra homogeneous coordinate distinguishes I from -I. A basis consists +of genuine prefixes with genuine assignments, so a failing representative +is a concrete counterexample rather than a formal linear combination. + +## Source and novelty boundary + +Hiroki KUMAZAKI's [PR #5716](https://github.com/CrocSwap/integer-mult-bounds/pull/5716), +head `946acb3a36953216dd9a39f0c5222a40a9e90cd3`, explicitly asks for a useful +restricted class with a tractable complete-endpoint identity test. This +package answers that open question with the bounded live-sign hypothesis. +Its CNF audit and Ali Romman's [PR #5369](https://github.com/CrocSwap/integer-mult-bounds/pull/5369) +reduction are cited, not rechecked as this contribution. Barrington retains +the classical five-role branching-program method. + +Reachable-span reduction and concrete witness retention are classical; see +Stefan Kiefer's [weighted-automata notes](https://arxiv.org/abs/2009.01217), +Section 2 and its Schutzenberger/Tzeng references. The new contribution is +the live-sign-conditioned complete-endpoint application and explicit bound, +not a new general equivalence algorithm or a literature-priority claim. +zxv's [PR #5235](https://github.com/CrocSwap/integer-mult-bounds/pull/5235) +handles independent formal operators, and +[PR #5441](https://github.com/CrocSwap/integer-mult-bounds/pull/5441) handles +already supplied fixed transfer tables across tensor columns. Neither is +the repeated-sign lifetime bound proved here. Their methods retain credit. + +Canonical base is `de5ec2e7a6074068452f45b1a191b5c72832df4a`, priority revision 8. +[SOURCES.json](SOURCES.json) pins the question and grammar documents; the direct +verifier checks their hashes without executing predecessor code. Selected +metadata and the task card are provenance only. This explicitly changes the +`formal-interface-lemma` card to an informal algorithmic side result; no proof +assistant build or selected assumption discharge is claimed. + +The initial overlap cache covered 470 open PRs and 5,432 Discussion records +with complete reported pagination. Its local filesystem search was sparse, +so separate main-tree README searches and merged-PR searches were also used. +These searches do not cover unpublished work or every historical code diff. +[Advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19217826). + +## Reproduction and evidence + +From the repository root, with CPython 3.12 and its standard library only: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/sign-frontier-identity/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/sign-frontier-identity/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/sign-frontier-identity +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/sign-frontier-identity --check-source-history +``` + +Elsewhere substitute a CPython 3.12 executable. Expected direct status is +`PASS_SIGN_FRONTIER_IDENTITY`; registered replay ends with +`PASS_REGISTERED_RESEARCH_PACKAGE`. Each registered command has a 120-second +timeout. The direct checker writes a generated JSON receipt to stdout, binding +every package file by SHA256; redirect it outside the checkout if desired. +It neither reads a saved expected receipt nor writes files into the package. + +The finite checks include: + +- All 1,555 words of length zero through four over the declared six-gate + alphabet, with 4,097 exhaustive sign assignments. +- 216 structured words on two, three and five roles, with 9,216 exhaustive + assignments. A separate column-vector interpreter checks every input column, + complete endpoint verdict and returned counterexample. +- Two 128-sign families. The width-zero negative family retains two matrices + and returns a literal witness although its all-positive assignment is the + identity. The width-one positive family preserves repeated-sign cancellation. + Each processes exactly 512 candidates. These families are not exhaustively + enumerated over their sign assignments. +- An eight-live-sign identity visiting all 256 live keys, with 1,020 candidate + updates, plus five capacity/inverse fixtures. These cover the 4,096-gate + limit, label 4,095, 64-bit coefficients, the empty one-role word and a mixed + ADD/QUERY/APPLY/SWAP inverse. +- Eighteen invalid-input/capacity rejections and three semantic controls for + homogeneous scalar phases, correlated repeated signs and independent signs. + +The infinite statement rests on the written invariant and bit argument; +finite comparisons corroborate the implementation. Local normal/optimized +registered replay, source metadata and committed-byte/source-history checks +are separate from hosted CI and independent scientific acceptance. + +## Limitations + +The executable accepts 1..5 roles, at most 4,096 gates, frontier limit at most +eight, sign labels 0..4,095 and exact fractions with numerator/denominator +length at most 64 bits. It rejects larger inputs rather than narrowing its +verdict silently. The written theorem does not require these implementation +caps. It is an exact code API, not a native-source parser or general compiler. + +Only commuting diagonal signs are covered. Arbitrary affine address changes, +quadratic phases, nonlinear leaves, rounding, ownership, physical routing, +precision/tapes and paid supplier costs need separate contracts. The test +does not supply a faster physical word or a new multiplication theorem. +No new kappa or selected-frontier change. Independent human and formal +proof-kernel review are unclaimed. No predecessor scientific suite, selected +cold replay, Lean or Docker run was performed. + +## Implementation inspection + +The bounded executable uses no recursion. All loops range over validated +inputs, finite sign branches, at most 256 live assignments and at most 26 +representatives per assignment. An input check precedes frontier allocation. +State and witnesses are local to one decision. Scientific checks use explicit +exceptions and remain enabled under optimization. Functions stay below 60 +physical lines. Warning-strict normal/optimized execution and AST compilation +provide the available standard-library diagnostics; no external static +analyzer is required or claimed. + +Power-of-Ten rule 3 deviation: CPython and Fraction allocate managed objects +during elimination. This is confined to the validated solver domain above, +with two adjacent layers, at most 26 elimination rows per key and the +polynomial rational-size bound in PROOF.md. Capacity rejection and maximum +frontier/gate/label/coefficient fixtures verify the bounds. A fixed-allocation +implementation would be a separate lower-level port; no constant-RSS claim +is made. Rule 8/9 deviation: the verifier loads the single package-local +solver via a fixed importlib path, and rejection controls use bounded local +callbacks. No external path or callback is accepted. Normal and optimized +replay exercise every such target. + +## Open next questions + +1. Does a useful emitted caller in this subclass have small k after legal + reordering? Extract labels and their first/last occurrences from one exact + word before attempting reordering. A source-bound extraction contract and + preservation of every dirty return are still needed. +2. Can one correlated family avoid explicit enumeration of its live signs? + Begin with a precise replacement invariant. Large k remains exponential + here; generic hardness is not contradicted. + +[TASK.json](TASK.json) records the relevance, first step and blockers for both. diff --git a/research/sign-frontier-identity/SOURCES.json b/research/sign-frontier-identity/SOURCES.json new file mode 100644 index 0000000000..8011cb37a2 --- /dev/null +++ b/research/sign-frontier-identity/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/reversible-cnf-independent-audit/PROOF.md", + "usage": "input", + "git_blob": "5d4ba20edc00381c72de756fd2fbd7fa33dfbeba", + "sha256": "5e35ffc14e07fa87d7e1fd467ca0aabe8a3922dd31a9bfd5a73a20d48b6df68c" + }, + { + "path": "research/reversible-cnf-independent-audit/README.md", + "usage": "input", + "git_blob": "5ae1ef6558a2218d8c54530fd131d1fdc49e87e8", + "sha256": "dce8411944f39a1bfdcbf7eacc40e0e55612e65b145dda0f674606f68a7e3c71" + } + ] +} diff --git a/research/sign-frontier-identity/TASK.json b/research/sign-frontier-identity/TASK.json new file mode 100644 index 0000000000..96ae20c0d1 --- /dev/null +++ b/research/sign-frontier-identity/TASK.json @@ -0,0 +1,111 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 8, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "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_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "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": "Exact complete dirty-endpoint identity testing for the commuting-sign ADD/QUERY/APPLY/SWAP grammar, parameterized by live sign frontier width.", + "scope_change_reason": "Take PR #5716 Open next questions: construct a tractable restricted identity test instead of formalizing an existing interface in a proof assistant.", + "bottleneck_link": "Side result for exact native-word verification: bounded sign lifetimes make complete all-width endpoint testing tractable. No selected caller frontier bound or physical cost saving is asserted.", + "budget_minutes": 60, + "stop_rule": "Ship the first proved restriction with a concrete counterexample-producing algorithm and exhaustive finite corroboration; do not expand to other native alphabets.", + "outcome": "completed", + "evidence": "PROOF.md; verify.py compares every complete column for 1555 small words and 216 structured words, tests 128-sign bounded-frontier families and rejection controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Does a concrete useful emitted native caller have a small live-sign frontier after legal instruction reordering?", + "why_it_matters": "The parameter controls this exact test, but no production caller bound is supplied.", + "first_step": "Extract sign labels and first/last occurrence intervals from one exact emitted commuting-sign word; preserve every instruction and dirty return.", + "blocked_by": "A caller in the stated commuting-sign subclass and a source-bound extraction contract." + }, + { + "question": "Can a stronger exact summary replace explicit 2^k live-sign assignments for a named correlated family?", + "why_it_matters": "The present theorem is exponential in frontier width, so large-overlap words remain expensive.", + "first_step": "Give one repeated-sign family and prove a correlation-preserving summary invariant before implementing it.", + "blocked_by": "No such summary is supplied; generic hardness remains predecessor work." + } + ], + "environment": { + "python": "CPython 3.12.15", + "platform": "macOS arm64", + "dependencies": "standard library only" + }, + "coordination": { + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19217826", + "checked_main": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "checked_utc": "2026-10-27T13:34:50.004618+00:00" + } +} diff --git a/research/sign-frontier-identity/VERIFY.json b/research/sign-frontier-identity/VERIFY.json new file mode 100644 index 0000000000..5a4d8ab168 --- /dev/null +++ b/research/sign-frontier-identity/VERIFY.json @@ -0,0 +1,37 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/reversible-cnf-independent-audit/PROOF.md", + "research/reversible-cnf-independent-audit/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact exhaustive endpoints, concrete witnesses, frontier capacity, 128-sign families and rejecting controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact exhaustive endpoints, concrete witnesses, frontier capacity, 128-sign families and rejecting controls." + } + ] +} diff --git a/research/sign-frontier-identity/solver.py b/research/sign-frontier-identity/solver.py new file mode 100644 index 0000000000..0702d009ff --- /dev/null +++ b/research/sign-frontier-identity/solver.py @@ -0,0 +1,144 @@ +"""Exact complete-endpoint tests for bounded live signs. + +Produced by Nick Petalas. Apache-2.0. +""" + +from dataclasses import dataclass +from fractions import Fraction + + +@dataclass(frozen=True) +class Gate: + kind: str + dst: int + src: int | None = None + coefficient: Fraction = Fraction(1) + sign: int | None = None + + +def validate(roles, word, frontier_limit): + """Check the executable capacity contract before allocating state tables.""" + if type(roles) is not int or not 1 <= roles <= 5: + raise ValueError("roles must be an integer in 1..5") + if type(frontier_limit) is not int or not 0 <= frontier_limit <= 8: + raise ValueError("frontier limit must be an integer in 0..8") + if not isinstance(word, tuple) or len(word) > 4096: + raise ValueError("word must be a tuple of at most 4096 gates") + for gate in word: + if not isinstance(gate, Gate) or gate.kind not in ("ADD", "QUERY", "APPLY", "SWAP"): + raise ValueError("invalid gate kind") + if type(gate.dst) is not int or not 0 <= gate.dst < roles: + raise ValueError("invalid destination") + if type(gate.coefficient) is not Fraction: + raise ValueError("coefficient must be an exact Fraction") + if max(abs(gate.coefficient.numerator).bit_length(), gate.coefficient.denominator.bit_length()) > 64: + raise ValueError("coefficient exceeds 64 bits") + if gate.kind != "APPLY": + if type(gate.src) is not int or not 0 <= gate.src < roles or gate.src == gate.dst: + raise ValueError("distinct source and destination required") + elif gate.src is not None: + raise ValueError("APPLY has no source") + if gate.kind in ("QUERY", "APPLY"): + if type(gate.sign) is not int or not 0 <= gate.sign < 4096: + raise ValueError("sign label must be an integer in 0..4095") + elif gate.sign is not None: + raise ValueError("unsigned gate carries a sign") + if gate.kind in ("SWAP", "APPLY") and gate.coefficient != 1: + raise ValueError("SWAP and APPLY have unit coefficient") + + +def identity(roles): + return tuple(Fraction(i == j) for i in range(roles) for j in range(roles)) + + +def advance(matrix, gate, roles, sign): + """Apply a literal elementary row operation to the complete prefix map.""" + result = list(matrix) + for column in range(roles): + dst = gate.dst * roles + column + if gate.kind == "APPLY": + result[dst] = sign * matrix[dst] + elif gate.kind == "SWAP": + src = gate.src * roles + column + result[dst], result[src] = matrix[src], matrix[dst] + else: + scale = gate.coefficient * (sign if gate.kind == "QUERY" else 1) + result[dst] += scale * matrix[gate.src * roles + column] + return tuple(result) + + +def retain(echelon, representatives, matrix, witness): + """Keep an actual prefix when its homogenization increases the span.""" + row = list(matrix) + [Fraction(1)] + for pivot, basis in echelon: + coefficient = row[pivot] + if coefficient: + row = [value - coefficient * entry for value, entry in zip(row, basis)] + pivot = next((i for i, value in enumerate(row) if value), None) + if pivot is not None: + scale = row[pivot] + echelon.append((pivot, tuple(value / scale for value in row))) + representatives.append((matrix, witness)) + assert len(representatives) <= len(matrix) + 1 + + +def schedule(word): + first, last = {}, {} + for index, gate in enumerate(word): + if gate.sign is not None: + first.setdefault(gate.sign, index) + last[gate.sign] = index + active, width, masks = 0, 0, [] + for index, gate in enumerate(word): + if gate.sign is not None: + bit = 1 << gate.sign + if first[gate.sign] == index: + active |= bit + if last[gate.sign] == index: + active &= ~bit + masks.append(active) + width = max(width, active.bit_count()) + assert active == 0 + return first, masks, width + + +def step(states, gate, roles, introduce, mask): + buffers = {} + candidates = 0 + for representatives in states.values(): + for matrix, witness in representatives: + for negative in ((False, True) if introduce else (False,)): + changed = witness | (1 << gate.sign) if negative else witness + sign = -1 if gate.sign is not None and (changed >> gate.sign) & 1 else 1 + updated = advance(matrix, gate, roles, sign) + echelon, kept = buffers.setdefault(changed & mask, ([], [])) + retain(echelon, kept, updated, changed) + candidates += 1 + return {key: kept for key, (_, kept) in buffers.items()}, candidates + + +def decide(roles, word, frontier_limit=8): + """Return identity status, an actual negative-sign mask if false, and counts.""" + validate(roles, word, frontier_limit) + first, masks, width = schedule(word) + if width > frontier_limit: + raise ValueError("live-sign frontier exceeds the declared limit") + states = {0: [(identity(roles), 0)]} + candidates, max_states, max_basis = 0, 1, 1 + for index, gate in enumerate(word): + introduce = gate.sign is not None and first[gate.sign] == index + states, count = step(states, gate, roles, introduce, masks[index]) + candidates += count + max_states = max(max_states, len(states)) + max_basis = max(max_basis, max(map(len, states.values()))) + assert len(states) <= 2 ** width + expected = identity(roles) + witness = next((bits for matrix, bits in states[0] if matrix != expected), None) + return {"identity": witness is None, "witness": witness, "frontier": width, + "max_states": max_states, "max_basis": max_basis, "candidates": candidates} + + +def inverse(word): + return tuple(Gate(g.kind, g.dst, g.src, + -g.coefficient if g.kind in ("ADD", "QUERY") else g.coefficient, + g.sign) for g in reversed(word)) diff --git a/research/sign-frontier-identity/verify.py b/research/sign-frontier-identity/verify.py new file mode 100644 index 0000000000..00b1ef974f --- /dev/null +++ b/research/sign-frontier-identity/verify.py @@ -0,0 +1,191 @@ +"""Exact finite corroboration. Produced by Nick Petalas. Apache-2.0.""" + +import hashlib +import importlib.util +import itertools +import json +from fractions import Fraction as F +from pathlib import Path +import sys + + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] + + +def require(condition, message): + if not condition: + raise RuntimeError(message) + + +def load_solver(): + spec = importlib.util.spec_from_file_location("sign_frontier_solver", PACKAGE / "solver.py") + module = importlib.util.module_from_spec(spec) + sys.modules[spec.name] = module + spec.loader.exec_module(module) + return module + + +def literal(roles, word, witness): + """Separate column-vector interpreter, without the solver's row updates.""" + columns = [] + for column in range(roles): + values = [F(row == column) for row in range(roles)] + for gate in word: + sign = -1 if gate.sign is not None and (witness >> gate.sign) & 1 else 1 + if gate.kind == "ADD": + values[gate.dst] += gate.coefficient * values[gate.src] + elif gate.kind == "QUERY": + values[gate.dst] += gate.coefficient * sign * values[gate.src] + elif gate.kind == "APPLY": + values[gate.dst] *= sign + else: + values[gate.dst], values[gate.src] = values[gate.src], values[gate.dst] + columns.append(values) + return tuple(columns[j][i] for i in range(roles) for j in range(roles)) + + +def exhaustive_check(solver, roles, word): + labels = sorted({gate.sign for gate in word if gate.sign is not None}) + require(len(labels) <= 8, "exhaustive sign limit") + good, count = True, 0 + for signs in itertools.product((0, 1), repeat=len(labels)): + witness = sum(bit << label for bit, label in zip(signs, labels)) + good &= literal(roles, word, witness) == solver.identity(roles) + count += 1 + result = solver.decide(roles, word) + require(result["identity"] == good, "identity verdict differs from exhaustive columns") + if not good: + require(literal(roles, word, result["witness"]) != solver.identity(roles), "invalid witness") + dimension = roles * roles + 1 + require(result["max_basis"] <= dimension, "basis capacity") + require(result["max_states"] <= 2 ** result["frontier"], "state capacity") + require(result["candidates"] <= len(word) * 2 ** (result["frontier"] + 1) * dimension, + "candidate bound") + return count + + +def small_words(solver): + gate = solver.Gate + alphabet = (gate("ADD", 0, 1, F(1, 2)), gate("ADD", 1, 0, F(-2)), + gate("QUERY", 0, 1, F(1), 0), gate("QUERY", 1, 0, F(-1, 2), 1), + gate("APPLY", 0, sign=0), gate("SWAP", 0, 1)) + words, assignments = 0, 0 + for length in range(5): + for word in itertools.product(alphabet, repeat=length): + assignments += exhaustive_check(solver, 2, word) + words += 1 + return words, assignments + + +def structured_words(solver): + gate = solver.Gate + words, assignments = 0, 0 + for roles in (2, 3, 5): + for seed in range(24): + prefix = tuple(gate("QUERY", (seed + j) % roles, (seed + j + 1) % roles, + F((-1) ** j, 1 + (j % 3)), (j * 3 + seed) % 5) + for j in range(8)) + for word in (prefix, prefix + solver.inverse(prefix), + prefix + solver.inverse(prefix) + (gate("APPLY", 0, sign=5),)): + assignments += exhaustive_check(solver, roles, word) + words += 1 + return words, assignments + + +def large_frontiers(solver): + gate = solver.Gate + once = tuple(gate("QUERY", 1, 0, F(1), j) for j in range(128)) + once += (gate("ADD", 1, 0, F(-128)),) + negative = solver.decide(5, once, frontier_limit=0) + require(not negative["identity"], "lost non-all-plus branch") + require(literal(5, once, 0) == solver.identity(5), "all-plus control") + require(literal(5, once, negative["witness"]) != solver.identity(5), "large witness") + require(negative["max_basis"] == 2, "rank-two affine prefix family") + paired = tuple(gate("QUERY", 1, 0, F(sign, 3), j) + for j in range(128) for sign in (1, -1)) + positive = solver.decide(5, paired, frontier_limit=1) + require(positive["identity"] and positive["frontier"] == 1, "repeated-sign cancellation") + crossing = tuple(gate("QUERY", 1, 0, F(1), j) for j in range(8)) + crossing += tuple(gate("QUERY", 1, 0, F(-1), j) for j in range(8)) + crossed = solver.decide(5, crossing) + require(crossed["identity"] and crossed["max_states"] == 256, "full frontier occupancy") + return {"once_128": negative, "paired_128": positive, "crossing_8": crossed} + + +def expect_rejection(callback): + try: + callback() + except ValueError: + return 1 + raise RuntimeError("invalid input accepted") + + +def controls(solver): + gate = solver.Gate + cases = ((0, ()), (True, ()), (6, ()), (2, []), + (2, (gate("BAD", 0, 1),)), (2, (gate("ADD", 0, 0),)), + (2, (gate("QUERY", 0, 1),)), (2, (gate("ADD", 0, 1, F(1), 0),)), + (2, (gate("APPLY", 0, 1, sign=0),)), + (2, (gate("SWAP", 0, 1, F(2)),)), + (2, (gate("QUERY", 0, 1, F(1), -1),)), + (2, (gate("ADD", 0, 1, 0.5),)), + (2, (gate("ADD", 0, 1, F(1 << 65)),)), + (2, (gate("ADD", 2, 0),)), (2, (gate("APPLY", True, sign=0),)), + (2, (gate("ADD", 0, 1),) * 4097)) + count = sum(expect_rejection(lambda r=r, w=w: solver.decide(r, w)) for r, w in cases) + repeated = (gate("APPLY", 0, sign=0),) * 2 + count += expect_rejection(lambda: solver.decide(2, repeated, frontier_limit=0)) + count += expect_rejection(lambda: solver.decide(2, (), frontier_limit=9)) + scalar = tuple(gate("APPLY", j, sign=0) for j in range(5)) + result = solver.decide(5, scalar) + require(not result["identity"] and result["witness"] == 1, "homogeneous scalar control") + require(solver.decide(2, repeated)["identity"], "repeated signs must agree") + require(not solver.decide(2, (repeated[0], gate("APPLY", 0, sign=1)))["identity"], + "independent signs must branch") + return count, 3 + + +def boundary_fixtures(solver): + gate = solver.Gate + fixtures = ((1, ()), (1, (gate("APPLY", 0, sign=4095),) * 2), + (5, (gate("SWAP", 0, 4),) * 4096), + (2, (gate("ADD", 0, 1, F((1 << 64) - 1)), + gate("ADD", 0, 1, F(-((1 << 64) - 1)))))) + for roles, word in fixtures: + require(solver.decide(roles, word)["identity"], "accepted capacity boundary") + mixed = (gate("ADD", 0, 1, F(2, 3)), gate("QUERY", 2, 0, F(-7, 5), 3), + gate("APPLY", 1, sign=1), gate("SWAP", 1, 4)) + exhaustive_check(solver, 5, mixed + solver.inverse(mixed)) + require(solver.decide(5, mixed + solver.inverse(mixed))["identity"], "mixed inverse") + return len(fixtures) + 1 + + +def authenticate(): + sources = json.loads((PACKAGE / "SOURCES.json").read_text()) + for row in sources["files"]: + if row["usage"] == "input": + require(hashlib.sha256((ROOT / row["path"]).read_bytes()).hexdigest() == row["sha256"], + "source input hash mismatch: " + row["path"]) + + +def main(): + authenticate() + solver = load_solver() + small, small_assignments = small_words(solver) + structured, structured_assignments = structured_words(solver) + large = large_frontiers(solver) + rejected, semantic = controls(solver) + boundaries = boundary_fixtures(solver) + result = {"status": "PASS_SIGN_FRONTIER_IDENTITY", "small_words": small, + "small_assignments": small_assignments, "structured_words": structured, + "structured_assignments": structured_assignments, "large_fixtures": large, + "input_rejections": rejected, "semantic_controls": semantic, + "capacity_and_inverse_fixtures": boundaries, + "package_sha256": {p.name: hashlib.sha256(p.read_bytes()).hexdigest() + for p in sorted(PACKAGE.iterdir()) if p.is_file()}} + print(json.dumps(result, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()