diff --git a/research/p104-cut353-independent-audit/CASES.json b/research/p104-cut353-independent-audit/CASES.json new file mode 100644 index 0000000000..76bdeebba2 --- /dev/null +++ b/research/p104-cut353-independent-audit/CASES.json @@ -0,0 +1,22 @@ +{ + "schema_version": 1, + "scope": "PR6716 cut353 fresh34 conditional LOCAL audit", + "source_head": "a467457692bc9e11113d9b2e2e34ea8ffb553b58", + "unretired_roles": 34, + "unretired_events": 562, + "final_roles": 35, + "final_events": 586, + "cut_after": 353, + "handoff_after": 362, + "fresh_first_contact": 363, + "pivot": 4, + "fresh": 34, + "equal_target_group": [4, 20, 21], + "fresh_stages": [10, 11, 12, 13], + "ring": "Q(i)[u]/(u^4-1)[t1^+-1,...,t18^+-1];u=sourceQ;proofq=u^-1", + "normalized_central": "((1+i)/2)*u^3+((1-i)/2)*u", + "expected_original_pivot": "u^3 without stage factors", + "expected_fresh_output": "t10*t11*t12*t13 without central factor", + "limits": {"seconds": 180, "input_bytes": 16777216, "artifact_bytes": 4194304, "simultaneous_matrix_terms": 100000}, + "excluded": ["common_idle_physical_bank", "native_LOCAL_realization", "complete_invoice", "compiler", "outer_transfer", "frontier_admission"] +} diff --git a/research/p104-cut353-independent-audit/NOTICE b/research/p104-cut353-independent-audit/NOTICE new file mode 100644 index 0000000000..03449aae49 --- /dev/null +++ b/research/p104-cut353-independent-audit/NOTICE @@ -0,0 +1,12 @@ +Independent logical cut353 audit. New material: substantial OpenAI Codex +assistance, Apache-2.0. This is a source-bound independent audit rather than +a new construction or frontier claim. + +Retain thu-nmrc/PR6716's root, two-sided witness and caller application; +DreamingOfClouds/PR6702's native word with Claude assistance; Ali Romman's +PR6348/6398 binary/root work and Cinna Davis's query/controller lineage; +PR6545 and PR5599's two-sided retirement method; PR6551's rebalanced +comparison; and all earlier native/helper, Clifford, compiler, BIT, +precision and analytic contributors and source-specific notices. + +Frozen original source texts remain unmodified and retain their notices. diff --git a/research/p104-cut353-independent-audit/ORACLE.json b/research/p104-cut353-independent-audit/ORACLE.json new file mode 100644 index 0000000000..2236f38219 --- /dev/null +++ b/research/p104-cut353-independent-audit/ORACLE.json @@ -0,0 +1,20 @@ +{ + "artifact_sha256": "ca09e50e074afde1af921461618e2f1d8349c643a16a6db0683f2a7efcd8e579", + "case_manifest_sha256": "7a7e961a1971c31653770af43b0097ba55d1eb980795a050c74786e8f5c7d6c0", + "cut_after": 353, + "cut_cells": 68, + "final_cells": 1225, + "final_events": 586, + "final_roles": 35, + "fresh": 34, + "fresh_first_contact": 363, + "handoff_after": 362, + "ordinary_identities": 6, + "pivot": 4, + "schema_version": 1, + "scope": "PR6716 cut353 fresh34 conditional LOCAL audit", + "source_manifest_sha256": "0de615eb3eac51539567c56e85e177c91c0d3e5c2c69b8cd64abff46f68fc902", + "stages": 18, + "unretired_events": 562, + "unretired_roles": 34 +} diff --git a/research/p104-cut353-independent-audit/PACKET.json b/research/p104-cut353-independent-audit/PACKET.json new file mode 100644 index 0000000000..609fe26b7b --- /dev/null +++ b/research/p104-cut353-independent-audit/PACKET.json @@ -0,0 +1 @@ +{"a_prefix":[[],[],[],[],[[1,[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],[-1,2,1,2]],[3,[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],[-1,2,-1,2]]],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[[1,[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],[1,2,-1,2]],[3,[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],[1,2,1,2]]],[],[],[],[],[],[],[],[],[],[],[],[],[]],"final_matrix":[[[[3,[1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1],[1,1,0,1]]],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[]],[[],[[3,[1,1,1,1,1,1,1,1,1,0,0,0,0,0,0,0,0,0],[1,1,0,1]]],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[]],[[],[],[[3,[0,0,0,0,0,0,0,0,0,1,1,1,1,1,1,1,1,1],[1,1,0,1]]],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[]],[[],[],[],[[3,[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],[1,1,0,1]]],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[]],[[],[],[],[],[[3,[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],[1,1,0,1]]],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[]],[[],[],[],[],[],[[3,[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],[1,1,0,1]]],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[]],[[],[],[],[],[],[],[[3,[0,0,0,0,1,1,1,1,1,0,0,0,0,0,0,0,0,0],[1,1,0,1]]],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[]],[[],[],[],[],[],[],[],[[3,[0,0,0,0,1,1,1,1,1,0,0,0,0,0,0,0,0,0],[1,1,0,1]]],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[]],[[],[],[],[],[],[],[],[],[[3,[1,1,1,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0],[1,1,0,1]]],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[]],[[],[],[],[],[],[],[],[],[],[[3,[1,1,1,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0],[1,1,0,1]]],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[]],[[],[],[],[],[],[],[],[],[],[],[[3,[1,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],[1,1,0,1]]],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[]],[[],[],[],[],[],[],[],[],[],[],[],[[3,[1,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],[1,1,0,1]]],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[]],[[],[],[],[],[],[],[],[],[],[],[],[],[[3,[0,0,1,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0],[1,1,0,1]]],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[]],[[],[],[],[],[],[],[],[],[],[],[],[],[],[[3,[0,0,1,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0],[1,1,0,1]]],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[]],[[],[],[],[],[],[],[],[],[],[],[],[],[],[],[[3,[0,0,0,0,1,1,0,0,0,0,0,0,0,0,0,0,0,0],[1,1,0,1]]],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[]],[[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[[3,[0,0,0,0,1,1,0,0,0,0,0,0,0,0,0,0,0,0],[1,1,0,1]]],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[]],[[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[[3,[0,0,0,0,0,0,1,1,1,0,0,0,0,0,0,0,0,0],[1,1,0,1]]],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[]],[[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[[3,[0,0,0,0,0,0,1,1,1,0,0,0,0,0,0,0,0,0],[1,1,0,1]]],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[]],[[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[[3,[0,0,0,0,0,0,0,1,1,0,0,0,0,0,0,0,0,0],[1,1,0,1]]],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[]],[[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[[3,[0,0,0,0,0,0,0,1,1,0,0,0,0,0,0,0,0,0],[1,1,0,1]]],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[]],[[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[[3,[0,0,0,0,0,0,0,0,0,1,1,1,1,0,0,0,0,0],[1,1,0,1]]],[],[],[],[],[],[],[],[],[],[],[],[],[],[]],[[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[[3,[0,0,0,0,0,0,0,0,0,1,1,1,1,0,0,0,0,0],[1,1,0,1]]],[],[],[],[],[],[],[],[],[],[],[],[],[]],[[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[[3,[0,0,0,0,0,0,0,0,0,1,1,0,0,0,0,0,0,0],[1,1,0,1]]],[],[],[],[],[],[],[],[],[],[],[],[]],[[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[[3,[0,0,0,0,0,0,0,0,0,1,1,0,0,0,0,0,0,0],[1,1,0,1]]],[],[],[],[],[],[],[],[],[],[],[]],[[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[[3,[0,0,0,0,0,0,0,0,0,0,0,1,1,0,0,0,0,0],[1,1,0,1]]],[],[],[],[],[],[],[],[],[],[]],[[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[[3,[0,0,0,0,0,0,0,0,0,0,0,1,1,0,0,0,0,0],[1,1,0,1]]],[],[],[],[],[],[],[],[],[]],[[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[[3,[0,0,0,0,0,0,0,0,0,0,0,0,0,1,1,1,1,1],[1,1,0,1]]],[],[],[],[],[],[],[],[]],[[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[[3,[0,0,0,0,0,0,0,0,0,0,0,0,0,1,1,1,1,1],[1,1,0,1]]],[],[],[],[],[],[],[]],[[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[[3,[0,0,0,0,0,0,0,0,0,0,0,0,0,1,1,0,0,0],[1,1,0,1]]],[],[],[],[],[],[]],[[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[[3,[0,0,0,0,0,0,0,0,0,0,0,0,0,1,1,0,0,0],[1,1,0,1]]],[],[],[],[],[]],[[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[[3,[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,1,1],[1,1,0,1]]],[],[],[],[]],[[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[[3,[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,1,1],[1,1,0,1]]],[],[],[]],[[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[[3,[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,1],[1,1,0,1]]],[],[]],[[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[[3,[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,1],[1,1,0,1]]],[]],[[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[[0,[0,0,0,0,0,0,0,0,0,1,1,1,1,0,0,0,0,0],[1,1,0,1]]]]],"prefix_d":[[[1,[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],[-1,1,1,1]],[3,[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],[-1,1,-1,1]]],[],[[1,[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],[1,1,-1,1]],[3,[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],[1,1,1,1]]],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[[1,[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],[-1,1,1,1]],[3,[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],[-1,1,-1,1]]],[[1,[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],[-1,2,1,2]],[3,[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],[-1,2,-1,2]]],[],[],[],[],[],[],[],[],[],[],[],[]],"schema_version":1} diff --git a/research/p104-cut353-independent-audit/PROOF.md b/research/p104-cut353-independent-audit/PROOF.md new file mode 100644 index 0000000000..c839892c29 --- /dev/null +++ b/research/p104-cut353-independent-audit/PROOF.md @@ -0,0 +1,128 @@ +# Conditional independent audit of the cut353 retirement + +This note audits the logical independent-input boundary in PR6716 at +`a467457692bc9e11113d9b2e2e34ea8ffb553b58`. It does not audit the common-idle +physical bank, native realization, complete invoice, claimed exponent, +compiler or outer transfer. The author-side construction and all earlier +methods retain their credit. The exact serialized controller data, rather +than the source's checker or constructor, are the executable audit inputs. + +## Algebra and conventions + +Write `u` for the source's operator `Q`, and retain only `u^4=1`. In the +source proof, `q=Q^-1=u^3`. All eighteen stage variables remain distinct +commuting invertible indeterminates. Computation takes place over + +`Q(i)[u]/(u^4-1)[t1^+-1,...,t18^+-1]`. + +There is no specialization of `u^2` to identity, no merging of stage +variables and no numerical evaluation. Every matrix cell is a finite +canonical Laurent polynomial with exact rational real and imaginary +coefficients. Put + +`lambda=((1+i)/2)+((1-i)/2)u^2`, + +`S=lambda*u^3=((1+i)/2)u^3+((1-i)/2)u`. + +The LOCAL opcode is an assumed algebraic interface: first add `u^3` times +the source row to the destination row, then multiply both rows by their +named fresh stage variable. Its native physical implementation is not +executed or proved by this audit. LAMBDA, QUERY, ordinary row operations +and the one- or two-row IDLE actions use the literal source opcode +specification retained as inert text. An IDLE on two rows is two algebraic +actions; this audit supplies no license to merge two independent arrays. + +## Why two-sided separation is sufficient + +Let `P` denote the unretired prefix through event353 inclusive. The ordinary +vectors in the actual witness satisfy + +`ab=cd=1`, `aP=S c`, `Pd=S b`. + +Let `G,J` be the literal ordinary basis words in that witness. Their +required identities are + +`e4^T G=c`, `Gd=e4`, `e4^T J=a`, `Jb=e4`. + +Consequently `e4^T J P G^-1=S e4^T` and +`J P G^-1 e4=S e4`. Both off-diagonal couplings at the pivot vanish. +Thus this transformed prefix is exactly `S` on pivot4 and an independent +operator on the other 33 inputs. A row identity alone would not establish +this conclusion; the column identity is independently required. + +The input basis uses only roles4,20,21. Their complete declared endpoint +targets are identical, so this ordinary basis commutes with that endpoint. +The full final-controller check below independently verifies the resulting +endpoints, rather than inferring them merely from this commutation argument. + +## Literal handoff and full endpoint + +The audit compares every event of the serialized retired word with the +following surgery on the serialized unretired word: inverse input basis; +prefix through353; middle basis `J`; inverse middle basis with pivot4 +renamed to fresh34; remaining unretired suffix with that same renaming; +the three recorded lambda returns; renamed final `G`; and the three +recorded original-group lambda adapters. This is an exact event comparison, +including scalar signs and chronology. + +No event through retired index362 uses role34; its first contact is363. +Its arbitrary input therefore remains independent until the handoff. +The original pivot receives `u^3` without stage factors. The new role +receives `t10*t11*t12*t13` without a central factor. All other targets +are taken from the unretired declaration. The final declaration is checked +against this independently assembled list. + +The independently implemented forward matrix calculation checks all +35 by35 cells of the actual final word against that diagonal list. The +unretired controller is computed only through the prefix; its remaining +declared targets are the contract used to assemble that expected list. +The entire final controller is checked directly. This +establishes the stated logical endpoint simultaneously for arbitrary +independent inputs, conditional on the declared LOCAL interface and ring +relations. It is stronger than testing selected numerical inputs, but is +not a native supplier or all-size multiplication theorem. + +The artifact retains all 68 prefix row/column cells and all 1,225 final +matrix cells. Default replay recomputes and compares those actual cells. +The ordered list of paid-opcode kinds, stage sets and central query signs +is also compared before and after surgery. That structural check is not +a complete price, native-caller or resource audit. + +## Evidence boundary and credit + +Both separately implemented blind first executions passed on +2026-11-04, finishing at 19:59:36 and 19:59:45 UTC. Every typed common +receipt field and every actual canonical polynomial cell agreed. The +common receipt SHA256 is +`9e9a7b5f05fc9e8824fc6206771625f91acf0aead53aae461cb0fdaf9afff6ef`; +the canonical packet SHA256 is +`ca09e50e074afde1af921461618e2f1d8349c643a16a6db0683f2a7efcd8e579`. +These are complete-value comparisons, not only selected summary counts. + +The primary has ten rejection controls. Three execute actual changed +controllers through the full polynomial engine and require the intended +endpoint failure: reverse the first QUERY central sign, change the first +input-basis coefficient to -2, or append a central operation to fresh34. +Before the first execution, static review corrected a no-op dual-pair +control and replaced two expected-object controls with these actual-engine +mutants. Both earlier unexecuted code versions were preserved. These +changes were not reactions to a failed scientific execution. + +Execution status and retained receipts are recorded separately in +`VALIDATION.md` and `RUN-RECORDS.json`; this written argument does not +substitute for an execution receipt. The source's existing independent +checker was not imported or executed. Reading its source during task +selection is disclosed in the scout record; the new implementation uses +fresh whole forward matrices rather than that checker's per-column and +reverse-row architecture. Independent AI work is not independent human +acceptance or proof-kernel verification. + +Credit thu-nmrc/PR6716 for the exact root, witness, caller application and +complete claimed budget; DreamingOfClouds/PR6702 for the inherited native +word; Ali Romman/PR6348 andPR6398 and Cinna Davis's query/controller lineage +for the binary supplier and normalization; PR6545 and PR5599's dual-pair +retirement lineage for the method; and PR6551 for the earlier rebalanced +comparison. No invention of dual-pair retirement, native normalization, +productive recursion or binary refinement is claimed here. New audit +material was prepared with substantial OpenAI Codex assistance and is +Apache-2.0. The frozen source texts retain their original notices. diff --git a/research/p104-cut353-independent-audit/README.md b/research/p104-cut353-independent-audit/README.md new file mode 100644 index 0000000000..3ed692c56c --- /dev/null +++ b/research/p104-cut353-independent-audit/README.md @@ -0,0 +1,67 @@ +# Independent logical audit of PR6716's cut353 + +This package independently checks the two-sided fresh-input retirement in +PR6716 at `a467457692bc9e11113d9b2e2e34ea8ffb553b58`. It interprets the actual +serialized controllers over exact Gaussian-rational Laurent polynomials, +retaining an order-four central operator and all eighteen stage variables. + +The scope is the ordinary dual-pair identities, their actual prefix, +literal event surgery, the first fresh-input contact and all 1,225 final +coefficient positions. It assumes the source's LOCAL algebraic interface. +It gives no new construction, invoice, conditional exponent, scientific +admission or frontier change. + +Both separately implemented blind first runs passed on 2026-11-04 at +19:59:36 and 19:59:45 UTC. Their complete receipts and all 68 prefix plus +1,225 final polynomial cells agree. The original pivot receives `Q^-1` +with no stage factor; fresh input34 receives the product of stages10–13 +with no central factor. These statements concern the declared logical +LOCAL interface, not its physical native implementation. + +The primary checks ten rejection controls, including three actual +full-matrix executions with a reversed query sign, wrong input-basis +coefficient and unearned central factor on the fresh output. Each must +fail at the polynomial endpoint check. Two unexecuted control drafts were +corrected before the first run and preserved separately; scientific +code and first artifacts were unchanged after that first execution. + +The unretired controller is evaluated only through its cut prefix. Its +declared target list supplies the unchanged endpoint contract; the entire +retired controller is checked directly against the independently assembled +35-input target list. This does not claim a second full unretired replay. + +`PROOF.md` states the argument and boundary. `SOURCE-PINS.json` binds six +inert original source objects. No predecessor checker is imported or +executed. Default verification is read-only and compares every retained +proof-relevant field of `PACKET.json` and `RESULT.json`. + +```sh +python3.12 -I -B verify.py +python3.12 -I -O -B verify.py +``` + +The explicitly mutating `--emit --write-packet PATH` mode regenerates an +audit packet and emits its receipt. Execution evidence belongs in +`VALIDATION.md` and `RUN-RECORDS.json`; an unexecuted prototype is not a +passing audit. Canonical JSON values determine mathematical equality; +file-container hashes are separate provenance evidence. + +Credit thu-nmrc/PR6716, DreamingOfClouds/PR6702, Ali Romman's PR6348/6398, +Cinna Davis's query/controller lineage, PR6545/5599's dual-pair method and +PR6551's rebalanced comparison, with all retained earlier native/helper, +Clifford, compiler, BIT, precision and analytic notices. New material has +substantial OpenAI Codex assistance. Separate AI checks do not imply +independent human acceptance or proof-kernel certification. + +## Open next questions + +1. Independently bind the actual common-idle bank and native absolute + phases to this logical caller. Start from the shared ordinary basis + and the exact source invocations; this audit does not price or replay + that physical supplier. +2. Audit the complete invoice, completion/compiler and outer transfer at + this same source head. Logical separation alone cannot certify their + costs, assumptions or claimed saving. +3. Discharge the consumed framework assumptions for the full recursive + interface. Finite symbolic coefficients do not establish the required + all-size native, ownership, stock, precision or analytic contracts. diff --git a/research/p104-cut353-independent-audit/RESULT.json b/research/p104-cut353-independent-audit/RESULT.json new file mode 100644 index 0000000000..f192870b5f --- /dev/null +++ b/research/p104-cut353-independent-audit/RESULT.json @@ -0,0 +1 @@ +{"artifact_sha256":"ca09e50e074afde1af921461618e2f1d8349c643a16a6db0683f2a7efcd8e579","case_manifest_sha256":"7a7e961a1971c31653770af43b0097ba55d1eb980795a050c74786e8f5c7d6c0","cut_after":353,"cut_cells":68,"final_cells":1225,"final_events":586,"final_roles":35,"fresh":34,"fresh_first_contact":363,"handoff_after":362,"ordinary_identities":6,"pivot":4,"schema_version":1,"scope":"PR6716 cut353 fresh34 conditional LOCAL audit","source_manifest_sha256":"0de615eb3eac51539567c56e85e177c91c0d3e5c2c69b8cd64abff46f68fc902","stages":18,"unretired_events":562,"unretired_roles":34} diff --git a/research/p104-cut353-independent-audit/REVIEW.md b/research/p104-cut353-independent-audit/REVIEW.md new file mode 100644 index 0000000000..fbd10b689b --- /dev/null +++ b/research/p104-cut353-independent-audit/REVIEW.md @@ -0,0 +1,132 @@ +# Conditional two-sided cut and fresh-input surgery review + +Verdict: the displayed algebraic surgery is **correct conditional on the premises below**. In particular the row and column identities are both needed, and the extracted suffix is D only because S commutes with the remaining fresh-stage target D. This note does not verify any actual prefix, endpoint, clock or physical address claim. + +Source: thu-nmrc PR6716 head `a467457692bc9e11113d9b2e2e34ea8ffb553b58`, package `research/p104-common-idle-double-retirement`, PROOF Sections 1 and 4 and WITNESS.json. Source identity, current-main guidance and the preceding read-only scouting boundary are recorded in MATH-SCOUT.md. No checker or mathematical program was executed for this written review. + +## Premises and operator order + +Use column payloads; the rightmost matrix acts first. Let P be an invertible literal prefix on the closed main-field interface and L its remaining suffix. Assume the entire normalized endpoint is `E=L P`, diagonal in the original independent input fields. Any omitted native/helper fields must form the promised closed interface at these boundaries under the inherited LOCAL contract; omitting an actual coupling is not justified by this lemma. + +Let e be the standard pivot column (source field 4). Let a,c be ordinary rational row vectors and b,d ordinary rational column vectors, satisfying + + ab=cd=1, aP=S c, Pd=S b. + +Here S is an invertible common payload operator; ordinary scalar matrices commute with it. Suppose invertible ordinary matrices G,J, derived from their literal gates, satisfy + + e^T G=c, Gd=e, e^T J=a, Jb=e. + +Assume G is supported only on a group of original fields with the same complete endpoint target SD (source fields 4,20,21), and ordinary rational coefficients commute with this target. Consequently `GE=EG`. Also assume `SD=DS`. The latter is supplied in the source by the central operator/fresh disjoint-stage interface, rather than by the dual-pair identities alone. All of these are premises to be checked against the actual source representation. + +## Exact block separation + +Insert G inverse at input and J at the cut, giving + + P' = J P G inverse. + +The pivot row is + + e^T P' = aP G inverse = S c G inverse = S e^T. + +Since `G inverse e=d`, its pivot column is + + P'e = J P d = J S b = S Jb = S e. + +Thus both off-diagonal pivot couplings vanish and, in pivot/rest order, + + P' = diag(S,K). + +Invertibility of P and the ordinary bases implies invertibility of K. The conditions ab=cd=1 make the row/column pairs normalized ordinary dual pairs; once the four G/J identities are supplied they are also implied by those identities. They do not replace either of the identities involving P. No S-valued coefficient is needed in G or J. + +The adjusted suffix is the literal composition of J inverse, the original suffix and the final G: + + L' = G L J inverse. + +Its product with P' is `G E G inverse=E`. Therefore + + L' = E (P') inverse = diag(SD S inverse, E_rest K inverse) + = diag(D,H). + +The last equality uses `SD=DS`. Without that premise the first block is `SD S inverse`, not D; the abstract row/column identities alone would not justify the claimed plain-stage suffix. In the source the premise is stated explicitly: central q, its square and lambda commute with the fresh stage operators. No other commutation of P or K with S is required. + +This also shows why both sided identities matter. A correct pivot row without the correct pivot column can leave other outputs depending on the completed pivot; a correct column without the row can leave the purported completed output depending on other independent inputs. + +## Fresh-input substitution and independence + +Let x contain all original independent inputs and introduce a genuinely new independent payload z in fresh field 34. The prefix and all input-basis gates must leave that field untouched. At the separated cut the abstract state is + + pivot = S x_p, rest = K x_rest, fresh = z. + +Freeze the completed original pivot. In the entire literal suffix L', rename every pivot reference to the fresh field, including the J inverse and final G gates. The resulting suffix acts as diag(D,H) on (fresh,rest), so the final state is + + original pivot = S x_p, rest = E_rest x_rest, fresh = D z. + +This is a direct-sum extension by an arbitrary input z. No duplication, equality, zero initialization or dependence on x is used. The other inputs retain their original targets because `HK=E_rest`. Intermediate suffix gates may mix fresh and other fields; only the complete suffix has the proved block form. Aggregate block separation alone does not establish that the original pivot is physically untouched: complete literal renaming and absence of address aliases are separate necessary checks. + +For the source's clocks, a three-gate input basis and six-gate cut basis explain why the unretired prefix ending at event 353 can lead to a retired handoff ending at event 362. This is only a consistency observation. The actual event list, inclusive indexing, instruction ordering and absence of earlier field-34 contacts must be verified independently, not inferred from that arithmetic. + +## Central phase and lambda return + +The source assumes the exact global central operator q obeys `q squared=X`, where X is an ordinary phase-plus-one translation and `X squared=I`. Its lambda is + + lambda = ((1+i)I+(1-i)X)/2, + lambda inverse = ((1-i)I+(1+i)X)/2. + +Because q commutes with its square, these give `lambda squared=X`, `lambda lambda inverse=I`, `S=lambda q`, and `S squared=I`. Returning lambda inverse on the original completed S pivot produces exactly `q x_p`. The fresh field receives D and must receive neither this lambda inverse nor an additional S/q target. Returning lambda on the original normalization group must preserve the source's exact direction/convention and exclude the fresh field. The literal audit, not this lemma, settles which opcode implements lambda inverse. + +The phase-plus-one premise is substantive: substituting an operator with `q squared=-X`, silently replacing X by I, or using one-column tensor-normalization identities would invalidate this derivation. At positive column multiplicity f the argument applies to the actual global q_f and its own square. It does not assert `S_f=(S_1) tensor f`, and it does not move exterior lambda coefficients inside a tensor power. + +## What remains unverified + +Neither `aP=S c` nor `Pd=S b`, nor the literal complete endpoint E, has been computed in this note. The earlier prose inspection checked only the displayed small ordinary G/J witness under target-first ADD. The actual main interface closure, common endpoint on fields 4/20/21, exact stage/central algebra, clock, complete suffix renaming, independent field-34 allocation and absence of native/helper/owned aliases remain obligations for the primary and independent literal audits. + +Paid LOCAL calls, thin queries, idles, ordinary bases, returns and job chronology must still be accounted for under their actual unchanged contracts. The lemma supplies no free call, no productive copy, no reusable owned bank, no new primitive and no invoice. Source-native all-column correctness, owned erasure, compiler, precision/tape and analytic recovery remain quantified assumptions. The complete signed price, claimed kappa, compiler completion and outer bounds are outside this review. No selected-frontier or scientific-admission change follows. + +Credit: thu-nmrc for the new source-specific witness and construction; PR6545 and the PR5599 lineage for the two-sided dual-pair method; DreamingOfClouds/PR6702 for the unchanged native source; Ali Romman/PR6348/PR6398 and Cinna Davis's retained query/controller lineage for the supplier and normalization framework. This is a separate written application audit using classical invertible linear algebra, with OpenAI Codex assistance, not a new general theorem or independent human review. Only this note was intentionally written; no source/package file was changed. + + +--- + +# Static implementation review: cut353 audit + +Verdict: **no material correctness or acceptance defect found in the reviewed scope**. The implementations compute both cut vectors and every cell of the retired formal main-field endpoint by distinct propagation methods. This is conditional LOCAL-contract evidence, not a physical-address/owned-bank audit or complete source-price validation. + +Read after root confirmed both blind firsts were sealed: package `research/p104-cut353-independent-audit/{verify.py,oracle.py}`, its six inert inputs, CASES/SCHEMA, and the two first RUN records. No checker, import, source generator, mutation or scientific program was executed by this reviewer; this note is the only intentional write. + +## Methods and exact ring + +Primary `verify.py:129–146,163–188,381–400` constructs the full 34-field prefix matrix chronologically, forms aP and Pd from that matrix, and separately propagates the full 35-field retired matrix. Oracle `oracle.py:161–217,248–299` instead pulls a backwards covector for aP, pushes a forwards vector for Pd, and pulls each of the 35 final output covectors independently. Its reverse routine is a row pullback, not a literal inverse program. This is the correct operation for obtaining aP. + +Both implement exact rational-Gaussian coefficients and independent commuting stage exponents, reducing only the central exponent modulo four. The primary stores `(u,t1,...,t18)` in a 19-coordinate monomial; its shift by stage index accesses the corresponding stage coordinate, and serialization emits all 18 stage exponents. The source's 20-entry target convention is `(u,dummy,t1,...,t18)`. Both explicitly require the dummy coordinate to be zero and omit it when constructing expected monomials. There is no accidental stage-zero variable or conflation of stages 1 and 18. Neither engine substitutes stage samples or collapses u squared to one. + +The stored central variable is source Q=u, whereas proof q=u inverse. Both therefore implement the normalized S as lambda(u squared) times u cubed. The oracle explicitly checks S squared=1, u to the fourth=1, S differing from bare u cubed, and u squared differing from one. This retains the exterior lambda phase rather than treating S as the one-column tensor power. + +## Conditional LOCAL order + +The inert `inputs/caller.py.txt` gives LOCAL(stage,src,dst) as a query `dst += u inverse src`, followed by the same fresh stage factor on both src and dst. Primary `verify.py:178–182` implements this exact chronological order. The oracle's forward column routine matches it; its backwards LOCAL step maps a row to `src := t_stage*(old_src+u inverse old_dst)` and `dst := t_stage*old_dst`, which is the correct pullback. ADD is target-first throughout both engines, consistent with the literal source and witness. + +This reads the declared endpoint semantics of an abstract LOCAL event. Neither implementation reconstructs the source native word, its helpers, its actual physical maps or all-column realization. The distinction is explicit in the oracle docstring and CASES exclusions and must remain explicit in publication. + +## Literal cut, fresh input and endpoint coverage + +Primary `verify.py:322–338` checks the complete serialized surgery, including inverse input G, the inclusive source prefix through event 353, J, renamed J inverse and suffix, intervening normalizations, renamed final G and original-group return. It checks the source cut event itself and requires the first formal fresh-role contact to be event 363. Oracle `oracle.py:256–285` independently checks the first-contact boundary, the literal input-basis/prefix/J segment and six ordinary pairing/basis identities. Both compute all 34 entries of each cut vector, for **68 cut cells**, not 63. + +Both derive the new expected target from the authenticated old diagonal declaration, replace old pivot 4 by bare u cubed, and append the stage-only target t10*t11*t12*t13 for field 34. All **1,225** final output/input cells are computed and checked, including every off-diagonal zero. The matrix basis supplies 35 formally independent arbitrary inputs, so this evidence does not assume a copied or zero fresh input. Primary also checks that the paid LOCAL-stage, QUERY-sign and idle-stage sequence is unchanged; this is not a complete physical price invoice. + +One scope distinction matters: the authenticated unretired diagonal is a declared source endpoint; these routines do not independently recompute the entire unretired 34-by-34 final endpoint. They do recompute the full cut vectors and the entire changed 35-by-35 endpoint. The latter gives direct formal endpoint evidence even though the general surgery explanation also uses the old endpoint as an inherited premise. + +Formal role 34 noncontact and consistent indexed renaming do not prove physical address disjointness from implicit LOCAL helper/owned banks. No actual ownership lifetime or common-idle physical noncontact is independently checked by these routines. This is correctly outside CASES. Avoid promoting this result into an audit of those premises. + +## Rejection guards and controls + +The primary authenticates metadata bytes, the six declared source hashes and source-path closure before computation. Its JSON loader rejects duplicate keys, booleans, floats and nonfinite numbers globally; recursive typed comparison checks the complete actual packet and retained receipt. The oracle authenticates exact frozen metadata/input hashes, source commit and Git blob identity. Its packet validator (`oracle.py:302–334`) enforces exact artifact keys/schema, dimensions, integer types excluding booleans, reduced positive-denominator Gaussian fractions, bounded exponents and strictly sorted unique nonzero monomials. It then compares the complete canonical artifact to its own recomputation, not merely an asserted packet hash. + +The oracle loader (`oracle.py:48–56`) rejects duplicate keys and named nonfinite constants but does **not** globally reject finite floats during JSON parsing. I found no proof-relevant acceptance gap from this: every numeric packet field has an exact integer-type guard, all source inputs/metadata are byte-authenticated, and the entire receipt is compared as canonical JSON bytes to the recomputed object (`oracle.py:439–444`). Thus 1.0 or true cannot pass as integer 1 in either the packet or receipt. Nevertheless, the precise claim should be proof-relevant typed/canonical rejection, rather than saying the oracle loader itself globally rejects all floats. No execution was performed to demonstrate or alter this behavior. + +Primary controls run three genuine source-word endpoint failures (query central sign, input G coefficient, extra fresh central factor), plus loader/type/pairing cases. The endpoint controls bypass the constructor equality guard and require the intended endpoint diagnostic. Oracle controls independently mutate the first query central sign and input basis coefficient, execute the actual reverse engine until it finds a nonzero wrong endpoint cell, and retain that witness. It also checks malformed fractions, duplicate/unsorted monomials and loader failures. These are meaningful semantic controls rather than solely digest rejection. They do not constitute a proof of arbitrary address-level/native mutations. + +## Retained execution evidence and limits + +I read, but did not recreate, the primary first RUN (19:59:36.374856–19:59:36.570176 UTC, exit 0, code SHA256 `882e13a044c22c37e2c93f048f70262b82fc16a8a0de7788ee9b39d38d8d21b7`) and oracle first RUN (19:59:44.985449–19:59:45.115717 UTC, exit 0, code SHA256 `348be3d563af88307198479ef843b414e0069f31a6752a58937e6aa7a709a211`). Both record Python 3.12.14, frozen metadata/input hashes, no peer-data read, empty stderr and completed artifacts. Their differing pretty/container artifact bytes are not a mathematical disagreement; root separately compares complete canonical packet values. + +No request for a core change follows from this review. Publication should retain the conditional LOCAL boundary, the formal/physical distinction, the old endpoint declaration distinction, and the exact float-validation qualification above. Source author thu-nmrc and all PR6702/PR6348/PR6398/PR6545/PR5599 predecessor credit remain unchanged. This separate static AI review is neither formal proof-kernel certification nor independent human scientific acceptance. diff --git a/research/p104-cut353-independent-audit/RUN-RECORDS.json b/research/p104-cut353-independent-audit/RUN-RECORDS.json new file mode 100644 index 0000000000..e7115fd4b1 --- /dev/null +++ b/research/p104-cut353-independent-audit/RUN-RECORDS.json @@ -0,0 +1,244 @@ +{ + "schema_version": 1, + "source_head": "a467457692bc9e11113d9b2e2e34ea8ffb553b58", + "canonical_base": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "firsts": { + "primary": { + "at": "2026-11-04T19:59:36.374856+00:00", + "code_sha256": "882e13a044c22c37e2c93f048f70262b82fc16a8a0de7788ee9b39d38d8d21b7", + "input_sha256": { + "SOURCE-PINS.json": "0de615eb3eac51539567c56e85e177c91c0d3e5c2c69b8cd64abff46f68fc902", + "CASES.json": "7a7e961a1971c31653770af43b0097ba55d1eb980795a050c74786e8f5c7d6c0", + "SCHEMA.json": "3936e155a437939af360d5b2c4be83036984e56c7d04665c5eca2dc7f09ba50d", + "inputs/PROOF.md": "bdf2a3e379d0aaf8ae42a49b09ee6f9d21c5c1a8ec8653fab75efac0c5c93099", + "inputs/README.md": "68f52f2e0fa916cbf98e18896f0f6026469d3e45474e6d4314f95e0959cef6cb", + "inputs/WITNESS.json": "4c820b99eb1ebebd7cd527f07b0aa86a355865072acace8bfc9fddd998086331", + "inputs/CONTROLLER-UNRETIRED.json": "8c58adc35a7055dde1eda8f2547492dda9f558a73262fc17f439819c39d2555e", + "inputs/CONTROLLER.json": "2a0fb1c11fccfcc4dacbc7c82cf439969caa295dba4fc1a21a83e01b4ab8affc", + "inputs/caller.py.txt": "ad0dd4aa97ae19f687defc8690e0ffb5f8ada551720aba4b48b8d307c776b5ba" + }, + "python": "3.12.14 (main, Aug 25 2026, 13:50:33) [Clang 22.1.3 ]", + "peer_data_read": false, + "timeout_seconds": 180, + "scope": "Independent blind first; no peer receipt/artifact consumed", + "finished_at": "2026-11-04T19:59:36.570176+00:00", + "wall_seconds": 0.1720201252028346, + "exit": 0, + "peak_rss_bytes": 30113792, + "stdout_sha256": "8c71919d559247a9128b208b15b2e3e24caad07918693c2f94dcc1af868154bd", + "stderr_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855", + "artifact_sha256": "60c367b1025181734a21437a644eac4941dbfeb025e0d2547dc8c233a847ce92", + "artifact_bytes": 6430, + "command": "python3 -I -B verify.py --emit --write-packet PACKET.json" + }, + "oracle": { + "at": "2026-11-04T19:59:44.985449+00:00", + "code_sha256": "348be3d563af88307198479ef843b414e0069f31a6752a58937e6aa7a709a211", + "input_sha256": { + "SOURCE-PINS.json": "0de615eb3eac51539567c56e85e177c91c0d3e5c2c69b8cd64abff46f68fc902", + "CASES.json": "7a7e961a1971c31653770af43b0097ba55d1eb980795a050c74786e8f5c7d6c0", + "SCHEMA.json": "3936e155a437939af360d5b2c4be83036984e56c7d04665c5eca2dc7f09ba50d", + "inputs/PROOF.md": "bdf2a3e379d0aaf8ae42a49b09ee6f9d21c5c1a8ec8653fab75efac0c5c93099", + "inputs/README.md": "68f52f2e0fa916cbf98e18896f0f6026469d3e45474e6d4314f95e0959cef6cb", + "inputs/WITNESS.json": "4c820b99eb1ebebd7cd527f07b0aa86a355865072acace8bfc9fddd998086331", + "inputs/CONTROLLER-UNRETIRED.json": "8c58adc35a7055dde1eda8f2547492dda9f558a73262fc17f439819c39d2555e", + "inputs/CONTROLLER.json": "2a0fb1c11fccfcc4dacbc7c82cf439969caa295dba4fc1a21a83e01b4ab8affc", + "inputs/caller.py.txt": "ad0dd4aa97ae19f687defc8690e0ffb5f8ada551720aba4b48b8d307c776b5ba" + }, + "python": "3.12.14 (main, Aug 25 2026, 13:50:33) [Clang 22.1.3 ]", + "peer_data_read": false, + "timeout_seconds": 180, + "scope": "Independent blind first; no peer receipt/artifact consumed", + "finished_at": "2026-11-04T19:59:45.115717+00:00", + "wall_seconds": 0.11189187504351139, + "exit": 0, + "peak_rss_bytes": 30375936, + "stdout_sha256": "d4f5f32f7815d420d27c0469ae0eced535a6cd6f6ef39e35dae7985d51ac2c51", + "stderr_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855", + "artifact_sha256": "c36b8e264f80b917725a18a09524763c425449f8e909bc878c714480e7bccd5e", + "artifact_bytes": 32173, + "command": "python3 -I -B oracle.py --package PACKAGE --first --write-packet OWN-PACKET.json --output OWN-COMMON.json" + } + }, + "comparison": { + "both_first_exit0": true, + "common_sha256": "9e9a7b5f05fc9e8824fc6206771625f91acf0aead53aae461cb0fdaf9afff6ef", + "artifact_canonical_sha256": "ca09e50e074afde1af921461618e2f1d8349c643a16a6db0683f2a7efcd8e579", + "actual_cut_cells": 68, + "actual_final_cells": 1225, + "actual_whole_packet_equal": true, + "container_bytes_differ_allowed": true, + "first_sources_and_codes_unchanged": true + }, + "strict_modes": [ + { + "name": "PRIMARY-NORMAL", + "at": "2026-11-04T20:01:38.652052+00:00", + "exit": 0, + "seconds": 0.1977525418624282, + "stdout_sha256": "0a0fe3c27e6fe12dc502d6b69c6391f1fcf3080b30b7e63411d802b4eaee5e34", + "stderr_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855" + }, + { + "name": "PRIMARY-OPTIMIZED", + "at": "2026-11-04T20:01:38.849953+00:00", + "exit": 0, + "seconds": 0.23299166653305292, + "stdout_sha256": "0a0fe3c27e6fe12dc502d6b69c6391f1fcf3080b30b7e63411d802b4eaee5e34", + "stderr_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855" + }, + { + "name": "PRIMARY-OPTIMIZED-EMIT", + "at": "2026-11-04T20:01:39.083247+00:00", + "exit": 0, + "seconds": 0.2195108337327838, + "stdout_sha256": "8c71919d559247a9128b208b15b2e3e24caad07918693c2f94dcc1af868154bd", + "stderr_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855" + }, + { + "name": "ORACLE-ACTUAL-NORMAL", + "at": "2026-11-04T20:01:39.302914+00:00", + "exit": 0, + "seconds": 0.09824633318930864, + "stdout_sha256": "d4f5f32f7815d420d27c0469ae0eced535a6cd6f6ef39e35dae7985d51ac2c51", + "stderr_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855" + }, + { + "name": "ORACLE-ACTUAL-OPTIMIZED", + "at": "2026-11-04T20:01:39.401314+00:00", + "exit": 0, + "seconds": 0.1373858330771327, + "stdout_sha256": "d4f5f32f7815d420d27c0469ae0eced535a6cd6f6ef39e35dae7985d51ac2c51", + "stderr_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855" + } + ], + "external_controls": { + "cases": 20, + "commands": 40, + "all_intended_rejections": true, + "first_harness_sha256": "135821a523b3d6748963431d9d9547e63911fa8d00b912f84cca0b0bd7ca0c7f" + }, + "pre_first_corrections": "Primary no-op dual-pair mutant corrected and expected-object-only mutants replaced with actual-engine endpoint mutants; oracle7controls added before first. All unexecuted variants retained locally. Neither scientific first failed; no core/input/firstreceipt/artifact changes afterward.", + "remaining_transport": "Final documentation commit byte/export checks, publication and originalhostedCI; mode/history/export/cold successes are local evidence.", + "transport_checks": { + "registered_commit_export": [ + { + "name": "REGISTERED", + "argv": [ + "/Users/evaayala/.cache/codex-runtimes/codex-primary-runtime/dependencies/python/bin/python3", + "-B", + "scripts/research_package.py", + "--package", + "research/p104-cut353-independent-audit" + ], + "at": "2026-11-04T20:06:13.183188+00:00", + "exit": 0, + "seconds": 0.9316202085465193 + }, + { + "name": "COMMIT-CHECK", + "argv": [ + "/Users/evaayala/.cache/codex-runtimes/codex-primary-runtime/dependencies/python/bin/python3", + "-B", + "scripts/check_research_commit.py", + "--package", + "research/p104-cut353-independent-audit", + "--check-source-history", + "--check-modes" + ], + "at": "2026-11-04T20:06:13.319390+00:00", + "exit": 0, + "seconds": 0.13598941639065742 + }, + { + "name": "EXPORT", + "argv": [ + "/Users/evaayala/.cache/codex-runtimes/codex-primary-runtime/dependencies/python/bin/python3", + "-B", + "scripts/export_research_package.py", + "export", + "--package", + "research/p104-cut353-independent-audit", + "--ref", + "HEAD", + "--output", + "/private/tmp/contribution-batch-b11-20261104T1654Z/session-02/PACKAGE.tar" + ], + "at": "2026-11-04T20:06:13.414631+00:00", + "exit": 0, + "seconds": 0.09506741631776094 + }, + { + "name": "EXPORT-CHECK", + "argv": [ + "/Users/evaayala/.cache/codex-runtimes/codex-primary-runtime/dependencies/python/bin/python3", + "-B", + "scripts/export_research_package.py", + "check", + "/private/tmp/contribution-batch-b11-20261104T1654Z/session-02/PACKAGE.tar", + "--check-inputs" + ], + "at": "2026-11-04T20:06:13.460573+00:00", + "exit": 0, + "seconds": 0.04580549988895655 + } + ], + "cold_commands": [ + { + "argv": [ + "/Users/evaayala/.cache/codex-runtimes/codex-primary-runtime/dependencies/python/bin/python3", + "-I", + "-W", + "error", + "-B", + "/private/tmp/contribution-batch-b11-20261104T1654Z/session-02/COLD/research/p104-cut353-independent-audit/verify.py" + ], + "exit": 0, + "seconds": 0.1854589581489563 + }, + { + "argv": [ + "/Users/evaayala/.cache/codex-runtimes/codex-primary-runtime/dependencies/python/bin/python3", + "-I", + "-W", + "error", + "-B", + "-O", + "/private/tmp/contribution-batch-b11-20261104T1654Z/session-02/COLD/research/p104-cut353-independent-audit/verify.py" + ], + "exit": 0, + "seconds": 0.22572812531143427 + }, + { + "argv": [ + "/Users/evaayala/.cache/codex-runtimes/codex-primary-runtime/dependencies/python/bin/python3", + "-I", + "-W", + "error", + "-B", + "/private/tmp/contribution-batch-b11-20261104T1654Z/session-02/COLD/research/p104-cut353-independent-audit/oracle.py", + "--package", + "/private/tmp/contribution-batch-b11-20261104T1654Z/session-02/COLD/research/p104-cut353-independent-audit" + ], + "exit": 0, + "seconds": 0.09095520805567503 + }, + { + "argv": [ + "/Users/evaayala/.cache/codex-runtimes/codex-primary-runtime/dependencies/python/bin/python3", + "-I", + "-W", + "error", + "-B", + "-O", + "/private/tmp/contribution-batch-b11-20261104T1654Z/session-02/COLD/research/p104-cut353-independent-audit/oracle.py", + "--package", + "/private/tmp/contribution-batch-b11-20261104T1654Z/session-02/COLD/research/p104-cut353-independent-audit" + ], + "exit": 0, + "seconds": 0.13333587441593409 + } + ], + "cold_bytes_and_modes_unchanged": true + } +} diff --git a/research/p104-cut353-independent-audit/SCHEMA.json b/research/p104-cut353-independent-audit/SCHEMA.json new file mode 100644 index 0000000000..ac05c661ad --- /dev/null +++ b/research/p104-cut353-independent-audit/SCHEMA.json @@ -0,0 +1,14 @@ +{ + "schema_version": 1, + "canonical_hash": "UTF-8 json.dumps(value,sort_keys=True,separators=(',',':'),ensure_ascii=True),without trailing newline", + "artifact": { + "keys": ["schema_version", "a_prefix", "prefix_d", "final_matrix"], + "a_prefix": "34 polynomial cells", + "prefix_d": "34 polynomial cells", + "final_matrix": "35 rows,each35 polynomial cells,in output-row/input-column order", + "polynomial": "sorted unique terms [u_exponent_mod4,[18 integer stage exponents],[real_numerator,real_denominator,imag_numerator,imag_denominator]];normalized Fractions;empty list is zero" + }, + "receipt_keys": ["schema_version", "scope", "source_manifest_sha256", "case_manifest_sha256", "cut_after", "handoff_after", "pivot", "fresh", "unretired_roles", "unretired_events", "final_roles", "final_events", "stages", "cut_cells", "final_cells", "ordinary_identities", "fresh_first_contact", "artifact_sha256"], + "strict_types": "integers exclude booleans;no floats,nonfinite values or duplicate keys;exact keys and list lengths", + "runtime_artifacts": ["PACKET.json", "RESULT.json"] +} diff --git a/research/p104-cut353-independent-audit/SOURCE-PINS.json b/research/p104-cut353-independent-audit/SOURCE-PINS.json new file mode 100644 index 0000000000..941700b3f9 --- /dev/null +++ b/research/p104-cut353-independent-audit/SOURCE-PINS.json @@ -0,0 +1,54 @@ +{ + "schema_version": 1, + "sources": [ + { + "local_path": "inputs/PROOF.md", + "sha256": "bdf2a3e379d0aaf8ae42a49b09ee6f9d21c5c1a8ec8653fab75efac0c5c93099", + "git_blob": "08f1031ea9da49072726deaceabca6aa5a4ac38c", + "git_commit": "a467457692bc9e11113d9b2e2e34ea8ffb553b58", + "origin_url": "https://github.com/thu-nmrc/integer-mult-bounds/blob/a467457692bc9e11113d9b2e2e34ea8ffb553b58/research/p104-common-idle-double-retirement/PROOF.md", + "usage": "inert literal source/opcode specification; never imported or executed" + }, + { + "local_path": "inputs/README.md", + "sha256": "68f52f2e0fa916cbf98e18896f0f6026469d3e45474e6d4314f95e0959cef6cb", + "git_blob": "bd68c6886162d433c7fe97c43a2954024996d28e", + "git_commit": "a467457692bc9e11113d9b2e2e34ea8ffb553b58", + "origin_url": "https://github.com/thu-nmrc/integer-mult-bounds/blob/a467457692bc9e11113d9b2e2e34ea8ffb553b58/research/p104-common-idle-double-retirement/README.md", + "usage": "inert literal source/opcode specification; never imported or executed" + }, + { + "local_path": "inputs/WITNESS.json", + "sha256": "4c820b99eb1ebebd7cd527f07b0aa86a355865072acace8bfc9fddd998086331", + "git_blob": "01c87980b187e0cbd8ea6385281eeab21512e311", + "git_commit": "a467457692bc9e11113d9b2e2e34ea8ffb553b58", + "origin_url": "https://github.com/thu-nmrc/integer-mult-bounds/blob/a467457692bc9e11113d9b2e2e34ea8ffb553b58/research/p104-common-idle-double-retirement/WITNESS.json", + "usage": "inert literal source/opcode specification; never imported or executed" + }, + { + "local_path": "inputs/CONTROLLER-UNRETIRED.json", + "sha256": "8c58adc35a7055dde1eda8f2547492dda9f558a73262fc17f439819c39d2555e", + "git_blob": "2a3c9e65fe704d878a68b58ace5dc06190918617", + "git_commit": "a467457692bc9e11113d9b2e2e34ea8ffb553b58", + "origin_url": "https://github.com/thu-nmrc/integer-mult-bounds/blob/a467457692bc9e11113d9b2e2e34ea8ffb553b58/research/p104-common-idle-double-retirement/CONTROLLER-UNRETIRED.json", + "usage": "inert literal source/opcode specification; never imported or executed" + }, + { + "local_path": "inputs/CONTROLLER.json", + "sha256": "2a0fb1c11fccfcc4dacbc7c82cf439969caa295dba4fc1a21a83e01b4ab8affc", + "git_blob": "97c6f04af7efe49ed982b843117120eaaf457d69", + "git_commit": "a467457692bc9e11113d9b2e2e34ea8ffb553b58", + "origin_url": "https://github.com/thu-nmrc/integer-mult-bounds/blob/a467457692bc9e11113d9b2e2e34ea8ffb553b58/research/p104-common-idle-double-retirement/CONTROLLER.json", + "usage": "inert literal source/opcode specification; never imported or executed" + }, + { + "local_path": "inputs/caller.py.txt", + "sha256": "ad0dd4aa97ae19f687defc8690e0ffb5f8ada551720aba4b48b8d307c776b5ba", + "git_blob": "9a7abb8ec7a89b756bfda80c82775364ec6583e8", + "git_commit": "a467457692bc9e11113d9b2e2e34ea8ffb553b58", + "origin_url": "https://github.com/thu-nmrc/integer-mult-bounds/blob/a467457692bc9e11113d9b2e2e34ea8ffb553b58/research/p104-common-idle-double-retirement/caller.py", + "usage": "inert literal source/opcode specification; never imported or executed" + } + ], + "scope": "Independent cut353/fresh34 audit over order4 sourceQ and18 formal commuting stage variables; source LOCAL operator contract assumed, no native physical admission." +} diff --git a/research/p104-cut353-independent-audit/SOURCES.json b/research/p104-cut353-independent-audit/SOURCES.json new file mode 100644 index 0000000000..75ea7c3d55 --- /dev/null +++ b/research/p104-cut353-independent-audit/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + } + ] +} diff --git a/research/p104-cut353-independent-audit/TASK.json b/research/p104-cut353-independent-audit/TASK.json new file mode 100644 index 0000000000..3d08ab2df4 --- /dev/null +++ b/research/p104-cut353-independent-audit/TASK.json @@ -0,0 +1,105 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "independent-moment", + "question": "Does a changed construction's serialized target/paid invoice independently support its claimed improvement?", + "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", + "docs/research/recursive-invoice-preflight.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": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.", + "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": "Independently recount one changed emitted word and its complete caller, importing no constructor or pricing engine. Include target losses, owned lifetimes, native orientation and extra charges. Check existing #5633/#5708/#5717/#5719 coverage to avoid duplicate audits and preserve its exact head. Stop after the chosen missing implication; a correct root alone is not supplier admission.", + "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": [ + "invoice", + "signed moment", + "productive target", + "independent recount" + ], + "existing_checks": [ + { + "scope": "PR #4088: mixed local/owner/phase ledger and moment reported.", + "evidence": "research/staged544-mixed-fourth-entry/README.md", + "remaining": "Independent binding of changed construction to paid histogram, distinct from full admission.", + "status": "author-checked", + "source_commit": "72d7efc181edb21806a878f174847c96dd410ab0", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4091: sharp pooled ceiling proposed for fixed THREE/FOUR words and inventory.", + "evidence": "research/staged-fourth-mixture-ceiling/README.md", + "remaining": "Validate dual, exhaustive pattern scope and exact source equivalence before applying to newer fills.", + "status": "author-checked", + "source_commit": "a29bdd8f56cd18b805917775cdec09ff935eddc4", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4067: paid (2,2) to (1,3) exchange and fixed OQ4 host reported.", + "evidence": "research/r437-two-window-carrier/README.md", + "remaining": "Independent full cost delta; remaining caller/precision/stock obligations are separate.", + "status": "author-checked", + "source_commit": "a95f11c52e3ca1e4c5171b3c20d8f4b0815aee2e", + "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": "Does literal unretired prefix353 satisfy all rational dual/corner identities and does final586word preserve35independent inputs with freshfield34 receiving plainD and no central factor?", + "scope_change_reason": "Take PR6716 explicit first-review request: independently certify one new productive-input split cut rather than reprice its full serialized invoice. Original complete paid/target gate remains unmet.", + "bottleneck_link": "Checks the exact independent-input legality gate of a newly proposed P104 productive split. The full source invoice and physical supplier admission remain separate.", + "budget_minutes": 60, + "stop_rule": "Mismatchedidentity/phase/freshaccess, incompleteendpoint, latecutoff20:32:21UTC; preservefailure; boundedpivotonlyifchangedpremisejustified.", + "outcome": "completed", + "evidence": "Two code-disjoint blind firsts agree on complete68cut+1225finalpolynomial cells, exactordinarydual/surgery/freshcontact and all35 independentoutputs. Normal/Oactualpacketchecks and regeneratedcanonicalvalues pass;10primary/7oraclecontrols plus20externalcases40CLIintendedrejections. No nativephysical/fullinvoice/compiler/outeradmission.", + "author": "ToikY", + "ai_assistance": "Substantial OpenAI Codex assistance, separate AI primary/independentoracle/static reviewer; no independenthuman or formal-kernel acceptance.", + "open_questions": [ + { + "question": "Does the same source satisfy complete physical/native ownership at this cut?", + "why_it_matters": "Formal role separation does not audit implicit native/helper/owned-bank addresses.", + "first_step": "Bind exact sourceLOCAL/native contacts and bank ownership to the cut353/fresh34 boundary.", + "blocked_by": "Nativeimplementation/address/ownedlifetimes and common-idlebank are inherited, not checked here." + }, + { + "question": "Does the complete source invoice, completion and outer transfer survive independent review?", + "why_it_matters": "This audit establishes a source-local algebraic legality gate only.", + "first_step": "Independently bind all emitted target/paidcounts and changed11/12completion to the exact same source head.", + "blocked_by": "No fullnative/price/compiler/outerreplay was run by this package." + } + ] +} diff --git a/research/p104-cut353-independent-audit/VALIDATION.md b/research/p104-cut353-independent-audit/VALIDATION.md new file mode 100644 index 0000000000..37ed6fa7ec --- /dev/null +++ b/research/p104-cut353-independent-audit/VALIDATION.md @@ -0,0 +1,17 @@ +# Validation and precise limits + +Two independent blind firsts passed, with separately frozen code and six exact inert inputs plus CASES/SCHEMA. Primary uses fullforward sparse Gaussian-rational Laurent matrices; oracle uses reverse covectors/rows and a forward column. Neither imports/runs source constructors, original native/pricing engines or peer code. Root read pinned caller.py as the opcode specification; that source file is included inert as caller.py.txt. + +Primary first:19:59:36UTC,0.172020125s,30,113,792B peakRSS. Oraclefirst:19:59:45UTC,0.111891875s,30,375,936B peakRSS, measured with managedCPython3.12.14/macOS26.5.2arm64. Exactargv/source/code/UTC/stdout/stderr/resources are retained in the local first records; RUN-RECORDS gives public receipt hashes and normalized command spelling. Both exit0 and empty stderr. No failed scientific first or post-first scientific correction. + +Whole common canonical SHA2569e9a7b5f05fc9e8824fc6206771625f91acf0aead53aae461cb0fdaf9afff6ef. Complete PACKET canonical SHA256ca09e50e074afde1af921461618e2f1d8349c643a16a6db0683f2a7efcd8e579; all68prefixvector+1225newendpointcells agree. Different pretty/compactcontainerbytes are retained, with mathematical equality over all canonical proof fields. Fourprimarystrictstages(firstnormalemit,retainednormal/O,optimizedregeneration), independentactualpacketnormal/O and fullcanonicalregeneration pass. Packagebytes unchanged across actualverification. + +Tenprimary controls include actual full-word wrongQUERYphase, wrongGcoefficient and unearnedfreshcentraloperation; sevenoraclecontrols include two actualreverse-engine wordmutants with explicit nonzero polynomialwitnesses and five typed-data controls. Twentyexternal mutationcases/40actualCLIcommands all reject on their first suite execution with intendeddiagnostics; sources/case/schema drift, absent files, duplicate/nonfinite/Boolean/float receipts, malformed/exact-type/canonicalpolynomialdata and wrongoffdiagonal/endpointshape are covered. Mutants exist only in a separate localcopy; originals restored. + +Beforefirst, static review corrected a no-op pairing mutant and replaced expected-object controls with actualenginecontrols; all unexecuted versions preserved. Scientific sourceinputs/cases/schema/code/firstreceipts/PACKET remain unchanged afterfirst. Oracle JSON parser accepts finite floats generally; exactinteger proof-field types and wholecanonicalreceipt equality reject such drift in proof-relevant positions. Do not claim a globally float-rejecting oracle decoder. + +The unretired34-fieldword is computed only through its354-event prefix; its complete targets remain authenticated declarations. The new586-event35-inputword is computed fully against independently assembledtargets. The exactsurgery and formalfirstcontact363 are checked. Physicalnative/helper/ownedbankaddresses, actual LOCAL implementation, common-idle noncontact, full price,11/12completion/compiler/outer and allfive selectedassumptions remain outside. This supplies a conditional finite-word symbolic identity, not a newκ or supplier admission. + +Root four registered commands,23file committed byte/declared-source-history/POSIX-mode preflight, official export with one declared PACKET input and all four read-only Git-free empty-PATH cold commands: PASS. Cold replay preserves every exported byte and0444/0555 file/directory mode. Hosted CI: PENDING; never infer a pass from the local checks. + +Metadata correction after science freeze: the first registered helper rejected outcome `completed_scoped_audit` before running any scientific command. The valid enum `completed` replaces it; the precise scoped result is unchanged. Original TASK/commit and diagnostic are retained. This is a TASK metadata correction in addition to later RUN/VALIDATION transport updates; no scientific code/input/receipt/artifact changed. diff --git a/research/p104-cut353-independent-audit/VERIFY.json b/research/p104-cut353-independent-audit/VERIFY.json new file mode 100644 index 0000000000..1d02e79146 --- /dev/null +++ b/research/p104-cut353-independent-audit/VERIFY.json @@ -0,0 +1,65 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p104-cut353-independent-audit/PACKET.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Complete68cut+1225retiredendpointpolynomialcells, exacttwo-sidedbasis/surgery/freshinput, sourcepins, actualretainedpacket and receipt; valid-engine semanticnegativecontrols. ConditionalLOCAL/sourcecommutationonly." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "-O", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Complete68cut+1225retiredendpointpolynomialcells, exacttwo-sidedbasis/surgery/freshinput, sourcepins, actualretainedpacket and receipt; valid-engine semanticnegativecontrols. ConditionalLOCAL/sourcecommutationonly." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/oracle.py", + "--package", + "{package}" + ], + "timeout_seconds": 180, + "checks": "Complete68cut+1225retiredendpointpolynomialcells, exacttwo-sidedbasis/surgery/freshinput, sourcepins, actualretainedpacket and receipt; valid-engine semanticnegativecontrols. ConditionalLOCAL/sourcecommutationonly." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "-O", + "{package}/oracle.py", + "--package", + "{package}" + ], + "timeout_seconds": 180, + "checks": "Complete68cut+1225retiredendpointpolynomialcells, exacttwo-sidedbasis/surgery/freshinput, sourcepins, actualretainedpacket and receipt; valid-engine semanticnegativecontrols. ConditionalLOCAL/sourcecommutationonly." + } + ] +} diff --git a/research/p104-cut353-independent-audit/inputs/CONTROLLER-UNRETIRED.json b/research/p104-cut353-independent-audit/inputs/CONTROLLER-UNRETIRED.json new file mode 100644 index 0000000000..2a3c9e65fe --- /dev/null +++ b/research/p104-cut353-independent-audit/inputs/CONTROLLER-UNRETIRED.json @@ -0,0 +1,4041 @@ +{ + "schema": "root8-common-idle-fusion/1", + "roles": 34, + "stages": 18, + "ambient_rank": 153, + "events": [ + [ + "ADD", + 0, + 1, + "-1" + ], + [ + "SWAP", + 0, + 1 + ], + [ + "SWAP", + 0, + 9 + ], + [ + "SWAP", + 1, + 8 + ], + [ + "SWAP", + 8, + 9 + ], + [ + "ADD", + 0, + 8, + "1" + ], + [ + "ADD", + 9, + 1, + "-1" + ], + [ + "LAMBDA", + 8, + -1 + ], + [ + "QUERY", + 8, + 9, + -1 + ], + [ + "LAMBDA", + 8, + 1 + ], + [ + "ADD", + 9, + 1, + "1" + ], + [ + "ADD", + 0, + 8, + "-1" + ], + [ + "IDLE", + 8, + 9, + [ + 1, + 2, + 3, + 4 + ] + ], + [ + "SCALE", + 1, + "-1" + ], + [ + "SWAP", + 1, + 11 + ], + [ + "SWAP", + 0, + 10 + ], + [ + "SWAP", + 10, + 11 + ], + [ + "ADD", + 1, + 10, + "1" + ], + [ + "ADD", + 11, + 0, + "-1" + ], + [ + "LAMBDA", + 10, + -1 + ], + [ + "QUERY", + 10, + 11, + -1 + ], + [ + "LAMBDA", + 10, + 1 + ], + [ + "ADD", + 11, + 0, + "1" + ], + [ + "ADD", + 1, + 10, + "-1" + ], + [ + "IDLE", + 10, + 11, + [ + 1, + 2 + ] + ], + [ + "SCALE", + 0, + "-1" + ], + [ + "LAMBDA", + 0, + -1 + ], + [ + "LOCAL", + 1, + 1, + 0 + ], + [ + "LAMBDA", + 0, + 1 + ], + [ + "SCALE", + 0, + "-1" + ], + [ + "LAMBDA", + 1, + -1 + ], + [ + "LOCAL", + 2, + 0, + 1 + ], + [ + "LAMBDA", + 1, + 1 + ], + [ + "ADD", + 1, + 10, + "1" + ], + [ + "SCALE", + 10, + "-1" + ], + [ + "ADD", + 10, + 1, + "1" + ], + [ + "SWAP", + 0, + 11 + ], + [ + "SCALE", + 11, + "-1" + ], + [ + "ADD", + 11, + 0, + "1" + ], + [ + "SCALE", + 1, + "-1" + ], + [ + "SWAP", + 0, + 13 + ], + [ + "SWAP", + 1, + 12 + ], + [ + "SWAP", + 12, + 13 + ], + [ + "ADD", + 0, + 12, + "1" + ], + [ + "ADD", + 13, + 1, + "-1" + ], + [ + "LAMBDA", + 12, + -1 + ], + [ + "QUERY", + 12, + 13, + -1 + ], + [ + "LAMBDA", + 12, + 1 + ], + [ + "ADD", + 13, + 1, + "1" + ], + [ + "ADD", + 0, + 12, + "-1" + ], + [ + "IDLE", + 12, + 13, + [ + 3, + 4 + ] + ], + [ + "SCALE", + 1, + "-1" + ], + [ + "LAMBDA", + 1, + -1 + ], + [ + "LOCAL", + 3, + 0, + 1 + ], + [ + "LAMBDA", + 1, + 1 + ], + [ + "SCALE", + 1, + "-1" + ], + [ + "LAMBDA", + 0, + -1 + ], + [ + "LOCAL", + 4, + 1, + 0 + ], + [ + "LAMBDA", + 0, + 1 + ], + [ + "ADD", + 0, + 12, + "1" + ], + [ + "SCALE", + 12, + "-1" + ], + [ + "ADD", + 12, + 0, + "1" + ], + [ + "SWAP", + 1, + 13 + ], + [ + "SCALE", + 13, + "-1" + ], + [ + "ADD", + 13, + 1, + "1" + ], + [ + "ADD", + 0, + 8, + "1" + ], + [ + "SCALE", + 8, + "-1" + ], + [ + "ADD", + 8, + 0, + "1" + ], + [ + "SWAP", + 1, + 9 + ], + [ + "SCALE", + 9, + "-1" + ], + [ + "ADD", + 9, + 1, + "1" + ], + [ + "ADD", + 0, + 1, + "-1" + ], + [ + "ADD", + 0, + 1, + "1" + ], + [ + "SCALE", + 1, + "-1" + ], + [ + "ADD", + 1, + 0, + "1" + ], + [ + "ADD", + 0, + 7, + "-1/2" + ], + [ + "ADD", + 7, + 6, + "29/2" + ], + [ + "ADD", + 1, + 6, + "-4" + ], + [ + "ADD", + 0, + 6, + "-37/4" + ], + [ + "SCALE", + 6, + "-1/2" + ], + [ + "SWAP", + 5, + 7 + ], + [ + "SWAP", + 4, + 6 + ], + [ + "SWAP", + 3, + 5 + ], + [ + "SWAP", + 2, + 4 + ], + [ + "SWAP", + 1, + 2 + ], + [ + "ADD", + 3, + 0, + "2" + ], + [ + "ADD", + 1, + 0, + "1/4" + ], + [ + "SCALE", + 0, + "1/4" + ], + [ + "SWAP", + 0, + 15 + ], + [ + "SWAP", + 1, + 14 + ], + [ + "SWAP", + 14, + 15 + ], + [ + "ADD", + 0, + 14, + "1" + ], + [ + "ADD", + 15, + 1, + "-1" + ], + [ + "LAMBDA", + 14, + -1 + ], + [ + "QUERY", + 14, + 15, + -1 + ], + [ + "LAMBDA", + 14, + 1 + ], + [ + "ADD", + 15, + 1, + "1" + ], + [ + "ADD", + 0, + 14, + "-1" + ], + [ + "IDLE", + 14, + 15, + [ + 5, + 6 + ] + ], + [ + "SCALE", + 1, + "-1" + ], + [ + "LAMBDA", + 1, + -1 + ], + [ + "LOCAL", + 5, + 0, + 1 + ], + [ + "LAMBDA", + 1, + 1 + ], + [ + "SCALE", + 1, + "-1" + ], + [ + "LAMBDA", + 0, + -1 + ], + [ + "LOCAL", + 6, + 1, + 0 + ], + [ + "LAMBDA", + 0, + 1 + ], + [ + "ADD", + 0, + 14, + "1" + ], + [ + "SCALE", + 14, + "-1" + ], + [ + "ADD", + 14, + 0, + "1" + ], + [ + "SWAP", + 1, + 15 + ], + [ + "SCALE", + 15, + "-1" + ], + [ + "ADD", + 15, + 1, + "1" + ], + [ + "ADD", + 0, + 1, + "-1" + ], + [ + "SCALE", + 1, + "-1" + ], + [ + "SWAP", + 1, + 17 + ], + [ + "SWAP", + 0, + 16 + ], + [ + "SWAP", + 16, + 17 + ], + [ + "ADD", + 1, + 16, + "1" + ], + [ + "ADD", + 17, + 0, + "-1" + ], + [ + "LAMBDA", + 16, + -1 + ], + [ + "QUERY", + 16, + 17, + -1 + ], + [ + "LAMBDA", + 16, + 1 + ], + [ + "ADD", + 17, + 0, + "1" + ], + [ + "ADD", + 1, + 16, + "-1" + ], + [ + "IDLE", + 16, + 17, + [ + 7, + 8, + 9 + ] + ], + [ + "SCALE", + 0, + "-1" + ], + [ + "LAMBDA", + 0, + -1 + ], + [ + "LOCAL", + 7, + 1, + 0 + ], + [ + "LAMBDA", + 0, + 1 + ], + [ + "SCALE", + 0, + "-1" + ], + [ + "SWAP", + 1, + 19 + ], + [ + "SWAP", + 0, + 18 + ], + [ + "SWAP", + 18, + 19 + ], + [ + "ADD", + 1, + 18, + "1" + ], + [ + "ADD", + 19, + 0, + "-1" + ], + [ + "LAMBDA", + 18, + -1 + ], + [ + "QUERY", + 18, + 19, + -1 + ], + [ + "LAMBDA", + 18, + 1 + ], + [ + "ADD", + 19, + 0, + "1" + ], + [ + "ADD", + 1, + 18, + "-1" + ], + [ + "IDLE", + 18, + 19, + [ + 8, + 9 + ] + ], + [ + "SCALE", + 0, + "-1" + ], + [ + "LAMBDA", + 0, + -1 + ], + [ + "LOCAL", + 8, + 1, + 0 + ], + [ + "LAMBDA", + 0, + 1 + ], + [ + "SCALE", + 0, + "-1" + ], + [ + "LAMBDA", + 1, + -1 + ], + [ + "LOCAL", + 9, + 0, + 1 + ], + [ + "LAMBDA", + 1, + 1 + ], + [ + "ADD", + 1, + 18, + "1" + ], + [ + "SCALE", + 18, + "-1" + ], + [ + "ADD", + 18, + 1, + "1" + ], + [ + "SWAP", + 0, + 19 + ], + [ + "SCALE", + 19, + "-1" + ], + [ + "ADD", + 19, + 0, + "1" + ], + [ + "ADD", + 1, + 16, + "1" + ], + [ + "SCALE", + 16, + "-1" + ], + [ + "ADD", + 16, + 1, + "1" + ], + [ + "SWAP", + 0, + 17 + ], + [ + "SCALE", + 17, + "-1" + ], + [ + "ADD", + 17, + 0, + "1" + ], + [ + "SCALE", + 1, + "-1" + ], + [ + "ADD", + 1, + 0, + "1" + ], + [ + "IDLE", + 2, + 3, + [ + 5, + 6, + 7, + 8, + 9 + ] + ], + [ + "SWAP", + 6, + 7 + ], + [ + "SWAP", + 5, + 6 + ], + [ + "SWAP", + 4, + 7 + ], + [ + "ADD", + 2, + 3, + "-1" + ], + [ + "ADD", + 1, + 3, + "-45/64" + ], + [ + "ADD", + 0, + 3, + "-37/64" + ], + [ + "SCALE", + 3, + "-1/4" + ], + [ + "SWAP", + 3, + 6 + ], + [ + "SWAP", + 2, + 7 + ], + [ + "ADD", + 0, + 1, + "-1" + ], + [ + "SCALE", + 1, + "-8" + ], + [ + "SWAP", + 1, + 7 + ], + [ + "ADD", + 7, + 0, + "-37" + ], + [ + "ADD", + 6, + 0, + "2" + ], + [ + "ADD", + 1, + 0, + "8" + ], + [ + "SCALE", + 0, + "4" + ], + [ + "ADD", + 5, + 7, + "1/4" + ], + [ + "ADD", + 1, + 7, + "-1/2" + ], + [ + "ADD", + 0, + 7, + "-1/4" + ], + [ + "SCALE", + 7, + "1/4" + ], + [ + "SWAP", + 6, + 7 + ], + [ + "ADD", + 0, + 5, + "1" + ], + [ + "SWAP", + 5, + 6 + ], + [ + "SWAP", + 4, + 5 + ], + [ + "SWAP", + 3, + 4 + ], + [ + "SWAP", + 2, + 3 + ], + [ + "SWAP", + 1, + 2 + ], + [ + "SWAP", + 0, + 1 + ], + [ + "LAMBDA", + 0, + -1 + ], + [ + "QUERY", + 0, + 1, + -1 + ], + [ + "LAMBDA", + 0, + 1 + ], + [ + "ADD", + 0, + 1, + "-1" + ], + [ + "ADD", + 2, + 6, + "2" + ], + [ + "ADD", + 0, + 6, + "-1" + ], + [ + "SCALE", + 6, + "4" + ], + [ + "SWAP", + 6, + 7 + ], + [ + "SWAP", + 4, + 5 + ], + [ + "SWAP", + 3, + 5 + ], + [ + "ADD", + 7, + 2, + "-2" + ], + [ + "ADD", + 1, + 2, + "-1/2" + ], + [ + "ADD", + 0, + 2, + "1/2" + ], + [ + "SCALE", + 2, + "1/2" + ], + [ + "SWAP", + 2, + 5 + ], + [ + "ADD", + 7, + 1, + "-4" + ], + [ + "ADD", + 5, + 1, + "1" + ], + [ + "ADD", + 0, + 1, + "1" + ], + [ + "SCALE", + 1, + "-2" + ], + [ + "ADD", + 7, + 0, + "4" + ], + [ + "ADD", + 5, + 0, + "-1" + ], + [ + "ADD", + 1, + 0, + "2" + ], + [ + "ADD", + 1, + 6, + "-2" + ], + [ + "ADD", + 1, + 5, + "1" + ], + [ + "ADD", + 2, + 4, + "-1" + ], + [ + "ADD", + 0, + 4, + "1/2" + ], + [ + "SCALE", + 4, + "1/2" + ], + [ + "ADD", + 1, + 3, + "1" + ], + [ + "SWAP", + 3, + 4 + ], + [ + "ADD", + 1, + 2, + "-1" + ], + [ + "SWAP", + 2, + 3 + ], + [ + "SWAP", + 0, + 2 + ], + [ + "LAMBDA", + 0, + -1 + ], + [ + "QUERY", + 0, + 1, + -1 + ], + [ + "LAMBDA", + 0, + 1 + ], + [ + "ADD", + 0, + 1, + "-1" + ], + [ + "ADD", + 1, + 6, + "2" + ], + [ + "ADD", + 1, + 5, + "-1" + ], + [ + "ADD", + 1, + 4, + "-1" + ], + [ + "ADD", + 2, + 3, + "1/2" + ], + [ + "ADD", + 1, + 3, + "1" + ], + [ + "ADD", + 0, + 3, + "1/2" + ], + [ + "SCALE", + 3, + "-1" + ], + [ + "SWAP", + 3, + 4 + ], + [ + "ADD", + 4, + 2, + "2" + ], + [ + "ADD", + 0, + 2, + "-1" + ], + [ + "SCALE", + 2, + "2" + ], + [ + "ADD", + 4, + 0, + "2" + ], + [ + "ADD", + 2, + 0, + "2" + ], + [ + "SCALE", + 0, + "-1" + ], + [ + "ADD", + 5, + 7, + "1/2" + ], + [ + "ADD", + 4, + 7, + "3/2" + ], + [ + "ADD", + 3, + 7, + "-1/2" + ], + [ + "ADD", + 2, + 7, + "3/2" + ], + [ + "ADD", + 1, + 7, + "-1/2" + ], + [ + "ADD", + 0, + 7, + "-1" + ], + [ + "SCALE", + 7, + "1/2" + ], + [ + "ADD", + 0, + 6, + "4" + ], + [ + "SWAP", + 6, + 7 + ], + [ + "ADD", + 0, + 5, + "-2" + ], + [ + "SWAP", + 5, + 6 + ], + [ + "ADD", + 0, + 4, + "-2" + ], + [ + "SWAP", + 4, + 5 + ], + [ + "ADD", + 0, + 3, + "-2" + ], + [ + "SWAP", + 3, + 4 + ], + [ + "ADD", + 0, + 2, + "2" + ], + [ + "SWAP", + 2, + 3 + ], + [ + "ADD", + 0, + 1, + "-2" + ], + [ + "SWAP", + 1, + 2 + ], + [ + "SWAP", + 0, + 1 + ], + [ + "LAMBDA", + 0, + -1 + ], + [ + "QUERY", + 0, + 1, + -1 + ], + [ + "LAMBDA", + 0, + 1 + ], + [ + "ADD", + 0, + 1, + "-1" + ], + [ + "ADD", + 1, + 7, + "-4" + ], + [ + "ADD", + 5, + 6, + "-3" + ], + [ + "ADD", + 4, + 6, + "1" + ], + [ + "ADD", + 3, + 6, + "-3" + ], + [ + "ADD", + 2, + 6, + "1" + ], + [ + "ADD", + 0, + 6, + "-1" + ], + [ + "SCALE", + 6, + "2" + ], + [ + "SWAP", + 6, + 7 + ], + [ + "ADD", + 1, + 5, + "2" + ], + [ + "ADD", + 7, + 4, + "-2" + ], + [ + "ADD", + 5, + 4, + "3" + ], + [ + "ADD", + 3, + 4, + "3" + ], + [ + "ADD", + 2, + 4, + "-1" + ], + [ + "ADD", + 1, + 4, + "8" + ], + [ + "ADD", + 0, + 4, + "1" + ], + [ + "SWAP", + 4, + 5 + ], + [ + "ADD", + 1, + 3, + "-2" + ], + [ + "ADD", + 7, + 2, + "-2" + ], + [ + "ADD", + 5, + 2, + "1" + ], + [ + "ADD", + 4, + 2, + "3" + ], + [ + "ADD", + 3, + 2, + "3" + ], + [ + "ADD", + 0, + 2, + "1" + ], + [ + "SCALE", + 2, + "-1" + ], + [ + "SWAP", + 2, + 3 + ], + [ + "ADD", + 7, + 1, + "-1" + ], + [ + "ADD", + 5, + 1, + "1/2" + ], + [ + "ADD", + 4, + 1, + "3/2" + ], + [ + "ADD", + 3, + 1, + "-1/2" + ], + [ + "ADD", + 2, + 1, + "3/2" + ], + [ + "ADD", + 0, + 1, + "1/2" + ], + [ + "SCALE", + 1, + "-1/2" + ], + [ + "ADD", + 7, + 0, + "2" + ], + [ + "ADD", + 5, + 0, + "-1" + ], + [ + "ADD", + 4, + 0, + "-3" + ], + [ + "ADD", + 3, + 0, + "1" + ], + [ + "ADD", + 2, + 0, + "-3" + ], + [ + "ADD", + 1, + 0, + "1" + ], + [ + "SCALE", + 0, + "2" + ], + [ + "ADD", + 0, + 6, + "4" + ], + [ + "ADD", + 0, + 5, + "-2" + ], + [ + "ADD", + 3, + 4, + "1/2" + ], + [ + "ADD", + 2, + 4, + "-1" + ], + [ + "ADD", + 0, + 4, + "1/2" + ], + [ + "SCALE", + 4, + "-1/2" + ], + [ + "ADD", + 0, + 3, + "-1" + ], + [ + "SWAP", + 3, + 4 + ], + [ + "ADD", + 0, + 2, + "2" + ], + [ + "SWAP", + 2, + 3 + ], + [ + "ADD", + 0, + 1, + "-2" + ], + [ + "SWAP", + 1, + 2 + ], + [ + "SWAP", + 0, + 1 + ], + [ + "LAMBDA", + 0, + -1 + ], + [ + "QUERY", + 0, + 1, + -1 + ], + [ + "LAMBDA", + 0, + 1 + ], + [ + "ADD", + 0, + 1, + "-1" + ], + [ + "ADD", + 1, + 6, + "-4" + ], + [ + "ADD", + 1, + 5, + "2" + ], + [ + "ADD", + 3, + 4, + "2" + ], + [ + "ADD", + 1, + 4, + "4" + ], + [ + "ADD", + 0, + 4, + "1" + ], + [ + "SCALE", + 4, + "2" + ], + [ + "ADD", + 4, + 3, + "-1" + ], + [ + "ADD", + 1, + 3, + "-3/2" + ], + [ + "ADD", + 0, + 3, + "-1/2" + ], + [ + "SCALE", + 3, + "1/2" + ], + [ + "ADD", + 1, + 2, + "2" + ], + [ + "ADD", + 4, + 1, + "2" + ], + [ + "ADD", + 3, + 1, + "-1" + ], + [ + "ADD", + 0, + 1, + "1" + ], + [ + "SCALE", + 1, + "2" + ], + [ + "SWAP", + 1, + 2 + ], + [ + "ADD", + 4, + 0, + "-2" + ], + [ + "ADD", + 3, + 0, + "1" + ], + [ + "ADD", + 2, + 0, + "-2" + ], + [ + "ADD", + 2, + 4, + "-2" + ], + [ + "ADD", + 0, + 4, + "1" + ], + [ + "SWAP", + 3, + 4 + ], + [ + "SWAP", + 1, + 3 + ], + [ + "SWAP", + 0, + 1 + ], + [ + "SWAP", + 0, + 21 + ], + [ + "SWAP", + 1, + 20 + ], + [ + "SWAP", + 20, + 21 + ], + [ + "ADD", + 0, + 20, + "1" + ], + [ + "ADD", + 21, + 1, + "-1" + ], + [ + "LAMBDA", + 20, + -1 + ], + [ + "QUERY", + 20, + 21, + -1 + ], + [ + "LAMBDA", + 20, + 1 + ], + [ + "ADD", + 21, + 1, + "1" + ], + [ + "ADD", + 0, + 20, + "-1" + ], + [ + "IDLE", + 20, + 21, + [ + 10, + 11, + 12, + 13 + ] + ], + [ + "SCALE", + 1, + "-1" + ], + [ + "SWAP", + 1, + 23 + ], + [ + "SWAP", + 0, + 22 + ], + [ + "SWAP", + 22, + 23 + ], + [ + "ADD", + 1, + 22, + "1" + ], + [ + "ADD", + 23, + 0, + "-1" + ], + [ + "LAMBDA", + 22, + -1 + ], + [ + "QUERY", + 22, + 23, + -1 + ], + [ + "LAMBDA", + 22, + 1 + ], + [ + "ADD", + 23, + 0, + "1" + ], + [ + "ADD", + 1, + 22, + "-1" + ], + [ + "IDLE", + 22, + 23, + [ + 10, + 11 + ] + ], + [ + "SCALE", + 0, + "-1" + ], + [ + "LAMBDA", + 0, + -1 + ], + [ + "LOCAL", + 10, + 1, + 0 + ], + [ + "LAMBDA", + 0, + 1 + ], + [ + "SCALE", + 0, + "-1" + ], + [ + "LAMBDA", + 1, + -1 + ], + [ + "LOCAL", + 11, + 0, + 1 + ], + [ + "LAMBDA", + 1, + 1 + ], + [ + "ADD", + 1, + 22, + "1" + ], + [ + "SCALE", + 22, + "-1" + ], + [ + "ADD", + 22, + 1, + "1" + ], + [ + "SWAP", + 0, + 23 + ], + [ + "SCALE", + 23, + "-1" + ], + [ + "ADD", + 23, + 0, + "1" + ], + [ + "SCALE", + 1, + "-1" + ], + [ + "SWAP", + 0, + 25 + ], + [ + "SWAP", + 1, + 24 + ], + [ + "SWAP", + 24, + 25 + ], + [ + "ADD", + 0, + 24, + "1" + ], + [ + "ADD", + 25, + 1, + "-1" + ], + [ + "LAMBDA", + 24, + -1 + ], + [ + "QUERY", + 24, + 25, + -1 + ], + [ + "LAMBDA", + 24, + 1 + ], + [ + "ADD", + 25, + 1, + "1" + ], + [ + "ADD", + 0, + 24, + "-1" + ], + [ + "IDLE", + 24, + 25, + [ + 12, + 13 + ] + ], + [ + "SCALE", + 1, + "-1" + ], + [ + "LAMBDA", + 1, + -1 + ], + [ + "LOCAL", + 12, + 0, + 1 + ], + [ + "LAMBDA", + 1, + 1 + ], + [ + "SCALE", + 1, + "-1" + ], + [ + "LAMBDA", + 0, + -1 + ], + [ + "LOCAL", + 13, + 1, + 0 + ], + [ + "LAMBDA", + 0, + 1 + ], + [ + "ADD", + 0, + 24, + "1" + ], + [ + "SCALE", + 24, + "-1" + ], + [ + "ADD", + 24, + 0, + "1" + ], + [ + "SWAP", + 1, + 25 + ], + [ + "SCALE", + 25, + "-1" + ], + [ + "ADD", + 25, + 1, + "1" + ], + [ + "ADD", + 0, + 20, + "1" + ], + [ + "SCALE", + 20, + "-1" + ], + [ + "ADD", + 20, + 0, + "1" + ], + [ + "SWAP", + 1, + 21 + ], + [ + "SCALE", + 21, + "-1" + ], + [ + "ADD", + 21, + 1, + "1" + ], + [ + "ADD", + 0, + 1, + "-1" + ], + [ + "IDLE_ONE", + 2, + [ + 10, + 11, + 12, + 13 + ] + ], + [ + "SWAP", + 3, + 4 + ], + [ + "ADD", + 1, + 2, + "1/2" + ], + [ + "ADD", + 0, + 2, + "1/2" + ], + [ + "SCALE", + 2, + "-1/2" + ], + [ + "SWAP", + 2, + 4 + ], + [ + "ADD", + 4, + 1, + "1" + ], + [ + "ADD", + 0, + 1, + "-1" + ], + [ + "SCALE", + 1, + "2" + ], + [ + "SWAP", + 1, + 2 + ], + [ + "ADD", + 4, + 0, + "1" + ], + [ + "ADD", + 2, + 0, + "2" + ], + [ + "SCALE", + 0, + "-1" + ], + [ + "ADD", + 0, + 2, + "1" + ], + [ + "SWAP", + 1, + 2 + ], + [ + "SWAP", + 0, + 1 + ], + [ + "SWAP", + 0, + 27 + ], + [ + "SWAP", + 1, + 26 + ], + [ + "SWAP", + 26, + 27 + ], + [ + "ADD", + 0, + 26, + "1" + ], + [ + "ADD", + 27, + 1, + "-1" + ], + [ + "LAMBDA", + 26, + -1 + ], + [ + "QUERY", + 26, + 27, + -1 + ], + [ + "LAMBDA", + 26, + 1 + ], + [ + "ADD", + 27, + 1, + "1" + ], + [ + "ADD", + 0, + 26, + "-1" + ], + [ + "IDLE", + 26, + 27, + [ + 14, + 15, + 16, + 17, + 18 + ] + ], + [ + "SCALE", + 1, + "-1" + ], + [ + "SWAP", + 1, + 29 + ], + [ + "SWAP", + 0, + 28 + ], + [ + "SWAP", + 28, + 29 + ], + [ + "ADD", + 1, + 28, + "1" + ], + [ + "ADD", + 29, + 0, + "-1" + ], + [ + "LAMBDA", + 28, + -1 + ], + [ + "QUERY", + 28, + 29, + -1 + ], + [ + "LAMBDA", + 28, + 1 + ], + [ + "ADD", + 29, + 0, + "1" + ], + [ + "ADD", + 1, + 28, + "-1" + ], + [ + "IDLE", + 28, + 29, + [ + 14, + 15 + ] + ], + [ + "SCALE", + 0, + "-1" + ], + [ + "LAMBDA", + 0, + -1 + ], + [ + "LOCAL", + 14, + 1, + 0 + ], + [ + "LAMBDA", + 0, + 1 + ], + [ + "SCALE", + 0, + "-1" + ], + [ + "LAMBDA", + 1, + -1 + ], + [ + "LOCAL", + 15, + 0, + 1 + ], + [ + "LAMBDA", + 1, + 1 + ], + [ + "ADD", + 1, + 28, + "1" + ], + [ + "SCALE", + 28, + "-1" + ], + [ + "ADD", + 28, + 1, + "1" + ], + [ + "SWAP", + 0, + 29 + ], + [ + "SCALE", + 29, + "-1" + ], + [ + "ADD", + 29, + 0, + "1" + ], + [ + "SCALE", + 1, + "-1" + ], + [ + "SWAP", + 0, + 31 + ], + [ + "SWAP", + 1, + 30 + ], + [ + "SWAP", + 30, + 31 + ], + [ + "ADD", + 0, + 30, + "1" + ], + [ + "ADD", + 31, + 1, + "-1" + ], + [ + "LAMBDA", + 30, + -1 + ], + [ + "QUERY", + 30, + 31, + -1 + ], + [ + "LAMBDA", + 30, + 1 + ], + [ + "ADD", + 31, + 1, + "1" + ], + [ + "ADD", + 0, + 30, + "-1" + ], + [ + "IDLE", + 30, + 31, + [ + 16, + 17, + 18 + ] + ], + [ + "SCALE", + 1, + "-1" + ], + [ + "LAMBDA", + 1, + -1 + ], + [ + "LOCAL", + 16, + 0, + 1 + ], + [ + "LAMBDA", + 1, + 1 + ], + [ + "SCALE", + 1, + "-1" + ], + [ + "SWAP", + 0, + 33 + ], + [ + "SWAP", + 1, + 32 + ], + [ + "SWAP", + 32, + 33 + ], + [ + "ADD", + 0, + 32, + "1" + ], + [ + "ADD", + 33, + 1, + "-1" + ], + [ + "LAMBDA", + 32, + -1 + ], + [ + "QUERY", + 32, + 33, + -1 + ], + [ + "LAMBDA", + 32, + 1 + ], + [ + "ADD", + 33, + 1, + "1" + ], + [ + "ADD", + 0, + 32, + "-1" + ], + [ + "IDLE", + 32, + 33, + [ + 17, + 18 + ] + ], + [ + "SCALE", + 1, + "-1" + ], + [ + "LAMBDA", + 1, + -1 + ], + [ + "LOCAL", + 17, + 0, + 1 + ], + [ + "LAMBDA", + 1, + 1 + ], + [ + "SCALE", + 1, + "-1" + ], + [ + "LAMBDA", + 0, + -1 + ], + [ + "LOCAL", + 18, + 1, + 0 + ], + [ + "LAMBDA", + 0, + 1 + ], + [ + "ADD", + 0, + 32, + "1" + ], + [ + "SCALE", + 32, + "-1" + ], + [ + "ADD", + 32, + 0, + "1" + ], + [ + "SWAP", + 1, + 33 + ], + [ + "SCALE", + 33, + "-1" + ], + [ + "ADD", + 33, + 1, + "1" + ], + [ + "ADD", + 0, + 30, + "1" + ], + [ + "SCALE", + 30, + "-1" + ], + [ + "ADD", + 30, + 0, + "1" + ], + [ + "SWAP", + 1, + 31 + ], + [ + "SCALE", + 31, + "-1" + ], + [ + "ADD", + 31, + 1, + "1" + ], + [ + "ADD", + 0, + 26, + "1" + ], + [ + "SCALE", + 26, + "-1" + ], + [ + "ADD", + 26, + 0, + "1" + ], + [ + "SWAP", + 1, + 27 + ], + [ + "SCALE", + 27, + "-1" + ], + [ + "ADD", + 27, + 1, + "1" + ], + [ + "ADD", + 0, + 1, + "-1" + ], + [ + "ADD", + 0, + 1, + "-1" + ], + [ + "SWAP", + 1, + 2 + ], + [ + "ADD", + 2, + 0, + "1" + ], + [ + "SCALE", + 0, + "-1" + ], + [ + "LAMBDA", + 0, + -1 + ], + [ + "LAMBDA", + 1, + -1 + ], + [ + "LAMBDA", + 2, + -1 + ], + [ + "LAMBDA", + 3, + -1 + ], + [ + "LAMBDA", + 4, + -1 + ], + [ + "LAMBDA", + 5, + -1 + ], + [ + "LAMBDA", + 6, + -1 + ], + [ + "LAMBDA", + 7, + -1 + ], + [ + "LAMBDA", + 8, + -1 + ], + [ + "LAMBDA", + 9, + -1 + ], + [ + "LAMBDA", + 10, + -1 + ], + [ + "LAMBDA", + 11, + -1 + ], + [ + "LAMBDA", + 12, + -1 + ], + [ + "LAMBDA", + 13, + -1 + ], + [ + "LAMBDA", + 14, + -1 + ], + [ + "LAMBDA", + 15, + -1 + ], + [ + "LAMBDA", + 16, + -1 + ], + [ + "LAMBDA", + 17, + -1 + ], + [ + "LAMBDA", + 18, + -1 + ], + [ + "LAMBDA", + 19, + -1 + ], + [ + "LAMBDA", + 20, + -1 + ], + [ + "LAMBDA", + 21, + -1 + ], + [ + "LAMBDA", + 22, + -1 + ], + [ + "LAMBDA", + 23, + -1 + ], + [ + "LAMBDA", + 24, + -1 + ], + [ + "LAMBDA", + 25, + -1 + ], + [ + "LAMBDA", + 26, + -1 + ], + [ + "LAMBDA", + 27, + -1 + ], + [ + "LAMBDA", + 28, + -1 + ], + [ + "LAMBDA", + 29, + -1 + ], + [ + "LAMBDA", + 30, + -1 + ], + [ + "LAMBDA", + 31, + -1 + ], + [ + "LAMBDA", + 32, + -1 + ], + [ + "LAMBDA", + 33, + -1 + ] + ], + "diagonal": [ + [ + -1, + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + [ + -1, + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + [ + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 0 + ], + [ + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + -1, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + -1, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + -1, + 0, + 1, + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + -1, + 0, + 1, + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + -1, + 0, + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + -1, + 0, + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + -1, + 0, + 0, + 0, + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + -1, + 0, + 0, + 0, + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + -1, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + -1, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 0 + ], + [ + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 0 + ], + [ + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 0, + 0, + 0, + 0, + 0 + ], + [ + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 0, + 0, + 0, + 0, + 0 + ], + [ + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 1 + ], + [ + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 1 + ], + [ + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 0, + 0, + 0 + ], + [ + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 0, + 0, + 0 + ], + [ + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1 + ], + [ + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1 + ], + [ + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1 + ], + [ + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1 + ] + ], + "nodes": [ + { + "roles": [ + 8, + 9 + ], + "stages": [ + 1, + 2, + 3, + 4 + ] + }, + { + "roles": [ + 10, + 11 + ], + "stages": [ + 1, + 2 + ] + }, + { + "roles": [ + 12, + 13 + ], + "stages": [ + 3, + 4 + ] + }, + { + "roles": [ + 14, + 15 + ], + "stages": [ + 5, + 6 + ] + }, + { + "roles": [ + 16, + 17 + ], + "stages": [ + 7, + 8, + 9 + ] + }, + { + "roles": [ + 18, + 19 + ], + "stages": [ + 8, + 9 + ] + }, + { + "roles": [ + 20, + 21 + ], + "stages": [ + 10, + 11, + 12, + 13 + ] + }, + { + "roles": [ + 22, + 23 + ], + "stages": [ + 10, + 11 + ] + }, + { + "roles": [ + 24, + 25 + ], + "stages": [ + 12, + 13 + ] + }, + { + "roles": [ + 26, + 27 + ], + "stages": [ + 14, + 15, + 16, + 17, + 18 + ] + }, + { + "roles": [ + 28, + 29 + ], + "stages": [ + 14, + 15 + ] + }, + { + "roles": [ + 30, + 31 + ], + "stages": [ + 16, + 17, + 18 + ] + }, + { + "roles": [ + 32, + 33 + ], + "stages": [ + 17, + 18 + ] + } + ] +} diff --git a/research/p104-cut353-independent-audit/inputs/CONTROLLER.json b/research/p104-cut353-independent-audit/inputs/CONTROLLER.json new file mode 100644 index 0000000000..97c6f04af7 --- /dev/null +++ b/research/p104-cut353-independent-audit/inputs/CONTROLLER.json @@ -0,0 +1,4197 @@ +{ + "schema": "root8-common-idle-fusion/1", + "roles": 35, + "stages": 18, + "ambient_rank": 153, + "events": [ + [ + "ADD", + 4, + 20, + "-1" + ], + [ + "ADD", + 21, + 4, + "-1" + ], + [ + "SCALE", + 4, + "-1" + ], + [ + "ADD", + 0, + 1, + "-1" + ], + [ + "SWAP", + 0, + 1 + ], + [ + "SWAP", + 0, + 9 + ], + [ + "SWAP", + 1, + 8 + ], + [ + "SWAP", + 8, + 9 + ], + [ + "ADD", + 0, + 8, + "1" + ], + [ + "ADD", + 9, + 1, + "-1" + ], + [ + "LAMBDA", + 8, + -1 + ], + [ + "QUERY", + 8, + 9, + -1 + ], + [ + "LAMBDA", + 8, + 1 + ], + [ + "ADD", + 9, + 1, + "1" + ], + [ + "ADD", + 0, + 8, + "-1" + ], + [ + "IDLE", + 8, + 9, + [ + 1, + 2, + 3, + 4 + ] + ], + [ + "SCALE", + 1, + "-1" + ], + [ + "SWAP", + 1, + 11 + ], + [ + "SWAP", + 0, + 10 + ], + [ + "SWAP", + 10, + 11 + ], + [ + "ADD", + 1, + 10, + "1" + ], + [ + "ADD", + 11, + 0, + "-1" + ], + [ + "LAMBDA", + 10, + -1 + ], + [ + "QUERY", + 10, + 11, + -1 + ], + [ + "LAMBDA", + 10, + 1 + ], + [ + "ADD", + 11, + 0, + "1" + ], + [ + "ADD", + 1, + 10, + "-1" + ], + [ + "IDLE", + 10, + 11, + [ + 1, + 2 + ] + ], + [ + "SCALE", + 0, + "-1" + ], + [ + "LAMBDA", + 0, + -1 + ], + [ + "LOCAL", + 1, + 1, + 0 + ], + [ + "LAMBDA", + 0, + 1 + ], + [ + "SCALE", + 0, + "-1" + ], + [ + "LAMBDA", + 1, + -1 + ], + [ + "LOCAL", + 2, + 0, + 1 + ], + [ + "LAMBDA", + 1, + 1 + ], + [ + "ADD", + 1, + 10, + "1" + ], + [ + "SCALE", + 10, + "-1" + ], + [ + "ADD", + 10, + 1, + "1" + ], + [ + "SWAP", + 0, + 11 + ], + [ + "SCALE", + 11, + "-1" + ], + [ + "ADD", + 11, + 0, + "1" + ], + [ + "SCALE", + 1, + "-1" + ], + [ + "SWAP", + 0, + 13 + ], + [ + "SWAP", + 1, + 12 + ], + [ + "SWAP", + 12, + 13 + ], + [ + "ADD", + 0, + 12, + "1" + ], + [ + "ADD", + 13, + 1, + "-1" + ], + [ + "LAMBDA", + 12, + -1 + ], + [ + "QUERY", + 12, + 13, + -1 + ], + [ + "LAMBDA", + 12, + 1 + ], + [ + "ADD", + 13, + 1, + "1" + ], + [ + "ADD", + 0, + 12, + "-1" + ], + [ + "IDLE", + 12, + 13, + [ + 3, + 4 + ] + ], + [ + "SCALE", + 1, + "-1" + ], + [ + "LAMBDA", + 1, + -1 + ], + [ + "LOCAL", + 3, + 0, + 1 + ], + [ + "LAMBDA", + 1, + 1 + ], + [ + "SCALE", + 1, + "-1" + ], + [ + "LAMBDA", + 0, + -1 + ], + [ + "LOCAL", + 4, + 1, + 0 + ], + [ + "LAMBDA", + 0, + 1 + ], + [ + "ADD", + 0, + 12, + "1" + ], + [ + "SCALE", + 12, + "-1" + ], + [ + "ADD", + 12, + 0, + "1" + ], + [ + "SWAP", + 1, + 13 + ], + [ + "SCALE", + 13, + "-1" + ], + [ + "ADD", + 13, + 1, + "1" + ], + [ + "ADD", + 0, + 8, + "1" + ], + [ + "SCALE", + 8, + "-1" + ], + [ + "ADD", + 8, + 0, + "1" + ], + [ + "SWAP", + 1, + 9 + ], + [ + "SCALE", + 9, + "-1" + ], + [ + "ADD", + 9, + 1, + "1" + ], + [ + "ADD", + 0, + 1, + "-1" + ], + [ + "ADD", + 0, + 1, + "1" + ], + [ + "SCALE", + 1, + "-1" + ], + [ + "ADD", + 1, + 0, + "1" + ], + [ + "ADD", + 0, + 7, + "-1/2" + ], + [ + "ADD", + 7, + 6, + "29/2" + ], + [ + "ADD", + 1, + 6, + "-4" + ], + [ + "ADD", + 0, + 6, + "-37/4" + ], + [ + "SCALE", + 6, + "-1/2" + ], + [ + "SWAP", + 5, + 7 + ], + [ + "SWAP", + 4, + 6 + ], + [ + "SWAP", + 3, + 5 + ], + [ + "SWAP", + 2, + 4 + ], + [ + "SWAP", + 1, + 2 + ], + [ + "ADD", + 3, + 0, + "2" + ], + [ + "ADD", + 1, + 0, + "1/4" + ], + [ + "SCALE", + 0, + "1/4" + ], + [ + "SWAP", + 0, + 15 + ], + [ + "SWAP", + 1, + 14 + ], + [ + "SWAP", + 14, + 15 + ], + [ + "ADD", + 0, + 14, + "1" + ], + [ + "ADD", + 15, + 1, + "-1" + ], + [ + "LAMBDA", + 14, + -1 + ], + [ + "QUERY", + 14, + 15, + -1 + ], + [ + "LAMBDA", + 14, + 1 + ], + [ + "ADD", + 15, + 1, + "1" + ], + [ + "ADD", + 0, + 14, + "-1" + ], + [ + "IDLE", + 14, + 15, + [ + 5, + 6 + ] + ], + [ + "SCALE", + 1, + "-1" + ], + [ + "LAMBDA", + 1, + -1 + ], + [ + "LOCAL", + 5, + 0, + 1 + ], + [ + "LAMBDA", + 1, + 1 + ], + [ + "SCALE", + 1, + "-1" + ], + [ + "LAMBDA", + 0, + -1 + ], + [ + "LOCAL", + 6, + 1, + 0 + ], + [ + "LAMBDA", + 0, + 1 + ], + [ + "ADD", + 0, + 14, + "1" + ], + [ + "SCALE", + 14, + "-1" + ], + [ + "ADD", + 14, + 0, + "1" + ], + [ + "SWAP", + 1, + 15 + ], + [ + "SCALE", + 15, + "-1" + ], + [ + "ADD", + 15, + 1, + "1" + ], + [ + "ADD", + 0, + 1, + "-1" + ], + [ + "SCALE", + 1, + "-1" + ], + [ + "SWAP", + 1, + 17 + ], + [ + "SWAP", + 0, + 16 + ], + [ + "SWAP", + 16, + 17 + ], + [ + "ADD", + 1, + 16, + "1" + ], + [ + "ADD", + 17, + 0, + "-1" + ], + [ + "LAMBDA", + 16, + -1 + ], + [ + "QUERY", + 16, + 17, + -1 + ], + [ + "LAMBDA", + 16, + 1 + ], + [ + "ADD", + 17, + 0, + "1" + ], + [ + "ADD", + 1, + 16, + "-1" + ], + [ + "IDLE", + 16, + 17, + [ + 7, + 8, + 9 + ] + ], + [ + "SCALE", + 0, + "-1" + ], + [ + "LAMBDA", + 0, + -1 + ], + [ + "LOCAL", + 7, + 1, + 0 + ], + [ + "LAMBDA", + 0, + 1 + ], + [ + "SCALE", + 0, + "-1" + ], + [ + "SWAP", + 1, + 19 + ], + [ + "SWAP", + 0, + 18 + ], + [ + "SWAP", + 18, + 19 + ], + [ + "ADD", + 1, + 18, + "1" + ], + [ + "ADD", + 19, + 0, + "-1" + ], + [ + "LAMBDA", + 18, + -1 + ], + [ + "QUERY", + 18, + 19, + -1 + ], + [ + "LAMBDA", + 18, + 1 + ], + [ + "ADD", + 19, + 0, + "1" + ], + [ + "ADD", + 1, + 18, + "-1" + ], + [ + "IDLE", + 18, + 19, + [ + 8, + 9 + ] + ], + [ + "SCALE", + 0, + "-1" + ], + [ + "LAMBDA", + 0, + -1 + ], + [ + "LOCAL", + 8, + 1, + 0 + ], + [ + "LAMBDA", + 0, + 1 + ], + [ + "SCALE", + 0, + "-1" + ], + [ + "LAMBDA", + 1, + -1 + ], + [ + "LOCAL", + 9, + 0, + 1 + ], + [ + "LAMBDA", + 1, + 1 + ], + [ + "ADD", + 1, + 18, + "1" + ], + [ + "SCALE", + 18, + "-1" + ], + [ + "ADD", + 18, + 1, + "1" + ], + [ + "SWAP", + 0, + 19 + ], + [ + "SCALE", + 19, + "-1" + ], + [ + "ADD", + 19, + 0, + "1" + ], + [ + "ADD", + 1, + 16, + "1" + ], + [ + "SCALE", + 16, + "-1" + ], + [ + "ADD", + 16, + 1, + "1" + ], + [ + "SWAP", + 0, + 17 + ], + [ + "SCALE", + 17, + "-1" + ], + [ + "ADD", + 17, + 0, + "1" + ], + [ + "SCALE", + 1, + "-1" + ], + [ + "ADD", + 1, + 0, + "1" + ], + [ + "IDLE", + 2, + 3, + [ + 5, + 6, + 7, + 8, + 9 + ] + ], + [ + "SWAP", + 6, + 7 + ], + [ + "SWAP", + 5, + 6 + ], + [ + "SWAP", + 4, + 7 + ], + [ + "ADD", + 2, + 3, + "-1" + ], + [ + "ADD", + 1, + 3, + "-45/64" + ], + [ + "ADD", + 0, + 3, + "-37/64" + ], + [ + "SCALE", + 3, + "-1/4" + ], + [ + "SWAP", + 3, + 6 + ], + [ + "SWAP", + 2, + 7 + ], + [ + "ADD", + 0, + 1, + "-1" + ], + [ + "SCALE", + 1, + "-8" + ], + [ + "SWAP", + 1, + 7 + ], + [ + "ADD", + 7, + 0, + "-37" + ], + [ + "ADD", + 6, + 0, + "2" + ], + [ + "ADD", + 1, + 0, + "8" + ], + [ + "SCALE", + 0, + "4" + ], + [ + "ADD", + 5, + 7, + "1/4" + ], + [ + "ADD", + 1, + 7, + "-1/2" + ], + [ + "ADD", + 0, + 7, + "-1/4" + ], + [ + "SCALE", + 7, + "1/4" + ], + [ + "SWAP", + 6, + 7 + ], + [ + "ADD", + 0, + 5, + "1" + ], + [ + "SWAP", + 5, + 6 + ], + [ + "SWAP", + 4, + 5 + ], + [ + "SWAP", + 3, + 4 + ], + [ + "SWAP", + 2, + 3 + ], + [ + "SWAP", + 1, + 2 + ], + [ + "SWAP", + 0, + 1 + ], + [ + "LAMBDA", + 0, + -1 + ], + [ + "QUERY", + 0, + 1, + -1 + ], + [ + "LAMBDA", + 0, + 1 + ], + [ + "ADD", + 0, + 1, + "-1" + ], + [ + "ADD", + 2, + 6, + "2" + ], + [ + "ADD", + 0, + 6, + "-1" + ], + [ + "SCALE", + 6, + "4" + ], + [ + "SWAP", + 6, + 7 + ], + [ + "SWAP", + 4, + 5 + ], + [ + "SWAP", + 3, + 5 + ], + [ + "ADD", + 7, + 2, + "-2" + ], + [ + "ADD", + 1, + 2, + "-1/2" + ], + [ + "ADD", + 0, + 2, + "1/2" + ], + [ + "SCALE", + 2, + "1/2" + ], + [ + "SWAP", + 2, + 5 + ], + [ + "ADD", + 7, + 1, + "-4" + ], + [ + "ADD", + 5, + 1, + "1" + ], + [ + "ADD", + 0, + 1, + "1" + ], + [ + "SCALE", + 1, + "-2" + ], + [ + "ADD", + 7, + 0, + "4" + ], + [ + "ADD", + 5, + 0, + "-1" + ], + [ + "ADD", + 1, + 0, + "2" + ], + [ + "ADD", + 1, + 6, + "-2" + ], + [ + "ADD", + 1, + 5, + "1" + ], + [ + "ADD", + 2, + 4, + "-1" + ], + [ + "ADD", + 0, + 4, + "1/2" + ], + [ + "SCALE", + 4, + "1/2" + ], + [ + "ADD", + 1, + 3, + "1" + ], + [ + "SWAP", + 3, + 4 + ], + [ + "ADD", + 1, + 2, + "-1" + ], + [ + "SWAP", + 2, + 3 + ], + [ + "SWAP", + 0, + 2 + ], + [ + "LAMBDA", + 0, + -1 + ], + [ + "QUERY", + 0, + 1, + -1 + ], + [ + "LAMBDA", + 0, + 1 + ], + [ + "ADD", + 0, + 1, + "-1" + ], + [ + "ADD", + 1, + 6, + "2" + ], + [ + "ADD", + 1, + 5, + "-1" + ], + [ + "ADD", + 1, + 4, + "-1" + ], + [ + "ADD", + 2, + 3, + "1/2" + ], + [ + "ADD", + 1, + 3, + "1" + ], + [ + "ADD", + 0, + 3, + "1/2" + ], + [ + "SCALE", + 3, + "-1" + ], + [ + "SWAP", + 3, + 4 + ], + [ + "ADD", + 4, + 2, + "2" + ], + [ + "ADD", + 0, + 2, + "-1" + ], + [ + "SCALE", + 2, + "2" + ], + [ + "ADD", + 4, + 0, + "2" + ], + [ + "ADD", + 2, + 0, + "2" + ], + [ + "SCALE", + 0, + "-1" + ], + [ + "ADD", + 5, + 7, + "1/2" + ], + [ + "ADD", + 4, + 7, + "3/2" + ], + [ + "ADD", + 3, + 7, + "-1/2" + ], + [ + "ADD", + 2, + 7, + "3/2" + ], + [ + "ADD", + 1, + 7, + "-1/2" + ], + [ + "ADD", + 0, + 7, + "-1" + ], + [ + "SCALE", + 7, + "1/2" + ], + [ + "ADD", + 0, + 6, + "4" + ], + [ + "SWAP", + 6, + 7 + ], + [ + "ADD", + 0, + 5, + "-2" + ], + [ + "SWAP", + 5, + 6 + ], + [ + "ADD", + 0, + 4, + "-2" + ], + [ + "SWAP", + 4, + 5 + ], + [ + "ADD", + 0, + 3, + "-2" + ], + [ + "SWAP", + 3, + 4 + ], + [ + "ADD", + 0, + 2, + "2" + ], + [ + "SWAP", + 2, + 3 + ], + [ + "ADD", + 0, + 1, + "-2" + ], + [ + "SWAP", + 1, + 2 + ], + [ + "SWAP", + 0, + 1 + ], + [ + "LAMBDA", + 0, + -1 + ], + [ + "QUERY", + 0, + 1, + -1 + ], + [ + "LAMBDA", + 0, + 1 + ], + [ + "ADD", + 0, + 1, + "-1" + ], + [ + "ADD", + 1, + 7, + "-4" + ], + [ + "ADD", + 5, + 6, + "-3" + ], + [ + "ADD", + 4, + 6, + "1" + ], + [ + "ADD", + 3, + 6, + "-3" + ], + [ + "ADD", + 2, + 6, + "1" + ], + [ + "ADD", + 0, + 6, + "-1" + ], + [ + "SCALE", + 6, + "2" + ], + [ + "SWAP", + 6, + 7 + ], + [ + "ADD", + 1, + 5, + "2" + ], + [ + "ADD", + 7, + 4, + "-2" + ], + [ + "ADD", + 5, + 4, + "3" + ], + [ + "ADD", + 3, + 4, + "3" + ], + [ + "ADD", + 2, + 4, + "-1" + ], + [ + "ADD", + 1, + 4, + "8" + ], + [ + "ADD", + 0, + 4, + "1" + ], + [ + "SWAP", + 4, + 5 + ], + [ + "ADD", + 1, + 3, + "-2" + ], + [ + "ADD", + 7, + 2, + "-2" + ], + [ + "ADD", + 5, + 2, + "1" + ], + [ + "ADD", + 4, + 2, + "3" + ], + [ + "ADD", + 3, + 2, + "3" + ], + [ + "ADD", + 0, + 2, + "1" + ], + [ + "SCALE", + 2, + "-1" + ], + [ + "SWAP", + 2, + 3 + ], + [ + "ADD", + 7, + 1, + "-1" + ], + [ + "ADD", + 5, + 1, + "1/2" + ], + [ + "ADD", + 4, + 1, + "3/2" + ], + [ + "ADD", + 3, + 1, + "-1/2" + ], + [ + "ADD", + 2, + 1, + "3/2" + ], + [ + "ADD", + 0, + 1, + "1/2" + ], + [ + "SCALE", + 1, + "-1/2" + ], + [ + "ADD", + 7, + 0, + "2" + ], + [ + "ADD", + 5, + 0, + "-1" + ], + [ + "ADD", + 4, + 0, + "-3" + ], + [ + "ADD", + 3, + 0, + "1" + ], + [ + "ADD", + 2, + 0, + "-3" + ], + [ + "ADD", + 1, + 0, + "1" + ], + [ + "SCALE", + 0, + "2" + ], + [ + "ADD", + 0, + 6, + "4" + ], + [ + "ADD", + 0, + 5, + "-2" + ], + [ + "ADD", + 3, + 4, + "1/2" + ], + [ + "ADD", + 2, + 4, + "-1" + ], + [ + "ADD", + 0, + 4, + "1/2" + ], + [ + "SCALE", + 4, + "-1/2" + ], + [ + "ADD", + 0, + 3, + "-1" + ], + [ + "SWAP", + 3, + 4 + ], + [ + "ADD", + 0, + 2, + "2" + ], + [ + "SWAP", + 2, + 3 + ], + [ + "ADD", + 0, + 1, + "-2" + ], + [ + "SWAP", + 1, + 2 + ], + [ + "SWAP", + 0, + 1 + ], + [ + "LAMBDA", + 0, + -1 + ], + [ + "QUERY", + 0, + 1, + -1 + ], + [ + "LAMBDA", + 0, + 1 + ], + [ + "ADD", + 0, + 1, + "-1" + ], + [ + "ADD", + 1, + 6, + "-4" + ], + [ + "ADD", + 1, + 5, + "2" + ], + [ + "ADD", + 3, + 4, + "2" + ], + [ + "ADD", + 1, + 4, + "4" + ], + [ + "ADD", + 0, + 4, + "1" + ], + [ + "SCALE", + 4, + "2" + ], + [ + "ADD", + 4, + 3, + "-1" + ], + [ + "ADD", + 1, + 3, + "-3/2" + ], + [ + "ADD", + 0, + 3, + "-1/2" + ], + [ + "SCALE", + 3, + "1/2" + ], + [ + "ADD", + 1, + 2, + "2" + ], + [ + "ADD", + 4, + 1, + "2" + ], + [ + "ADD", + 3, + 1, + "-1" + ], + [ + "ADD", + 0, + 1, + "1" + ], + [ + "SCALE", + 1, + "2" + ], + [ + "SWAP", + 1, + 2 + ], + [ + "ADD", + 4, + 0, + "-2" + ], + [ + "ADD", + 3, + 0, + "1" + ], + [ + "ADD", + 2, + 0, + "-2" + ], + [ + "ADD", + 2, + 4, + "-2" + ], + [ + "ADD", + 0, + 4, + "1" + ], + [ + "SWAP", + 3, + 4 + ], + [ + "SWAP", + 1, + 3 + ], + [ + "SWAP", + 0, + 1 + ], + [ + "SWAP", + 0, + 21 + ], + [ + "SWAP", + 1, + 20 + ], + [ + "SWAP", + 20, + 21 + ], + [ + "ADD", + 0, + 20, + "1" + ], + [ + "ADD", + 21, + 1, + "-1" + ], + [ + "LAMBDA", + 20, + -1 + ], + [ + "QUERY", + 20, + 21, + -1 + ], + [ + "LAMBDA", + 20, + 1 + ], + [ + "SWAP", + 4, + 21 + ], + [ + "ADD", + 4, + 1, + "1" + ], + [ + "ADD", + 4, + 20, + "-1" + ], + [ + "ADD", + 0, + 4, + "2" + ], + [ + "ADD", + 2, + 4, + "-2" + ], + [ + "ADD", + 20, + 4, + "2" + ], + [ + "ADD", + 20, + 34, + "-2" + ], + [ + "ADD", + 2, + 34, + "2" + ], + [ + "ADD", + 0, + 34, + "-2" + ], + [ + "ADD", + 34, + 20, + "1" + ], + [ + "ADD", + 34, + 1, + "-1" + ], + [ + "SWAP", + 34, + 21 + ], + [ + "ADD", + 21, + 1, + "1" + ], + [ + "ADD", + 0, + 20, + "-1" + ], + [ + "IDLE", + 20, + 21, + [ + 10, + 11, + 12, + 13 + ] + ], + [ + "SCALE", + 1, + "-1" + ], + [ + "SWAP", + 1, + 23 + ], + [ + "SWAP", + 0, + 22 + ], + [ + "SWAP", + 22, + 23 + ], + [ + "ADD", + 1, + 22, + "1" + ], + [ + "ADD", + 23, + 0, + "-1" + ], + [ + "LAMBDA", + 22, + -1 + ], + [ + "QUERY", + 22, + 23, + -1 + ], + [ + "LAMBDA", + 22, + 1 + ], + [ + "ADD", + 23, + 0, + "1" + ], + [ + "ADD", + 1, + 22, + "-1" + ], + [ + "IDLE", + 22, + 23, + [ + 10, + 11 + ] + ], + [ + "SCALE", + 0, + "-1" + ], + [ + "LAMBDA", + 0, + -1 + ], + [ + "LOCAL", + 10, + 1, + 0 + ], + [ + "LAMBDA", + 0, + 1 + ], + [ + "SCALE", + 0, + "-1" + ], + [ + "LAMBDA", + 1, + -1 + ], + [ + "LOCAL", + 11, + 0, + 1 + ], + [ + "LAMBDA", + 1, + 1 + ], + [ + "ADD", + 1, + 22, + "1" + ], + [ + "SCALE", + 22, + "-1" + ], + [ + "ADD", + 22, + 1, + "1" + ], + [ + "SWAP", + 0, + 23 + ], + [ + "SCALE", + 23, + "-1" + ], + [ + "ADD", + 23, + 0, + "1" + ], + [ + "SCALE", + 1, + "-1" + ], + [ + "SWAP", + 0, + 25 + ], + [ + "SWAP", + 1, + 24 + ], + [ + "SWAP", + 24, + 25 + ], + [ + "ADD", + 0, + 24, + "1" + ], + [ + "ADD", + 25, + 1, + "-1" + ], + [ + "LAMBDA", + 24, + -1 + ], + [ + "QUERY", + 24, + 25, + -1 + ], + [ + "LAMBDA", + 24, + 1 + ], + [ + "ADD", + 25, + 1, + "1" + ], + [ + "ADD", + 0, + 24, + "-1" + ], + [ + "IDLE", + 24, + 25, + [ + 12, + 13 + ] + ], + [ + "SCALE", + 1, + "-1" + ], + [ + "LAMBDA", + 1, + -1 + ], + [ + "LOCAL", + 12, + 0, + 1 + ], + [ + "LAMBDA", + 1, + 1 + ], + [ + "SCALE", + 1, + "-1" + ], + [ + "LAMBDA", + 0, + -1 + ], + [ + "LOCAL", + 13, + 1, + 0 + ], + [ + "LAMBDA", + 0, + 1 + ], + [ + "ADD", + 0, + 24, + "1" + ], + [ + "SCALE", + 24, + "-1" + ], + [ + "ADD", + 24, + 0, + "1" + ], + [ + "SWAP", + 1, + 25 + ], + [ + "SCALE", + 25, + "-1" + ], + [ + "ADD", + 25, + 1, + "1" + ], + [ + "ADD", + 0, + 20, + "1" + ], + [ + "SCALE", + 20, + "-1" + ], + [ + "ADD", + 20, + 0, + "1" + ], + [ + "SWAP", + 1, + 21 + ], + [ + "SCALE", + 21, + "-1" + ], + [ + "ADD", + 21, + 1, + "1" + ], + [ + "ADD", + 0, + 1, + "-1" + ], + [ + "IDLE_ONE", + 2, + [ + 10, + 11, + 12, + 13 + ] + ], + [ + "SWAP", + 3, + 34 + ], + [ + "ADD", + 1, + 2, + "1/2" + ], + [ + "ADD", + 0, + 2, + "1/2" + ], + [ + "SCALE", + 2, + "-1/2" + ], + [ + "SWAP", + 2, + 34 + ], + [ + "ADD", + 34, + 1, + "1" + ], + [ + "ADD", + 0, + 1, + "-1" + ], + [ + "SCALE", + 1, + "2" + ], + [ + "SWAP", + 1, + 2 + ], + [ + "ADD", + 34, + 0, + "1" + ], + [ + "ADD", + 2, + 0, + "2" + ], + [ + "SCALE", + 0, + "-1" + ], + [ + "ADD", + 0, + 2, + "1" + ], + [ + "SWAP", + 1, + 2 + ], + [ + "SWAP", + 0, + 1 + ], + [ + "SWAP", + 0, + 27 + ], + [ + "SWAP", + 1, + 26 + ], + [ + "SWAP", + 26, + 27 + ], + [ + "ADD", + 0, + 26, + "1" + ], + [ + "ADD", + 27, + 1, + "-1" + ], + [ + "LAMBDA", + 26, + -1 + ], + [ + "QUERY", + 26, + 27, + -1 + ], + [ + "LAMBDA", + 26, + 1 + ], + [ + "ADD", + 27, + 1, + "1" + ], + [ + "ADD", + 0, + 26, + "-1" + ], + [ + "IDLE", + 26, + 27, + [ + 14, + 15, + 16, + 17, + 18 + ] + ], + [ + "SCALE", + 1, + "-1" + ], + [ + "SWAP", + 1, + 29 + ], + [ + "SWAP", + 0, + 28 + ], + [ + "SWAP", + 28, + 29 + ], + [ + "ADD", + 1, + 28, + "1" + ], + [ + "ADD", + 29, + 0, + "-1" + ], + [ + "LAMBDA", + 28, + -1 + ], + [ + "QUERY", + 28, + 29, + -1 + ], + [ + "LAMBDA", + 28, + 1 + ], + [ + "ADD", + 29, + 0, + "1" + ], + [ + "ADD", + 1, + 28, + "-1" + ], + [ + "IDLE", + 28, + 29, + [ + 14, + 15 + ] + ], + [ + "SCALE", + 0, + "-1" + ], + [ + "LAMBDA", + 0, + -1 + ], + [ + "LOCAL", + 14, + 1, + 0 + ], + [ + "LAMBDA", + 0, + 1 + ], + [ + "SCALE", + 0, + "-1" + ], + [ + "LAMBDA", + 1, + -1 + ], + [ + "LOCAL", + 15, + 0, + 1 + ], + [ + "LAMBDA", + 1, + 1 + ], + [ + "ADD", + 1, + 28, + "1" + ], + [ + "SCALE", + 28, + "-1" + ], + [ + "ADD", + 28, + 1, + "1" + ], + [ + "SWAP", + 0, + 29 + ], + [ + "SCALE", + 29, + "-1" + ], + [ + "ADD", + 29, + 0, + "1" + ], + [ + "SCALE", + 1, + "-1" + ], + [ + "SWAP", + 0, + 31 + ], + [ + "SWAP", + 1, + 30 + ], + [ + "SWAP", + 30, + 31 + ], + [ + "ADD", + 0, + 30, + "1" + ], + [ + "ADD", + 31, + 1, + "-1" + ], + [ + "LAMBDA", + 30, + -1 + ], + [ + "QUERY", + 30, + 31, + -1 + ], + [ + "LAMBDA", + 30, + 1 + ], + [ + "ADD", + 31, + 1, + "1" + ], + [ + "ADD", + 0, + 30, + "-1" + ], + [ + "IDLE", + 30, + 31, + [ + 16, + 17, + 18 + ] + ], + [ + "SCALE", + 1, + "-1" + ], + [ + "LAMBDA", + 1, + -1 + ], + [ + "LOCAL", + 16, + 0, + 1 + ], + [ + "LAMBDA", + 1, + 1 + ], + [ + "SCALE", + 1, + "-1" + ], + [ + "SWAP", + 0, + 33 + ], + [ + "SWAP", + 1, + 32 + ], + [ + "SWAP", + 32, + 33 + ], + [ + "ADD", + 0, + 32, + "1" + ], + [ + "ADD", + 33, + 1, + "-1" + ], + [ + "LAMBDA", + 32, + -1 + ], + [ + "QUERY", + 32, + 33, + -1 + ], + [ + "LAMBDA", + 32, + 1 + ], + [ + "ADD", + 33, + 1, + "1" + ], + [ + "ADD", + 0, + 32, + "-1" + ], + [ + "IDLE", + 32, + 33, + [ + 17, + 18 + ] + ], + [ + "SCALE", + 1, + "-1" + ], + [ + "LAMBDA", + 1, + -1 + ], + [ + "LOCAL", + 17, + 0, + 1 + ], + [ + "LAMBDA", + 1, + 1 + ], + [ + "SCALE", + 1, + "-1" + ], + [ + "LAMBDA", + 0, + -1 + ], + [ + "LOCAL", + 18, + 1, + 0 + ], + [ + "LAMBDA", + 0, + 1 + ], + [ + "ADD", + 0, + 32, + "1" + ], + [ + "SCALE", + 32, + "-1" + ], + [ + "ADD", + 32, + 0, + "1" + ], + [ + "SWAP", + 1, + 33 + ], + [ + "SCALE", + 33, + "-1" + ], + [ + "ADD", + 33, + 1, + "1" + ], + [ + "ADD", + 0, + 30, + "1" + ], + [ + "SCALE", + 30, + "-1" + ], + [ + "ADD", + 30, + 0, + "1" + ], + [ + "SWAP", + 1, + 31 + ], + [ + "SCALE", + 31, + "-1" + ], + [ + "ADD", + 31, + 1, + "1" + ], + [ + "ADD", + 0, + 26, + "1" + ], + [ + "SCALE", + 26, + "-1" + ], + [ + "ADD", + 26, + 0, + "1" + ], + [ + "SWAP", + 1, + 27 + ], + [ + "SCALE", + 27, + "-1" + ], + [ + "ADD", + 27, + 1, + "1" + ], + [ + "ADD", + 0, + 1, + "-1" + ], + [ + "ADD", + 0, + 1, + "-1" + ], + [ + "SWAP", + 1, + 2 + ], + [ + "ADD", + 2, + 0, + "1" + ], + [ + "SCALE", + 0, + "-1" + ], + [ + "LAMBDA", + 0, + -1 + ], + [ + "LAMBDA", + 1, + -1 + ], + [ + "LAMBDA", + 2, + -1 + ], + [ + "LAMBDA", + 3, + -1 + ], + [ + "LAMBDA", + 34, + -1 + ], + [ + "LAMBDA", + 5, + -1 + ], + [ + "LAMBDA", + 6, + -1 + ], + [ + "LAMBDA", + 7, + -1 + ], + [ + "LAMBDA", + 8, + -1 + ], + [ + "LAMBDA", + 9, + -1 + ], + [ + "LAMBDA", + 10, + -1 + ], + [ + "LAMBDA", + 11, + -1 + ], + [ + "LAMBDA", + 12, + -1 + ], + [ + "LAMBDA", + 13, + -1 + ], + [ + "LAMBDA", + 14, + -1 + ], + [ + "LAMBDA", + 15, + -1 + ], + [ + "LAMBDA", + 16, + -1 + ], + [ + "LAMBDA", + 17, + -1 + ], + [ + "LAMBDA", + 18, + -1 + ], + [ + "LAMBDA", + 19, + -1 + ], + [ + "LAMBDA", + 20, + -1 + ], + [ + "LAMBDA", + 21, + -1 + ], + [ + "LAMBDA", + 22, + -1 + ], + [ + "LAMBDA", + 23, + -1 + ], + [ + "LAMBDA", + 24, + -1 + ], + [ + "LAMBDA", + 25, + -1 + ], + [ + "LAMBDA", + 26, + -1 + ], + [ + "LAMBDA", + 27, + -1 + ], + [ + "LAMBDA", + 28, + -1 + ], + [ + "LAMBDA", + 29, + -1 + ], + [ + "LAMBDA", + 30, + -1 + ], + [ + "LAMBDA", + 31, + -1 + ], + [ + "LAMBDA", + 32, + -1 + ], + [ + "LAMBDA", + 33, + -1 + ], + [ + "LAMBDA", + 34, + 1 + ], + [ + "LAMBDA", + 20, + 1 + ], + [ + "LAMBDA", + 21, + 1 + ], + [ + "SCALE", + 34, + "-1" + ], + [ + "ADD", + 21, + 34, + "1" + ], + [ + "ADD", + 34, + 20, + "1" + ], + [ + "LAMBDA", + 4, + -1 + ], + [ + "LAMBDA", + 20, + -1 + ], + [ + "LAMBDA", + 21, + -1 + ] + ], + "diagonal": [ + [ + -1, + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + [ + -1, + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + [ + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + -1, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + -1, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + -1, + 0, + 1, + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + -1, + 0, + 1, + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + -1, + 0, + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + -1, + 0, + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + -1, + 0, + 0, + 0, + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + -1, + 0, + 0, + 0, + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + -1, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + -1, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 0 + ], + [ + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 0 + ], + [ + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 0, + 0, + 0, + 0, + 0 + ], + [ + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 0, + 0, + 0, + 0, + 0 + ], + [ + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 1 + ], + [ + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 1 + ], + [ + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 0, + 0, + 0 + ], + [ + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 0, + 0, + 0 + ], + [ + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1 + ], + [ + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1 + ], + [ + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1 + ], + [ + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1 + ], + [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 0 + ] + ], + "nodes": [ + { + "roles": [ + 8, + 9 + ], + "stages": [ + 1, + 2, + 3, + 4 + ] + }, + { + "roles": [ + 10, + 11 + ], + "stages": [ + 1, + 2 + ] + }, + { + "roles": [ + 12, + 13 + ], + "stages": [ + 3, + 4 + ] + }, + { + "roles": [ + 14, + 15 + ], + "stages": [ + 5, + 6 + ] + }, + { + "roles": [ + 16, + 17 + ], + "stages": [ + 7, + 8, + 9 + ] + }, + { + "roles": [ + 18, + 19 + ], + "stages": [ + 8, + 9 + ] + }, + { + "roles": [ + 20, + 21 + ], + "stages": [ + 10, + 11, + 12, + 13 + ] + }, + { + "roles": [ + 22, + 23 + ], + "stages": [ + 10, + 11 + ] + }, + { + "roles": [ + 24, + 25 + ], + "stages": [ + 12, + 13 + ] + }, + { + "roles": [ + 26, + 27 + ], + "stages": [ + 14, + 15, + 16, + 17, + 18 + ] + }, + { + "roles": [ + 28, + 29 + ], + "stages": [ + 14, + 15 + ] + }, + { + "roles": [ + 30, + 31 + ], + "stages": [ + 16, + 17, + 18 + ] + }, + { + "roles": [ + 32, + 33 + ], + "stages": [ + 17, + 18 + ] + } + ] +} diff --git a/research/p104-cut353-independent-audit/inputs/PROOF.md b/research/p104-cut353-independent-audit/inputs/PROOF.md new file mode 100644 index 0000000000..08f1031ea9 --- /dev/null +++ b/research/p104-cut353-independent-audit/inputs/PROOF.md @@ -0,0 +1,238 @@ +# A common-idle root with a new independent continuation + +This is a conditional construction at the exact native boundary of PR6702. +The proof uses no approximate border, limiting parameter or unpriced +Gaussian repair. New notation below describes the actual emitted word. + +## 1. Normalize the actual central operator + +Let `q=Q^-1` be the source central Gaussian. The source physical checker +verifies `q^2=X`, where X is an ordinary translation with phase+1, and +`X^2=I`. Set + +```text +lambda = (1+i)I/2 + (1-i)X/2, +lambda^-1 = (1-i)I/2 + (1+i)X/2, +S = lambda*q. +``` + +Then `lambda^2=X`, `S^2=I`, and `lambda^-1*S=q`. All commute with the fresh +stage operators. A native full supplier `D U(q)` becomes `D U(S)` by +ordinary lambda conjugation on its query destination; an ordinary ADD +changes this to `D U(S-1)`. A thin query receives the same conjugation +and retains its paidH1 charge. Each emitted LAMBDA uses the retained +four-operation in-place two-address-pair map. It adds no productive input. + +For each positive column multiplicity f, these formulas use the actual +global `q_f` and its square. The coefficients of lambda remain outside the +tensor power. In general this S is not the tensor power of a one-column S. + +## 2. The exact root and its common idle subspace + +`ROOT.json` lists the nine rational rank-one square-zero matrices R_i, +ordinary native bases and five commuting coordinate projectors P_i. +All coefficients are dyadic. The full sites are0,1,2,7,8. Direct exact +multiplication gives + +```text +(I-2R_8) ... (I-2R_0) = -I_8. +``` + +At every full site, `P_i R_i=R_i P_i=R_i`, and P_i commutes with its +complete query prefix. Consequently each independent stage factor can +move past its query prefix. The plus/minus central characters give +`S*diag(stage products)`. The checker also multiplies the 64 combinations +of the two central characters and five stage nodes{1,2}. Degree at most +one in each independent stage variable makes this an exact coefficient +check, not a numerical sample. + +The stage supports, in the eight input/output coordinates, are + +| Site | Support | Rank | +|---|---|---:| +|0|0,1|2| +|1|0,1,6,7|4| +|2|0,1,6,7|4| +|7|0,2,4|3| +|8|0,2|2| + +The eight Gaussian output masks are + +```text +ABCDE, ABC, DE, empty, D, empty, BC, BC. +``` + +For the actual single ordinary basis C used across sites 1 and 2, + +```text +C^-1 R_1 C = E01, C^-1 R_2 C = -E10, +C^-1 P_1 C = C^-1 P_2 C = diag(1,1,1,1,0,0,0,0). +``` + +Both queries and both child suppliers touch only the first two active +coordinates and their separately named binary auxiliaries. Coordinates2 +and 3 are neither read nor written by these operations. Each therefore +needs exactly `D_B D_C` on its own unchanged payload. The B and C axes +are disjoint fresh blocks; their two positive transforms combine into +one rank-`8(B+C)` job on each of these two coordinates. The emitted IDLE +opcode pays **two** such jobs. It does not treat two independent arrays +as one call or copy an input to gain another target. + +The remaining rank-three site 7 pays its single wholeD idle. All native +two-field work and 17 thin queries remain paid. + +## 3. Binary suppliers and the complete source interface + +Use the retained binary query extension on child sizes `(4,2,3,4,5)`. +Its13 internal node sizes are `{2:8,3:2,4:2,5:1}`. Each internal node has +its own two arbitrary productive auxiliary inputs, two charged whole +idles and one paid thin query. The resulting unretired caller has 34 +independent main inputs. None is assumed zero or supplied by copying +another productive input. + +The18 LOCAL invocations are the exact PR6702 native word, in stage order +1 through 18. Every invocation gets all 563 independent native helpers, +the same771 public native labels and 29 owned labels. The47 native owned +lifetimes, peak14 and 18,577-event program are unchanged. Lambda and basis +maps occur only on main fields outside the source invocation. Thus +arbitrary-input native correctness applies to their current contents. + +## 4. Source-specific two-sided cut + +Let P be the literal unretired prefix through zero-based event 353, after +the lambda return following its first D-child thin query. This D child +contains fresh stages 10 through 13. Main fields 4,20,21 have the same +complete `S D` target after ordinary output normalization. Set + +```text +a = e1^T - e20^T + e21^T, +b = -2e0 + 2e2 - 2e20 - e21, +c = e20^T - e4^T, +d = -e4 - e21. +``` + +Exact full-ring checks give + +```text +ab = cd = 1, aP = S c, Pd = S b. +``` + +These identities retain all 18 distinct stage variables and `Q^4=I`. +They do not specialize the central square to identity. All four vectors +are ordinary rational dyadics; no unavailable S or stage transform is +hidden in a basis coefficient. + +The literal ordinary words G and J in WITNESS.json satisfy + +```text +e4^T G = c, Gd=e4, +e4^T J = a, Jb=e4. +``` + +G has three gates and J six. Applying `G^-1` at input and J at the cut +makes the pivot row and column of `J P G^-1` exactly `S e4`. It is +therefore `S ⊕ K`, with no coupling to any other independent input. +G mixes only fields 4,20,21 with equal complete normalized targets, so +G commutes with the complete endpoint. The matching suffix has pivot +block D and no coupling to the other fields. + +Return the completed S pivot. Give that suffix a **new independent input** +in field34, and rename pivot4 to 34 in `J^-1` and all later gates, including +the final G. No gate touches field34 before this handoff. The two inputs +then receive S and D separately in place of one S D. Restore lambda on +the original group. The original pivot receives q and the new field +receives the plain rank 32 Gaussian, with no earned central factor. + +The final caller has 35 independent main inputs and 586 instructions. +Forward and reverse-row engines check all 1,225 coefficient positions; +deleting the input basis, handoff or return, or giving the fresh field +an extra central target, is rejected. Every paid job before and after +retirement has the same stage set, sign and chronological order. + +## 5. Full invoice and strict improvement + +Count every LOCAL helper target/paid call18 times, every thin query104 +times, both fields of every paired idle, the individualD idle, and all 35 +main outputs. The independent formula equals the literal event/endpoint +invoice. The totals are13,774 productive fields,66,956 paid jobs, +target rank mass179,048 and paid rank mass178,288. Their surplus is 760. + +For `H_r=r^t`, `0 0. +``` + +This is a second-retirement-equivalent **invoice** improvement. The emitted +new word contains one explicit fresh-input retirement, `H33 -> H1+H32`. +The shared-idle/root change supplies the other part of the comparison. +Fusion alone only matches the preceding best signed tariff after its own +child-size optimization; the new fresh-input proof is necessary. + +A negative derivative bound through the retained BIT cap makes the raw +crossing unique. This fixed invoice cannot reach0.0033042804236. No global +caller or native-word optimality is claimed. + +At canonical main `7c49fe32c55de02c2c873655c804b16e4c3fef0a`, the selected +result is PR6030, conditional κ=0.003125804. This contribution compares with +the stronger pending P104 source PR6702. It does not claim to dominate +different, unadmitted research-family proposals. + +## Reproduce + +Python 3.12 and the standard library; no network, solver, NumPy, SymPy, +Lean or Docker is required by the registered replay. + +```sh +python3.12 -I -B research/p104-common-idle-double-retirement/verify.py +python3.12 -I -O -B research/p104-common-idle-double-retirement/verify.py +``` + +The final marker is `PASS_CONDITIONAL_KAPPA_00330420_COMMON_IDLE_RETIREMENT`. +Direct replay works in a Git-free package export. `--write-result` explicitly +regenerates only the new RESULT.json; ordinary replay is read-only. The +retained source files and their expected receipts are never regenerated or +weakened. [VALIDATION.md](VALIDATION.md) records the actual executions. + +## Scope and predecessor credit + +The inherited assumptions are `native_all_columns`, `owned_erasure`, +`compiler`, `precision_tape` and `analytic_recovery`. Finite native tests +do not discharge these quantified hypotheses. The huge winning uniform +word, rounded multiplier and full multiplication theorem are not materialized +or formally verified. A passing replay is author-side evidence, not admission. + +The full native word is inherited unchanged from PR6702 at +`edd6a37a9ff87b254fb7466184348d1432d0c8c0`, by DreamingOfClouds with Claude +assistance. The binary query supplier is from PR6348, and common-projector +roots/normalization are from PR6398, by Ali Romman building on Cinna Davis's +query/controller lineage. The two-sided retirement method is inherited from +PR6545 and the PR5599 dual-pair lineage; PR6551 supplies the preceding +rebalanced tree comparison. All native/helper, Clifford, compiler, BIT, +precision and analytic predecessors retain their credit and notices. + +The new contribution is the rank-(2,4,4,3,2) source-compatible root, +actual common-idle implementation, its new fresh-input cut and complete +source-bound price. It does not claim invention of binary refinement, +central normalization, dual-pair retirement or productive recursion. +Prepared for **thu-nmrc with substantial OpenAI Codex assistance**, including +parallel mathematical and verification agents. All validation here is +author-side; no external independent reviewer is implied. Apache-2.0. + +`SOURCE6702.json` authenticates the 17 unchanged top-level predecessor files +by SHA256 and Git blob. Its nested runtime archives retain their original +manifests. The source's SOURCES.json contains a stale outer archive digest; +its actual source.tar and executable RETAINED.json agree. This package pins +the actual bytes and preserves that historical metadata without editing it. + +## Open next questions + +- Independently audit the actual common-idle bank and the new two-sided + fresh-input cut, then replay this package. This is the gate to scientific + adoption; archive merging or CI success alone is insufficient. +- Can another exact caller or source-specific split beat the fixed-invoice + ceiling? Start with a complete signed budget and independent-input + identity. More digits of this crossing do not supply a new construction. +- Can the remaining quantified framework assumptions be discharged for the + consumed source and full recursive interface? Finite coefficient and + phase checks do not settle those all-size obligations. diff --git a/research/p104-cut353-independent-audit/inputs/WITNESS.json b/research/p104-cut353-independent-audit/inputs/WITNESS.json new file mode 100644 index 0000000000..01c87980b1 --- /dev/null +++ b/research/p104-cut353-independent-audit/inputs/WITNESS.json @@ -0,0 +1,86 @@ +{ + "cut_after": 353, + "handoff_after": 362, + "pivot": 4, + "fresh": 34, + "group": [ + 4, + 20, + 21 + ], + "boundary": [ + [ + "SCALE", + 4, + "-1" + ], + [ + "ADD", + 21, + 4, + "1" + ], + [ + "ADD", + 4, + 20, + "1" + ] + ], + "middle": [ + [ + "SWAP", + 4, + 21 + ], + [ + "ADD", + 4, + 1, + "1" + ], + [ + "ADD", + 4, + 20, + "-1" + ], + [ + "ADD", + 0, + 4, + "2" + ], + [ + "ADD", + 2, + 4, + "-2" + ], + [ + "ADD", + 20, + 4, + "2" + ] + ], + "a": { + "1": "1", + "20": "-1", + "21": "1" + }, + "b": { + "0": "-2", + "2": "2", + "20": "-2", + "21": "-1" + }, + "c": { + "20": "1", + "4": "-1" + }, + "d": { + "4": "-1", + "21": "-1" + } +} diff --git a/research/p104-cut353-independent-audit/inputs/caller.py.txt b/research/p104-cut353-independent-audit/inputs/caller.py.txt new file mode 100644 index 0000000000..9a7abb8ec7 --- /dev/null +++ b/research/p104-cut353-independent-audit/inputs/caller.py.txt @@ -0,0 +1,134 @@ +"""Changed eight-field common-idle caller, using exact ordinary bases. + +Cinna Davis supplies the native query and binary supplier lineage. The +six-field root and exact coefficient-ring replay are by Ali Romman with +Codex assistance. The changed rank-(2,4,4,3,2) root, common-idle fusion and +fresh-input application are by thu-nmrc with substantial Codex assistance. +Apache-2.0. This constructor requires only the Python standard library. +""" +from collections import Counter +from copy import deepcopy +from hashlib import sha256 +from pathlib import Path +import json +from algebra import Q,accumulate,coefficient,eye,matrix,need,shifted,zmul +HERE=Path(__file__).resolve().parent + +def unit(q): + q=Q(q) + return q and abs(q.numerator)&(abs(q.numerator)-1)==0 and q.denominator&(q.denominator-1)==0 + +def construct(): + data=json.loads((HERE/'ROOT.json').read_text()) + full,masks=data['full_sites'],data['masks'] + bases={int(i):matrix(m)for i,m in data['bases'].items()} + events,targets,nodes,cuts=[],{},[],{} + stage,next_role=0,8 + def emit(op,*args):events.append([op,*args]) + def mix(rows): + a=deepcopy(rows);ops=[] + for j in range(8): + k=next((k for k in range(j,8)if unit(a[k][j])),None) + need(k is not None,'Declared dyadic unit pivot') + if k!=j:a[j],a[k]=a[k],a[j];ops.append(['SWAP',j,k]) + c=1/a[j][j] + if c!=1:a[j]=[c*x for x in a[j]];ops.append(['SCALE',j,str(c)]) + for k in range(8): + if k!=j and a[k][j]: + c=-a[k][j];a[k]=[x+c*y for x,y in zip(a[k],a[j])];ops.append(['ADD',k,j,str(c)]) + need(a==eye(8),'Complete ordinary basis elimination') + for e in reversed(ops): + if e[0]=='ADD':e[-1]=str(-Q(e[-1])) + elif e[0]=='SCALE':e[-1]=str(1/Q(e[-1])) + emit(*e) + def label(t): + nonlocal stage + if t==1:stage+=1;return {'stage':stage,'stages':[stage]} + a,b=map(label,t);return {'left':a,'right':b,'stages':a['stages']+b['stages']} + def shape(n): + return 1 if n==1 else [shape(n//2),shape(n-n//2)] + trees=[label(shape(n))for n in data['child_sizes']] + need(trees==data['trees'],'Declared independent stage allocation') + def query(x,y): + emit('LAMBDA',x,-1);emit('QUERY',x,y,-1);emit('LAMBDA',x,1) + def supplier(t,x,y): + nonlocal next_role + if 'stage'in t: + emit('LAMBDA',x,-1);emit('LOCAL',t['stage'],y,x);emit('LAMBDA',x,1);return + a,b=next_role,next_role+1;next_role+=2;st=t['stages'];nodes.append({'roles':[a,b],'stages':st}) + emit('SWAP',x,b);emit('SWAP',y,a);emit('SWAP',a,b) + emit('ADD',x,a,'1');emit('ADD',b,y,'-1');query(a,b) + cuts[tuple(st)]={'cut_after':len(events)-1,'pivot_aux':[a,b],'active':[x,y]} + emit('ADD',b,y,'1');emit('ADD',x,a,'-1');emit('IDLE',a,b,st) + emit('SCALE',y,'-1');supplier(t['left'],y,x);emit('SCALE',y,'-1');supplier(t['right'],x,y) + emit('ADD',x,a,'1');emit('SCALE',a,'-1');emit('ADD',a,x,'1');emit('SWAP',y,b);emit('SCALE',b,'-1');emit('ADD',b,y,'1') + targets[a],targets[b]=[-1,st],[-1,st] + from algebra import inverse + fi,i=0,0 + while i<9: + c=bases[i];mix(inverse(c)) + if i==1: + b,ct=trees[fi:fi+2];fi+=2 + supplier(b,0,1);emit('ADD',0,1,'-1') + emit('SCALE',1,'-1');supplier(ct,1,0);emit('SCALE',1,'-1');emit('ADD',1,0,'1') + emit('IDLE',2,3,b['stages']+ct['stages']);i+=2 + elif i in full: + t=trees[fi];fi+=1;supplier(t,0,1);emit('ADD',0,1,'-1') + for r in range(2,masks[full.index(i)].bit_count()):emit('IDLE_ONE',r,t['stages']) + i+=1 + else:query(0,1);emit('ADD',0,1,'-1');i+=1 + mix(c) + for r in range(8): + targets[r]=[-1,[j for mask,t in zip(masks,trees)if mask>>r&1 for j in t['stages']]] + for r in range(next_role):emit('LAMBDA',r,-1) + diagonal=[[targets[r][0],0]+[int(j in targets[r][1])for j in range(1,stage+1)]for r in range(next_role)] + need((stage,next_role)==(18,34),'Complete caller dimensions') + return {'schema':'root8-common-idle-fusion/1','roles':next_role,'stages':stage,'ambient_rank':9+8*stage, + 'events':events,'diagonal':diagonal,'nodes':nodes} + +def replay(word): + n,width=word['roles'],word['stages']+2;zero=(0,)*width + rows=[[{zero:coefficient(1)}if i==j else {}for j in range(n)]for i in range(n)];seen=[] + for event in word['events']: + op=event[0] + if op=='ADD': + _,dst,src,c=event + for a,b in zip(rows[dst],rows[src]):accumulate(a,b,coefficient(c)) + elif op=='SCALE': + _,dst,c=event;rows[dst]=[{key:zmul(coefficient(c),value)for key,value in cell.items()}for cell in rows[dst]] + elif op=='SWAP': + _,a,b=event;rows[a],rows[b]=rows[b],rows[a] + elif op in ('LOCAL','QUERY'): + if op=='LOCAL':_,stage,src,dst=event;exponent=-1;seen.append(stage) + else:_,dst,src,exponent=event + term=(exponent,)+(0,)*(width-1) + for a,b in zip(rows[dst],shifted(rows[src],term)):accumulate(a,b) + if op=='LOCAL': + term=(0,)+tuple(int(s==stage)for s in range(width-1)) + for r in (src,dst):rows[r]=shifted(rows[r],term) + elif op=='Q_POWER':rows[event[1]]=shifted(rows[event[1]],(event[2],)+(0,)*(width-1)) + elif op=='LAMBDA': + _,r,sign=event;need(sign in(-1,1),'Ordinary normalization sign') + old=rows[r];other=shifted(old,(2,)+(0,)*(width-1));rows[r]=[{}for _ in range(n)] + for dst,a,b in zip(rows[r],old,other): + accumulate(dst,a,(Q(1,2),Q(sign,2)));accumulate(dst,b,(Q(1,2),Q(-sign,2))) + elif op in('IDLE','IDLE_ONE'): + roles,stages=(event[1:3],event[3])if op=='IDLE'else([event[1]],event[2]) + need(len(stages)==len(set(stages)),'Distinct whole-idle axes') + term=(0,)+tuple(int(s in stages)for s in range(width-1)) + for r in roles:rows[r]=shifted(rows[r],term) + else:raise ValueError('Unknown caller opcode') + expected=[[{(word['diagonal'][i][0]%4,)+tuple(word['diagonal'][i][1:]):coefficient(1)}if i==j else {}for j in range(n)]for i in range(n)] + need(sorted(seen)==list(range(1,word['stages']+1)),'Every distinct native stage once') + need(rows==expected,'Every arbitrary-input forward coefficient') + return {'inputs':n,'coefficients':n*n,'native_stages':len(seen),'events':len(word['events']), + 'event_sha256':sha256(json.dumps(word['events'],separators=(',',':')).encode()).hexdigest()} + +def controls(word): + controls={} + for op in('LOCAL','QUERY','IDLE','IDLE_ONE','LAMBDA','ADD'): + bad=deepcopy(word);del bad['events'][next(i for i,e in enumerate(bad['events'])if e[0]==op)] + try:replay(bad) + except ValueError as error:controls['missing_'+op.lower()]=str(error) + else:raise ValueError('Missing gate accepted: '+op) + return controls diff --git a/research/p104-cut353-independent-audit/oracle.py b/research/p104-cut353-independent-audit/oracle.py new file mode 100644 index 0000000000..e2cc736988 --- /dev/null +++ b/research/p104-cut353-independent-audit/oracle.py @@ -0,0 +1,455 @@ +#!/usr/bin/env python3 +"""Reverse-covector/forward-vector exact oracle for the PR6716 cut. + +The first monomial coordinate is source Q (not the proof's q=Q^-1). +LOCAL is an explicit conditional contract, not native supplier admission. +""" +import argparse +from fractions import Fraction as F +from hashlib import sha256, sha1 +import json +from pathlib import Path + +N = 18 +UNIT = (0, (0,) * N) +ONE = {UNIT: (F(1), F(0))} +MAX_TERMS = 100000 +INPUT_PINS = { + "inputs/PROOF.md": "bdf2a3e379d0aaf8ae42a49b09ee6f9d21c5c1a8ec8653fab75efac0c5c93099", + "inputs/README.md": "68f52f2e0fa916cbf98e18896f0f6026469d3e45474e6d4314f95e0959cef6cb", + "inputs/WITNESS.json": "4c820b99eb1ebebd7cd527f07b0aa86a355865072acace8bfc9fddd998086331", + "inputs/CONTROLLER-UNRETIRED.json": "8c58adc35a7055dde1eda8f2547492dda9f558a73262fc17f439819c39d2555e", + "inputs/CONTROLLER.json": "2a0fb1c11fccfcc4dacbc7c82cf439969caa295dba4fc1a21a83e01b4ab8affc", + "inputs/caller.py.txt": "ad0dd4aa97ae19f687defc8690e0ffb5f8ada551720aba4b48b8d307c776b5ba", +} +META_PINS = { + "SOURCE-PINS.json": "0de615eb3eac51539567c56e85e177c91c0d3e5c2c69b8cd64abff46f68fc902", + "CASES.json": "7a7e961a1971c31653770af43b0097ba55d1eb980795a050c74786e8f5c7d6c0", + "SCHEMA.json": "3936e155a437939af360d5b2c4be83036984e56c7d04665c5eca2dc7f09ba50d", +} + + +def need(ok, why): + if not ok: + raise ValueError(why) + + +def canonical(obj): + return json.dumps(obj, sort_keys=True, separators=(",", ":"), ensure_ascii=True).encode() + + +def pairs(items): + out = {} + for k, v in items: + need(k not in out, "duplicate JSON key") + out[k] = v + return out + + +def decode_json(raw): + def bad(value): + raise ValueError("nonfinite JSON: " + value) + need(len(raw) <= 16777216, "bounded JSON input bytes") + return json.loads(raw, object_pairs_hook=pairs, parse_constant=bad) + + +def load(path): + return decode_json(path.read_bytes()) + + +def rational(text): + need(type(text) is str and len(text) <= 128, "bounded rational string") + value = F(text) + need(str(value) == text and value.denominator & (value.denominator - 1) == 0, "canonical dyadic") + need(value.numerator.bit_length() <= 256 and value.denominator.bit_length() <= 256, "rational height") + return value + + +def add(a, b): + out = a.copy() + for m, (r, i) in b.items(): + x, y = out.get(m, (F(0), F(0))) + value = (x + r, y + i) + if value == (0, 0): + out.pop(m, None) + else: + out[m] = value + need(len(out) <= MAX_TERMS, "polynomial term budget") + return out + + +def scale(poly, real, imag=0): + if real == 0 and imag == 0: + return {} + return {m: (r * real - i * imag, r * imag + i * real) for m, (r, i) in poly.items()} + + +def shift(poly, power=0, stages=()): + exponents = [0] * N + for stage in stages: + exponents[stage - 1] += 1 + return {((q + power) % 4, tuple(a + b for a, b in zip(d, exponents))): value + for (q, d), value in poly.items()} + + +def times(a, b): + out = {} + for (q, d), (r, i) in b.items(): + temp = {((p + q) % 4, tuple(x + y for x, y in zip(c, d))): (x * r - y * i, x * i + y * r) + for (p, c), (x, y) in a.items()} + out = add(out, temp) + return out + + +def lambda_action(poly, sign): + return add(scale(poly, F(1, 2), F(sign, 2)), + scale(shift(poly, 2), F(1, 2), F(-sign, 2))) + + +def serialize(poly): + return [[q, list(d), [r.numerator, r.denominator, i.numerator, i.denominator]] + for (q, d), (r, i) in sorted(poly.items())] + + +def vector(sparse, size): + out = [{} for unused in range(size)] + for key, text in sparse.items(): + need(key.isdecimal() and str(int(key)) == key and int(key) < size, "sparse vector role") + out[int(key)] = scale(ONE, rational(text)) + return out + + +def roles(event): + op = event[0] + if op == "LOCAL": + return event[2:4] + if op in ("ADD", "SWAP", "QUERY", "IDLE"): + return event[1:3] + return event[1:2] + + +def check_events(events, size): + need(type(events) is list and len(events) <= 1024, "bounded event list") + for event in events: + need(type(event) is list and event, "instruction list") + op = event[0] + lengths = {"ADD": 4, "SWAP": 3, "SCALE": 3, "LAMBDA": 3, + "QUERY": 4, "LOCAL": 4, "IDLE": 4, "IDLE_ONE": 3} + need(op in lengths and len(event) == lengths[op], "typed opcode") + indices = roles(event) + need(all(type(x) is int and 0 <= x < size for x in indices), "typed role indices") + need(len(set(indices)) == len(indices), "distinct two-field operands") + if op in ("ADD", "SCALE"): + value = rational(event[-1]) + need(op != "SCALE" or value != 0, "invertible ordinary scale") + elif op in ("QUERY", "LAMBDA"): + need(type(event[-1]) is int and event[-1] in (-1, 1), "signed phase exponent") + elif op == "LOCAL": + need(type(event[1]) is int and 1 <= event[1] <= N, "typed LOCAL stage") + elif op in ("IDLE", "IDLE_ONE"): + stages = event[-1] + need(type(stages) is list and stages and all(type(x) is int and 1 <= x <= N for x in stages), + "typed idle stage list") + need(stages == sorted(set(stages)), "distinct ascending idle stages") + + +def reverse(row, events): + """Pull one output covector through M_last ... M_first.""" + row = row.copy() + for event in reversed(events): + op = event[0] + if op == "ADD": + dst, src, text = event[1:] + row[src] = add(row[src], scale(row[dst], rational(text))) + elif op == "SWAP": + a, b = event[1:] + row[a], row[b] = row[b], row[a] + elif op == "SCALE": + row[event[1]] = scale(row[event[1]], rational(event[2])) + elif op == "LAMBDA": + row[event[1]] = lambda_action(row[event[1]], event[2]) + elif op == "QUERY": + dst, src, exponent = event[1:] + row[src] = add(row[src], shift(row[dst], exponent)) + elif op == "LOCAL": + stage, src, dst = event[1:] + old_src, old_dst = row[src], row[dst] + row[src] = shift(add(old_src, shift(old_dst, -1)), stages=(stage,)) + row[dst] = shift(old_dst, stages=(stage,)) + else: + for role in roles(event): + row[role] = shift(row[role], stages=event[-1]) + need(sum(len(x) for x in row) <= MAX_TERMS, "reverse live term budget") + return row + + +def forward(column, events): + """Push one independent column through chronological instructions.""" + column = column.copy() + for event in events: + op = event[0] + if op == "ADD": + dst, src, text = event[1:] + column[dst] = add(column[dst], scale(column[src], rational(text))) + elif op == "SWAP": + a, b = event[1:] + column[a], column[b] = column[b], column[a] + elif op == "SCALE": + column[event[1]] = scale(column[event[1]], rational(event[2])) + elif op == "LAMBDA": + column[event[1]] = lambda_action(column[event[1]], event[2]) + elif op == "QUERY": + dst, src, exponent = event[1:] + column[dst] = add(column[dst], shift(column[src], exponent)) + elif op == "LOCAL": + stage, src, dst = event[1:] + old_src, old_dst = column[src], column[dst] + column[dst] = shift(add(old_dst, shift(old_src, -1)), stages=(stage,)) + column[src] = shift(old_src, stages=(stage,)) + else: + for role in roles(event): + column[role] = shift(column[role], stages=event[-1]) + need(sum(len(x) for x in column) <= MAX_TERMS, "forward live term budget") + return column + + +def basis(index, size): + out = [{} for unused in range(size)] + out[index] = ONE.copy() + return out + + +def expected_target(declaration): + need(type(declaration) is list and len(declaration) == 20 and + all(type(x) is int for x in declaration) and declaration[1] == 0, + "20-coordinate source diagonal, dummy coordinate zero") + return {(declaration[0] % 4, tuple(declaration[2:])): (F(1), F(0))} + + +def dot(left, right): + out = {} + for a, b in zip(left, right): + out = add(out, times(a, b)) + return out + + +def inverse_ordinary(events): + out = [] + for event in reversed(events): + if event[0] == "SWAP": + out.append(event.copy()) + elif event[0] == "ADD": + out.append(event[:-1] + [str(-rational(event[-1]))]) + else: + need(event[0] == "SCALE", "ordinary inverse opcode") + out.append(event[:-1] + [str(1 / rational(event[-1]))]) + return out + + +def compute(unretired, final, witness): + need(unretired["roles"] == 34 and final["roles"] == 35, "independent role counts") + need(unretired["stages"] == final["stages"] == N, "18 independent Laurent stages") + old_events, new_events = unretired["events"], final["events"] + need(len(old_events) == 562 and len(new_events) == 586, "literal event counts") + check_events(old_events, 34) + check_events(new_events, 35) + need([witness[x] for x in ("cut_after", "handoff_after", "pivot", "fresh")] == [353, 362, 4, 34], + "literal cut and fresh handoff indices") + first = next(index for index, event in enumerate(new_events) if 34 in roles(event)) + need(first == 363 and all(34 not in roles(e) for e in new_events[:363]), "fresh input untouched until handoff") + a, b, c, d = [vector(witness[key], 34) for key in ("a", "b", "c", "d")] + boundary, middle = witness["boundary"], witness["middle"] + need(len(boundary) == 3 and len(middle) == 6, "ordinary witness word sizes") + check_events(boundary, 34) + check_events(middle, 34) + need(all(e[0] in ("ADD", "SCALE", "SWAP") for e in boundary + middle), "ordinary witness coefficients") + need(new_events[:3] == inverse_ordinary(boundary) and new_events[3:357] == old_events[:354] + and new_events[357:363] == middle, "literal inverseG/prefix/J binding at handoff") + pivot = basis(4, 34) + identities = [dot(a, b) == ONE, dot(c, d) == ONE, + reverse(pivot, boundary) == c, forward(d, boundary) == pivot, + reverse(pivot, middle) == a, forward(b, middle) == pivot] + need(all(identities), "six ordinary dual-pair/basis identities") + S = lambda_action(shift(ONE, -1), 1) + need(times(S, S) == ONE and shift(ONE, 4) == ONE, "S involution with Q^4=1") + need(S != shift(ONE, -1) and shift(ONE, 2) != ONE, "retain central square and global lambda") + prefix = old_events[:354] + a_prefix, prefix_d = reverse(a, prefix), forward(d, prefix) + need(a_prefix == [times(S, entry) for entry in c], "all34 exact aP=S*c positions") + need(prefix_d == [times(S, entry) for entry in b], "all34 exact Pd=S*b positions") + final_matrix = [reverse(basis(row, 35), new_events) for row in range(35)] + need(len(unretired["diagonal"]) == 34 and len(final["diagonal"]) == 35, "declared diagonal lengths") + targets = [expected_target(entry) for entry in unretired["diagonal"]] + need(witness["group"] == [4, 20, 21] and targets[4] == targets[20] == targets[21], + "G mixes equal complete old targets") + need(all(set(roles(e)) <= {4, 20, 21} for e in boundary), "G support in equal-target group") + targets[4] = shift(ONE, -1) + targets.append(shift(ONE, stages=(10, 11, 12, 13))) + need([expected_target(entry) for entry in final["diagonal"]] == targets, "fresh expected target contract") + for row in range(35): + for col in range(35): + need(final_matrix[row][col] == (targets[row] if row == col else {}), "literal35x35 endpoint") + artifact = {"schema_version": 1, "a_prefix": [serialize(x) for x in a_prefix], + "prefix_d": [serialize(x) for x in prefix_d], + "final_matrix": [[serialize(x) for x in row] for row in final_matrix]} + need(len(canonical(artifact)) <= 4194304, "canonical artifact byte budget") + return artifact, {"cut_after": 353, "handoff_after": 362, "pivot": 4, "fresh": 34, + "unretired_roles": 34, "unretired_events": 562, "final_roles": 35, + "final_events": 586, "stages": 18, "cut_cells": 68, "final_cells": 1225, + "ordinary_identities": 6, "fresh_first_contact": first} + + +def validate_poly(poly): + need(type(poly) is list and len(poly) <= MAX_TERMS, "polynomial term list") + previous = None + for term in poly: + need(type(term) is list and len(term) == 3, "term triple") + q, stages, coefficient = term + need(type(q) is int and 0 <= q < 4, "reduced central exponent") + need(type(stages) is list and len(stages) == N and + all(type(x) is int and -1024 <= x <= 1024 for x in stages), "typed Laurent exponents") + need(type(coefficient) is list and len(coefficient) == 4 and + all(type(x) is int and x.bit_length() <= 4096 for x in coefficient), "typed Gaussian rational") + rn, rd, im, iden = coefficient + need(rd > 0 and iden > 0, "positive denominators") + r, i = F(rn, rd), F(im, iden) + need([r.numerator, r.denominator, i.numerator, i.denominator] == coefficient and (r != 0 or i != 0), + "normalized nonzero Gaussian coefficient") + key = (q, tuple(stages)) + need(previous is None or previous < key, "strictly sorted unique monomials") + previous = key + + +def validate_artifact(obj): + need(type(obj) is dict and set(obj) == {"schema_version", "a_prefix", "prefix_d", "final_matrix"}, "artifact keys") + need(type(obj["schema_version"]) is int and obj["schema_version"] == 1, "artifact schema") + for key in ("a_prefix", "prefix_d"): + need(type(obj[key]) is list and len(obj[key]) == 34, "34 cut positions") + for poly in obj[key]: + validate_poly(poly) + need(type(obj["final_matrix"]) is list and len(obj["final_matrix"]) == 35, "35 endpoint rows") + for row in obj["final_matrix"]: + need(type(row) is list and len(row) == 35, "35 endpoint columns") + for poly in row: + validate_poly(poly) + + +def actual_controls(unretired, final, artifact): + """Exercise the real reverse engine on valid mutated source instructions. + + These endpoint tests deliberately bypass the constructor-prefix equality + gate. Expected targets come again from the unretired target declaration, + not the source final packet or recomputed final matrix. + """ + targets = [expected_target(x) for x in unretired["diagonal"]] + targets[4] = shift(ONE, -1) + targets.append(shift(ONE, stages=(10, 11, 12, 13))) + events = final["events"] + query_index = next(j for j, e in enumerate(events) if e[0] == "QUERY") + need(events[query_index][-1] == -1 and events[0][0] == "ADD" and events[0][-1] == "-1", + "control mutation sites") + mutants = [] + changed_query = [e.copy() for e in events] + changed_query[query_index][-1] = 1 + mutants.append(("first_QUERY_central_inverse", changed_query)) + changed_input_basis = [e.copy() for e in events] + changed_input_basis[0][-1] = "-2" + mutants.append(("first_input_G_ADD_coefficient", changed_input_basis)) + witnesses = [] + for name, instructions in mutants: + check_events(instructions, 35) + witness = None + for row in range(35): + actual = reverse(basis(row, 35), instructions) + for col in range(35): + expected = targets[row] if row == col else {} + difference = add(actual[col], scale(expected, -1)) + if difference: + witness = {"name": name, "row": row, "column": col, + "nonzero_difference": serialize(difference)} + break + if witness is not None: + break + need(witness is not None, "actual reverse engine failed to detect source-word mutant") + witnesses.append(witness) + + def rejection(function, name): + try: + function() + except ValueError: + return name + raise ValueError("strict malformed-artifact control accepted: " + name) + + def changed_artifact(mode): + obj = json.loads(canonical(artifact)) + poly = next(poly for poly in obj["a_prefix"] if len(poly) >= 2) + if mode == "boolean_denominator": + poly[0][2][1] = True + elif mode == "duplicate_monomial": + poly.append(poly[0]) + else: + poly.reverse() + return obj + + strict = [rejection(lambda mode=mode: validate_artifact(changed_artifact(mode)), mode) + for mode in ("boolean_denominator", "duplicate_monomial", "unsorted_monomials")] + strict.append(rejection(lambda: decode_json(b'{"bad":NaN}'), "nonfinite_JSON")) + strict.append(rejection(lambda: decode_json(b'{"key":1,"key":1}'), "duplicate_JSON_key")) + return {"actual_source_word_mutations": witnesses, "strict_rejections": strict, + "total_controls": len(witnesses) + len(strict)} + + +def authenticate(package): + need(INPUT_PINS and META_PINS, "oracle not sealed with frozen input pins") + for name, expected in META_PINS.items(): + need(sha256((package / name).read_bytes()).hexdigest() == expected, "frozen metadata: " + name) + manifest = load(package / "SOURCE-PINS.json") + need(manifest["schema_version"] == 1 and + {entry["local_path"] for entry in manifest["sources"]} == set(INPUT_PINS), "six inert source manifest entries") + for name, expected in INPUT_PINS.items(): + raw = (package / name).read_bytes() + need(len(raw) <= 16777216 and sha256(raw).hexdigest() == expected, "frozen inert input: " + name) + entry = next(x for x in manifest["sources"] if x["local_path"] == name) + need(entry["sha256"] == expected and entry["git_commit"] == "a467457692bc9e11113d9b2e2e34ea8ffb553b58", + "frozen source head and SHA") + need(sha1(b"blob " + str(len(raw)).encode() + b"\0" + raw).hexdigest() == entry["git_blob"], "source Git blob") + return manifest + + +def main(): + p = argparse.ArgumentParser(description=__doc__) + p.add_argument("--package", type=Path, default=Path(__file__).resolve().parent) + p.add_argument("--first", action="store_true") + p.add_argument("--artifact", type=Path) + p.add_argument("--expected", type=Path) + p.add_argument("--write-actions", "--write-packet", dest="write_actions", type=Path) + p.add_argument("--output", type=Path) + args = p.parse_args() + authenticate(args.package) + inputs = args.package / "inputs" + unretired = load(inputs / "CONTROLLER-UNRETIRED.json") + final = load(inputs / "CONTROLLER.json") + artifact, counts = compute(unretired, final, load(inputs / "WITNESS.json")) + validate_artifact(artifact) + controls = actual_controls(unretired, final, artifact) + common = {"schema_version": 1, "scope": "PR6716 cut353 fresh34 conditional LOCAL audit", + "source_manifest_sha256": META_PINS["SOURCE-PINS.json"], + "case_manifest_sha256": META_PINS["CASES.json"], **counts, + "artifact_sha256": sha256(canonical(artifact)).hexdigest()} + if not args.first: + actual = load(args.artifact or args.package / "PACKET.json") + validate_artifact(actual) + need(canonical(actual) == canonical(artifact), "actual artifact differs from reverse-row oracle") + expected = load(args.expected or args.package / "RESULT.json") + need(canonical(expected) == canonical(common), "actual receipt differs from recomputation") + if args.write_actions: + args.write_actions.write_text(json.dumps(artifact, indent=2, sort_keys=True) + "\n") + if args.output: + args.output.write_text(json.dumps(common, indent=2, sort_keys=True) + "\n") + print("PASS reverse-row cut oracle") + print(json.dumps(common, sort_keys=True)) + print(json.dumps({"oracle_controls": controls}, sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/p104-cut353-independent-audit/verify.py b/research/p104-cut353-independent-audit/verify.py new file mode 100644 index 0000000000..52fd61bd66 --- /dev/null +++ b/research/p104-cut353-independent-audit/verify.py @@ -0,0 +1,481 @@ +#!/usr/bin/env python3 +"""Exact independent audit of PR6716's serialized cut353 retirement.""" +import argparse +import copy +from fractions import Fraction as F +import hashlib +import json +from pathlib import Path +import sys +import time + +ROOT = Path(__file__).resolve().parent +SOURCE_SHA = "0de615eb3eac51539567c56e85e177c91c0d3e5c2c69b8cd64abff46f68fc902" +CASE_SHA = "7a7e961a1971c31653770af43b0097ba55d1eb980795a050c74786e8f5c7d6c0" +SCHEMA_SHA = "3936e155a437939af360d5b2c4be83036984e56c7d04665c5eca2dc7f09ba50d" +ZERO = (F(0), F(0)) +UNIT = (F(1), F(0)) +MONOMIAL_ONE = (0,) * 19 +ONE = {MONOMIAL_ONE: UNIT} +BYTE_CAP = 16777216 + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":"), + ensure_ascii=True).encode("ascii") + + +def sha(data): + return hashlib.sha256(data).hexdigest() + + +def unique_pairs(items): + result = {} + for key, value in items: + need(key not in result, "duplicate JSON key") + result[key] = value + return result + + +def forbidden_number(_): + raise ValueError("noninteger or nonfinite JSON number") + + +def json_types(value): + need(type(value) in (dict, list, int, str, type(None)), + "unsupported JSON type (including boolean)") + if type(value) is dict: + for key, item in value.items(): + need(type(key) is str, "nonstring JSON key") + json_types(item) + elif type(value) is list: + for item in value: + json_types(item) + + +def decode(data): + need(len(data) <= BYTE_CAP, "input exceeds byte cap") + value = json.loads(data, object_pairs_hook=unique_pairs, + parse_float=forbidden_number, + parse_constant=forbidden_number) + json_types(value) + return value + + +def load(path): + return decode(path.read_bytes()) + + +def exact(actual, expected, label): + need(type(actual) is type(expected), label + ": type mismatch") + if type(expected) is dict: + need(set(actual) == set(expected), label + ": keys differ") + for key in expected: + exact(actual[key], expected[key], label + "/" + key) + elif type(expected) is list: + need(len(actual) == len(expected), label + ": lengths differ") + for index, (left, right) in enumerate(zip(actual, expected)): + exact(left, right, label + "/" + str(index)) + else: + need(actual == expected, label + ": value differs") + + +def authenticate(): + for name, expected in (("SOURCE-PINS.json", SOURCE_SHA), + ("CASES.json", CASE_SHA), + ("SCHEMA.json", SCHEMA_SHA)): + need(sha((ROOT / name).read_bytes()) == expected, + "source/case/schema byte authentication: " + name) + manifest = load(ROOT / "SOURCE-PINS.json") + need(type(manifest.get("sources")) is list + and len(manifest["sources"]) == 6, "six inert source objects") + paths = [] + for row in manifest["sources"]: + path = row["local_path"] + need(path.startswith("inputs/") and ".." not in Path(path).parts, + "source path outside inputs") + need(sha((ROOT / path).read_bytes()) == row["sha256"], + "source bytes differ: " + path) + paths.append(path) + need(len(set(paths)) == 6, "duplicate source path") + + +def zproduct(a, b): + return a[0] * b[0] - a[1] * b[1], a[0] * b[1] + a[1] * b[0] + + +def padd(left, right, factor=UNIT): + result = dict(left) + for key, value in right.items(): + real, imag = zproduct(value, factor) + old = result.get(key, ZERO) + value = old[0] + real, old[1] + imag + if value == ZERO: + result.pop(key, None) + else: + result[key] = value + return result + + +def pscale(poly, coefficient): + return padd({}, poly, (F(coefficient), F(0))) + + +def pshift(poly, q=0, stages=(), degree=1): + result = {} + for key, value in poly.items(): + exponents = list(key) + exponents[0] = (exponents[0] + q) % 4 + for stage in stages: + exponents[stage] += degree + result[tuple(exponents)] = value + return result + + +def plambda(poly, sign): + return padd(padd({}, poly, (F(1, 2), F(sign, 2))), + pshift(poly, q=2), (F(1, 2), F(-sign, 2))) + + +def normalized_central(poly): + return plambda(pshift(poly, q=-1), 1) + + +def eye(size): + return [[dict(ONE) if row == column else {} + for column in range(size)] for row in range(size)] + + +def row_add(left, right, coefficient): + factor = F(coefficient), F(0) + return [padd(a, b, factor) for a, b in zip(left, right)] + + +def row_shift(row, q=0, stages=()): + return [pshift(poly, q=q, stages=stages) for poly in row] + + +def apply(matrix, event): + op = event[0] + if op == "ADD": + matrix[event[1]] = row_add(matrix[event[1]], matrix[event[2]], event[3]) + elif op == "SWAP": + matrix[event[1]], matrix[event[2]] = matrix[event[2]], matrix[event[1]] + elif op == "SCALE": + matrix[event[1]] = [pscale(poly, event[2]) for poly in matrix[event[1]]] + elif op == "LAMBDA": + matrix[event[1]] = [plambda(poly, event[2]) for poly in matrix[event[1]]] + elif op == "Q_POWER": + matrix[event[1]] = row_shift(matrix[event[1]], q=event[2]) + elif op == "QUERY": + source = row_shift(matrix[event[2]], q=event[3]) + matrix[event[1]] = row_add(matrix[event[1]], source, 1) + elif op == "LOCAL": + _, stage, src, dst = event + matrix[dst] = row_add(matrix[dst], row_shift(matrix[src], q=-1), 1) + for owner in (src, dst): + matrix[owner] = row_shift(matrix[owner], stages=[stage]) + elif op in ("IDLE", "IDLE_ONE"): + owners, stages = (event[1:3], event[3]) if op == "IDLE" else ([event[1]], event[2]) + for owner in owners: + matrix[owner] = row_shift(matrix[owner], stages=stages) + else: + raise ValueError("unknown opcode: " + str(op)) + + +def valid_index(value, size): + need(type(value) is int and 0 <= value < size, "invalid role index") + + +def validate_event(event, size, ordinary=False): + need(type(event) is list and len(event) >= 3, "event shape") + op = event[0] + lengths = {"ADD": 4, "SWAP": 3, "SCALE": 3, "LAMBDA": 3, + "Q_POWER": 3, "QUERY": 4, "LOCAL": 4, + "IDLE": 4, "IDLE_ONE": 3} + need(op in lengths and len(event) == lengths[op], "opcode arity") + if ordinary: + need(op in ("ADD", "SWAP", "SCALE"), "nonordinary basis opcode") + positions = [1, 2] if op in ("ADD", "SWAP", "QUERY", "IDLE") else [1] + if op == "LOCAL": + positions = [2, 3] + need(type(event[1]) is int and 1 <= event[1] <= 18, "native stage") + for index in positions: + valid_index(event[index], size) + if len(positions) == 2: + need(event[positions[0]] != event[positions[1]], "aliased event roles") + if op in ("ADD", "SCALE"): + need(type(event[-1]) is str and F(event[-1]) != 0, "nonzero rational scalar") + if op in ("QUERY", "LAMBDA"): + need(type(event[-1]) is int and event[-1] in (-1, 1), "central sign") + if op == "Q_POWER": + need(type(event[-1]) is int, "central exponent") + if op in ("IDLE", "IDLE_ONE"): + stages = event[-1] + need(type(stages) is list and len(stages) == len(set(stages)), "idle stage set") + need(all(type(x) is int and 1 <= x <= 18 for x in stages), "idle stages") + + +def validate_controller(value, size, events): + need(type(value) is dict and set(value) == {"schema", "roles", "stages", + "ambient_rank", "events", "diagonal", "nodes"}, "controller keys") + need(value["roles"] == size and type(value["roles"]) is int, + "controller role count") + need(value["stages"] == 18 and value["ambient_rank"] == 153, + "controller stage/rank contract") + need(len(value["events"]) == events, "controller event count") + for event in value["events"]: + validate_event(event, size) + need(len(value["diagonal"]) == size, "controller target count") + for target in value["diagonal"]: + need(type(target) is list and len(target) == 20 + and all(type(x) is int for x in target), "target exponent schema") + need(target[1] == 0, "nonzero undeclared stage-zero target") + + +def run_matrix(events, size): + matrix = eye(size) + for event in events: + apply(matrix, event) + need(sum(len(cell) for row in matrix for cell in row) <= 100000, + "simultaneous matrix polynomial term cap exceeded") + return matrix + + +def scalar_vector(entries, size): + need(type(entries) is dict, "ordinary vector schema") + vector = [F(0) for _ in range(size)] + for key, value in entries.items(): + need(type(key) is str and str(int(key)) == key, "ordinary vector index") + valid_index(int(key), size) + need(type(value) is str, "ordinary vector coefficient") + vector[int(key)] = F(value) + return vector + + +def scalar_pair(left, right): + return sum(a * b for a, b in zip(left, right)) + + +def linear_combination(polys, coefficients): + result = {} + for poly, coefficient in zip(polys, coefficients): + if coefficient: + result = padd(result, poly, (coefficient, F(0))) + return result + + +def row_times(vector, matrix): + return [linear_combination(column, vector) for column in zip(*matrix)] + + +def matrix_times(matrix, vector): + return [linear_combination(row, vector) for row in matrix] + + +def expected_vector(vector): + return [normalized_central(pscale(ONE, coefficient)) for coefficient in vector] + + +def check_bases(witness, a, b, c, d): + for name, row, column in (("boundary", c, d), ("middle", a, b)): + for event in witness[name]: + validate_event(event, 34, ordinary=True) + matrix = run_matrix(witness[name], 34) + need(matrix[4] == [pscale(ONE, value) for value in row], + "ordinary basis row: " + name) + image = matrix_times(matrix, column) + need(image == [ONE if role == 4 else {} for role in range(34)], + "ordinary basis column: " + name) + + +def inverse_ordinary(events): + inverse = [] + for event in reversed(events): + op = event[0] + if op == "ADD": + inverse.append([op, event[1], event[2], str(-F(event[3]))]) + elif op == "SCALE": + inverse.append([op, event[1], str(1 / F(event[2]))]) + else: + need(op == "SWAP", "inverse requires ordinary gates") + inverse.append(event[:]) + return inverse + + +def renamed(event, pivot, fresh): + out = event[:] + positions = {"ADD": [1, 2], "SWAP": [1, 2], "SCALE": [1], + "LAMBDA": [1], "Q_POWER": [1], "QUERY": [1, 2], + "LOCAL": [2, 3], "IDLE": [1, 2], "IDLE_ONE": [1]} + for position in positions[event[0]]: + if out[position] == pivot: + out[position] = fresh + return out + + +def check_serialized_surgery(base, final, witness): + cut, pivot, fresh = witness["cut_after"], witness["pivot"], witness["fresh"] + need((cut, pivot, fresh, witness["handoff_after"]) == (353, 4, 34, 362), + "literal cut/handoff ABI") + need(base["events"][353] == ["LAMBDA", 20, 1], "actual normalized cut") + need(witness["group"] == [4, 20, 21], "equal-target group") + expected = inverse_ordinary(witness["boundary"]) + expected += base["events"][:cut + 1] + witness["middle"] + expected += [renamed(e, pivot, fresh) for e in inverse_ordinary(witness["middle"])] + expected += [renamed(e, pivot, fresh) for e in base["events"][cut + 1:]] + expected += [["LAMBDA", owner, 1] for owner in (fresh, 20, 21)] + expected += [renamed(e, pivot, fresh) for e in witness["boundary"]] + expected += [["LAMBDA", owner, -1] for owner in (pivot, 20, 21)] + need(final["events"] == expected, "complete serialized retirement surgery") + contacts = [index for index, event in enumerate(final["events"]) + if renamed(event, fresh, 35) != event] + need(contacts and contacts[0] == 363, "fresh role touched before handoff") + + +def paid_signature(events): + result = [] + for event in events: + op = event[0] + if op == "LOCAL": + result.append([op, event[1]]) + elif op == "QUERY": + result.append([op, event[3]]) + elif op in ("IDLE", "IDLE_ONE"): + result.append([op, event[-1]]) + return result + + +def encode_poly(poly): + return [[key[0], list(key[1:]), [value[0].numerator, value[0].denominator, + value[1].numerator, value[1].denominator]] + for key, value in sorted(poly.items())] + + +def encode_vector(vector): + return [encode_poly(poly) for poly in vector] + + +def derive_targets(base): + targets = copy.deepcopy(base["diagonal"]) + need(targets[4] == targets[20] == targets[21], "complete equal-endpoint group") + targets[4] = [-1] + [0] * 19 + targets.append([0, 0] + [int(10 <= stage <= 13) for stage in range(1, 19)]) + return targets + + +def check_endpoint(matrix, targets): + for row in range(35): + for column in range(35): + target = targets[row] + key = (target[0] % 4, *target[2:]) + need(matrix[row][column] == ({key: UNIT} if row == column else {}), + "complete independent-input endpoint row/column") + + +def scientific(base, final, witness): + validate_controller(base, 34, 562) + validate_controller(final, 35, 586) + a, b, c, d = [scalar_vector(witness[name], 34) for name in ("a", "b", "c", "d")] + need(scalar_pair(a, b) == scalar_pair(c, d) == 1, "two ordinary dual pairings") + check_bases(witness, a, b, c, d) + check_serialized_surgery(base, final, witness) + prefix = run_matrix(base["events"][:354], 34) + a_prefix, prefix_d = row_times(a, prefix), matrix_times(prefix, d) + need(a_prefix == expected_vector(c), "prefix row aP=S c") + need(prefix_d == expected_vector(b), "prefix column Pd=S b") + targets = derive_targets(base) + need(final["diagonal"] == targets, "independently derived retired targets") + matrix = run_matrix(final["events"], 35) + check_endpoint(matrix, targets) + need(paid_signature(base["events"]) == paid_signature(final["events"]), + "paid stage/sign/order changed") + artifact = {"schema_version": 1, "a_prefix": encode_vector(a_prefix), + "prefix_d": encode_vector(prefix_d), + "final_matrix": [encode_vector(row) for row in matrix]} + return artifact + + +def rejected(function, label, diagnostic=None): + try: + function() + except (ValueError, TypeError, KeyError, json.JSONDecodeError) as error: + need(diagnostic is None or diagnostic in str(error), + "control rejected for unintended reason: " + label + ": " + str(error)) + return + raise ValueError("control accepted: " + label) + + +def controls(base, final, witness): + for raw in (b'{"x":1,"x":2}', b'{"x":NaN}', b'{"x":1.0}', b'{"x":true}'): + rejected(lambda raw=raw: decode(raw), "strict JSON") + rejected(lambda: validate_event(["ADD", True, 1, "1"], 35), "boolean role") + rejected(lambda: validate_event(["LOCAL", 19, 0, 1], 35), "unbound stage") + mutant = copy.deepcopy(witness) + mutant["a"]["20"] = "-2" + a, b = [scalar_vector(mutant[name], 34) for name in ("a", "b")] + rejected(lambda: need(scalar_pair(a, b) == 1, "broken dual pairing"), "pairing") + targets = derive_targets(base) + bad_query = copy.deepcopy(final["events"]) + index = next(i for i, event in enumerate(bad_query) if event[0] == "QUERY") + bad_query[index][-1] *= -1 + bad_basis = copy.deepcopy(final["events"]) + bad_basis[0][-1] = "-2" + bad_fresh = final["events"] + [["Q_POWER", 34, 1]] + for events, label in ((bad_query, "query central sign"), + (bad_basis, "input basis coefficient"), + (bad_fresh, "unearned fresh central factor")): + rejected(lambda events=events: check_endpoint(run_matrix(events, 35), targets), + label, "complete independent-input endpoint") + return 10 + + +def receipt(artifact): + return {"schema_version": 1, "source_manifest_sha256": SOURCE_SHA, + "case_manifest_sha256": CASE_SHA, + "scope": "PR6716 cut353 fresh34 conditional LOCAL audit", + "cut_after": 353, "handoff_after": 362, "pivot": 4, "fresh": 34, + "unretired_roles": 34, "unretired_events": 562, + "final_roles": 35, "final_events": 586, "stages": 18, + "cut_cells": 68, "final_cells": 1225, "ordinary_identities": 6, + "fresh_first_contact": 363, + "artifact_sha256": sha(canonical(artifact))} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--emit", action="store_true") + parser.add_argument("--write-packet", type=Path) + args = parser.parse_args() + start = time.monotonic() + authenticate() + base = load(ROOT / "inputs/CONTROLLER-UNRETIRED.json") + final = load(ROOT / "inputs/CONTROLLER.json") + witness = load(ROOT / "inputs/WITNESS.json") + artifact = scientific(base, final, witness) + need(len(canonical(artifact)) <= 4194304, "artifact exceeds4MiB") + count = controls(base, final, witness) + result = receipt(artifact) + need(time.monotonic() - start <= 180, "runtime exceeds180seconds") + if args.write_packet: + args.write_packet.write_bytes(canonical(artifact) + b"\n") + else: + exact(load(ROOT / "PACKET.json"), artifact, "actual packet") + if args.emit: + sys.stdout.buffer.write(canonical(result) + b"\n") + else: + exact(load(ROOT / "RESULT.json"), result, "retained result") + print(f"PASS_P104_CUT353_INDEPENDENT_AUDIT positions=1225 controls={count} no_new_kappa") + + +if __name__ == "__main__": + try: + main() + except (ValueError, OSError, KeyError, TypeError) as error: + print("FAIL_P104_CUT353_INDEPENDENT_AUDIT: " + str(error), file=sys.stderr) + raise SystemExit(1)