diff --git a/research/rectangular-dirty-certificates/DECISIONS.md b/research/rectangular-dirty-certificates/DECISIONS.md new file mode 100644 index 0000000000..209b47b766 --- /dev/null +++ b/research/rectangular-dirty-certificates/DECISIONS.md @@ -0,0 +1,39 @@ +# Implementation limits + +Investigation playbook. Build the Lever shaped the choice to retain a runnable +certificate producer/checker. Prove It Works shaped the explicit-word and +literal rectangular matrix oracles. The Power of Ten inspections are scoped +to the three new Python files; predecessor files are read-only provenance. + +All control flow is structured and nonrecursive. Public inputs limit roles +to 16, types to 8, arrows to 16 and each program to 128 instructions. The +combined state dimension is at most 288. The basis accepts at most D rows; +there are at most 16D arrow successor candidates. Each path has fewer than D +letters. Echelon and coordinate loops have at most D rows or entries. The +finite test loops have explicit bounds. No solver, subprocess or unbounded +queue is used. All functions are shorter than sixty lines. + +Rule 3, fixed allocation, requires a managed-runtime deviation in these three +files. Python lists, dictionaries and Fraction allocate during elimination. +Live rational-cell storage is polynomial in the enforced finite input sizes; +exact rational bit growth can still be large. Certificate encodings are capped +and refused explicitly. The implementation makes no practical space or runtime +promise for every capped problem. No fixed-size real-time allocator is supplied. +The bounded small fixtures and registered 120-second timeout cover this replay. +A deployment requiring a hard memory budget must use an external process +memory limit or a bounded exact-arithmetic backend before accepting untrusted +workloads. The tool is intended for local research input, not a service. + +Rule 9, indirect calls, has a narrow test-only deviation: must_reject receives +one of the locally defined validation/checker lambdas. There are fourteen +enumerated controls. Production compilation and certificate checking call +named functions directly. No runtime registration or generated executable code +is used. File resources use context managers; CLI writes are exclusive-create. + +Externally supplied arguments use ordinary rejecting checks. Internal compiler +state-count and basis-dimension invariants use assertions; every scientific +acceptance condition uses require and remains active under Python -O. Both +registered commands enable warning errors. No external linter or type checker +is installed in the declared standard-library environment. Repository metadata, +publication-byte/source-history checks and literal CLI examples supplement the +normal/optimized scientific replay. No repository-wide diagnostics are changed. diff --git a/research/rectangular-dirty-certificates/PROOF.md b/research/rectangular-dirty-certificates/PROOF.md new file mode 100644 index 0000000000..c681aeec96 --- /dev/null +++ b/research/rectangular-dirty-certificates/PROOF.md @@ -0,0 +1,164 @@ +# Compact certificates with rectangular payload types + +This contribution was produced by Nick Petalas. Apache-2.0. + +## Statement and credit + +Let K be a field. A finite set of types t has independently chosen +finite-dimensional spaces V_t, which may have dimension zero. Each arrow a +has a declared source s(a) and target t(a), and denotes an arbitrary linear +map X_a:V_s(a)->V_t(a). Different arrows are independent, including arrows +with identical endpoints. A register has one fixed type and an arbitrary +independent initial value. Scalar ADD and SWAP require equal register types; +SCALE acts within one register; QUERY adds c X_a v_src to v_dst with matching +types. APPLY is permitted only for an endomorphism of the register's type. +Every register is retained in the complete endpoint. Scalars are central. + +**Typed bridge.** A program with r registers and q unary occurrences has +r+q dependency states. For two programs on the same registers, let +D=2r+q_left+q_right. Equality for every choice of the V_t and X_a is +equivalent to a reachable-row closure certificate with at most D rows. +Exact arithmetic finds either such a certificate or a shortest nonzero +typed coefficient path w of length k. In the latter case a literal +rectangular substitution with zero/one entries distinguishes the endpoints, +using dimension + + d_t = number of visits to type t along w, + sum_t d_t = k+1. + +Here k is at most the larger unary dependency depth of the two programs, +and at most D-1. Types not visited by w have dimension zero. If all type +spaces must be nonzero, add one unused coordinate to each unvisited type. +This is a constructive upper bound, not a minimum-dimension theorem for +arbitrary counterexamples. + +The equal-space dependency compiler and closure method are zxv's +[PR5235](https://github.com/CrocSwap/integer-mult-bounds/pull/5235), whose +proof is pinned in SOURCES.json. Its classical weighted-automata and +noncommutative PIT credit remains with Kiefer and Raz–Shpilka. Expanded +typed block-polynomial identities already occur in Philipp / mightyOil's +[PR1294](https://github.com/CrocSwap/integer-mult-bounds/pull/1294), following +Charles Bethin's PR1278. Krzysztof Wójt's PR5262 supplies a different, +inverse-aware equal-space model. No new general PIT algorithm, first typed +path algebra, or literature priority is claimed. The present contribution +is the typed compact interface, per-type path-witness construction, and +rerunnable implementation with complete dirty boundaries. + +## 1. Typed dependency representation + +Create one leaf atom x_i for each original register. Maintain each current +register as a scalar row of atoms of its own type. At a unary occurrence, +first read the entire old source row e. Introduce an atom z_j=X_a e, of +type t(a), with dependency row e supported on atoms of type s(a). APPLY +replaces its register row by the new unit row; QUERY adds c times that row. +Scalar operations update rows directly. This also specifies self queries: +they read the pre-instruction value. Dependencies point only to older atoms. +Thus exactly r+q atoms suffice without expanding paths. + +Let U be the final register rows. Define T_a to have dependency row e in +row j precisely when atom j was introduced with label a, and zero elsewhere. +Let V project leaf atoms to their original input register and other atoms +to zero. Induction on the dependency order gives + + coefficient of w=a_1...a_k in endpoint (o,i) + = (U T_a1 ... T_ak V)_(o,i). + +Matrix product order is literal: QP applies P first. A row supported on +atoms of type t(a) becomes a row supported on type s(a) after multiplication +by T_a; a mismatched arrow gives zero. Therefore every nonzero path has +the declared endpoint types. Empty paths are identities within one type. + +For a pair of programs take block diagonal transitions, concatenate their +final rows with a minus sign on the right, and stack their leaf projections. +The two compiled leaf copies project to the same original input roles. +They do not create additional independent payloads. This gives D states. + +## 2. Closure certificate and decision + +A certificate supplies reachable rows B_j=U_o T_w, an initial-span matrix H, +and closure matrices C_a satisfying + + U = H B, B T_a = C_a B for every a, B V = 0. + +These finite equations imply U T_w V=0 for every path by induction. Typed +paths form the basis of the free path algebra. Evaluating each arrow in its +declared rectangular block preserves addition, scalar multiplication and +composable products, so all complete endpoint blocks agree in every dimension. + +Conversely, if every typed coefficient is zero, the reachable row space is +annihilated by V and stable under all T_a. Choose a basis of reachable rows. +It has at most D elements and supplies H and C_a. The next section proves +that a nonzero coefficient contradicts universal equality, completing both +directions of the theorem. + +The producer processes independent rows breadth first, starting with U's +rows, and enqueues every composable arrow successor. A dependent candidate +is expressed using earlier accepted rows of no greater path length. Its +successors are therefore spanned by their successors. Induction on length +shows no shortest nonzero coefficient is lost by rejecting dependent rows. +The search accepts at most D rows, so a discovered path has length at most +D-1. Acyclic atom dependencies also bound its length by the program's maximum +unary dependency depth. Exact elimination constructs all displayed coordinates. + +The checker reconstructs the path rows and checks only the three equations; +it performs no elimination and does not need basis independence. A negative +certificate checks a nonzero coefficient and constructs the matrices below. +It does not certify shortestness. Shortestness is a property of the producer +and the proof, supplemented by explicit-word comparisons in the finite tests. + +## 3. Rectangular path witnesses + +Take a nonzero coefficient c in output o, input i and composable word +w=a_1...a_k. Let t_0 be the output type and t_j=s(a_j), so +a_j:t_j->t_(j-1) and t_k is the input type. For each t choose a basis + + {e_j : 0<=j<=k and t_j=t} + +of V_t. These basis vectors are distinct even when a type repeats. Define + + N_a e_(j+1) = e_j if a_(j+1)=a, + N_a e_l = 0 on every remaining basis vector. + +Equivalently, N_a is the sum of the matching rectangular matrix units. +Every factor decreases the global path index by exactly one. Thus a product +N_u has its (e_0,e_k) entry equal to one exactly when u=w. Shorter products +cannot traverse k steps; longer products vanish. Repeated vertices and +repeated arrow labels do not create shortcuts because coordinates retain +their global indices. Consequently input e_k in register i and zero in every +other register gives discrepancy c in output register o at coordinate e_0. +This proves the displayed dimension formula. For k=0 all arrows are zero, +the visited type has one coordinate, and the empty coefficient is detected. + +For a directed chain through distinct types every type must be nonzero for +its monomial to be nonzero. The construction uses exactly one coordinate at +each vertex. This observation does not assert a sharp general witness bound +when types repeat or different monomials interact. + +## 4. Tensor substitution and executable boundary + +A positive typed identity can be evaluated at X_a=G_a^(tensor f) for each +positive f, with register type space V_t^(tensor f). Rectangular composition +still commutes with tensor powers. Scalar c stays c, outside the tensor power; +the procedure never tensors an entire sum. This is an algebraic substitution +corollary, not native implementation or a complete supplier invoice. + +The theorem is over arbitrary fields. The executable uses exact Q only and +rejects excess resource sizes. It admits at most sixteen registers, eight +types, sixteen arrows, and 128 instructions per side, hence D<=288. Input +scalar encodings have at most 160 characters and 512 numerator/denominator +bits. Certificate scalars have at most 4096 characters and 8192 bits. A +larger certificate is explicitly refused by the producer. The unbounded +field-operation theorem does not claim executable success beyond these caps. +Program validation rejects mismatched types instead of coercing spaces. + +The checker shares the compiler, arithmetic, path reconstruction and witness +routine with the producer. Those components, the input transcription and +Python remain trusted. Explicit-word expansion and literal rectangular matrix +execution are separately implemented finite oracles. The proof is written +mathematics, not a proof-assistant theorem or independent human review. + +No relations between arrows, affine offsets, external aliases, nonlinear +operations or rounded endpoints are covered. Dirty restoration is checked +algebraically because every role is retained. Physical storage, native +delivery, precision, all-size compiler uniformity and the complete signed +invoice remain separate obligations. No new kappa is claimed. diff --git a/research/rectangular-dirty-certificates/README.md b/research/rectangular-dirty-certificates/README.md new file mode 100644 index 0000000000..83aa5bdc4b --- /dev/null +++ b/research/rectangular-dirty-certificates/README.md @@ -0,0 +1,102 @@ +# Compact universal certificates for rectangular dirty circuits + +This contribution was produced by Nick Petalas. Apache-2.0. + +This is a scoped written proof and exact implementation of the independent +rectangular-operator interface missing from zxv's [PR5235](https://github.com/CrocSwap/integer-mult-bounds/pull/5235). +Registers may belong to different payload spaces. An arrow has a fixed source +and target type, and every initial register is arbitrary. Equality certificates +retain all returned dirt. No supplier or new kappa is claimed. + +[PROOF.md](PROOF.md) extends the predecessor's r+q dependency-state method to +this interface. Two programs need D=2r+q_left+q_right states. An equality +certificate has at most D reachable rows and finite closure equations. +A nonzero path of length k has a concrete zero/one rectangular counterexample +using one coordinate per visit to each type, totaling k+1 coordinates. +This replaces padding every type to a common square witness dimension. +It is an upper bound, not a general minimum-dimension claim. + +The contribution adds the typed compact compiler, closure checker, explicit +per-type witnesses and runnable examples. Classical weighted-automata/PIT +methods and zxv's equal-space bridge retain their credit. Philipp / mightyOil's +PR1294 already proves expanded typed block identities following Charles Bethin +PR1278; that result is cited rather than reverified. Krzysztof Wójt's PR5262 +handles named inverses in a common space, a different operator model. The +retained dirty-echo lineage includes androolloyd, Chafik Boukhalfa / chafreaky +PR628 and Ali Romman PR621; the tensor and universal-phase lineage retains +Cinna Davis PR4100/4088, ToikY, Sagar Thakrar and roger-sato. + +## Reproduce + +From the repository root, using Python 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/rectangular-dirty-certificates +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/rectangular-dirty-certificates/verify.py +``` + +The registered normal and optimized checks print a generated JSON receipt +with source hashes. They write no files. The finite suite covers 160 program +pairs against explicit ordered-word expansion, 86 equal and 74 different; +all 74 differences have literal rectangular matrix witnesses. It also covers +64 dimension vectors and 352 full-column or zero-input echo cases, including +zero-dimensional spaces; six dirty product witnesses through degree six; +and fourteen rejecting or discrepancy controls. The degree-six example uses +type dimensions 4 and 3, totaling seven rather than a square padded total +of fourteen. That comparison concerns this path construction only. + +Run a single problem and check its inspectable certificate with a fresh output +path inside a scratch directory: + +```sh +PYTHON=/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 +"$PYTHON" -I -B research/rectangular-dirty-certificates/typed_words.py \ + research/rectangular-dirty-certificates/echo.json --output /tmp/rectangular-certificate.json +"$PYTHON" -I -B research/rectangular-dirty-certificates/check_certificate.py \ + research/rectangular-dirty-certificates/echo.json /tmp/rectangular-certificate.json +``` + +The output path must not exist. To inspect a negative matrix witness, replace +the two example paths with `chain6.json` and its committed `chain6.certificate.json`. +Arrow endpoints are `[source_type,target_type]`. Scalar instructions require +equal types. APPLY requires a loop; QUERY permits rectangular arrows. Scalars +are integers or explicit rational strings. Order QP means P applies first. + +## Scope and trust + +The executable uses Q. The written theorem works over any field. Inputs are +bounded to sixteen roles, eight types, sixteen arrows and 128 instructions per +side. Exact scalar encoding caps and the trusted shared compiler are documented +in PROOF.md. A scalar-size refusal is not a verdict of equality or inequality. +The checker performs no elimination; it shares compilation and arithmetic with +the producer. The two finite oracles are separately written, not independent +human reviewers. Independent human and formal proof-kernel review are unclaimed. + +Inverse, finite-group and commutation relations are excluded. So are native +implementation, nonlinear inputs, external aliases, rounding, precision, +hosting, physical tapes and a complete paid/target invoice. None of the five +selected framework assumptions is discharged, and the selected record is +unchanged. This is a changed scope from `joint-query-controller`: it supplies +an algebraic gate for mixed-width interfaces rather than a cheaper caller. +The card's selected-baseline orientation passed, with no supplier replay. + +Live open/merged searches, main README searches and reservations were checked +before the advance [claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19267728). +The overlap cache covered 317 open PRs and 5858 discussion records; the local +working search omitted 8486 sparse note paths, so main was also searched +directly for rectangular certificates, typed operators and quivers. This is +bounded overlap evidence, not proof of global novelty. + +## Open next questions + +- Bind a mixed-width supplier's literal source and complete endpoint to this + grammar. Start with one declared producer/consumer boundary and record all + arrows and dirt. Native relations or unpriced physical delivery may prevent + applying this independent-arrow test. +- Characterize the type graphs for which scalar spaces already separate all + paths. Start with acyclic graphs, then isolate the obstruction from multiple + cycles. This could reduce diagnostics further; no such classification or + random-testing guarantee is supplied here. + +Structured questions are in TASK.json. The first proved interface improvement +is frozen; these follow-ons are outside this contribution. diff --git a/research/rectangular-dirty-certificates/SOURCES.json b/research/rectangular-dirty-certificates/SOURCES.json new file mode 100644 index 0000000000..deb8636486 --- /dev/null +++ b/research/rectangular-dirty-certificates/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "3f0152a32eeebac0df11946dbd50cabe5a7f7839", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/inverse-dirty-certificates/README.md", + "usage": "input", + "git_blob": "1f895da66011f6ae59970cc0331b2fa00840568d", + "sha256": "e43549a712b8aab26b904b4da140b2924f7fee82407c5cdbe362303802456184" + }, + { + "path": "research/universal-dirty-certificates/PROOF.md", + "usage": "input", + "git_blob": "3a405e327a7fd5d59a570d7f9920f1ce7f229a76", + "sha256": "ef4cfcfd65b1dde1f11eedace0ed90a1b47a2cc100daaf778fbecbff3ec685a7" + }, + { + "path": "research/universal-dirty-phase-identities/README.md", + "usage": "input", + "git_blob": "fdebc9c89099f0f59b2b1cc4353bc33786529011", + "sha256": "3620ec8ae93b66af22d9dff045a339ff75160b4e6c334518a01768dd69e6a0ea" + } + ] +} diff --git a/research/rectangular-dirty-certificates/TASK.json b/research/rectangular-dirty-certificates/TASK.json new file mode 100644 index 0000000000..9f6485f456 --- /dev/null +++ b/research/rectangular-dirty-certificates/TASK.json @@ -0,0 +1,90 @@ +{ + "schema_version": 1, + "task_id": "joint-query-controller", + "priority_revision": 8, + "base_commit": "3f0152a32eeebac0df11946dbd50cabe5a7f7839", + "original_card": { + "id": "joint-query-controller", + "question": "Can a changed query demand or caller remove real work while satisfying native chronology and restoration?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Choose an exact caller and a new demand/interface hypothesis. Read the scoped #5617/#5631/#5649/#5747 and #5720/#5745 objections before rebuilding an excluded schedule. Compare the complete matched source/consumer protocols including all retained helper outputs. For an active-mode injection, first check #5745: its canonical delivery claim repays the eight removed centre jobs. Audit that exact claim or change its channel/feedback hypothesis; do not repeat the same free-injection search. Stop if the full favorable budget fails or the required restored output is unobservable.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "query demand", + "active mode", + "5720", + "5745", + "5747", + "caller" + ], + "existing_checks": [ + { + "scope": "PR #4166: author-checked installed producer/service/return/bridge connection; native-component comparison loses.", + "evidence": "research/qq16-caller-install/README.md", + "remaining": "Complete matched physical protocol bill, or changed source-compatible demand/circuit; no affordable supplier yet.", + "status": "author-checked", + "source_commit": "0b082d22a0e9a442d264ab0633e35ef26c790630", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Compact exact rational certificates and explicit per-type path witnesses for complete dirty linear programs with independent rectangular operators.", + "scope_change_reason": "This replaces the caller-cost experiment with the missing typed algebraic interface explicitly excluded by PR5235. It is a new compiler and proof, not an audit or a physical caller.", + "bottleneck_link": "Mixed-width producer/consumer programs need universal complete-boundary identities before their signed invoices can be compared. This package supplies only that algebraic gate.", + "budget_minutes": 60, + "stop_rule": "Stop after the first typed bridge, inspectable examples, literal rectangular witnesses and bounded exact replay; leave native adapters and further type-graph theory open.", + "outcome": "completed", + "evidence": "PROOF.md; registered normal/optimized verifier; explicit-word differential cases; zero/unequal-space matrix controls; per-type chain witnesses; generated source-hash receipts.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can an actual mixed-width supplier boundary be transcribed into this typed grammar?", + "why_it_matters": "The universal identity gate could then support a real changed caller.", + "first_step": "Pin its literal source, every arbitrary input and returned role, then declare all arrow types.", + "blocked_by": "No native relation-aware source adapter or paid physical invoice is supplied." + }, + { + "question": "Which type graphs admit faithful scalar path tests?", + "why_it_matters": "A structural criterion could reduce diagnostic dimensions further.", + "first_step": "Prove the acyclic case and identify a multiple-cycle obstruction.", + "blocked_by": "No type-graph classification or randomized certification theorem is supplied." + } + ] +} diff --git a/research/rectangular-dirty-certificates/VERIFY.json b/research/rectangular-dirty-certificates/VERIFY.json new file mode 100644 index 0000000000..415bbf15cd --- /dev/null +++ b/research/rectangular-dirty-certificates/VERIFY.json @@ -0,0 +1,38 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/inverse-dirty-certificates/README.md", + "research/universal-dirty-certificates/PROOF.md", + "research/universal-dirty-phase-identities/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Typed closure equations, explicit-word differential oracle, literal rectangular counterexamples, zero/unequal dimensions, dirty-return and corruption controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Typed closure equations, explicit-word differential oracle, literal rectangular counterexamples, zero/unequal dimensions, dirty-return and corruption controls." + } + ] +} diff --git a/research/rectangular-dirty-certificates/chain6.certificate.json b/research/rectangular-dirty-certificates/chain6.certificate.json new file mode 100644 index 0000000000..2c65fe8d16 --- /dev/null +++ b/research/rectangular-dirty-certificates/chain6.certificate.json @@ -0,0 +1,14 @@ +{ + "coefficient": "1", + "equal": false, + "input": 0, + "output": 6, + "word": [ + "a5", + "a4", + "a3", + "a2", + "a1", + "a0" + ] +} diff --git a/research/rectangular-dirty-certificates/chain6.json b/research/rectangular-dirty-certificates/chain6.json new file mode 100644 index 0000000000..90fb00615e --- /dev/null +++ b/research/rectangular-dirty-certificates/chain6.json @@ -0,0 +1,698 @@ +{ + "arrows": { + "a0": [ + "A", + "B" + ], + "a1": [ + "B", + "A" + ], + "a2": [ + "A", + "B" + ], + "a3": [ + "B", + "A" + ], + "a4": [ + "A", + "B" + ], + "a5": [ + "B", + "A" + ] + }, + "left": [ + { + "arrow": "a0", + "c": 1, + "dst": 1, + "op": "query", + "src": 0 + }, + { + "arrow": "a1", + "c": 1, + "dst": 2, + "op": "query", + "src": 1 + }, + { + "arrow": "a2", + "c": 1, + "dst": 3, + "op": "query", + "src": 2 + }, + { + "arrow": "a3", + "c": 1, + "dst": 4, + "op": "query", + "src": 3 + }, + { + "arrow": "a4", + "c": 1, + "dst": 5, + "op": "query", + "src": 4 + }, + { + "arrow": "a5", + "c": 1, + "dst": 6, + "op": "query", + "src": 5 + }, + { + "arrow": "a4", + "c": -1, + "dst": 5, + "op": "query", + "src": 4 + }, + { + "arrow": "a5", + "c": -1, + "dst": 6, + "op": "query", + "src": 5 + }, + { + "arrow": "a3", + "c": -1, + "dst": 4, + "op": "query", + "src": 3 + }, + { + "arrow": "a5", + "c": 1, + "dst": 6, + "op": "query", + "src": 5 + }, + { + "arrow": "a4", + "c": 1, + "dst": 5, + "op": "query", + "src": 4 + }, + { + "arrow": "a5", + "c": -1, + "dst": 6, + "op": "query", + "src": 5 + }, + { + "arrow": "a4", + "c": -1, + "dst": 5, + "op": "query", + "src": 4 + }, + { + "arrow": "a2", + "c": -1, + "dst": 3, + "op": "query", + "src": 2 + }, + { + "arrow": "a4", + "c": 1, + "dst": 5, + "op": "query", + "src": 4 + }, + { + "arrow": "a5", + "c": 1, + "dst": 6, + "op": "query", + "src": 5 + }, + { + "arrow": "a4", + "c": -1, + "dst": 5, + "op": "query", + "src": 4 + }, + { + "arrow": "a5", + "c": -1, + "dst": 6, + "op": "query", + "src": 5 + }, + { + "arrow": "a3", + "c": 1, + "dst": 4, + "op": "query", + "src": 3 + }, + { + "arrow": "a5", + "c": 1, + "dst": 6, + "op": "query", + "src": 5 + }, + { + "arrow": "a4", + "c": 1, + "dst": 5, + "op": "query", + "src": 4 + }, + { + "arrow": "a5", + "c": -1, + "dst": 6, + "op": "query", + "src": 5 + }, + { + "arrow": "a4", + "c": -1, + "dst": 5, + "op": "query", + "src": 4 + }, + { + "arrow": "a3", + "c": -1, + "dst": 4, + "op": "query", + "src": 3 + }, + { + "arrow": "a1", + "c": -1, + "dst": 2, + "op": "query", + "src": 1 + }, + { + "arrow": "a3", + "c": 1, + "dst": 4, + "op": "query", + "src": 3 + }, + { + "arrow": "a4", + "c": 1, + "dst": 5, + "op": "query", + "src": 4 + }, + { + "arrow": "a5", + "c": 1, + "dst": 6, + "op": "query", + "src": 5 + }, + { + "arrow": "a4", + "c": -1, + "dst": 5, + "op": "query", + "src": 4 + }, + { + "arrow": "a5", + "c": -1, + "dst": 6, + "op": "query", + "src": 5 + }, + { + "arrow": "a3", + "c": -1, + "dst": 4, + "op": "query", + "src": 3 + }, + { + "arrow": "a5", + "c": 1, + "dst": 6, + "op": "query", + "src": 5 + }, + { + "arrow": "a4", + "c": 1, + "dst": 5, + "op": "query", + "src": 4 + }, + { + "arrow": "a5", + "c": -1, + "dst": 6, + "op": "query", + "src": 5 + }, + { + "arrow": "a4", + "c": -1, + "dst": 5, + "op": "query", + "src": 4 + }, + { + "arrow": "a2", + "c": 1, + "dst": 3, + "op": "query", + "src": 2 + }, + { + "arrow": "a4", + "c": 1, + "dst": 5, + "op": "query", + "src": 4 + }, + { + "arrow": "a5", + "c": 1, + "dst": 6, + "op": "query", + "src": 5 + }, + { + "arrow": "a4", + "c": -1, + "dst": 5, + "op": "query", + "src": 4 + }, + { + "arrow": "a5", + "c": -1, + "dst": 6, + "op": "query", + "src": 5 + }, + { + "arrow": "a3", + "c": 1, + "dst": 4, + "op": "query", + "src": 3 + }, + { + "arrow": "a5", + "c": 1, + "dst": 6, + "op": "query", + "src": 5 + }, + { + "arrow": "a4", + "c": 1, + "dst": 5, + "op": "query", + "src": 4 + }, + { + "arrow": "a5", + "c": -1, + "dst": 6, + "op": "query", + "src": 5 + }, + { + "arrow": "a4", + "c": -1, + "dst": 5, + "op": "query", + "src": 4 + }, + { + "arrow": "a3", + "c": -1, + "dst": 4, + "op": "query", + "src": 3 + }, + { + "arrow": "a2", + "c": -1, + "dst": 3, + "op": "query", + "src": 2 + }, + { + "arrow": "a0", + "c": -1, + "dst": 1, + "op": "query", + "src": 0 + }, + { + "arrow": "a2", + "c": 1, + "dst": 3, + "op": "query", + "src": 2 + }, + { + "arrow": "a3", + "c": 1, + "dst": 4, + "op": "query", + "src": 3 + }, + { + "arrow": "a4", + "c": 1, + "dst": 5, + "op": "query", + "src": 4 + }, + { + "arrow": "a5", + "c": 1, + "dst": 6, + "op": "query", + "src": 5 + }, + { + "arrow": "a4", + "c": -1, + "dst": 5, + "op": "query", + "src": 4 + }, + { + "arrow": "a5", + "c": -1, + "dst": 6, + "op": "query", + "src": 5 + }, + { + "arrow": "a3", + "c": -1, + "dst": 4, + "op": "query", + "src": 3 + }, + { + "arrow": "a5", + "c": 1, + "dst": 6, + "op": "query", + "src": 5 + }, + { + "arrow": "a4", + "c": 1, + "dst": 5, + "op": "query", + "src": 4 + }, + { + "arrow": "a5", + "c": -1, + "dst": 6, + "op": "query", + "src": 5 + }, + { + "arrow": "a4", + "c": -1, + "dst": 5, + "op": "query", + "src": 4 + }, + { + "arrow": "a2", + "c": -1, + "dst": 3, + "op": "query", + "src": 2 + }, + { + "arrow": "a4", + "c": 1, + "dst": 5, + "op": "query", + "src": 4 + }, + { + "arrow": "a5", + "c": 1, + "dst": 6, + "op": "query", + "src": 5 + }, + { + "arrow": "a4", + "c": -1, + "dst": 5, + "op": "query", + "src": 4 + }, + { + "arrow": "a5", + "c": -1, + "dst": 6, + "op": "query", + "src": 5 + }, + { + "arrow": "a3", + "c": 1, + "dst": 4, + "op": "query", + "src": 3 + }, + { + "arrow": "a5", + "c": 1, + "dst": 6, + "op": "query", + "src": 5 + }, + { + "arrow": "a4", + "c": 1, + "dst": 5, + "op": "query", + "src": 4 + }, + { + "arrow": "a5", + "c": -1, + "dst": 6, + "op": "query", + "src": 5 + }, + { + "arrow": "a4", + "c": -1, + "dst": 5, + "op": "query", + "src": 4 + }, + { + "arrow": "a3", + "c": -1, + "dst": 4, + "op": "query", + "src": 3 + }, + { + "arrow": "a1", + "c": 1, + "dst": 2, + "op": "query", + "src": 1 + }, + { + "arrow": "a3", + "c": 1, + "dst": 4, + "op": "query", + "src": 3 + }, + { + "arrow": "a4", + "c": 1, + "dst": 5, + "op": "query", + "src": 4 + }, + { + "arrow": "a5", + "c": 1, + "dst": 6, + "op": "query", + "src": 5 + }, + { + "arrow": "a4", + "c": -1, + "dst": 5, + "op": "query", + "src": 4 + }, + { + "arrow": "a5", + "c": -1, + "dst": 6, + "op": "query", + "src": 5 + }, + { + "arrow": "a3", + "c": -1, + "dst": 4, + "op": "query", + "src": 3 + }, + { + "arrow": "a5", + "c": 1, + "dst": 6, + "op": "query", + "src": 5 + }, + { + "arrow": "a4", + "c": 1, + "dst": 5, + "op": "query", + "src": 4 + }, + { + "arrow": "a5", + "c": -1, + "dst": 6, + "op": "query", + "src": 5 + }, + { + "arrow": "a4", + "c": -1, + "dst": 5, + "op": "query", + "src": 4 + }, + { + "arrow": "a2", + "c": 1, + "dst": 3, + "op": "query", + "src": 2 + }, + { + "arrow": "a4", + "c": 1, + "dst": 5, + "op": "query", + "src": 4 + }, + { + "arrow": "a5", + "c": 1, + "dst": 6, + "op": "query", + "src": 5 + }, + { + "arrow": "a4", + "c": -1, + "dst": 5, + "op": "query", + "src": 4 + }, + { + "arrow": "a5", + "c": -1, + "dst": 6, + "op": "query", + "src": 5 + }, + { + "arrow": "a3", + "c": 1, + "dst": 4, + "op": "query", + "src": 3 + }, + { + "arrow": "a5", + "c": 1, + "dst": 6, + "op": "query", + "src": 5 + }, + { + "arrow": "a4", + "c": 1, + "dst": 5, + "op": "query", + "src": 4 + }, + { + "arrow": "a5", + "c": -1, + "dst": 6, + "op": "query", + "src": 5 + }, + { + "arrow": "a4", + "c": -1, + "dst": 5, + "op": "query", + "src": 4 + }, + { + "arrow": "a3", + "c": -1, + "dst": 4, + "op": "query", + "src": 3 + }, + { + "arrow": "a2", + "c": -1, + "dst": 3, + "op": "query", + "src": 2 + }, + { + "arrow": "a1", + "c": -1, + "dst": 2, + "op": "query", + "src": 1 + } + ], + "right": [], + "roles": [ + "A", + "B", + "A", + "B", + "A", + "B", + "A" + ] +} diff --git a/research/rectangular-dirty-certificates/check_certificate.py b/research/rectangular-dirty-certificates/check_certificate.py new file mode 100644 index 0000000000..89c0cc98a4 --- /dev/null +++ b/research/rectangular-dirty-certificates/check_certificate.py @@ -0,0 +1,65 @@ +"""Check rectangular closure equations without elimination or search.""" + +import argparse +import json +from pathlib import Path +import sys + +sys.path.insert(0, str(Path(__file__).resolve().parent)) + +from typed_words import (Q, advance, combine, compile_problem, path_row, + projection, require, scalar, witness) + + +def linear_combination(basis, encoded, dimension): + require(type(encoded) is list and len(encoded) == len(basis), "coordinate count") + row = [Q(0)] * dimension + for c, b in zip(encoded, basis, strict=True): + row = combine(row, b, scalar(c, certificate=True)) + return row + + +def check(problem, certificate): + model = compile_problem(problem) + require(type(certificate) is dict and type(certificate.get("equal")) is bool, + "certificate must contain Boolean equal") + if not certificate["equal"]: + require(set(certificate) == {"equal", "output", "word", "input", "coefficient"}, + "negative certificate keys") + return witness(problem, certificate) + require(set(certificate) == {"equal", "basis", "initial", "closure"}, "positive certificate keys") + paths = certificate["basis"] + d = len(model["types"]) + require(type(paths) is list and len(paths) <= d, "basis bound") + basis = [] + for path in paths: + require(type(path) is dict and set(path) == {"output", "word"}, "path keys") + row, _ = path_row(model, path["output"], path["word"]) + require(not any(projection(model, row)), "nonzero final projection") + basis.append(row) + initial, closure = certificate["initial"], certificate["closure"] + require(type(initial) is list and len(initial) == len(model["roles"]), "initial count") + for expected, encoded in zip(model["output"], initial, strict=True): + require(expected == linear_combination(basis, encoded, d), "initial-span equation") + require(type(closure) is dict and set(closure) == set(model["arrows"]), "closure alphabet") + for a, rows in closure.items(): + require(type(rows) is list and len(rows) == len(basis), "closure row count") + for b, encoded in zip(basis, rows, strict=True): + require(advance(model, b, a) == linear_combination(basis, encoded, d), + "closure equation") + return {"equal": True, "states": d, "basis_rows": len(basis)} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("problem", type=Path) + parser.add_argument("certificate", type=Path) + args = parser.parse_args() + for path in (args.problem, args.certificate): + require(path.stat().st_size <= 16_000_000, "input file too large") + print(json.dumps(check(json.loads(args.problem.read_text()), + json.loads(args.certificate.read_text())), sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/rectangular-dirty-certificates/echo.certificate.json b/research/rectangular-dirty-certificates/echo.certificate.json new file mode 100644 index 0000000000..dfe2b0ca8e --- /dev/null +++ b/research/rectangular-dirty-certificates/echo.certificate.json @@ -0,0 +1,97 @@ +{ + "basis": [ + { + "output": 0, + "word": [] + }, + { + "output": 1, + "word": [] + }, + { + "output": 2, + "word": [] + }, + { + "output": 2, + "word": [ + "Q" + ] + } + ], + "closure": { + "P": [ + [ + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0" + ], + [ + "1", + "0", + "0", + "0" + ] + ], + "Q": [ + [ + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "1" + ], + [ + "0", + "0", + "0", + "0" + ] + ] + }, + "equal": true, + "initial": [ + [ + "1", + "0", + "0", + "0" + ], + [ + "0", + "1", + "0", + "0" + ], + [ + "0", + "0", + "1", + "0" + ] + ] +} diff --git a/research/rectangular-dirty-certificates/echo.json b/research/rectangular-dirty-certificates/echo.json new file mode 100644 index 0000000000..d0b3943323 --- /dev/null +++ b/research/rectangular-dirty-certificates/echo.json @@ -0,0 +1,77 @@ +{ + "arrows": { + "P": [ + "A", + "B" + ], + "Q": [ + "B", + "C" + ] + }, + "left": [ + { + "arrow": "P", + "c": 1, + "dst": 1, + "op": "query", + "src": 0 + }, + { + "arrow": "Q", + "c": 1, + "dst": 2, + "op": "query", + "src": 1 + }, + { + "arrow": "P", + "c": -1, + "dst": 1, + "op": "query", + "src": 0 + }, + { + "arrow": "Q", + "c": -1, + "dst": 2, + "op": "query", + "src": 1 + } + ], + "right": [ + { + "arrow": "Q", + "c": -1, + "dst": 2, + "op": "query", + "src": 1 + }, + { + "arrow": "P", + "c": 1, + "dst": 1, + "op": "query", + "src": 0 + }, + { + "arrow": "Q", + "c": 1, + "dst": 2, + "op": "query", + "src": 1 + }, + { + "arrow": "P", + "c": -1, + "dst": 1, + "op": "query", + "src": 0 + } + ], + "roles": [ + "A", + "B", + "C" + ] +} diff --git a/research/rectangular-dirty-certificates/typed_words.py b/research/rectangular-dirty-certificates/typed_words.py new file mode 100644 index 0000000000..be0b3b6d2c --- /dev/null +++ b/research/rectangular-dirty-certificates/typed_words.py @@ -0,0 +1,242 @@ +"""Compact typed free-operator certificates. Apache-2.0; Nick Petalas. + +Extends zxv's PR5235 dependency-state construction to rectangular maps. +The compiler is shared with the checker and belongs to the trusted surface. +""" + +import argparse +from fractions import Fraction as Q +import json +from pathlib import Path + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def scalar(value, certificate=False): + require(type(value) in (int, str), "scalar must be an integer or fraction string") + require(len(str(value)) <= (4096 if certificate else 160), "scalar encoding too long") + require("." not in str(value) and "e" not in str(value).lower(), "use explicit fractions") + result = Q(value) + require(max(abs(result.numerator).bit_length(), result.denominator.bit_length()) <= + (8192 if certificate else 512), + "scalar too large") + return result + + +def validate(problem): + require(type(problem) is dict, "problem must be an object") + require(set(problem) == {"roles", "arrows", "left", "right"}, "unexpected problem keys") + roles, arrows = problem["roles"], problem["arrows"] + require(type(roles) is list and 1 <= len(roles) <= 16, "role count must be 1..16") + require(all(type(t) is str and 1 <= len(t) <= 32 for t in roles), "invalid role type") + require(len(set(roles)) <= 8, "at most eight types") + require(type(arrows) is dict and len(arrows) <= 16, "at most sixteen arrows") + for name, ends in arrows.items(): + require(type(name) is str and 1 <= len(name) <= 32, "invalid arrow name") + require(type(ends) is list and len(ends) == 2 and all(t in roles for t in ends), + "arrow endpoints must be declared role types") + for side in ("left", "right"): + program = problem[side] + require(type(program) is list and len(program) <= 128, "at most 128 instructions per side") + for ins in program: + validate_instruction(ins, roles, arrows) + return problem + + +def validate_instruction(ins, roles, arrows): + require(type(ins) is dict and "op" in ins, "instruction must have an op") + op = ins["op"] + keys = {"add": {"op", "src", "dst", "c"}, "scale": {"op", "dst", "c"}, + "swap": {"op", "src", "dst"}, "query": {"op", "src", "dst", "arrow", "c"}, + "apply": {"op", "dst", "arrow"}} + require(type(op) is str and op in keys and set(ins) == keys[op], "invalid instruction keys") + for key in ("src", "dst"): + if key in ins: + require(type(ins[key]) is int and 0 <= ins[key] < len(roles), "invalid register") + if "c" in ins: + scalar(ins["c"]) + if op in ("add", "swap"): + require(roles[ins["src"]] == roles[ins["dst"]], "scalar operation crosses types") + if op in ("query", "apply"): + require(type(ins["arrow"]) is str and ins["arrow"] in arrows, "unknown arrow") + src = ins.get("src", ins["dst"]) + require(arrows[ins["arrow"]] == [roles[src], roles[ins["dst"]]], "ill-typed arrow") + + +def combine(x, y, c=Q(1)): + return [a + c * b for a, b in zip(x, y, strict=True)] + + +def compile_side(problem, side): + r = len(problem["roles"]) + n = r + sum(ins["op"] in ("query", "apply") for ins in problem[side]) + registers = [[Q(i == j) for j in range(n)] for i in range(r)] + atoms = list(problem["roles"]) + transitions = {a: [] for a in problem["arrows"]} + cursor = r + for ins in problem[side]: + op, dst = ins["op"], ins["dst"] + if op == "add": + registers[dst] = combine(registers[dst], registers[ins["src"]], scalar(ins["c"])) + elif op == "scale": + registers[dst] = [scalar(ins["c"]) * v for v in registers[dst]] + elif op == "swap": + src = ins["src"] + registers[src], registers[dst] = registers[dst], registers[src] + else: + source = ins.get("src", dst) + transitions[ins["arrow"]].append((cursor, registers[source][:])) + atoms.append(problem["roles"][dst]) + unit = [Q(j == cursor) for j in range(n)] + registers[dst] = unit if op == "apply" else combine(registers[dst], unit, scalar(ins["c"])) + cursor += 1 + assert cursor == n and len(atoms) == n + return registers, transitions, atoms + + +def compile_problem(problem): + validate(problem) + u, t, types_left = compile_side(problem, "left") + v, s, types_right = compile_side(problem, "right") + n, m = len(types_left), len(types_right) + output = [x + [-a for a in y] for x, y in zip(u, v, strict=True)] + transitions = {} + for arrow in t: + transitions[arrow] = [(j, row + [Q(0)] * m) for j, row in t[arrow]] + transitions[arrow] += [(n + j, [Q(0)] * n + row) for j, row in s[arrow]] + return {"output": output, "transitions": transitions, "types": types_left + types_right, + "right_offset": n, "roles": problem["roles"], "arrows": problem["arrows"]} + + +def advance(model, row, arrow): + result = [Q(0)] * len(row) + for j, dependency in model["transitions"][arrow]: + if row[j]: + result = combine(result, dependency, row[j]) + return result + + +def projection(model, row): + offset = model["right_offset"] + return [row[i] + row[offset + i] for i in range(len(model["roles"]))] + + +def path_row(model, output, word): + require(type(output) is int and 0 <= output < len(model["roles"]), "invalid output") + require(type(word) is list and len(word) < len(model["types"]), "invalid path length") + row = model["output"][output][:] + current = model["roles"][output] + for arrow in word: + require(type(arrow) is str and arrow in model["arrows"], "unknown path arrow") + source, target = model["arrows"][arrow] + require(current == target, "noncomposable certificate path") + row = advance(model, row, arrow) + current = source + return row, current + + +def reduce_row(row, echelon): + rest = row[:] + coefficients = [Q(0)] * len(row) + for pivot, normal, coordinates in echelon: + c = rest[pivot] + if c: + rest = combine(rest, normal, -c) + coefficients = combine(coefficients, coordinates, c) + return rest, coefficients + + +def extend_basis(row, description, basis, paths, echelon): + rest, coefficients = reduce_row(row, echelon) + if not any(rest): + return + pivot = next(i for i, v in enumerate(rest) if v) + gain = rest[pivot] + normal = [v / gain for v in rest] + coordinates = [-v / gain for v in coefficients] + coordinates[len(basis)] += 1 / gain + echelon.append((pivot, normal, coordinates)) + basis.append(row) + paths.append(description) + + +def coordinates(row, echelon, size): + rest, result = reduce_row(row, echelon) + require(not any(rest), "closure construction failed") + encoded = [str(c) for c in result[:size]] + for value in encoded: + scalar(value, certificate=True) + return encoded + + +def decide(problem): + model = compile_problem(problem) + basis, paths, echelon = [], [], [] + for i, row in enumerate(model["output"]): + extend_basis(row, {"output": i, "word": []}, basis, paths, echelon) + d = len(model["types"]) + for cursor in range(d): + if cursor == len(basis): + break + row, path = basis[cursor], paths[cursor] + image = projection(model, row) + if any(image): + i = next(i for i, c in enumerate(image) if c) + scalar(str(image[i]), certificate=True) + return {"equal": False, **path, "input": i, "coefficient": str(image[i])} + _, current = path_row(model, path["output"], path["word"]) + for a, (_, target) in model["arrows"].items(): + if target == current: + extend_basis(advance(model, row, a), + {"output": path["output"], "word": path["word"] + [a]}, + basis, paths, echelon) + assert len(basis) <= d + return {"equal": True, "basis": paths, + "initial": [coordinates(row, echelon, len(basis)) for row in model["output"]], + "closure": {a: [coordinates(advance(model, row, a), echelon, len(basis)) + for row in basis] for a in model["arrows"]}} + + +def witness(problem, certificate): + model = compile_problem(problem) + row, current = path_row(model, certificate["output"], certificate["word"]) + i = certificate["input"] + require(type(i) is int and 0 <= i < len(model["roles"]), "invalid input") + require(current == model["roles"][i], "witness input has wrong type") + c = projection(model, row)[i] + require(c != 0 and c == scalar(certificate["coefficient"], certificate=True), "false discrepancy") + visits = [model["roles"][certificate["output"]]] + for a in certificate["word"]: + visits.append(model["arrows"][a][0]) + positions = {t: [j for j, v in enumerate(visits) if v == t] for t in set(model["roles"])} + matrices = {} + for a, (src, dst) in model["arrows"].items(): + matrix = [[0] * len(positions[src]) for _ in positions[dst]] + for j, letter in enumerate(certificate["word"]): + if letter == a: + matrix[positions[dst].index(j)][positions[src].index(j + 1)] = 1 + matrices[a] = matrix + return {"dimensions": {t: len(p) for t, p in positions.items()}, "matrices": matrices, + "input_coordinate": positions[current].index(len(visits) - 1), + "output_coordinate": positions[visits[0]].index(0), "coefficient": str(c)} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("problem", type=Path) + parser.add_argument("--output", required=True, type=Path) + args = parser.parse_args() + require(args.problem.stat().st_size <= 1_000_000, "problem file too large") + result = decide(json.loads(args.problem.read_text())) + encoded = json.dumps(result, indent=2, sort_keys=True) + "\n" + require(len(encoded.encode()) <= 16_000_000, "certificate file too large") + with args.output.open("x") as stream: + require(stream.write(encoded) == len(encoded), "short certificate write") + print("EQUAL" if result["equal"] else "DIFFERENT") + + +if __name__ == "__main__": + main() diff --git a/research/rectangular-dirty-certificates/verify.py b/research/rectangular-dirty-certificates/verify.py new file mode 100644 index 0000000000..00ae4dedb8 --- /dev/null +++ b/research/rectangular-dirty-certificates/verify.py @@ -0,0 +1,254 @@ +"""Finite corroboration of the typed closure and path-witness theorem.""" + +from copy import deepcopy +from fractions import Fraction +import hashlib +import json +from pathlib import Path +import random +import sys + +sys.path.insert(0, str(Path(__file__).resolve().parent)) + +from check_certificate import check +from typed_words import decide, require, validate, witness + + +def expanded(problem, side): + """Independent literal path expansion, used only for small fixtures.""" + registers = [{(i, ()): Fraction(1)} for i in range(len(problem["roles"]))] + for ins in problem[side]: + op, d = ins["op"], ins["dst"] + if op == "swap": + s = ins["src"] + registers[s], registers[d] = registers[d], registers[s] + continue + if op == "scale": + registers[d] = {k: Fraction(ins["c"]) * v for k, v in registers[d].items() if v} + continue + s = ins.get("src", d) + source = registers[s].copy() + if op in ("query", "apply"): + source = {(i, (ins["arrow"],) + w): c for (i, w), c in source.items()} + if op == "apply": + registers[d] = source + continue + for k, v in source.items(): + registers[d][k] = registers[d].get(k, 0) + Fraction(ins["c"]) * v + registers[d] = {k: v for k, v in registers[d].items() if v} + return [{k: v for k, v in row.items() if v} for row in registers] + + +def residual(problem): + result = [] + for left, right in zip(expanded(problem, "left"), expanded(problem, "right"), strict=True): + row = {k: left.get(k, 0) - right.get(k, 0) for k in left.keys() | right.keys()} + result.append({k: v for k, v in row.items() if v}) + return result + + +def execute(problem, side, matrices, initial): + """Literal rectangular matrix execution, independent of dependency states.""" + values = [row[:] for row in initial] + for ins in problem[side]: + op, d = ins["op"], ins["dst"] + if op == "swap": + s = ins["src"] + values[s], values[d] = values[d], values[s] + continue + if op == "scale": + values[d] = [Fraction(ins["c"]) * v for v in values[d]] + continue + source = values[ins.get("src", d)][:] + if op in ("query", "apply"): + source = [sum(a * b for a, b in zip(row, source, strict=True)) + for row in matrices[ins["arrow"]]] + if op == "apply": + values[d] = source + else: + values[d] = [a + Fraction(ins["c"]) * b for a, b in zip(values[d], source, strict=True)] + return values + + +def literal_witness(problem, certificate): + concrete = witness(problem, certificate) + initial = [[0] * concrete["dimensions"][t] for t in problem["roles"]] + initial[certificate["input"]][concrete["input_coordinate"]] = 1 + left = execute(problem, "left", concrete["matrices"], initial) + right = execute(problem, "right", concrete["matrices"], initial) + o, j = certificate["output"], concrete["output_coordinate"] + require(left[o][j] - right[o][j] == Fraction(certificate["coefficient"]), "literal witness failed") + require(sum(concrete["dimensions"].values()) == len(certificate["word"]) + 1, "visit-count bound") + return concrete + + +def query(src, dst, arrow, c=1): + return {"op": "query", "src": src, "dst": dst, "arrow": arrow, "c": c} + + +def echo_problem(): + return {"roles": ["A", "B", "C"], "arrows": {"P": ["A", "B"], "Q": ["B", "C"]}, + "left": [query(0, 1, "P"), query(1, 2, "Q"), query(0, 1, "P", -1), query(1, 2, "Q", -1)], + "right": [query(1, 2, "Q", -1), query(0, 1, "P"), query(1, 2, "Q"), query(0, 1, "P", -1)]} + + +def random_problem(rng, index): + roles = ["A", "B", "A", "C"] + arrows = {f"{s}{t}": [s, t] for s in ("A", "B", "C") for t in ("A", "B", "C")} + left = [] + for _ in range(9): + s, d = rng.randrange(4), rng.randrange(4) + op = rng.randrange(5) + c = rng.choice(["1/2", "-3/2", -1, 0, 1, 2]) + if op == 0: + left.append({"op": "scale", "dst": d, "c": c}) + elif op == 1: + left.append({"op": "apply", "dst": d, "arrow": roles[d] * 2}) + elif op == 2 and roles[s] == roles[d]: + left.append({"op": "swap", "src": s, "dst": d}) + elif op == 3 and roles[s] == roles[d]: + left.append({"op": "add", "src": s, "dst": d, "c": c}) + else: + left.append(query(s, d, roles[s] + roles[d], c)) + right = deepcopy(left) + if index % 2: + right.append(query(0, 1, "AB", rng.choice([-1, "1/2", 2]))) + else: + right += [query(1, 3, "BC"), query(1, 3, "BC", -1)] + return {"roles": roles, "arrows": arrows, "left": left, "right": right} + + +def chain_problem(length): + """Iterative dirty commutator construction; no recursive Python calls.""" + roles = ["A" if j % 2 == 0 else "B" for j in range(length + 1)] + arrows = {f"a{j}": [roles[j], roles[j + 1]] for j in range(length)} + word = [query(length - 1, length, f"a{length - 1}")] + for j in range(length - 2, -1, -1): + inverse = [{**ins, "c": -ins["c"]} for ins in reversed(word)] + word = [query(j, j + 1, f"a{j}")] + word + [query(j, j + 1, f"a{j}", -1)] + inverse + return {"roles": roles, "arrows": arrows, "left": word, "right": []} + + +def verify_differentials(): + rng = random.Random(780231) + counts = {"program_pairs": 0, "equal": 0, "different": 0, "literal_witnesses": 0} + for i in range(160): + problem = random_problem(rng, i) + expected = residual(problem) + certificate = decide(problem) + check(problem, certificate) + require(certificate["equal"] == (not any(expected)), "explicit-word verdict disagrees") + counts["program_pairs"] += 1 + if certificate["equal"]: + counts["equal"] += 1 + else: + counts["different"] += 1 + o, s, w = certificate["output"], certificate["input"], tuple(certificate["word"]) + require(expected[o][s, w] == Fraction(certificate["coefficient"]), "coefficient disagreement") + require(len(w) == min(len(k[1]) for row in expected for k in row), "not shortest") + literal_witness(problem, certificate) + counts["literal_witnesses"] += 1 + return counts + + +def verify_echo(): + problem = echo_problem() + certificate = decide(problem) + result = check(problem, certificate) + require(certificate["equal"], "rectangular echo mismatch") + rng = random.Random(91) + cases = 0 + for a in range(4): + for b in range(4): + for c in range(4): + dims = {"A": a, "B": b, "C": c} + matrices = {k: [[rng.randrange(-2, 3) for _ in range(dims[s])] + for _ in range(dims[t])] for k, (s, t) in problem["arrows"].items()} + width = sum(dims[t] for t in problem["roles"]) + for axis in range(width + 1): + initial = [[0] * dims[t] for t in problem["roles"]] + flat = [(r, j) for r, t in enumerate(problem["roles"]) for j in range(dims[t])] + if axis < width: + r, j = flat[axis] + initial[r][j] = 1 + require(execute(problem, "left", matrices, initial) == + execute(problem, "right", matrices, initial), "unequal-space echo") + cases += 1 + return {**result, "dimension_vectors": 64, "full_column_or_zero_tests": cases}, certificate + + +def must_reject(callback): + try: + callback() + except (ValueError, TypeError, KeyError, ZeroDivisionError): + return + raise ValueError("invalid control accepted") + + +def verify_controls(certificate): + controls = [] + for name in ("arrow-type", "cross-type-add", "bad-index", "float", "zero-denominator", "unknown-op"): + p = echo_problem() + if name == "arrow-type": p["left"][0]["arrow"] = "Q" + if name == "cross-type-add": p["left"][0] = {"op": "add", "src": 0, "dst": 1, "c": 1} + if name == "bad-index": p["left"][0]["src"] = True + if name == "float": p["left"][0]["c"] = 0.5 + if name == "zero-denominator": p["left"][0]["c"] = "1/0" + if name == "unknown-op": p["left"][0]["op"] = "erase" + must_reject(lambda: validate(p)) + controls.append(name) + for name in ("initial", "closure", "basis", "missing-arrow", "nonboolean"): + bad = deepcopy(certificate) + if name == "initial": bad["initial"][0][0] = str(Fraction(bad["initial"][0][0]) + 1) + if name == "closure": bad["closure"]["P"][0][0] = str(Fraction(bad["closure"]["P"][0][0]) + 1) + if name == "basis": bad["basis"][0]["word"] = ["P", "Q"] + if name == "missing-arrow": del bad["closure"]["P"] + if name == "nonboolean": bad["equal"] = 1 + must_reject(lambda: check(echo_problem(), bad)) + controls.append(name) + for event in (0, 2, 3): + p = echo_problem() + del p["left"][event] + c = decide(p) + require(not c["equal"], "missing restoration/sign not detected") + check(p, c) + literal_witness(p, c) + controls.append(f"deleted-event-{event}") + return controls + + +def main(): + root = Path(__file__).resolve().parent + sources = json.loads((root / "SOURCES.json").read_text()) + repo = root.parent.parent + for item in sources["files"]: + if item["usage"] == "input": + require(hashlib.sha256((repo / item["path"]).read_bytes()).hexdigest() == item["sha256"], + f"source bytes changed: {item['path']}") + differentials = verify_differentials() + echo, certificate = verify_echo() + controls = verify_controls(certificate) + chains = [] + for length in range(1, 7): + p = chain_problem(length) + c = decide(p) + require(not c["equal"] and len(c["word"]) == length, "chain degree") + check(p, c) + w = literal_witness(p, c) + require(not any(residual(p)[:-1]), "chain lost dirty input") + chains.append({"length": length, "instructions": len(p["left"]), + "dimensions": w["dimensions"], "coefficient": c["coefficient"]}) + for name, expected in (("echo", echo_problem()), ("chain6", chain_problem(6))): + problem = json.loads((root / f"{name}.json").read_text()) + saved = json.loads((root / f"{name}.certificate.json").read_text()) + require(problem == expected and saved == decide(problem), "committed example mismatch") + check(problem, saved) + files = {p.name: hashlib.sha256(p.read_bytes()).hexdigest() + for p in sorted(root.iterdir()) if p.is_file()} + print(json.dumps({"status": "PASS_RECTANGULAR_DIRTY_CERTIFICATES", "differentials": differentials, + "echo": echo, "chain_witnesses": chains, "controls": controls, + "source_hashes": files}, sort_keys=True)) + + +if __name__ == "__main__": + main()