diff --git a/research/rank7-complete-native-boundary/PROOF.md b/research/rank7-complete-native-boundary/PROOF.md new file mode 100644 index 0000000000..c1a3cd7c1e --- /dev/null +++ b/research/rank7-complete-native-boundary/PROOF.md @@ -0,0 +1,105 @@ +# Complete finite source/native boundary + +## Statement and scope + +Fix the two literal PR2979 words pinned in SOURCES.json, the emitted programs +and recipes authenticated by their retained native receipt, and either the +forward or inverse-transpose orientation. Assume physical rational scalar +operations, COPY/CLEAR in the declared common charts, and fresh zero allocation +with the stated lifetime contract. + +Every native event in the complete emitted stream realizes the source-bound +chart operator, including its global phase. In normalized source coordinates, +each of the 408 original dirty helpers ends at its own arbitrary input, with +no dependence on the other original inputs. Every one of the 91 private arrays +is zero immediately before its actual free. These statements hold for arbitrary +source, target and dirty-helper arrays. + +The statement is a finite conditional macro/native refinement. A restored +normalized helper is not automatically a physical identity on its entire array. +Its physical entrance/terminal frames and the supplied residual Fourier child +remain charged. The result supplies no physical backing, allocation fit, +precision, all-size implementation or new exponent. + +## Eventwise native realization + +The retained PR3038 source decoder reconstructs the whole source schedule, +including rational operations, both center paths, ordered charts, warps, +private lifetimes and wrapper positions. It independently decodes the emitted +program, checks every source metadata field it consumes and requires equality +of the complete event sequences. No dependency pruning occurs in this audit. + +For every native event, the retained native selector assigns its literal +child, warp, ordinary adapter or residual-wrapper class. A class is checked +against the exact serialized recipe selected by that event. The separate +Gaussian-integer kernel compares all 512 basis columns with the source-derived +reference, including global phase. Equality on a basis implies equality on every +array. Cached equality uses the entire candidate circuit, reference circuit, +selected record and orientation. A local frame number is not a global key. +The receipt retains every event association and every exact identity digest. + +For a residual with entrance E and terminal U, the reference is T_U T_E^-1. +Both inverse wrappers are included in the checked sandwich, whose factor is +the coordinate Fourier transform on dim(U)-dim(E) axes. The inverse-transpose +orientation conjugates the complete chronological circuit. It does not reverse +execution order or replace inverse transpose with adjoint. + +Induction over the complete event sequence now gives the source macro's +normalized semantics, subject to the stated physical scalar and allocation +contracts. Common-chart incidence and nested center paths are checked by the +source decoder. Native identities do not implement an unpriced scalar or +physical allocator. + +## Helper and private observations + +The new forward observer assigns an independent formal input to every original +live role and zero to each private allocation. It propagates exact rational +linear combinations over the free algebra of signed warp words. Only adjacent +inverse warp symbols cancel. ADD, SCALE, COPY and CLEAR have their literal +semantics. Each actual private free requires the zero row before deletion. +At the end, every helper row must be exactly its own input. + +This is stronger than testing a collection of numerical arrays. A formal +identity remains an identity after substituting arbitrary arrays and the +actual native warp operators. It uses no accidental commuting relations. +The source decoder/native selector and the forward algebra arithmetic are +credited reused tools. Their existing independence is reused, not newly claimed. + +A second, retained algorithm pulls each helper output covector backwards +through the original source word. It swaps and negates directed shears for +inverse transpose and retains noncommutative operator order. The projected row +on the 632 original inputs must be the corresponding helper basis row. Terms +from private entrances are retained in the receipt but those entrances are +zero by the allocation premise. This source check is separate from the emitted +forward observer. It does not replace the native phase checks. + +## Added coverage and failure witnesses + +PR3038 checks the helper249/private953 cone. PR3238 adds every actual private +free. This audit takes every event in the complete stream and every original +dirty-helper output. Exact class-set subtraction against the two pinned prior +receipts identifies the additional native classes and their event occurrences. +The previous classes are checked again along with the added classes. +Here RESULT.prior_delta.new_native_events counts occurrences of added classes, +not the total newly included native events. The latter also includes new +occurrences of old classes. These coverage deltas are relative to PR3238; the +group-A and group-B direct-path audits already cover selected identities. + +For each orientation, a literal helper ADD outside the prior expanded cone has +its coefficient sign flipped. All 91 private frees and helper249 still pass +under the retained observer. The complete helper-output check rejects it. +For example, changing the sign at inverse-transpose event 21,886 gives +helper287 the row x287-2*x286. +Taking x286 nonzero and x287 zero witnesses failure while the old roots pass. A +separate fault changes the global phase of a newly covered native child recipe; +the all-column comparison rejects it. These mutants are failure controls, not +reported faults in the original construction. + +## Remaining obligations + +The intended source/target endpoint identities, their application, physical +scalar/COPY/CLEAR implementations, storage and movement, the actual owner fill, +precision/prefix/tape costs, both supplier caps, outer coupling and all-size +compiler/analytic premises remain separate. No selected result is modified. +This proof is an exact finite argument backed by Python replay; independent +human and formal proof-kernel review are unclaimed. diff --git a/research/rank7-complete-native-boundary/README.md b/research/rank7-complete-native-boundary/README.md new file mode 100644 index 0000000000..51ffcc5870 --- /dev/null +++ b/research/rank7-complete-native-boundary/README.md @@ -0,0 +1,112 @@ +# Complete PR2979 source/native boundary + +This finite audit checks both complete emitted native streams and all 408 +arbitrary dirty-helper outputs of the original PR2979 construction, in both +orientations. It extends PR3038's single endpoint cone and PR3238's all-private +free cone. The source word, allocation and paid costs are unchanged. No new +supplier, kappa or selected-frontier change is claimed. + +The precise statement and composition argument are in [PROOF.md](PROOF.md). +[SOURCES.json](SOURCES.json) pins every consumed input to canonical main +`6f100d4bb5083f8c35d96fd95a539811c62f245c`, priority revision 6. The original +construction is PR2979 at `be191346391661f4d35fc0d1508d0a6029572576`. + +## Added coverage + +Each complete source stream has 22,748 events. Every native event is selected +from that complete stream, without dependency pruning. Both orientations have +3,481 classes per provider. Against PR3238's exact class union, that adds 833 +forward classes and 314 inverse-transpose classes. Those new classes cover +998 and 317 event occurrences. In total, native event coverage increases from +3,717/4,537 to 5,125 in each orientation, adding 1,408 forward and 588 +inverse-transpose event occurrences. This also includes new occurrences of +previously checked classes. Existing classes are replayed too. These increments +are relative to PR3238, not claims that every individual identity is new. +The group-A and group-B direct-path audits already cover selected identities. + +The new forward observer checks all 408 final helper rows and every actual +private free over exact rational free-warp expressions. A separate retained +backward source-covector algorithm checks every original helper output. +Native classes are checked on all 512 address columns, including global phase. +The residual Fourier factors, all 91 private families and the full local +paid profile remain charged. + +A literal helper ADD outside the prior expanded cone can have its sign flipped +while all earlier private-free and helper249 roots still pass. The complete +helper check rejects that mutant. A global-phase fault in a newly covered +native class also rejects. At inverse-transpose event 21,886, the helper ADD +sign change leaves helper287 equal to x287-2*x286 while all older roots pass. +These are semantic failure controls, not defects reported in the original +word. Exact indices, rows and class/event associations +are retained in the two compressed RESULT files. + +The source decoder, native selector, exact Gaussian kernel, forward arithmetic +and backward covector machinery are credited reused checking tools. This is a +coverage extension using those independent implementations, not a claim to +have independently reimplemented them. + +## Reproduce + +Use Python 3.12 with `numpy==2.3.5`, which the unchanged producer requires. +The new proof calculations and exact kernel use the standard library. Run +commands sequentially with an external session-owned temporary directory: + +```sh +mkdir -p "$RUN_ROOT/scratch" +TMPDIR="$RUN_ROOT/scratch" python3.12 -Werror -B scripts/research_package.py \ + --package research/rank7-complete-native-boundary +``` + +The registered hook runs eight behavioral groups, then a fresh source/native +replay for each provider. Direct replay is: + +```sh +TMPDIR="$RUN_ROOT/scratch" python3.12 -I -O -Werror -B \ + research/rank7-complete-native-boundary/verify.py --provider base +TMPDIR="$RUN_ROOT/scratch" python3.12 -I -O -Werror -B \ + research/rank7-complete-native-boundary/verify.py --provider extra +``` + +Each command authenticates inputs before executing retained code, generates +fresh recipes, checks source/event and retained artifact equality, executes +semantic controls and compares the complete deterministic receipt. It prints +`PASS_COMPLETE_SOURCE_NATIVE_BOUNDARY provider=base` or `provider=extra`. +`--emit` prints a fresh uncompressed receipt. `--artifacts DIR` reuses supplied +producer artifacts but still authenticates and checks all identities; that mode +does not claim a fresh producer execution. Replay needs no network or Git. + +## Limits + +The theorem is conditional on physical rational scalar, COPY/CLEAR and +fresh-zero allocation contracts. Normalized restoration includes paid native +residual Fourier children; it is not a physical identity on every helper's +whole array. Actual backing and owner geometry, movement, storage, +precision/prefix/tape, the complete intended source/target application, +both supplier caps, outer coupling and all-size/compiler/analytic obligations +are separate. Independent human and formal proof-kernel review are unclaimed. + +## Open next questions + +The next useful step is to join a newly covered helper endpoint and its +recursive residual to the actual owner placement and paid physical scalar +implementation. This determines whether the checked local operator fits the +complete invoice. Unknown physical and precision costs block admission. +Another native-class census of this fixed word is unnecessary. + +## Credit + +Nick Petalas. Apache-2.0, following the repository license. Frozen predecessor +sources and their notices remain unchanged. + +Marius-Paul Dumitrean supplied PR2979 and PR2942. ToikY supplied PR3038's +source/native machinery and Sagar Thakrar supplied its separate exact +Gaussian-integer kernel. commdata2338 supplied PR3238's forward free-algebra +arithmetic and all-private-free coverage. Nick Petalas supplied +PR2993/3006/3008/3014 and the backward covector engine. The group-A and group-B +native/interface audits are credited complementary checks. Retain Jeremy +Kothe's frame/native/cleanup and rewrite credit, Mason Hale and Jeremy +Diviney's extraction lineage, icekylinx's native compiler, Ross Richardson's +packing/invoice audits, and Tekalign, Yiyang Lu, Dugongue, Cinna Davis, +DreamingOfClouds, Douglas Colkitt and the source packages' geometry lineage. + +[Canonical scoped claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/2612#discussioncomment-19009367). diff --git a/research/rank7-complete-native-boundary/RESULT-base.json.gz b/research/rank7-complete-native-boundary/RESULT-base.json.gz new file mode 100644 index 0000000000..9e0de9a4e9 Binary files /dev/null and b/research/rank7-complete-native-boundary/RESULT-base.json.gz differ diff --git a/research/rank7-complete-native-boundary/RESULT-extra.json.gz b/research/rank7-complete-native-boundary/RESULT-extra.json.gz new file mode 100644 index 0000000000..25a6c74587 Binary files /dev/null and b/research/rank7-complete-native-boundary/RESULT-extra.json.gz differ diff --git a/research/rank7-complete-native-boundary/SOURCES.json b/research/rank7-complete-native-boundary/SOURCES.json new file mode 100644 index 0000000000..a48d62aba4 --- /dev/null +++ b/research/rank7-complete-native-boundary/SOURCES.json @@ -0,0 +1,138 @@ +{ + "schema_version": 1, + "base_commit": "6f100d4bb5083f8c35d96fd95a539811c62f245c", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + }, + { + "path": "research/frontier1094-recipes-exact-seed76/clifford.py", + "usage": "input", + "git_blob": "6f1e6a38febde7eb7a7341d317522e6650d84408", + "sha256": "d5e42ddabd141b7bfbd70fe13908f3c3a06aeccebeab90623596bfb1988b97fb" + }, + { + "path": "research/rank7-joint-endframes/data/WORD-base.json.gz", + "usage": "input", + "git_blob": "d9aa96a93fea5f7395e7783aef0bc117c0a0ae89", + "sha256": "abaf67bfcb257528658c906b612f57025617592bd7889828f92b97a5f4f4300d" + }, + { + "path": "research/rank7-joint-endframes/data/WORD-extra.json.gz", + "usage": "input", + "git_blob": "74f6cb64595c21f7726ae77e69437868620bdcee", + "sha256": "e0eaf64c4d5d324693d43889bce1b9e53e8da00402105c8c978fd102f208bed7" + }, + { + "path": "research/rank7-joint-endframes/evidence/FULL-NATIVE-RECEIPT.json", + "usage": "input", + "git_blob": "87ac21d0878479877bb75961b3c054843711d4d4", + "sha256": "6d27c89d5e3a2c7f28387e4b20c462b0dff6c9fa92aacdde715d4b29cc286d41" + }, + { + "path": "research/rank7-peer-private-free-audit/RESULT-base.json", + "usage": "input", + "git_blob": "3a7bd808ad6d25ed69a3a773a3fe6f39ffbac195", + "sha256": "adb6b7de5dd70db6c44174c5e8dcd98f56a9a3fcaea86cddbe413f8f5eb6fb40" + }, + { + "path": "research/rank7-peer-private-free-audit/RESULT-extra.json", + "usage": "input", + "git_blob": "30ef75fd1e032dd18a570e81263e7c3e43bc7274", + "sha256": "5d41601ed7dff21f7b9a6e2c0ae5c7ee099f0462330ee61e6d2defbeb828ab73" + }, + { + "path": "research/rank7-peer-private-free-audit/lifetimes.py", + "usage": "input", + "git_blob": "aa60e87471293b7c0b6e5b9dee6ce9303f58916b", + "sha256": "51a93c571ccfc697d890940552b35f5c76161b059b451fb0cc83221e8faa201c" + }, + { + "path": "research/rank7-v45-native-cone-seed78/RESULT-base.json", + "usage": "input", + "git_blob": "9f78923a15b9dc13fbf5d78b7c94a75a3f7083ad", + "sha256": "5cea9b1f2c51b07d62a225100ca2abbcb710943f2d88aaedab0619d214297b40" + }, + { + "path": "research/rank7-v45-native-cone-seed78/RESULT-extra.json", + "usage": "input", + "git_blob": "a2a293d5157846a80068bace94ce26e647b54a80", + "sha256": "86b999e314f5d66ce7db7171b1cda9e78c2e5b69bd7f51bee189cac963c3b958" + }, + { + "path": "research/rank7-v45-native-cone-seed78/audit.py", + "usage": "input", + "git_blob": "8841684e69da3beac4c5461630f9b549807f1bb7", + "sha256": "175d0e7bb67b3a4c48080c2189451a798f747d8ae486af949528acc59e404ed3" + }, + { + "path": "research/rank7-v45-native-cone-seed78/native.py", + "usage": "input", + "git_blob": "1a86a5649bdf5a409eac6f583cd2962a0f61c7e8", + "sha256": "3598214e804a042006d2343801bfbf94eaf4d4ff10810bb41081b94d53865171" + }, + { + "path": "research/rank7-v45-native-cone-seed78/source.py", + "usage": "input", + "git_blob": "dbe5c740991f399e7070bfe31431aad87b05f266", + "sha256": "879357b502b007ca7d8b17e4cc542750a5b9d9702bbae000bb3880c0179d6834" + }, + { + "path": "research/rank7-v45-native-cone-seed78/support.py", + "usage": "input", + "git_blob": "26f8526137ab404009ac06c02816b538bf42beaa", + "sha256": "ef58c76411c62a9baf263ab1a275e056de8dd2fec8f7d50d0cebb60765af373e" + }, + { + "path": "research/rank7-v45-native-endpoint/endpoints.py", + "usage": "input", + "git_blob": "79c2495d2e0208ecf4d6f0a53f5f108a54217a47", + "sha256": "d5e8b8bf640cc6283141065995ade7f475b7ab3116ea01ce682765b5f84405c0" + }, + { + "path": "research/two-sided-helper-extraction/vendor/fastnative/vendor/native/new/code/borrow/bw_adapters.py", + "usage": "input", + "git_blob": "82beaa9c1d13bcd5f79d0a5e10e8a10733eac347", + "sha256": "c5907050a9a7fa36d4fcba3ad4fe440d1bec2063360c095013891785ba65c3ce" + }, + { + "path": "research/two-sided-helper-extraction/vendor/fastnative/vendor/native/new/code/borrow/bw_emit.py", + "usage": "input", + "git_blob": "6d47f63ab7a533941b3881bbfd3ae4dac5f76932", + "sha256": "99b59a6fa3feda86785e4225157dcb1a6169d256cec4f5e0acc9cea7a701df76" + }, + { + "path": "research/two-sided-helper-extraction/vendor/fastnative/vendor/native/new/code/borrow/bw_gauss.py", + "usage": "input", + "git_blob": "1ff29dfb244e2114de8e586a450ae9fb70308d58", + "sha256": "0884b14d6d77cde419a3c773ad9b21d0d18de1e6e20e6b6d5add458ed32ba4cb" + }, + { + "path": "research/two-sided-helper-extraction/vendor/fastnative/vendor/native/new/code/borrow/bw_phases.py", + "usage": "input", + "git_blob": "99f351785ebca5fbf3336bedcd7b48bac9c255e5", + "sha256": "9d1a620e26715f4c42fd0347ecc14ef5a4a9031867869b64e8bae4d8526a821e" + }, + { + "path": "research/two-sided-helper-extraction/vendor/fastnative/vendor/native/new/code/borrow/bw_transport.py", + "usage": "input", + "git_blob": "08248542b18864c94a5ac050c8669f68519838e1", + "sha256": "9818e08b819310b40f1441b89be8c4369584a5b3fa5dfe9b86b1df9a7f5d6a76" + }, + { + "path": "research/two-sided-helper-extraction/vendor/fastnative/vendor/native/new/code/borrow/vendor/clifford/clifford_exact.py", + "usage": "input", + "git_blob": "166841a037f069249f6f7f6dedb89248812f59e2", + "sha256": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962" + } + ] +} diff --git a/research/rank7-complete-native-boundary/TASK.json b/research/rank7-complete-native-boundary/TASK.json new file mode 100644 index 0000000000..851e3d6362 --- /dev/null +++ b/research/rank7-complete-native-boundary/TASK.json @@ -0,0 +1,92 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 6, + "base_commit": "6f100d4bb5083f8c35d96fd95a539811c62f245c", + "original_card": { + "id": "independent-moment", + "question": "Does one changed supplier or assembly claim lack a source-bound independent check of a specific new implication?", + "starting_points": [ + "certificates/selected-result.json", + "research/rank7-joint-endframes/README.md", + "docs/research/research-family-status.md" + ], + "methods": [ + "Independently reconstruct a coordinated frame/circuit change and its single-change control, then derive the complete rank and physical ledger.", + "Implement certified moment inequalities through a different exact enclosure method." + ], + "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": "Read #2979 joint rank-7 end-frame proposal and the revision-6 evidence status. Its claimed kappa is not selected. Compare coordinated changes with the losing single-change controls and locate the complete physical ledger; an aggregate moment alone does not validate the mechanism.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Prioritize a bounded independent audit of #2979: reconstruct one joint group and its single-lowering control, check the declared frames/chronology, then trace changed children, idle widths and cleanup buffers into the complete invoice and both supplier caps. Choose one still-missing implication after checking existing audits. Stop with exact unresolved dependencies if full admission exceeds the session; do not launch a new lowering census on an unvalidated premise or substitute extra root digits for mechanism checking.", + "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.", + "Promoting #2979 from merged source archive to validated supplier solely from author PASS receipts or aggregate pricing." + ], + "overlap_terms": [ + "independent moment", + "rank histogram", + "exact enclosure", + "2979", + "rank7 joint endframes", + "paired extraction", + "joint lowering" + ] + }, + "scope_status": "refined", + "actual_scope": "Complete source-native realization for both literal PR2979 streams and all 408 dirty-helper output restorations in both orientations.", + "scope_change_reason": "PR3038 and PR3238 leave the original dirty-helper output family and unpruned full stream outside their scopes. Reuse their independent checker machinery with explicit credit; no new checker independence claim.", + "bottleneck_link": "The joint rank-seven paid profile cannot be used through a source/native boundary whose dirty-helper outputs and complete native stream were not covered. This closes that finite implication while leaving physical tariffs and full admission separate.", + "budget_minutes": 60, + "stop_rule": "Check the complete finite source-native boundary; stop at any mismatch. No word or packing search, cost adoption or kappa claim.", + "outcome": "partial", + "evidence": "RESULT-base.json.gz and RESULT-extra.json.gz; exact full class/event associations, all 408 source/emitted helper observations, actual private frees and new-coverage phase/helper controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can the checked complete local source/native boundary be realized on the actual final owner fill with paid scalar/COPY/CLEAR and storage/precision contracts?", + "why_it_matters": "Exact local operator identities do not show that the claimed paid profile is physically affordable or satisfies the outer supplier contract.", + "first_step": "Join one newly covered helper endpoint and its actual recursive residual to its source-bound owner placement and physical scalar implementation, retaining the complete invoice.", + "blocked_by": "Actual backing, movement and scalar/precision contracts and complete supplier/outer review remain separate. Another fixed-word native-class census is unnecessary." + } + ], + "existing_checks": [ + { + "pr": 3038, + "scope": "One source-bound helper/private dependency cone; source decoder, native selector, exact kernel and comparison cache explicitly reused.", + "head": "c7d0d7be056ba77fda1c168641b2bcffb10cf43d" + }, + { + "pr": 3238, + "scope": "All 91 actual private frees and expanded native cone; forward algebra arithmetic and exact coverage receipts reused.", + "head": "3c689aac34ff240f82e27dcc7f0247b96b8676af" + }, + { + "pr": 3245, + "scope": "Isolated cleanup arbitrary dirty/private identity; corroborative context, not replayed.", + "head": "171c95e2940341e56377d655a162635fa3caedfa" + }, + { + "pr": 3411, + "scope": "Group B direct native residual/width-to-fill binding; contextual pending work, not used as an acceptance dependency.", + "head": "24a291a502fc93e1bf7bdbb2d7b351ce75f0bee8" + }, + { + "path": "research/rank7-group-a-entrance-audit", + "scope": "Five direct mixed-entrance paths and invoice join; contextual predecessor, no new discovery of their local identities." + } + ] +} diff --git a/research/rank7-complete-native-boundary/VALIDATION.json b/research/rank7-complete-native-boundary/VALIDATION.json new file mode 100644 index 0000000000..e614e05d59 --- /dev/null +++ b/research/rank7-complete-native-boundary/VALIDATION.json @@ -0,0 +1,97 @@ +{ + "schema_version": 1, + "scientific_base": "6f100d4bb5083f8c35d96fd95a539811c62f245c", + "original_construction_head": "be191346391661f4d35fc0d1508d0a6029572576", + "environment": { + "python": "CPython 3.12.15", + "numpy": "2.3.5", + "platform": "macOS arm64", + "numeric_threads": 1 + }, + "checks": { + "fresh_registered_replay": "PASS_REGISTERED_RESEARCH_PACKAGE research/rank7-complete-native-boundary outcome=partial", + "behavioral_groups": 8, + "normal_and_optimized_tests": "passed with isolated Python and warnings as errors", + "native_identities_total": 13924, + "columns_per_identity": 512, + "original_source_lineage_files_equal": 9, + "ruff": "E,F,B,UP,SIM,I and format check passed", + "new_python_maximum_function_lines": 46 + }, + "results": { + "base": { + "native_identities": 6962, + "events_per_orientation": [ + 22748, + 22748 + ], + "helper_outputs_per_orientation": [ + 408, + 408 + ], + "frees_per_orientation": [ + 91, + 91 + ], + "result_sha256": "11f4b51da791e4280ce1e184c8c2da9a6c78f320054f5b566d2db6e26010c7c4", + "decoded_sha256": "ab97522037df47f9dda00c2253ec789cda2aa82dc487803bb2cc64b4808155b0" + }, + "extra": { + "native_identities": 6962, + "events_per_orientation": [ + 22748, + 22748 + ], + "helper_outputs_per_orientation": [ + 408, + 408 + ], + "frees_per_orientation": [ + 91, + 91 + ], + "result_sha256": "b492adcb4448046cc27984f17224156fa2d5df9725595eeb29933f45bc1a3767", + "decoded_sha256": "4e3f82dd15337915e679835d428d6c22062737832c1fd9c8c0946907f7e46cd1" + } + }, + "coverage": { + "base": { + "backward": { + "complete_native_event_occurrences": 5125, + "prior_native_event_occurrences": 4537, + "total_added_native_event_occurrences": 588, + "added_classes": 314, + "occurrences_in_added_classes": 317 + }, + "forward": { + "complete_native_event_occurrences": 5125, + "prior_native_event_occurrences": 3717, + "total_added_native_event_occurrences": 1408, + "added_classes": 833, + "occurrences_in_added_classes": 998 + } + }, + "extra": { + "backward": { + "complete_native_event_occurrences": 5125, + "prior_native_event_occurrences": 4537, + "total_added_native_event_occurrences": 588, + "added_classes": 314, + "occurrences_in_added_classes": 317 + }, + "forward": { + "complete_native_event_occurrences": 5125, + "prior_native_event_occurrences": 3717, + "total_added_native_event_occurrences": 1408, + "added_classes": 833, + "occurrences_in_added_classes": 998 + } + } + }, + "limits": [ + "Finite conditional native/macro refinement; physical rational scalar/COPY/CLEAR and fresh-zero allocation contracts remain premises.", + "No new word, allocation, tariff, supplier, kappa or selected-frontier change.", + "Physical backing, owner fit, precision/tape, intended source/target endpoint application, supplier/outer and all-size obligations are separate.", + "Independent human and formal proof-kernel review are unclaimed." + ] +} diff --git a/research/rank7-complete-native-boundary/VERIFY.json b/research/rank7-complete-native-boundary/VERIFY.json new file mode 100644 index 0000000000..679ced56dc --- /dev/null +++ b/research/rank7-complete-native-boundary/VERIFY.json @@ -0,0 +1,72 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [ + "numpy==2.3.5" + ], + "inputs": [ + "research/frontier1094-recipes-exact-seed76/clifford.py", + "research/rank7-joint-endframes/data/WORD-base.json.gz", + "research/rank7-joint-endframes/data/WORD-extra.json.gz", + "research/rank7-joint-endframes/evidence/FULL-NATIVE-RECEIPT.json", + "research/rank7-peer-private-free-audit/RESULT-base.json", + "research/rank7-peer-private-free-audit/RESULT-extra.json", + "research/rank7-peer-private-free-audit/lifetimes.py", + "research/rank7-v45-native-cone-seed78/RESULT-base.json", + "research/rank7-v45-native-cone-seed78/RESULT-extra.json", + "research/rank7-v45-native-cone-seed78/audit.py", + "research/rank7-v45-native-cone-seed78/native.py", + "research/rank7-v45-native-cone-seed78/source.py", + "research/rank7-v45-native-cone-seed78/support.py", + "research/rank7-v45-native-endpoint/endpoints.py", + "research/two-sided-helper-extraction/vendor/fastnative/vendor/native/new/code/borrow/bw_adapters.py", + "research/two-sided-helper-extraction/vendor/fastnative/vendor/native/new/code/borrow/bw_emit.py", + "research/two-sided-helper-extraction/vendor/fastnative/vendor/native/new/code/borrow/bw_gauss.py", + "research/two-sided-helper-extraction/vendor/fastnative/vendor/native/new/code/borrow/bw_phases.py", + "research/two-sided-helper-extraction/vendor/fastnative/vendor/native/new/code/borrow/bw_transport.py", + "research/two-sided-helper-extraction/vendor/fastnative/vendor/native/new/code/borrow/vendor/clifford/clifford_exact.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 60, + "checks": "Eight behavioral groups, including actual source helper observations, missing restoration, COPY/CLEAR, warp orientation, lifetime/zero faults and source authentication before code execution." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{package}/verify.py", + "--provider", + "base" + ], + "timeout_seconds": 540, + "checks": "Complete source-bound native stream and all dirty-helper output identities, exact coverage delta and semantic controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{package}/verify.py", + "--provider", + "extra" + ], + "timeout_seconds": 540, + "checks": "Complete source-bound native stream and all dirty-helper output identities, exact coverage delta and semantic controls." + } + ] +} diff --git a/research/rank7-complete-native-boundary/boundary.py b/research/rank7-complete-native-boundary/boundary.py new file mode 100644 index 0000000000..3c256df8f4 --- /dev/null +++ b/research/rank7-complete-native-boundary/boundary.py @@ -0,0 +1,123 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Complete normalized helper observations and exact coverage comparisons.""" + +from collections import Counter +from fractions import Fraction + + +def require(ok, reason): + if not ok: + raise ValueError(reason) + + +def scalar(rows, active, event, algebra): + op, target = event[1], event[1][1] + used = op[1:3] if op[0] in ("add", "copy") else op[1:2] + require( + all(not r.startswith("Z") or r in active for r in used), + "private use outside lifetime", + ) + if op[0] == "clear": + require(target in rows or target.startswith("C"), "CLEAR target") + rows[target] = {} + elif op[0] == "copy": + require(target != op[2], "distinct COPY operands") + rows[target] = dict(rows[op[2]]) + elif op[0] == "scale": + q = Fraction(op[2], op[3]) + require(q != 0, "nonzero scale") + rows[target] = {k: q * v for k, v in rows[target].items()} + else: + require(op[0] == "add" and target != op[2], "distinct ADD operands") + rows[target] = algebra.merge(rows[target], rows[op[2]], Fraction(op[3], op[4])) + + +def normalized(events, original, helpers, backward, algebra): + """All original inputs are formal variables; allocated private inputs are zero.""" + require(len(events) <= 100000 and len(original) == 632, "finite stream domain") + rows = {r: {(r, ()): Fraction(1)} for r in original} + active, allocated, frees, post = set(), set(), [], {} + for index, event in enumerate(events): + tag = event[0] + if tag == "zero_buffer": + action, role = event[1:] + if action == "alloc": + require(role not in allocated and role not in rows, "fresh private") + active.add(role) + allocated.add(role) + rows[role] = {} + else: + require(action == "free" and role in active, "matched private free") + require(not rows[role], "nonzero private at actual free") + frees.append([role, index]) + active.remove(role) + del rows[role] + elif tag == "scalar": + scalar(rows, active, event, algebra) + elif tag == "warp": + role, op = event[1:3] + if backward: + op = (1 if op > 0 else -1) * (1000000 + abs(op)) + rows[role] = algebra.warp(rows[role], op) + else: + require( + tag in ("phase", "climb", "center", "adapter", "residual_adapter"), + "known event kind", + ) + if tag == "residual_adapter" and event[1] == "post": + require(event[2] not in post, "unique helper post wrapper") + post[event[2]] = [index, algebra.encode(rows[event[2]])] + require(not active and len(frees) == len(allocated) == 91, "all 91 actual frees") + result = {r: algebra.encode(rows[r]) for r in sorted(helpers)} + bad = next(((r, v) for r, v in result.items() if v != [[r, [], "1"]]), None) + require(bad is None, "all dirty helper outputs restored: " + repr(bad)) + return {"helper_outputs": result, "post_wrappers": post, "private_frees": frees} + + +def source_rows(engine, word, helpers): + """A distinct retained backward algorithm checks the original source word.""" + live = set(range(704)) - set(word["removed"]) + buffers = {704 + int(h) for h in word["helper_final"]} + gates, result = engine.program(word), {} + for dual in (False, True): + rows = {} + for role in sorted(helpers): + index = int(role[1:]) + pulled = engine.endpoint(gates, index, dual, live, buffers) + projected = [r for r in pulled if r[0] in live] + require(projected == [(index, (), "1")], "source helper restoration") + rows[role] = [[r, list(w), q] for r, w, q in pulled] + result["backward" if dual else "forward"] = rows + return result + + +def prior_delta(native, events, canonical, previous, old_pair, orientation): + full = native.classes( + events, [i for i, e in enumerate(events) if e[0] != "phase"], canonical + ) + old = previous["orientations"][orientation]["native"] + earlier = old_pair["orientations"][orientation]["native"]["associations"] + old_classes = {tuple(row["class"]) for row in earlier} + old_classes.update(tuple(row["class"]) for row in old["new_class_associations"]) + require(len(old_classes) == old["expanded_classes"], "prior union class count") + require(old_classes <= set(full), "prior classes belong to complete stream") + new = sorted(set(full) - old_classes, key=native.stable_key) + return { + "prior_classes": len(old_classes), + "complete_classes": len(full), + "new_classes": [list(k) for k in new], + "new_native_events": sum(len(full[k]) for k in new), + "complete_native_events": sum(len(v) for v in full.values()), + } + + +def paid_profile(events): + return dict( + sorted( + Counter( + e[5] if e[0] == "climb" else e[4] + for e in events + if e[0] in ("climb", "center") + ).items() + ) + ) diff --git a/research/rank7-complete-native-boundary/controls.py b/research/rank7-complete-native-boundary/controls.py new file mode 100644 index 0000000000..cbd48bee72 --- /dev/null +++ b/research/rank7-complete-native-boundary/controls.py @@ -0,0 +1,97 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Semantic faults outside the old private-free/native coverage.""" + +from copy import deepcopy + +import boundary + + +def rejected(action, text): + try: + action() + except ValueError as error: + boundary.require(text in str(error), "wrong semantic rejection: " + str(error)) + return str(error) + raise ValueError("semantic fault accepted: " + text) + + +def phase(native, kernel, canonical, recipes, adapters, backward, delta): + key = next(tuple(k) for k in delta["new_classes"] if k[0] == "child") + changed = dict(recipes) + changed["children"] = list(recipes["children"]) + index = next( + i + for i, row in enumerate(recipes["children"]) + if (row["old"], row["new"]) == key[1:] + ) + row = deepcopy(recipes["children"][index]) + row["left"]["phase"] = (row["left"]["phase"] + 1) % 4 + changed["children"][index] = row + reason = rejected( + lambda: native.check(kernel, key, canonical, changed, adapters, backward), + "exact native class mismatch", + ) + return {"class_outside_prior_native_cones": list(key), "rejection": reason} + + +def helper(events, original, helpers, backward, algebra, previous, orientation): + ranges = previous["orientations"][orientation]["expanded"]["event_ranges_half_open"] + covered = {i for lo, hi in ranges for i in range(lo, hi)} + candidates = [ + i + for i, e in enumerate(events) + if i not in covered + and e[0] == "scalar" + and e[1][0] == "add" + and e[1][1] in helpers + and e[1][1] != "L249" + and e[1][2].startswith("L") + ] + boundary.require(candidates, "uncovered actual helper ADD exists") + # A single actual last uncovered helper write has no path to the old roots. + index = candidates[-1] + changed = list(events) + changed[index] = deepcopy(events[index]) + changed[index][1][3] *= -1 + old = algebra.values(changed, original, backward) + boundary.require( + old["helper249"] == [["L249", [], "1"]], "old helper root still passes" + ) + boundary.require( + all(not r["value"] for r in old["frees"]), "all old private roots still pass" + ) + reason = rejected( + lambda: boundary.normalized(changed, original, helpers, backward, algebra), + "all dirty helper outputs restored", + ) + return { + "event_outside_prior_expanded_cone": index, + "original_event": events[index], + "mutant_event": changed[index], + "old_helper_and_91_frees_pass": True, + "rejection": reason, + } + + +def run(modules, data, events, metadata, helpers, previous, orientation, delta): + backward = orientation == "backward" + return { + "helper": helper( + events, + metadata["start"], + helpers, + backward, + modules["algebra"], + previous, + orientation, + ), + "phase": phase( + modules["native"], + modules["kernel"], + data["canonical_word"], + data["recipes"], + data["adapters"], + backward, + delta, + ), + } diff --git a/research/rank7-complete-native-boundary/io_support.py b/research/rank7-complete-native-boundary/io_support.py new file mode 100644 index 0000000000..585e9a23b4 --- /dev/null +++ b/research/rank7-complete-native-boundary/io_support.py @@ -0,0 +1,91 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Authenticate explicit inputs before loading credited checking/producer code.""" + +import gzip +import hashlib +import json +import sys +import types +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +PRIOR = "research/rank7-v45-native-cone-seed78/" +PEER = "research/rank7-peer-private-free-audit/" +LIMIT = 64 * 1024 * 1024 + + +def require(ok, reason): + if not ok: + raise ValueError(reason) + + +def unique(pairs): + value = dict(pairs) + require(len(value) == len(pairs), "duplicate JSON key") + return value + + +def read(path): + with path.open("rb") as stream: + raw = stream.read(LIMIT + 1) + require(len(raw) <= LIMIT, "input byte capacity") + return raw + + +def decode(raw): + return json.loads(raw, object_pairs_hook=unique) + + +def sha(raw): + return hashlib.sha256(raw).hexdigest() + + +def inputs(root=ROOT): + pins = decode(read(PACKAGE / "SOURCES.json"))["files"] + declared = decode(read(PACKAGE / "VERIFY.json"))["inputs"] + active = [r for r in pins if r["usage"] == "input"] + require(len(active) == len(declared) == len(set(declared)), "unique source closure") + require( + len(active) <= 32 and {r["path"] for r in active} == set(declared), + "exact declared source closure", + ) + blobs = {} + for row in active: + path = root / row["path"] + require(path.is_file() and not path.is_symlink(), "regular source file") + raw = read(path) + require(sha(raw) == row["sha256"], "source SHA256: " + row["path"]) + blobs[row["path"]] = raw + return blobs + + +def result(provider): + path = PACKAGE / ("RESULT-" + provider + ".json.gz") + with gzip.open(path, "rb") as stream: + raw = stream.read(LIMIT + 1) + require(len(raw) <= LIMIT, "decoded result capacity") + return decode(raw) + + +def load(blobs, path, name): + module = types.ModuleType(name) + module.__file__ = str(ROOT / path) + sys.modules[name] = module + exec(compile(blobs[path], str(ROOT / path), "exec"), module.__dict__) + return module + + +def modules(blobs): + result = { + name: load(blobs, PRIOR + name + ".py", "complete_native_" + name) + for name in ("source", "native", "audit", "support") + } + result["algebra"] = load(blobs, PEER + "lifetimes.py", "complete_native_algebra") + result["endpoints"] = load( + blobs, + "research/rank7-v45-native-endpoint/endpoints.py", + "complete_native_source_covectors", + ) + result["kernel"] = load(blobs, result["support"].KERNEL, "complete_native_kernel") + return result diff --git a/research/rank7-complete-native-boundary/test_verify.py b/research/rank7-complete-native-boundary/test_verify.py new file mode 100644 index 0000000000..657b994c92 --- /dev/null +++ b/research/rank7-complete-native-boundary/test_verify.py @@ -0,0 +1,132 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Behavioral checks for complete helper scope and source authentication.""" + +import copy +import gzip +import sys +import tempfile +import unittest +from pathlib import Path + +sys.path.insert(0, str(Path(__file__).resolve().parent)) +import boundary +import io_support as io + + +def fixture(): + original = {"L" + str(i) for i in range(632)} + helpers = {"L" + str(i) for i in range(224, 632)} + events = [["zero_buffer", "alloc", "Z" + str(i)] for i in range(91)] + events += [ + ["scalar", ["add", "L224", "L0", 1, 1], ()], + ["scalar", ["add", "L224", "L0", -1, 1], ()], + ] + events += [["zero_buffer", "free", "Z" + str(i)] for i in range(91)] + return events, original, helpers + + +class BoundaryTests(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.blobs = io.inputs() + cls.modules = io.modules(cls.blobs) + + def normalize(self, events, original, helpers, backward=False): + return boundary.normalized( + events, original, helpers, backward, self.modules["algebra"] + ) + + def test_all_outputs_positive(self): + events, original, helpers = fixture() + result = self.normalize(events, original, helpers) + self.assertEqual(len(result["helper_outputs"]), 408) + self.assertEqual(len(result["private_frees"]), 91) + + def test_helper_fault_without_private_fault(self): + events, original, helpers = fixture() + del events[92] + with self.assertRaisesRegex(ValueError, "all dirty helper outputs restored"): + self.normalize(events, original, helpers) + + def test_actual_source_all_helpers(self): + source, algebra = self.modules["source"], self.modules["algebra"] + for tag in ("base", "extra"): + raw = self.blobs[self.modules["support"].WORDS[tag]] + word = io.decode(gzip.decompress(raw)) + kept, original, _, _ = source.metadata(word) + helpers = {"L" + str(i) for i in kept if i >= 224} + for backward in (False, True): + result = boundary.normalized( + source.expected(word, backward), + original, + helpers, + backward, + algebra, + ) + self.assertEqual(len(result["helper_outputs"]), 408) + + def test_warp_cancellation_both_orientations(self): + events, original, helpers = fixture() + for backward in (False, True): + changed = ( + events[:91] + [["warp", "L224", 3], ["warp", "L224", -3]] + events[91:] + ) + self.normalize(changed, original, helpers, backward) + del changed[92] + with self.assertRaisesRegex( + ValueError, "all dirty helper outputs restored" + ): + self.normalize(changed, original, helpers, backward) + + def test_lifetime_and_zero_at_free(self): + events, original, helpers = fixture() + changed = copy.deepcopy(events) + changed.insert(91, ["scalar", ["add", "Z0", "L0", 1, 1], ()]) + with self.assertRaisesRegex(ValueError, "nonzero private at actual free"): + self.normalize(changed, original, helpers) + changed = copy.deepcopy(events) + changed.insert(92, ["zero_buffer", "free", "Z0"]) + with self.assertRaisesRegex(ValueError, "matched private free"): + self.normalize(changed, original, helpers) + + def test_copy_clear_and_scale(self): + rows = {"a": {("a", ()): 1}, "b": {("b", ()): 1}} + boundary.scalar( + rows, set(), ["scalar", ["copy", "a", "b"]], self.modules["algebra"] + ) + self.assertEqual(rows["a"], rows["b"]) + boundary.scalar( + rows, set(), ["scalar", ["scale", "a", -2, 3]], self.modules["algebra"] + ) + self.assertEqual(str(rows["a"][("b", ())]), "-2/3") + boundary.scalar( + rows, set(), ["scalar", ["clear", "a"]], self.modules["algebra"] + ) + self.assertEqual(rows["a"], {}) + with self.assertRaisesRegex(ValueError, "nonzero scale"): + boundary.scalar( + rows, set(), ["scalar", ["scale", "a", 0, 1]], self.modules["algebra"] + ) + + def test_source_bytes_rejected_before_execution(self): + with tempfile.TemporaryDirectory() as name: + root = Path(name) + for path, raw in self.blobs.items(): + target = root / path + target.parent.mkdir(parents=True, exist_ok=True) + target.write_bytes(raw) + first = next(iter(self.blobs)) + (root / first).write_bytes(b"raise RuntimeError('must not execute')\n") + with self.assertRaisesRegex(ValueError, "source SHA256"): + io.inputs(root) + + def test_duplicate_keys_and_capacity(self): + with self.assertRaisesRegex(ValueError, "duplicate JSON key"): + io.decode(b'{"a":1,"a":2}') + events, original, helpers = fixture() + with self.assertRaisesRegex(ValueError, "finite stream domain"): + self.normalize(events, original - {"L0"}, helpers) + + +if __name__ == "__main__": + unittest.main(verbosity=2) diff --git a/research/rank7-complete-native-boundary/verify.py b/research/rank7-complete-native-boundary/verify.py new file mode 100644 index 0000000000..feda481528 --- /dev/null +++ b/research/rank7-complete-native-boundary/verify.py @@ -0,0 +1,134 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Check the complete PR2979 source/native boundary without accepting its invoice.""" + +import argparse +import json +import sys +import tempfile +from pathlib import Path + +sys.path.insert(0, str(Path(__file__).resolve().parent)) +import boundary +import controls +import io_support as io + + +def case( + modules, data, previous, old_pair, helper_names, orientation, checked, progress +): + backward = orientation == "backward" + events, metadata = modules["source"].bind( + data["word"], data["canonical_word"], data["programs"][orientation], backward + ) + normalized = boundary.normalized( + events, metadata["start"], helper_names, backward, modules["algebra"] + ) + profile = boundary.paid_profile(events) + io.require( + profile == {1: 2445, 2: 706, 3: 232, 4: 108, 5: 18, 8: 8}, + "unchanged complete local paid profile", + ) + delta = boundary.prior_delta( + modules["native"], + events, + data["canonical_word"], + previous, + old_pair, + orientation, + ) + faults = controls.run( + modules, data, events, metadata, helper_names, previous, orientation, delta + ) + native = modules["audit"].native_case( + modules["native"], + modules["kernel"], + events, + [i for i, e in enumerate(events) if e[0] != "phase"], + data["canonical_word"], + data["recipes"], + data["adapters"], + backward, + checked, + progress, + ) + return { + "source_bound_events": len(events), + "normalized": normalized, + "prior_delta": delta, + "paid_profile": profile, + "native": native, + "semantic_controls": faults, + } + + +def audit(blobs, modules, provider, run, progress=None): + data = modules["support"].artifacts(blobs, provider, run) + previous = io.decode(blobs[io.PEER + "RESULT-" + provider + ".json"]) + old_pair = io.decode(blobs[io.PRIOR + "RESULT-" + provider + ".json"]) + checked, cases = {}, {} + helpers = { + "L" + str(h) for h in range(224, 704) if h not in data["word"]["removed"] + } + io.require(len(helpers) == 408, "all 408 dirty helpers") + source_rows = boundary.source_rows(modules["endpoints"], data["word"], helpers) + for orientation in ("forward", "backward"): + cases[orientation] = case( + modules, data, previous, old_pair, helpers, orientation, checked, progress + ) + cases[orientation]["source_covector_rows"] = source_rows[orientation] + return { + "status": "PASS_COMPLETE_SOURCE_NATIVE_BOUNDARY", + "provider": provider, + "scientific_head": "be191346391661f4d35fc0d1508d0a6029572576", + "orientations": cases, + "distinct_native_identities": len(checked), + "native_identity_receipts": sorted( + checked.values(), key=lambda r: r["receipt_id"] + ), + "input_sha256": {p: io.sha(b) for p, b in sorted(blobs.items())}, + "new_supplier": False, + "new_kappa": False, + } + + +def compute(provider, artifacts=None, progress=None): + blobs = io.inputs() + own = {p.name: io.sha(io.read(p)) for p in io.PACKAGE.glob("*.py")} + modules = io.modules(blobs) + if artifacts is None: + with tempfile.TemporaryDirectory(prefix="complete-native-") as name: + run = modules["support"].generate(blobs, provider, Path(name), progress) + result = audit(blobs, modules, provider, run, progress) + else: + result = audit(blobs, modules, provider, artifacts, progress) + io.require(io.inputs() == blobs, "all source inputs unchanged during replay") + io.require( + own == {p.name: io.sha(io.read(p)) for p in io.PACKAGE.glob("*.py")}, + "checking code unchanged during replay", + ) + result["checker_sha256"] = own + return io.decode(json.dumps(result)) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--provider", required=True, choices=("base", "extra")) + parser.add_argument("--artifacts", type=Path) + parser.add_argument("--emit", action="store_true") + parser.add_argument("--progress", action="store_true") + args = parser.parse_args() + + def progress(value): + print(json.dumps(value, sort_keys=True), file=sys.stderr, flush=True) + + result = compute(args.provider, args.artifacts, progress if args.progress else None) + if args.emit: + print(json.dumps(result, sort_keys=True, indent=2)) + else: + expected = io.result(args.provider) + io.require(result == expected, "complete deterministic receipt equality") + print(result["status"] + " provider=" + args.provider) + + +if __name__ == "__main__": + main()