diff --git a/research/rank7-shared-restore-fanin/.gitattributes b/research/rank7-shared-restore-fanin/.gitattributes new file mode 100644 index 0000000000..ccceda6408 --- /dev/null +++ b/research/rank7-shared-restore-fanin/.gitattributes @@ -0,0 +1,5 @@ +# Preserve exact pinned predecessor bytes, including their original newlines. +vendor/** -text +evidence/** -text +# R1 is retained byte-for-byte with its original CRLF line endings. +vendor/R1.json whitespace=cr-at-eol diff --git a/research/rank7-shared-restore-fanin/ENGINEERING.md b/research/rank7-shared-restore-fanin/ENGINEERING.md new file mode 100644 index 0000000000..3e5c38dde3 --- /dev/null +++ b/research/rank7-shared-restore-fanin/ENGINEERING.md @@ -0,0 +1,80 @@ +# Engineering and verification limits + +Build the Lever led to a deterministic rewriter rather than hand-edited final +words. Retained word containers bind the actual released source and native run. +Prove It Works led to actual-word forward/dual audits, a separate frame census +and an explicit complete source release. Power of Ten +shaped the bounded inputs, process cleanup and refusal of existing work paths. + +## Scope and bounds + +New code has no recursive algorithm, retry loop or concurrent writer. The +rewriter touches one pinned pair of words. It accepts restore lengths 203 or +204, checks literal source and consumer contacts, and changes only restore, +report and derived cleanup. The separate frame census has at most 4,100 A +gates, 1,900 B gates, 204 restore gates, 72 warps and four registers. Its +subspaces contain at most 512 vectors; its cache holds at most 128 entries. + +The finite check also compares all 704 columns of the literal restore operator +with a separate rational implementation. Its bounded matrix has 704 rows and +at most 204 gates. It runs eight positive actual-word audits and fourteen +rejecting audits, sequentially, each with a 30-second timeout. Two additional +controls exercise the source-observer boundary. Unit tests cover the exact consumer +preimage, source-address order, unchanged scalar count, pin failures and recipe +argument changes. New checks use exceptions, not disableable assertions. + +The complete release is opt-in. It requires POSIX and enabled assertions for +the inherited validators. A stage has a 1,800-second timeout and its process +group is terminated on every exit. One recipe has thirteen stages including +preflight, and jobs are fixed at one. A new external work path owns all exports, +words and logs. Failures retain that explicit directory. The cheap default +verification uses a private temporary directory and removes it on normal +success or exception. Hard kills may bypass cleanup. + +Every external Python engine is authenticated before loading. A fresh +bytecode namespace prevents preexisting caches from replacing source bytes. +The inherited script runner receives the same isolation. Direct driver calls +can still read preexisting caches for their own initial imports; use a clean +checkout or a fresh PYTHONPYCACHEPREFIX. The registered launcher isolates the +whole interpreter. No claim is made that -B alone prevents cache reads. The +source release exports one exact Git package, validates its complete manifest, +and changes +only declared data and descriptive source labels. No frozen input is edited. +The stage program copies and their notices remain byte-identical. + +## Runtime deviations + +- Rule 1, library recursion. Python's JSON and deepcopy implementations may + recurse through the fixed acyclic word containers. Source authentication + fixes their shape and finite size. No new recursive traversal is introduced. + The interpreter's library stack is outside this package's control. An + iterative copier would be needed if arbitrary nested input were admitted. +- Rule 3, allocation. Python's containers, exact integers, JSON and subprocess + libraries allocate dynamically. Fixed input pins, at most 2 MB per ordinary + input, the explicit frame limits and serial audits bound the new computation. + The full inherited scientific toolchain has its own memory costs. It is not + claimed to be a fixed-memory implementation. Reassess capacity before adding + arbitrary words, larger geometries or parallel execution. +- Rules 8 and 9, source loading. Three fixed, pinned inherited Python engines + are loaded from explicit paths. This avoids copying or modifying scientific + predecessors. No user-selected module or evaluation string is accepted. + The full recipe invokes the pinned predecessor's literal code adapters; + their generation mechanisms and inherited assertions are unchanged. Moving + those adapters into shared code would need a separate source-binding review. +- Rule 10, inherited diagnostics. The new Python paths receive configured Ruff + checks and Python warning/compilation checks. Upstream Python and C++ tools + keep their original diagnostics and proof checks. Reformatting or repairing + frozen source packages is outside this change; their assumptions remain + explicit rather than being described as universally verified. + +Before publication, run configured Ruff plus `--select E,F,I,B,UP,C4,SIM`, +`ruff format --check`, warning-as-error unit tests, and Python compilation with +a fresh cache prefix. The actual full environment is in +`evidence/ENVIRONMENT.json`. Normal and optimized finite runs check the same +literal evidence. All new functions remain below 60 physical lines. Every new file is scoped +to this package. Stored scientific evidence omits disposable exports, binaries +and regenerated fill files. Compression-container hashes bind recorded replay +inputs; canonical decoded word hashes establish cross-environment equality. +The pinned R1 JSON retains its original CRLF bytes. Its single-file +`whitespace=cr-at-eol` attribute recognizes that source convention without +normalizing the scientific input or changing its hash. diff --git a/research/rank7-shared-restore-fanin/GIT-SOURCES.json b/research/rank7-shared-restore-fanin/GIT-SOURCES.json new file mode 100644 index 0000000000..392925ea4a --- /dev/null +++ b/research/rank7-shared-restore-fanin/GIT-SOURCES.json @@ -0,0 +1,11 @@ +[ + {"head":"e244296debb45fe6f4da84d29e4d64fbab55fda0","path":"research/rank7-joint-endframes-restore-edit"}, + {"head":"51309592971e3b5be935599eed2a95404dc7781e","path":"research/two-sided-helper-extraction"}, + {"head":"224bd5e56041c40078ff6b5fa7393733a215de5c","path":"research/paired-helper-extension"}, + {"head":"a027b0f6fdb0ab2b42ba10fc31b53960166bf2bf","path":"research/paired-extension-normal45"}, + {"head":"b74b25f3ccc84c16e1a801d73b2f47e5ea764c78","path":"research/paired-extension-cap-fill-swaps"}, + {"head":"e62d3eb9005117d82a9babcfa937ecc53237c490","path":"research/paired-extension-normal45-rewrites"}, + {"head":"e2ca469b08385d3d5e29a918d66dbefaf889e9f3","path":"research/paired-swap-normal45"}, + {"head":"18d03c447886895ef9abf888398178e0428533ca","path":"research/shared-kernel-packing"}, + {"head":"e9307b48d7d1b690939935ecef0f8e524e6d92f4","path":"research/gmx-t74-borrow43-handoff"} +] diff --git a/research/rank7-shared-restore-fanin/README.md b/research/rank7-shared-restore-fanin/README.md new file mode 100644 index 0000000000..2ed3a44ebf --- /dev/null +++ b/research/rank7-shared-restore-fanin/README.md @@ -0,0 +1,253 @@ +# One shared restore covector at two consumers + +R2 replaces two separated reads of `X40 - 2 X54` with one temporary +aggregation in X40. Both dirty sources are restored. It saves two rank-one +children at the cost of one rank-two child per call, without another register, +a helper-width change or an increase in scalar gate count. + +R2 composes with Jeremy Kothe's R1 from [PR3015][3015]. On both of +Marius-Paul Dumitrean's [PR2979][2979] providers, their common local profile is + +```text +before, R1 {1:2443, 2:707, 3:232, 4:108, 5:18, 8:8} +after, R1 + R2 {1:2441, 2:708, 3:232, 4:108, 5:18, 8:8} +``` + +The original literal T74 allocation still fits the unchanged ordered widths. +Its complete complex moment root is certified in + +```text +[0.0017292679803119446932163, 0.0017292679803119446932164]. +``` + +Even this older packing beats the published T740+R1 moment in +[PR3030][3030] by about `1.15224307614e-7`. The verifier recomputes both full +profiles with their different denominators; it does not infer this comparison +from the local delta. PR3030 remains credited for its exact fixed-word packing +cap. R2 changes that word, not its allocation problem. + +A fresh complete source/native/admission/modern-outer release passes at + +```text +kappa = 0.001729267980311944693216 - 10^-46 - 10^-70. +``` + +Its exact gain over PR3030's released nomination is +`115224307613758681/10^24`. The recorded thirteen stages total 1,272.70 seconds +on Linux with CPython 3.12.15. This is an author-checked conditional finite +candidate, not a selected-frontier update or a complete multiplication theorem. +No selected-result file changes. + +## Literal construction + +The scientific base is canonical main +`d8e0f83f00191df62174b641e9fff055c357f641`, priority revision 6. +[SOURCES.json](SOURCES.json) binds the two original words and inherited engines. +[VENDOR.json](VENDOR.json) pins Kothe's literal R1 and the PR3030 comparison. +The [canonical investigation][discussion] gives the live scope and overlap. + +Here Xr denotes the current register r, not necessarily its original input +value. In the original restore word, the relevant source-addressed gates are + +```text +162 X18 += X40 +163 X18 -= 2 X54 +... +175 X22 += X40 +176 X22 -= X45 +177 X22 -= 2 X54 +``` + +All five gates use the rank-8 frame `E42`. X40 and X54 both already have the +rank-7 frame + +```text +W = span(256,128,64,34,17,11,4) = E25 intersect E42 intersect E51. +``` + +There are exactly four contacts with X40 or X54 from gate 162 through the +end of restore, at 162, 163, 175 and 177. In particular neither source has an +intervening observer or writer. Gate 176 only adds the X45 term +into X22, so it commutes with X22's X54 update. The rewriter checks these +literal preimages and this contact census. + +Insert `X40 -= 2 X54` at W before gate 162. Retain the two X40 consumers, +remove gates 163 and 177, and append `X40 += 2 X54` at FULL after restore. +Keep every other scalar gate and frame, then rederive inverse cleanup. Apply +R1 first because its indices refer to the original word. The full source +builder receives the equivalent combined literal hunks, with exact preimages. + +## Proof and complete bill + +For arbitrary dirty values `a,b,u,v`, the new four-operation sequence is + +```text +a -= 2b +u += a +v += a +a += 2b +``` + +Its endpoint is `(a,b,u+a-2b,v+a-2b)`, exactly the original two consumers. +No zero-source premise is used. Intervening original operations preserve the +identity for the reasons above. `verify.py` checks the rational four-register +matrix and the complete 704-column literal restore operator separately from +the inherited all-input auditor. Coefficient and missing-operation controls +must fail that independent equality check; they do not merely rely on a stale +cleanup being rejected. + +Originally X54 climbs W to E42 to FULL, with jumps 1 and 1. After R2 it is +only used at W and FULL, so its final jump is 2. X40 still has jumps 1 and 1. +The temporary source restoration is charged at FULL, not discarded as free +cleanup. The other two registers' itineraries do not change. The independent +set-of-vectors census in `frame_trace.py` checks this directly from the literal +A/B/warp/restore chronology, without importing the inherited frame pricer: + +```text +four touched registers, R1 {1:20, 2:1, 3:2, 4:1} +four touched registers, R1+R2 {1:18, 2:2, 3:2, 4:1} +``` + +Write `Hr(b) = r*(73/r)^b`. The per-call delta is + +```text +H2(b) - 2H1(b) = 2*73^b*(2^(-b)-1) < 0, for every b > 0. +``` + +Thus this is a strict moment improvement, not just a scalar simplification. +Its rank mass is unchanged. All 408 ordered helper widths, 91 private zero +buffers, source cut, compensation, entrances, helper endpoints and warps stay +unchanged. R2 replaces four ADDs with four ADDs and its inverse cleanup also +has unchanged length. The source T74 fill/order/dispatch therefore remain +literal inputs. All idle children and every local child are included: + +```text +T = 74; calls = 666; live = 66304 +complete profile = {1:1643016, 2:471528, 3:159468, 4:71928, + 5:13716, 8:5328, 48:28190} +rank mass = 4816512 = 74*65088 +physical families = 66304 + 408 + 8 + 91 + 2 = 66813 +``` + +The local formula proves the sign over the whole positive b interval. The +source-authenticated rational logarithm/Taylor engine supplies the numeric +root brackets. This reuses the inherited arithmetic; it is not an independent +implementation of that engine. + +The coverage/halving packing relaxation for the new profile has cap about +`0.001756475065598923` in this moment variable. T74 realizes about 98.4510% +of that bound. Its idle mass is 2,093 per call; placing that entire mass at the +maximum halving-legal rank 51 gives the favorable relaxation, because cost per +unit rank decreases with rank for positive b. The verifier certifies its root +and the realized fraction with rational intervals. This is the model of +`complex-local-word-ceiling/ceiling.py`, not a feasible packing, a new +fixed-inventory optimum or an application of an older outer-transfer formula. +Its slack does not justify another packing search. + +## Reproduce + +The bounded standard-library check rebuilds parent, R1, R2 and R1+R2 for both +providers, audits all 632 independent dirty columns forward and dual, checks +the separate frame census and both complete moments, and rejects 16 controls: + +```sh +python3.12 -B scripts/research_package.py \ + --package research/rank7-shared-restore-fanin +python3.12 -B research/rank7-shared-restore-fanin/test_verify.py +``` + +To retain generated words and diagnostic logs, choose a fresh external path: + +```sh +python3.12 -B research/rank7-shared-restore-fanin/verify.py --work "$RUN/finite" +``` + +The default mode removes its private temporary directory, including on failure. +Explicit `--work` refuses existing data and preserves diagnostics. No default +command writes generated words into the checkout. + +The expansion decision was to continue through one complete T74 verification, +not another construction search. The proved recursive saving and unchanged +physical inventory justify that test. Prefix/magnitude costs were unknown +until the emitted-program invoice; they were not set to zero. Failure of a +source, physical or prefix gate stops the release. T740 composition stays a +separate next question. + +`reproduce.py` exports the exact PR3015 package and obtains its unchanged +complete source recipe. It replaces only the declared-edit parameter directory +and the descriptive source labels. Stage programs, the literal allocation, +all native checks and every admission/outer acceptance gate remain unchanged. +The parameter directory contains the explicit R1+R2 edit list and final words; +it does not edit a frozen predecessor. The command runs all stages serially, +including a fresh retained bootstrap and both fresh native providers: + +```sh +python3.12 -B research/rank7-shared-restore-fanin/reproduce.py \ + --repo . --work "$RUN/full" +``` + +It needs the exact objects in [GIT-SOURCES.json](GIT-SOURCES.json). Fetch them +from canonical upstream before the network-free replay: + +```sh +python3 -c 'import json, subprocess; subprocess.run(["git", "fetch", "https://github.com/CrocSwap/integer-mult-bounds.git", *[x["head"] for x in json.load(open("research/rank7-shared-restore-fanin/GIT-SOURCES.json"))]], check=True)' +``` + +It also needs a C++ compiler and NumPy 2.4.5, SciPy 1.16.1, +SymPy 1.14.0 and mpmath 1.3.0. gmpy2 2.3.2 and psutil 7.2.1 +were also installed locally. `--dry-run` performs source export and recipe +checks only. Full replay is explicit, not part of the registered cheap check. +Direct calls should use a clean checkout or a fresh `PYTHONPYCACHEPREFIX`; +`-B` alone does not prevent existing bytecode reads. The registered launcher +isolates its complete interpreter automatically. + +The [retained release](evidence/RESULT.json), native receipt, source manifest, +final word containers and stage logs are bound in +[evidence/BINDINGS.json](evidence/BINDINGS.json). The registered check also runs +`verify_release.py`, which checks these bindings and rejects ten receipt/invoice +mutants. It does not rerun native execution. Frozen word hashes bind actual +released bytes; regenerated words compare by canonical decoded payload, not +compression headers. + +The actual emitted-program invoice retains all 666 invocation and 666 bridge +sweeps, 91 private buffers and 66,813 physical families. It reports local/global +prefixes 93/1,475 bits, stock exponent 1,322 and reserve 1,510 below the charged +2,048-bit payload. The inherited owner's legacy `live+490` diagnostic is not +this full `live+509` charge. The actual source release and +[evidence/INVOICE.json.gz](evidence/INVOICE.json.gz) supply the complete bill. + +## Limits + +A conditional finite release does not prove the complete multiplication +theorem. Inherited all-size/compiler, physical realization and storage, +precision/tape, caller, analytic and universal block-energy hypotheses remain. +No independent human or formal-kernel review is claimed. Frozen sources and +the selected frontier are unchanged. + +## Open next questions + +1. Independently replay the exact source/native/admission chain before adoption. + Start with the fresh external command above and compare word, manifest, + complete profile and release bindings. Scientific dependencies remain review + obligations even if the replay passes. +2. Compose R2 with the already published T740 allocation only after this word + is checked. Unchanged helper widths suggest compatibility, but actual source, + physical/prefix and complete release bindings must be regenerated. An old + T740 receipt does not cover R2. This session does not run another packing + search or that second release. + +## Credit + +Nick Petalas contributed R2, its independent frame census and this composition. +Jeremy Kothe contributed R1, the restore-rewrite handoff and the reused literal +edit builder/reviewer. Marius-Paul Dumitrean contributed PR2979's joint rank-7 +words and complete allocation. Credit also Mason Hale, Jeremy Diviney, Yiyang +Lu, Tekalign, Ross Richardson, Dugongue, icekylinx, themilkman216 and the retained +geometry/native/owner lineage. Original [credits](vendor/PR3015-CREDITS.md) and +[notice](vendor/PR3015-NOTICE) are unchanged. Apache-2.0. +[ENGINEERING.md](ENGINEERING.md) records verification and runtime limits. + +[3015]: https://github.com/CrocSwap/integer-mult-bounds/pull/3015 +[2979]: https://github.com/CrocSwap/integer-mult-bounds/pull/2979 +[3030]: https://github.com/CrocSwap/integer-mult-bounds/pull/3030 +[discussion]: https://github.com/CrocSwap/integer-mult-bounds/discussions/2612#discussioncomment-18981612 diff --git a/research/rank7-shared-restore-fanin/SOURCES.json b/research/rank7-shared-restore-fanin/SOURCES.json new file mode 100644 index 0000000000..d3d5f97485 --- /dev/null +++ b/research/rank7-shared-restore-fanin/SOURCES.json @@ -0,0 +1,54 @@ +{ + "schema_version": 1, + "base_commit": "d8e0f83f00191df62174b641e9fff055c357f641", + "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/rank7-joint-endframes/allocation/PROFILE.json", + "usage": "input", + "git_blob": "46a83eeda67ab67cccbffe8b7ad8e44368b40ea7", + "sha256": "94a819747f3ced41f1544ada0036c983fc0c92847b9644380f877a06cd7931cf" + }, + { + "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/tools/root.py", + "usage": "input", + "git_blob": "bd6dc2eb4e5013625d17cc08461b67622bcfed69", + "sha256": "55f5aca39b5ee2fe4687ac8863e6c24569010f27a332883c069b8e14b8fe09e3" + }, + { + "path": "research/rank7-joint-endframes/vendor/audit_local.py", + "usage": "input", + "git_blob": "8224873d0497cf0b4c202f31b145fa273553d978", + "sha256": "a38940094f7d19cd6376aafdd4734fa68eabc9aff4c98c3c4a3e9540328b1c90" + }, + { + "path": "research/rank7-joint-endframes/vendor/preload_move.py", + "usage": "input", + "git_blob": "55b435035bbc439a9d55e8abd125993208cef8d9", + "sha256": "c8fda4674644fcd5cbf39b6645ce148a21daa90a998b678cbe51f970b78b0044" + } + ] +} diff --git a/research/rank7-shared-restore-fanin/TASK.json b/research/rank7-shared-restore-fanin/TASK.json new file mode 100644 index 0000000000..a980c3132a --- /dev/null +++ b/research/rank7-shared-restore-fanin/TASK.json @@ -0,0 +1,83 @@ +{ + "schema_version": 1, + "task_id": "scalar-to-moment", + "priority_revision": 6, + "base_commit": "d8e0f83f00191df62174b641e9fff055c357f641", + "original_card": { + "id": "scalar-to-moment", + "question": "Can one known scalar simplification be converted into an actual paid-profile improvement?", + "starting_points": [ + "research/r439-bsection-stars-seed01/README.md", + "certificates/selected-result.json" + ], + "methods": [ + "Derive the changed legal frame itinerary and exact child histogram.", + "Prove a scoped obstruction showing why that scalar gain cannot change the paid contract." + ], + "acceptance_gate": "An unchanged histogram is not a kappa gain; record any separate runtime or proof benefit explicitly.", + "first_step": { + "command": [ + "python3", + "-B", + "research/r439-bsection-stars-seed01/verify.py" + ], + "expected": "PASS_R439_BSECTION_STARS", + "inspect": "Observe that the positive control improves scalar counts while retaining the paid histogram.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Choose one simplification and derive the complete changed frame itinerary, or prove why it cannot change the histogram.", + "bottleneck_link": "A legal change to the histogram, not addition count alone, is the bridge to an exponent gain.", + "allowed_variations": [ + "One existing scalar simplification and one proposed frame-path change." + ], + "scope_change_triggers": [ + "Submitting only another scalar count as completion of a paid-profile task." + ], + "overlap_terms": [ + "scalar simplification", + "paid profile", + "R439" + ] + }, + "scope_status": "changed", + "actual_scope": "One shared dirty-source covector across two nonadjacent PR2979 restore consumers, composed with Jeremy Kothe's R1 and priced on the literal T74 allocation.", + "scope_change_reason": "Take PR3015's live restore-rewrite handoff rather than the card's historical R439 bit example. The changed complex word has fresh paid-profile headroom beyond PR3030's attained fixed-word packing cap. Selected source bindings were checked first.", + "bottleneck_link": "The binding complex supplier pays two rank-one jumps on X54. A source-restoring shared covector replaces them with one rank-two jump without new storage or scalar gates.", + "budget_minutes": 60, + "upstream_checkpoint": { + "commit": "d8e0f83f00191df62174b641e9fff055c357f641", + "checked_at": "2026-10-16T20:20:39Z", + "priority_revision": 6, + "relevant_guidance_or_source_changes": false + }, + "overlap": { + "open_prs": 286, + "closed_prs": 2440, + "closed_snapshot_at": "2026-10-16T20:01:23Z", + "discussions": 1779, + "complete_pagination": true, + "warnings": [], + "nearest_work": [3015, 2979, 3030], + "limitation": "Bodies, comments and available local notes were searched, not every diff or unpublished work. Historical X54 slot names are not this source-register rewrite; no-match is not proof of novelty.", + "canonical_thread": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2612#discussioncomment-18981612" + }, + "stop_rule": "Stop after R2, its exact R1 composition and one serial full T74 source/native/admission/outer release. No larger rewrite search, packing expansion or selected-frontier change.", + "outcome": "completed", + "evidence": "README.md, evidence/FINITE.json, separate 704-column restore equivalence and set-span frame census, plus fresh source/native/admission/outer release in evidence/RESULT.json with exact word/invoice/log bindings and rejection controls.", + "author": "Nick Petalas", + "ai_assistance": "Substantial automated development assistance; no independent human or formal-kernel review is claimed.", + "open_questions": [ + { + "question": "Does an independent fresh replay reproduce the complete R1+R2 T74 release?", + "why_it_matters": "Author replay is not independent supplier admission or mathematical review.", + "first_step": "Run reproduce.py with the pinned Git objects, declared dependencies and a fresh external work directory; compare exact word, source, native, profile and release bindings.", + "blocked_by": "Scientific review of inherited all-size, physical, precision and analytic hypotheses remains separate." + }, + { + "question": "Does R2 compose through a fresh complete release of the published T740 packing?", + "why_it_matters": "The unchanged widths suggest another small gain, but old T740 receipts do not cover the new word.", + "first_step": "Bind the R1+R2 literal words to PR3030's exact allocation and regenerate its source/native/admission/outer chain without another packing search.", + "blocked_by": "A separately scoped source-bound composition, including T-dependent physical and prefix checks." + } + ] +} diff --git a/research/rank7-shared-restore-fanin/VENDOR.json b/research/rank7-shared-restore-fanin/VENDOR.json new file mode 100644 index 0000000000..c699c2997b --- /dev/null +++ b/research/rank7-shared-restore-fanin/VENDOR.json @@ -0,0 +1,32 @@ +[ + { + "path": "vendor/R1.json", + "head": "e244296debb45fe6f4da84d29e4d64fbab55fda0", + "source_path": "research/rank7-joint-endframes-restore-edit/edits/EDITS.json", + "author": "Jeremy Kothe", + "license": "Apache-2.0", + "sha256": "c9c68660d07bfd12ed20fd8cbfe3d36301ceb2d7bb9b4ea11350cc399b19e0b1" + }, + { + "path": "vendor/PR3030-FINITE.json", + "head": "78e77d820393c6b8648b47af219e991edfcc54e6", + "source_path": "research/rank7-t740-release/evidence/FINITE.json", + "author": "Nick Petalas", + "license": "Apache-2.0", + "sha256": "00ee90400fa3f35b19a12b89e4d2a2754a02832d4800351657970dc18042b406" + }, + { + "path": "vendor/PR3015-CREDITS.md", + "head": "e244296debb45fe6f4da84d29e4d64fbab55fda0", + "source_path": "research/rank7-joint-endframes-restore-edit/CREDITS.md", + "license": "Apache-2.0", + "sha256": "bd4b09fcd2861933883cbce6ecf0e30743d5d3b4cb0cc38e258530c370c121b9" + }, + { + "path": "vendor/PR3015-NOTICE", + "head": "e244296debb45fe6f4da84d29e4d64fbab55fda0", + "source_path": "research/rank7-joint-endframes-restore-edit/NOTICE", + "license": "Apache-2.0", + "sha256": "ffcc3de2243815db0e9fb8d820b4ca511fce3c7673c966e14b486f05d30ac11a" + } +] diff --git a/research/rank7-shared-restore-fanin/VERIFY.json b/research/rank7-shared-restore-fanin/VERIFY.json new file mode 100644 index 0000000000..48f3a29434 --- /dev/null +++ b/research/rank7-shared-restore-fanin/VERIFY.json @@ -0,0 +1,35 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/rank7-joint-endframes/allocation/PROFILE.json", + "research/rank7-joint-endframes/data/WORD-base.json.gz", + "research/rank7-joint-endframes/data/WORD-extra.json.gz", + "research/rank7-joint-endframes/tools/root.py", + "research/rank7-joint-endframes/vendor/audit_local.py", + "research/rank7-joint-endframes/vendor/preload_move.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Both exact providers, R1/R2 composition, 632-column forward/dual audits, separate frame census, full moments and 16 rejection controls." + }, + { + "argv": ["{python}", "-B", "{package}/test_verify.py"], + "timeout_seconds": 30, + "checks": "Ten behavioral groups covering source contacts, exact consumer preimages, profile gain, stage reconstruction, source pins and recipe changes." + }, + { + "argv": ["{python}", "-B", "{package}/verify_release.py"], + "timeout_seconds": 30, + "checks": "Retained source/native/admission/outer, actual words, invoice, all stage-log bindings and ten rejecting receipt/invoice mutants; no fresh native replay." + } + ] +} diff --git a/research/rank7-shared-restore-fanin/decisions.tsv b/research/rank7-shared-restore-fanin/decisions.tsv new file mode 100644 index 0000000000..c0abd1be23 --- /dev/null +++ b/research/rank7-shared-restore-fanin/decisions.tsv @@ -0,0 +1,6 @@ +timestamp phase decision reason evidence result +2026-10-16T19:38Z selection longer restore rewrite current packing cap already attained; short-block search only PR3015,3030 and complete overlap snapshot bounded constructive probe +2026-10-16T19:45Z verification start one fresh full T74 release R2 local gain exceeds current T740 candidate; keep scope small finite-first/RESULT.json and source preflight serial jobs=1, external output +2026-10-16T20:10Z full-result retain the R1+R2 T74 candidate fresh full recipe passed every gate full/RESULT.json; source manifest 4f52f55e conditional kappa 0.001729267980311944693216 minus strict margins +2026-10-16T20:11Z postflight accept final driver and parameters stricter current checks and exact 8-file parameter equality pass postflight.log and final-preflight no scientific input changed during driver cleanup +2026-10-16T20:17Z verification prepare one focused publication normal/optimized and Python3.13 finite checks, 10 unit groups and 10 release mutants pass final-registered.log and evidence/BINDINGS.json no selected-frontier change; independent review remains diff --git a/research/rank7-shared-restore-fanin/evidence/ADMISSION-RESULT.json b/research/rank7-shared-restore-fanin/evidence/ADMISSION-RESULT.json new file mode 100644 index 0000000000..ff747fc2bc --- /dev/null +++ b/research/rank7-shared-restore-fanin/evidence/ADMISSION-RESULT.json @@ -0,0 +1,382 @@ +{ + "actual_expected_helpers": 408, + "comparison_claim_sha256": "656a4c93411b078753783513e2e71b1722a56e7b70120264a38118811982fa77", + "comparison_head": "e2ca469b08385d3d5e29a918d66dbefaf889e9f3", + "comparison_kappa": "17240352247481048785499999999999999999999998999999999999999999999999/10000000000000000000000000000000000000000000000000000000000000000000000", + "comparison_pr": 2969, + "complex_lower": "54039624384748271663/31250000000000000000000", + "dispatch_sha256": "65e435bd68e97243c003677271b88485a29d4d0fae2dff1354100404a145e74c", + "external_input_sha256": { + "/home/nick/.cache/integer-mult-bounds-runs/20261016T1936-frontier/full/pr3015/allocation/DISPATCH.json": "65e435bd68e97243c003677271b88485a29d4d0fae2dff1354100404a145e74c", + "/home/nick/.cache/integer-mult-bounds-runs/20261016T1936-frontier/full/pr3015/allocation/FILL.json.gz": "c2136be9434cda511a1a8a44d98f9f72ea5376830a8426674253b4ee351c4c39", + "/home/nick/.cache/integer-mult-bounds-runs/20261016T1936-frontier/full/pr3015/allocation/ORDER.json": "519d1d5dbb997a219fcfcad34c0b03e7838bef24199784d7e964fa10090f66e1", + "/home/nick/.cache/integer-mult-bounds-runs/20261016T1936-frontier/full/run/adapters/extension_blocknorm.py": "6e6b8683cc87a84e5410c399b1128eb68694f852a3927cb124067f503ed7d7c7", + "/home/nick/.cache/integer-mult-bounds-runs/20261016T1936-frontier/full/run/parent-export/pr2894/vendor/pr2857/vendor/pr2839/lift_parent.py": "9a1edd7d4ab4a2f2ac8d15b42b7e40f93653d65026bac59e4c1ce80b486bd60e", + "/home/nick/.cache/integer-mult-bounds-runs/20261016T1936-frontier/full/run/parent-export/pr2894/vendor/pr2857/vendor/pr2839/reconstruct_replica.py": "5472811c24aef3852dc7e189dff5060076a6c0b25bfde928da50dcfe9b5bdc15", + "/home/nick/.cache/integer-mult-bounds-runs/20261016T1936-frontier/full/run/parent-export/pr2894/vendor/pr2857/vendor/pr2839/replica_parent.py": "48bdbf28f59d80edb266803ec61bf5e22e8fb5e5a0e2b88004b6039147589bd4", + "/home/nick/.cache/integer-mult-bounds-runs/20261016T1936-frontier/full/run/pr2969/CLAIM.json": "656a4c93411b078753783513e2e71b1722a56e7b70120264a38118811982fa77" + }, + "fill_sha256": "c2136be9434cda511a1a8a44d98f9f72ea5376830a8426674253b4ee351c4c39", + "gain": "2616377781919907333/500000000000000000000000", + "kappa": "17292679803119446932159999999999999999999998999999999999999999999999/10000000000000000000000000000000000000000000000000000000000000000000000", + "kappa_decimal": "0.0017292679803119446932159999999999999999999998999999999999999999999999", + "native_receipt_sha256": "3dce85d535c34dd5755b7a7828b9706cd38198aa99e849dc0f166ac4e7ea47df", + "order_sha256": "519d1d5dbb997a219fcfcad34c0b03e7838bef24199784d7e964fa10090f66e1", + "package_manifest_sha256": "c74a7aafa9f6ed15e9e989d9f23c859781f50167cf1d2bec94fcf2236425f05d", + "patches": [ + { + "after_sha256": "52f8b4cec2dab69cbe590e1fd0f7a68e1b35de5a540bd22fd2adfce07a92b46b", + "before_sha256": "faf283eb4edd2e6a1ccb40b3cb3ba30ae54338eaf5ea0a10d84d11d7939502af", + "path": "new/rebind.py", + "replacements": [ + [ + "physical=spec['expected']['live'] + 8 + R + 2)", + "physical=spec['expected']['live'] + 8 + R + 2 + max(len(rd(d / 'CANONICAL-WORD.json.gz').get('zero_buffers', [])) for d in locs.values()))" + ] + ] + }, + { + "after_sha256": "99bef04f24a99088e5c0c9b8f6bbc8386669d8315b8f572d6bbfb932c5d51145", + "before_sha256": "7edb4732b34e5814b27650a55c938626cb50d68f06397744dd4fe451437e90e0", + "path": "geometry_controls.py", + "replacements": [ + [ + " i['complete_invocation_sweeps']=i['bridge_sweeps']=333", + " i['complete_invocation_sweeps']-=1;i['bridge_sweeps']-=1" + ], + [ + " o,i=copy.deepcopy(owner),copy.deepcopy(invoice);fn(o,i);oh=digest(o);i['owner_audit_sha256']=oh", + " o,i=copy.deepcopy(owner),copy.deepcopy(invoice);fn(o,i);assert (o,i)!=(owner,invoice), 'geometry mutant must change actual receipts';oh=digest(o);i['owner_audit_sha256']=oh" + ] + ] + }, + { + "after_sha256": "6cfefe80c02a6c0f243f50ca9e146e1ab1440b84a033d8a71d42be5a5fa27f6b", + "before_sha256": "c43680a2da390f79925547a5ee1919d8a76637cccf98e2c8164b6f667fbc3183", + "path": "verify_release.py", + "replacements": [ + [ + "Fraction(1, 10 ** 3046) - Fraction(1, 10 ** 3022)", + "Fraction(1, 10 ** (spec['outer_refinement']['endpoint_digits'] + 46)) - Fraction(1, 10 ** (spec['outer_refinement']['endpoint_digits'] + 22))" + ], + [ + "epsilon=1-(1025/1024)e-3080", + "epsilon=1-(1025/1024)e-{spec['outer_refinement']['endpoint_digits']+80}" + ], + [ + "at the one 3000-digit rejection call", + "at the one {spec['outer_refinement']['endpoint_digits']}-digit rejection call" + ] + ] + }, + { + "after_sha256": "1dd56009986eb14dd6603c9193c7ad71dd45c7d005bf71c9cd3f916e66f54d98", + "before_sha256": "9e12909c73d3b3a31a45d801ae76c034510d6306400412e474df79bc4f1dc67e", + "path": "outer/check_ledger.py", + "replacements": [ + [ + "assert (m,W)==(73,66304)", + "T=spec['geometry']['replicas']\nassert type(T) is int and T>0\nassert m==73 and W==896*T and W==BJ['live']" + ] + ] + }, + { + "after_sha256": "ebaf637f1f818dac9c0fce0ee3f18df300873105818cea29a8ae9e8b737b5c7d", + "before_sha256": "08ca58abff11bdfba721dc56ab8acf06ec1b7c48a8699a0955cf35324680aca7", + "path": "code/witness.py", + "replacements": [ + [ + " with open(os.environ['WITNESS_RECORD'],'a')as f:f.write(json.dumps([key,got],default=str)+chr(10))", + " import time as _wr_time\n _wr_path=Path(os.environ['WITNESS_RECORD'])\n _wr_lock=_wr_path.with_name(_wr_path.name+'.append.lock')\n _wr_deadline=_wr_time.monotonic()+60\n _wr_fd=None\n while _wr_fd is None:\n try:_wr_fd=os.open(_wr_lock,os.O_CREAT|os.O_EXCL|os.O_WRONLY)\n except FileExistsError:\n if _wr_time.monotonic()>=_wr_deadline:raise TimeoutError('discovery record lock timeout; existing lock preserved')\n _wr_time.sleep(.005)\n try:\n with _wr_path.open('a',encoding='utf-8',newline='\\n')as _wr_out:\n _wr_out.write(json.dumps([key,got],default=str)+chr(10))\n _wr_out.flush()\n finally:\n os.close(_wr_fd)\n _wr_lock.unlink()" + ] + ] + }, + { + "after_sha256": "2964ea185a64061d72e4a6c648a48cd0ddbfc7ea8174ecb39be2a2eee52a3be8", + "before_sha256": "8dee5aa1663a70edcf1099a30b72166d89c29fa29ba2025fb5707fdbcc237f83", + "path": "verify.py", + "replacements": [ + [ + "run('lift-parent',P/'lift_parent.py','--owners',work/'rebuilt-owners','--out',work/'rebuilt-parent')", + "run('lift-parent',P/'lift_parent.py','--package',P,'--owners',work/'rebuilt-owners','--out',work/'rebuilt-parent')" + ] + ] + }, + { + "after_sha256": "0d8cc021d2401d047aaec79060ec2ea28ba06f12eca8dbf4c60c78bb31975c4e", + "before_sha256": "ebaf637f1f818dac9c0fce0ee3f18df300873105818cea29a8ae9e8b737b5c7d", + "path": "code/witness.py", + "replacements": [ + [ + "PAYLOAD==1<<(192+(GEO['dimension']+1)//2+2*CALLS+4).bit_length()", + "PAYLOAD==1<<(128+(GEO['dimension']+1)//2+18+1330+1+4).bit_length()" + ] + ] + }, + { + "after_sha256": "c5106e0d7a97382677fa228fbade989262347968a0e54acfcf6712aa37e02f47", + "before_sha256": "bb213d0af12218ff7c9c572717e522d8bbeeb2856b87a253f4a7f44e0fd71f15", + "path": "code/invoice_allcold.py", + "replacements": [ + [ + " required_prefix=localbits+input_l2_bits+call_count+bridge_sweeps+4", + " from blocknorm_certificate import certify\n blocknorm=certify(template, {pid:base/'providers'/pid for pid in template['local_providers']})\n assert blocknorm['status'] == 'PASS_TENSOR_BLOCK_NORM_CERTIFICATE'\n assert localbits <= 128, 'actual native scalar/Horner prefix exceeds charged local reserve'\n required_prefix=localbits+input_l2_bits+blocknorm['max_active_depth']+blocknorm['stock_l2_bits']+1+4" + ] + ] + }, + { + "after_sha256": "0d522b09c7fe6a5e62fe80c28f3eefe733557a82d77c6212e5d4b91ffb7e3421", + "before_sha256": "02502a217fe8c9e10229075b50745518beac512c48db20e64c3e06514a4da5b5", + "path": "independent_core.py", + "replacements": [ + [ + " payload = 1 << (192 + (M+1)//2 + 2*len(c['order']) + 4).bit_length()", + " require(localbits <= 128, 'measured native prefix exceeds local reserve')\n payload = 1 << (128 + (M+1)//2 + 18 + 1330 + 1 + 4).bit_length()" + ] + ] + }, + { + "after_sha256": "d598a2ac1e2e8eaee14a8c285e0277a7ae44ca6a15bd2b5cfc67fb40844fb387", + "before_sha256": "c5106e0d7a97382677fa228fbade989262347968a0e54acfcf6712aa37e02f47", + "path": "code/invoice_allcold.py", + "replacements": [ + [ + " complete_invocation_sweeps=call_count,bridge_sweeps=bridge_sweeps,row_prefix_extra=2*payload,", + " complete_invocation_sweeps=call_count,bridge_sweeps=bridge_sweeps,row_prefix_extra=2*payload,blocknorm=blocknorm," + ], + [ + " primitive_arithmetic_margin_bits=4,controller_audit_sha256=", + " tensor_block_norm=blocknorm,partial_cover_margin_bits=1,physical_stock_l2_bits=blocknorm['stock_l2_bits'],primitive_arithmetic_margin_bits=4,controller_audit_sha256=" + ], + [ + "Sum every actual invocation and bridge sweep and take the maximum local scalar/Horner prefix over both orientations of the fixed provider.", + "All invocations and bridge sweeps remain charged. Bound completed-boundary energy by at most eighteen active steps per owner replica, using exact tensor-isomorphic whole-family helper unitaries. Add the full group-indexed physical-stock sup-to-l2 factor and one partial-cover margin, then the maximum local scalar/Horner prefix." + ] + ] + }, + { + "after_sha256": "e051aaa166e01263780d5ae03699690670b597fed6593af4c37a7e978825eb85", + "before_sha256": "0d522b09c7fe6a5e62fe80c28f3eefe733557a82d77c6212e5d4b91ffb7e3421", + "path": "independent_core.py", + "replacements": [ + [ + " prefix = localbits + (M + 1) // 2 + len(c['order']) + c['bridges'] + 4", + " bn=c['blocknorm']\n require(bn['status']=='PASS_TENSOR_BLOCK_NORM_CERTIFICATE' and bn['max_active_depth']==18 and bn['stock_l2_bits']<=1330, 'independent tensor block certificate')\n prefix = localbits + (M + 1) // 2 + bn['max_active_depth'] + bn['stock_l2_bits'] + 1 + 4" + ], + [ + "prefix_formula=dict(local_scalar=localbits, input_l2=(M + 1) // 2, invocations=len(c['order']), bridges=c['bridges'], margin=4)", + "prefix_formula=dict(local_scalar=localbits, input_l2=(M + 1) // 2, invocations=len(c['order']), bridges=c['bridges'], active_block_depth=18,stock_l2=bn['stock_l2_bits'],partial_cover=1,margin=4),blocknorm=bn" + ] + ] + }, + { + "after_sha256": "393323f150d0bb686419804d51cf43d0f58450d2a1e7929725acdd26fdbb3640", + "before_sha256": "2286f00e462ff28abbb3f396095463482a1e063213b9526a7225275980c77eaf", + "path": "audit_mixed.py", + "replacements": [ + [ + "pending=A.check_pending_axes(ctx);receipt=A.check_roles(ctx,roles)", + "import blocknorm_certificate as BN;ctx['blocknorm']=BN.certify_context(ctx,roles,dirs,source_parent=parent);pending=A.check_pending_axes(ctx);receipt=A.check_roles(ctx,roles)" + ] + ] + }, + { + "after_sha256": "0542dde915af8902324db2f59136da078d5256bfaa8f1510f3e59336be7e2680", + "before_sha256": "f25e1e870df5d5a16a1e367b3df8843cb01644ab4b75895d7939af81e4fcb833", + "path": "code/assemble.py", + "replacements": [ + [ + " assert invoice['global_prefix_bits']==max(z['prefix_bits']for p in invoice['providers'].values()for z in p['local'].values())+37+CALLS+CALLS+4", + " bn=invoice['blocknorm']\n assert bn['status']=='PASS_TENSOR_BLOCK_NORM_CERTIFICATE' and bn['replicas']==REPLICAS\n assert bn['max_active_depth']==bn['boundary_depth_bits']==18 and bn['active_calls_per_block']==bn['bridges_per_block']==9\n assert bn['block_width_families']==896 and bn['physical_families']==invoice['physical'] and bn['live_families']==invoice['live']\n assert bn['partial_cover_bits']==1 and bn['input_l2_bits']==37 and bn['local_reserve_bits']==128 and bn['retained_payload_bits']==PAYLOAD\n localbits=max(z['prefix_bits']for p in invoice['providers'].values()for z in p['local'].values())\n assert bn['local_actual_prefix_bits']==localbits and localbits<=128\n assert invoice['global_prefix_bits']==bn['actual_prefix_bits']==localbits+37+18+bn['stock_l2_bits']+1+4\n assert bn['required_reserve_bits']==128+37+18+bn['stock_l2_bits']+1+4 0 and size & (size - 1) == 0, "subspace cardinality") + return size.bit_length() - 1 + + +def step(gate, current, paid): + if gate[0] == "warp": + register = gate[1] + if register in current: + need(current[register] == span(tuple(gate[3])), "warp entry") + current[register] = span(tuple(gate[4])) + return + registers = gate[1:3] if gate[0] == "add" else gate[1:2] + for register in registers: + if register in current: + space = span(tuple(gate[-1])) + need(current[register] <= space, "monotone four-register frame") + delta = dimension(space) - dimension(current[register]) + if delta: + paid[delta] += 1 + current[register] = space + + +def census(word): + need(not set(REGISTERS) & set(word["centers"]), "no omitted centre-path charge") + need( + len(word["A"]) <= 4100 + and len(word["B"]) <= 1900 + and len(word["restore"]) <= 204 + and len(word["warps"]) <= 72, + "fixed-word bounds", + ) + current = {r: span((word["ports"][r],)) for r in REGISTERS} + paid = Counter() + for gate in word["A"]: + step(gate, current, paid) + warps = {} + for record in word["warps"]: + warps.setdefault(record[0], []).append(record) + for index in range(len(word["B"]) + 1): + for record in warps.get(index, []): + step(["warp", record[1], None, record[3], record[4]], current, paid) + if index < len(word["B"]): + step(word["B"][index], current, paid) + before = {str(r): dimension(current[r]) for r in REGISTERS} + for gate in word["restore"]: + step(gate, current, paid) + full = span(tuple(1 << i for i in range(9))) + for register in REGISTERS: + delta = 9 - dimension(current[register]) + if delta: + paid[delta] += 1 + current[register] = full + return {str(rank): count for rank, count in sorted(paid.items())}, before diff --git a/research/rank7-shared-restore-fanin/reproduce.py b/research/rank7-shared-restore-fanin/reproduce.py new file mode 100644 index 0000000000..7a0a52dc29 --- /dev/null +++ b/research/rank7-shared-restore-fanin/reproduce.py @@ -0,0 +1,367 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Run the unchanged PR3015 release recipe with the explicit R1+R2 edit list. + +Credit Jeremy Kothe, Marius-Paul Dumitrean, Mason Hale, Jeremy Diviney and +all retained source authors. No predecessor file or acceptance gate is edited. +""" + +import argparse +import contextlib +import gzip +import io +import json +import os +import shutil +import signal +import subprocess +import sys +import tarfile +import time +from fractions import Fraction +from pathlib import Path, PurePosixPath + +import rewrite as rw +import verify as v + +HEAD = "e244296debb45fe6f4da84d29e4d64fbab55fda0" +PREFIX = "research/rank7-joint-endframes-restore-edit" +MANIFEST = "5e113822c0c36ee7dd9366578fbaf5daa108b8c51e37f4d10eda25dd6ed52cae" +NAMES = [ + "export-pr2894", + "export-pr2833", + "fresh-retained-bootstrap", + "four-kernel-stage", + "preload-stage", + "parent-paired-stage", + "paired-extension-stage", + "rank7-overlay-stage", + "declared-edit-stage", + "derive-closed-adapters", + "fresh-current-native", + "complete-admission", +] + + +def authenticate_tree(path): + files = list(path.rglob("*")) + rw.need( + len(files) <= 10000 and not any(p.is_symlink() for p in files), + "bounded regular source tree", + ) + actual = { + p.relative_to(path).as_posix(): v.digest(p) + for p in files + if p.is_file() and p != path / "MANIFEST.json" + } + rw.need(actual == v.read(path / "MANIFEST.json"), "complete source inventory") + + +def export(repo, out): + result = subprocess.run( + ["git", "-C", str(repo), "archive", HEAD, PREFIX], + capture_output=True, + check=True, + timeout=60, + ) + rw.need(len(result.stdout) < 10_000_000, "bounded source export") + out.mkdir() + with tarfile.open(fileobj=io.BytesIO(result.stdout)) as archive: + members = archive.getmembers() + rw.need(len(members) <= 256, "bounded package entries") + for member in members: + name = PurePosixPath(member.name) + rw.need(not name.is_absolute() and ".." not in name.parts, "archive path") + rw.need(member.isfile() or member.isdir(), "regular archive entries") + if member.isdir(): + continue + rw.need(name.is_relative_to(PurePosixPath(PREFIX)), "exact package prefix") + target = out / name.relative_to(PurePosixPath(PREFIX)) + target.parent.mkdir(parents=True, exist_ok=True) + stream = archive.extractfile(member) + rw.need(stream is not None, "source stream") + with stream: + target.write_bytes(stream.read()) + rw.need(v.digest(out / "MANIFEST.json") == MANIFEST, "exact PR3015 manifest") + authenticate_tree(out) + + +def parameters(source, work): + """Only declared data change. Both stage programs remain byte-identical.""" + out = work / "parameters" + (out / "edits").mkdir(parents=True) + (out / "data").mkdir() + frames = v.load(v.PARENT / "vendor/preload_move.py", "release_frames") + edits = {} + for variant in ("base", "extra"): + words = v.words(variant, frames) + old, new = words["parent"], words["R1R2"] + rw.need( + v.canonical(new) + == v.read(v.PACKAGE / "evidence/FINITE.json")["variants"][variant]["R1R2"][ + "canonical_sha256" + ], + "release word equals checked finite word", + ) + edits[variant] = rw.stage_spec(old, new) + shutil.copy2( + source / f"data/WORD-{variant}.json.gz", + out / f"data/WORD-{variant}.json.gz", + ) + payload = json.dumps(new, sort_keys=True, separators=(",", ":")).encode() + (out / f"edits/FINAL-WORD-{variant}.json.gz").write_bytes( + gzip.compress(payload, compresslevel=1, mtime=0) + ) + v.save( + out / "edits/EDITS.json", + { + "edits": edits, + "declared": {"local_profile": rw.LOCAL, "width_inventory": rw.INVENTORY}, + }, + ) + for name in ("declared_edits.py", "edits_review.py"): + shutil.copy2(source / "edits" / name, out / "edits" / name) + pins = { + p.relative_to(out).as_posix(): v.digest(p) + for p in sorted((out / "edits").iterdir()) + } + v.save(out / "EDIT-PINS.json", pins) + return out + + +def stage(name, command, work, env, stages): + log, started = work / (name + ".log"), time.monotonic() + with log.open("w") as stream: + process = subprocess.Popen( + command, + cwd=work, + env=env, + stdin=subprocess.DEVNULL, + stdout=stream, + stderr=subprocess.STDOUT, + start_new_session=True, + ) + try: + code = process.wait(timeout=1800) + finally: + try: + os.killpg(process.pid, signal.SIGTERM) + process.wait(timeout=5) + except ProcessLookupError: + pass + except subprocess.TimeoutExpired: + os.killpg(process.pid, signal.SIGKILL) + process.wait(timeout=5) + with contextlib.suppress(ProcessLookupError): + os.killpg(process.pid, signal.SIGKILL) + stages.append( + { + "stage": name, + "exit_code": code, + "seconds": time.monotonic() - started, + "log_sha256": v.digest(log), + } + ) + v.save(work / "STAGES.json", stages) + rw.need(code == 0, "failed " + name + "; see " + str(log)) + print("PASS", name, flush=True) + + +def retarget(recipe, parameters): + changes = [] + for name, command in recipe: + if name == "declared-edit-stage": + flag, value = "--local-package", str(parameters) + elif name in ("derive-closed-adapters", "complete-admission"): + flag, value = "--source-profile", "rank7-shared-restore-fanin" + else: + continue + index = command.index(flag) + 1 + changes.append( + {"stage": name, "flag": flag, "old": command[index], "new": value} + ) + command[index] = value + if name == "derive-closed-adapters": + index = command.index("--source-commit") + 1 + changes.append( + { + "stage": name, + "flag": "--source-commit", + "old": command[index], + "new": value, + } + ) + command[index] = value + rw.need(len(changes) == 4, "only explicit stage data and source labels change") + return changes + + +def check_admission(work, source): + run = work / "run" + admission = v.read(run / "candidate/RESULT.json") + receipt_path = run / "candidate/release/RELEASE-RECEIPT.json" + receipt = v.read(receipt_path) + rw.need( + admission["status"] == "PASS_REPLICA_ORDER_FILL_DERIVATIVE_COMPLETE_RELEASE", + "full admission", + ) + rw.need(receipt["status"] == "PASS_RELEASE", "modern outer release") + rw.need( + {int(k): n for k, n in admission["profile"].items()} == v.EXPECTED, + "complete R1+R2 bill", + ) + rw.need( + admission["fill_sha256"] == v.digest(source / "allocation/FILL.json.gz"), + "unchanged literal fill", + ) + rw.need( + admission["order_sha256"] == v.digest(source / "allocation/ORDER.json"), + "unchanged order", + ) + rw.need( + admission["dispatch_sha256"] == v.digest(source / "allocation/DISPATCH.json"), + "unchanged dispatch", + ) + rw.need( + admission["release_receipt_sha256"] == v.digest(receipt_path), "release binding" + ) + rw.need( + admission["package_manifest_sha256"] == receipt["manifest_sha256"], + "same admitted package", + ) + rw.need( + Fraction(admission["kappa"]) == Fraction(receipt["kappa_decimal"]), + "same released endpoint", + ) + finite = v.read(v.PACKAGE / "evidence/FINITE.json") + rw.need( + Fraction(admission["kappa"]) > Fraction(finite["moment"]["PR3030_root"][1]), + "gain beyond PR3030", + ) + return admission, receipt_path, finite + + +def check_source(work, source, admission, finite): + run = work / "run" + edited = run / "source-edits" + authenticate_tree(edited) + authenticate_tree(source) + manifest = v.digest(edited / "MANIFEST.json") + native = v.read(run / "native/NATIVE-RECEIPT.json") + rw.need( + native["manifest_sha256"] == admission["source_manifest_sha256"] == manifest, + "exact new source", + ) + rw.need( + v.digest(run / "native/NATIVE-RECEIPT.json") + == admission["native_receipt_sha256"], + "native binding", + ) + rw.need(native["fresh_current_provider_count"] == 2, "both fresh providers") + for variant in ("base", "extra"): + path = edited / f"new/borrow/words/BORROW-WORD-43{variant}.json.gz" + rw.need( + v.canonical(v.read(path)) + == finite["variants"][variant]["R1R2"]["canonical_sha256"], + "actual checked word", + ) + rw.need( + native["providers"][variant]["word_sha256"] == v.digest(path), + "native exact word", + ) + return manifest + + +def check(work, source, stages): + admission, receipt_path, finite = check_admission(work, source) + manifest = check_source(work, source, admission, finite) + rw.need( + [s["stage"] for s in stages] == ["source-preflight", *NAMES], + "all source stages", + ) + rw.need(all(s["exit_code"] == 0 for s in stages), "successful complete recipe") + return { + "status": "PASS_SHARED_RESTORE_COMPLETE_RELEASE", + "kappa": admission["kappa"], + "source_manifest_sha256": manifest, + "admission_sha256": v.digest(work / "run/candidate/RESULT.json"), + "release_receipt_sha256": v.digest(receipt_path), + "fresh_retained_bootstrap": True, + "profile": v.EXPECTED, + "scope": "Conditional finite release; inherited theorem hypotheses remain.", + } + + +def environment(work): + env = dict( + os.environ, + PYTHONDONTWRITEBYTECODE="1", + PYTHONPYCACHEPREFIX=str(work / "bytecode"), + OPENBLAS_NUM_THREADS="1", + OMP_NUM_THREADS="1", + PYTHONINTMAXSTRDIGITS="0", + ) + for name in ( + "PYTHONPATH", + "PYTHONOPTIMIZE", + "WITNESS_SPEC", + "WITNESS_RECORD", + "WITNESS_DISCOVER", + ): + env.pop(name, None) + return env + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--repo", type=Path, required=True) + parser.add_argument("--work", type=Path, required=True) + parser.add_argument("--dry-run", action="store_true") + args = parser.parse_args() + work = args.work.resolve() + rw.need( + os.name == "posix" and sys.flags.optimize == 0, + "POSIX and enabled inherited assertions", + ) + rw.need( + not work.exists() and not work.is_relative_to(v.ROOT), + "fresh external workspace", + ) + v.authenticate() + work.mkdir(parents=True) + sys.dont_write_bytecode, sys.pycache_prefix = True, str(work / "bytecode") + source = work / "pr3015" + export(args.repo.resolve(), source) + data = parameters(source, work) + env = environment(work) + stages = [] + command = [ + sys.executable, + "-B", + str(source / "reproduce.py"), + "--repo", + str(args.repo.resolve()), + "--work", + str(work / "run"), + "--jobs", + "1", + "--dry-run", + ] + stage("source-preflight", command, work, env, stages) + recipe = v.read(work / "run/PREFLIGHT.json")["commands"] + rw.need([name for name, _ in recipe] == NAMES, "exact complete predecessor recipe") + v.save( + work / "RECIPE.json", {"commands": recipe, "changes": retarget(recipe, data)} + ) + if args.dry_run: + print("PREFLIGHT_ONLY_NOT_A_RELEASE", flush=True) + return + for name, command in recipe: + stage(name, command, work, env, stages) + result = check(work, source, stages) + v.save(work / "RESULT.json", result) + print(result["status"], result["kappa"], flush=True) + + +if __name__ == "__main__": + main() diff --git a/research/rank7-shared-restore-fanin/rewrite.py b/research/rank7-shared-restore-fanin/rewrite.py new file mode 100644 index 0000000000..c83002bc0d --- /dev/null +++ b/research/rank7-shared-restore-fanin/rewrite.py @@ -0,0 +1,96 @@ +# SPDX-License-Identifier: Apache-2.0 +"""One shared dirty-source covector across two separated restore consumers.""" + +import copy + +LOW = [256, 128, 64, 34, 17, 11, 4] +FULL = [256, 128, 64, 32, 16, 8, 4, 2, 1] +HIGH = [256, 128, 64, 34, 16, 10, 4, 1] +LOCAL = {"1": 2441, "2": 708, "3": 232, "4": 108, "5": 18, "8": 8} +INVENTORY = {"4": 26, "5": 2, "6": 16, "7": 52, "8": 99, "9": 213} + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def r1(word, specification, variant): + """Apply Jeremy Kothe's literal R1, retaining its exact source preimage.""" + edit = specification["edits"][variant][0] + need(len(specification["edits"][variant]) == 1, "one credited R1 edit") + need( + (edit["section"], edit["start"], edit["stop"]) == ("restore", 178, 180), + "R1 source address", + ) + need(word["restore"][178:180] == edit["old"], "R1 literal preimage") + changed = copy.deepcopy(word) + changed["restore"][178:180] = copy.deepcopy(edit["new"]) + return changed + + +def r2(word): + """Aggregate X40-2*X54, use it twice, and restore both dirty sources.""" + old = word["restore"] + need(len(old) in (203, 204), "bounded parent or R1 restore") + expected = { + 162: ["add", 18, 40, 1, 1], + 163: ["add", 18, 54, -2, 1], + 175: ["add", 22, 40, 1, 1], + 177: ["add", 22, 54, -2, 1], + } + for index, gate in expected.items(): + need(old[index] == gate + [HIGH], "literal R2 preimage at " + str(index)) + need( + old[176] == ["add", 22, 45, -1, 1, HIGH], "literal commuting consumer preimage" + ) + # Only these four source contacts may occur after the aggregation point. + contacts = [ + i for i in range(162, len(old)) if any(r in (40, 54) for r in old[i][1:3]) + ] + need(contacts == list(expected), "no intervening source observer or writer") + changed = copy.deepcopy(word) + gates = [copy.deepcopy(g) for i, g in enumerate(old) if i not in (163, 177)] + gates.insert(162, ["add", 40, 54, -2, 1, LOW.copy()]) + gates.append(["add", 40, 54, 2, 1, FULL.copy()]) + changed["restore"] = gates + need(len(gates) == len(old), "R2 preserves scalar gate count") + return changed + + +def finish(word, original, frames): + """Re-derive both paid profiles and the complete inverse cleanup.""" + profile, inventory = frames.frame_report(word) + need(inventory == INVENTORY, "unchanged helper widths") + word["report"]["local_profile"] = profile + word["report"]["width_inventory"] = inventory + forward = copy.deepcopy(word) + forward["A"] = forward["A"][forward["prelude_events"] :] + word["cleanup"] = frames.derive_cleanup(forward, frames.restored_of(original)) + changes = {key for key in original if original[key] != word[key]} + need(changes <= {"restore", "report", "cleanup"}, "only declared sections change") + need(len(word["helper_final"]) == 91, "all private buffers retained") + return word + + +def stage_spec(original, composed): + """Encode R1+R2 for PR3015's unchanged declared-edit source builder.""" + # The combined hunk is necessary because R2's second deletion adjoins R1. + return [ + { + "id": "R1+R2-shared-consumers", + "section": "restore", + "start": 162, + "stop": 180, + "old": original["restore"][162:180], + "new": composed["restore"][162:180], + }, + { + "id": "R2-full-source-restoration", + "section": "restore", + "start": 203, + "stop": 203, + "old": [], + "new": [composed["restore"][-1]], + }, + ] diff --git a/research/rank7-shared-restore-fanin/test_verify.py b/research/rank7-shared-restore-fanin/test_verify.py new file mode 100644 index 0000000000..34fdef928d --- /dev/null +++ b/research/rank7-shared-restore-fanin/test_verify.py @@ -0,0 +1,129 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Behavioral controls for the exact source rewrite and release recipe.""" + +import copy +import unittest +from unittest.mock import patch + +import frame_trace +import reproduce +import rewrite as rw +import verify as v + + +class SharedRestoreTests(unittest.TestCase): + @classmethod + def setUpClass(cls): + v.authenticate() + cls.parent = v.read(v.PARENT / "data/WORD-base.json.gz") + cls.specification = v.read(v.PACKAGE / "vendor/R1.json") + cls.frames = v.load(v.PARENT / "vendor/preload_move.py", "test_bound_frames") + + def test_dirty_sources_and_targets(self): + self.assertEqual( + v.scalar_identity(), + [ + ["1", "0", "0", "0"], + ["0", "1", "0", "0"], + ["1", "-2", "1", "0"], + ["1", "-2", "0", "1"], + ], + ) + + def test_both_literal_providers(self): + for variant in ("base", "extra"): + candidates = v.words(variant, self.frames) + self.assertEqual(candidates["R1R2"]["report"]["local_profile"], rw.LOCAL) + self.assertEqual(len(candidates["R1"]["restore"]), 204) + self.assertEqual(len(candidates["R1R2"]["restore"]), 204) + self.assertEqual(len(candidates["R1R2"]["helper_final"]), 91) + self.assertEqual(len(candidates["R1"]["cleanup"]), 5208) + self.assertEqual(len(candidates["R1R2"]["cleanup"]), 5208) + for key in ( + "A", + "B", + "warps", + "compensation", + "helper_final", + "start_extra", + ): + self.assertEqual(candidates["R1R2"][key], candidates["parent"][key]) + + def test_frame_gain_and_bad_high_frame(self): + r1 = rw.r1(self.parent, self.specification, "base") + candidate = rw.r2(r1) + old, entry = frame_trace.census(r1) + new, new_entry = frame_trace.census(candidate) + self.assertEqual(entry, new_entry) + self.assertEqual(new["1"] - old["1"], -2) + self.assertEqual(new["2"] - old["2"], 1) + candidate["restore"][162][-1] = rw.HIGH + too_expensive, _ = frame_trace.census(candidate) + self.assertEqual(too_expensive, old) + + def test_source_addressed_order_refused(self): + composed = rw.r2(rw.r1(self.parent, self.specification, "base")) + # R2 shifts R1's original address. Refuse that order instead of silently + # reinterpreting a source-addressed edit on a different word. + self.assertEqual(len(composed["restore"]), 204) + with self.assertRaisesRegex(ValueError, "R1 literal preimage"): + rw.r1(rw.r2(self.parent), self.specification, "base") + + def test_changed_preimages_refused(self): + for index, field, value in ((162, 3, -1), (163, -1, rw.FULL), (177, 2, 55)): + mutant = copy.deepcopy(self.parent) + mutant["restore"][index][field] = value + with self.assertRaisesRegex(ValueError, "literal R2 preimage"): + rw.r2(mutant) + + def test_consumer_observer_refused(self): + mutant = copy.deepcopy(self.parent) + mutant["restore"][176] = ["add", 45, 22, 1, 1, rw.HIGH] + with self.assertRaisesRegex(ValueError, "commuting consumer"): + rw.r2(mutant) + + def test_hidden_source_contact_refused(self): + mutant = copy.deepcopy(self.parent) + mutant["restore"][164] = ["add", 18, 54, 1, 1, rw.HIGH] + with self.assertRaisesRegex(ValueError, "observer"): + rw.r2(mutant) + + def test_declared_stage_reconstructs_exact_restore(self): + original = self.parent + composed = rw.r2(rw.r1(original, self.specification, "base")) + actual = copy.deepcopy(original["restore"]) + edits = rw.stage_spec(original, composed) + for edit in sorted(edits, key=lambda item: -item["start"]): + self.assertEqual(actual[edit["start"] : edit["stop"]], edit["old"]) + actual[edit["start"] : edit["stop"]] = edit["new"] + self.assertEqual(actual, composed["restore"]) + + def test_source_pin_failure(self): + with ( + patch.object(v, "digest", return_value="0" * 64), + self.assertRaisesRegex(ValueError, "source pin"), + ): + v.authenticate() + + def test_only_declared_recipe_arguments_change(self): + recipe = [ + ["declared-edit-stage", ["builder", "--local-package", "original"]], + [ + "derive-closed-adapters", + ["derive", "--source-profile", "old", "--source-commit", "old"], + ], + [ + "complete-admission", + ["admit", "--source-profile", "old", "--fill", "unchanged"], + ], + ] + changes = reproduce.retarget(recipe, v.PACKAGE) + self.assertEqual(len(changes), 4) + self.assertEqual(recipe[-1][1][-2:], ["--fill", "unchanged"]) + self.assertEqual(recipe[-1][1][2], "rank7-shared-restore-fanin") + with self.assertRaisesRegex(ValueError, "four|explicit"): + reproduce.retarget([], v.PACKAGE) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/rank7-shared-restore-fanin/vendor/PR3015-CREDITS.md b/research/rank7-shared-restore-fanin/vendor/PR3015-CREDITS.md new file mode 100644 index 0000000000..3b6022cd64 --- /dev/null +++ b/research/rank7-shared-restore-fanin/vendor/PR3015-CREDITS.md @@ -0,0 +1,17 @@ +# Credits + +- **PR #2908, Jeremy Diviney**: the paired input/output extraction, its compensation rule `C*S`, the exact two-sided certificate (`structure.py`, vendored unchanged) and the closed-adapter admission chain. +- **PR #2917, Mason Hale**: the nine paired extractions and 82-endpoint words under PR2942, the refit/compose producer model that stage 2 follows, the T74 chronology (ORDER/DISPATCH), the allocation checker, moment auditor, extension stage and adapter derivation reused here. +- **PR #2957 / #2948 / #2966, Jeremy Kothe (jeremykothe2)**: the fourteen declared exactness-preserving gate rewrites in five classes (R-retime, A3779-cut-start-read, PM-carrier-lender-entry, B-carrier-retime, A-commuting-swap) and their pure applier (`vendor/declared_rewrites.py`, vendored unchanged); stage 3 composes exactly these rewrites onto this package's stage-2 word (`data/REWRITES-2957.json`, re-addressed with exact preimages). PR2966 composed the same rewrites onto our PR2942 words. +- **PR #2969, Dugongue**: the PR2942 + PR2957 composition at T370 and its cap-level headline nomination, this package's comparator and moment baseline (`allocation/baseline/`). Our stage 3 composes the same fourteen rewrites, here onto the stage-2 word. +- **PR #2918 (research/helper408-rank7-pairing), RossRichardson**: the fixed-cut rank-seven obstruction for helper408; this package's census of fresh rank-7 extractions reproduces it exactly and is consistent with it. +- **PR #2894 / #2833, Jeremy Kothe**: the preload re-synthesis supplier, the frame accounting and inverse-reverse cleanup (`vendor/preload_move.py`), the source materializer and the inherited supplier lineage. +- **PR #2857 / #2848, Yiyang Lu (Lyy-iiis)**: the shared-kernel words, the staged native/overlay tooling and the chronological flow model and realization (edge colouring) used to construct the allocation; PR2843 (Marius-Paul Dumitrean) is that flow model's starting point. +- **PR #2863 / #2839, Dugongue**: the packing lineage and the PR2839 owner engine. +- **Tekalign**: the independent owner/chronology checker (`allocation/vendor/independent_owners.py`) and admission tooling. +- **icekylinx**: the exact free-operator auditor retained as `vendor/audit_local.py` (PR2833). +- **themilkman216**: the observation that a cap-level allocation of these inventories needs a T whose basic counts are integral, which the allocation's degenerate-face step builds on. +- **Gareth Davidson (bitplane), PR #1995 / #2013**: the fixed-word terminal-subspace bounds that frame stage 1's scope; earlier rank-seven helper ends on other words are in `research/complex-rank7-end-pair`, `research/k8-rank7-composition` and the PR1090/PR1104 lineage (credited there). +- **PR #2930 / #2942, Marius-Paul Dumitrean**: the cap allocation of PR2917's words, the four normal-45 extractions under these words, the relaxation tools and the overlay/producer conventions reused here. +- **New here (Marius-Paul Dumitrean, with substantial AI assistance from Anthropic Claude via Claude Code)**: the codimension-2 census on paired-extraction words, the joint end-frame lowering of 22 restored helpers in five groups (stage 1), the five further extractions it makes profitable (stage 2), the exact composition with PR2957's rewrites (stage 3), the producer and local verification for all three stages, the overlay stage `rank7-joint-endframes` with its rebuild guards, the adapter generalization to six width classes, the literal T74 allocation of the changed inventory, its relaxation certificates and recorded gap, and the complete fresh replay. +- **New here (Jeremy Kothe (jeremykothe2), with AI assistance; edit found by our Stack2979 search)**: the declared literal edit stage (`edits/`, `tools/build_edits.py`) with its independent review, the edit R1 on PR #2979's restore section, the re-derived paid profile and cap certificate. PR #2979 (mdumitrean) is the base and is credited first for everything else. diff --git a/research/rank7-shared-restore-fanin/vendor/PR3015-NOTICE b/research/rank7-shared-restore-fanin/vendor/PR3015-NOTICE new file mode 100644 index 0000000000..70a09b472e --- /dev/null +++ b/research/rank7-shared-restore-fanin/vendor/PR3015-NOTICE @@ -0,0 +1,28 @@ +research/rank7-joint-endframes +Copyright 2026 Marius-Paul Dumitrean. Licensed under the Apache License, Version 2.0. +Prepared with substantial AI assistance (Anthropic Claude, via Claude Code). + +This package retains, byte-identical, Apache-2.0 files from: PR #2942 (Marius-Paul Dumitrean, head +a027b0f6fdb0ab2b42ba10fc31b53960166bf2bf, research/paired-extension-normal45): data/PARENT-base.json.gz and +data/PARENT-extra.json.gz (its data/WORD-*.json.gz), comparators/PR2942-CLAIM.json and tools/wordedit.py; PR #2917 +(Mason Hale, head 224bd5e56041c40078ff6b5fa7393733a215de5c, research/paired-helper-extension): structure.py (Jeremy +Diviney's PR2908 two-sided certificate checker), vendor/audit_local.py (PR2833's independent exact auditor, icekylinx +attribution), vendor/preload_move.py (Jeremy Kothe's PR2894 frame accounting and cleanup), allocation/ORDER.json, +allocation/DISPATCH.json and allocation/vendor/ (independent_owners.py: Tekalign's independent owner checker as vendored +by PR2839/PR2917; PLAN.json.gz, TEMPLATE.json.gz); PR #2957 (Jeremy Kothe, head b74b25f3ccc84c16e1a801d73b2f47e5ea764c78, +research/paired-extension-cap-fill-swaps): vendor/declared_rewrites.py (the pure applier of the fourteen declared +rewrites) and comparators/PR2957-CLAIM.json; PR #2966 (Jeremy Kothe, head e62d3eb9005117d82a9babcfa937ecc53237c490, +research/paired-extension-normal45-rewrites): comparators/PR2966-CLAIM.json; PR #2969 (Dugongue, head +e2ca469b08385d3d5e29a918d66dbefaf889e9f3, research/paired-swap-normal45): allocation/baseline/ (its CLAIM.json and its +allocation ORDER.json and PROFILE.json); and PR #2930 (head 81f3b5d12977eba09e06fbff729167d59faabe90): tools/relax.py, +tools/root.py, tools/relax_exact.py. +data/REWRITES-2957.json is Jeremy Kothe's PR2957 rewrite list, re-addressed to this package's stage-2 word with exact +preimages (every entry keeps a credit field). producer.py follows PR2917's producer.py (Mason Hale) for its paired steps; +verify.py, check_allocation.py, check_cap.py, run_registered.py and reproduce.py adapt our PR2942 versions of PR2917's and +PR2930's; tools/audit_allocation_moment.py is PR2917's exact moment auditor with only its authenticated baseline changed (to +the PR2969 headline); tools/derive_adapters.py generalizes PR2917's adapter derivation (PR2908, Jeremy Diviney); +tools/build_overlay.py follows the overlay conventions of PR2908's and PR2917's builders. construction/allocation/ retains +the flow model of PR2857/PR2843 (Yiyang Lu, Marius-Paul Dumitrean) as adapted for this allocation. All original notices of +the exported predecessor packages remain in force. + +Derived work (Apache-2.0): this package is PR #2979's (Marius-Paul Dumitrean, head be191346, research/rank7-joint-endframes) package, retained byte-identical except for the files named in README.md, plus a declared literal edit stage by Jeremy Kothe (jeremykothe2), with AI assistance: edits/ (declared_edits.py, edits_review.py, EDITS.json, FINAL-WORD-*.json.gz), tools/build_edits.py, EDIT-PINS.json, comparators/PR2979-CLAIM.json, and the edits to reproduce.py, run_registered.py, check_allocation.py, check_cap.py, allocation/PROFILE.json, allocation/PROVIDERS.json, certificates/RELAX-CAP.json, CLAIM.json, PINS.json and the release contract files (RELEASE.json, verify_release.py, verify_manifest.py). PR #2979's own evidence is kept under evidence/pr2979/. diff --git a/research/rank7-shared-restore-fanin/vendor/PR3030-FINITE.json b/research/rank7-shared-restore-fanin/vendor/PR3030-FINITE.json new file mode 100644 index 0000000000..0ddf2aba46 --- /dev/null +++ b/research/rank7-shared-restore-fanin/vendor/PR3030-FINITE.json @@ -0,0 +1,94 @@ +{ + "calls": 6660, + "idle": { + "1": 173160, + "3": 49617, + "48": 281903, + "5": 17205 + }, + "live": 663040, + "moment": { + "exchange_sign": { + "delta": { + "1": 20, + "14": -10, + "3": 17, + "48": 3, + "5": -15 + }, + "factored_f_derivative_upper": "-9740691/100000", + "saving_interval": "0 < b <= 1/100" + }, + "gain_over_previous_root": [ + "15520213124915363/10000000000000000000000000", + "3104042624983073/2000000000000000000000000" + ], + "previous_released_kappa": "17291512039830184429979999999999999999999998999999999999999999999999/10000000000000000000000000000000000000000000000000000000000000000000000", + "r1_cap": { + "cap_lower": "345830551200866186907/200000000000000000000000", + "cap_upper": "17291527560043309345351/10000000000000000000000000", + "idle_per_replica": { + "1": "234", + "3": "1341/20", + "48": "7619/20", + "5": "93/4" + }, + "invariant": { + "cap_requires_T_multiple_of": 20, + "first_multiple_of_74": 740, + "identity": "20*N_[9,9,9,9,9]@48 = 1341*T", + "scope": "Pattern integrality; chronological sufficiency is not asserted." + }, + "minimum_slack_lower": "330765675305227204675371142393288108400151493175513616739741339618653761718041326298111057624781171125553985546713931380045589238715164684519680158082564740064663626585139779201278666945976271879210312552348945421842669479860034347625742282914882395550466970485099678801067095436401756055414599223858358045300620622572136335593899309576755132023072924000625232706202289892486468856482758190936016483225256005340027972594846416378903928488242877276718725872416334489569899876284894464567074525397636741615414416512178272514355557374077726632979830127341350785520875007989552785927437863408466173223802409362040928161903300682009368388022327606117750186058531177130486222532353473629990336123001666673453285550918689932752488873889800407408618663032684827164043100388063145568074124864004671327888352440148634170348081682763216459720440600473567758633447479756936881069232841299315182009213270746341095947229872623984953305659320971822234633628503084874050627189372339056880769747466281694324513868890186542568399493669814325528063369943581616724732903252851537556934617596147852096403830386971101932076078846509096157094005135661650016075760947032213965707873129939184689263987243478656040906464411334211690007822733347623898160446742448648210266592497727349409694316897300189398121201087445724945334874140855821854415515276641951455907807350241364838774433095096175333305053290637933525897282705413481161097167181637390050045065310941579633986151479433320996941088323147696390012023269/81041342522688389710889387537294203079509119498590816677390723091620647310394495647029073126180702147730052952998589633954567841435821298786820185301991996265365431464176659884385965729599723770208940372607986728020752670720000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "patterns": 2551, + "strict_patterns": 2539, + "tight_patterns": 12 + }, + "root": [ + "345830551200866186907/200000000000000000000000", + "17291527560043309345351/10000000000000000000000000" + ] + }, + "physical": 663549, + "profile": { + "1": 16443540, + "2": 4708620, + "3": 1594737, + "4": 719280, + "48": 281903, + "5": 137085, + "8": 53280 + }, + "rank_mass": 48165120, + "replicas": 740, + "roles": 2717280, + "scope": "Finite composed allocation and moment; fresh release is separate.", + "status": "PASS_T740_R1_FINITE", + "stock": { + "buffers": 91, + "group_order_times_physical_bit_length": 2647, + "live": 663040, + "namespaces": { + "centers": [ + 663040, + 663048 + ], + "coefficients": [ + 663547, + 663549 + ], + "tableau": [ + 663048, + 663456 + ], + "zero_buffers": [ + 663456, + 663547 + ] + }, + "payload": 2048, + "physical": 663549, + "reserve": 1512, + "stock_l2_bits": 1324 + } +} diff --git a/research/rank7-shared-restore-fanin/vendor/R1.json b/research/rank7-shared-restore-fanin/vendor/R1.json new file mode 100644 index 0000000000..90894fc659 --- /dev/null +++ b/research/rank7-shared-restore-fanin/vendor/R1.json @@ -0,0 +1,216 @@ +{ + "declared": { + "local_profile": { + "1": 2443, + "2": 707, + "3": 232, + "4": 108, + "5": 18, + "8": 8 + }, + "width_inventory": { + "4": 26, + "5": 2, + "6": 16, + "7": 52, + "8": 99, + "9": 213 + } + }, + "edits": { + "base": [ + { + "id": "R1", + "new": [ + [ + "add", + 61, + 63, + 1, + 1, + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ] + ], + [ + "add", + 22, + 61, + -1, + 1, + [ + 256, + 128, + 64, + 34, + 16, + 10, + 4, + 1 + ] + ], + [ + "add", + 61, + 63, + -1, + 1, + [ + 256, + 128, + 64, + 32, + 16, + 8, + 4, + 2, + 1 + ] + ] + ], + "old": [ + [ + "add", + 22, + 61, + -1, + 1, + [ + 256, + 128, + 64, + 34, + 16, + 10, + 4, + 1 + ] + ], + [ + "add", + 22, + 63, + -1, + 1, + [ + 256, + 128, + 64, + 34, + 16, + 10, + 4, + 1 + ] + ] + ], + "section": "restore", + "start": 178, + "stop": 180 + } + ], + "extra": [ + { + "id": "R1", + "new": [ + [ + "add", + 61, + 63, + 1, + 1, + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ] + ], + [ + "add", + 22, + 61, + -1, + 1, + [ + 256, + 128, + 64, + 34, + 16, + 10, + 4, + 1 + ] + ], + [ + "add", + 61, + 63, + -1, + 1, + [ + 256, + 128, + 64, + 32, + 16, + 8, + 4, + 2, + 1 + ] + ] + ], + "old": [ + [ + "add", + 22, + 61, + -1, + 1, + [ + 256, + 128, + 64, + 34, + 16, + 10, + 4, + 1 + ] + ], + [ + "add", + 22, + 63, + -1, + 1, + [ + 256, + 128, + 64, + 34, + 16, + 10, + 4, + 1 + ] + ] + ], + "section": "restore", + "start": 178, + "stop": 180 + } + ] + } +} \ No newline at end of file diff --git a/research/rank7-shared-restore-fanin/verify.py b/research/rank7-shared-restore-fanin/verify.py new file mode 100644 index 0000000000..08412ada94 --- /dev/null +++ b/research/rank7-shared-restore-fanin/verify.py @@ -0,0 +1,388 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Rebuild R2 and its R1 composition, audit actual words, certify full moments.""" + +import argparse +import copy +import gzip +import hashlib +import importlib.util +import json +import subprocess +import sys +import tempfile +from fractions import Fraction +from pathlib import Path + +import frame_trace +import rewrite as rw + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +PARENT = ROOT / "research/rank7-joint-endframes" +EXPECTED = {1: 1643016, 2: 471528, 3: 159468, 4: 71928, 5: 13716, 8: 5328, 48: 28190} + + +def read(path): + raw = path.read_bytes() + rw.need(len(raw) <= 2_000_000, "bounded input bytes") + return json.loads(gzip.decompress(raw) if path.suffix == ".gz" else raw) + + +def save(path, value): + path.write_text(json.dumps(value, indent=2, sort_keys=True) + "\n") + + +def canonical(value): + return hashlib.sha256( + json.dumps(value, sort_keys=True, separators=(",", ":")).encode() + ).hexdigest() + + +def digest(path): + return hashlib.sha256(path.read_bytes()).hexdigest() + + +def authenticate(): + pins = read(PACKAGE / "SOURCES.json")["files"] + rw.need(len(pins) <= 16, "bounded dependency inventory") + for entry in pins: + if entry["usage"] == "input": + rw.need( + digest(ROOT / entry["path"]) == entry["sha256"], + "source pin: " + entry["path"], + ) + vendor = read(PACKAGE / "VENDOR.json") + rw.need(len(vendor) <= 4, "bounded retained sources") + for entry in vendor: + rw.need(digest(PACKAGE / entry["path"]) == entry["sha256"], "retained pin") + + +def load(path, name): + # Callers authenticate every external module before loading it. + spec = importlib.util.spec_from_file_location(name, path) + rw.need(spec is not None and spec.loader is not None, "source module") + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +def words(variant, frames): + original = read(PARENT / f"data/WORD-{variant}.json.gz") + r1 = rw.r1(original, read(PACKAGE / "vendor/R1.json"), variant) + candidates = { + "parent": copy.deepcopy(original), + "R1": r1, + "R2": rw.r2(original), + "R1R2": rw.r2(r1), + } + expected = { + "parent": {"1": 2445, "2": 706}, + "R1": {"1": 2443, "2": 707}, + "R2": {"1": 2443, "2": 707}, + "R1R2": {"1": 2441, "2": 708}, + } + for name, word in candidates.items(): + rw.finish(word, original, frames) + profile = {**rw.LOCAL, **expected[name]} + rw.need(word["report"]["local_profile"] == profile, "exact local bill") + return candidates + + +def scalar_identity(): + """Independent four-register Q matrix check, not a frame-engine result.""" + rows = [[Fraction(i == j) for j in range(4)] for i in range(4)] + original = copy.deepcopy(rows) + for target in (2, 3): + original[target] = [ + a + b - 2 * c + for a, b, c in zip(original[target], original[0], original[1], strict=True) + ] + for target, source, coefficient in ((0, 1, -2), (2, 0, 1), (3, 0, 1), (0, 1, 2)): + rows[target] = [ + a + coefficient * b for a, b in zip(rows[target], rows[source], strict=True) + ] + rw.need(rows == original, "dirty-source/target matrix identity") + rw.need(rows[:2] == [[1, 0, 0, 0], [0, 1, 0, 0]], "both sources restored") + return [[str(x) for x in row] for row in rows] + + +def restore_matrix(word): + """Exact scalar action of every literal restore gate on all 704 inputs.""" + rw.need(len(word["restore"]) <= 204, "bounded restore matrix") + rows = [{i: Fraction(1)} for i in range(704)] + for gate in word["restore"]: + target = gate[1] + rw.need(0 <= target < 704, "restore target") + if gate[0] == "add": + source, coefficient = gate[2], Fraction(gate[3], gate[4]) + rw.need(0 <= source < 704 and target != source, "restore source") + for column, value in tuple(rows[source].items()): + total = rows[target].get(column, 0) + coefficient * value + if total: + rows[target][column] = total + else: + rows[target].pop(column, None) + else: + rw.need(gate[0] == "scale", "restore scalar opcode") + coefficient = Fraction(gate[2], gate[3]) + rw.need(coefficient != 0, "invertible restore scale") + rows[target] = {c: coefficient * x for c, x in rows[target].items()} + return rows + + +def audit(word, label, work, accepted=True, reason=None): + path, output = work / (label + ".json.gz"), work / (label + ".audit.json") + payload = json.dumps(word, sort_keys=True, separators=(",", ":")).encode() + path.write_bytes(gzip.compress(payload, compresslevel=1, mtime=0)) + command = [ + sys.executable, + "-I", + "-B", + "-X", + "pycache_prefix=" + str(work / "audit-bytecode"), + str(PARENT / "vendor/audit_local.py"), + "--word", + str(path), + "--output", + str(output), + ] + with (work / (label + ".log")).open("w") as log: + result = subprocess.run( + command, stdout=log, stderr=subprocess.STDOUT, timeout=30, check=False + ) + if not accepted: + rw.need(result.returncode != 0, "mutant accepted: " + label) + text = (work / (label + ".log")).read_text() + rw.need( + reason is not None and reason in text, "actual mutation rejection reason" + ) + return "rejected" + rw.need(result.returncode == 0, "failed actual word audit: " + label) + report = read(output) + rw.need(report["status"] == "PASS_INDEPENDENT_EXACT_BORROWING_WORD", "audit status") + rw.need( + report["checked_columns"] == 632 and report["zero_buffers"] == 91, + "all dirty columns and private buffers", + ) + rw.need( + report["orientations"] == {"forward": "PASS", "dual": "PASS"}, + "both orientations", + ) + return { + "canonical_sha256": canonical(word), + "local_profile": report["local_profile"], + "width_inventory": report["width_inventory"], + "checked_columns": 632, + "orientations": report["orientations"], + "zero_buffers": 91, + } + + +def controls(candidate, original, variant, work): + labels = [] + for name in ( + "omit-aggregate", + "wrong-aggregate", + "omit-undo", + "wrong-undo", + "frame-too-small", + "stale-cleanup", + "stale-profile", + ): + mutant = copy.deepcopy(candidate) + if name == "omit-aggregate": + del mutant["restore"][162] + elif name == "wrong-aggregate": + mutant["restore"][162][3] = -1 + elif name == "omit-undo": + mutant["restore"].pop() + elif name == "wrong-undo": + mutant["restore"][-1][3] = -2 + elif name == "frame-too-small": + mutant["restore"][162][-1] = rw.LOW[:-1] + elif name == "stale-cleanup": + mutant["cleanup"] = copy.deepcopy(original["cleanup"]) + else: + mutant["report"]["local_profile"] = copy.deepcopy( + original["report"]["local_profile"] + ) + rw.need(mutant != candidate, "effective rejection control") + if name in ("omit-aggregate", "wrong-aggregate", "omit-undo", "wrong-undo"): + rw.need( + restore_matrix(mutant) != restore_matrix(candidate), + "independent scalar-equivalence control", + ) + reason = "explicit cleanup differs" + if name == "frame-too-small": + reason = "frame not monotone" + elif name == "stale-profile": + reason = "paid profile mismatch" + audit(mutant, variant + "-" + name, work, accepted=False, reason=reason) + labels.append(name) + # A coefficient-preserving but semantically invalid intervening read must + # fail the rewriter boundary, before any generated word is accepted. + mutant = copy.deepcopy(original) + mutant["restore"][164] = ["add", 18, 40, 1, 1, rw.FULL] + try: + rw.r2(mutant) + except ValueError as error: + rw.need("observer" in str(error), "contact guard rejects the actual obligation") + else: + raise ValueError("intervening source observer accepted") + return labels + ["intervening-source-observer"] + + +def moment(): + root = load(PARENT / "tools/root.py", "source_bound_moment") + parent = {int(k): n for k, n in read(PARENT / "allocation/PROFILE.json").items()} + r1 = {**parent, 1: parent[1] - 1332, 2: parent[2] + 666} + rw.need( + {**parent, 1: parent[1] - 2664, 2: parent[2] + 1332} == EXPECTED, + "complete bill", + ) + lower, upper = root.kappa_from_profile(EXPECTED, 74) + r1_lower, r1_upper = root.kappa_from_profile(r1, 74) + previous = read(PACKAGE / "vendor/PR3030-FINITE.json") + previous_profile = {int(k): n for k, n in previous["profile"].items()} + previous_cap_lower, previous_cap_upper = root.kappa_from_profile( + previous_profile, 740 + ) + rw.need( + [str(previous_cap_lower), str(previous_cap_upper)] + == previous["moment"]["root"], + "pinned T740 comparison", + ) + rw.need( + lower > previous_cap_upper > r1_upper, + "strict gain beyond current published T740 candidate", + ) + rw.need(root.rank_mass(EXPECTED) == 74 * 65088, "complete rank mass") + return { + "T": 74, + "calls": 666, + "profile": EXPECTED, + "rank_mass": 74 * 65088, + "root": [str(lower), str(upper)], + "R1_root": [str(r1_lower), str(r1_upper)], + "PR3030_root": [str(previous_cap_lower), str(previous_cap_upper)], + "gain_over_PR3030": [ + str(lower - previous_cap_upper), + str(upper - previous_cap_lower), + ], + "packing_relaxation": packing_ceiling(root, lower, upper), + } + + +def packing_ceiling(root, lower, upper): + local = {int(r): n for r, n in rw.LOCAL.items()} + idle_mass = 65088 - 9 * sum(r * n for r, n in local.items()) + rw.need( + idle_mass == 18837 and 2 * 51**2 < 73**2 <= 2 * 52**2, + "coverage and halving cap", + ) + relaxed = {r: 9 * n for r, n in local.items()} + relaxed[51] = Fraction(idle_mass, 51) + cap_lower, cap_upper = root.kappa_from_profile(relaxed, 1) + rw.need(upper < cap_lower, "favorable packing ceiling, not a feasible invoice") + return { + "maximum_idle_rank": 51, + "idle_mass_per_call": "2093", + "root": [str(cap_lower), str(cap_upper)], + "fraction_realized": [str(lower / cap_upper), str(upper / cap_lower)], + "scope": ( + "Coverage/halving relaxation in the moment variable; " + "not a packing construction." + ), + } + + +def run(work): + authenticate() + sys.dont_write_bytecode = True + sys.pycache_prefix = str(work / "module-bytecode") + frames = load(PARENT / "vendor/preload_move.py", "source_bound_frames") + reports = {} + for variant in ("base", "extra"): + candidates = words(variant, frames) + expected_restore = restore_matrix(candidates["parent"]) + rw.need( + all( + restore_matrix(word) == expected_restore for word in candidates.values() + ), + "all literal restore operators agree on every scalar input", + ) + reports[variant] = { + name: audit(word, variant + "-" + name, work) + for name, word in candidates.items() + } + reports[variant]["restore_matrix_sha256"] = canonical( + [sorted((c, str(x)) for c, x in row.items()) for row in expected_restore] + ) + reports[variant]["controls"] = controls( + candidates["R1R2"], candidates["parent"], variant, work + ) + before, entrance = frame_trace.census(candidates["R1"]) + after, new_entrance = frame_trace.census(candidates["R1R2"]) + delta = { + r: after.get(r, 0) - before.get(r, 0) for r in set(before) | set(after) + } + rw.need( + {r: n for r, n in delta.items() if n} == {"1": -2, "2": 1}, + "separate four-register set-span census", + ) + rw.need(entrance == new_entrance, "same restore-entry frames") + reports[variant]["frame_census"] = { + "R1": before, + "R1R2": after, + "restore_entry": entrance, + } + return { + "status": "PASS_SHARED_RESTORE_FANIN", + "variants": reports, + "scalar_matrix": scalar_identity(), + "moment": moment(), + "scope": ( + "Finite exact words and full fixed-allocation moment; " + "native/admission release is separate." + ), + } + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument( + "--work", type=Path, help="fresh external directory; retained on failure" + ) + parser.add_argument( + "--record", + action="store_true", + help="write evidence/FINITE.json after validation", + ) + args = parser.parse_args() + if args.work: + work = args.work.resolve() + rw.need( + not work.exists() and not work.is_relative_to(ROOT), + "fresh external work directory", + ) + work.mkdir(parents=True) + result = run(work) + save(work / "RESULT.json", result) + else: + with tempfile.TemporaryDirectory(prefix="shared-restore-") as directory: + result = run(Path(directory)) + result = json.loads(json.dumps(result, sort_keys=True)) + if args.record: + (PACKAGE / "evidence").mkdir(exist_ok=True) + save(PACKAGE / "evidence/FINITE.json", result) + else: + rw.need( + result == read(PACKAGE / "evidence/FINITE.json"), + "published deterministic evidence", + ) + print(result["status"], "local=2441,708,232,108,18,8 controls=16", flush=True) + + +if __name__ == "__main__": + main() diff --git a/research/rank7-shared-restore-fanin/verify_release.py b/research/rank7-shared-restore-fanin/verify_release.py new file mode 100644 index 0000000000..04eea38a09 --- /dev/null +++ b/research/rank7-shared-restore-fanin/verify_release.py @@ -0,0 +1,277 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Check retained release bindings, not a substitute for a fresh native replay.""" + +import copy +from fractions import Fraction + +import reproduce +import rewrite as rw +import verify as v + +REQUIRED = { + "RESULT.json", + "ADMISSION-RESULT.json", + "NATIVE-RECEIPT.json", + "RELEASE-RECEIPT.json", + "SOURCE-MANIFEST.json", + "EDIT-DERIVATION.json", + "STAGES.json", + "RECIPE.json", + "WORD-base.json.gz", + "WORD-extra.json.gz", + "INVOICE.json.gz", +} + + +def load(): + directory = v.PACKAGE / "evidence" + bindings = v.read(directory / "BINDINGS.json") + allowed = REQUIRED | {"ENVIRONMENT.json", "ADMISSION-STAGES.json"} + allowed |= { + "logs/" + name + ".log.txt" for name in ["source-preflight", *reproduce.NAMES] + } + rw.need(REQUIRED <= set(bindings) <= allowed, "closed retained evidence inventory") + hashes = {} + for name, expected in bindings.items(): + path = directory / name + rw.need(not path.is_symlink() and path.is_file(), "regular retained evidence") + hashes[name] = v.digest(path) + rw.need(hashes[name] == expected, "retained evidence hash: " + name) + records = { + name: v.read(directory / name) for name in REQUIRED if not name.endswith(".gz") + } + records["words"] = { + variant: v.read(directory / f"WORD-{variant}.json.gz") + for variant in ("base", "extra") + } + records["invoice"] = v.read(directory / "INVOICE.json.gz") + return records, hashes + + +def validate_bindings(records, hashes): + result = records["RESULT.json"] + admission, native = records["ADMISSION-RESULT.json"], records["NATIVE-RECEIPT.json"] + release = records["RELEASE-RECEIPT.json"] + derivation = records["EDIT-DERIVATION.json"] + rw.need( + result["status"] == "PASS_SHARED_RESTORE_COMPLETE_RELEASE", "composed release" + ) + rw.need( + admission["status"] == "PASS_REPLICA_ORDER_FILL_DERIVATIVE_COMPLETE_RELEASE", + "admission", + ) + rw.need( + native["status"] + == "PASS_COMPOSED_FRESH_NATIVE_PROVIDERS_AND_AUTHENTICATED_CACHE", + "native status", + ) + rw.need(native["fresh_current_provider_count"] == 2, "both fresh providers") + rw.need(release["status"] == "PASS_RELEASE", "outer release") + rw.need(result["fresh_retained_bootstrap"] is True, "fresh retained bootstrap") + source = hashes["SOURCE-MANIFEST.json"] + rw.need( + result["source_manifest_sha256"] + == admission["source_manifest_sha256"] + == native["manifest_sha256"] + == derivation["manifest_sha256"] + == source, + "same actual source", + ) + rw.need( + admission["source_profile"] == "rank7-shared-restore-fanin", "new source label" + ) + rw.need( + admission["native_receipt_sha256"] == hashes["NATIVE-RECEIPT.json"], + "native binding", + ) + rw.need( + admission["release_receipt_sha256"] + == result["release_receipt_sha256"] + == hashes["RELEASE-RECEIPT.json"], + "outer binding", + ) + rw.need( + result["admission_sha256"] == hashes["ADMISSION-RESULT.json"], + "admission binding", + ) + rw.need( + admission["package_manifest_sha256"] == release["manifest_sha256"], + "admitted package", + ) + + +def validate_endpoint(records): + result, admission = records["RESULT.json"], records["ADMISSION-RESULT.json"] + release = records["RELEASE-RECEIPT.json"] + rw.need( + {int(k): n for k, n in admission["profile"].items()} == v.EXPECTED, + "full paid profile", + ) + rw.need( + {int(k): n for k, n in result["profile"].items()} == v.EXPECTED, + "same complete bill", + ) + rw.need( + admission["replicas"] == 74 and admission["actual_expected_helpers"] == 408, + "T74 helper census", + ) + finite = v.read(v.PACKAGE / "evidence/FINITE.json") + lower = Fraction(finite["moment"]["root"][0]) + expected = ( + Fraction((lower * 10**24).__floor__(), 10**24) + - Fraction(1, 10**46) + - Fraction(1, 10**70) + ) + rw.need( + Fraction(result["kappa"]) + == Fraction(admission["kappa"]) + == Fraction(release["kappa_decimal"]) + == expected, + "exact strict released endpoint", + ) + return finite, expected + + +def validate(records, hashes): + validate_bindings(records, hashes) + finite, expected = validate_endpoint(records) + validate_invoice(records["invoice"]) + validate_words( + records, + hashes, + finite, + records["NATIVE-RECEIPT.json"], + records["SOURCE-MANIFEST.json"], + ) + stages = records["STAGES.json"] + rw.need( + [s["stage"] for s in stages] == ["source-preflight", *reproduce.NAMES], + "complete fresh stages", + ) + for entry in stages: + rw.need(entry["exit_code"] == 0, "successful actual stage") + name = "logs/" + entry["stage"] + ".log.txt" + rw.need(hashes[name] == entry["log_sha256"], "actual stage log binding") + return str(expected) + + +def validate_words(records, hashes, finite, native, manifest): + for variant in ("base", "extra"): + word = records["words"][variant] + rw.need( + v.canonical(word) + == finite["variants"][variant]["R1R2"]["canonical_sha256"], + "retained word equals the regenerated semantic payload", + ) + name = f"new/borrow/words/BORROW-WORD-43{variant}.json.gz" + rw.need( + native["providers"][variant]["word_sha256"] + == manifest[name] + == hashes[f"WORD-{variant}.json.gz"], + "native word and compiled source binding", + ) + rw.need(len(word["helper_final"]) == 91, "all private buffers") + rw.need(word["report"]["local_profile"] == rw.LOCAL, "actual local bill") + rw.need(word["report"]["width_inventory"] == rw.INVENTORY, "unchanged widths") + + +def validate_invoice(invoice): + rw.need( + invoice["status"] + == "PASS_INDEPENDENT_MIXED_ASYNC_SCALAR_PREFIX_AND_FINITE_INVOICE", + "actual emitted-program invoice", + ) + rw.need( + invoice["physical"] == 66813 + and invoice["live"] == 66304 + and invoice["private_zero_buffers"] == 91, + "all physical families and buffers", + ) + local = {int(r): n for r, n in invoice["selected_local_paid_profile"].items()} + rw.need( + local == {int(r): 666 * n for r, n in rw.LOCAL.items()}, + "actual paid local calls", + ) + rw.need( + invoice["complete_invocation_sweeps"] == invoice["bridge_sweeps"] == 666, + "all invocation and bridge sweeps", + ) + block = invoice["blocknorm"] + rw.need( + block["physical_families"] == 66813 and block["stock_l2_bits"] == 1322, + "actual stock bound", + ) + rw.need( + block["local_actual_prefix_bits"] == 93 + and invoice["global_prefix_bits"] == block["actual_prefix_bits"] == 1475, + "actual local/global prefixes", + ) + rw.need( + block["required_reserve_bits"] + == 1510 + <= invoice["charged_prefix_bits"] + == block["retained_payload_bits"] + == 2048, + "charged prefix allowance", + ) + checks = invoice["strict_checks"] + rw.need( + len(checks) == 9 and all(value is True for value in checks.values()), + "all strict finite invoice checks", + ) + + +def controls(records, hashes): + names = [ + "native-count", + "paid-profile", + "stale-kappa", + "source-manifest", + "native-word", + "missing-stage", + "derivation", + "private-buffer", + "prefix", + "missing-sweep", + ] + for name in names: + mutant = copy.deepcopy(records) + if name == "native-count": + mutant["NATIVE-RECEIPT.json"]["fresh_current_provider_count"] = 1 + elif name == "paid-profile": + mutant["ADMISSION-RESULT.json"]["profile"]["1"] += 1 + elif name == "stale-kappa": + mutant["RESULT.json"]["kappa"] = "0.001729152756004330934535" + elif name == "source-manifest": + mutant["ADMISSION-RESULT.json"]["source_manifest_sha256"] = "0" * 64 + elif name == "native-word": + mutant["NATIVE-RECEIPT.json"]["providers"]["base"]["word_sha256"] = "0" * 64 + elif name == "missing-stage": + mutant["STAGES.json"].pop(3) + elif name == "derivation": + mutant["EDIT-DERIVATION.json"]["manifest_sha256"] = "0" * 64 + elif name == "private-buffer": + mutant["invoice"]["private_zero_buffers"] = 90 + elif name == "prefix": + mutant["invoice"]["charged_prefix_bits"] = 1474 + else: + mutant["invoice"]["bridge_sweeps"] = 665 + try: + validate(mutant, hashes) + except ValueError: + continue + raise ValueError("accepted release mutant: " + name) + return len(names) + + +def main(): + v.authenticate() + records, hashes = load() + kappa = validate(records, hashes) + count = controls(records, hashes) + print("PASS_SHARED_RESTORE_RECORDED_RELEASE", kappa, "controls=" + str(count)) + + +if __name__ == "__main__": + main()