From 467b9da6fe130a12d0d6edda310cd6b0efd22a7e Mon Sep 17 00:00:00 2001 From: Oscar Fennell <124218296+ofennell-quipex@users.noreply.github.com> Date: Tue, 13 Oct 2026 16:09:53 +1100 Subject: [PATCH] Research: certify rooted R420 target forests and save 4784 XORs --- research/r420-target-forest/CERTIFICATE.json | 95 ++++++ research/r420-target-forest/CLAIM.json | 83 +++++ research/r420-target-forest/PROOF.md | 112 +++++++ research/r420-target-forest/README.md | 169 ++++++++++ research/r420-target-forest/RECIPE.json | 259 ++++++++++++++++ research/r420-target-forest/SOURCES.json | 24 ++ research/r420-target-forest/VALIDATION.json | 90 ++++++ research/r420-target-forest/discover.py | 108 +++++++ research/r420-target-forest/independent.py | 73 +++++ research/r420-target-forest/native.py | 77 +++++ research/r420-target-forest/verify.py | 310 +++++++++++++++++++ 11 files changed, 1400 insertions(+) create mode 100644 research/r420-target-forest/CERTIFICATE.json create mode 100644 research/r420-target-forest/CLAIM.json create mode 100644 research/r420-target-forest/PROOF.md create mode 100644 research/r420-target-forest/README.md create mode 100644 research/r420-target-forest/RECIPE.json create mode 100644 research/r420-target-forest/SOURCES.json create mode 100644 research/r420-target-forest/VALIDATION.json create mode 100644 research/r420-target-forest/discover.py create mode 100644 research/r420-target-forest/independent.py create mode 100644 research/r420-target-forest/native.py create mode 100644 research/r420-target-forest/verify.py diff --git a/research/r420-target-forest/CERTIFICATE.json b/research/r420-target-forest/CERTIFICATE.json new file mode 100644 index 0000000000..faad42ec93 --- /dev/null +++ b/research/r420-target-forest/CERTIFICATE.json @@ -0,0 +1,95 @@ +{ + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "labels": { + "labels": 120, + "lattice_rank": 8, + "gram_det": 1, + "frames": 672 + }, + "minimum_forest_certificate": { + "cost": 14921, + "cycle_inequalities": 7260 + }, + "minimum_nominated_tree": { + "D_XORs": 14921, + "ADDs": 21915, + "records": 24873, + "COPYs": 9, + "ERASEs": 9, + "profile": { + "1": 1320, + "2": 1440, + "4": 60, + "5": 120, + "8": 9 + }, + "rank_mass": 5112, + "prefix": { + "forward": 144651, + "reverse": 19231132, + "payload": "71639738627497752220685905038336", + "payload_bits": 106 + }, + "word_sha256": "ee77ccdf2dcf10f4d33f5b26ccdb28523a41d797efbfe7c144cb1aad94d67c10" + }, + "baseline": { + "D_XORs": 19922, + "ADDs": 26916, + "records": 29874, + "COPYs": 9, + "ERASEs": 9, + "profile": { + "1": 1320, + "2": 1440, + "4": 60, + "5": 120, + "8": 9 + }, + "rank_mass": 5112, + "prefix": { + "forward": 144651, + "reverse": 2270064, + "payload": "998206739997057013039187410944", + "payload_bits": 100 + }, + "word_sha256": "e597e3885c0a8daa262afa5985ee2930443329126aece76d33159d81882bdcc2" + }, + "feasible_forest": { + "D_XORs": 15138, + "ADDs": 22132, + "records": 25090, + "COPYs": 9, + "ERASEs": 9, + "profile": { + "1": 1320, + "2": 1440, + "4": 60, + "5": 120, + "8": 9 + }, + "rank_mass": 5112, + "prefix": { + "forward": 144651, + "reverse": 9640706, + "payload": "18003708514079901815901709480704", + "payload_bits": 104 + }, + "word_sha256": "d7fbc12b50b35c39c10a8f416d5ad19b2486b7b87bd064f11bdda0fdd6bbb345" + }, + "roots": 12, + "preparation_XORs": 108, + "columns_per_direction": 660, + "negative_controls": [ + "cyclic parent", + "nonminimum tree", + "missing preparation", + "missing restoration", + "missing correction", + "nonzero D frame", + "helper write", + "minimum-cost nominated tree exceeds payload cap" + ], + "positive_control": "F2-neutral target pair costs two ADDs", + "interface": "Semantic H2-prime; literal H2 and literal K extractor reject. All other H and C predicates pass.", + "scope": "Finite F2 circuit and exact rooted-forest cost optimum; feasible cut is not claimed precision-constrained optimal; no new kappa." +} diff --git a/research/r420-target-forest/CLAIM.json b/research/r420-target-forest/CLAIM.json new file mode 100644 index 0000000000..a830bd27a3 --- /dev/null +++ b/research/r420-target-forest/CLAIM.json @@ -0,0 +1,83 @@ +{ + "track": "Bit supplier", + "assignment_seed": 5, + "random_source": "Python secrets.randbelow(100), operating-system randomness", + "started_utc": "2026-10-13T04:54:08.686716+00:00", + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "claim_utc": "2026-10-13T04:56:56.290190+00:00", + "expected_finish_utc": "2026-10-13T05:44:08Z", + "time_budget_minutes": 50, + "orientation_limit_minutes": 10, + "verification_and_handoff_reserved_minutes": 12.5, + "coordination": "No pinned issues returned by GitHub GraphQL; local claim per sprint instructions.", + "candidates": [ + { + "object": "R420 phase-A cell or quad circuits", + "decision": "Existing PR691 already changes quad synthesis; simple cell gates are too narrow." + }, + { + "object": "R420 phase-B block resynthesis", + "decision": "Existing PR670/674/688 cover circuit shortening and integration." + }, + { + "object": "R420 frame-zero target forest basis", + "decision": "Selected: replace disjoint pairs with arbitrary rooted forests; exact minimum spanning tree certificate and full dirty restoration." + } + ], + "hypothesis": "Rooted target forests lower frame-zero compensation XOR cost beyond the disjoint-pair class without modifying helper contents or recursive frame paths.", + "method": "All 7260 edges on 120 targets plus zero root; seeded tie ordering from seed 5; one MST; independent path-max optimality witness; complete 660-column replay; positive-prefix accounting.", + "deliverable": "Finite bit-circuit construction and exact scoped optimum, reproducible verifier, proof, pins, controls; no new kappa.", + "scope_exclusions": [ + "General linear basis synthesis", + "Helper basis changes", + "Composition with pending work", + "New recursive profile or kappa" + ], + "related_prs": { + "713": "Target-pair basis, independently developed; direct mechanism predecessor.", + "716": "Exact disjoint target-pair optimum; tree class strictly extends this domain.", + "694": "Helper-column basis; different domain and potentially stronger scalar reduction.", + "710": "Cleanup-only rewrite; distinct section.", + "742": "Concurrent shared-donor stars; credited. This contribution adds multiple levels, exact full-forest floor, and 1496 extra saved XORs.", + "733": "Two-sided helper/target basis with larger overall reduction; distinct domain, credited and not superseded.", + "731": "Independent compensation rank/kernel verification; distinct obligation." + }, + "overlap_snapshot": { + "open_pr_count": 545, + "max_pr_number": 726, + "tree_or_forest_matches": [] + }, + "initial_complete_cost": { + "baseline_D_XORs": 19922, + "forest_D_XORs_including_restore": 14921, + "savings": 5001 + }, + "result": { + "updated_utc": "2026-10-13T05:09:53.117846+00:00", + "status": "Completed finite construction and verification; ready for focused PR", + "D_XORs": 15138, + "saved_native_XORs": 4784, + "exact_unconstrained_forest_floor": 14921, + "payload_bits": 104, + "native_stages_verified": [ + 5, + 9, + 11 + ], + "kappa": "unchanged", + "result_link": "https://github.com/ofennell-quipex/integer-mult-bounds/tree/research/r420-target-forest-seed5/research/r420-target-forest" + }, + "final_overlap": { + "checked_utc": "2026-10-13T05:09:53.117836+00:00", + "open_pr_count": 575, + "max_pr_number": 756, + "pinned_issues": [], + "main_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "outcome": "No competing general rooted-forest floor found; PR742 shared-donor overlap explicitly credited." + }, + "experiment_update": { + "reason": "The nominated cheapest tree fails the inherited 104-bit budget.", + "bounded_search": "256 seed-ordered minimum trees, followed by 900 root-cut candidates over 8 rounds.", + "scope": "Same target-forest mechanism; no precision-constrained optimality claim." + } +} diff --git a/research/r420-target-forest/PROOF.md b/research/r420-target-forest/PROOF.md new file mode 100644 index 0000000000..43221b58b3 --- /dev/null +++ b/research/r420-target-forest/PROOF.md @@ -0,0 +1,112 @@ +# Proof and exact scope + +Work over F2. Write the 120 target registers as y and the 420 arbitrary helper +registers as s. The pinned D matrix K has 120 rows and 420 columns. Its original +implementation adds each nonzero coefficient separately, for |K| = 19,922 XORs. +All sources, targets and helpers are independent symbolic inputs; source rows +are not read by this replacement. + +## Rooted-forest identity, including restoration + +Fix a forest on the target vertices, orienting every component away from one +root. For a nonroot t with parent p(t), prepare `y_t <- y_t + y_p(t)` in decreasing +depth order. Since a parent has not yet been changed when its child executes, +the prepared target vector is Py, where row t of P is e_t+e_p(t) for nonroots +and e_t for roots. The product of these elementary transvections is invertible. +The reversed preparation stream is its inverse over F2. + +At target t add `(K_t+K_p(t))s` for a nonroot, and `K_t s` for a root. This adds +PKs in the prepared basis. Apply the reversed preparation stream: + +`P^-1 (Py + PKs) = y + Ks`. + +Sources and helpers have not changed at any time in D. This identity holds for +arbitrary original y and s. In particular, preparation cannot be omitted merely +because the zero-target case seems correct. All gates act on existing frame-zero +target/helper registers. No descent, new frame, extra helper, source read, copy, +or recursive child is introduced. Both the preparation and its inverse are +included in the invoice. + +Replacing D by this operator leaves the input to A identical to the original +word, on every input column. Thus the unchanged A/scatter/B/C program retains its +full dirty-restored endpoint. Its original literal H2 syntax and literal K +extractor are insufficient to recognize this implementation; the sufficient +semantic contract is the full D endpoint just proved. The rest of the scalar +interface is inherited without alteration. Same-frame target XOR operations +use the original common-label conditional realization. + +## Exact optimal scalar cost within this class + +A forest F implemented by the preceding recipe costs + +`C(F) = sum_roots |K_t| + sum_nonroots (|K_t XOR K_p(t)| + 2)`. + +The two units per forest edge are its preparation and restoration. This defines +the scoped class: one parent-difference helper row per target and no additional +factoring among those rows. More general target bases, helper bases, shared +helper expressions, cycles or arbitrary reversible circuits are outside it. + +Add a vertex z with K_z = 0. Give each edge z--t weight |K_t| and each target +edge u--v weight |K_u XOR K_v|+2. Joining every component root to z maps a rooted +forest to a spanning tree of the 121-vertex graph, at identical cost. Conversely, +removing z from any spanning tree and orienting away from its neighbors gives a +rooted forest with the same invoice. Therefore the exact class minimum is the +minimum-spanning-tree weight. + +`RECIPE.json:minimum_parents` specifies an attaining tree. The verifier checks +its connectivity and acyclicity and all 7,260 pair inequalities + +`w(u,v) >= max { w(e) : e lies on the tree path u to v }`. + +These inequalities are sufficient for minimality. To transform an arbitrary +spanning tree S into the proposed tree T, add an edge e of T absent from S and +consider its fundamental cut in T. The cycle in S+e contains an edge f of S not +in T crossing that cut. The T-path of f contains e, so the verified inequality +gives w(f) >= w(e). Replacing f by e does not increase cost and increases the +number of shared edges. Repeating reaches T. Thus no S costs less than T. +The verified sum is **14,921**, yielding the exact unconstrained saving ceiling +**19,922 - 14,921 = 5,001** within this recipe class. The separate Prim +implementation confirms the same integer minimum without using this certificate +checker or the nomination algorithm. + +## Precision-limited submitted construction + +The certificate above concerns scalar counts; it contains no precision premise. +The best reverse-bound tree among 256 nominated minimum-cost trees needs 106 +payload bits under the inherited bound. This is a failed budget check on those +nominations, **not a proof that every optimum tree fails**. + +Deleting eight target edges, making their children roots, gives the submitted +forest. Its 12 roots and 108 edges cost 14,922 helper XORs plus 216 target XORs, +or **15,138** total. No precision-constrained optimality is asserted. The +complete scalar stream costs **22,132**, a reduction of **4,784** from 26,916. + +The actual exported stream is used to recompute both positive prefix envelopes: +initialize every local row bound to one; ADD replaces L_d by L_d+|c|L_s; +COPY opens a temporary with its source bound; ERASE closes it. Reverse traversal +interchanges COPY and ERASE. This is an entrywise triangle-inequality bound for +the signed lift, independently of F2 cancellations. The largest forward and +reverse bounds are respectively **144,651** and **9,640,706**. The inherited +local invoice is therefore + +`64 * 144651^3 * 9640706^2 = 18003708514079901815901709480704 < 2^104`. + +The unchanged C++ checker independently verifies this bound. The nominated +minimum-cost tree fails that same native budget check. Missing target restoration +fails the native full-column check at five, nine and eleven stages. + +No gate outside D changes. All D gates remain at frame zero. Consequently every +frame transition, COPY and ERASE is identical to the source. Exact comparison of +the entire exported non-ADD subsequence checks this directly, including source +and helper endpoints. The paid histogram remains +`{1:1320, 2:1440, 4:60, 5:120, 8:9}`, with rank mass **5,112**. + +This proves a finite F2 circuit identity, a forest-class scalar floor, and the +stated local invoices. It does not prove a new κ, a precision-constrained +optimum, equality of the signed integer endpoint, or the uniform/physical/tape/ +analytic hypotheses of integer multiplication. Global hosting and invoice +integration remain separate obligations; an increased local prefix must not +silently inherit an old global receipt. + +Oscar Fennell, with substantial OpenAI Codex assistance; Apache-2.0. Predecessor +credit and exact source pins are in README.md and SOURCES.json. diff --git a/research/r420-target-forest/README.md b/research/r420-target-forest/README.md new file mode 100644 index 0000000000..e3a786e72b --- /dev/null +++ b/research/r420-target-forest/README.md @@ -0,0 +1,169 @@ +# R420 target forests: 4,784 fewer XORs with a certified forest cost floor + +**Finite bit-circuit construction and scoped optimum; no new κ.** This changes +only the frame-zero dirt compensation D of eumemic's PR543 R420 supplier. +Twelve rooted target trees reduce the complete native word from **26,916 to +22,132 binary XOR additions**, including all preparation and restoration. +The D section falls from **19,922 to 15,138** additions. Every arbitrary target +input is restored before leaving D, apart from the required dirt correction; +helpers are never modified in D. + +The exact minimum D cost over the explicitly defined *rooted target forest* +class is **14,921**. A spanning-tree cycle certificate proves this floor, and +an independent Prim implementation reproduces it. The nominated minimum-cost +tree needs 106 payload bits, exceeding the inherited 104-bit allowance. Eight +cuts produce the submitted 15,138-addition forest, whose recomputed payload +fits below 2^104. **We do not claim that every minimum-cost tree exceeds the +allowance, or that the submitted forest is optimal subject to that allowance.** + +| Quantity | Pinned PR543 | Submitted forest | +|---|---:|---:| +| D binary XORs, including preparation/restoration | 19,922 | 15,138 | +| Complete native ADDs | 26,916 | 22,132 | +| Exported records | 29,874 | 25,090 | +| Helpers / retained COPYs | 420 / 9 | 420 / 9 | +| Paid rank mass | 5,112 | 5,112 | +| Forward positive prefix bound | 144,651 | 144,651 | +| Reverse positive prefix bound | 2,270,064 | 9,640,706 | +| Payload allowance needed | 100 bits | 104 bits | + +All per-register frame paths and the complete MOVE/COPY/ERASE subsequence are +unchanged. The local recursive histogram remains +`{1:1320, 2:1440, 4:60, 5:120, 8:9}`. This is a scalar circuit improvement, +not a changed recursive exponent or a practical multiplication benchmark. + +## Reproduce + +Python 3.10+ and the standard library, from the repository root: + +```sh +python3 -I -B research/r420-target-forest/verify.py +python3 -I -B research/r420-target-forest/independent.py +``` + +Expected final lines: + +```text +PASS_R420_TARGET_FOREST D=19922->15138 ADDs=26916->22132 saved=4784 forest_floor=14921 payload_bits=104 columns=660 controls=8 no_new_kappa +PASS_INDEPENDENT_FOREST minimum=14921 feasible=15138 preparation=108 restoration=108 dirty_columns=660 +``` + +The first command verifies the source pins, all 672 E8 frames, full forward and +reverse arbitrary-input endpoints, all 7,260 spanning-tree cycle inequalities, +complete certificate equality, native exporter agreement, positive prefix +bounds and eight negative controls. It invokes the original unmodified PR543 +checker for labels, frames and interface predicates. A separate set-valued +interpreter replays both directions of the actual exported record streams. +`independent.py` imports no package code: it uses Prim and set-valued target +algebra instead of Kruskal, cycle inequalities and integer-bitset algebra. +These are independently implemented algorithms by the same AI-assisted author, +not an independent human review. + +For the unchanged C++17/Boost legality and 5/9/11-stage checks: + +```sh +BOOST_INCLUDE=/path/containing/boost python3 -I -B research/r420-target-forest/verify.py --native +``` + +Omit `BOOST_INCLUDE` if the headers are in `/usr/include`. The optional run +checks both source and changed words on 900/1,380/1,620 columns, rejects all +96 omitted-bridge controls, rejects the nominated cheapest tree for its +106-bit payload and rejects missing restoration at every stage count. +It writes only to a temporary directory. The native receipt is printed. + +The bounded nomination is reproducible separately: + +```sh +python3 -I -B research/r420-target-forest/discover.py +``` + +This checks all 7,260 graph edges in each of 256 seed-ordered Kruskal runs +(seeds 5 through 260), chooses attempt 1 by the smallest reverse positive +bound, then considers 900 single-edge root cuts over eight greedy rounds. +Cuts are selected by exact rational prefix reduction per added XOR and stop +as soon as the 104-bit cap holds. The committed cuts are +`68,50,0,39,78,97,57,3`. No exhaustive coverage of spanning trees, admissible +linear bases, or precision-constrained forests is claimed. The *cost floor* +is proved by the certificate, not by failure to find a cheaper candidate. +`--write-certificate` deliberately regenerates the receipt; normal verification +never updates committed files. + +## Mechanism and interface + +For parent map p, descendants first execute `y_t ^= y_p(t)`. Roots are unchanged. +Each target then reads helper row `K_t XOR K_p(t)` (roots read `K_t`). The target +operations are reversed to restore the original basis. There are 108 preparation +and 108 restoration XORs and 14,922 helper reads, totaling 15,138. The written +argument and graph certificate are in [PROOF.md](PROOF.md). + +The original syntactic H2 requires D to read only helpers. Its literal K +extractor also assumes that syntax. **Both reject the changed representation**, +as the verifier explicitly checks; no predecessor checker is patched. The +replacement H2′ requires frame-zero D to have the complete semantic endpoint +`(x,s,y) -> (x,s,y+Ks)`. All other original H1–H5 hypotheses and decomposition +checks pass. Target-to-target operations in D use existing frame-zero rows, +with no new helper, COPY, source-access or recursive-child cost. + +Full hosted-parent reconstruction, whole-owner and residual-host integration, +updated global finite invoices, adoption of the semantic H2′ interface, and a +changed-word outer assembly remain integration obligations. The increased local +positive prefix must not be substituted into an old global invoice without +replay. The selected construction remains #626/#543 at conditional +`κ = 51110230636731/31250000000000000`. + +All-size compilation, common-label/mutable-basis realization, hosting, precision, +tape and analytic transfer remain inherited assumptions. F2 endpoint equality +and positive integer envelopes do not assert equality of the signed integer +endpoint, a full multiplication theorem, or a Lean proof. The unchanged selected +cold replay and repository-wide regeneration suite were not rerun for this +standalone package. Local Linux checks and remote CI are distinct; see +[VALIDATION.json](VALIDATION.json). + +## Provenance, overlap and credit + +Exact base: `66849e1475c930fd7732b1a0067ffee7e1e95f60`. +PR543 source: `2065fe4f72a914d907f1046603f5a36f17018535`. +[SOURCES.json](SOURCES.json) pins every consumed repository implementation. +The compressed word is compared using its complete canonical JSON payload, so +recompression does not change mathematical identity. No pending PR code is +imported. [CLAIM.json](CLAIM.json) records the OS-random seed **5**, candidate +selection, local claim and final overlap refresh; no pinned coordination issue +existed when the scope was selected. + +Scott Woolsey Biggart's [PR713](https://github.com/CrocSwap/integer-mult-bounds/pull/713) +and Sagar Thakrar's [PR716](https://github.com/CrocSwap/integer-mult-bounds/pull/716) +are direct predecessors for restored target-row factoring. PR716 proves the +3,250-saving disjoint-pair optimum. This contribution extends the circuit class +to arbitrary rooted forests, proves its scalar cost floor and supplies a +104-bit-feasible forest saving an additional 1,534 XORs. **No priority for +pair factoring is claimed.** + +Concurrent [PR742](https://github.com/CrocSwap/integer-mult-bounds/pull/742), +prepared for @ellipsi2, appeared during the final refresh and independently +extends pairs to shared-donor stars, saving 3,288 XORs. It receives explicit +credit for the shared-donor extension. The present construction permits +multiple tree levels, adds an exact floor for the whole rooted-forest class, +and saves another 1,496 XORs while satisfying the 104-bit bound. No priority +for shared donors is claimed, and no PR742 code is used. + +Greer Guthrie's [PR694](https://github.com/CrocSwap/integer-mult-bounds/pull/694) +and PR686 factor helper columns. PR694 has a larger reported scalar reduction; +this target-only class never modifies helpers during D and is not presented as +the best arbitrary D circuit. PR708 modifies separate decoder totals; PR710 +modifies cleanup. Concurrent PR733 composes helper and target bases and reports 8,368 saved XORs; +that broader class is credited and is not superseded. PR731 independently +checks the original compensation matrix rank and kernel. Neither is imported. +None is composed here. Dugongue's PR476 and earlier PR450 +supply target-mixing precedents. + +Credit remains with eumemic for PR543/493 and the interleaved scalar interface; +Dylan Crow for the E8 word/record format and exporter; DreamingOfClouds for the +retained-totals/nine-stage lineage; Zhihao Chen for the scalar-interface +framework; DaysSky for bridged stages/hosting; and the complete cumulative +construction and realization lineage in the [original notice](../e8-bit-r420/NOTICE.md) +and [maintainer review](../../docs/research/community-k492-review.md). + +Contributed by **Oscar Fennell (@ofennell-quipex)** with substantial +**OpenAI Codex assistance** in the mathematical analysis, bounded search, +implementation, verification and writing. New material is Apache-2.0, under the +repository license. Existing source files and notices are unchanged. diff --git a/research/r420-target-forest/RECIPE.json b/research/r420-target-forest/RECIPE.json new file mode 100644 index 0000000000..5c49bf11d7 --- /dev/null +++ b/research/r420-target-forest/RECIPE.json @@ -0,0 +1,259 @@ +{ + "assignment_seed": 5, + "minimum_parents": [ + 5, + 7, + 4, + 5, + 21, + 102, + 3, + 50, + 14, + 15, + 12, + 13, + 52, + 45, + 24, + 10, + 18, + 21, + 0, + 76, + 18, + 19, + 16, + 17, + 72, + 51, + 31, + 30, + 25, + 24, + 70, + 10, + 34, + 120, + 85, + 66, + 80, + 120, + 32, + 47, + 61, + 79, + 93, + 33, + 41, + 41, + 43, + 91, + 37, + 68, + 49, + 64, + 120, + 60, + 53, + 35, + 63, + 48, + 50, + 79, + 75, + 78, + 56, + 57, + 66, + 39, + 33, + 49, + 48, + 67, + 68, + 65, + 75, + 92, + 73, + 63, + 61, + 57, + 58, + 77, + 51, + 80, + 6, + 12, + 120, + 49, + 9, + 82, + 94, + 91, + 83, + 75, + 90, + 59, + 78, + 59, + 16, + 50, + 61, + 102, + 97, + 96, + 100, + 98, + 110, + 63, + 48, + 93, + 106, + 107, + 12, + 105, + 19, + 0, + 3, + 79, + 114, + 115, + 112, + 113 + ], + "minimum_search_attempt": 1, + "feasible_parents": [ + 120, + 7, + 4, + 120, + 21, + 102, + 3, + 50, + 14, + 15, + 12, + 13, + 52, + 45, + 24, + 10, + 18, + 21, + 0, + 76, + 18, + 19, + 16, + 17, + 72, + 51, + 31, + 30, + 25, + 24, + 70, + 10, + 34, + 120, + 85, + 66, + 80, + 120, + 32, + 120, + 61, + 79, + 93, + 33, + 41, + 41, + 43, + 91, + 37, + 68, + 120, + 64, + 120, + 60, + 53, + 35, + 63, + 120, + 50, + 79, + 75, + 78, + 56, + 57, + 66, + 39, + 33, + 49, + 120, + 67, + 68, + 65, + 75, + 92, + 73, + 63, + 61, + 57, + 120, + 77, + 51, + 80, + 6, + 12, + 120, + 49, + 9, + 82, + 94, + 91, + 83, + 75, + 90, + 59, + 78, + 59, + 16, + 120, + 61, + 102, + 97, + 96, + 100, + 98, + 110, + 63, + 48, + 93, + 106, + 107, + 12, + 105, + 19, + 0, + 3, + 79, + 114, + 115, + 112, + 113 + ], + "cut_vertices": [ + 68, + 50, + 0, + 39, + 78, + 97, + 57, + 3 + ], + "search_attempts": 256 +} diff --git a/research/r420-target-forest/SOURCES.json b/research/r420-target-forest/SOURCES.json new file mode 100644 index 0000000000..58b79cf761 --- /dev/null +++ b/research/r420-target-forest/SOURCES.json @@ -0,0 +1,24 @@ +{ + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "PR543": "2065fe4f72a914d907f1046603f5a36f17018535", + "context_only_PR713": "1a19af5c5ddb6de9797a6d085e5df0b90ed6d58b", + "context_only_PR716": "afeb452f58ff0cbf109172335e2ba282aac3dcde", + "gzip_policy": "Canonical complete JSON payload; container recompression is allowed. All other files are exact SHA-256.", + "files": { + "research/e8-bit-r420/data/bitE8mut-r420.json.gz": "e597e3885c0a8daa262afa5985ee2930443329126aece76d33159d81882bdcc2", + "research/e8-bit-r420/code/xcheck.py": "5737d18a7826fd51e131035f2d7bebba2e2868af91dd7672a5f11208b036d424", + "research/e8-bit-carrier-skeleton/code/bit/export_records.py": "8a5999601f917dbb492bb9ae9a344611f18cc7cedc53dc3c76496a369e530eb3", + "research/e8-bit-carrier-skeleton/code/bit/checkers/columns_k.cpp": "1c344d18fcd494eeca93e259f10cafae7705780e6592f6dcb35b34752dab9bc2", + "research/e8-bit-carrier-skeleton/code/bit/checkers/legality_h.cpp": "6c1ef2b24e57781d6951c172a1024fc4300e6fd392c9d6672079a7806ab663b3", + "research/e8-bit-carrier-skeleton/code/bit/checkers/json.hpp": "aaf127c04cb31c406e5b04a63f1ae89369fccde6d8fa7cdda1ed4f32dfc5de63", + "research/e8-bit-carrier-skeleton/code/bit/regression/stage_cohort.py": "6c288f6f234b528c1a7c0a4adfb724e91e0fe6b18c8dffad96af3f973de1829a", + "research/e8-bit-carrier-skeleton/portable-include/bits/stdc++.h": "420094be2af295eed03a983dd66debbbe9cfb78d8252859f4498a615a0074b99" + }, + "PR543_git_blobs": { + "research/e8-bit-r420/data/bitE8mut-r420.json.gz": "0c63ca62759dc63d302be6552aeeee1ede70350f", + "research/e8-bit-r420/code/xcheck.py": "fbff8607e4c61e18481f696b99dd38a32444e90d" + }, + "context_only_PR742": "6e7a5d271a123886dc7b54ca3180d0b9f9beda5a", + "context_only_PR733": "dfe84e09298abc5c5e0074afda59a821e10abfb4", + "context_only_PR731": "cf5ff54a358b400a7e69abe941d1d0ad0944b25e" +} diff --git a/research/r420-target-forest/VALIDATION.json b/research/r420-target-forest/VALIDATION.json new file mode 100644 index 0000000000..b5d9991e4d --- /dev/null +++ b/research/r420-target-forest/VALIDATION.json @@ -0,0 +1,90 @@ +{ + "status": "Passed local finite checks; no remote CI result claimed", + "checked_utc": "2026-10-13T05:06:52.019456+00:00", + "platform": "Linux-7.2.5-3-omarchy-x86_64-with-glibc2.44", + "python": "3.14.7", + "compiler": "g++ (GCC) 16.2.1 20260810", + "boost": { + "version": "1.92.0-1", + "url": "https://stable-mirror.omarchy.org/extra/os/x86_64/boost-1.92.0-1-x86_64.pkg.tar.zst", + "archive_sha256": "0d795c6401c8bfa16012ada7e2e7f34934fb268f9174470edac1b389056f79bb", + "installation": "Extracted headers in task scratch; no system installation" + }, + "native": { + "baseline": { + "ADDs": 26916, + "checks": [ + { + "bridge_controls": 6, + "columns": 900, + "payload_bits": 100, + "stages": 5 + }, + { + "bridge_controls": 18, + "columns": 1380, + "payload_bits": 100, + "stages": 9 + }, + { + "bridge_controls": 24, + "columns": 1620, + "payload_bits": 100, + "stages": 11 + } + ], + "rank_mass": 5112, + "records": 29874 + }, + "forest": { + "ADDs": 22132, + "checks": [ + { + "bridge_controls": 6, + "columns": 900, + "payload_bits": 104, + "stages": 5 + }, + { + "bridge_controls": 18, + "columns": 1380, + "payload_bits": 104, + "stages": 9 + }, + { + "bridge_controls": 24, + "columns": 1620, + "payload_bits": 104, + "stages": 11 + } + ], + "rank_mass": 5112, + "records": 25090 + } + }, + "native_negative_controls": { + "omitted_bridges": 96, + "missing_restoration": 3, + "over_budget_minimum_tree": 1 + }, + "commands_passed": [ + "python3 -I -B research/r420-target-forest/verify.py --native", + "python3 -I -B research/r420-target-forest/independent.py", + "python3 -I -B research/r420-target-forest/discover.py", + "make selected-record-check", + "python3 -I -O -B research/r420-target-forest/verify.py", + "Relocated minimal source package replay under -I -O", + "Canonical gzip recompression acceptance", + "Changed source / underpriced certificate / corrupted forest rejection" + ], + "not_run": [ + "Full hosted-parent reconstruction and invoice", + "Changed-word outer assembly", + "Unchanged selected cold replay", + "Repository-wide make verify", + "Lean", + "Remote CI" + ], + "scope": "Exact finite evidence, not a complete multiplication theorem", + "source_git_blobs_match_PR543": true +} diff --git a/research/r420-target-forest/discover.py b/research/r420-target-forest/discover.py new file mode 100644 index 0000000000..0ddb34cc82 --- /dev/null +++ b/research/r420-target-forest/discover.py @@ -0,0 +1,108 @@ +#!/usr/bin/env python3 +"""Reproduce the bounded seed-5 nomination and eight precision-driven cuts. +This search chooses a witness. verify.py certifies optimality independently. +Oscar Fennell, with substantial OpenAI Codex assistance; Apache-2.0. +""" +import importlib.util +import json +from pathlib import Path +import random +from fractions import Fraction + +HERE = Path(__file__).resolve().parent +spec = importlib.util.spec_from_file_location('forest_verify', HERE/'verify.py') +v = importlib.util.module_from_spec(spec) +spec.loader.exec_module(v) +w = v.load_source() +K = v.rows(w) +# Reverse positive envelopes before D; no frame calculations or F2 cancellation. +stream = [] +for section in ('A', 'scatter', 'B', 'C'): + if section == 'scatter': + for k, q in enumerate(w['ret']): + stream.append(('copy', 660, q)) + for t, row in enumerate(w['scatter']): + if k in row: + stream.append(('add', 120+t, 660)) + stream.append(('erase', 660, q)) + else: + for frame, d, sources in w[section]: + stream.extend(('add', d, s) for s in sources) +base = [1]*661 +for op, d, s in reversed(stream): + if op == 'add': + base[d] += base[s] + else: + base[d] = base[s] if op == 'erase' else 0 + + +def measure(parents): + order = v.traversal(parents) + norms = base[:] + for t in reversed(order): + if parents[t] != 120: + norms[120+t] += norms[120+parents[t]] + for t, p in enumerate(parents): + row = K[t] ^ (K[p] if p != 120 else 0) + norms[120+t] += sum(base[s] for s in range(240, 660) if row >> s & 1) + for t in order: + if parents[t] != 120: + norms[120+t] += norms[120+parents[t]] + reverse = max(norms) + return v.forest_cost(K, parents), reverse, (64*144651**3*reverse**2).bit_length() + + +best = None +for attempt in range(256): + rng = random.Random(5+attempt) + edges = [(row.bit_count(), rng.random(), 120, t) for t, row in enumerate(K)] + edges += [((K[i]^K[j]).bit_count()+2, rng.random(), i, j) for i in range(120) for j in range(i)] + components = list(range(121)) + adjacency = [[] for _ in range(121)] + def component(x): + while components[x] != x: + x = components[x] + return x + for cost, tie, a, b in sorted(edges): + ca, cb = component(a), component(b) + if ca != cb: + components[ca] = cb + adjacency[a].append(b) + adjacency[b].append(a) + parents = {120: None} + queue = [120] + for a in queue: + for b in adjacency[a]: + if b not in parents: + parents[b] = a + queue.append(b) + parents = [parents[t] for t in range(120)] + cost, reverse, bits = measure(parents) + v.need(cost == 14921, 'nominated tree must attain certified floor') + key = bits, reverse, attempt + if best is None or key < best[0]: + best = key, parents +minimum = best[1] +feasible = minimum[:] +cuts = [] +while measure(feasible)[2] > 104: + cost0, reverse0, _ = measure(feasible) + candidates = [] + for t, p in enumerate(feasible): + if p == 120: + continue + proposal = feasible[:] + proposal[t] = 120 + cost, reverse, bits = measure(proposal) + if reverse < reverse0: + v.need(cost > cost0, 'this cut domain has positive extra cost') + candidates.append((Fraction(reverse0-reverse, cost-cost0), -cost, -reverse, t)) + v.need(candidates, 'no improving precision cut') + t = max(candidates)[-1] + cuts.append(t) + feasible[t] = 120 +recipe = {'assignment_seed':5, 'minimum_parents':minimum, + 'minimum_search_attempt':best[0][2], 'feasible_parents':feasible, + 'cut_vertices':cuts, 'search_attempts':256} +v.need(recipe == json.loads((HERE/'RECIPE.json').read_text()), 'nomination reproduction mismatch') +print('PASS_FOREST_DISCOVERY trees=256 chosen_attempt='+str(best[0][2])+' cuts='+str(cuts)+' cost='+str(measure(feasible)[0])) diff --git a/research/r420-target-forest/independent.py b/research/r420-target-forest/independent.py new file mode 100644 index 0000000000..6d6a3483da --- /dev/null +++ b/research/r420-target-forest/independent.py @@ -0,0 +1,73 @@ +#!/usr/bin/env python3 +"""Independent Prim optimum and direct set-valued D verification; no local imports. +Oscar Fennell, with substantial OpenAI Codex assistance; Apache-2.0. +""" +import gzip +import hashlib +import heapq +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +word = json.loads(gzip.decompress((ROOT/'research/e8-bit-r420/data/bitE8mut-r420.json.gz').read_bytes())) +pins = json.loads((HERE/'SOURCES.json').read_text()) +raw = json.dumps(word, sort_keys=True, separators=(',', ':')).encode() +if hashlib.sha256(raw).hexdigest() != pins['files']['research/e8-bit-r420/data/bitE8mut-r420.json.gz']: + raise ValueError('source mismatch') +coefficients = [set() for _ in range(120)] +for frame, dst, source in word['D']: + coefficients[dst-120].symmetric_difference_update(source) +coefficients.append(set()) +# Prim, rather than nomination's Kruskal or the verifier's cycle inequalities. +reached = {120} +queue = [(len(coefficients[t]), t) for t in range(120)] +heapq.heapify(queue) +minimum = 0 +while len(reached) < 121: + cost, vertex = heapq.heappop(queue) + if vertex in reached: + continue + minimum += cost + reached.add(vertex) + for other in range(120): + if other not in reached: + heapq.heappush(queue, (len(coefficients[vertex] ^ coefficients[other])+2, other)) +if minimum != 14921: + raise ValueError('independent forest optimum') +recipe = json.loads((HERE/'RECIPE.json').read_text()) +parents = recipe['feasible_parents'] +depths = [] +for vertex in range(120): + path = set() + current = vertex + while current != 120: + if current in path or not 0 <= current < 120: + raise ValueError('not a rooted forest') + path.add(current) + current = parents[current] + depths.append(len(path)) +# Decreasing depth implements y_v ^= y_parent before the parent is changed. +prepare = sorted((v for v in range(120) if parents[v] != 120), key=lambda v: (-depths[v], v)) +state = [{r} for r in range(660)] +for vertex in prepare: + state[120+vertex] ^= state[120+parents[vertex]] +correction_cost = 0 +for vertex in range(120): + patch = coefficients[vertex] ^ coefficients[parents[vertex]] + correction_cost += len(patch) + state[120+vertex] ^= patch +for vertex in reversed(prepare): + state[120+vertex] ^= state[120+parents[vertex]] +expected = [{r} for r in range(660)] +for vertex in range(120): + expected[120+vertex] |= coefficients[vertex] +if state != expected: + raise ValueError('independent arbitrary-dirty D operator') +cost = correction_cost + 2*len(prepare) +if cost != 15138 or len(prepare) != 108: + raise ValueError('independent circuit invoice') +cert = json.loads((HERE/'CERTIFICATE.json').read_text()) +if cert['minimum_forest_certificate']['cost'] != minimum or cert['feasible_forest']['D_XORs'] != cost: + raise ValueError('certificate differs from independent calculation') +print('PASS_INDEPENDENT_FOREST minimum=14921 feasible=15138 preparation=108 restoration=108 dirty_columns=660') diff --git a/research/r420-target-forest/native.py b/research/r420-target-forest/native.py new file mode 100644 index 0000000000..a46d753f07 --- /dev/null +++ b/research/r420-target-forest/native.py @@ -0,0 +1,77 @@ +"""Unchanged predecessor C++ legality and finite bridged-column checks. +Oscar Fennell, with substantial OpenAI Codex assistance; Apache-2.0. +""" +import json +import os +from pathlib import Path +import struct +import subprocess +import sys + + +def run(root, work, minimum_records): + package = root / 'research/e8-bit-carrier-skeleton' + code = package / 'code/bit' + checkers = code / 'checkers' + boost = Path(os.environ.get('BOOST_INCLUDE', '/usr/include')) + if not (boost / 'boost/multiprecision/cpp_int.hpp').is_file(): + raise RuntimeError('Set BOOST_INCLUDE to the directory containing boost/multiprecision/cpp_int.hpp') + common = [os.environ.get('CXX', 'c++'), '-O2', '-std=c++17', '-DHDIM=8', '-DNCOPY=9', + '-DVPORTS=120', '-DRHELP=420', '-I'+str(package/'portable-include'), + '-I'+str(checkers), '-I'+str(boost)] + def command(args): + proc = subprocess.run([str(a) for a in args], capture_output=True, text=True) + if proc.returncode: + raise RuntimeError('Command failed: '+str(args)+'\n'+proc.stderr[-4000:]) + return proc + legality = work / 'legality' + command(common + ['-o', legality, checkers/'legality_h.cpp']) + bins = {} + for pairs in (2, 4, 5): + exe = work / ('columns'+str(pairs)) + command(common + ['-DKPAIRS='+str(pairs), '-o', exe, checkers/'columns_k.cpp']) + bins[pairs] = exe + receipts = {} + for name in ('baseline', 'forest'): + directory = work / name + cin, cout = directory/'cin', directory/'cout' + command([sys.executable, '-I', '-B', code/'regression/stage_cohort.py', directory, directory, cin, cout]) + command([legality, cin, cout, cout/'legality.json']) + legal = json.loads((cout/'legality.json').read_text()) + if legal['common_frame_ADDs'] != (26916 if name == 'baseline' else 22132): + raise RuntimeError('native ADD count') + stages = [] + for pairs, exe in bins.items(): + out = cout / ('columns'+str(pairs)+'.json') + command([exe, cout/'COHORT249-RECORDS.bin', out]) + report = json.loads(out.read_text()) + if not all(c['rejected'] for c in report['negative_controls']): + raise RuntimeError('bridge control accepted') + if report['formal_columns_checked'] != 2*pairs*120+420 or report['payload_prefix_bits'] > 104: + raise RuntimeError('native column count or budget') + expected = (144651, 2270064) if name == 'baseline' else (144651, 9640706) + actual = tuple(int(p['cancellation_free_signed_row_l1_upper']) for p in report['signed_lift_prefix']) + if actual != expected: + raise RuntimeError('native prefix disagreement') + stages.append({'stages':2*pairs+1,'columns':report['formal_columns_checked'], + 'bridge_controls':len(report['negative_controls']), + 'payload_bits':report['payload_prefix_bits']}) + receipts[name] = {'ADDs':legal['common_frame_ADDs'], 'records':legal['records'], 'rank_mass':legal['rank_mass'], 'checks':stages} + # Keep the mathematically cheapest nominated tree as a genuine native budget rejection. + minimum = work/'minimum.bin' + minimum.write_bytes(b''.join(struct.pack('<6i', *r) for r in minimum_records)) + result = subprocess.run([str(bins[4]), str(minimum), str(work/'rejected.json')], capture_output=True, text=True) + if result.returncode == 0 or 'payloadfiniteprefix2^104' not in result.stderr: + raise RuntimeError('native minimum-tree budget control did not fail as intended') + # A missing target restoration has legal geometry; it must fail scalar formal columns. + raw = list(struct.iter_unpack('<6i', (work/'forest/249-records.bin').read_bytes())) + index = max(i for i,r in enumerate(raw) if r[0] == 1 and r[5] == 1) + del raw[index] + corrupted = work/'missing-restore.bin' + corrupted.write_bytes(b''.join(struct.pack('<6i', *r) for r in raw)) + for pairs, exe in bins.items(): + result = subprocess.run([str(exe), str(corrupted), str(work/'bad.json')], capture_output=True, text=True) + if result.returncode == 0 or 'local defining-decoder full formal column' not in result.stderr: + raise RuntimeError('native restoration control did not fail as intended') + print('NATIVE_RECEIPT '+json.dumps(receipts, sort_keys=True)) + print('PASS_NATIVE_FOREST baseline_and_forest stages=5,9,11 bridge_controls=96 budget_control=1 restoration_controls=3') diff --git a/research/r420-target-forest/verify.py b/research/r420-target-forest/verify.py new file mode 100644 index 0000000000..3c0a0f6ca8 --- /dev/null +++ b/research/r420-target-forest/verify.py @@ -0,0 +1,310 @@ +#!/usr/bin/env python3 +"""R420 target forests: exact scalar costs, dirty endpoints and forest bound. +Oscar Fennell, with substantial OpenAI Codex assistance; Apache-2.0. +""" +import argparse +import copy +import gzip +import hashlib +import importlib.util +import json +from pathlib import Path +import struct +import subprocess +import sys +import tempfile +from collections import Counter + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +SOURCE = ROOT / 'research/e8-bit-r420/data/bitE8mut-r420.json.gz' +PHASES = ('D', 'A', 'scatter', 'B', 'C') + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def canonical(obj): + return json.dumps(obj, sort_keys=True, separators=(',', ':')).encode() + + +def digest(obj): + return hashlib.sha256(canonical(obj)).hexdigest() + + +def load_source(): + pins = json.loads((HERE / 'SOURCES.json').read_text()) + for path, expected in pins['files'].items(): + raw = (ROOT / path).read_bytes() + if path.endswith('.gz'): + raw = canonical(json.loads(gzip.decompress(raw))) + need(hashlib.sha256(raw).hexdigest() == expected, 'source pin: ' + path) + return json.loads(gzip.decompress(SOURCE.read_bytes())) + + +def rows(word): + out = [0] * 120 + for frame, dst, sources in word['D']: + need(frame == 0 and 120 <= dst < 240, 'baseline D shape') + for source in sources: + need(240 <= source < 660, 'baseline helper source') + out[dst-120] ^= 1 << source + return out + + +def traversal(parents): + need(len(parents) == 120 and all(type(p) is int and 0 <= p <= 120 for p in parents), 'parent range') + order, reached = [], {120} + while len(order) < 120: + layer = [v for v in range(120) if v not in reached and parents[v] in reached] + need(layer, 'cycle or disconnected forest') + order += layer + reached.update(layer) + return order + + +def edge_weight(K, u, v): + return K[v if u == 120 else u].bit_count() if 120 in (u, v) else (K[u] ^ K[v]).bit_count() + 2 + + +def all_edges(K): + return [(edge_weight(K, u, v), u, v) for u in range(121) for v in range(u)] + + +def forest_cost(K, parents): + traversal(parents) + return sum(edge_weight(K, v, p) for v, p in enumerate(parents)) + + +def certify_mst(K, parents): + """Cycle property is a certificate, not a replay of the nomination solver.""" + traversal(parents) + adj = [[] for _ in range(121)] + for v, p in enumerate(parents): + c = edge_weight(K, v, p) + adj[v].append((p, c)) + adj[p].append((v, c)) + checked = 0 + for u in range(121): + stack = [(u, -1, 0)] + maximum = {} + while stack: + v, prev, m = stack.pop() + maximum[v] = m + stack.extend((n, v, max(m, c)) for n, c in adj[v] if n != prev) + for v in range(u): + need(edge_weight(K, u, v) >= maximum[v], 'MST cycle inequality') + checked += 1 + return {'cost': forest_cost(K, parents), 'cycle_inequalities': checked} + + +def construct(word, parents): + K = rows(word) + order = traversal(parents) + prep = [[0, 120+v, [120+parents[v]]] for v in reversed(order) if parents[v] != 120] + correction = [] + for v, p in enumerate(parents): + row = K[v] ^ (K[p] if p != 120 else 0) + src = [s for s in range(240, 660) if row >> s & 1] + if src: + correction.append([0, 120+v, src]) + changed = copy.deepcopy(word) + changed['D'] = prep + correction + list(reversed(prep)) + return changed + + +def semantic_D(word, baseline): + """All 660 symbolic columns; target inputs are independent and nonzero.""" + state = [1 << r for r in range(660)] + for f, d, srcs in word['D']: + need(f == 0 and 120 <= d < 240, 'D must touch only frame-zero targets') + need(srcs and len(set([d] + srcs)) == 1+len(srcs), 'D operands') + for s in srcs: + need(120 <= s < 660, 'D source must be target or helper') + state[d] ^= state[s] + want = [1 << r for r in range(660)] + for t, row in enumerate(rows(baseline)): + want[120+t] ^= row + need(state == want, 'dirty D endpoint') + + +def records(word, dims): + cur = list(word['start']) + result = [] + def move(r, frame): + if cur[r] != frame: + result.append((0, r, cur[r], frame, dims[frame]-dims[cur[r]], 0)) + cur[r] = frame + for phase, name in enumerate(PHASES, 1): + if name == 'scatter': + for k, q in enumerate(word['ret']): + f = cur[q] + result.append((2, q, 660, f, 0, dims[f])) + for t, row in enumerate(word['scatter']): + if k in row: + result.append((1, 120+t, 660, 1, 0, 3)) + result.append((3, q, 660, f, 0, 0)) + else: + for f, d, srcs in word[name]: + for r in [d] + srcs: + move(r, f) + result.extend((1, d, s, 1, f, phase) for s in srcs) + for r, f in enumerate(word['final']): + move(r, f) + return result + + +def prefix_bounds(rec): + maxima = [] + for reverse in (False, True): + norms = [1] * 661 + largest, opened = 1, False + for op, a, b, c, f, z in (reversed(rec) if reverse else rec): + if op == 1: + norms[a] += abs(c)*norms[b] + largest = max(largest, norms[a]) + elif op in (2, 3): + opening = (op == 2) != reverse + need(opened != opening, 'copy lifecycle') + norms[b] = norms[a] if opening else 0 + opened = opening + need(not opened, 'open copy at endpoint') + maxima.append(largest) + F, B = maxima + payload = 64 * F**3 * B**2 + return {'forward': F, 'reverse': B, 'payload': str(payload), 'payload_bits': payload.bit_length()} + + +def independent_set_replay(rec): + """Separate set-valued interpreter for the actual binary native stream.""" + for backwards in (False, True): + state = [{r} for r in range(660)] + [set()] + opened = False + for op, a, b, c, f, z in (reversed(rec) if backwards else rec): + if op == 1 and c % 2: + state[a].symmetric_difference_update(state[b]) + elif op in (2, 3): + opening = (op == 2) != backwards + need(opened != opening, 'set copy lifecycle') + state[b] = set(state[a]) if opening else set() + opened = opening + want = [{r} if not 120 <= r < 240 else {r, r-120} for r in range(660)] + [set()] + need(state == want and not opened, 'independent full endpoint') + + +def inventory(word, rec): + profile = Counter() + for op, a, b, c, f, z in rec: + if op == 0: + profile[f] += 1 + elif op == 2: + profile[z] += 1 + return {'D_XORs': sum(len(g[2]) for g in word['D']), + 'ADDs': sum(r[0] == 1 for r in rec), 'records': len(rec), + 'COPYs': sum(r[0] == 2 for r in rec), + 'ERASEs': sum(r[0] == 3 for r in rec), + 'profile': {str(k): v for k, v in sorted(profile.items())}, + 'rank_mass': sum(k*v for k, v in profile.items()), + 'prefix': prefix_bounds(rec), 'word_sha256': digest(word)} + + +def expect_rejection(fn, label): + try: + fn() + except (ValueError, RuntimeError): + return label + raise ValueError('control was accepted: ' + label) + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument('--write-certificate', action='store_true') + parser.add_argument('--native', action='store_true') + args = parser.parse_args() + baseline = load_source() + recipe = json.loads((HERE / 'RECIPE.json').read_text()) + K = rows(baseline) + optimum = certify_mst(K, recipe['minimum_parents']) + changed = construct(baseline, recipe['feasible_parents']) + minword = construct(baseline, recipe['minimum_parents']) + semantic_D(changed, baseline) + semantic_D(minword, baseline) + need({k:v for k,v in changed.items() if k != 'D'} == {k:v for k,v in baseline.items() if k != 'D'}, 'changed exterior') + spec = importlib.util.spec_from_file_location('r420_pinned_xcheck', ROOT / 'research/e8-bit-r420/code/xcheck.py') + xc = importlib.util.module_from_spec(spec) + spec.loader.exec_module(xc) + check = xc.Word(baseline) + labels = check.labels() + check.full() + H, C, _ = check.interface() + need(all(H.values()) and all(C.values()), 'baseline interface') + check.w = changed + check.full() + H, C, _ = check.interface() + need(not H['H2_D_frame0_targets_from_helpers'], 'literal H2 must reject new syntax') + need(not C['K_equals_D'], 'literal K extractor must reject new syntax') + need(all(v for k,v in H.items() if k != 'H2_D_frame0_targets_from_helpers'), 'other interface hypotheses') + need(all(v for k,v in C.items() if k != 'K_equals_D'), 'other interface conclusions') + rec0, rec1, recmin = [records(w, check.fdim) for w in (baseline, changed, minword)] + need([r for r in rec0 if r[0] != 1] == [r for r in rec1 if r[0] != 1], 'paid movement/copy/erase subsequence changed') + controls = [] + cyc = recipe['feasible_parents'][:] + cyc[5] = 5 + controls.append(expect_rejection(lambda: traversal(cyc), 'cyclic parent')) + badtree = [120]*120 + controls.append(expect_rejection(lambda: certify_mst(K, badtree), 'nonminimum tree')) + preparation_count = sum(p != 120 for p in recipe['feasible_parents']) + for label, index in [('missing preparation', 0), ('missing restoration', len(changed['D'])-1), ('missing correction', preparation_count)]: + mutant = copy.deepcopy(changed) + del mutant['D'][index] + controls.append(expect_rejection(lambda: semantic_D(mutant, baseline), label)) + mutant = copy.deepcopy(changed) + mutant['D'][0][0] = 1 + controls.append(expect_rejection(lambda: semantic_D(mutant, baseline), 'nonzero D frame')) + mutant = copy.deepcopy(changed) + mutant['D'][0][1] = 240 + controls.append(expect_rejection(lambda: semantic_D(mutant, baseline), 'helper write')) + need(prefix_bounds(rec1)['payload_bits'] <= 104, 'feasible forest exceeds payload cap') + controls.append(expect_rejection(lambda: need(prefix_bounds(recmin)['payload_bits'] <= 104, 'payload cap'), 'minimum-cost nominated tree exceeds payload cap')) + neutral = copy.deepcopy(changed) + neutral['D'][:0] = [[0, 120, [121]], [0, 120, [121]]] + semantic_D(neutral, baseline) + need(inventory(neutral, records(neutral, check.fdim))['ADDs'] == len([r for r in rec1 if r[0] == 1])+2, 'neutral pair must be paid') + with tempfile.TemporaryDirectory(prefix='r420-forest-') as tmp: + tmp = Path(tmp) + exporter = ROOT / 'research/e8-bit-carrier-skeleton/code/bit/export_records.py' + for label, word, expected in [('baseline', baseline, rec0), ('forest', changed, rec1)]: + path = tmp / (label+'.json') + path.write_text(json.dumps(word)) + out = tmp / label + subprocess.run([sys.executable, '-I', '-B', str(exporter), str(path), str(out)], check=True, capture_output=True, text=True) + actual = list(struct.iter_unpack('<6i', (out/'249-records.bin').read_bytes())) + need(actual == expected, 'official record stream mismatch') + independent_set_replay(actual) + if args.native: + spec = importlib.util.spec_from_file_location("forest_native", HERE / "native.py") + native = importlib.util.module_from_spec(spec) + spec.loader.exec_module(native) + native.run(ROOT, tmp, recmin) + result = {'base_commit': '66849e1475c930fd7732b1a0067ffee7e1e95f60', + 'labels': labels, 'minimum_forest_certificate': optimum, + 'minimum_nominated_tree': inventory(minword, recmin), + 'baseline': inventory(baseline, rec0), 'feasible_forest': inventory(changed, rec1), + 'roots': sum(p == 120 for p in recipe['feasible_parents']), + 'preparation_XORs': sum(p != 120 for p in recipe['feasible_parents']), + 'columns_per_direction': 660, 'negative_controls': controls, + 'positive_control': 'F2-neutral target pair costs two ADDs', + 'interface': 'Semantic H2-prime; literal H2 and literal K extractor reject. All other H and C predicates pass.', + 'scope': 'Finite F2 circuit and exact rooted-forest cost optimum; feasible cut is not claimed precision-constrained optimal; no new kappa.'} + certificate = HERE / 'CERTIFICATE.json' + if args.write_certificate: + certificate.write_text(json.dumps(result, indent=2)+'\n') + else: + need(json.loads(certificate.read_text()) == result, 'certificate mismatch') + print('PASS_R420_TARGET_FOREST D=19922->15138 ADDs=26916->22132 saved=4784 forest_floor=14921 payload_bits=104 columns=660 controls=8 no_new_kappa') + + +if __name__ == '__main__': + main()