diff --git a/research/source-invoice-conformance/.gitattributes b/research/source-invoice-conformance/.gitattributes new file mode 100644 index 0000000000..7467454cb8 --- /dev/null +++ b/research/source-invoice-conformance/.gitattributes @@ -0,0 +1 @@ +source/** -text diff --git a/research/source-invoice-conformance/CALIBRATIONS.json b/research/source-invoice-conformance/CALIBRATIONS.json new file mode 100644 index 0000000000..2cc634c90f --- /dev/null +++ b/research/source-invoice-conformance/CALIBRATIONS.json @@ -0,0 +1,176 @@ +{ + "cases": [ + { + "claim": { + "invoice": { + "contract": { + "ambient_rank": 145, + "boundary": "complete p16/a7 unit before the retained mixed-target compiler", + "model": "mixed-target-unnormalized-power-v1", + "rank_semantics": "H_r has raw tariff r^(1-C), with surrendered productive fields debited" + }, + "paid": { + "1": 41298, + "16": 448, + "2": 7416, + "24": 448, + "3": 9180, + "32": 448, + "4": 2286, + "40": 448, + "48": 448, + "5": 720, + "56": 448, + "64": 448, + "72": 224, + "8": 144 + }, + "schema": "integer-mult-recursive-invoice/v1", + "targets": { + "145": 224, + "17": 448, + "25": 448, + "33": 448, + "4": 504, + "41": 448, + "49": 448, + "57": 448, + "65": 448, + "7": 126, + "73": 224, + "8": 846, + "9": 5868 + } + }, + "schema": "source-invoice-claim/v1", + "source_binding": { + "controller_canonical_sha256": "80dabeec6ea2ccd0a41e3cbb3f99674cff5b44cb64e846186e1d006f5871aa3c", + "word_canonical_sha256": "cfcd36b40326d7a5815e1db5313444379b3fb756b27d5201c561574c085cc0dd" + } + }, + "file": "source/PR4610-WORD.json.gz", + "histogram_origin": { + "base_path": "research/kappa-round6-compiler-tightening-20261022/ARITHMETIC.json", + "sha256": "b4f720a7ccbb5b46e472eaf85dc8739a40598986f19b37d26c4f9ecfbd31f0de" + }, + "name": "PR4610" + }, + { + "claim": { + "invoice": { + "contract": { + "ambient_rank": 145, + "boundary": "complete p16/a7 unit before the retained mixed-target compiler", + "model": "mixed-target-unnormalized-power-v1", + "rank_semantics": "H_r has raw tariff r^(1-C), with surrendered productive fields debited" + }, + "paid": { + "1": 41170, + "16": 448, + "2": 7416, + "24": 448, + "3": 9180, + "32": 448, + "4": 2286, + "40": 448, + "48": 448, + "5": 720, + "56": 448, + "64": 448, + "72": 224, + "8": 16 + }, + "schema": "integer-mult-recursive-invoice/v1", + "targets": { + "145": 224, + "17": 448, + "25": 448, + "33": 448, + "4": 504, + "41": 448, + "49": 448, + "57": 448, + "65": 448, + "7": 126, + "73": 224, + "8": 846, + "9": 5740 + } + }, + "schema": "source-invoice-claim/v1", + "source_binding": { + "controller_canonical_sha256": "80dabeec6ea2ccd0a41e3cbb3f99674cff5b44cb64e846186e1d006f5871aa3c", + "word_canonical_sha256": "86a9f0b429e73185f63ecc41afd40b13d33108fa5056e6d6d499a07d249bba58" + } + }, + "file": "source/PR5383-WORD.json.gz", + "histogram_origin": { + "field": "arithmetic", + "head": "4bd6efa51a495a7c7b7754915cf0244e7e60969e", + "path": "research/kappa-joint-relations-20261023/RESULT.json", + "pr": 5383, + "sha256": "d6a99bd75c6b7a2146b0fc4cfa038890aaf1d4adcdef42d767fdb40b687e61aa" + }, + "name": "PR5383" + }, + { + "claim": { + "invoice": { + "contract": { + "ambient_rank": 145, + "boundary": "complete p16/a7 unit before the retained mixed-target compiler", + "model": "mixed-target-unnormalized-power-v1", + "rank_semantics": "H_r has raw tariff r^(1-C), with surrendered productive fields debited" + }, + "paid": { + "1": 41170, + "16": 448, + "2": 7416, + "24": 448, + "3": 9180, + "32": 448, + "4": 2286, + "40": 448, + "48": 448, + "5": 720, + "56": 448, + "64": 448, + "72": 224, + "8": 16 + }, + "schema": "integer-mult-recursive-invoice/v1", + "targets": { + "145": 224, + "17": 448, + "25": 448, + "33": 448, + "4": 504, + "41": 448, + "49": 448, + "57": 448, + "65": 448, + "7": 126, + "73": 224, + "8": 846, + "9": 5740 + } + }, + "schema": "source-invoice-claim/v1", + "source_binding": { + "controller_canonical_sha256": "80dabeec6ea2ccd0a41e3cbb3f99674cff5b44cb64e846186e1d006f5871aa3c", + "word_canonical_sha256": "4d679409264d24264bd8d3121f39dce86b98a4faebce6fde8af2ec1ff13d5545" + } + }, + "file": "source/PR5387-WORD.json.gz", + "histogram_origin": { + "field": "arithmetic", + "head": "b1ab650d36f59e5be682a813145b7c67e219e341", + "path": "research/eight-owned-relations/RESULT.json", + "pr": 5387, + "sha256": "34ad456c1f98f7f8c361d63539ef26d75dad8ffb3444edf29652372acabf1aaf" + }, + "name": "PR5387" + } + ], + "schema_version": 1 +} diff --git a/research/source-invoice-conformance/EVIDENCE.md b/research/source-invoice-conformance/EVIDENCE.md new file mode 100644 index 0000000000..f3a0069488 --- /dev/null +++ b/research/source-invoice-conformance/EVIDENCE.md @@ -0,0 +1,107 @@ +# Source and validation record + +Canonical base `1ec1119972c9aefe42525172d07b332fcff81cb4`, priority revision 7. +The selected record, source manifest and review were resolved before this work: +κ=.0030217758 under five inherited framework assumptions; reproduce through +`make frontier4610-verify`. This opt-in package changes no selected data, +predecessor source or shared implementation. + +Inputs are package-local data exports, authenticated before verification by +EXPORTS.json. Original-word/caller bytes came from `git show BASE:path`. +Pending word bytes came from the GitHub contents API with explicit pinned `ref`. +No producer evaluator, price engine or receipt is imported or executed. + +* [#5383](https://github.com/CrocSwap/integer-mult-bounds/pull/5383): + `4bd6efa51a495a7c7b7754915cf0244e7e60969e`. +* [#5387](https://github.com/CrocSwap/integer-mult-bounds/pull/5387): + `b1ab650d36f59e5be682a813145b7c67e219e341`. + +CALIBRATIONS.json records the separately inspected producer-claim paths, +heads and raw receipt hashes from which its expected paid/target fields were +retained. Those fields are comparison fixtures, not evidence substituted for +the independent source interpretation. Native/caller profile annotations are +deliberately ignored. Source/checker hashes identify the actual execution; +they confer no physical or scientific acceptance by themselves. + +## Reproduction and coverage + +macOS 26.5.1 arm64, CPython 3.12.8, standard library only. Isolated branch +`codex/source-invoice-conformance`. Execute from the repository root: + +```sh +python3.12 -B scripts/research_package.py --package research/source-invoice-conformance --check-only +python3.12 -B scripts/research_package.py --package research/source-invoice-conformance +``` + +The manifest runs complete isolated, warning-strict normal and optimized +verification serially, with 120 seconds per command. The external run guard +also limits the complete pair to 300 seconds and samples descendant RSS every +0.5 seconds with a 1-GiB stop. RESOURCE.json records the final command and result. +The final pair passed in 24.793 seconds with sampled peak 290704 KiB. These resource measurements are not a mathematical storage guarantee. + +Coverage consists of the original selected word and two actual owned-relation +successors, both orientations and all independent entry columns, all native +frame transports, all paid events and helper endpoints, and the complete literal +p16/a7 caller with both boundary programs. The factored ledger accounts for +every recursive contribution at actual caller IDs. Its independent reconstruction +matches all three separately retained claim profiles. The CLI round trip writes +and rereads the full source audit and preflight invoice, checks its expected +claim, and rejects overwrite. The 24 controls cover source mutations, ownership, +rank/frame changes, false zero retags, target debits, queries/idles, caller +semantics, stale same-invoice bindings, malformed inputs and growth limits. + +The original and changed invoices exported from the checked result were also +accepted by the published signed preflight interface of +[#5397](https://github.com/CrocSwap/integer-mult-bounds/pull/5397), reporting +`uniformly_better` with paid delta−128H1−128H8 and target delta−128H9. +That is a format/arithmetic integration check, not new funding or a rerun of +the predecessor research package. + +Separate assisted reviews checked native interpretation, caller composition, +source binding and claim scope. Review led to explicit main port/endpoint +subspace gates, symbolic growth guards, bounded rational syntax and a hash of +the complete recursive ledger. Registered receipt checking also exposed an +unstable first-failing-role diagnostic from set iteration; sorted role order +fixes it. Golden data were updated only after confirming all positive invoices +and native semantic-audit hashes remained unchanged. The final normal/optimized +replays use the corrected code. Reviews share context; no independent human +or formal-kernel acceptance is claimed. + +## Freshness and limits + +The overlap helper at 2026-10-23 22:56 UTC reported complete pagination for 353 +open PR bodies and 4689 Discussion records. Sparse local-note coverage was +zero of 7267 tracked top-level notes; no missing local match establishes novelty. +Start-here, handoff and relevant current [Discussion #4930](https://github.com/CrocSwap/integer-mult-bounds/discussions/4930) / [#5125](https://github.com/CrocSwap/integer-mult-bounds/discussions/5125) activity were read +separately. Exact related code/claims distinguish the signed histogram preflight, +price compatibility oracle and this independent extractor. Arbitrary diffs and +unpublished work remain outside coverage. No public Discussion post was made +during the donor's local-draft checkpoint. + +Final targeted refresh retained the canonical base and both scientific word +heads. [#5391](https://github.com/CrocSwap/integer-mult-bounds/pull/5391) was +re-read at `96f193143a7a2ff8a4e6b9d574d7f551d68a7da3`: it remains a compatibility +oracle consuming trusted evidence, distinct from this source extractor. Recent +native-provider/normalization/controller-ceiling work changes constructions +rather than supplying this extractor; it is not imported or replayed here. + +No native absolute-phase engine, physical fresh-stage/coordinate embedding, +precision/tape implementation, complete ordinary-cost funding, compiler, +analytic recovery, selected cold replay, Lean or Docker was run or inferred. +The source-port guard binds the supported symbolic ABI; it does not prove the +all-size physical embedding. Unsupported schemas or growth reject as outside +this tool's domain, not as mathematical impossibility results. + +The checkout is shallow. Optional full source-history checking is unavailable; +metadata/source pins, direct base ancestry, committed bytes and portable export +verification are separate checks and do not imply full publication history. + +Final transport checks passed at scientific-code commit +`1d9608a86ac1f0b6ea51475874021fc49d5338dd`: committed-byte verification, +the official nineteen-file export and its integrity check, and a complete +optimized isolated replay from that Git-free export with empty PATH. Every +exported file remained byte-identical after replay. Direct base ancestry passes; +the optional history command reports `source-history check requires full Git +history`. A final static assisted review confirmed the native boundary and +symbolic-growth issues resolved, with no residual blocking issue. Subsequent +changes only record these validation results. diff --git a/research/source-invoice-conformance/EXPORTS.json b/research/source-invoice-conformance/EXPORTS.json new file mode 100644 index 0000000000..9531ddafa5 --- /dev/null +++ b/research/source-invoice-conformance/EXPORTS.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "exports": [ + { + "file": "source/PR5383-WORD.json.gz", + "head": "4bd6efa51a495a7c7b7754915cf0244e7e60969e", + "path": "research/kappa-joint-relations-20261023/WORD.json.gz", + "pr": 5383, + "author": "aliromman", + "sha256": "7883ba0faefc96505bb61ca7312d588fa22dfe2164050c817c1718b8fa28693a" + }, + { + "file": "source/PR5387-WORD.json.gz", + "head": "b1ab650d36f59e5be682a813145b7c67e219e341", + "path": "research/eight-owned-relations/WORD.json.gz", + "pr": 5387, + "author": "Dugongue", + "sha256": "6412632c28e265597fb088087048091d81c19500fb28a0c9c9d2a48f61b8665b" + }, + { + "file": "source/PR4610-WORD.json.gz", + "base_path": "research/kappa-round3-warp-20261022/ACTUAL-WORD.json.gz", + "sha256": "7679daa4ec6a40f56fc7f0202379a6f454310e94945aba4f48beaaaafb838d05" + }, + { + "file": "source/CONTROLLER.json", + "base_path": "research/joint-helper-lattice/CONTROLLER.json", + "sha256": "1f5d6aa267e4e66048818714b5d3b5eae17a58abe91d15deeaa34574f7391a5f" + } + ], + "scope": "Frozen source bytes only; no producer engine imported." +} diff --git a/research/source-invoice-conformance/PROOF.md b/research/source-invoice-conformance/PROOF.md new file mode 100644 index 0000000000..de18522c4a --- /dev/null +++ b/research/source-invoice-conformance/PROOF.md @@ -0,0 +1,178 @@ +# Source-to-invoice conformance argument + +## Claim and trust boundary + +The checker accepts a literal h9/v112 native word in the retained original or +owned-relation schema and a literal complex p16/a7 caller. It recomputes their +symbolic endpoint/ownership protocol and recursive invoice. Its conclusion is +that the extracted paid and productive target counts agree with a claim bound +to those exact sources. It is not a physical supplier or funding theorem. + +In particular, the h9 frame tariff and mixed-target Gaussian interpretation +are inherited interfaces. Caller stage labels denote independent formal Laurent +variables. The input does not contain a physical coordinate/tape embedding +that would establish those variables' realization at every size. The checker +therefore cannot validate a reused-coordinate realization merely by checking +the formal fresh-stage identity. Absolute phases, precision/tape lowering, +ordinary-work funding, the recursive compiler and analytic recovery remain +explicit unchecked obligations in every output. + +The contribution is a reusable independent source extractor and diagnostic +gate. Its calibrations are known results, not new discoveries or scientific +admission of pending work. It imports no author replay, pricing, relation +witness, declared histogram or PASS receipt to determine the invoice. + +## Native rows, frames and ownership + +At entry, each persistent L field and declared owned C field is an independent +formal variable. Owned L helpers likewise start arbitrary; they are not silently +initialized to zero. Main inputs may not be declared owned. The legacy original +schema admits only C0 as owned; successor schemas require explicit ownership. + +Each row is a finite rational map from (entry variable, reduced signed native +operator word) to its coefficient. Scalar ADD and SCALE implement exact rational +linear operations. CLEAR is allowed only on owned inputs. COPY requires a +cleared owned destination. At every scalar action, source and destination +frames must match the event's declared frame. Dyadic coefficient domains and +the inherited abstract real-scalar allowance are checked and recorded. + +A native warp prefixes its signed operator symbol and cancels an immediately +opposite prefix. Left multiplication in a free group is injective, so this +dictionary transformation cannot silently combine distinct keys. Backward +execution uses its own formal alphabet under the retained primitive-wise +conjugation ABI; it is not inferred by reversing or taking an adjoint of the +forward program. Exact sparse propagation checks all independent entry columns +simultaneously. No test input vector substitutes for this identity. + +Binary frame bases are validated for independence by complete span generation. +Every declared binary G map is checked invertible. At each warp occurrence, +its actual signed map must carry the complete current frame subspace exactly +onto the declared output frame subspace. A discrepancy rejects as an unpriced +native residual. This checks the G_columns representation supplied by the word; +it does not derive a unitary's absolute phase or independently authenticate a +different physical implementation of those columns. + +For every climb or centre, actual old/new frame subspaces must be strictly +nested, and the charged rank is recomputed as the difference of their basis +dimensions. The record's rank must agree. Paid events get source orientation, +event index, role, old frame, new frame and independently derived rank. +The recursive transport changes the frame in this retained symbolic protocol; +its physical Gaussian implementation remains an inherited tariff obligation. + +An uncharged zero-retag is allowed only when the entire current row is exactly +zero, including every arbitrary owned entry column. The final frame vector must +match the source return contract. Every borrowed helper returns its independent +identity row, each main row returns the prescribed signed shear, and all owned +rows return zero. Entry/exit adapter markers must occur exactly once for each +main input and agree with its endpoint frames. Phase-section markers are checked +as annotations; they are not a native phase proof. + +For each helper i, its productive rank is derived from its actual start/final +frames. It earns one target only if borrowed, strictly ascending and returned +as an independent identity. Owned helpers earn none even if their frame labels +match borrowed helpers. Their surrendered target ranks are retained explicitly +in the audit. Thus the credit rule follows the checked endpoint/ownership ABI, +not a declared helper histogram or a count of physical output fields. + +The fixed caller tariff also requires its native main endpoint contract. Ports +must be distinct nonzero odd-parity h-bit vectors p_i. The first main bank must +start on span(p_i) and end at the full h-space; the second must start at zero +and end on the p_i-orthogonal hyperplane. These exact subspaces are checked, +not merely their net dimensions. A further paid main climb and updated adapter +cannot silently inherit the old rank1+8-times-stages target interpretation. + +## Caller identity and recursive composition + +For a caller with 2p rows and 2p+1 stages, use one Laurent exponent for A and +one for every stage R_j. Execute each left/right scalar boundary program on +an identity matrix over exact rationals; require agreement with its separately +declared matrix. Initialize the Laurent rows from the computed right matrix. + +LOCAL and QUERY_SHEAR apply their oriented elementary A shear. LOCAL then +multiplies both rows by its R_j. IDLE multiplies both selected rows by precisely +the listed distinct stage product. ADD, SWAP and SIGNED_SWAP act literally. +Every stage must occur exactly once as LOCAL or QUERY_SHEAR. Finally apply the +computed left boundary matrix. Require zero off-diagonal entries and exactly +one coefficient-one monomial in every diagonal cell. Its exponents must have +A exponent ±1 and every R exponent in {0,1}; compare this derived diagonal with +the declaration only after computing it. + +Induction on each source instruction proves that these sparse Laurent rows are +the exact formal caller matrix. The complete coefficient identity is finite +and exact; it makes no claim that a proposed physical caller realizes fresh +independent stages or commutes in the required way. + +For the explicitly supported p16/a7 h9/v112 tariff: + +* Each LOCAL contributes its actual oriented native paid events and credited + helper targets once. Its source caller event ID is retained. +* Each QUERY_SHEAR contributes v=112 rank-one calls. +* Each IDLE with t distinct listed stages contributes 2v=224 calls of rank 8t. +* Each derived main diagonal contributes v=112 targets of rank 1+8 times the + number of R exponents, using the inherited Gaussian-product interpretation. + +These are the retained caller's tariff/ownership rules, not newly proved +physical implementations. A different ABI must use a reviewed adapter rather +than inherit these labels. Ambient rank, pairs, prefix count, native dimensions +and canonical endpoint shapes are checked before a result gets this contract. + +Every recursive charge appears in one disjoint category: an actual local event +at an actual LOCAL call site, an outer query, or an outer idle. Every target is +a credited local helper or a derived main target. Local events are stored once +per orientation with their complete call-site ID list. Expanding this factored +ledger yields precisely the same multiset as enumerating each call separately. +Summing ranks/counts is therefore a complete recursive census of this symbolic +protocol. Ordinary scalar, boundary, native-map and adapter records remain in +the audit and require their separate physical/precision/funding evidence. + +## Claim binding and diagnostics + +The emitted preflight object includes both paid and target histograms. A checked +claim must contain the same contract and both canonical-JSON source hashes. +It cannot transfer between different recipes merely because their histograms +match. All source JSON is data, never executable code. Duplicate keys, floating +point/nonfinite values, noncanonical rank keys, Boolean counts and unsupported +schemas/operations reject. Rational strings accept bounded integer/ratio syntax, +not exponent notation. Explicit input/table/term bounds limit this implementation's +supported domain; these are tool limits, not mathematical impossibility claims. + +Canonical hashes identify compact sorted-key JSON, excluding trailing newlines. +Raw gzip/decompressed byte hashes serve a separate export-provenance role. +The audit additionally names the native/caller/CLI code hashes. The complete +recursive-ledger hash covers local groups, outer queries/idles and main targets. +These hashes identify what was checked; reviewer trust in the code and the +unchecked scientific obligations are not derived from a hash comparison. + +New output files are explicit opt-ins and refuse overwrite. Extraction without +an expected claim is labeled EXTRACTED_RECURSIVE_INVOICE; a successful expected +claim match is labeled PASS_SOURCE_INVOICE_CONFORMANCE. Neither label grants +funding, admission, publication or a selected-frontier transition. + +## Corroboration and limits + +The three source calibrations compare independently extracted invoices with +the separately retained producer claim fields. Original selected-word input +has 64404 paid / 10928 productive; both owned successors have 64148/10800. +The unchanged caller has 2 forward and 16 backward LOCAL calls. Eight owned +backward helper inputs thus surrender 128 H9 targets. Omitting that debit is +detected per rank even if the paid side is unchanged. + +The two successors have the same recursive invoice but different prepared +programs, owned pivots, scalar allowances and canonical source hashes. Their +backward scalar allowances 158744 and 158776 differ by 32. The stale-source +control rejects transferring one claim to the other. This is an executable +distinction, not an assumption that same histograms transfer physical evidence. + +The control suite changes actual programs, source frames, maps, ownership, +boundary programs, orientations, idles and diagonal declarations. Other controls +change invoice bins with equal rank mass, omit queries/idles/target debits, +or introduce unknown operations and malformed input. Poisoning author profile +annotations leaves the computed counts unchanged, showing that extraction does +not merely validate the hash of a declared invoice. No predecessor pricing +engine, compiler, native phase suite, selected cold replay, Lean or Docker +is executed by this package. + +This written argument establishes the finite interpreter's symbolic protocol +and census. It does not replace a production all-size embedding, absolute phase, +precision/storage/movement proof or the complete multiplication theorem. +Substantial OpenAI Codex assistance; source/contributor credit is in README.md. diff --git a/research/source-invoice-conformance/README.md b/research/source-invoice-conformance/README.md new file mode 100644 index 0000000000..a17a6bddf6 --- /dev/null +++ b/research/source-invoice-conformance/README.md @@ -0,0 +1,131 @@ +# Extract recursive invoices from actual word and caller sources + +This opt-in checker derives the recursive paid/target invoice from the literal +native word, its ownership contract and the literal p16/a7 caller. It does not +read author pricing functions, declared native paid profiles or caller invoice +tables to decide what to charge. A source-bound claim is compared against the +extracted result, with an event ledger for every bin. + +The current [#5383](https://github.com/CrocSwap/integer-mult-bounds/pull/5383) +and [#5387](https://github.com/CrocSwap/integer-mult-bounds/pull/5387) words both +produce **64148 paid calls / 10800 productive targets**, including 128 lost H9 +helper credits. Their backward scalar allowances are **158744 and 158776**, +respectively. Equal recursive histograms therefore do not identify their +implementations or ordinary costs. The checker preserves both differences. + +The original selected-word calibration produces 64404 paid / 10928 targets. +All three exact histograms match separately retained author claim data. +This is independent extraction and symbolic protocol checking, not a new +construction, discovery of those known deltas or selected-frontier update. + +## Use on a new recipe + +Python 3.12, standard library only. Export the literal word and caller in the +supported schemas; no predecessor evaluator is imported. + +```sh +python3.12 -I -B research/source-invoice-conformance/conform.py \ + --word path/to/WORD.json.gz --controller path/to/CONTROLLER.json \ + --write-invoice /tmp/extracted-invoice.json \ + --write-audit /tmp/source-event-audit.json \ + --write-claim /tmp/proposed-invoice-claim.json +``` + +The first run reports `EXTRACTED_RECURSIVE_INVOICE`. Review the proposed claim +and compare it with the intended pricing input. To check an existing claim, +add `--expect path/to/CLAIM.json`; a successful match reports +`PASS_SOURCE_INVOICE_CONFORMANCE`, and mismatches exit nonzero with per-rank +claimed/extracted counts. Output paths refuse to overwrite existing files. +For example, an omitted debit reports `targets H9: claimed 5868, extracted 5740`. + +The invoice output uses the signed preflight schema of +[#5397](https://github.com/CrocSwap/integer-mult-bounds/pull/5397). The audit +contains actual native event IDs, actual caller call IDs, explicit surrendered +targets, outer query/idle charges, derived main targets, scalar/native/adapter +obligations and exact source/checker hashes. Local templates and call-site +lists factor repeated events without losing multiplicity. The complete +recursive-ledger hash includes local, outer and main contributions. + +The claim format is `source-invoice-claim/v1`: `source_binding` holds the SHA256 +of canonical compact JSON for the word and caller, and `invoice` holds the full +preflight object. Canonical hashes exclude whitespace and the final newline; +they are different from raw decompressed-payload or gzip hashes. No algorithm +executes source-supplied Python. JSON rejects duplicate keys and floating-point +numbers; rational strings use bounded integer/ratio notation. Supported table +and symbolic-term limits are explicit in the interpreters. + +## What the pass establishes + +[PROOF.md](PROOF.md) specifies the interpretation and accounting argument. + +* Exact sparse rows check every borrowed main/helper endpoint, owned erasure, + CLEAR/COPY ownership, and every zero-retag's full zero row. +* Binary subspace images check each declared native map's frame transport; + paid ranks are independently derived from nested frame dimensions. +* Exact Laurent replay executes both scalar boundary programs and all caller + events, checks every stage occurrence and derives the whole diagonal. +* Actual LOCAL orientations multiply local event ledgers. Query/whole-idle + calls and main targets are derived directly from the caller. Owned helper + inputs earn no autonomous target credit. + +This is **symbolic source-protocol and recursive-invoice conformance**. The +caller stage labels are independent formal variables; the input format does +not supply a proof of their physical fresh-stage/coordinate embedding. Absolute +native phase, precision/tape implementation, ordinary-work funding, recursive +compiler and analytic recovery remain separate, explicit report obligations. +The checker does not independently resolve the physical-reference/embedding +failure classes discussed in +[#5349](https://github.com/CrocSwap/integer-mult-bounds/pull/5349) and +[#5380](https://github.com/CrocSwap/integer-mult-bounds/pull/5380). + +The compatibility/funding oracle in +[#5391](https://github.com/CrocSwap/integer-mult-bounds/pull/5391) consumes trusted +independent evidence. This package supplies a preceding source-extraction tool; +it does not replace that oracle, its reviewer policy or its scientific engines. +Hashes identify artifacts and code, not the truth of an unchecked physical claim. + +## Reproduce the calibrations + +```sh +python3.12 -B scripts/research_package.py --package research/source-invoice-conformance --check-only +python3.12 -B scripts/research_package.py --package research/source-invoice-conformance +python3.12 -B scripts/check_research_commit.py --package research/source-invoice-conformance +``` + +Normal and optimized checks compare the full typed RESULT.json. `verify.py +--emit` prints a fresh receipt without changing the committed one. Three +complete source calibrations, 24 semantic/interface controls and a full CLI +round trip exercise the tool. [EVIDENCE.md](EVIDENCE.md) records exact source +pins, provenance, environment, coverage and unrun obligations. + +## Open next questions + +1. Bind a generated physical caller's coordinate/tape maps to these formal + stages. Start with one actual LOCAL/IDLE transition; embedding and absolute + native phase remain required before any physical supplier conclusion. +2. Emit this source ledger directly from a current generator and add a consumer + to the evidence oracle under a separately reviewed policy. The first step + is byte-bound recipe export; a generator's own histogram is insufficient. +3. Add another ownership/target ABI only after stating its endpoint contract. + Coupled helper outputs require an explicit new adapter, not autonomous + target credit inferred from their count or rank. + +## Attribution + +[@intqwq](https://github.com/intqwq) supplied the selected native word in +[#4610](https://github.com/CrocSwap/integer-mult-bounds/pull/4610), +[@aliromman](https://github.com/aliromman) supplied the changed owned-relation +word in [#5383](https://github.com/CrocSwap/integer-mult-bounds/pull/5383), +and [@Dugongue](https://github.com/Dugongue) supplied the successor in +[#5387](https://github.com/CrocSwap/integer-mult-bounds/pull/5387). +[@Clear1nsight](https://github.com/Clear1nsight)'s +[#5241](https://github.com/CrocSwap/integer-mult-bounds/pull/5241) and +[#5391](https://github.com/CrocSwap/integer-mult-bounds/pull/5391) retain their +independent admission/oracle credit. The source schemas, formal-row convention, +caller, dyadic allowance and mixed-target tariff retain Cinna Davis, zxv, +Jacob Alan Sussman, the native Clifford/controller/analytic/ordinary-BIT lineage +and original contributor credit. This independent tool imports none of the +producer engines. New implementation by [@zxv](https://github.com/zxv), with +substantial OpenAI Codex assistance in code, source analysis and assisted review. +Review shares source context; no independent human or formal-kernel acceptance +is claimed. Apache-2.0. diff --git a/research/source-invoice-conformance/RESOURCE.json b/research/source-invoice-conformance/RESOURCE.json new file mode 100644 index 0000000000..4f44991e56 --- /dev/null +++ b/research/source-invoice-conformance/RESOURCE.json @@ -0,0 +1,13 @@ +{ + "exit_code": 0, + "elapsed_seconds": 24.793, + "peak_descendant_rss_kib": 290704, + "resource_stop": null, + "command": [ + "/opt/local/bin/python3.12", + "-B", + "scripts/research_package.py", + "--package", + "research/source-invoice-conformance" + ] +} diff --git a/research/source-invoice-conformance/RESULT.json b/research/source-invoice-conformance/RESULT.json new file mode 100644 index 0000000000..d4bc4b1a8b --- /dev/null +++ b/research/source-invoice-conformance/RESULT.json @@ -0,0 +1,438 @@ +{ + "calibrations": { + "PR4610": { + "checker_code_sha256": { + "caller_invoice.py": "249b448b1961ec2a784531e63d1f427d73be98a71850e63e7ceb6b5cc94a9f09", + "conform.py": "b3686f6c8551b3cbc2767a2f366f924716d3972d75fb48bf7d104fb1e2857927", + "native_invoice.py": "48e7be042c862855c6da823db988cdc8497412d692fea1586e12036a45e89638" + }, + "complete_factored_ledger_sha256": "4f3d1ef9e6d77c7a6cedda12c323d45d78c3fa58f1db8eef8d6c1b372ad358b6", + "invoice": { + "contract": { + "ambient_rank": 145, + "boundary": "complete p16/a7 unit before the retained mixed-target compiler", + "model": "mixed-target-unnormalized-power-v1", + "rank_semantics": "H_r has raw tariff r^(1-C), with surrendered productive fields debited" + }, + "paid": { + "1": 41298, + "16": 448, + "2": 7416, + "24": 448, + "3": 9180, + "32": 448, + "4": 2286, + "40": 448, + "48": 448, + "5": 720, + "56": 448, + "64": 448, + "72": 224, + "8": 144 + }, + "schema": "integer-mult-recursive-invoice/v1", + "targets": { + "145": 224, + "17": 448, + "25": 448, + "33": 448, + "4": 504, + "41": 448, + "49": 448, + "57": 448, + "65": 448, + "7": 126, + "73": 224, + "8": 846, + "9": 5868 + } + }, + "local": { + "backward": { + "helpers": { + "4": 28, + "7": 7, + "8": 47, + "9": 326 + }, + "paid": { + "1": 2201, + "2": 412, + "3": 510, + "4": 127, + "5": 40, + "8": 8 + }, + "scalar_allowance": 158168 + }, + "forward": { + "helpers": { + "4": 28, + "7": 7, + "8": 47, + "9": 326 + }, + "paid": { + "1": 2201, + "2": 412, + "3": 510, + "4": 127, + "5": 40, + "8": 8 + }, + "scalar_allowance": 158120 + } + }, + "native_audit_sha256": "321bb92e77bc483a4a96a212fe530cacc58306bd8abbb3b77961719aeb67ca44", + "orientations": { + "backward": 16, + "forward": 2 + }, + "source_binding": { + "controller_canonical_sha256": "80dabeec6ea2ccd0a41e3cbb3f99674cff5b44cb64e846186e1d006f5871aa3c", + "word_canonical_sha256": "cfcd36b40326d7a5815e1db5313444379b3fb756b27d5201c561574c085cc0dd" + }, + "status": "PASS_SOURCE_INVOICE_CONFORMANCE", + "surrendered_target_ledger": {}, + "totals": { + "paid": 64404, + "rank_surplus": 752, + "targets": 10928 + }, + "unchecked_obligations": [ + "native_absolute_phase", + "precision_and_tape_implementation", + "physical_fresh_stage_and_coordinate_embedding", + "ordinary_cost_funding", + "recursive_compiler", + "analytic_recovery", + "publication_and_selected_status" + ] + }, + "PR5383": { + "checker_code_sha256": { + "caller_invoice.py": "249b448b1961ec2a784531e63d1f427d73be98a71850e63e7ceb6b5cc94a9f09", + "conform.py": "b3686f6c8551b3cbc2767a2f366f924716d3972d75fb48bf7d104fb1e2857927", + "native_invoice.py": "48e7be042c862855c6da823db988cdc8497412d692fea1586e12036a45e89638" + }, + "complete_factored_ledger_sha256": "709b41e9037e761c2c6f4bf21e376b894c720e8812f038842ee031d074065cc3", + "invoice": { + "contract": { + "ambient_rank": 145, + "boundary": "complete p16/a7 unit before the retained mixed-target compiler", + "model": "mixed-target-unnormalized-power-v1", + "rank_semantics": "H_r has raw tariff r^(1-C), with surrendered productive fields debited" + }, + "paid": { + "1": 41170, + "16": 448, + "2": 7416, + "24": 448, + "3": 9180, + "32": 448, + "4": 2286, + "40": 448, + "48": 448, + "5": 720, + "56": 448, + "64": 448, + "72": 224, + "8": 16 + }, + "schema": "integer-mult-recursive-invoice/v1", + "targets": { + "145": 224, + "17": 448, + "25": 448, + "33": 448, + "4": 504, + "41": 448, + "49": 448, + "57": 448, + "65": 448, + "7": 126, + "73": 224, + "8": 846, + "9": 5740 + } + }, + "local": { + "backward": { + "helpers": { + "4": 28, + "7": 7, + "8": 47, + "9": 318 + }, + "paid": { + "1": 2193, + "2": 412, + "3": 510, + "4": 127, + "5": 40 + }, + "scalar_allowance": 158744 + }, + "forward": { + "helpers": { + "4": 28, + "7": 7, + "8": 47, + "9": 326 + }, + "paid": { + "1": 2201, + "2": 412, + "3": 510, + "4": 127, + "5": 40, + "8": 8 + }, + "scalar_allowance": 158120 + } + }, + "native_audit_sha256": "c702be3469b7be328faf84f5e3be2d719dffcb1f27cc3e1805f450054678a12e", + "orientations": { + "backward": 16, + "forward": 2 + }, + "source_binding": { + "controller_canonical_sha256": "80dabeec6ea2ccd0a41e3cbb3f99674cff5b44cb64e846186e1d006f5871aa3c", + "word_canonical_sha256": "86a9f0b429e73185f63ecc41afd40b13d33108fa5056e6d6d499a07d249bba58" + }, + "status": "PASS_SOURCE_INVOICE_CONFORMANCE", + "surrendered_target_ledger": { + "9": 128 + }, + "totals": { + "paid": 64148, + "rank_surplus": 752, + "targets": 10800 + }, + "unchecked_obligations": [ + "native_absolute_phase", + "precision_and_tape_implementation", + "physical_fresh_stage_and_coordinate_embedding", + "ordinary_cost_funding", + "recursive_compiler", + "analytic_recovery", + "publication_and_selected_status" + ] + }, + "PR5387": { + "checker_code_sha256": { + "caller_invoice.py": "249b448b1961ec2a784531e63d1f427d73be98a71850e63e7ceb6b5cc94a9f09", + "conform.py": "b3686f6c8551b3cbc2767a2f366f924716d3972d75fb48bf7d104fb1e2857927", + "native_invoice.py": "48e7be042c862855c6da823db988cdc8497412d692fea1586e12036a45e89638" + }, + "complete_factored_ledger_sha256": "b3e0d56e5cc3b24d524c3d37d7b6e17e73f10236f12b0de6ac29b9b28c0bb0d1", + "invoice": { + "contract": { + "ambient_rank": 145, + "boundary": "complete p16/a7 unit before the retained mixed-target compiler", + "model": "mixed-target-unnormalized-power-v1", + "rank_semantics": "H_r has raw tariff r^(1-C), with surrendered productive fields debited" + }, + "paid": { + "1": 41170, + "16": 448, + "2": 7416, + "24": 448, + "3": 9180, + "32": 448, + "4": 2286, + "40": 448, + "48": 448, + "5": 720, + "56": 448, + "64": 448, + "72": 224, + "8": 16 + }, + "schema": "integer-mult-recursive-invoice/v1", + "targets": { + "145": 224, + "17": 448, + "25": 448, + "33": 448, + "4": 504, + "41": 448, + "49": 448, + "57": 448, + "65": 448, + "7": 126, + "73": 224, + "8": 846, + "9": 5740 + } + }, + "local": { + "backward": { + "helpers": { + "4": 28, + "7": 7, + "8": 47, + "9": 318 + }, + "paid": { + "1": 2193, + "2": 412, + "3": 510, + "4": 127, + "5": 40 + }, + "scalar_allowance": 158776 + }, + "forward": { + "helpers": { + "4": 28, + "7": 7, + "8": 47, + "9": 326 + }, + "paid": { + "1": 2201, + "2": 412, + "3": 510, + "4": 127, + "5": 40, + "8": 8 + }, + "scalar_allowance": 158120 + } + }, + "native_audit_sha256": "d3b136ff2f7bb50c449329320257bf8f18fc6a8c081ed883c1864e57a0c9149c", + "orientations": { + "backward": 16, + "forward": 2 + }, + "source_binding": { + "controller_canonical_sha256": "80dabeec6ea2ccd0a41e3cbb3f99674cff5b44cb64e846186e1d006f5871aa3c", + "word_canonical_sha256": "4d679409264d24264bd8d3121f39dce86b98a4faebce6fde8af2ec1ff13d5545" + }, + "status": "PASS_SOURCE_INVOICE_CONFORMANCE", + "surrendered_target_ledger": { + "9": 128 + }, + "totals": { + "paid": 64148, + "rank_surplus": 752, + "targets": 10800 + }, + "unchecked_obligations": [ + "native_absolute_phase", + "precision_and_tape_implementation", + "physical_fresh_stage_and_coordinate_embedding", + "ordinary_cost_funding", + "recursive_compiler", + "analytic_recovery", + "publication_and_selected_status" + ] + } + }, + "cli": { + "audit_sha256": "2c934b55ca50435e6e21bfa714de1db228455f8143a0d115f2184b8a6855029b", + "invoice_sha256": "84a12932912a43d95107c5fe844c910499b5791bb356fe56ac176d56030e7b40", + "status": "PASS_SOURCE_INVOICE_CONFORMANCE" + }, + "controls": [ + { + "control": "omitted_128_owned_helper_debits", + "rejection": "Invoice mismatch: targets H9: claimed 5868, extracted 5740" + }, + { + "control": "stale_paid_rank8", + "rejection": "Invoice mismatch: paid H8: claimed 144, extracted 16" + }, + { + "control": "omitted_query_calls", + "rejection": "Invoice mismatch: paid H1: claimed 39490, extracted 41170" + }, + { + "control": "omitted_whole_idles", + "rejection": "Invoice mismatch: paid H16: claimed 0, extracted 448" + }, + { + "control": "equal_rank_mass_wrong_profile", + "rejection": "Invoice mismatch: paid H1: claimed 41154, extracted 41170; paid H2: claimed 7424, extracted 7416" + }, + { + "control": "same_invoice_stale_word_binding", + "rejection": "Claim source binding differs from the extracted literal word/caller" + }, + { + "control": "boolean_count_is_not_integer", + "rejection": "Claim rank/count must be exact nonnegative integers" + }, + { + "control": "misstated_actual_paid_rank", + "rejection": "forward event 6276: paid rank differs from independently derived frame rank" + }, + { + "control": "unpriced_native_frame_residual", + "rejection": "forward event 6275: native map has an unpriced residual between its actual input and output frames" + }, + { + "control": "false_zero_retag", + "rejection": "forward event 6276: uncharged zero-retag requires an identically zero full symbolic row" + }, + { + "control": "wrong_preparation_sign", + "rejection": "backward: symbolic return mismatch for ['L', 0]" + }, + { + "control": "undeclared_owned_input_clear", + "rejection": "backward event 0: CLEAR may erase only declared owned input" + }, + { + "control": "unknown_native_operation", + "rejection": "forward event 0: unknown event opcode unpriced_magic" + }, + { + "control": "changed_literal_idle", + "rejection": "Caller off-diagonal residual 8,9" + }, + { + "control": "changed_literal_orientation", + "rejection": "Caller off-diagonal residual 8,24" + }, + { + "control": "wrong_main_diagonal", + "rejection": "Caller literal/declared diagonal mismatch" + }, + { + "control": "unknown_caller_operation", + "rejection": "caller event 0: Known caller opcode" + }, + { + "control": "boundary_program_mismatch", + "rejection": "Boundary right program/matrix mismatch" + }, + { + "control": "unknown_source_schema", + "rejection": "unsupported explicit native-word schema or missing owned contract" + }, + { + "control": "changed_main_endpoint_tariff", + "rejection": "unsupported native boundary at main pair 0: second bank must be zero to the port-orthogonal hyperplane" + }, + { + "control": "symbolic_word_growth_limit", + "rejection": "forward event 4097: unsupported symbolic replay domain: free word exceeds 4096 operators" + }, + { + "control": "duplicate_json_keys", + "rejection": "Duplicate JSON key: a" + }, + { + "control": "floating_point_input", + "rejection": "Exact integer/rational source JSON required: 1.0" + }, + { + "control": "exponent_rational_notation", + "rejection": "Rational must use bounded integer or integer/positive-integer spelling" + } + ], + "scope": "Source-protocol and recursive invoice conformance; separate ordinary costs, phase, precision/tape, compiler and analytic obligations remain.", + "status": "PASS_SOURCE_INVOICE_CONFORMANCE_SUITE" +} diff --git a/research/source-invoice-conformance/SOURCES.json b/research/source-invoice-conformance/SOURCES.json new file mode 100644 index 0000000000..043dcd1a72 --- /dev/null +++ b/research/source-invoice-conformance/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "1ec1119972c9aefe42525172d07b332fcff81cb4", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b288ae44032fd84dd5564243422836cbcd29835e", + "sha256": "f9ed52bb642cd1e1486cf2743557ac5fa23cf1514a3277d786a644e39a565038" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/kappa-round3-warp-20261022/ACTUAL-WORD.json.gz", + "usage": "provenance", + "git_blob": "46d929df83817b85a5387bcdb9745e0627d6366e", + "sha256": "7679daa4ec6a40f56fc7f0202379a6f454310e94945aba4f48beaaaafb838d05" + }, + { + "path": "research/joint-helper-lattice/CONTROLLER.json", + "usage": "provenance", + "git_blob": "49a2f0675819f9deeea27ed77be2c2b6ff2e87e5", + "sha256": "1f5d6aa267e4e66048818714b5d3b5eae17a58abe91d15deeaa34574f7391a5f" + }, + { + "path": "research/kappa-round6-compiler-tightening-20261022/ARITHMETIC.json", + "usage": "provenance", + "git_blob": "0fdb65f946d557c13d8e2781b9151e2a8ddee5c3", + "sha256": "b4f720a7ccbb5b46e472eaf85dc8739a40598986f19b37d26c4f9ecfbd31f0de" + } + ] +} diff --git a/research/source-invoice-conformance/TASK.json b/research/source-invoice-conformance/TASK.json new file mode 100644 index 0000000000..1236ed66e8 --- /dev/null +++ b/research/source-invoice-conformance/TASK.json @@ -0,0 +1,105 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 7, + "base_commit": "1ec1119972c9aefe42525172d07b332fcff81cb4", + "original_card": { + "id": "independent-moment", + "question": "Does a new paid-profile or mixture-ceiling claim have independent source-bound coverage of its actual changed ledger?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/staged544-mixed-fourth-entry/README.md", + "research/staged-fourth-mixture-ceiling/README.md", + "research/r437-two-window-carrier/README.md" + ], + "methods": [ + "Independently reconstruct one changed paid ledger or pooled dual with exact source and model binding.", + "Check a genuinely uncovered moment implication with a different enclosure method and semantic controls." + ], + "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_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Choose one uncovered implication in #4088 literal mixed fill, #4091 pooled dual/model binding or #4067 changed frame/host bill. #4091 pins an earlier #4088 head: validate word, capacity and stock equivalence before applying that ceiling to the later fill.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Independently reconstruct one changed ledger or pooled certificate with a positive case and a semantic failure control. Compare exact sources and name what existing checks miss. Keep this separate from supplier-boundary-audit (ordinary/outer dispatch) and uniform-transfer-audit (all-size proof). Stop after the chosen implication; more digits of an unchanged root are not additional mechanism coverage.", + "bottleneck_link": "Independent pricing prevents unsupported frontier claims and can reveal genuine accounting slack.", + "allowed_variations": [ + "Reconstruct either a source ledger or a numeric enclosure with a different method." + ], + "scope_change_triggers": [ + "Importing the primary function and calling its output independent verification.", + "Calling an aggregate histogram or source archive an independently accepted physical supplier." + ], + "overlap_terms": [ + "independent moment", + "rank histogram", + "exact enclosure", + "2979", + "rank7 joint endframes", + "paired extraction", + "joint lowering", + "4088", + "4091", + "4067", + "staged544-mixed-fourth-entry", + "staged-fourth-mixture-ceiling", + "r437-two-window-carrier" + ], + "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_status": "refined", + "actual_scope": "Reusable independent literal p16/a7 source-to-recursive-invoice extractor, symbolic conformance checker and event ledger.", + "scope_change_reason": "Explicit donor-assigned third sequential contribution; precede price compatibility with source-derived paid/target census, rather than recomputing another endpoint.", + "bottleneck_link": "Manual invoices can omit target debits or reuse a receipt from a different equal-histogram recipe.", + "stop_rule": "Complete this scoped tool, source calibrations and semantic controls; show local proposed PR and wait for donor confirmation before regular publication.", + "outcome": "completed", + "evidence": "PROOF.md protocol/census argument; RESULT.json three independently extracted source invoices,24 controls and fullCLIroundtrip; source/checker-bound audits.", + "author": "zxv with OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance in implementation, source interpretation, tests and separate assisted reviews sharing source context.", + "open_questions": [ + { + "question": "Can the formal stages be bound to actual physical fresh coordinates at every size?", + "why_it_matters": "A formal caller identity does not prove that a proposed physical embedding implements it.", + "first_step": "Bind one LOCAL/IDLE transition to its actual coordinate/tape maps and native phase receipt.", + "blocked_by": "Physical embedding, absolute phase, precision/tape and outer assumptions remain separate." + }, + { + "question": "Can current generators and the price oracle consume the source ledger directly?", + "why_it_matters": "A reviewed adapter could eliminate manual paid/target transcription.", + "first_step": "Export a literal recipe, run conformance, then add an explicit evidence-consumer policy for this source/code-bound report.", + "blocked_by": "Reviewer trust in the code, complete ordinary costs and full scientific evidence are not supplied by histogram or hash equality." + } + ] +} diff --git a/research/source-invoice-conformance/VERIFY.json b/research/source-invoice-conformance/VERIFY.json new file mode 100644 index 0000000000..b78e0dffd4 --- /dev/null +++ b/research/source-invoice-conformance/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Three complete literal source/claim calibrations; event/callsiteledger; exactsource mutations and24 controls; profileannotationpoisoning; fullCLIexports; typed deterministic receipt." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same independent native/caller extraction and semantic rejection controls with assertions disabled." + } + ] +} diff --git a/research/source-invoice-conformance/caller_invoice.py b/research/source-invoice-conformance/caller_invoice.py new file mode 100644 index 0000000000..fd0ee0ccbd --- /dev/null +++ b/research/source-invoice-conformance/caller_invoice.py @@ -0,0 +1,164 @@ +"""Independent literal caller/Laurent check and factored recursive ledger. + +No invoice tables or producer pricing/replay engines are used. Target arities +come from the extracted diagonal; local helper ownership comes from native +conformance. This is a source-protocol check, not a physical phase proof. +""" +from collections import Counter +from fractions import Fraction as Q +from hashlib import sha256 +import json +import re + + +def need(ok,message): + if not ok:raise ValueError(message) + + +def canonical(value):return json.dumps(value,sort_keys=True,separators=(',',':')).encode() + + +def integer(x,lo,hi):return type(x) is int and lo<=x<=hi + + +def rational(value): + need(type(value) in (int,str) and len(str(value))<=256,'Bounded exact rational') + need(re.fullmatch(r'[+-]?[0-9]+(?:/[1-9][0-9]*)?',str(value),flags=re.ASCII) is not None, + 'Rational must use bounded integer or integer/positive-integer spelling') + return Q(value) + + +def accumulate(dst,src,factor=Q(1),shift=None): + for key,value in src.items(): + if shift is not None:key=tuple(a+b for a,b in zip(key,shift)) + result=dst.get(key,Q(0))+factor*value + if result:dst[key]=result + else:dst.pop(key,None) + need(len(dst)<=32768,'Supported Laurent row term budget') + + +def boundary(data,side,n): + rows=[[Q(i==j) for j in range(n)] for i in range(n)] + program=data[side+'_program'] + need(type(program) is list and len(program)<=4096,'Supported boundary program') + for index,event in enumerate(program): + try: + op=event[0];i=event[1];need(integer(i,0,n-1),'Boundary destination') + if op=='SWAP': + need(len(event)==3 and integer(event[2],0,n-1),'Boundary SWAP shape') + rows[i],rows[event[2]]=rows[event[2]],rows[i] + elif op=='SCALE': + need(len(event)==3,'Boundary SCALE shape');q=rational(event[2]);need(q!=0,'Nonzero boundary SCALE') + rows[i]=[q*x for x in rows[i]] + else: + need(op=='ADD' and len(event)==4 and integer(event[2],0,n-1) and event[2]!=i,'Boundary ADD shape') + q=rational(event[3]);rows[i]=[a+q*b for a,b in zip(rows[i],rows[event[2]])] + except (ValueError,IndexError,TypeError,ZeroDivisionError) as error: + raise ValueError(f'boundary {side} event {index}: {error}') from error + declared=data[side] + need(type(declared) is list and len(declared)==n and all(type(row) is list and len(row)==n for row in declared),'Boundary matrix shape') + need(rows==[[rational(q) for q in row] for row in declared],f'Boundary {side} program/matrix mismatch') + return rows + + +def extract(controller,native): + need(type(controller) is dict and controller.get('kind')=='complex','Supported complex caller schema') + pairs=controller['pairs'];need(integer(pairs,1,32),'Supported caller pair count') + n=2*pairs;stages=n+1;width=stages+1;zero=(0,)*width + left=boundary(controller['boundaries'],'left',n);right=boundary(controller['boundaries'],'right',n) + rows=[[({zero:q} if q else {}) for q in row] for row in right] + physical=controller['physical_events'];need(type(physical) is list and len(physical)<=16384,'Supported caller event count') + used_stages=set();calls=[];outer_paid=[];ordinary=[];events=Counter() + v=native['v'];h=native['h'];need(integer(v,1,4096) and integer(h,2,16),'Supported native dimensions') + for index,event in enumerate(physical): + try: + need(type(event) is list and event,'Caller event record');kind=event[0];events[kind]+=1 + if kind in ('LOCAL','QUERY_SHEAR'): + need(len(event)==4,'Call event shape');_,stage,pair,back=event + need(integer(stage,0,stages-1) and stage not in used_stages,'Exactly one occurrence of each stage') + need(integer(pair,0,pairs-1) and type(back) is bool,'Pair and literal orientation') + used_stages.add(stage);x,y=2*pair,2*pair+1 + if back:x,y=y,x + shift=(1 if back else -1,)+(0,)*stages + for dst,src in zip(rows[y],rows[x]):accumulate(dst,src,Q(-1 if back else 1),shift) + if kind=='LOCAL': + direction='backward' if back else 'forward' + calls.append({'id':f'caller:{index}','event':index,'stage':stage,'pair':pair,'orientation':direction}) + shift=(0,)+tuple(int(j==stage) for j in range(stages)) + for role in (x,y): + rows[role]=[{tuple(a+b for a,b in zip(term,shift)):q for term,q in cell.items()} for cell in rows[role]] + else:outer_paid.append({'id':f'caller:{index}:query','event':index,'kind':'query','rank':1,'count':v}) + elif kind=='IDLE': + need(len(event)==3 and integer(event[1],0,pairs-1),'Idle shape') + subset=event[2] + need(type(subset) is list and subset and all(integer(j,0,stages-1) for j in subset) and len(set(subset))==len(subset),'Idle exact distinct stage subset') + shift=(0,)+tuple(int(j in subset) for j in range(stages)) + for role in (2*event[1],2*event[1]+1): + rows[role]=[{tuple(a+b for a,b in zip(term,shift)):q for term,q in cell.items()} for cell in rows[role]] + outer_paid.append({'id':f'caller:{index}:idle','event':index,'kind':'idle','rank':(h-1)*len(subset),'count':2*v}) + elif kind=='ADD': + need(len(event)==4 and integer(event[1],0,n-1) and integer(event[2],0,n-1) and event[1]!=event[2],'Caller ADD shape') + for dst,src in zip(rows[event[1]],rows[event[2]]):accumulate(dst,src,rational(event[3])) + ordinary.append({'event':index,'operation':event}) + else: + need(kind in ('SWAP','SIGNED_SWAP') and len(event)==3 and integer(event[1],0,n-1) and integer(event[2],0,n-1) and event[1]!=event[2],'Known caller opcode') + a,b=event[1:];old=rows[a];rows[a]=rows[b] + rows[b]=[{key:(-q if kind=='SIGNED_SWAP' else q) for key,q in cell.items()} for cell in old] + ordinary.append({'event':index,'operation':event}) + except (ValueError,IndexError,TypeError,KeyError,ZeroDivisionError) as error: + raise ValueError(f'caller event {index}: {error}') from error + need(used_stages==set(range(stages)),'Every caller stage is present exactly once') + result=[[{} for _ in range(n)] for _ in range(n)] + for i in range(n): + for k,q in enumerate(left[i]): + if q: + for j in range(n):accumulate(result[i][j],rows[k][j],q) + diagonal=[] + for i in range(n): + for j in range(n): + cell=result[i][j] + if i!=j:need(not cell,f'Caller off-diagonal residual {i},{j}') + else: + need(len(cell)==1 and next(iter(cell.values()))==1,f'Caller non-unit diagonal {i}') + term=next(iter(cell));need(term[0] in (-1,1) and all(x in (0,1) for x in term[1:]),'Whole Gaussian target exponents') + diagonal.append(list(term)) + need(diagonal==controller['diagonal'],'Caller literal/declared diagonal mismatch') + main=[{'id':f'caller:main:{i}','role':i,'rank':1+(h-1)*sum(term[1:]),'count':v,'exponents':term} + for i,term in enumerate(diagonal)] + paid=Counter();targets=Counter();orientations=Counter(c['orientation'] for c in calls) + local_groups=[] + for direction in ('forward','backward'): + local=native['orientations'][direction];call_ids=[c['id'] for c in calls if c['orientation']==direction] + for record in local['paid_events']: + rank=record['rank'];paid[rank]+=len(call_ids) + local_groups.append({'side':'paid','orientation':direction,'native_event':record['event'],'rank':rank,'count':len(call_ids),'call_ids':call_ids}) + for record in local['helper_targets']: + rank=record['target_rank'] + if record['credited']:targets[rank]+=len(call_ids) + local_groups.append({'side':'targets' if record['credited'] else 'surrendered_targets', + 'orientation':direction,'native_role':record['role'], + 'rank':rank,'count':len(call_ids),'call_ids':call_ids}) + for record in outer_paid:paid[record['rank']]+=record['count'] + for record in main:targets[record['rank']]+=record['count'] + ambient=controller['ambient_rank'] + need(integer(ambient,1,10**9) and max((*paid.keys(),*targets.keys()))<=ambient,'Ranks within caller ambient') + histogram=lambda counter:{str(r):n for r,n in sorted(counter.items()) if n} + invoice={'schema':'integer-mult-recursive-invoice/v1', + 'contract':{'model':'mixed-target-unnormalized-power-v1', + 'rank_semantics':'H_r has raw tariff r^(1-C), with surrendered productive fields debited', + 'ambient_rank':ambient,'boundary':'complete p16/a7 unit before the retained mixed-target compiler'}, + 'paid':histogram(paid),'targets':histogram(targets)} + # The supported caller is the actual p16/a7 interface. Other grammars need + # their own tariff/ownership adapter instead of inheriting this label. + need(pairs==16 and controller['prefix_pairs']==7 and h==9 and v==112 and ambient==145, + 'Supported source-certified p16/a7 tariff binding') + return {'schema':'source-caller-invoice/v1','controller_sha256':sha256(canonical(controller)).hexdigest(), + 'invoice':invoice,'orientations':dict(orientations),'calls':calls, + 'local_groups':local_groups,'outer_paid':outer_paid,'main_targets':main, + 'caller_event_counts':dict(events),'ordinary_caller_events':ordinary, + 'ordinary_boundary_events':[{'id':f'boundary:{side}:{index}','side':side,'event':index,'operation':operation} + for side in ('left','right') + for index,operation in enumerate(controller['boundaries'][side+'_program'])], + 'boundary_operation_counts':{side:len(controller['boundaries'][side+'_program']) for side in ('left','right')}, + 'totals':{'paid':sum(paid.values()),'targets':sum(targets.values()), + 'rank_surplus':sum(r*n for r,n in targets.items())-sum(r*n for r,n in paid.items())}} diff --git a/research/source-invoice-conformance/conform.py b/research/source-invoice-conformance/conform.py new file mode 100644 index 0000000000..56aa133a05 --- /dev/null +++ b/research/source-invoice-conformance/conform.py @@ -0,0 +1,144 @@ +#!/usr/bin/env python3 +"""Extract and check a p16/a7 recursive invoice from its literal source word. + +Example: + python3.12 -B conform.py --word WORD.json.gz --controller CONTROLLER.json \ + --expect CLAIM.json --write-invoice INVOICE.json --write-audit AUDIT.json + +Outputs are opt-in and refuse to overwrite files. A pass checks the symbolic +source protocol and invoice binding, not funding or complete supplier admission. +""" +import argparse +import gzip +from hashlib import sha256 +import json +from pathlib import Path +import sys + +HERE=Path(__file__).resolve().parent +sys.path.insert(0,str(HERE)) +import native_invoice +import caller_invoice + +MAX_BYTES=16*1024*1024 + + +def need(ok,message): + if not ok:raise ValueError(message) + + +def pairs(rows): + result={} + for key,value in rows: + need(key not in result,'Duplicate JSON key: '+key);result[key]=value + return result + + +def no_float(text):raise ValueError('Exact integer/rational source JSON required: '+text) + + +def bounded_integer(text): + need(len(text.lstrip('-'))<=256,'JSON integer exceeds supported 256 digits') + return int(text) + + +def parse(raw): + need(type(raw) is bytes and len(raw)<=MAX_BYTES,'Source JSON exceeds 16 MiB') + return json.loads(raw.decode('utf-8'),object_pairs_hook=pairs,parse_int=bounded_integer, + parse_float=no_float,parse_constant=no_float) + + +def read(path): + path=Path(path) + if path.suffix=='.gz': + with gzip.open(path,'rb') as stream:raw=stream.read(MAX_BYTES+1) + else: + with path.open('rb') as stream:raw=stream.read(MAX_BYTES+1) + return parse(raw) + + +def digest(value):return sha256(caller_invoice.canonical(value)).hexdigest() + + +def extract(word,controller): + need(type(word) is dict and type(word.get('canonical')) is dict and + type(word['canonical'].get('h')) is int and word['canonical']['h']==9 and + type(word['canonical'].get('v')) is int and word['canonical']['v']==112, + 'This caller adapter supports the literal h9/v112 native interface') + native=native_invoice.extract(word) + caller=caller_invoice.extract(controller,native) + binding={'word_canonical_sha256':digest(word),'controller_canonical_sha256':digest(controller)} + return {'schema':'source-invoice-audit/v1','source_binding':binding,'native':native,'caller':caller, + 'checker_code_sha256':{name:sha256((HERE/name).read_bytes()).hexdigest() + for name in ('native_invoice.py','caller_invoice.py','conform.py')}, + 'invoice':caller['invoice'], + 'unchecked_obligations':['native_absolute_phase','precision_and_tape_implementation', + 'physical_fresh_stage_and_coordinate_embedding', + 'ordinary_cost_funding','recursive_compiler','analytic_recovery', + 'publication_and_selected_status']} + + +def claim(audit): + return {'schema':'source-invoice-claim/v1','source_binding':audit['source_binding'],'invoice':audit['invoice']} + + +def compare(audit,expected): + need(type(expected) is dict and set(expected)=={'schema','source_binding','invoice'} and + expected['schema']=='source-invoice-claim/v1','Expected source-bound invoice claim schema') + need(caller_invoice.canonical(expected['source_binding'])==caller_invoice.canonical(audit['source_binding']), + 'Claim source binding differs from the extracted literal word/caller') + want=expected['invoice'];got=audit['invoice'] + need(type(want) is dict and set(want)=={'schema','contract','paid','targets'},'Expected complete paid-and-target invoice') + need(caller_invoice.canonical(want['schema'])==caller_invoice.canonical(got['schema']) and + caller_invoice.canonical(want['contract'])==caller_invoice.canonical(got['contract']), + 'Claim tariff/ownership boundary differs') + mismatches=[] + for side in ('paid','targets'): + need(type(want[side]) is dict,'Claim histogram must be an object') + for key,value in want[side].items(): + need(type(key) is str and key.isascii() and key.isdecimal() and key==str(int(key)) and + 1<=int(key)<=got['contract']['ambient_rank'] and type(value) is int and value>=0, + 'Claim rank/count must be exact nonnegative integers') + for rank in sorted(set(want[side])|set(got[side]),key=int): + if want[side].get(rank,0)!=got[side].get(rank,0): + mismatches.append(f'{side} H{rank}: claimed {want[side].get(rank,0)}, extracted {got[side].get(rank,0)}') + need(not mismatches,'Invoice mismatch: '+'; '.join(mismatches)) + return True + + +def summary(audit,checked=False): + caller=audit['caller'];native=audit['native'] + return {'status':'PASS_SOURCE_INVOICE_CONFORMANCE' if checked else 'EXTRACTED_RECURSIVE_INVOICE', + 'source_binding':audit['source_binding'],'invoice':audit['invoice'], + 'checker_code_sha256':audit['checker_code_sha256'], + 'totals':caller['totals'],'orientations':caller['orientations'], + 'local':{direction:{key:local[key] for key in ('paid','helpers','scalar_allowance')} + for direction,local in native['orientations'].items()}, + 'complete_factored_ledger_sha256':digest({key:caller[key] for key in ('local_groups','outer_paid','main_targets')}), + 'native_audit_sha256':digest(native),'unchecked_obligations':audit['unchecked_obligations']} + + +def write_new(path,value): + with Path(path).open('x',encoding='utf-8') as target:target.write(json.dumps(value,indent=2,sort_keys=True)+'\n') + + +def main(): + parser=argparse.ArgumentParser(description=__doc__) + parser.add_argument('--word',type=Path,required=True) + parser.add_argument('--controller',type=Path,required=True) + parser.add_argument('--expect',type=Path) + parser.add_argument('--write-invoice',type=Path) + parser.add_argument('--write-audit',type=Path) + parser.add_argument('--write-claim',type=Path,help='Emit a proposed source-bound claim for review; does not fund it') + args=parser.parse_args() + audit=extract(read(args.word),read(args.controller)) + if args.expect:compare(audit,read(args.expect)) + for path,value in ((args.write_invoice,audit['invoice']),(args.write_audit,audit),(args.write_claim,claim(audit))): + if path:write_new(path,value) + print(json.dumps(summary(audit,args.expect is not None),indent=2,sort_keys=True)) + + +if __name__=='__main__': + try:main() + except (ValueError,KeyError,IndexError,TypeError,RecursionError,UnicodeError,OSError,EOFError) as error: + print('SOURCE_INVOICE_REJECTED: '+str(error),file=sys.stderr);raise SystemExit(1) diff --git a/research/source-invoice-conformance/native_invoice.py b/research/source-invoice-conformance/native_invoice.py new file mode 100644 index 0000000000..579e4e1138 --- /dev/null +++ b/research/source-invoice-conformance/native_invoice.py @@ -0,0 +1,377 @@ +#!/usr/bin/env python3 +"""Independently extract an invoice from the literal retained native-word schema. + +No author evaluator, price module, declared paid profile, relation witness or +receipt is executed. Exact sparse rows establish symbolic endpoint and zero-row +conformance; binary subspaces establish the charged ranks and uncharged native +frame transports. Absolute phases, physical precision and supplier admission +remain separate obligations. + +The schema and free-word convention come from Cao Yifan's PR4610 word and the +retained Cinna Davis/zxv native lineage. Ali Romman supplied PR5383's changed +word; Dugongue supplied PR5387's successor. Independently implemented with +substantial OpenAI Codex assistance. Apache-2.0. +""" +from collections import Counter +from fractions import Fraction +from hashlib import sha256 +import json + + +Q = Fraction +SCHEMA = 'native-word-source-invoice/v1' +PHASES = ['zero_frame_precondition', 'entry_adapters', 'A', 'centers', 'B', + 'cleanup_tail', 'final', 'exit_adapters', 'full_frame_cleanup', 'done'] +MAX_ROW_TERMS = 4096 +MAX_WORD_LENGTH = 4096 +MAX_COEFFICIENT_BITS = 4096 + + +def _need(ok, why): + if not ok: + raise ValueError(why) + + +def _integer(value, why): + _need(type(value) is int, why) + return value + + +def _digest(value): + return sha256(json.dumps(value, sort_keys=True, separators=(',', ':'), + ensure_ascii=True).encode()).hexdigest() + + +def _role(value, fields): + _need(type(value) in (list, tuple) and len(value) == 2, 'role must be [L|C,index]') + kind, index = value + _integer(index, 'role index must be an integer') + _need(kind in ('L', 'C') and 0 <= index <= 1000000, 'unsupported role') + _need(kind != 'L' or index < fields, 'persistent role outside declared inputs') + return kind, index + + +def _span(basis, h): + _need(type(basis) is list and len(basis) <= h, 'binary frame basis') + result = {0} + for vector in basis: + _integer(vector, 'binary frame coordinate must be an integer') + _need(0 <= vector < 1 << h and vector not in result, 'dependent or invalid binary frame basis') + result |= {value ^ vector for value in tuple(result)} + return frozenset(result) + + +def _binary_image(value, columns): + result = 0 + for index, column in enumerate(columns): + if value >> index & 1: + result ^= column + return result + + +def _add(destination, source, coefficient): + for key, value in source.items(): + value = destination.get(key, Q(0)) + coefficient * value + if value: + destination[key] = value + else: + destination.pop(key, None) + + +def _guard_row(row): + """Bound this explicit symbolic backend, without rejecting the mathematics.""" + _need(len(row) <= MAX_ROW_TERMS, + 'unsupported symbolic replay domain: row exceeds 4096 terms') + for (_, word), coefficient in row.items(): + _need(len(word) <= MAX_WORD_LENGTH, + 'unsupported symbolic replay domain: free word exceeds 4096 operators') + _need(abs(coefficient.numerator).bit_length() <= MAX_COEFFICIENT_BITS + and coefficient.denominator.bit_length() <= MAX_COEFFICIENT_BITS, + 'unsupported symbolic replay domain: rational coefficient exceeds 4096 bits') + + +def _coefficient(operation, offset): + _need(len(operation) == offset + 2, 'scalar coefficient needs numerator and denominator') + numerator, denominator = operation[offset:] + _integer(numerator, 'scalar numerator must be integer') + _integer(denominator, 'scalar denominator must be integer') + _need(numerator != 0 and denominator != 0, 'nonzero scalar with nonzero denominator') + coefficient = Q(numerator, denominator) + denominator = coefficient.denominator + _need(denominator & (denominator - 1) == 0, 'scalar denominator must be dyadic') + return coefficient + + +def _scalar_allowance(opcode, coefficient=None): + if opcode in ('clear', 'copy'): + return 2 + numerator, denominator = abs(coefficient.numerator), coefficient.denominator + if opcode == 'scale': + _need(numerator & (numerator - 1) == 0, 'SCALE must be an invertible dyadic unit') + return 2 * (abs(numerator.bit_length() - denominator.bit_length()) + int(coefficient < 0)) + return 2 * (3 + numerator.bit_length() - 1 + numerator.bit_count() + denominator.bit_length() - 1) + + +def _frames_and_maps(canonical): + h = _integer(canonical['h'], 'binary width h must be integer') + _need(1 <= h <= 12, 'extractor supports binary widths 1..12') + frames = canonical['frames'] + _need(type(frames) is list and 0 < len(frames) <= 20000, 'bounded explicit frame table') + _need(all(type(frame) is list and len(frame) <= h for frame in frames), 'bounded binary frame bases') + _need(sum(1 << len(frame) for frame in frames) <= 2000000, 'expanded binary frame table exceeds budget') + spaces = [_span(frame, h) for frame in frames] + warps = canonical['warps'] + _need(type(warps) is list and len(warps) <= 10000, 'bounded native-map table') + _need(len(warps) * (1 << h) <= 2000000, 'expanded binary native maps exceed budget') + maps = [] + for index, warp in enumerate(warps): + _need(type(warp) is dict and type(warp.get('op')) is int and warp['op'] == index + 1, 'consecutive declared native operator IDs') + columns = warp['G_columns'] + _need(type(columns) is list and len(columns) == h, 'native binary-map columns') + _need(len(_span(columns, h)) == 1 << h, 'invertible native binary map') + forward = tuple(_binary_image(value, columns) for value in range(1 << h)) + inverse = [0] * (1 << h) + for value, image in enumerate(forward): + inverse[image] = value + maps.append((forward, tuple(inverse))) + return h, spaces, maps + + +def _port_boundary(canonical, h, spaces): + """Bind both native main banks to the target tariff used by the caller.""" + v = canonical['v'] + ports = canonical.get('ports') + _need(type(ports) is list and len(ports) == v, + 'unsupported native boundary: one explicit port per main pair required') + _need(all(type(port) is int and 0 < port < 1 << h and port.bit_count() % 2 == 1 for port in ports) + and len(set(ports)) == v, + 'unsupported native boundary: ports must be distinct odd-parity nonzero binary vectors') + full = frozenset(range(1 << h)) + for index, port in enumerate(ports): + _need(spaces[canonical['start'][index]] == frozenset((0, port)) + and spaces[canonical['final'][index]] == full, + f'unsupported native boundary at main pair {index}: first bank must be port-line to full') + hyperplane = frozenset(value for value in full if (value & port).bit_count() % 2 == 0) + _need(spaces[canonical['start'][v + index]] == frozenset((0,)) + and spaces[canonical['final'][v + index]] == hyperplane, + f'unsupported native boundary at main pair {index}: second bank must be zero to the port-orthogonal hyperplane') + + +def _extract_direction(word, direction, h, spaces, maps): + canonical = word['canonical'] + v, fields = canonical['v'], len(canonical['start']) + program = word['programs'][direction] + _need(type(program) is list and len(program) <= 200000, direction + ': bounded explicit event list') + if 'owned' in word: + _need(type(word['owned']) is dict and set(word['owned']) == {'forward', 'backward'}, 'owned contracts for both orientations') + declaration = word['owned'][direction] + _need(type(declaration) is list, direction + ': owned role list') + owned_list = [_role(role, fields) for role in declaration] + _need(len(set(owned_list)) == len(owned_list), direction + ': duplicate owned role') + owned = set(owned_list) + ownership_origin = 'explicit word owned contract' + else: + # Original PR4610's established schema has no owned field. Its sole + # C0 workspace is admitted as owned; all persistent L fields are borrowed. + owned = {('C', 0)} + ownership_origin = 'legacy original schema: C0 owned, every L input borrowed' + _need(all(kind != 'L' or index >= 2 * v for kind, index in owned), direction + ': main input cannot be owned') + _need(len(owned) <= 10000, direction + ': bounded owned input list') + roles = {('L', index) for index in range(fields)} | owned + rows = {role: {(role, ()): Q(1)} for role in sorted(roles)} + current = {('L', index): frame for index, frame in enumerate(canonical['start'])} + current.update({role: None for role in owned if role[0] == 'C'}) + paid, counts = Counter(), Counter() + paid_events, scalar_events, zero_retags, native_events = [], [], [], [] + scalar_total, maximum_l1, maximum_denominator, maximum_terms = 0, Q(1), 1, 1 + phase_labels, adapters = [], [] + + def frame_id(value): + _integer(value, 'frame identifier must be integer') + _need(0 <= value < len(spaces), 'frame identifier outside explicit table') + return value + + for position, event in enumerate(program): + try: + _need(type(event) is list and event and type(event[0]) is str, 'event must be a nonempty opcode list') + kind = event[0] + counts[kind] += 1 + touched = None + if kind == 'scalar': + _need(len(event) == 3 and type(event[1]) is list and event[1], 'scalar event shape') + operation, frame = event[1], frame_id(event[2]) + opcode = operation[0] + _need(opcode in ('clear', 'copy', 'add', 'scale') and len(operation) >= 2, 'known scalar instruction') + target = _role(operation[1], fields) + _need(target in rows, 'scalar destination is not an input or declared owned role') + touched = target + coefficient = None + if opcode == 'clear': + _need(len(operation) == 2 and target in owned, 'CLEAR may erase only declared owned input') + rows[target] = {} + current[target] = frame + else: + _need(current[target] == frame, 'scalar destination frame mismatch') + if opcode in ('add', 'copy'): + _need(len(operation) >= 3, 'scalar source operand') + source = _role(operation[2], fields) + _need(source in rows and source != target, 'distinct declared scalar source') + _need(current[source] == frame, 'scalar source frame mismatch') + if opcode == 'copy': + _need(len(operation) == 3 and target in owned and not rows[target], 'COPY requires a cleared owned destination') + rows[target] = dict(rows[source]) + else: + coefficient = _coefficient(operation, 3) + _add(rows[target], rows[source], coefficient) + else: + coefficient = _coefficient(operation, 2) + _scalar_allowance(opcode, coefficient) + rows[target] = {key: coefficient * value for key, value in rows[target].items()} + allowance = _scalar_allowance(opcode, coefficient) + scalar_total += allowance + scalar_events.append({'event': position, 'opcode': opcode, 'role': list(target), + 'frame': frame, 'real_scalar_allowance': allowance}) + elif kind in ('climb', 'center'): + if kind == 'climb': + _need(len(event) == 6 and type(event[1]) is str, 'climb event shape') + target = _role(['L', event[2]], fields) + old, new, declared = event[3:] + else: + _need(len(event) == 5, 'centre event shape') + target = _role(['C', event[1]], fields) + old, new, declared = event[2:] + _need(target in owned, 'centre workspace must be declared owned') + old, new = frame_id(old), frame_id(new) + _integer(declared, 'declared paid rank must be integer') + _need(target in rows and current[target] == old, 'paid input frame mismatch') + _need(spaces[old] < spaces[new] if kind == 'climb' else + spaces[old] < spaces[new] or spaces[new] < spaces[old], 'paid transport must have nested distinct frames') + rank = abs(len(canonical['frames'][new]) - len(canonical['frames'][old])) + _need(rank == declared, 'paid rank differs from independently derived frame rank') + paid[rank] += 1 + paid_events.append({'event': position, 'kind': kind, 'role': list(target), + 'input_frame': old, 'output_frame': new, 'rank': rank}) + current[target] = new + touched = target + elif kind == 'zero_retag': + _need(len(event) == 4, 'zero-retag event shape') + target = _role(event[1], fields) + old, new = frame_id(event[2]), frame_id(event[3]) + _need(target in rows and current[target] == old, 'zero-retag input frame mismatch') + _need(not rows[target], 'uncharged zero-retag requires an identically zero full symbolic row') + current[target] = new + zero_retags.append({'event': position, 'role': list(target), 'input_frame': old, 'output_frame': new}) + touched = target + elif kind == 'warp': + _need(len(event) == 5, 'native event shape') + target = _role(event[1], fields) + operator = _integer(event[2], 'native operator ID must be integer') + old, new = frame_id(event[3]), frame_id(event[4]) + _need(target in rows and current[target] == old and 1 <= abs(operator) <= len(maps), 'native role, operator or input frame mismatch') + binary_map = maps[abs(operator) - 1][int(operator < 0)] + _need(frozenset(binary_map[value] for value in spaces[old]) == spaces[new], + 'native map has an unpriced residual between its actual input and output frames') + # The retained backward ABI is primitive-wise conjugation, + # not adjoint or reversal. It uses an independent formal alphabet. + symbol = (1 if operator > 0 else -1) * (abs(operator) + (1000000 if direction == 'backward' else 0)) + rows[target] = {(variable, word[1:] if word and word[0] == -symbol else (symbol,) + word): value + for (variable, word), value in rows[target].items()} + current[target] = new + native_events.append({'event': position, 'role': list(target), 'operator': operator, + 'input_frame': old, 'output_frame': new, 'residual_rank': 0}) + touched = target + elif kind == 'adapter': + _need(len(event) == 4 and event[1] in ('old_to_new', 'new_to_old'), 'known endpoint adapter marker') + index = _integer(event[2], 'main adapter index must be integer') + _need(0 <= index < 2 * v, 'endpoint adapters may touch main roles only') + frame = frame_id(event[3]) + expected = canonical['start' if event[1] == 'old_to_new' else 'final'][index] + _need(frame == expected, 'adapter marker disagrees with endpoint frame') + adapters.append((event[1], index, frame)) + elif kind == 'phase': + _need(len(event) == 2 and event[1] in PHASES, 'known retained phase annotation') + phase_labels.append(event[1]) + else: + raise ValueError('unknown event opcode ' + kind) + if touched is not None: + row = rows[touched] + _guard_row(row) + maximum_terms = max(maximum_terms, len(row)) + maximum_l1 = max(maximum_l1, sum(map(abs, row.values()), Q(0))) + maximum_denominator = max(maximum_denominator, max((value.denominator for value in row.values()), default=1)) + except (KeyError, TypeError, IndexError, ZeroDivisionError, ValueError) as error: + raise ValueError(f'{direction} event {position}: {error}') from None + _need(phase_labels == PHASES, direction + ': complete retained phase annotation sequence') + expected_adapters = {(kind, index, canonical[side][index]) for kind, side in + [('old_to_new', 'start'), ('new_to_old', 'final')] for index in range(2 * v)} + _need(len(adapters) == len(expected_adapters) and set(adapters) == expected_adapters, + direction + ': exactly one entry and exit adapter for each main role') + _need([current['L', index] for index in range(fields)] == canonical['final'], direction + ': final persistent frame mismatch') + for role, row in sorted(rows.items()): + expected = {} if role in owned else {(role, ()): Q(1)} + if role not in owned and role[0] == 'L': + index = role[1] + if direction == 'backward' and index < v: + expected[(('L', index + v), ())] = Q(-1) + elif direction == 'forward' and v <= index < 2 * v: + expected[(('L', index - v), ())] = Q(1) + _need(row == expected, direction + ': symbolic return mismatch for ' + str(list(role))) + helpers, helper_targets = Counter(), [] + for index in range(2 * v, fields): + role = 'L', index + old, new = canonical['start'][index], current[role] + rank = len(canonical['frames'][new]) - len(canonical['frames'][old]) + credited = role not in owned + if credited: + _need(spaces[old] < spaces[new], direction + ': retained helper has nonascending target contract') + helpers[rank] += 1 + helper_targets.append({'role': list(role), 'input_frame': old, 'output_frame': new, + 'target_rank': rank, 'credited': credited, + 'reason': 'independent symbolic identity return' if credited else 'owned input erased; no productive credit'}) + return {'paid': {str(rank): count for rank, count in sorted(paid.items())}, + 'helpers': {str(rank): count for rank, count in sorted(helpers.items())}, + 'paid_events': paid_events, 'helper_targets': helper_targets, + 'scalar_allowance': scalar_total, 'scalar_events': scalar_events, + 'zero_retags': zero_retags, 'native_events': native_events, + 'owned': [list(role) for role in sorted(owned)], 'ownership_origin': ownership_origin, + 'independent_owned_entry_columns': len(owned), + 'independent_persistent_columns': fields - sum(kind == 'L' for kind, _ in owned), + 'owned_outputs_zero': True, 'event_counts': dict(sorted(counts.items())), + 'max_formal_prefix_l1': str(maximum_l1), 'max_denominator': maximum_denominator, + 'max_row_terms': maximum_terms, + 'paid_calls': sum(paid.values()), 'productive_helpers': sum(helpers.values())} + + +def extract(word): + """Return source-derived JSON-friendly native ledgers, or raise ValueError. + + Input is an already decoded literal native-word dict. The original legacy + schema and the two explicit-owned successor schemas share this interpreter. + Every declared paid_profiles/local_profile entry is deliberately ignored. + The returned hashes identify canonical JSON objects, not compressed bytes. + """ + try: + _need(type(word) is dict and type(word.get('canonical')) is dict, 'word and canonical must be objects') + if 'schema' in word: + _need(word['schema'] in ('joint-helper-relations-word/1', 'eight-owned-helper-relations/1') + and 'owned' in word, 'unsupported explicit native-word schema or missing owned contract') + else: + _need('owned' not in word, 'legacy original schema cannot add an implicit owned contract') + canonical = word['canonical'] + v = _integer(canonical['v'], 'main-port count must be integer') + _need(1 <= v <= 1000 and type(canonical['start']) is list and type(canonical['final']) is list, 'bounded main ports and explicit endpoints') + fields = len(canonical['start']) + _need(2 * v <= fields <= 10000 and len(canonical['final']) == fields, 'persistent endpoint field inventory') + _need(type(word.get('programs')) is dict and set(word['programs']) == {'forward', 'backward'}, 'literal forward and backward programs required') + h, spaces, maps = _frames_and_maps(canonical) + for frame in canonical['start'] + canonical['final']: + _need(type(frame) is int and 0 <= frame < len(spaces), 'endpoint frame outside explicit table') + _port_boundary(canonical, h, spaces) + orientations = {direction: _extract_direction(word, direction, h, spaces, maps) + for direction in ('forward', 'backward')} + return {'schema': SCHEMA, 'word_sha256': _digest(word), + 'canonical_sha256': _digest(canonical), 'v': v, 'h': h, + 'fields': fields, 'orientations': orientations, + 'scope': 'Literal-source symbolic endpoint/ownership and frame-rank conformance only; no absolute phase, precision, physical cost implementation, compiler or supplier admission.'} + except (KeyError, TypeError, IndexError, ZeroDivisionError) as error: + raise ValueError('malformed native word: ' + str(error)) from None diff --git a/research/source-invoice-conformance/source/CONTROLLER.json b/research/source-invoice-conformance/source/CONTROLLER.json new file mode 100644 index 0000000000..49a2f06758 --- /dev/null +++ b/research/source-invoice-conformance/source/CONTROLLER.json @@ -0,0 +1,5224 @@ +{ + "ambient_rank": 145, + "boundaries": { + "left": [ + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "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", + "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", + "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", + "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", + "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", + "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", + "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", + "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" + ], + [ + "1", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "1", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "1", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "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", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "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", + "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", + "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", + "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", + "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", + "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", + "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", + "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", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "1", + "0", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ] + ], + "left_program": [ + [ + "SWAP", + 30, + 31 + ], + [ + "SWAP", + 29, + 30 + ], + [ + "SWAP", + 28, + 30 + ], + [ + "SWAP", + 27, + 29 + ], + [ + "SWAP", + 26, + 28 + ], + [ + "SWAP", + 25, + 30 + ], + [ + "SWAP", + 24, + 25 + ], + [ + "SWAP", + 23, + 26 + ], + [ + "SWAP", + 22, + 30 + ], + [ + "SWAP", + 20, + 26 + ], + [ + "SWAP", + 19, + 22 + ], + [ + "SWAP", + 18, + 29 + ], + [ + "SWAP", + 17, + 23 + ], + [ + "SWAP", + 16, + 27 + ], + [ + "SCALE", + 15, + "-1" + ], + [ + "SWAP", + 15, + 31 + ], + [ + "ADD", + 12, + 14, + "1" + ], + [ + "ADD", + 10, + 14, + "-1" + ], + [ + "ADD", + 8, + 14, + "1" + ], + [ + "ADD", + 6, + 14, + "-1" + ], + [ + "ADD", + 4, + 14, + "1" + ], + [ + "ADD", + 2, + 14, + "-1" + ], + [ + "ADD", + 0, + 14, + "1" + ], + [ + "SWAP", + 14, + 15 + ], + [ + "ADD", + 31, + 13, + "1" + ], + [ + "SWAP", + 13, + 30 + ], + [ + "ADD", + 10, + 12, + "1" + ], + [ + "ADD", + 8, + 12, + "-1" + ], + [ + "ADD", + 6, + 12, + "1" + ], + [ + "ADD", + 4, + 12, + "-1" + ], + [ + "ADD", + 2, + 12, + "1" + ], + [ + "ADD", + 0, + 12, + "-1" + ], + [ + "SWAP", + 12, + 14 + ], + [ + "ADD", + 31, + 11, + "-1" + ], + [ + "ADD", + 30, + 11, + "-1" + ], + [ + "SCALE", + 11, + "-1" + ], + [ + "SWAP", + 11, + 29 + ], + [ + "ADD", + 8, + 10, + "1" + ], + [ + "ADD", + 6, + 10, + "-1" + ], + [ + "ADD", + 4, + 10, + "1" + ], + [ + "ADD", + 2, + 10, + "-1" + ], + [ + "ADD", + 0, + 10, + "1" + ], + [ + "SWAP", + 10, + 13 + ], + [ + "ADD", + 31, + 9, + "1" + ], + [ + "ADD", + 30, + 9, + "1" + ], + [ + "ADD", + 29, + 9, + "1" + ], + [ + "SWAP", + 9, + 28 + ], + [ + "ADD", + 6, + 8, + "1" + ], + [ + "ADD", + 4, + 8, + "-1" + ], + [ + "ADD", + 2, + 8, + "1" + ], + [ + "ADD", + 0, + 8, + "-1" + ], + [ + "SWAP", + 8, + 12 + ], + [ + "ADD", + 31, + 7, + "-1" + ], + [ + "ADD", + 30, + 7, + "-1" + ], + [ + "ADD", + 29, + 7, + "-1" + ], + [ + "ADD", + 28, + 7, + "-1" + ], + [ + "SCALE", + 7, + "-1" + ], + [ + "SWAP", + 7, + 27 + ], + [ + "ADD", + 4, + 6, + "1" + ], + [ + "ADD", + 2, + 6, + "-1" + ], + [ + "ADD", + 0, + 6, + "1" + ], + [ + "SWAP", + 6, + 11 + ], + [ + "ADD", + 31, + 5, + "1" + ], + [ + "ADD", + 30, + 5, + "1" + ], + [ + "ADD", + 29, + 5, + "1" + ], + [ + "ADD", + 28, + 5, + "1" + ], + [ + "ADD", + 27, + 5, + "1" + ], + [ + "SWAP", + 5, + 26 + ], + [ + "ADD", + 2, + 4, + "1" + ], + [ + "ADD", + 0, + 4, + "-1" + ], + [ + "SWAP", + 4, + 10 + ], + [ + "ADD", + 31, + 3, + "-1" + ], + [ + "ADD", + 30, + 3, + "-1" + ], + [ + "ADD", + 29, + 3, + "-1" + ], + [ + "ADD", + 28, + 3, + "-1" + ], + [ + "ADD", + 27, + 3, + "-1" + ], + [ + "ADD", + 26, + 3, + "-1" + ], + [ + "SCALE", + 3, + "-1" + ], + [ + "SWAP", + 3, + 25 + ], + [ + "ADD", + 0, + 2, + "1" + ], + [ + "SWAP", + 2, + 9 + ], + [ + "ADD", + 31, + 1, + "1" + ], + [ + "ADD", + 30, + 1, + "1" + ], + [ + "ADD", + 29, + 1, + "1" + ], + [ + "ADD", + 28, + 1, + "1" + ], + [ + "ADD", + 27, + 1, + "1" + ], + [ + "ADD", + 26, + 1, + "1" + ], + [ + "ADD", + 25, + 1, + "1" + ], + [ + "SWAP", + 1, + 24 + ], + [ + "SWAP", + 0, + 8 + ] + ], + "right": [ + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "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", + "0", + "0", + "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", + "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", + "0", + "0", + "0", + "0", + "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", + "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", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "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", + "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", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "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", + "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", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "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", + "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", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "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", + "0", + "0", + "0", + "0", + "0", + "1", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "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", + "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", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "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", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "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", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "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", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "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", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "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", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "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", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "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", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "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" + ], + [ + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "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" + ] + ], + "right_program": [ + [ + "ADD", + 30, + 31, + "-1" + ], + [ + "ADD", + 29, + 31, + "-1" + ], + [ + "ADD", + 28, + 31, + "-1" + ], + [ + "ADD", + 27, + 31, + "-1" + ], + [ + "SCALE", + 31, + "-1" + ], + [ + "ADD", + 31, + 30, + "-1" + ], + [ + "ADD", + 29, + 30, + "-1" + ], + [ + "ADD", + 28, + 30, + "-1" + ], + [ + "ADD", + 27, + 30, + "-1" + ], + [ + "ADD", + 31, + 29, + "-1" + ], + [ + "ADD", + 28, + 29, + "-1" + ], + [ + "ADD", + 27, + 29, + "-1" + ], + [ + "SCALE", + 29, + "-1" + ], + [ + "ADD", + 31, + 28, + "-1" + ], + [ + "ADD", + 27, + 28, + "-1" + ], + [ + "SWAP", + 28, + 29 + ], + [ + "ADD", + 31, + 27, + "-1" + ], + [ + "SCALE", + 27, + "-1" + ], + [ + "SWAP", + 27, + 29 + ], + [ + "ADD", + 31, + 26, + "1" + ], + [ + "SWAP", + 26, + 29 + ], + [ + "ADD", + 29, + 25, + "-1" + ], + [ + "ADD", + 24, + 25, + "-1" + ], + [ + "SWAP", + 25, + 28 + ], + [ + "ADD", + 28, + 24, + "1" + ], + [ + "SWAP", + 23, + 29 + ], + [ + "SWAP", + 22, + 25 + ], + [ + "SWAP", + 20, + 23 + ], + [ + "SWAP", + 19, + 25 + ], + [ + "SWAP", + 18, + 27 + ], + [ + "SWAP", + 17, + 29 + ], + [ + "SWAP", + 16, + 31 + ], + [ + "ADD", + 14, + 15, + "-1" + ], + [ + "SWAP", + 15, + 30 + ], + [ + "ADD", + 13, + 14, + "-1" + ], + [ + "SWAP", + 14, + 30 + ], + [ + "ADD", + 12, + 13, + "-1" + ], + [ + "SWAP", + 13, + 22 + ], + [ + "ADD", + 11, + 12, + "-1" + ], + [ + "SWAP", + 12, + 30 + ], + [ + "ADD", + 10, + 11, + "-1" + ], + [ + "SWAP", + 11, + 18 + ], + [ + "ADD", + 9, + 10, + "-1" + ], + [ + "SWAP", + 10, + 22 + ], + [ + "ADD", + 8, + 9, + "-1" + ], + [ + "SWAP", + 9, + 26 + ], + [ + "SWAP", + 8, + 30 + ], + [ + "SWAP", + 7, + 16 + ], + [ + "SWAP", + 6, + 18 + ], + [ + "SWAP", + 5, + 20 + ], + [ + "SWAP", + 4, + 22 + ], + [ + "SWAP", + 3, + 24 + ], + [ + "SWAP", + 2, + 26 + ], + [ + "SWAP", + 1, + 28 + ], + [ + "SWAP", + 0, + 30 + ] + ] + }, + "diagonal": [ + [ + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 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, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 0, + 1, + 1 + ], + [ + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 0, + 1, + 0, + 1, + 1 + ], + [ + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 1 + ], + [ + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 1 + ], + [ + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 1 + ], + [ + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 1 + ], + [ + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 1 + ], + [ + -1, + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + -1, + 1, + 1, + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + -1, + 1, + 1, + 0, + 1, + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + -1, + 1, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + -1, + 1, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + -1, + 1, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + -1, + 1, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + -1, + 1, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 1 + ], + [ + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 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, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 0, + 1, + 1 + ], + [ + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 0, + 1, + 0, + 1, + 1 + ], + [ + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 1 + ], + [ + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 1 + ], + [ + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 1 + ], + [ + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 1 + ], + [ + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 1 + ], + [ + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 1, + 1, + 1, + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 1, + 1, + 1, + 0, + 1, + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 1, + 1, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 1, + 1, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 1, + 1, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 1, + 1, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 1, + 1, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 1 + ] + ], + "invoice": { + "main": { + "17": 448, + "25": 448, + "33": 448, + "41": 448, + "49": 448, + "57": 448, + "65": 448, + "73": 224, + "145": 224 + }, + "owned_streams_reused_sequentially": 1, + "paid": { + "1": 46446, + "2": 12834, + "3": 4032, + "4": 1836, + "5": 360, + "8": 144, + "16": 448, + "24": 448, + "32": 448, + "40": 448, + "48": 448, + "56": 448, + "64": 448, + "72": 224 + }, + "paid_calls": 69012, + "productive_fields": 10928, + "rank_surplus": 752, + "raw_scalar_record_bound": 1000000000, + "targets": { + "5": 504, + "6": 324, + "7": 1008, + "8": 1674, + "9": 3834, + "17": 448, + "25": 448, + "33": 448, + "41": 448, + "49": 448, + "57": 448, + "65": 448, + "73": 224, + "145": 224 + }, + "thick_calls": 18, + "thick_stages": [ + 0, + 1, + 3, + 5, + 7, + 9, + 11, + 13, + 15, + 17, + 19, + 21, + 23, + 25, + 27, + 29, + 31, + 32 + ], + "thin_queries": 1680, + "whole_idle": { + "16": 448, + "24": 448, + "32": 448, + "40": 448, + "48": 448, + "56": 448, + "64": 448, + "72": 224 + } + }, + "keep_mask": 35047648968703, + "kind": "complex", + "pairs": 16, + "physical_events": [ + [ + "LOCAL", + 0, + 0, + false + ], + [ + "LOCAL", + 1, + 0, + true + ], + [ + "IDLE", + 1, + [ + 0, + 1 + ] + ], + [ + "ADD", + 0, + 2, + 1 + ], + [ + "ADD", + 3, + 1, + -1 + ], + [ + "QUERY_SHEAR", + 2, + 0, + false + ], + [ + "ADD", + 0, + 2, + -1 + ], + [ + "ADD", + 3, + 1, + 1 + ], + [ + "LOCAL", + 3, + 1, + true + ], + [ + "IDLE", + 2, + [ + 0, + 1, + 3 + ] + ], + [ + "ADD", + 2, + 4, + 1 + ], + [ + "ADD", + 5, + 3, + -1 + ], + [ + "QUERY_SHEAR", + 4, + 1, + false + ], + [ + "ADD", + 2, + 4, + -1 + ], + [ + "ADD", + 5, + 3, + 1 + ], + [ + "LOCAL", + 5, + 2, + true + ], + [ + "IDLE", + 3, + [ + 0, + 1, + 3, + 5 + ] + ], + [ + "ADD", + 4, + 6, + 1 + ], + [ + "ADD", + 7, + 5, + -1 + ], + [ + "QUERY_SHEAR", + 6, + 2, + false + ], + [ + "ADD", + 4, + 6, + -1 + ], + [ + "ADD", + 7, + 5, + 1 + ], + [ + "LOCAL", + 7, + 3, + true + ], + [ + "IDLE", + 4, + [ + 0, + 1, + 3, + 5, + 7 + ] + ], + [ + "ADD", + 6, + 8, + 1 + ], + [ + "ADD", + 9, + 7, + -1 + ], + [ + "QUERY_SHEAR", + 8, + 3, + false + ], + [ + "ADD", + 6, + 8, + -1 + ], + [ + "ADD", + 9, + 7, + 1 + ], + [ + "LOCAL", + 9, + 4, + true + ], + [ + "IDLE", + 5, + [ + 0, + 1, + 3, + 5, + 7, + 9 + ] + ], + [ + "ADD", + 8, + 10, + 1 + ], + [ + "ADD", + 11, + 9, + -1 + ], + [ + "QUERY_SHEAR", + 10, + 4, + false + ], + [ + "ADD", + 8, + 10, + -1 + ], + [ + "ADD", + 11, + 9, + 1 + ], + [ + "LOCAL", + 11, + 5, + true + ], + [ + "IDLE", + 6, + [ + 0, + 1, + 3, + 5, + 7, + 9, + 11 + ] + ], + [ + "ADD", + 10, + 12, + 1 + ], + [ + "ADD", + 13, + 11, + -1 + ], + [ + "QUERY_SHEAR", + 12, + 5, + false + ], + [ + "ADD", + 10, + 12, + -1 + ], + [ + "ADD", + 13, + 11, + 1 + ], + [ + "LOCAL", + 13, + 6, + true + ], + [ + "IDLE", + 7, + [ + 0, + 1, + 3, + 5, + 7, + 9, + 11, + 13 + ] + ], + [ + "ADD", + 12, + 14, + 1 + ], + [ + "ADD", + 15, + 13, + -1 + ], + [ + "QUERY_SHEAR", + 14, + 6, + false + ], + [ + "ADD", + 12, + 14, + -1 + ], + [ + "ADD", + 15, + 13, + 1 + ], + [ + "LOCAL", + 15, + 7, + true + ], + [ + "ADD", + 14, + 16, + 1 + ], + [ + "ADD", + 17, + 15, + -1 + ], + [ + "QUERY_SHEAR", + 16, + 7, + false + ], + [ + "ADD", + 14, + 16, + -1 + ], + [ + "ADD", + 17, + 15, + 1 + ], + [ + "LOCAL", + 17, + 8, + true + ], + [ + "ADD", + 16, + 18, + 1 + ], + [ + "ADD", + 19, + 17, + -1 + ], + [ + "QUERY_SHEAR", + 18, + 8, + false + ], + [ + "ADD", + 16, + 18, + -1 + ], + [ + "ADD", + 19, + 17, + 1 + ], + [ + "LOCAL", + 19, + 9, + true + ], + [ + "ADD", + 18, + 20, + 1 + ], + [ + "ADD", + 21, + 19, + -1 + ], + [ + "QUERY_SHEAR", + 20, + 9, + false + ], + [ + "ADD", + 18, + 20, + -1 + ], + [ + "ADD", + 21, + 19, + 1 + ], + [ + "LOCAL", + 21, + 10, + true + ], + [ + "ADD", + 20, + 22, + 1 + ], + [ + "ADD", + 23, + 21, + -1 + ], + [ + "QUERY_SHEAR", + 22, + 10, + false + ], + [ + "ADD", + 20, + 22, + -1 + ], + [ + "ADD", + 23, + 21, + 1 + ], + [ + "LOCAL", + 23, + 11, + true + ], + [ + "ADD", + 22, + 24, + 1 + ], + [ + "ADD", + 25, + 23, + -1 + ], + [ + "QUERY_SHEAR", + 24, + 11, + false + ], + [ + "ADD", + 22, + 24, + -1 + ], + [ + "ADD", + 25, + 23, + 1 + ], + [ + "LOCAL", + 25, + 12, + true + ], + [ + "ADD", + 24, + 26, + 1 + ], + [ + "ADD", + 27, + 25, + -1 + ], + [ + "QUERY_SHEAR", + 26, + 12, + false + ], + [ + "ADD", + 24, + 26, + -1 + ], + [ + "ADD", + 27, + 25, + 1 + ], + [ + "LOCAL", + 27, + 13, + true + ], + [ + "ADD", + 26, + 28, + 1 + ], + [ + "ADD", + 29, + 27, + -1 + ], + [ + "QUERY_SHEAR", + 28, + 13, + false + ], + [ + "ADD", + 26, + 28, + -1 + ], + [ + "ADD", + 29, + 27, + 1 + ], + [ + "LOCAL", + 29, + 14, + true + ], + [ + "ADD", + 28, + 30, + 1 + ], + [ + "ADD", + 31, + 29, + -1 + ], + [ + "QUERY_SHEAR", + 30, + 14, + false + ], + [ + "ADD", + 28, + 30, + -1 + ], + [ + "ADD", + 31, + 29, + 1 + ], + [ + "LOCAL", + 31, + 15, + true + ], + [ + "LOCAL", + 32, + 15, + false + ], + [ + "IDLE", + 7, + [ + 17, + 19, + 21, + 23, + 25, + 27, + 29, + 31, + 32 + ] + ], + [ + "IDLE", + 8, + [ + 19, + 21, + 23, + 25, + 27, + 29, + 31, + 32 + ] + ], + [ + "IDLE", + 9, + [ + 21, + 23, + 25, + 27, + 29, + 31, + 32 + ] + ], + [ + "IDLE", + 10, + [ + 23, + 25, + 27, + 29, + 31, + 32 + ] + ], + [ + "IDLE", + 11, + [ + 25, + 27, + 29, + 31, + 32 + ] + ], + [ + "IDLE", + 12, + [ + 27, + 29, + 31, + 32 + ] + ], + [ + "IDLE", + 13, + [ + 29, + 31, + 32 + ] + ], + [ + "IDLE", + 14, + [ + 31, + 32 + ] + ], + [ + "ADD", + 30, + 28, + 1 + ], + [ + "ADD", + 29, + 31, + -1 + ], + [ + "ADD", + 28, + 26, + 1 + ], + [ + "ADD", + 27, + 29, + -1 + ], + [ + "ADD", + 26, + 24, + 1 + ], + [ + "ADD", + 25, + 27, + -1 + ], + [ + "ADD", + 24, + 22, + 1 + ], + [ + "ADD", + 23, + 25, + -1 + ], + [ + "ADD", + 22, + 20, + 1 + ], + [ + "ADD", + 21, + 23, + -1 + ], + [ + "ADD", + 20, + 18, + 1 + ], + [ + "ADD", + 19, + 21, + -1 + ], + [ + "ADD", + 18, + 16, + 1 + ], + [ + "ADD", + 17, + 19, + -1 + ], + [ + "ADD", + 16, + 14, + 1 + ], + [ + "ADD", + 15, + 17, + -1 + ], + [ + "ADD", + 14, + 12, + 1 + ], + [ + "ADD", + 13, + 15, + -1 + ], + [ + "ADD", + 12, + 10, + 1 + ], + [ + "ADD", + 11, + 13, + -1 + ], + [ + "ADD", + 10, + 8, + 1 + ], + [ + "ADD", + 9, + 11, + -1 + ], + [ + "ADD", + 8, + 6, + 1 + ], + [ + "ADD", + 7, + 9, + -1 + ], + [ + "ADD", + 6, + 4, + 1 + ], + [ + "ADD", + 5, + 7, + -1 + ], + [ + "ADD", + 4, + 2, + 1 + ], + [ + "ADD", + 3, + 5, + -1 + ], + [ + "ADD", + 2, + 0, + 1 + ], + [ + "ADD", + 1, + 3, + -1 + ], + [ + "SIGNED_SWAP", + 0, + 1 + ], + [ + "SIGNED_SWAP", + 2, + 3 + ], + [ + "SIGNED_SWAP", + 4, + 5 + ], + [ + "SIGNED_SWAP", + 6, + 7 + ], + [ + "SIGNED_SWAP", + 8, + 9 + ], + [ + "SIGNED_SWAP", + 10, + 11 + ], + [ + "SIGNED_SWAP", + 12, + 13 + ], + [ + "SIGNED_SWAP", + 14, + 15 + ], + [ + "SIGNED_SWAP", + 16, + 17 + ], + [ + "SIGNED_SWAP", + 18, + 19 + ], + [ + "SIGNED_SWAP", + 20, + 21 + ], + [ + "SIGNED_SWAP", + 22, + 23 + ], + [ + "SIGNED_SWAP", + 24, + 25 + ], + [ + "SIGNED_SWAP", + 26, + 27 + ], + [ + "SIGNED_SWAP", + 28, + 29 + ], + [ + "SIGNED_SWAP", + 30, + 31 + ] + ], + "prefix_pairs": 7 +} diff --git a/research/source-invoice-conformance/source/PR4610-WORD.json.gz b/research/source-invoice-conformance/source/PR4610-WORD.json.gz new file mode 100644 index 0000000000..46d929df83 Binary files /dev/null and b/research/source-invoice-conformance/source/PR4610-WORD.json.gz differ diff --git a/research/source-invoice-conformance/source/PR5383-WORD.json.gz b/research/source-invoice-conformance/source/PR5383-WORD.json.gz new file mode 100644 index 0000000000..a4a58afce1 Binary files /dev/null and b/research/source-invoice-conformance/source/PR5383-WORD.json.gz differ diff --git a/research/source-invoice-conformance/source/PR5387-WORD.json.gz b/research/source-invoice-conformance/source/PR5387-WORD.json.gz new file mode 100644 index 0000000000..c62fcb5964 Binary files /dev/null and b/research/source-invoice-conformance/source/PR5387-WORD.json.gz differ diff --git a/research/source-invoice-conformance/verify.py b/research/source-invoice-conformance/verify.py new file mode 100644 index 0000000000..8516b28b4f --- /dev/null +++ b/research/source-invoice-conformance/verify.py @@ -0,0 +1,160 @@ +#!/usr/bin/env python3 +"""Independent claim calibrations and discriminating conformance failures.""" +import argparse +from collections import Counter +from copy import deepcopy +from hashlib import sha256 +import json +from pathlib import Path +import subprocess +import sys +import tempfile + +HERE=Path(__file__).resolve().parent +sys.path.insert(0,str(HERE)) +import conform +import native_invoice +import caller_invoice + + +def need(ok,message): + if not ok:raise ValueError(message) + + +def reject(name,action,contains): + try:action() + except ValueError as error: + need(contains in str(error),f'{name}: unexpected rejection {error}') + return {'control':name,'rejection':str(error)} + raise ValueError('Accepted invalid conformance control: '+name) + + +def authenticate(): + for row in conform.read(HERE/'EXPORTS.json')['exports']: + need(sha256((HERE/row['file']).read_bytes()).hexdigest()==row['sha256'],'Source export drift: '+row['file']) + + +def ledger_check(audit): + c=audit['caller'];calls={row['id']:row for row in c['calls']};paid=Counter();targets=Counter();debits=Counter() + for group in c['local_groups']: + need(len(group['call_ids'])==len(set(group['call_ids']))==group['count'],'Unique source call occurrences') + need(all(calls[identifier]['orientation']==group['orientation'] for identifier in group['call_ids']),'Source call orientation provenance') + dst=paid if group['side']=='paid' else targets if group['side']=='targets' else debits + dst[group['rank']]+=group['count'] + for row in c['outer_paid']:paid[row['rank']]+=row['count'] + for row in c['main_targets']:targets[row['rank']]+=row['count'] + clean=lambda x:{str(k):v for k,v in sorted(x.items()) if v} + need(clean(paid)==audit['invoice']['paid'] and clean(targets)==audit['invoice']['targets'],'Complete factored event ledger equals emitted invoice') + return clean(debits) + + +def controls(audits,words,controller): + a=audits['PR5383'];b=audits['PR5387'];rejections=[] + bad=conform.claim(a);bad['invoice']=deepcopy(bad['invoice']);bad['invoice']['targets']['9']+=128 + rejections.append(reject('omitted_128_owned_helper_debits',lambda:conform.compare(a,bad),'targets H9:')) + for name,side,rank,count in [('stale_paid_rank8','paid','8',128),('omitted_query_calls','paid','1',-1680),('omitted_whole_idles','paid','16',-448)]: + bad=deepcopy(conform.claim(a));bad['invoice'][side][rank]+=count + rejections.append(reject(name,lambda bad=bad:conform.compare(a,bad),'Invoice mismatch:')) + bad=deepcopy(conform.claim(a));bad['invoice']['paid']['1']-=16;bad['invoice']['paid']['2']+=8 + need(sum(int(k)*v for k,v in bad['invoice']['paid'].items())==sum(int(k)*v for k,v in a['invoice']['paid'].items()),'Rank-mass-preserving billing mutation') + rejections.append(reject('equal_rank_mass_wrong_profile',lambda:conform.compare(a,bad),'Invoice mismatch:')) + rejections.append(reject('same_invoice_stale_word_binding',lambda:conform.compare(b,conform.claim(a)),'Claim source binding differs')) + bad=deepcopy(conform.claim(a));bad['invoice']['paid']['1']=True + rejections.append(reject('boolean_count_is_not_integer',lambda:conform.compare(a,bad),'exact nonnegative integers')) + # These invoke the independent interpreter on altered source programs, not + # author receipts or the annotation hashes that the source parser ignores. + base=words['PR5383'] + bad=deepcopy(base);next(e for e in bad['programs']['forward'] if e[0]=='climb')[5]+=1 + rejections.append(reject('misstated_actual_paid_rank',lambda:native_invoice.extract(bad),'independently derived frame rank')) + bad=deepcopy(base);e=next(e for e in bad['programs']['forward'] if e[0]=='warp' and e[3]!=e[4]);e[4]=e[3] + rejections.append(reject('unpriced_native_frame_residual',lambda:native_invoice.extract(bad),'unpriced residual')) + bad=deepcopy(base) + index,event=next((i,e) for i,e in enumerate(bad['programs']['forward']) if e[0]=='climb') + bad['programs']['forward'][index]=['zero_retag',['L',event[2]],event[3],event[4]] + rejections.append(reject('false_zero_retag',lambda:native_invoice.extract(bad),'identically zero full symbolic row')) + bad=deepcopy(base);bad['programs']['backward'][1][1][3]*=-1 + rejections.append(reject('wrong_preparation_sign',lambda:native_invoice.extract(bad),'symbolic return mismatch')) + bad=deepcopy(base);bad['owned']['backward'].remove(['L',225]) + rejections.append(reject('undeclared_owned_input_clear',lambda:native_invoice.extract(bad),'only declared owned input')) + bad=deepcopy(base);bad['programs']['forward'].insert(0,['unpriced_magic',1]) + rejections.append(reject('unknown_native_operation',lambda:native_invoice.extract(bad),'unknown event opcode')) + native=a['native'] + for name,mutate,needle in [ + ('changed_literal_idle',lambda c:next(e for e in c['physical_events'] if e[0]=='IDLE')[2].append(32),'Caller'), + ('changed_literal_orientation',lambda c:next(e for e in c['physical_events'] if e[0]=='LOCAL').__setitem__(3,True),'Caller'), + ('wrong_main_diagonal',lambda c:c['diagonal'][0].__setitem__(0,1),'diagonal mismatch'), + ('unknown_caller_operation',lambda c:c['physical_events'].insert(0,['unpriced_magic']),'Known caller opcode'), + ('boundary_program_mismatch',lambda c:c['boundaries']['right_program'][0].__setitem__(3,'1'),'program/matrix mismatch')]: + bad=deepcopy(controller);mutate(bad) + rejections.append(reject(name,lambda bad=bad:caller_invoice.extract(bad,native),needle)) + bad=deepcopy(base);bad['schema']='unknown-new-abi/1' + rejections.append(reject('unknown_source_schema',lambda:native_invoice.extract(bad),'schema')) + # Altering the main endpoint while keeping its formal row cannot inherit + # the fixed caller tariff. Include the additional paid transport and update + # its adapter, rather than relying on a stale-final-frame rejection. + bad=deepcopy(base);v=bad['canonical']['v'];old=bad['canonical']['final'][v] + full=bad['canonical']['final'][0];bad['canonical']['final'][v]=full + for direction,program in bad['programs'].items(): + index=next(i for i,e in enumerate(program) if e[:3]==['adapter','new_to_old',v]) + program[index][3]=full + program.insert(index,['climb','changed_main_contract',v,old,full,1]) + rejections.append(reject('changed_main_endpoint_tariff',lambda:native_invoice.extract(bad),'unsupported native boundary')) + bad=deepcopy(base);role=next(i for i in range(224,632) if bad['canonical']['start'][i]==0) + bad['programs']['forward'][1:1]=[['warp',['L',role],1,0,0] for _ in range(4097)] + rejections.append(reject('symbolic_word_growth_limit',lambda:native_invoice.extract(bad),'unsupported symbolic replay domain')) + rejections.append(reject('duplicate_json_keys',lambda:conform.parse(b'{"a":1,"a":2}'),'Duplicate JSON key')) + rejections.append(reject('floating_point_input',lambda:conform.parse(b'{"a":1.0}'),'Exact integer/rational')) + rejections.append(reject('exponent_rational_notation',lambda:caller_invoice.rational('1e10000'),'integer/positive-integer spelling')) + # Deleting or poisoning author profile annotations leaves extraction intact. + changed=deepcopy(base);changed['paid_profiles']={'forward':{'1':0},'backward':{'1':999}} + changed['canonical']['local_profile']={'untrusted':'fabricated'} + actual=native_invoice.extract(changed) + need(all(actual['orientations'][d]['paid']==a['native']['orientations'][d]['paid'] and + actual['orientations'][d]['helpers']==a['native']['orientations'][d]['helpers'] for d in ('forward','backward')), + 'Declared histograms do not drive extraction') + return rejections + + +def cli_check(case): + with tempfile.TemporaryDirectory(prefix='source-invoice-') as directory: + root=Path(directory);claim_file=root/'CLAIM.json';claim_file.write_text(json.dumps(case['claim'])) + invoice=root/'INVOICE.json';audit=root/'AUDIT.json' + cmd=[sys.executable,'-I','-B',str(HERE/'conform.py'),'--word',str(HERE/case['file']), + '--controller',str(HERE/'source/CONTROLLER.json'),'--expect',str(claim_file), + '--write-invoice',str(invoice),'--write-audit',str(audit)] + p=subprocess.run(cmd,capture_output=True,text=True,timeout=45) + need(p.returncode==0,'CLI conformance and opt-in exports: '+p.stderr) + stdout=conform.parse(p.stdout.encode());need(stdout['status']=='PASS_SOURCE_INVOICE_CONFORMANCE','CLI reports a checked claim') + need(conform.read(invoice)==case['claim']['invoice'],'CLI preflight-compatible complete invoice') + blob=conform.read(audit);need(blob['source_binding']==case['claim']['source_binding'],'CLI audit source binding') + try:conform.write_new(invoice,{}) + except FileExistsError:pass + else:raise ValueError('CLI output overwrite accepted') + return {'status':stdout['status'],'audit_sha256':conform.digest(blob),'invoice_sha256':conform.digest(conform.read(invoice))} + + +def run(): + authenticate();controller=conform.read(HERE/'source/CONTROLLER.json') + cases=conform.read(HERE/'CALIBRATIONS.json')['cases'];audits={};words={};results={} + for case in cases: + name=case['name'];words[name]=conform.read(HERE/case['file']) + audit=conform.extract(words[name],controller);conform.compare(audit,case['claim']);audits[name]=audit + result=conform.summary(audit,True);result['surrendered_target_ledger']=ledger_check(audit) + results[name]=result + a,b=audits['PR5383'],audits['PR5387'] + need(a['invoice']==b['invoice'] and a['source_binding']!=b['source_binding'],'Same recursive invoice, different source programs') + need(b['native']['orientations']['backward']['scalar_allowance']- + a['native']['orientations']['backward']['scalar_allowance']==32,'Actual scalar-cost difference is retained') + need(results['PR5383']['surrendered_target_ledger']=={'9':128},'Every lost target is traced to owned source roles and actual call sites') + return {'status':'PASS_SOURCE_INVOICE_CONFORMANCE_SUITE','calibrations':results, + 'controls':controls(audits,words,controller),'cli':cli_check(cases[1]), + 'scope':'Source-protocol and recursive invoice conformance; separate ordinary costs, phase, precision/tape, compiler and analytic obligations remain.'} + + +if __name__=='__main__': + parser=argparse.ArgumentParser(description=__doc__);parser.add_argument('--emit',action='store_true');args=parser.parse_args() + result=run() + if not args.emit: + expected=conform.read(HERE/'RESULT.json') + need(caller_invoice.canonical(result)==caller_invoice.canonical(expected),'Complete typed deterministic receipt') + print(json.dumps(result,indent=2,sort_keys=True))