From 42f8d3a7ee84a5223b794a4b1fdf0753e75990e2 Mon Sep 17 00:00:00 2001 From: ToikY <27568617+ToikY@users.noreply.github.com> Date: Tue, 10 Nov 2026 17:18:25 -0800 Subject: [PATCH 1/2] Bound joint BIT descent replacement and target cover --- .../bit-joint-descent-cover-bound/JOINT.json | 61 ++++++++ .../bit-joint-descent-cover-bound/PROOF.md | 143 ++++++++++++++++++ .../bit-joint-descent-cover-bound/README.md | 60 ++++++++ .../SOURCES.json | 24 +++ .../TARGET-COVER.json | 14 ++ .../bit-joint-descent-cover-bound/TASK.json | 77 ++++++++++ .../TRANSPORT.json | 81 ++++++++++ .../bit-joint-descent-cover-bound/VERIFY.json | 21 +++ .../five_cover.py | 79 ++++++++++ .../bit-joint-descent-cover-bound/joint.py | 27 ++++ .../transport.py | 133 ++++++++++++++++ .../bit-joint-descent-cover-bound/verify.py | 36 +++++ 12 files changed, 756 insertions(+) create mode 100644 research/bit-joint-descent-cover-bound/JOINT.json create mode 100644 research/bit-joint-descent-cover-bound/PROOF.md create mode 100644 research/bit-joint-descent-cover-bound/README.md create mode 100644 research/bit-joint-descent-cover-bound/SOURCES.json create mode 100644 research/bit-joint-descent-cover-bound/TARGET-COVER.json create mode 100644 research/bit-joint-descent-cover-bound/TASK.json create mode 100644 research/bit-joint-descent-cover-bound/TRANSPORT.json create mode 100644 research/bit-joint-descent-cover-bound/VERIFY.json create mode 100644 research/bit-joint-descent-cover-bound/five_cover.py create mode 100644 research/bit-joint-descent-cover-bound/joint.py create mode 100644 research/bit-joint-descent-cover-bound/transport.py create mode 100644 research/bit-joint-descent-cover-bound/verify.py diff --git a/research/bit-joint-descent-cover-bound/JOINT.json b/research/bit-joint-descent-cover-bound/JOINT.json new file mode 100644 index 0000000000..cec5f8af19 --- /dev/null +++ b/research/bit-joint-descent-cover-bound/JOINT.json @@ -0,0 +1,61 @@ +{ + "checked_summary_counts": [ + 1, + 2, + 3, + 4 + ], + "cover_capacities": { + "0": 0, + "1": 1, + "2": 2, + "4": 12, + "6": 30, + "7": 62, + "8": 111 + }, + "lower_multiples": { + "1": 48, + "2": 24, + "4": 4, + "6": 2, + "7": 1, + "8": 1 + }, + "mass_by_count": { + "1": { + "1": 48, + "2": 48, + "4": 16, + "6": 12, + "7": 7, + "8": 8 + }, + "2": { + "1": 49, + "2": 50, + "4": 20, + "6": 18, + "7": 14, + "8": 16 + }, + "3": { + "1": 50, + "2": 52, + "4": 24, + "6": 24, + "7": 21, + "8": 24 + }, + "4": { + "1": 51, + "2": 54, + "4": 28, + "6": 30, + "7": 28, + "8": 32 + } + }, + "minimum_nonzero_weight": 48, + "status": "PASS_JOINT_MONOTONE_DESCENT_BOUND" +} diff --git a/research/bit-joint-descent-cover-bound/PROOF.md b/research/bit-joint-descent-cover-bound/PROOF.md new file mode 100644 index 0000000000..443458de2b --- /dev/null +++ b/research/bit-joint-descent-cover-bound/PROOF.md @@ -0,0 +1,143 @@ +# Owned BIT descents through lower-rank catalogue transports + +The exact selected #7001 native has nine owned rank-seven +descents to chart zero, roles 770 through 778. Each gathers +three source rows and supplies a later fanout to main outputs. +One uncharged descent would exceed the required native gain +of about 1.67 rank-one equivalents. The test retains all +other descents and allows one summary to be rebuilt with +arbitrary timing, XORs and any number of lower-rank existing +catalogue transports in the fixed monotone source flow. + +Project each normalized scalar row onto the first 111 +independent main coordinates. Label those coordinates by +their initial rank-one rational chart lines. Along a public +MOVE the set of contained initial lines can only increase. +An ADD uses a common chart, a SWAP exchanges chart and row, +and owned INIT contributes zero. Thus the main support of +a live row is confined to lines contained in its chart, +modulo the span of the retained owned descents already +introduced at chart zero. No other downward MOVE occurs. +The exact replay checks line-set monotonicity on every +public MOVE. It also checks that the selected summary is +outside the span of all other live chart-zero rows at its +first read, granting the other eight summaries. + +The nine descent rows projected onto the main coordinates +generate 512 distinct codewords. The minimum nonzero weight +is 48. Even granting all other eight descents from the +start, every representative of the selected descent's +coset has weight at least 48. + +The existing rational catalogue contains at most 0, 1, 2, +12 and 30 initial main lines at ranks 0, 1, 2, 4 and 6 +respectively. Those are all available ranks below seven. +An exact integer capacity bound gives at most 30 distinct +lines in a union of charts of total rank at most six. For +`f(r)=r^(1−κ)`, 0<κ<1, the sum of paid powers is at least +the power of the total transported rank. A cheaper +replacement for one rank-seven descent must therefore +use total rank at most six. Its main support modulo the +retained descents can cover only 30 lines, below 48. +This rules out a strict saving by this replacement, even +with any number of asynchronous lower-rank accumulators. + +# Up to four simultaneous descents + +Use the same literal nine projected summary rows, catalogue and +monotone source-flow contract as the one-descent proof. Select k +of the nine summaries and retain the other 9−k. Allow any number +of new catalogue accumulators, arbitrary timing and arbitrary +XOR recovery after their descents. At each new descent the +monotone source-flow invariant confines the row to its source +chart's lines modulo the retained and already completed +descent rows. Subtract a combination of those earlier rows +to get a supported representative. In chronological order +this elimination preserves the span after every descent, so +recovery can use the representatives even when a later +accumulator uses an earlier descended value. + +Order positive-rank new transports from largest to smallest. +The selected k target rows are independent modulo the retained +span. Consider the k recovery coefficient vectors on the new +transports. Some nonzero linear combination of the target rows +has a recovery expression whose coefficients on the k−1 largest +transports vanish, by the dimension of a homogeneous linear +system with k variables and at most k−1 equations. The result +is a nonzero codeword even after adding any retained summaries. +It has weight at least 48. Thus the union of the source supports +of the remaining transports must have capacity at least 48. +Zero-rank transports have no such support and can be omitted. + +Let r be the largest remaining rank, and p=1−κ in (0,1). +Each of the removed k−1 ranks costs at least r^p. The possible +values of r are 1, 2, 4, 6, 7 and 8. Lower bounds for the +remaining cost, in multiples of r^p, are 48, 24, 4, 2, 1 +and 1 respectively: + +- At r=1 or 2, each available chart covers at most its rank. + Thus the sum of remaining ranks is at least 48. +- At r=4, the capacity is at most three times rank. Thus the + sum of remaining ranks is at least 16. In all three cases + use s^p ≥ s r^(p−1) for 0 35−5/3 ≥ 5·7^p−5/3, +using log 34 < 4. Thus R≤33. + +Cancel the four largest transports as in the joint proof. +The tail must cover at least 48 lines. A tail maximum of +rank at most two costs at least 48 total tail rank. A tail +maximum of six needs at least 12 tail rank and four earlier +ranks of at least six, hence R≥36. A tail maximum of seven +or eight gives R≥35. The remaining possibility is rank four. +It needs at least 16 tail rank and four earlier ranks ≥4. +Those earlier ranks must all be four, since a six would +force R≥34. If the tail has at most three rank-four rows, +its capacity is at most 17+8·3=41, using a tail rank budget +of 17 and capacity at most one per rank below four. Thus +the only possible profile is eight rank-four transports and +at most one rank-one transport. + +Cancel any four of the eight rank-four transports. The +remaining four rank-four charts must cover at least 47 lines +because the optional transport contributes at most one. Every +one of the eight charts must contain at least 11 lines. +The union of any pair must contain at least 23. These are +necessary conditions even with free, arbitrarily timed +recovery and unrestricted use of the optional line. + +The exact catalogue contains 70 rank-four charts and 51 +distinct eligible line supports. A depth-first search checks +the pair and four-chart conditions, rejecting paths with too +few remaining charts to reach eight. It exhausts after 59 +visited states, with no eight-set and no unresolved cases. +Thus changing five summaries cannot supply the full required +BIT gap under this fixed catalogue and monotone source flow. +This leaves sub-target savings on five summaries, joint +changes to six through nine, and changed source interfaces +open. diff --git a/research/bit-joint-descent-cover-bound/README.md b/research/bit-joint-descent-cover-bound/README.md new file mode 100644 index 0000000000..baccf555bc --- /dev/null +++ b/research/bit-joint-descent-cover-bound/README.md @@ -0,0 +1,60 @@ +# Joint BIT descent replacement through the fixed catalogue + +**NO VERIFIED GAIN.** On the exact selected paired BIT native word, +replacing any one through four of its nine owned rank-seven summary +descents cannot reduce the paid moment for any 0<κ<1 under the +retained monotone source flow, fixed rational chart catalogue and fixed +remaining summary rows. Arbitrary timing, XOR recovery, reuse of earlier +descended values and any number of new catalogue accumulators are allowed. + +The nine summary projections form a binary [111,9] code of minimum +weight 48. A cheaper single replacement has total rank at most six +and covers at most 30 source lines. For k joint replacements, a recovery +combination eliminates the k−1 largest new transports. The residual +48-line requirement forces paid cost at least k·7^(1−κ) for k≤4. +At the moonshot target, the fixed catalogue also excludes any +five-summary replacement saving at least 5/3 paid units per copy. +The necessary eight-chart cover search exhausted 59 states. +[The proof](PROOF.md) gives both bounds and their scope. + +## Reproduce + +Use CPython 3.12 and a clean checkout. + +```sh +python3.12 -B scripts/research_package.py --package research/bit-joint-descent-cover-bound +``` + +The replay checks every public MOVE for source-support monotonicity, +all rational chart annihilators, all 511 nonzero codewords and the +integer capacity inequalities. Controls reject a duplicate summary +and a corrupted rank-six chart capacity. The only live scientific +input is the existing selected BIT word, declared in VERIFY.json. + +Its compressed SHA-256 is +`51203e7fc75ba10bd3ac3f8e675759f47e13d262bea66b6600d1e515095cad78`, +Git blob `b718d6b2848215ad785022106dfa9f871a3d1c0c`. SOURCES.json +pins its exact canonical path and the task provenance. This package +leaves predecessor files unchanged. [Selected BIT source](../paired-query-only-bit/README.md) + +## Scope, overlap and credit + +The selected word and caller, ordinary BIT saving 0.00385248, +bootstrap and inherited assumptions are retained. The result excludes +this transport route and supplies no new native construction. + +Ali Romman's #5421 supplied the nine owned relation method. +DreamingOfClouds, zxv, CubeJerry and retained authors supplied the +selected native, chain-root caller and E-free paired implementation. +The G20 nine-owned package applies the construction to another word. +This contribution supplies the exact support-code audit and joint +replacement lower bound. Prepared for ToikY with substantial OpenAI +Codex and subagent assistance. Apache-2.0. + +## Open next questions + +The full target gap from joint changes to six through nine summaries +remains open. Test one exact low-rank cover in the quotient by the retained +summaries. A passing cover still needs legal source availability, +arbitrary-input equality, restoration and a full charged invoice. +New nonmonotone source paths or chart spaces require a separate audit. diff --git a/research/bit-joint-descent-cover-bound/SOURCES.json b/research/bit-joint-descent-cover-bound/SOURCES.json new file mode 100644 index 0000000000..d7caabea2b --- /dev/null +++ b/research/bit-joint-descent-cover-bound/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8", + "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/paired-query-only-bit/retained/inputs/BIT-NATIVE-WORD.json.gz", + "usage": "input", + "git_blob": "b718d6b2848215ad785022106dfa9f871a3d1c0c", + "sha256": "51203e7fc75ba10bd3ac3f8e675759f47e13d262bea66b6600d1e515095cad78" + } + ] +} diff --git a/research/bit-joint-descent-cover-bound/TARGET-COVER.json b/research/bit-joint-descent-cover-bound/TARGET-COVER.json new file mode 100644 index 0000000000..01742bf27d --- /dev/null +++ b/research/bit-joint-descent-cover-bound/TARGET-COVER.json @@ -0,0 +1,14 @@ +{ + "cap": 4096, + "capped": false, + "checked_states": 59, + "disjoint_pairs": 591, + "distinct_eligible_supports": 51, + "eligible_charts": 51, + "first_survivor": null, + "minimum_four_chart_cover": 47, + "optional_extra_line": 1, + "rank_four_charts": 70, + "status": "NECESSARY_FIVE_SUMMARY_TARGET_COVER_ONLY", + "word_sha256": "51203e7fc75ba10bd3ac3f8e675759f47e13d262bea66b6600d1e515095cad78" +} diff --git a/research/bit-joint-descent-cover-bound/TASK.json b/research/bit-joint-descent-cover-bound/TASK.json new file mode 100644 index 0000000000..7aa74ed498 --- /dev/null +++ b/research/bit-joint-descent-cover-bound/TASK.json @@ -0,0 +1,77 @@ +{ + "actual_scope": "The exact selected paired BIT native word. Replace any one through four of its nine owned rank-seven descents, retaining all other summary rows, the rational chart catalogue and monotone source flow. Allow arbitrary timing, XORs and any number of new catalogue accumulators. Also test the necessary source-cover condition for any five-summary replacement that could pay the fixed moonshot target gap.", + "ai_assistance": "Substantial OpenAI Codex and three-subagent assistance, including an independently implemented bitset recount.", + "author": "ToikY", + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "bottleneck_link": "The moonshot BIT target needs a real paid-moment reduction. This proves that changing at most four high-rank summary descents in the retained monotone catalogue cannot supply any reduction.", + "budget_minutes": 20, + "evidence": "Exact dimension-nine binary summary code of length111 and minimum weight48; rank6 catalogue unions cover at most30. A recovery-nullspace argument forces at least k*7^(1-kappa) paid moment for k<=4. Exact rank-four cover census excludes five-summary replacements saving at least 5/3 per native copy.", + "open_questions": [ + { + "blocked_by": "The union-capacity relaxation gives only a necessary condition; legal source availability, arbitrary-input equality, restoration and the full paid bill must still be proved.", + "first_step": "Form the quotient by the retained summary span and test one rank-four-chart cover profile against exact column recoverability.", + "question": "Can at least six summary descents be redesigned jointly to fund the BIT target?", + "why_it_matters": "The target-budget exclusion leaves the six-through-nine-summary domain open." + } + ], + "original_card": { + "acceptance_gate": "A full boundary contract and paid profile; unchanged scalar counts alone are insufficient. 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": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "existing_checks": [ + { + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "status": "reviewed" + } + ], + "first_experiment": "First read #5679/#5708 and their audits as pending component proposals. Choose one uncovered helper group/cut on an exact word; compare arbitrary-input native action, targets, owned storage, both orientations and full signed bill. Stop if the gain is only a scalar count or repaid by lost targets. Do not rerun the frozen #5609 common-frame domain without changing its hypothesis.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "id": "bit-helper-contract", + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "overlap_terms": [ + "G20", + "helper split", + "5679", + "5708", + "independent target" + ], + "question": "Can a changed G20 helper path or independent-target split improve the complete BIT moment without losing its physical endpoint?", + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "research/g20-helper-split/README.md", + "research/g20-conjugation-admission/README.md" + ] + }, + "outcome": "negative-result", + "priority_revision": 8, + "schema_version": 1, + "scope_change_reason": "Derive a source-specific necessary support condition before searching for a cheaper native transport.", + "scope_status": "refined", + "stop_rule": "Exhaust the 511 nonzero summary combinations and all catalogue chart capacities, then prove the recovery-coefficient lower bound for k=1,2,3,4. Stop the five-summary cover after 4096 states or exhaustion.", + "task_id": "bit-helper-contract" +} diff --git a/research/bit-joint-descent-cover-bound/TRANSPORT.json b/research/bit-joint-descent-cover-bound/TRANSPORT.json new file mode 100644 index 0000000000..4962cec78d --- /dev/null +++ b/research/bit-joint-descent-cover-bound/TRANSPORT.json @@ -0,0 +1,81 @@ +{ + "first_use": { + "770": { + "available_rank": 117, + "event": 32938 + }, + "771": { + "available_rank": 118, + "event": 32931 + }, + "772": { + "available_rank": 118, + "event": 32932 + }, + "773": { + "available_rank": 117, + "event": 32941 + }, + "774": { + "available_rank": 119, + "event": 32922 + }, + "775": { + "available_rank": 119, + "event": 32923 + }, + "776": { + "available_rank": 119, + "event": 32924 + }, + "777": { + "available_rank": 119, + "event": 32925 + }, + "778": { + "available_rank": 119, + "event": 32926 + } + }, + "max_catalogue_lines_by_rank": { + "0": 0, + "1": 1, + "2": 2, + "4": 12, + "6": 30, + "7": 62, + "8": 111 + }, + "minimum_nonzero_weight": 48, + "nonzero_summary_code_weights": { + "48": 4, + "49": 12, + "50": 32, + "51": 50, + "52": 76, + "53": 52, + "54": 24, + "55": 5, + "56": 5, + "57": 24, + "58": 52, + "59": 76, + "60": 50, + "61": 32, + "62": 12, + "63": 4, + "111": 1 + }, + "public_monotone_moves": 2862, + "status": "PASS_OWNED_DESCENT_TRANSPORT_BOUND", + "total_rank_capacities": [ + 0, + 1, + 2, + 3, + 12, + 13, + 30 + ], + "word_sha256": "51203e7fc75ba10bd3ac3f8e675759f47e13d262bea66b6600d1e515095cad78" +} diff --git a/research/bit-joint-descent-cover-bound/VERIFY.json b/research/bit-joint-descent-cover-bound/VERIFY.json new file mode 100644 index 0000000000..886046dc97 --- /dev/null +++ b/research/bit-joint-descent-cover-bound/VERIFY.json @@ -0,0 +1,21 @@ +{ + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "checks": "Authenticate the exact word; verify rational chart annihilators, every monotone source MOVE and owned descent; enumerate all511 nonzero codewords; prove the k<=4 integer support bound; reject duplicate summaries and corrupt chart capacity. Exhaust the necessary rank-four cover for the five-summary target-budget profile.", + "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-joint-descent-cover-bound/five_cover.py b/research/bit-joint-descent-cover-bound/five_cover.py new file mode 100644 index 0000000000..9b23b9a685 --- /dev/null +++ b/research/bit-joint-descent-cover-bound/five_cover.py @@ -0,0 +1,79 @@ +"""Necessary disjoint source-line packing for the eight rank-four profile.""" +import argparse +from fractions import Fraction +import gzip +from hashlib import sha256 +from itertools import combinations +import json +from pathlib import Path + +CAP = 4096 +PIN = "51203e7fc75ba10bd3ac3f8e675759f47e13d262bea66b6600d1e515095cad78" + + +def scan(path, extra_line=False): + raw = path.read_bytes() + assert sha256(raw).hexdigest() == PIN + word = json.loads(gzip.decompress(raw)) + frames = word["frames"] + lines = [tuple(map(Fraction, frames[str(i)]["B"][0])) for i in word["start"][:111]] + groups = {} + count = 0 + for chart, frame in frames.items(): + if frame["dim"] != 4: + continue + count += 1 + annihilator = [tuple(map(Fraction, row)) for row in frame["A"]] + support = sum(1 << i for i, line in enumerate(lines) + if all(not sum(x * y for x, y in zip(line, row, strict=True)) for row in annihilator)) + assert support.bit_count() <= 12 + if support.bit_count() >= 12 - int(extra_line): + groups.setdefault(support, []).append(int(chart)) + masks = list(groups) + states = 0 + stopped = False + + def choose(chosen, remaining): + nonlocal states, stopped + if len(chosen) == 8: + return chosen + if len(chosen) + len(remaining) < 8: + return None + if states >= CAP: + stopped = True + return None + states += 1 + for i, mask in enumerate(remaining): + if extra_line: + if any((a | b | c | mask).bit_count() < 47 for a, b, c in combinations(chosen, 3)): + continue + others = [other for other in remaining[i + 1:] if (mask | other).bit_count() >= 23] + else: + others = [other for other in remaining[i + 1:] if not (mask & other)] + found = choose([*chosen, mask], others) + if found is not None or stopped: + return found + return None + + found = choose([], masks) + result = dict(status="NECESSARY_DISJOINT_COVER_ONLY", rank_four_charts=count, + maximal_charts=sum(map(len, groups.values())), distinct_maximal_supports=len(masks), + disjoint_pairs=sum(not (a & b) for i, a in enumerate(masks) for b in masks[i + 1:]), + checked_states=states, cap=CAP, capped=stopped, + first_survivor=None if found is None else [groups[mask] for mask in found], + word_sha256=PIN) + if extra_line: + result.update(status="NECESSARY_FIVE_SUMMARY_TARGET_COVER_ONLY", optional_extra_line=1, + minimum_four_chart_cover=47) + result["eligible_charts"] = result.pop("maximal_charts") + result["distinct_eligible_supports"] = result.pop("distinct_maximal_supports") + return result + + +if __name__ == "__main__": + if not __debug__: + raise RuntimeError("Use assertions") + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("path", type=Path) + parser.add_argument("--extra-line", action="store_true") + print(json.dumps(scan(**vars(parser.parse_args())), indent=2, sort_keys=True)) diff --git a/research/bit-joint-descent-cover-bound/joint.py b/research/bit-joint-descent-cover-bound/joint.py new file mode 100644 index 0000000000..14a09667e0 --- /dev/null +++ b/research/bit-joint-descent-cover-bound/joint.py @@ -0,0 +1,27 @@ +"""Check integer premises of the k-summary descent cost bound.""" +import json +from pathlib import Path +import sys + + +def check(transport): + assert transport["minimum_nonzero_weight"] == 48 + capacities = {int(rank): count for rank, count in transport["max_catalogue_lines_by_rank"].items()} + assert capacities == {0: 0, 1: 1, 2: 2, 4: 12, 6: 30, 7: 62, 8: 111} + assert all(capacities[r] <= r for r in (1, 2)) + assert all(capacities[r] <= 3 * r for r in (1, 2, 4)) + lower_multiples = {1: 48, 2: 24, 4: 4, 6: 2, 7: 1, 8: 1} + mass = {} + for k in range(1, 5): + mass[k] = {r: (k - 1 + b) * r for r, b in lower_multiples.items()} + assert all(v >= 7 * k for v in mass[k].values()) + assert (5 - 1 + lower_multiples[4]) * 4 < 7 * 5 + return dict(status="PASS_JOINT_MONOTONE_DESCENT_BOUND", + checked_summary_counts=[1, 2, 3, 4], cover_capacities=capacities, + minimum_nonzero_weight=48, lower_multiples=lower_multiples, mass_by_count=mass) + + +if __name__ == "__main__": + if not __debug__: + raise RuntimeError("Use assertions") + print(json.dumps(check(json.loads(Path(sys.argv[1]).read_bytes())), sort_keys=True, indent=2)) diff --git a/research/bit-joint-descent-cover-bound/transport.py b/research/bit-joint-descent-cover-bound/transport.py new file mode 100644 index 0000000000..a94db1bc18 --- /dev/null +++ b/research/bit-joint-descent-cover-bound/transport.py @@ -0,0 +1,133 @@ +"""Exact support and span checks for the selected BIT owned descents.""" +from collections import Counter +from fractions import Fraction as Q +from hashlib import sha256 +from pathlib import Path +import gzip +import json +import sys + +PIN = '51203e7fc75ba10bd3ac3f8e675759f47e13d262bea66b6600d1e515095cad78' + + +def basis(values): + out = {} + for value in values: + while value: + pivot = value.bit_length() - 1 + if pivot not in out: + out[pivot] = value + break + value ^= out[pivot] + return out + + +def residue(value, pivots): + while value and value.bit_length() - 1 in pivots: + value ^= pivots[value.bit_length() - 1] + return value + + +def rational_rank(matrix): + rows = [list(map(Q, row)) for row in matrix] + rank = 0 + for column in range(8): + pivot = next((i for i in range(rank, len(rows)) if rows[i][column]), None) + if pivot is None: + continue + rows[rank], rows[pivot] = rows[pivot], rows[rank] + scale = rows[rank][column] + rows[rank] = [x / scale for x in rows[rank]] + for i in range(len(rows)): + if i != rank and rows[i][column]: + scale = rows[i][column] + rows[i] = [x - scale * y for x, y in zip(rows[i], rows[rank], strict=True)] + rank += 1 + return rank + + +def main(path): + raw = path.read_bytes() + assert sha256(raw).hexdigest() == PIN + word = json.loads(gzip.decompress(raw)) + n = word['public'] + frames = {int(i): frame for i, frame in word['frames'].items()} + lines = [tuple(map(Q, frames[f]['B'][0])) for f in word['start'][:111]] + assert len(set(word['start'][:111])) == 111 + allowed = {} + maxima = Counter() + for f, frame in frames.items(): + annihilator = [tuple(map(Q, row)) for row in frame['A']] + subspace = [tuple(map(Q, row)) for row in frame['B']] + assert len(subspace) == rational_rank(subspace) == frame['dim'] + assert len(annihilator) == rational_rank(annihilator) == 8 - frame['dim'] + assert all(sum(x*y for x,y in zip(a,b,strict=True)) == 0 + for a in annihilator for b in subspace) + mask = sum(1 << i for i, line in enumerate(lines) + if all(sum(x*y for x,y in zip(line, row)) == 0 for row in annihilator)) + allowed[f] = mask + maxima[frame['dim']] = max(maxima[frame['dim']], mask.bit_count()) + assert maxima == {0: 0, 1: 1, 2: 2, 4: 12, 6: 30, 7: 62, 8: 111} + capacities = [0] + for cap in range(1, 7): + capacities.append(max(capacities[cap-d]+maximum for d,maximum in maxima.items() if 0 capacities[-1] + print(json.dumps(dict(status='PASS_OWNED_DESCENT_TRANSPORT_BOUND', word_sha256=PIN, + public_monotone_moves=public_moves, first_use=first_use, + max_catalogue_lines_by_rank=maxima, total_rank_capacities=capacities, + nonzero_summary_code_weights=weights, minimum_nonzero_weight=48), + sort_keys=True, indent=2)) + + +if __name__ == '__main__': + main(Path(sys.argv[1])) diff --git a/research/bit-joint-descent-cover-bound/verify.py b/research/bit-joint-descent-cover-bound/verify.py new file mode 100644 index 0000000000..aab189ba7a --- /dev/null +++ b/research/bit-joint-descent-cover-bound/verify.py @@ -0,0 +1,36 @@ +"""Read-only replay of the fixed-catalogue joint BIT descent bound.""" +import contextlib +import io +import json +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent +SOURCE = "research/paired-query-only-bit/retained/inputs/BIT-NATIVE-WORD.json.gz" +sys.path.insert(0, str(HERE)) +import five_cover +import joint +import transport + +if not __debug__: + raise RuntimeError("Run with assertions enabled") +root = HERE.parents[1] +out = io.StringIO() +with contextlib.redirect_stdout(out): + transport.main(root / SOURCE) +assert out.getvalue() == (HERE / "TRANSPORT.json").read_text(), "Literal rows, code and catalogue receipt" +receipt = json.loads(out.getvalue()) +result = joint.check(receipt) +assert json.dumps(result, sort_keys=True, indent=2) + "\n" == (HERE / "JOINT.json").read_text() +bad = json.loads(out.getvalue()) +bad["max_catalogue_lines_by_rank"]["6"] = 48 +try: + joint.check(bad) +except AssertionError: + pass +else: + raise AssertionError("Corrupt chart capacity accepted") +target = five_cover.scan(root / SOURCE, extra_line=True) +assert not target["capped"] and target["first_survivor"] is None +assert json.dumps(target, sort_keys=True, indent=2) + "\n" == (HERE / "TARGET-COVER.json").read_text() +print("PASS_JOINT_MONOTONE_BIT_DESCENT_BOUND k=1..4 plus k=5 target exclusion") From cd0d2c277f415316d98ff1689b966232f43d8c2f Mon Sep 17 00:00:00 2001 From: ToikY <27568617+ToikY@users.noreply.github.com> Date: Wed, 11 Nov 2026 16:15:15 -0800 Subject: [PATCH 2/2] Reuse the selected CI guide and historical replay repair Reuse bb36fc65ee0b161229169505f4840c436c5ca2b9 and d2e54af81f9dda6487636b79d4964a2385d89b2b from #7257, also verified in #7339. The current guide follows selected #7000/#7001 and the historical audit checks its inspected snapshot. Credit to Rohan Arun and the #7147/#7156 source authors for navigation, unpaidmoon for the audit, Dennis for the historical gate, and Matarener for the pinned snapshot precedent. --- docs/ci-verification.md | 19 +++++- .../historical-selected-replay-gap/README.md | 6 +- .../SOURCES.json | 60 +++++++++--------- .../VERIFY.json | 31 +-------- .../historical-selected-replay-gap/verify.py | 63 ++++++++++++++----- 5 files changed, 100 insertions(+), 79 deletions(-) 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/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")