diff --git a/docs/ci-verification.md b/docs/ci-verification.md index 63ba3e9aa8..52b62d0481 100644 --- a/docs/ci-verification.md +++ b/docs/ci-verification.md @@ -1,8 +1,25 @@ # CI verification -## Current selected-family replay: #6030 +## Current selected-family replay: #7000 with #7001 The [selected record](../certificates/selected-result.json) binds conditional +κ = 0.00363005817 to the [application review](research/pr-intake-evidence/pr7000-application/PROOF-REVIEW.md), +[validation receipts](research/pr-intake-evidence/pr7000-application/VALIDATION.json), +and [explicit source closure](../certificates/frontier7000-source.json). +`make frontier7000-verify` follows that exact-source selected replay. The review +reuses eleven authenticated preceding executions and records seven fresh serial +application, scalar and complete native-catalogue executions. The earlier +monolithic timeout is retained separately and is not completed coverage. +Consult the receipts for exact commands, source heads and limits. + +The five inherited framework assumptions remain. No complete uniform word, +literal multiplier execution, independent human proof or formal-kernel proof +is asserted. Routine research submissions do not need to rerun this +selected-family replay. The sections below preserve historical checkpoints. + +## Historical selected-family replay: #6030 + +The [historical checkpoint](../certificates/checkpoints/frontier6030.json) binds conditional κ = 0.003125804 to the [proof review](research/pr-intake-evidence/pr6030-audit/PROOF-REVIEW.md), [validation receipts](research/pr-intake-evidence/pr6030-audit/VALIDATION.json), and [explicit source closure](../certificates/frontier6030-source.json). diff --git a/research/bit-paired-reflection-bound/PROOF.md b/research/bit-paired-reflection-bound/PROOF.md new file mode 100644 index 0000000000..7a5d11d5dd --- /dev/null +++ b/research/bit-paired-reflection-bound/PROOF.md @@ -0,0 +1,45 @@ +# A paid-volume bound for paired BIT reflections + +**NO VERIFIED GAIN.** On the retained #7001 BIT interface, two independent full-fibre rank-one address reflections cannot be made cheaper by packing them into reflection children with normalized linear adapters. This applies at κ = 0.0040075385047236 and throughout 0 ≤ κ ≤ 1/2. + +## Literal address maps + +The [#7001](https://github.com/CrocSwap/integer-mult-bounds/pull/7001) provider uses the #6726 native word. A nested chart move uses the split involution $D_P$ for the projector P of the orthogonal difference. Write its address variables as $(x,y)=(H,C_nD)$, with $C_n$ reversing atom positions. In these coordinates $D_P(x,y)=((I-P)x+Py,Px+(I-P)y)$. In the sum and difference variables $(x+y,x-y)$ this is $\operatorname{diag}(I,I-2P)$. The change is invertible at every admissible odd prime and every power of it. Hence the exact rational reflection $I-2P$ acts on the difference coordinates, with the sum coordinates as spectators. The resulting permutation acts linearly on binary data. The move rank is $\operatorname{rank}P$. [Physical split involution and cover](https://github.com/CrocSwap/integer-mult-bounds/blob/e54523517d0f03e58352e647c403a5af3e525a57/research/kappa-rebuild/bit/DELAYED-COVER-BRIDGE.md#2-native-projector-jobs-before-canonical-lowering) + +The rational orthogonal reframe $A=I-2nn^{\mathsf T}/4$, with $n=(0,1,0,-1,1,0,1,0)$, permutes all 111 port head lines and their paired body hyperplanes. Of 1,386 rank-one MOVE occurrences, 660 have independent original and rotated paid directions, all with absolute cosine 1/2. Exactly 264 share their source span and 396 change it. The first common-source pair is zero-based event 19152, role 0, charts 2→125. Its directions are $d=e_3$ and $u=(0,1,0,1,1,0,1,0)/2$. In the plane basis $(d,u)$ the exact maps are + +$$R_d=\begin{pmatrix}-1&-1\\0&1\end{pmatrix},\qquad R_u=\begin{pmatrix}1&0\\-1&-1\end{pmatrix}.$$ + +Both fix the perpendicular complement, are self-inverse and fail to commute. The rank-two reflection of the plane is $-I$ on that plane. The first changed-source pair is event 19167, role 225, charts 3→213. [REFLECTION.json](REFLECTION.json) gives the exact ambient matrices. The two fields are independent in the all-column contract. Their normalized target is the direct sum of the two address permutations. + +## Rank of the binary data operator + +Put $s=q^f$, with q an admissible odd prime and f≥1 the digit width of one active rank axis, including its atom width. A full-fibre bank of volume V contains all combinations of the active digit coordinates and an unchanged spectator set. A rank-r reflection has $V/s^r$ fixed positions, since all $rf$ flipped digits must be zero. Every other position is paired into a transposition. On binary data a transposition contributes one to $\operatorname{rank}_{\mathbb F_2}(K-I)$. The defect of this child is $V(1-s^{-r})/2$. Spectator multiplicity is included in V. + +Let the original rank-one fields have volumes $V_1,V_2$ and direct-sum target T. Then $\operatorname{rank}(T-I)=(V_1+V_2)(1-s^{-1})/2$. Allow any sequence of linear adapters, workspace initialization, child banks and linear readout. Each child acts as identity away from its bank. Use the same preparation and readout when replacing all children by identity, and require that the resulting external map be identity. Only the external map on the required input space is normalized. + +Telescope the difference between the two external maps, changing one child at a time. Each term factors through $K_i-I$ and has rank at most $V_i'(1-s^{-r_i})/2$, where $V_i'$ is the complete child volume. This permits overlapping banks, rectangular adapters and clean padding. Consequently + +$$ (V_1+V_2)(1-s^{-1})\le\sum_i V_i'(1-s^{-r_i}). $$ + +For a single rank-two child of two equal original volumes V this requires $V'\ge 2sV/(s+1)\ge3V/2$. A volume-V child is too small. Charging the larger volume at $V'(2f)^{1-\kappa}$ costs strictly more than the two original calls at $2Vf^{1-\kappa}$ for the stated κ range. + +For r=1 the quotient $(1-s^{-r})/(1-s^{-1})$ is one, for r=2 it is at most 4/3, and for r≥3 it is less than 3/2. Hence it is at most $\sqrt r\le r^{1-\kappa}$, strictly at r≥2. The summed volume-weighted tariff is at least $(V_1+V_2)f^{1-\kappa}$, with a strict surcharge if any positive-volume child has rank ≥2. This calculation grants free setup, routing, linear mixing and restoration inside the stated scope. Charging those operations cannot yield a saving there. + +## Cover routes alone cannot pay the missing rank + +If replacing the children by identity produces a map H, telescoping bounds $\operatorname{rank}(T-H)$ by the same child capacity. The retained matchers route complete cover rows by $g\mapsto gS$. This changes the cover index and preserves the ambient address z in every moved row. Pointwise scalar operations and zero preparation preserve the same address grading. Any no-child map composed of these operations is block diagonal by z, even if it mixes all rows and roles at each address. + +Let m be the number of transpositions in T. Every one changes the ambient address, with the cover index and role fixed. Fix a total order on z and orient each transposition from lower address $a_i$ to higher address $b_i$. Take the rows of the lower endpoints and the columns of the corresponding higher endpoints, ordered by $a_i$. T gives the identity on this minor. The H entry $(i,j)$ can be nonzero only if $a_i=b_j>a_j$. Thus H is strictly lower triangular on this minor and $\operatorname{rank}(T-H)\ge m=\operatorname{rank}(T-I)$. The same paid-volume bound applies to any address-preserving no-child map. In particular, existing cover right routes can conjugate a retained child but cannot supply one of these two address reflections alone. + +For a general H the weaker necessary inequality is $\operatorname{rank}(H-I)\ge\operatorname{rank}(T-I)-\sum_i V_i'(1-s^{-r_i})/2$. A genuinely address-changing H, incomplete fibres, changed external contracts and other paid primitives remain separate questions. + +## Verification and credit + +The replay checks all 111 port correspondences, all 1,386 rank-one sites and the common-source and changed-source examples over the rationals. It enumerates all plane addresses at primes 5, 7 and 11 and checks all 53,001 input cases of the corresponding doubled split involutions. At q=5 the two independent fields have combined defect rank 20 per sum-coordinate spectator, and the one-plane rank-two permutation has rank 12. Replacing the second field by a literal identity spectator reduces the target rank to 10 and removes the obstruction. The checker also tests 28 exact finite tariff comparisons. For event 19167 an exact control across all 480 GL₂(F₅) rows retains all 9,600 triangular pivots under a nonidentity cover route with 2,240 strict-lower entries. A true address-changing no-child map equal to T cancels those pivots. The general inequalities prove the result for all admissible widths and ranks. + +[Androo Lloyd's #673](https://github.com/androolloyd/integer-mult-bounds/blob/0b4f514c60d9bc7786415d7cbc24754f24d6dc3b/research/bit-role-sharing-budget/PROOF.md) supplies the rank-defect argument for one fixed address permutation. This contribution evaluates different literal rank-one directions and higher-rank reflection children with distinct bank volumes and charges. [#1920](https://github.com/CrocSwap/integer-mult-bounds/pull/1920) and [#1924](https://github.com/CrocSwap/integer-mult-bounds/pull/1924) study complex reciprocal and clean-selector encodings. Credit zxv and the #6726 lineage for the word, DreamingOfClouds and CubeJerry for the #6834/#6980/#7001 paired construction, and the Round 8 projective search for the candidate reflection. [#7162](https://github.com/CrocSwap/integer-mult-bounds/pull/7162) covers a separate change to the caller schedule with the native bill fixed. OpenAI Codex and subagents materially assisted the derivation and independent audit. + +## Open next questions + +Can an already-required address-changing map supply H without exceeding the price saved by removing a reflection? Begin at event 19167 and compute H on both retained source charts. The cover right routes alone cannot supply it. Charge every address change and require the full binary action on arbitrary complete fields. All-width realization, ordinary adapter costs, larger BIT atom admission and the fixed-tape proof remain open. diff --git a/research/bit-paired-reflection-bound/README.md b/research/bit-paired-reflection-bound/README.md new file mode 100644 index 0000000000..b851c83694 --- /dev/null +++ b/research/bit-paired-reflection-bound/README.md @@ -0,0 +1,19 @@ +# Paired BIT reflection packing bound + +**NO VERIFIED GAIN.** Full-fibre reflection children and linear adapters whose no-child composite preserves ambient addresses cannot save paid moment on the two independent rank-one reflections of the proposed #7001 reframe. The lower bound charges arbitrary child volumes and ranks and allows overlapping banks and restored padding. It uses the number of moved addresses in the odd-prime fibre. [Proof](PROOF.md) · [Exact receipt](REFLECTION.json) + +## Clean replay + +Run from the repository root with CPython 3.12 and assertions enabled. + +```sh +python3.12 -B scripts/research_package.py --package research/bit-paired-reflection-bound +``` + +The verifier pins the literal native word, checks 111 port correspondences and 1,386 rank-one sites, and specializes the exact split address actions over three odd primes and checks the cover-route minor on all 480 GL₂(F₅) rows. The full-width tariff inequality is proved in the accompanying text. + +## Open next questions + +An adapter whose no-child composite changes ambient addresses can evade the normalization. Test the first changed-source pair at native event 19167, beginning with its original and rotated chart maps. Establish the exact action and debit of that adapter before pricing a whole family. The full paired supplier and larger BIT atom remain open. + +Credit Androo Lloyd #673 for the fixed-permutation rank method, zxv #6726 for the word, DreamingOfClouds and CubeJerry for the paired source lineage, and #1920/#1924 for related complex encodings. OpenAI Codex and subagents materially assisted. Apache-2.0. diff --git a/research/bit-paired-reflection-bound/REFLECTION.json b/research/bit-paired-reflection-bound/REFLECTION.json new file mode 100644 index 0000000000..8d94d370f7 --- /dev/null +++ b/research/bit-paired-reflection-bound/REFLECTION.json @@ -0,0 +1,479 @@ +{ + "checked_port_pairs": 111, + "common_plane_full_reflection": [ + [ + "-1", + "0" + ], + [ + "0", + "-1" + ] + ], + "cover_route_minor_control": { + "address_prime": 5, + "changed_conjugated_addresses": 11520, + "cover_rows": 480, + "difference_addresses_per_row": 25, + "input_slots": 24000, + "minor_pivots_cancelled_by_address_changing_control": 9600, + "nonzero_strictly_lower_control_entries": 2240, + "triangular_minor_dimension": 9600 + }, + "finite_controls": [ + { + "address_prime": 5, + "minimum_bank_volume_ratio": "5/3", + "operand_plane_volume": 25, + "rank_minus_identity": [ + 10, + 10, + 12 + ], + "split_address_cases": 1875 + }, + { + "address_prime": 7, + "minimum_bank_volume_ratio": "7/4", + "operand_plane_volume": 49, + "rank_minus_identity": [ + 21, + 21, + 24 + ], + "split_address_cases": 7203 + }, + { + "address_prime": 11, + "minimum_bank_volume_ratio": "11/6", + "operand_plane_volume": 121, + "rank_minus_identity": [ + 55, + 55, + 60 + ], + "split_address_cases": 43923 + } + ], + "finite_efficiency_controls": 28, + "first_cases": { + "changed_source": { + "directions": [ + [ + "-1", + "0", + "0", + "-1", + "0", + "1", + "1", + "0" + ], + [ + "-1", + "-1", + "0", + "0", + "-1", + "1", + "0", + "0" + ] + ], + "event": 19167, + "role": 225, + "source": 3, + "target": 213 + }, + "common_source": { + "directions": [ + [ + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0" + ], + [ + "0", + "1/2", + "0", + "1/2", + "1/2", + "0", + "1/2", + "0" + ] + ], + "event": 19152, + "role": 0, + "source": 2, + "target": 125 + } + }, + "first_changed_source_addresses": [ + [ + [ + "1/2", + "0", + "0", + "-1/2", + "0", + "1/2", + "1/2", + "0" + ], + [ + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0" + ], + [ + "-1/2", + "0", + "0", + "1/2", + "0", + "1/2", + "1/2", + "0" + ], + [ + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0" + ], + [ + "1/2", + "0", + "0", + "1/2", + "0", + "1/2", + "-1/2", + "0" + ], + [ + "1/2", + "0", + "0", + "1/2", + "0", + "-1/2", + "1/2", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1" + ] + ], + [ + [ + "1/2", + "-1/2", + "0", + "0", + "-1/2", + "1/2", + "0", + "0" + ], + [ + "-1/2", + "1/2", + "0", + "0", + "-1/2", + "1/2", + "0", + "0" + ], + [ + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0" + ], + [ + "-1/2", + "-1/2", + "0", + "0", + "1/2", + "1/2", + "0", + "0" + ], + [ + "1/2", + "1/2", + "0", + "0", + "1/2", + "1/2", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1" + ] + ] + ], + "first_original_address": [ + [ + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "-1", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1" + ] + ], + "first_plane_addresses": [ + [ + [ + "-1", + "-1" + ], + [ + "0", + "1" + ] + ], + [ + [ + "1", + "0" + ], + [ + "-1", + "-1" + ] + ] + ], + "first_rotated_address": [ + [ + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "1/2", + "0", + "-1/2", + "-1/2", + "0", + "-1/2", + "0" + ], + [ + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "-1/2", + "0", + "1/2", + "-1/2", + "0", + "-1/2", + "0" + ], + [ + "0", + "-1/2", + "0", + "-1/2", + "1/2", + "0", + "-1/2", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0" + ], + [ + "0", + "-1/2", + "0", + "-1/2", + "-1/2", + "0", + "1/2", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1" + ] + ], + "fixed_target": "10018846261809/2500000000000000", + "independent_rank_one_pairs": { + "changed_source": 396, + "common_source": 264 + }, + "native_rank_one_sites": 1386, + "pins": { + "bit/retained/inputs/BIT-NATIVE-WORD.json.gz": "51203e7fc75ba10bd3ac3f8e675759f47e13d262bea66b6600d1e515095cad78" + }, + "status": "EXCLUDED_NORMALIZED_PAID_REFLECTION_PACKING" +} diff --git a/research/bit-paired-reflection-bound/SOURCES.json b/research/bit-paired-reflection-bound/SOURCES.json new file mode 100644 index 0000000000..79789550cf --- /dev/null +++ b/research/bit-paired-reflection-bound/SOURCES.json @@ -0,0 +1,30 @@ +{ + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "files": [ + { + "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8", + "path": "certificates/selected-result.json", + "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1", + "usage": "provenance" + }, + { + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "path": "docs/research/agent-task-catalog.json", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81", + "usage": "provenance" + }, + { + "git_blob": "b718d6b2848215ad785022106dfa9f871a3d1c0c", + "path": "research/paired-query-only-bit/retained/inputs/BIT-NATIVE-WORD.json.gz", + "sha256": "51203e7fc75ba10bd3ac3f8e675759f47e13d262bea66b6600d1e515095cad78", + "usage": "input" + }, + { + "git_blob": "a58774e237c9362869a60a22bda35be09fb85872", + "path": "research/kappa-rebuild/bit/DELAYED-COVER-BRIDGE.md", + "sha256": "9731b93026717f5fa15851e3633cbb4bdc76eba2bffb9d6b4a3b69f7dd502443", + "usage": "provenance" + } + ], + "schema_version": 1 +} diff --git a/research/bit-paired-reflection-bound/TASK.json b/research/bit-paired-reflection-bound/TASK.json new file mode 100644 index 0000000000..92e14fcbd0 --- /dev/null +++ b/research/bit-paired-reflection-bound/TASK.json @@ -0,0 +1,64 @@ +{ + "actual_scope": "Paired #7001 independent full-fibre rank-one reflections, arbitrary full-fibre paid child banks, address-preserving external no-child map and linear adapters.", + "ai_assistance": "Substantial OpenAI Codex and subagent assistance with proof, replay and independent rank and price audits.", + "author": "ToikY", + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "bottleneck_link": "The proposed BIT pair packing must reduce the full volume-weighted rank tariff to fund the raw moment gap.", + "budget_minutes": 30, + "evidence": "Exact rational charts, 111 paired port maps, 1,386 rank-one sites, all addresses on three finite planes and an all-width volume proof. Exact split-address conjugacy and a GL2(F5) cover-route minor with 9600 pivots.", + "open_questions": [ + { + "blocked_by": "Arbitrary-input linear action and all-width fixed-tape accounting of the address map.", + "first_step": "At event 19167 derive the two exact chart maps and price the nonidentity part under the existing ordinary and recursive budget.", + "question": "Can a charged nonidentity no-child address map fund the missing defect?", + "why_it_matters": "The rank bound identifies the displacement that must be supplied by the map." + } + ], + "original_card": { + "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "allowed_variations": [ + "Choose a fixed larger register count or a specified nonabelian operation family." + ], + "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.", + "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "id": "bit-new-register-model", + "methods": [ + "Construct the smallest exact identity in a newly specified legal operation alphabet.", + "Derive a target-specific relaxation bound for that same explicit alphabet." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ], + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "scope_change_triggers": [ + "Remaining inside the already-excluded three-register abelian model.", + "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result." + ], + "starting_points": [ + "docs/research/research-family-status.md", + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json", + "research/bit-gl3-mixed-targets-length10/README.md", + "docs/research/community-efficient1000-review.md" + ] + }, + "outcome": "negative-result", + "priority_revision": 8, + "schema_version": 1, + "scope_change_reason": "Test an actual changed native interface rather than the fixed native invoice of the paired schedule proof.", + "scope_status": "changed", + "stop_rule": "Stop if the all-width displacement rank and child tariff bounds exclude every address-preserving no-child map.", + "task_id": "bit-new-register-model" +} diff --git a/research/bit-paired-reflection-bound/VERIFY.json b/research/bit-paired-reflection-bound/VERIFY.json new file mode 100644 index 0000000000..3aa2648bbc --- /dev/null +++ b/research/bit-paired-reflection-bound/VERIFY.json @@ -0,0 +1,21 @@ +{ + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "checks": "Authenticate the #7001 word, replay exact paired address maps and fixed-point defect and tariff controls. Includes the split address involution and address-preserving cover route.", + "timeout_seconds": 60 + } + ], + "inputs": [ + "research/paired-query-only-bit/retained/inputs/BIT-NATIVE-WORD.json.gz" + ], + "python": "3.12", + "requirements": [], + "schema_version": 1, + "status": "ready" +} diff --git a/research/bit-paired-reflection-bound/verify.py b/research/bit-paired-reflection-bound/verify.py new file mode 100644 index 0000000000..695e65af73 --- /dev/null +++ b/research/bit-paired-reflection-bound/verify.py @@ -0,0 +1,265 @@ +"""Check the first paired BIT reflection and a normalized bank-volume bound.""" + +import argparse +from collections import Counter +from fractions import Fraction as Q +from functools import cache +import gzip +from hashlib import sha256 +from itertools import product +import json +from pathlib import Path + +PINS = { + 'bit/retained/inputs/BIT-NATIVE-WORD.json.gz': '51203e7fc75ba10bd3ac3f8e675759f47e13d262bea66b6600d1e515095cad78', +} + + +def read(path, key): + raw = path.read_bytes() + if sha256(raw).hexdigest() != PINS[key]: + raise ValueError(f'SHA-256 mismatch: {key}') + return raw + + +def dot(a,b): + return sum(x*y for x,y in zip(a,b,strict=True)) + + +def act(matrix, vector): + return tuple(dot(row,vector) for row in matrix) + + +def reflection(d): + norm = dot(d,d) + return tuple(tuple(Q(i==j)-Q(2)*x*y/norm for j,y in enumerate(d)) for i,x in enumerate(d)) + + +def encode(matrix): + return [[str(x) for x in row] for row in matrix] + + +def echelon(vectors): + basis = {} + for vector in vectors: + row = tuple(map(Q, vector)) + for pivot, prior in sorted(basis.items()): + row = tuple(x-row[pivot]*y for x,y in zip(row,prior,strict=True)) + first = next((i for i,x in enumerate(row) if x), None) + if first is not None: + pivot = row[first] + basis[first] = tuple(x/pivot for x in row) + for pivot in sorted(basis,reverse=True): + for earlier in sorted(p for p in basis if p < pivot): + row = basis[earlier] + basis[earlier] = tuple(x-row[pivot]*y for x,y in zip(row,basis[pivot],strict=True)) + return basis + + +def line_kernel(vectors): + basis = echelon(vectors) + col, = set(range(8))-basis.keys() + vector = [Q(0)]*8 + vector[col] = Q(1) + for p,row in basis.items(): + vector[p] = -row[col] + return tuple(vector) + + +def span(vectors): + return tuple(row for _,row in sorted(echelon(vectors).items())) + + +def cover_control(d, u): + def dot(x, y): + return sum(a * b for a, b in zip(x, y, strict=True)) + + cosine = Q(dot(d, u), dot(d, d)) + assert dot(d, d) == dot(u, u) and abs(cosine) == Q(1, 2) + reflections = ((-1, int(-2 * cosine), 0, 1), (1, 0, int(-2 * cosine), -1)) + swap = (0, 1, 1, 0) + q = 5 + + def matmul(a, b): + return tuple(sum(a[2 * i + k] * b[2 * k + j] for k in range(2)) % q + for i, j in product(range(2), repeat=2)) + + def inverse(a): + aa, ab, ba, bb = a + factor = pow((aa * bb - ab * ba) % q, -1, q) + return tuple(factor * x % q for x in (bb, -ab, -ba, aa)) + + def apply(a, x): + return tuple(sum(a[2 * i + j] * x[j] for j in range(2)) % q for i in range(2)) + + rows = [a for a in product(range(q), repeat=4) if (a[0] * a[3] - a[1] * a[2]) % q] + addresses = list(product(range(q), repeat=2)) + routed = {g: matmul(g, swap) for g in rows} + assert set(routed.values()) == set(rows) and all(routed[g] != g for g in rows) + assert matmul(swap, matmul(reflections[0], swap)) == tuple(x % q for x in reflections[1]) + targets = {} + changed_by_matcher = 0 + for g in rows: + matrices = [matmul(g, matmul(r, inverse(g))) for r in reflections] + gs = routed[g] + assert matmul(gs, matmul(reflections[0], inverse(gs))) == matrices[1] + for address in addresses: + changed_by_matcher += apply(matrices[0], address) != apply(matrices[1], address) + for role, matrix in enumerate(matrices): + targets[role, g, address] = role, g, apply(matrix, address) + assert all(targets[target] == key for key, target in targets.items()) + + lower = [key for key, target in targets.items() if key[-1] < target[-1]] + lower.sort(key=lambda key: key[-1]) + upper_column = {targets[key]: i for i, key in enumerate(lower)} + assert len(lower) == len(upper_column) == 2 * len(rows) * (q * q - q) // 2 + + # The no-child control routes just role zero and mixes role one into it + # at the matched row, always keeping the entire ambient address intact. + below_diagonal = 0 + for row, key in enumerate(lower): + role, g, z = key + source_rows = ((0, routed[g], z), (1, g, z)) if role == 0 else (key,) + for source in source_rows: + column = upper_column.get(source) + if column is not None: + assert column < row + below_diagonal += 1 + assert upper_column[targets[key]] == row + assert below_diagonal and changed_by_matcher + + # Allowing a true address permutation in H changes every minor pivot. + cancelled_by_physical_route = sum(upper_column[targets[key]] == i for i, key in enumerate(lower)) + assert cancelled_by_physical_route == len(lower) + return {"address_prime": q, "cover_rows": len(rows), "difference_addresses_per_row": len(addresses), + "input_slots": len(targets), "changed_conjugated_addresses": changed_by_matcher, + "triangular_minor_dimension": len(lower), "nonzero_strictly_lower_control_entries": below_diagonal, + "minor_pivots_cancelled_by_address_changing_control": cancelled_by_physical_route} + + +def main(bit): + native = 'retained/inputs/BIT-NATIVE-WORD.json.gz' + w = json.loads(gzip.decompress(read(bit / native, 'bit/'+native))) + matrix = reflection((0,1,0,-1,1,0,1,0)) + frames = {int(key):value for key,value in w['frames'].items()} + spaces = {f:span(v['B']) for f,v in frames.items()} + heads = [spaces[f] for f in w['start'][:111]] + assert len(heads)==len(set(heads))==111 + for i,head in enumerate(heads): + j = heads.index(span(act(matrix,v) for v in head)) + body = spaces[w['final'][111+i]] + assert span(act(matrix,v) for v in body)==spaces[w['final'][111+j]] + + @cache + def complements(source,target): + a,b = sorted((source,target),key=lambda f:frames[f]['dim']) + direction = line_kernel(tuple(frames[b]['A'])+spaces[a]) + rotated = act(matrix,direction) + return direction,rotated,span(act(matrix,v) for v in spaces[source])==spaces[source] + + first = {} + counts = Counter() + total_rank_one = 0 + for i,(op,role,*args) in enumerate(w['program']): + if op != 'MOVE': + continue + source,target = args + if abs(frames[source]['dim']-frames[target]['dim']) != 1: + continue + total_rank_one += 1 + a,b,same_source = complements(source,target) + if len(span((a,b))) != 2: + continue + assert dot(a,a)==dot(b,b) and 2*abs(dot(a,b))==dot(a,a) + key = 'common_source' if same_source else 'changed_source' + counts[key] += 1 + first.setdefault(key,(i,role,source,target,a,b)) + assert counts=={'common_source':264, 'changed_source':396} + assert total_rank_one==1386 + assert first['common_source'][:4]==(19152,0,2,125) + + i,role,source,target,d,u = first['common_source'] + a,b = reflection(d),reflection(u) + cosine = dot(d,u)/dot(d,d) + ab_plane = (((Q(-1),-2*cosine),(Q(0),Q(1))), ((Q(1),Q(0)),(-2*cosine,Q(-1)))) + for ambient, plane in zip((a,b),ab_plane,strict=True): + for j, axis in enumerate((d,u)): + assert act(ambient,axis)==tuple(plane[0][j]*x+plane[1][j]*y for x,y in zip(d,u,strict=True)) + defect = [tuple(x-Q(i==j) for j,x in enumerate(row)) for i,row in enumerate(ambient)] + assert len(span(defect))==1 + assert act(a,act(b,d))!=act(b,act(a,d)) + + def mod(v,q): + return (v.numerator*pow(v.denominator,-1,q))%q + + def perm(map_, points, q): + return [tuple(mod(v,q) for v in act(map_,p)) for p in points] + + controls = [] + for q in (5,7,11): + points = list(product(range(q),repeat=2)) + index = {point:j for j,point in enumerate(points)} + involutions = (*ab_plane, ((Q(-1),Q(0)),(Q(0),Q(-1)))) + permutations = [[index[y] for y in perm(m,points,q)] for m in involutions] + rank = [] + for permutation in permutations: + assert all(permutation[permutation[j]]==j for j in range(q*q)) + rank.append(sum(j rank[-1] + assert 4*Q(q,q+1)**2 > 2 + for permutation, defect in zip(permutations,rank,strict=True): + reflected = {x:points[permutation[j]] for j,x in enumerate(points)} + half = pow(2,-1,q) + projector = {x:tuple(half*(a-b)%q for a,b in zip(x,y,strict=True)) + for x,y in reflected.items()} + fixed = 0 + for x,y in product(points,repeat=2): + difference = tuple((a-b)%q for a,b in zip(x,y,strict=True)) + p = projector[difference] + out_left = tuple((a-b)%q for a,b in zip(x,p,strict=True)) + out_right = tuple((a+b)%q for a,b in zip(y,p,strict=True)) + assert tuple((a-b)%q for a,b in zip(out_left,out_right,strict=True))==reflected[difference] + assert tuple((a+b)%q for a,b in zip(out_left,out_right,strict=True))==tuple( + (a+b)%q for a,b in zip(x,y,strict=True)) + fixed += out_left==x and out_right==y + assert fixed==q*q*(q*q-2*defect) + controls.append({'address_prime':q,'operand_plane_volume':q*q,'rank_minus_identity':rank, + 'split_address_cases':3*q**4, + 'minimum_bank_volume_ratio':str(Q(2*q,q+1))}) + + # Replacing the second true operand by an identity field erases its + # defect and invalidates the two-field obstruction. + assert all(x['rank_minus_identity'][0] <= x['rank_minus_identity'][-1] for x in controls) + for side in (3,5,7,11): + for rank in range(2,9): + assert rank*(1-Q(1,side))**2>(1-Q(1,side**rank))**2 + return {'status':'EXCLUDED_NORMALIZED_PAID_REFLECTION_PACKING', + 'pins':PINS, 'fixed_target':'10018846261809/2500000000000000', + 'checked_port_pairs':111,'native_rank_one_sites':total_rank_one, + 'independent_rank_one_pairs':dict(counts), + 'first_cases':{k:{'event':v[0],'role':v[1],'source':v[2],'target':v[3], + 'directions':encode(v[4:])} for k,v in first.items()}, + 'first_original_address':encode(a),'first_rotated_address':encode(b), + 'first_changed_source_addresses':[encode(reflection(direction)) for direction in first['changed_source'][4:]], + 'first_plane_addresses':[encode(m) for m in ab_plane], + 'common_plane_full_reflection':encode(((Q(-1),Q(0)),(Q(0),Q(-1)))), + 'finite_controls':controls,'finite_efficiency_controls':28, + 'cover_route_minor_control':cover_control(*first['changed_source'][4:])} + + +if __name__ == '__main__': + if not __debug__: + raise SystemExit('Use CPython 3.12 with assertions enabled') + parser = argparse.ArgumentParser(description=__doc__) + default = Path(__file__).resolve().parents[1] / 'paired-query-only-bit' + parser.add_argument('--bit-package',type=Path,default=default) + args=parser.parse_args() + result = json.dumps(main(args.bit_package),indent=2,sort_keys=True)+'\n' + receipt = Path(__file__).with_name('REFLECTION.json') + if args.bit_package==default and result!=receipt.read_text(): + raise ValueError('Frozen reflection receipt differs') + if args.bit_package==default: + print('PASS_BIT_REFLECTION_DEFECT_BOUND') + else: + print(result,end='') diff --git a/research/historical-selected-replay-gap/README.md b/research/historical-selected-replay-gap/README.md index 55d8cc3b49..36d9a873ca 100644 --- a/research/historical-selected-replay-gap/README.md +++ b/research/historical-selected-replay-gap/README.md @@ -69,7 +69,11 @@ python3 -B scripts/research_package.py --package research/historical-selected-re The direct command prints `PASS_HISTORICAL_SELECTED_REPLAY_GAP`. A registered replay prints `PASS_REGISTERED_RESEARCH_PACKAGE`. Both require Git history -containing the two inspected commits. +containing the two inspected commits and the source and manifest objects at +`2485805a6d47f36ea83ddde6327d453ac82d44dc`. The verifier uses a temporary +sparse checkout of that commit, checks the declared source digests there, and +uses its planner and manifest inventory. The recorded rejections and selection +therefore remain reproducible after later changes to the live Makefile or CI guide. ## Open next questions diff --git a/research/historical-selected-replay-gap/SOURCES.json b/research/historical-selected-replay-gap/SOURCES.json index c1010eec95..62bb8b3950 100644 --- a/research/historical-selected-replay-gap/SOURCES.json +++ b/research/historical-selected-replay-gap/SOURCES.json @@ -4,13 +4,13 @@ "files": [ { "path": "Makefile", - "usage": "input", + "usage": "provenance", "git_blob": "0d683a06b9e7ee162496108ce9a7c5d2ee94fccf", "sha256": "4f2d4f2dcd15139ec82658a975f85ed300897385f85799218539f4c8d60567da" }, { "path": "certificates/partial-swap-network.json", - "usage": "input", + "usage": "provenance", "git_blob": "eccafa830c16170c36faf93045ddf1f638f7bcd4", "sha256": "4c0b9d37e1034b2076e30a70f8e514416298c462d9ee98bc87fe6556b14df786" }, @@ -22,7 +22,7 @@ }, { "path": "docs/ci-verification.md", - "usage": "input", + "usage": "provenance", "git_blob": "63ba3e9aa8bdc5e942b56e34244b92b16f854085", "sha256": "c7d3027e9ad8bcbff68f07aa9576b30fb2f3c76c44d876d40c7fdbf4a3e2228a" }, @@ -34,163 +34,163 @@ }, { "path": "research/clifford-state-performance/SOURCE.json", - "usage": "input", + "usage": "provenance", "git_blob": "6f98a0061a5104dfab82c9e806f819b41811f684", "sha256": "396d0f08df24952248140d5c65c51b8c902ef1c580892ff7ea182890530f67ee" }, { "path": "research/community-batch1047-audit/CONTENT-COVERAGE.json", - "usage": "input", + "usage": "provenance", "git_blob": "5e0f92af463ec12c5e1dcc3effd44081a88af647", "sha256": "07a9daeaf2bda308a92e9a4684f13d5fc766c7772d74801fceb7f4599fdab226" }, { "path": "research/community-batch1099-audit/CONTENT-COVERAGE.json", - "usage": "input", + "usage": "provenance", "git_blob": "9e13266bf85e627f1b7dc225e9530ea69fd2c7f0", "sha256": "421e1211fb1897c45621dc6801c276e53f2e6f335583c9c9049e535f87c0a3b1" }, { "path": "research/community-batch932-audit/CONTENT-COVERAGE.json", - "usage": "input", + "usage": "provenance", "git_blob": "cc4d03eb59b9ab3f952735f7e88ff18c2d15d7af", "sha256": "184629cac91a5cfaca50330a88596008b824221433867dcf8117539c913c284a" }, { "path": "research/community-batch970-audit/CONTENT-COVERAGE.json", - "usage": "input", + "usage": "provenance", "git_blob": "8b9f4111badf7de5d97684799560b55110e9da79", "sha256": "23188ed920e38a54006cb883e181585620821c63bf7e8b5e05d32719417cc37e" }, { "path": "research/community-frontier741-audit/CONTENT-COVERAGE.json", - "usage": "input", + "usage": "provenance", "git_blob": "a5300d4e7a5381a3f443fc54c768ca6f0f236d68", "sha256": "3c820fb30e1b4d9bcfc6a7ab524375e5b2abd66b940af2c509146104f0bcd79c" }, { "path": "research/community-frontier890-audit/CONTENT-COVERAGE.json", - "usage": "input", + "usage": "provenance", "git_blob": "d7ff6d777b01d69b6ce84caf25d3b7e4a4d2f211", "sha256": "6b185a9902652f893f3ebd8ada92d2f11b6de6533a9a4d11718a8a4496101128" }, { "path": "research/community-hyperplane599-audit/SOURCE.json", - "usage": "input", + "usage": "provenance", "git_blob": "546f37d326d10a99910ae8f908e71ef768524d98", "sha256": "65099d764bfcc39bda5e4d9966783611b094c3522dbdd1435cd498d657a8ef8e" }, { "path": "research/community-k492-audit/SOURCE.json", - "usage": "input", + "usage": "provenance", "git_blob": "e538481e4cb16ed936d3195f2dfb5b5a9ca0a76b", "sha256": "2c0f4fa5bc150d05658af2e7c54c4d2c337dd52b7efd3d69530ae73bcbdf452a" }, { "path": "research/community-reconciliation92-audit/MANIFEST.json", - "usage": "input", + "usage": "provenance", "git_blob": "2a2e93685173d5f13cbb5abe740f5d90352e0228", "sha256": "5f501f3c118131e7d069f30ad77186eb2ad6961f9680a0ef105f4514ed41808a" }, { "path": "research/partial-swap-digest/baseline.py", - "usage": "input", + "usage": "provenance", "git_blob": "a2f0190704db83bd8ef48e46e723c49b925804fe", "sha256": "81e9af92cdf38243a540cdcff2062778e449467848d444da37a9553c12ca4c34" }, { "path": "research/r420-two-sided-basis/SOURCES.json", - "usage": "input", + "usage": "provenance", "git_blob": "5d718e11e62f4bcadecf1e02d6b61f87dbe190b0", "sha256": "d9810b0d139c5a1211fd2c1f0d142187cc1fca30026e1e7bc4f9ecfacf1596d1" }, { "path": "research/skip-clones/SOURCE.json", - "usage": "input", + "usage": "provenance", "git_blob": "8d1bb3b9c8189e35e5d8bfdfa632d7473e8be0d5", "sha256": "0b68e63e35a97ce6b0cdb6e291b88ebaa8f2dd4afb70b2498f10ee89428258dc" }, { "path": "research/split-skip/SOURCE.json", - "usage": "input", + "usage": "provenance", "git_blob": "2ab610b6ea2edd2865fda793ef2168b0c76afb4f", "sha256": "7c2b4646a3ecfef6f881da5c43e4bd0fa9a4d1b00548b8ab458d897e16735134" }, { "path": "scripts/historical-ci-inputs/Makefile", - "usage": "input", + "usage": "provenance", "git_blob": "aff68409021c9d401a6f8013b9dfd7dbcc30f2a8", "sha256": "ea8830dd79da493e2d75baf753d733ff7efbcf2b4794afe41fae0ac8f3055646" }, { "path": "scripts/historical-ci-inputs/ledger-batch932-run_isolated_tests.py", - "usage": "input", + "usage": "provenance", "git_blob": "65db599ab0b1dea0312c4ca048e0bd0f44c3736f", "sha256": "96ea543e6c707424afe247e77bd86c82152f90fc76a0773c4232145da5cdf8d1" }, { "path": "scripts/historical-ci-inputs/ledger-batch932-test_isolated_test_runner.py", - "usage": "input", + "usage": "provenance", "git_blob": "34820a8f24678f918f4d0e7a35380d8013fc3495", "sha256": "628391b6abfbc8674ceec1751867a4392f2cc0b5b66886243e139af86cf355ac" }, { "path": "scripts/historical-ci-inputs/ledger-batch970-verify_selected_result.py", - "usage": "input", + "usage": "provenance", "git_blob": "c755b76e0d44ba4917aa94440ebe54daefce5b2a", "sha256": "d7fd929726b326aeeaf0a3996475adec88eee9aac09ae0bebeeaa0bc1fc8f199" }, { "path": "scripts/historical-ci-inputs/ledger-frontier741-ci-verification.md", - "usage": "input", + "usage": "provenance", "git_blob": "7f3c012504187917a728b9fe87043f0fc8cd006a", "sha256": "a854022e0e1d5d4db4d60e586be3ea56005013ef14a1fc06d02bc06e8529c4b0" }, { "path": "scripts/historical-ci-inputs/partial-swap-context.json", - "usage": "input", + "usage": "provenance", "git_blob": "ad65114886bf34a4fd27e79f3be502389e689faa", "sha256": "833a9642f33aeab2ffea17ec9c6b82e0a953f90192b2c82e10bef21538dccba9" }, { "path": "scripts/historical-ci-inputs/partial-swap-network.json", - "usage": "input", + "usage": "provenance", "git_blob": "52075f2463f60af5e16571347f24274fce73a1ea", "sha256": "f3c4be597b2f2136da4ae2cc80c7454f63c90aa01f84e5b8131cee4dd55de815" }, { "path": "scripts/partial_swap/shared.py", - "usage": "input", + "usage": "provenance", "git_blob": "44a0e454c70f9c4b98e258b8443612e6a119904b", "sha256": "5a0646a50b9f3e8ea55168620a78e8853b0ab810517cefc8cfb8696aedee278a" }, { "path": "scripts/replay_historical_check.py", - "usage": "input", + "usage": "provenance", "git_blob": "1e92fff2782970ef71378f594f2350d245a4db26", "sha256": "5467619c78183d3adc82b0cb55af28e5c1a01fca2b0588677816244b53e2bafd" }, { "path": "scripts/research_package.py", - "usage": "input", + "usage": "provenance", "git_blob": "091b4c8f58bac9a9580d76025b887dc5c873d05f", "sha256": "e1256016e7f51827d04fa2179255989f639ae1d97afaa9c16265f85a0c6abd70" }, { "path": "scripts/run_isolated_tests.py", - "usage": "input", + "usage": "provenance", "git_blob": "a96ab35b315ce492e7fbbfd6c5ae211aa066b541", "sha256": "49eb56dd0fc0d8d8ffdb209970a7adf2176223580646f575d5c22e59543b381c" }, { "path": "scripts/verify_selected_result.py", - "usage": "input", + "usage": "provenance", "git_blob": "6882a4700e410dec569b51ae2eaf1a19cc019195", "sha256": "d6b305eac5b9bdb8172c469ad30a1655a60fa0aceac8b1bf610e1b73f51babd8" }, { "path": "tests/test_isolated_test_runner.py", - "usage": "input", + "usage": "provenance", "git_blob": "343b24abf6719b81805eba5a84c74e57634c8288", "sha256": "3a5470d0b139828b90e19bf9583ddeafcd69f8e34f2824664eb3a2958a52e34d" } diff --git a/research/historical-selected-replay-gap/VERIFY.json b/research/historical-selected-replay-gap/VERIFY.json index 98553e72ed..ab7efa3471 100644 --- a/research/historical-selected-replay-gap/VERIFY.json +++ b/research/historical-selected-replay-gap/VERIFY.json @@ -4,36 +4,7 @@ "python": "3.12", "requirements": [], "inputs": [ - "Makefile", - "certificates/partial-swap-network.json", - "docs/ci-verification.md", - "research/clifford-state-performance/SOURCE.json", - "research/community-batch1047-audit/CONTENT-COVERAGE.json", - "research/community-batch1099-audit/CONTENT-COVERAGE.json", - "research/community-batch932-audit/CONTENT-COVERAGE.json", - "research/community-batch970-audit/CONTENT-COVERAGE.json", - "research/community-frontier741-audit/CONTENT-COVERAGE.json", - "research/community-frontier890-audit/CONTENT-COVERAGE.json", - "research/community-hyperplane599-audit/SOURCE.json", - "research/community-k492-audit/SOURCE.json", - "research/community-reconciliation92-audit/MANIFEST.json", - "research/partial-swap-digest/baseline.py", - "research/r420-two-sided-basis/SOURCES.json", - "research/skip-clones/SOURCE.json", - "research/split-skip/SOURCE.json", - "scripts/historical-ci-inputs/Makefile", - "scripts/historical-ci-inputs/ledger-batch932-run_isolated_tests.py", - "scripts/historical-ci-inputs/ledger-batch932-test_isolated_test_runner.py", - "scripts/historical-ci-inputs/ledger-batch970-verify_selected_result.py", - "scripts/historical-ci-inputs/ledger-frontier741-ci-verification.md", - "scripts/historical-ci-inputs/partial-swap-context.json", - "scripts/historical-ci-inputs/partial-swap-network.json", - "scripts/partial_swap/shared.py", - "scripts/replay_historical_check.py", - "scripts/research_package.py", - "scripts/run_isolated_tests.py", - "scripts/verify_selected_result.py", - "tests/test_isolated_test_runner.py" + "scripts/research_package.py" ], "commands": [ { diff --git a/research/historical-selected-replay-gap/verify.py b/research/historical-selected-replay-gap/verify.py index 83b995941a..9d266c5a4e 100644 --- a/research/historical-selected-replay-gap/verify.py +++ b/research/historical-selected-replay-gap/verify.py @@ -6,8 +6,10 @@ """ import hashlib import importlib.util +import json import subprocess import sys +import tempfile from pathlib import Path ROOT = Path(__file__).resolve().parents[2] @@ -61,31 +63,47 @@ def require(ok, message): raise SystemExit(message) -def load_checker(): - path = ROOT / "scripts/replay_historical_check.py" - spec = importlib.util.spec_from_file_location("historical_selected_replay_gap_checker", path) +def load_module(path): + spec = importlib.util.spec_from_file_location(path.stem, path) module = importlib.util.module_from_spec(spec) spec.loader.exec_module(module) return module +def checkout_snapshot(snapshot, sources, runner, env): + paths = [runner.canonical_relative_path(row["path"]) for row in sources["files"]] + git = ["git", "-c", "maintenance.auto=false", "-c", "gc.auto=0", + "-c", "core.autocrlf=false"] + subprocess.run([*git, "clone", "--quiet", "--shared", "--no-tags", "--no-checkout", + "--", str(ROOT), str(snapshot)], cwd=ROOT, env=env, check=True) + subprocess.run([*git, "update-ref", "--no-deref", "HEAD", INSPECTED], + cwd=snapshot, env=env, check=True) + # The pinned planner reads omitted manifests from the sparse HEAD/index. + patterns = "".join(f"/{path.as_posix()}\n" for path in paths) + subprocess.run([*git, "sparse-checkout", "set", "--no-cone", "--stdin"], + cwd=snapshot, env=env, input=patterns.encode("utf-8"), check=True) + subprocess.run([*git, "read-tree", "-mu", "HEAD"], cwd=snapshot, env=env, check=True) + for path, row in zip(paths, sources["files"], strict=True): + require(hashlib.sha256((snapshot / path).read_bytes()).hexdigest() == row["sha256"], + "historical checkout source digest changed: " + path.as_posix()) + + def entries(checker): for name, config in checker.CONFIG.items(): for entry in [config, *config.get("additional_inputs", [])]: yield name, entry -def reject(checker, entry): +def reject(root, checker, entry): try: - checker.authenticated_input(ROOT, entry) + checker.authenticated_input(root, entry) except ValueError as exc: return str(exc) raise SystemExit("historical input was admitted: " + entry["path"]) -def main(): - require(not sys.flags.optimize, "assertions must stay enabled") - checker = load_checker() +def check_snapshot(root, env): + checker = load_module(root / "scripts/replay_historical_check.py") selected = [entry for name, entry in entries(checker) if name == "tooling-ledger" and entry["path"] == SELECTED_PATH] require(len(selected) == 1, "selected-result checker overlay is not unique") @@ -94,7 +112,7 @@ def main(): require(entry["accepted_live_sha256"] == [SELECTED_ACCEPTED], "accepted selected-checker successors changed") frozen = (checker.INPUTS / entry["input"]).read_bytes() - live = (ROOT / SELECTED_PATH).read_bytes() + live = (root / SELECTED_PATH).read_bytes() require(hashlib.sha256(frozen).hexdigest() == SELECTED_PIN, "frozen selected checker bytes changed") require(hashlib.sha256(live).hexdigest() == SELECTED_LIVE, "live selected checker digest changed") require(SELECTED_LIVE not in (SELECTED_PIN, SELECTED_ACCEPTED), "live checker was already admitted") @@ -102,7 +120,7 @@ def main(): # live successor, not a broken comparison. require(SELECTED_PIN in (SELECTED_PIN, *entry["accepted_live_sha256"]), "pin membership control failed") - require(reject(checker, entry) == REJECTIONS[SELECTED_PATH][1], + require(reject(root, checker, entry) == REJECTIONS[SELECTED_PATH][1], "selected checker rejection text changed") counts = {path: 0 for path in REJECTIONS} @@ -110,7 +128,7 @@ def main(): for _name, item in entries(checker): if item["path"] not in REJECTIONS: continue - message = reject(checker, item) + message = reject(root, checker, item) counts[item["path"]] += 1 messages.setdefault(item["path"], message) for path, (count, message) in REJECTIONS.items(): @@ -118,20 +136,31 @@ def main(): require(messages[path] == message, "rejection text changed for " + path) require(sum(counts.values()) == 19, "rejection total changed") ci = [item for _name, item in entries(checker) if item["path"] == CI_PATH] - require(len(ci) == 1 and hashlib.sha256((ROOT / CI_PATH).read_bytes()).hexdigest() == CI_LIVE, + require(len(ci) == 1 and hashlib.sha256((root / CI_PATH).read_bytes()).hexdigest() == CI_LIVE, "selected CI note digest changed") diff = subprocess.check_output( - ["git", "diff", "--name-only", PARENT, INSPECTED], cwd=ROOT, text=True) + ["git", "diff", "--name-only", PARENT, INSPECTED], cwd=root, env=env, text=True) changed = sorted(name for name in diff.splitlines() if name) require(changed == CHANGED, "inspected commit diff changed") - sys.path.insert(0, str(ROOT / "scripts")) - from research_package import plan_details - details = plan_details(ROOT, set(changed)) + planner = load_module(root / "scripts/research_package.py") + details = planner.plan_details(root, set(changed)) require([row["package"] for row in details] == PLAN_PACKAGES, "helper plan selection changed") matched = {name for row in details for names in row["causes"].values() for name in names} require(sorted(set(changed) - matched) == UNMATCHED, "unmatched plan paths changed") - require(plan_details(ROOT, set()) == [], "empty change set selected a package") + require(planner.plan_details(root, set()) == [], "empty change set selected a package") + + +def main(): + require(not sys.flags.optimize, "assertions must stay enabled") + sources = json.loads(Path(__file__).with_name("SOURCES.json").read_bytes()) + require(sources["base_commit"] == INSPECTED, "historical checkout base changed") + runner = load_module(ROOT / "scripts/research_package.py") + env = runner.git_source_env() + with tempfile.TemporaryDirectory(prefix="historical-selected-replay-") as temporary: + snapshot = Path(temporary) / "snapshot" + checkout_snapshot(snapshot, sources, runner, env) + check_snapshot(snapshot, env) print("PASS_HISTORICAL_SELECTED_REPLAY_GAP") print("selected_checker_live=" + SELECTED_LIVE) print("rejections=19 distinct_paths=7 plan_packages=9")