From a3352606f71a97ab3a707ee6c5173df6345c5f38 Mon Sep 17 00:00:00 2001 From: ToikY <27568617+ToikY@users.noreply.github.com> Date: Tue, 10 Nov 2026 20:01:02 -0800 Subject: [PATCH 1/2] Bound BIT sender fusion at owned recipients Co-authored-by: OpenAI Codex --- research/bit-send-cochart-gate/PROOF.md | 58 +++++++ research/bit-send-cochart-gate/README.md | 45 ++++++ research/bit-send-cochart-gate/RECEIPT.json | 23 +++ research/bit-send-cochart-gate/SOURCES.json | 24 +++ research/bit-send-cochart-gate/TASK.json | 77 +++++++++ research/bit-send-cochart-gate/VERIFY.json | 14 ++ research/bit-send-cochart-gate/verify.py | 165 ++++++++++++++++++++ 7 files changed, 406 insertions(+) create mode 100644 research/bit-send-cochart-gate/PROOF.md create mode 100644 research/bit-send-cochart-gate/README.md create mode 100644 research/bit-send-cochart-gate/RECEIPT.json create mode 100644 research/bit-send-cochart-gate/SOURCES.json create mode 100644 research/bit-send-cochart-gate/TASK.json create mode 100644 research/bit-send-cochart-gate/VERIFY.json create mode 100644 research/bit-send-cochart-gate/verify.py diff --git a/research/bit-send-cochart-gate/PROOF.md b/research/bit-send-cochart-gate/PROOF.md new file mode 100644 index 0000000000..baa869c84e --- /dev/null +++ b/research/bit-send-cochart-gate/PROOF.md @@ -0,0 +1,58 @@ +# Exact sender support and chronology exclusions + +Replay the literal selected #7001 word over 659 independent binary input +rows. ADD applies XOR in its declared common chart. SWAP exchanges rows and +charts, MOVE changes the chart, and INIT and CLEAR use the retained owned +allocation and erasure semantics. The complete final chart vector and all +arbitrary-input public rows match the selected interface. This proof uses +the necessary chart and linear-row contracts of that replay. + +## Fixed recipient route + +There are 360 consecutive public-sender contact triples `MOVE F→H`, +`ADD A→B`, `MOVE H→G`, with ranks `(6,7,8)` and nonzero cargo. A direct +`F→G` can expose the sender only on its endpoint charts in the isolated +window. The 120 original recipients B are owned. The verifier checks their +entire literal lifetimes. Their chart ranks are seven and, for nine summary +owners, zero. Neither sender endpoint can be cocharted with B, even if every +recipient contact barrier is waived and the fused MOVE may occur anywhere +in the sender's contact gap. Correcting XORs across a recipient observation +do not change this missing chart. + +## Rebind the owned chart + +Each owner has three incoming sends on the same middle chart. If all three +senders use their early endpoints, the new owner requires a common rational +rank-six subspace. Exact annihilator tests reject all 120 groups. If the +owner uses the common late chart, all three senders can supply full-rank +rows in the relaxed timing model. For 111 owners, the one original consumer +never occupies any rank-eight chart in its whole trajectory. Its unchanged +route therefore cannot consume the full-rank owner by a direct ADD. + +The other nine owners descend to chart zero before their first read. Their +old descent has rank seven. A full-rank rebind changes its rank to eight. +Put p=1−κ. Three rank-one pairs replaced by three rank-two MOVEs save +`3(2−2^p) < 6κ`. By integration, the added descent cost +`8^p−7^p` is at least `p·8^(−κ) ≥ (1−κ)/8`. At the exact target κ the latter +bound exceeds `6κ`. All nine late rebinds lose before any additional costs. +This scope keeps the original one consumer or one descent per owner. + +## Keep the owned chart and replace sender rows + +For each owner, keep its rank-seven chart and its original first output +barrier, which is the sole outgoing rank-seven ADD or the summary descent. +Choose a nonempty subset of its three input senders to fuse. For each +chosen sender, remove its original transient rank-seven availability from +the first MOVE through the second. Leave other old rows intact. Grant free +XOR access to the union of every other literal row in the owner's chart +from INIT through the output barrier, including other valid appearances of +a chosen sender outside its removed interval. The owner itself starts zero. +Even with arbitrary copies, its additional row contribution must lie in +this granted span. The old unselected inputs are kept, so the extra target +is the XOR of exactly the chosen source rows. + +Exact elimination excludes all 840 nonempty subsets, with zero unresolved +cases. All 840 controls pass when the removed source rows are restored to +the pool. The full receiver-window union deliberately overgrants simultaneous +availability and erasure. The conclusion does not cover altered producer +rows or alternative routes for the original public consumers. diff --git a/research/bit-send-cochart-gate/README.md b/research/bit-send-cochart-gate/README.md new file mode 100644 index 0000000000..1252ea2351 --- /dev/null +++ b/research/bit-send-cochart-gate/README.md @@ -0,0 +1,45 @@ +# BIT sender fusion at owned recipients + +**NO VERIFIED GAIN.** On the exact selected #7001 word, 360 consecutive +public sender triples have a rank-six to rank-seven MOVE, one outgoing ADD, +and a rank-seven to rank-eight MOVE. Their 120 owned recipients never occupy +either outer rank in the literal trajectory. Retiming across a recipient read +cannot supply the missing cochart. + +Rebinding all three sends to one owned chart also fails the tested gates. +The early spaces differ. Of the late cases, 111 unchanged consumers never +reach full rank and nine summaries lose paid price. At the original +rank-seven chart, no nonempty subset of sender rows can be replaced by +other retained rows, even with a free union of donor rows over the entire +window. [Proof](PROOF.md) · [Exact receipt](RECEIPT.json) + +## Replay + +From a clean checkout, use CPython 3.12 with assertions enabled. + +```sh +python3.12 -B scripts/research_package.py --package research/bit-send-cochart-gate +``` + +The verifier reconstructs all 659 arbitrary-input endpoint rows, exact +charts, owned lifetimes and sender triples. It checks all 120 group gates +and 840 alias subsets. Both the retained word and canonical task card are +source-pinned. + +## Scope and credit + +[#7157](https://github.com/CrocSwap/integer-mult-bounds/pull/7157) fixes +the source rows for two public carriers of summary 770. This package tests +all literal one-ADD sends into owned rank-seven recipients and their +recovery before the next use. Credit Ali Romman's #5421 for owned summary +relations, and DreamingOfClouds, zxv, CubeJerry and the retained authors for +the #6834/#7001 native and paired-controller sources. Substantial OpenAI +Codex and subagent assistance. Apache-2.0. + +## Open next questions + +Can a coupled prefix rewrite supply a new live receiver row? Start with two +paid source arrivals and check the exact displaced destination rows jointly. +Any replacement needs the same arbitrary-input public endpoints, restored +ownership and a complete paid bill. A changed producer prefix or receiver +operator is outside the three tested scopes. diff --git a/research/bit-send-cochart-gate/RECEIPT.json b/research/bit-send-cochart-gate/RECEIPT.json new file mode 100644 index 0000000000..71f819f505 --- /dev/null +++ b/research/bit-send-cochart-gate/RECEIPT.json @@ -0,0 +1,23 @@ +{ + "alias_hits": 0, + "alias_positive_controls": 840, + "alias_subsets": { + "1": 360, + "2": 360, + "3": 120 + }, + "dependencies": { + "research/paired-query-only-bit/retained/inputs/BIT-NATIVE-WORD.json.gz": "51203e7fc75ba10bd3ac3f8e675759f47e13d262bea66b6600d1e515095cad78" + }, + "fixed_route_hits": 0, + "owned_recipients": 120, + "public_endpoint_rows": 659, + "rebind": { + "early_spaces_incompatible": 120, + "late_consumer_never_full": 111, + "late_summary_descent": 9 + }, + "sender_triples": 360, + "status": "PASS_BIT_SEND_COCHART_GATE", + "target": "10018846261809/2500000000000000" +} diff --git a/research/bit-send-cochart-gate/SOURCES.json b/research/bit-send-cochart-gate/SOURCES.json new file mode 100644 index 0000000000..d7caabea2b --- /dev/null +++ b/research/bit-send-cochart-gate/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-send-cochart-gate/TASK.json b/research/bit-send-cochart-gate/TASK.json new file mode 100644 index 0000000000..cdaf3b8fca --- /dev/null +++ b/research/bit-send-cochart-gate/TASK.json @@ -0,0 +1,77 @@ +{ + "actual_scope": "The exact #7001 360 outgoing-ADD sender triples, 120 owned receiver rebinds and all 840 nonempty sender subsets under fixed first output and granted rank-seven aliases.", + "ai_assistance": "Substantial OpenAI Codex and subagent assistance, including independent chart and row checks.", + "author": "ToikY", + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "bottleneck_link": "The optimistic one-ADD price requires real cocharted recipient support. These three exact necessary gates exclude the tested sender fusions.", + "budget_minutes": 20, + "evidence": "360 fixed-route sends, 120 full-group rebinds and 840 existing-row alias subsets exhausted. Exact 659 input-row endpoints and 840 restored-source controls pass.", + "open_questions": [ + { + "blocked_by": "Exact live rows, compatible arrival clocks, endpoint restoration, and fully charged price remain open.", + "first_step": "Pin two paid arrivals and solve the two displaced destination rows against the retained same-chart basis.", + "question": "Can a coupled prefix rewrite supply a new live receiver row?", + "why_it_matters": "A changed producer can provide a direction unavailable in the original cochart span." + } + ], + "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": "Investigate actual sender-to-owned receiver routes after the fixed two-carrier source-pool exclusion.", + "scope_status": "refined", + "stop_rule": "Exhaust 360 fixed-route sends, 120 complete rebinds and 840 nonempty subsets. Use exact necessary support and directed or rigorous analytic price. Stop before a literal build if none survives.", + "task_id": "bit-helper-contract" +} diff --git a/research/bit-send-cochart-gate/VERIFY.json b/research/bit-send-cochart-gate/VERIFY.json new file mode 100644 index 0000000000..2a37fc1b75 --- /dev/null +++ b/research/bit-send-cochart-gate/VERIFY.json @@ -0,0 +1,14 @@ +{ + "commands": [ + { + "argv": ["{python}", "-I", "-B", "{package}/verify.py"], + "checks": "Authenticate the selected word, check all arbitrary public rows and owned charts, exhaust the fixed recipient and rebind gates, and test all 840 exact sender subsets against the granted cochart span.", + "timeout_seconds": 30 + } + ], + "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-send-cochart-gate/verify.py b/research/bit-send-cochart-gate/verify.py new file mode 100644 index 0000000000..e2ccdf5edb --- /dev/null +++ b/research/bit-send-cochart-gate/verify.py @@ -0,0 +1,165 @@ +"""Exact cochart and source-row gates for the selected BIT sends.""" +from collections import Counter, defaultdict +from fractions import Fraction +from hashlib import sha256 +from itertools import combinations +import gzip +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +SOURCE = 'research/paired-query-only-bit/retained/inputs/BIT-NATIVE-WORD.json.gz' +PIN = '51203e7fc75ba10bd3ac3f8e675759f47e13d262bea66b6600d1e515095cad78' +TARGET = Fraction('0.0040075385047236') + + +def xor_rows(rows): + total = 0 + for row in rows: + total ^= row + return total + + +def in_span(values, target): + basis = {} + for row in values: + while row: + lead = row & -row + if lead not in basis: + basis[lead] = row + break + row ^= basis[lead] + while target: + lead = target & -target + if lead not in basis: + return False + target ^= basis[lead] + return True + + +def trace(word): + n = word['public'] + current = [(f,1 << r) for r,f in enumerate(word['start'])] + [None]*word['owned_fields'] + begins = [0]*len(current) + spans, touch = defaultdict(list), defaultdict(list) + moves = {} + charts = defaultdict(set) + + def set_role(role, state, cut): + old = current[role] + if old is not None: + spans[old[0]].append((begins[role],cut,role,old[1])) + charts[role].add(old[0]) + current[role] = state + begins[role] = cut + + for i, (op,a,*args) in enumerate(word['program']): + touch[a].append(i) + if op == 'ADD': + b,f = args + assert a != b and current[a][0] == current[b][0] == f + touch[b].append(i) + set_role(a,(f,current[a][1] ^ current[b][1]),i+1) + elif op == 'MOVE': + f,g = args + assert current[a][0] == f + row = current[a][1] + if a < n: + moves[i] = (a,f,g,row) + set_role(a,(g,row),i+1) + elif op == 'SWAP': + b = args[0] + touch[b].append(i) + x,y = current[a],current[b] + set_role(a,y,i+1) + set_role(b,x,i+1) + elif op == 'INIT': + assert a >= n and current[a] is None + set_role(a,(args[0],0),i+1) + else: + assert op == 'CLEAR' and a >= n and current[a][0] == args[0] + set_role(a,None,i+1) + assert n == 659 and len(moves) == 2862 + assert [c[0] for c in current[:n]] == word['final'] and not any(current[n:]) + for i,(_,row) in enumerate(current[:n]): + expected = (1 << i) ^ ((1 << (i-111)) if 111 <= i < 222 else 0) + assert row == expected + set_role(i,None,len(word['program'])+1) + return spans,touch,moves,charts + + +def verify(path): + raw = path.read_bytes() + assert sha256(raw).hexdigest() == PIN + word = json.loads(gzip.decompress(raw)) + frames = {int(label):frame for label,frame in word['frames'].items()} + dims = {label:frame['dim'] for label,frame in frames.items()} + spans,touch,moves,charts = trace(word) + p = word['program'] + groups = defaultdict(list) + for owner,times in touch.items(): + if owner >= word['public']: + continue + for i,t,j in zip(times,times[1:],times[2:]): + if i not in moves or j not in moves or p[t][0] != 'ADD' or p[t][2] != owner: + continue + a,f,h,row = moves[i] + aa,hh,g,after = moves[j] + b = p[t][1] + assert a == aa == owner and h == hh == p[t][3] and row == after and row + assert (dims[f],dims[h],dims[g]) == (6,7,8) and g == 1 and b >= word['public'] + assert all(dims[c] in (0,7) for c in charts[b]) + groups[b].append((t,i,j,owner,f,h,g,row)) + assert len(groups) == 120 and {len(v) for v in groups.values()} == {3} + assert len({move[3] for group in groups.values() for move in group}) == 360 + def same_space(a,b): + assert dims[a] == dims[b] + return all(sum(Fraction(x)*Fraction(y) for x,y in zip(ann,vec,strict=True)) == 0 + for ann in frames[a]['A'] for vec in frames[b]['B']) + counts = Counter() + subsets = Counter() + for b, group in sorted(groups.items()): + group.sort() + h, = {v[5] for v in group} + init,*writes,deadline = touch[b][:5] + assert p[init] == ['INIT',b,h] and writes == [v[0] for v in group] + assert not all(same_space(group[0][4],v[4]) for v in group[1:]) + counts['early_spaces_incompatible'] += 1 + if p[deadline][0] == 'MOVE': + assert p[deadline] == ['MOVE',b,h,0] + counts['late_summary_descent'] += 1 + else: + _,c,s,frame = p[deadline] + assert p[deadline][0] == 'ADD' and s == b and frame == h + assert len(touch[b]) == 6 and all(dims[k] != 8 for k in charts[c]) + counts['late_consumer_never_full'] += 1 + pool = [(max(lo,init+1),min(hi,deadline+1),r,row) for lo,hi,r,row in spans[h] + if r != b and lo <= deadline and hi > init+1] + for n in range(1,4): + for choice in combinations(group,n): + release = {r:(i+1,j+1) for _,i,j,r,*_ in choice} + donors = [row for lo,hi,r,row in pool + if r not in release or lo < release[r][0] or hi > release[r][1]] + cargo = [v[-1] for v in choice] + target = xor_rows(cargo) + assert target and not in_span(donors,target) + assert in_span([*donors,*cargo],target) + subsets[n] += 1 + assert counts == {'early_spaces_incompatible':120,'late_summary_descent':9,'late_consumer_never_full':111} + assert subsets == {1:360,2:360,3:120} + # Three (1,1)->2 fusions save less than 6*kappa, while the late + # owned rank 8->0 descent costs at least (1-kappa)/8 more. + assert 6*TARGET < (1-TARGET)/8 and 0 < TARGET < 1 + assert in_span([0b110,0b011],0b101) and not in_span([0b110,0b011],0b100) + return dict(status='PASS_BIT_SEND_COCHART_GATE', public_endpoint_rows=word['public'], + sender_triples=360, owned_recipients=120, fixed_route_hits=0, + rebind=counts, alias_subsets=subsets, alias_positive_controls=840, + alias_hits=0, target=str(TARGET),dependencies={SOURCE:PIN}) + + +if __name__ == '__main__': + if not __debug__: + raise RuntimeError('Use assertions') + result = verify(HERE.parents[1]/SOURCE) + assert json.dumps(result,indent=2,sort_keys=True)+'\n' == (HERE/'RECEIPT.json').read_text() + print(result['status']) From 7781c0426949f39590c39ee5ba15fbdb72a762d6 Mon Sep 17 00:00:00 2001 From: ToikY <27568617+ToikY@users.noreply.github.com> Date: Wed, 11 Nov 2026 16:14:59 -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")