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-single-role-idle-rank-bound/NOTICE b/research/bit-single-role-idle-rank-bound/NOTICE new file mode 100644 index 0000000000..324d78df13 --- /dev/null +++ b/research/bit-single-role-idle-rank-bound/NOTICE @@ -0,0 +1,5 @@ +Apache-2.0. +Retained #7001 paired BIT caller and invoice and #6726 native word. +Credit #6834 and #6980 for the caller lineage, and #7163, #7190 and #7201 +for related native volume and same-mask packing bounds. +OpenAI Codex and subagents materially assisted. diff --git a/research/bit-single-role-idle-rank-bound/PRIMARY.json b/research/bit-single-role-idle-rank-bound/PRIMARY.json new file mode 100644 index 0000000000..89fd5d5ba3 --- /dev/null +++ b/research/bit-single-role-idle-rank-bound/PRIMARY.json @@ -0,0 +1,32 @@ +{ + "caller_sha256": "757b3523798f840bdb02028b23708c3416627a99ea09e7a3c4bcdc5cd0c7ce4b", + "disjoint_scope": 256, + "field_polynomial": "0x11b", + "physical_sites": 0, + "q": 1, + "rank_counts": { + "2": 256 + }, + "stage_probe": [ + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 11, + 12, + 13, + 14, + 15, + 16, + 17, + 18, + 19 + ], + "unresolved": [], + "unvisited": 0 +} diff --git a/research/bit-single-role-idle-rank-bound/README.md b/research/bit-single-role-idle-rank-bound/README.md new file mode 100644 index 0000000000..3e3336ec41 --- /dev/null +++ b/research/bit-single-role-idle-rank-bound/README.md @@ -0,0 +1,85 @@ +# Arbitrary-slot single-role BIT idle fusion + +**NO VERIFIED GAIN. Conditional κ change 0%.** On the exact #7001 +paired E-free caller, every pair of disjoint-mask IDLE_ONE events +requires a rank-two correction after deletion. One one-role idle +changes the scalar operator by rank at most one, at any clock. +The complete 256-pair scope has zero compatible savings. The +fixed target κ = 0.0040075385047236 remains short by about +60.10389921914735 raw units. #7277 at κ = 0.003645669928698 remains +the complete comparable witness. + +## Rank certificate + +Fix one 38-role port group and specialize the formal caller at +q=1 and nonzero body symbols in a finite extension of F₂. Write +the operator around two idle events as L D_j M D_i R, with M +the intervening word and L,R the unchanged outer words. Deleting +both idles leaves L M R. The difference after inserting one +one-role diagonal idle anywhere in the deleted word is of the +form A(D−I)B. Its rank is at most one at every specialization. + +For original idle factors D_i = I + α e_r e_r^T and +D_j = I + β e_s e_s^T, take off-axis entries +l = (M e_r)_u ≠ 0 with u ≠ s and +h = (e_s^T M)_v ≠ 0 with v ≠ r. The inner difference +D_j M D_i − M on rows (u,s) and columns (r,v) has determinant +αβlh. All 256 disjoint pairs have such a nonzero minor in +GF(128), with nonzero idle corrections. The outside factors +L,R are invertible at the probe because each stage scalar is +nonzero and every remaining shear or swap is invertible. +The exact symbolic equality required by a replacement would +survive this specialization. A direct whole-operator replay +over a different GF(256) specialization also finds rank two +for all 256 pairs. + +The disjoint stock is exhaustive within this scope. The 240 +overlapping-mask pairs, additional ordinary edits, changes to +other caller factors, and a genuinely multi-role child are +outside it. No physical site is tested. + +## Whole signed price + +There are 32 literal IDLE_ONE events, each repeated over 111 +port groups, giving 444 paid jobs at each rank 7,14,…,56. +Write H(r)=r^(1−κ). Concavity gives +H(a+b) ≥ H(2)(H(a)+H(b))/2. Even granting every compatible +rank-additive pair free setup and routing, the disjoint-pair +saving upper is about 305.93670924546 before support. The rank +obstruction then reduces the declared stock upper to exactly +zero. The independent verifier reconstructs the 36-copy bill +of 107,352 paid and 19,950 productive jobs, authenticates all +62,474 native contact incidences and rejects a missing paid +MOVE and a missing original idle. + +## Reproduction + +Use CPython 3.12 with assertions. From a clean checkout: + + python3.12 -B scripts/research_package.py --package research/bit-single-role-idle-rank-bound + python3.12 -B scripts/check_research_commit.py --package research/bit-single-role-idle-rank-bound --check-modes --check-source-history + +From a Git-free official export root: + + python3.12 -I -B research/bit-single-role-idle-rank-bound/replay.py --root . + +The exact caller, native word and signed receipt are declared +by stable source path with Git blob and SHA-256 pins. Duplicate +JSON and source-path controls reject. The replay needs no prior +temporary state, external interpreter path or network. + +## Open next questions + +Can one charged two-role child supply the necessary rank-two +correction while preserving both arbitrary-input fields? First +reprice the compatible paid stock including extra ordinary +operators, ownership and restoration. Then check one exact +signed native prototype only if the total can reach the target. + +Credit #7001 and #6726 for the retained exact inputs, #6834 +and #6980 for the caller lineage, and #7277 for the complete +comparison. #7163 concerns native full-fibre reflection volume, +and #7190 and #7201 treat equal-mask alignment and cover +assumptions. They are different from the fixed remaining +caller and disjoint masks used here. OpenAI Codex and subagents +materially assisted. diff --git a/research/bit-single-role-idle-rank-bound/RESULT.json.gz b/research/bit-single-role-idle-rank-bound/RESULT.json.gz new file mode 100644 index 0000000000..47b392672e Binary files /dev/null and b/research/bit-single-role-idle-rank-bound/RESULT.json.gz differ diff --git a/research/bit-single-role-idle-rank-bound/SOURCES.json b/research/bit-single-role-idle-rank-bound/SOURCES.json new file mode 100644 index 0000000000..4e3b018f8f --- /dev/null +++ b/research/bit-single-role-idle-rank-bound/SOURCES.json @@ -0,0 +1,36 @@ +{ + "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": "575f76487f9999ecc3e7b1b70f9f71bc582ef8a8", + "path": "research/paired-query-only-bit/EFREE-RESULT.json", + "sha256": "a46b6c6040f75184cab5467656811ad988c216e3bc8e44d595a5015b6e49620b", + "usage": "input" + }, + { + "git_blob": "f022272a8d51ede841778dec76e2bfb24b614d04", + "path": "research/paired-query-only-bit/EFREE-CALLER.json.gz", + "sha256": "757b3523798f840bdb02028b23708c3416627a99ea09e7a3c4bcdc5cd0c7ce4b", + "usage": "input" + } + ], + "schema_version": 1 +} diff --git a/research/bit-single-role-idle-rank-bound/TASK.json b/research/bit-single-role-idle-rank-bound/TASK.json new file mode 100644 index 0000000000..f4cc2e7040 --- /dev/null +++ b/research/bit-single-role-idle-rank-bound/TASK.json @@ -0,0 +1,77 @@ +{ + "actual_scope": "Replace a pair of disjoint-mask retained BIT IDLE_ONE events by one one-role scalar idle at an arbitrary clock, with every other caller event and the native word fixed.", + "ai_assistance": "OpenAI Codex and subagents materially assisted proof, implementation, independent audit and packaging.", + "author": "Round 38 research campaign", + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "bottleneck_link": "Resolve whether one-role idle fusion can meet the fixed BIT shortfall before constructing a provider.", + "budget_minutes": 2, + "evidence": "Two finite field specializations, all-pair rank-two certificates, complete literal signed invoice and omitted paid MOVE and idle controls.", + "open_questions": [ + { + "blocked_by": "A rank-two scalar fit still requires a legal signed native operator, ownership and restoration, and complete paid and tape cost.", + "first_step": "Price one exact two-role replacement and account for all boundary work before attempting a physical site.", + "question": "Can a changed multi-role child contract or an additional ordinary caller edit absorb the rank-two difference?", + "why_it_matters": "The single-role replacement has only one transported correction direction." + } + ], + "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": "This tests paid caller idle stock rather than productive helper stock.", + "scope_status": "changed", + "stop_rule": "Census all 256 disjoint-mask pairs. If every omitted-pair difference has rank two, close the declared one-role family without any physical site.", + "task_id": "bit-helper-contract" +} diff --git a/research/bit-single-role-idle-rank-bound/VERIFY.json b/research/bit-single-role-idle-rank-bound/VERIFY.json new file mode 100644 index 0000000000..9e0baf0652 --- /dev/null +++ b/research/bit-single-role-idle-rank-bound/VERIFY.json @@ -0,0 +1,25 @@ +{ + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/replay.py", + "--root", + "." + ], + "checks": "Reconstruct the full BIT invoice, then verify arbitrary-slot rank obstruction in two field specializations and detect omitted paid operations.", + "timeout_seconds": 20 + } + ], + "inputs": [ + "research/paired-query-only-bit/retained/inputs/BIT-NATIVE-WORD.json.gz", + "research/paired-query-only-bit/EFREE-RESULT.json", + "research/paired-query-only-bit/EFREE-CALLER.json.gz" + ], + "python": "3.12", + "requirements": [], + "schema_version": 1, + "status": "ready" +} diff --git a/research/bit-single-role-idle-rank-bound/rank_gate.py b/research/bit-single-role-idle-rank-bound/rank_gate.py new file mode 100644 index 0000000000..b0f08e69a4 --- /dev/null +++ b/research/bit-single-role-idle-rank-bound/rank_gate.py @@ -0,0 +1,106 @@ +"""Whole-stock rank obstruction to a single relocated BIT idle.""" +from collections import Counter +import gzip +from hashlib import sha256 +from itertools import combinations +import json +from pathlib import Path +from time import monotonic + +HERE=Path(__file__).resolve().parent +PIN='757b3523798f840bdb02028b23708c3416627a99ea09e7a3c4bcdc5cd0c7ce4b' + + +def residue(a,b): + d=b.bit_length()-1 + while a and a.bit_length()-1>=d: + a ^= b << (a.bit_length()-1-d) + return a + + +def multiply(a,b): + z=0 + while b: + if b&1: + z^=a + a<<=1 + b>>=1 + return residue(z,0x11b) + + +def run(): + deadline=monotonic()+18 + assert all(residue(0x11b,b) for b in range(2,32)) + products=[bytes(multiply(a,b) for b in range(256)) for a in range(256)] + raw=(HERE/'EFREE-CALLER.json.gz').read_bytes() + assert sha256(raw).hexdigest()==PIN + word=json.loads(gzip.decompress(raw)) + n=word['roles'] + def xor(row,other): + return bytes(a^b for a,b in zip(row,other,strict=True)) + def forward(values,omit): + rows=[bytes(i==j for j in range(n)) for i in range(n)] + for t,(op,*args) in enumerate(word['events']): + if t in omit: + continue + if op=='ADD' or op=='QUERY': + d,s=args + rows[d]=xor(rows[d],rows[s]) + elif op=='SWAP': + d,s=args + rows[d],rows[s]=rows[s],rows[d] + elif op=='LOCAL': + stage,s,d=args + rows[d]=xor(rows[d],rows[s]) + row=products[values[stage-1]] + rows[s]=bytes(map(row.__getitem__,rows[s])) + rows[d]=bytes(map(row.__getitem__,rows[d])) + elif op=='IDLE_ONE': + d,stages=args + scale=1 + for s in stages: + scale=products[scale][values[s-1]] + rows[d]=bytes(map(products[scale].__getitem__,rows[d])) + else: + raise ValueError(op) + return rows + def rank_two(rows): + pivot=next((r for r in rows if any(r)),None) + if pivot is None: + return 0 + i=next(i for i,v in enumerate(pivot) if v) + for r in rows: + if any(products[pivot[i]][v]!=products[r[i]][u] for u,v in zip(pivot,r,strict=True)): + return 2 + return 1 + assert rank_two([b'\x01\x00',b'\x00\x01'])==2 + assert rank_two([b'\x01\x00',b'\x03\x00'])==1 + assert rank_two([bytes(2),bytes(2)])==0 + probe=tuple(range(2,20)) + orig=forward(probe,set()) + for i,d in enumerate(word['diagonal']): + scale=1 + for stage in d['stages']: + scale=products[scale][probe[stage-1]] + assert orig[i]==bytes(scale if i==j else 0 for j in range(n)) + idles={t:set(e[2]) for t,e in enumerate(word['events']) if e[0]=='IDLE_ONE'} + pairs=[(i,j) for i,j in combinations(idles,2) if not idles[i]&idles[j]] + assert len(pairs)==256 + counts=Counter() + unresolved=[] + for i,j in pairs: + if monotonic()>=deadline: + break + changed=forward(probe,{i,j}) + rk=rank_two([xor(a,b) for a,b in zip(orig,changed,strict=True)]) + counts[rk]+=1 + if rk<2: + unresolved.append([i,j,rk]) + return {'caller_sha256':PIN,'field_polynomial':hex(0x11b),'q':1, + 'stage_probe':probe,'disjoint_scope':len(pairs),'rank_counts':dict(counts), + 'unresolved':unresolved,'unvisited':len(pairs)-sum(counts.values()), + 'physical_sites':0} + + +if __name__=='__main__': + print(json.dumps(run(),sort_keys=True,indent=2)) diff --git a/research/bit-single-role-idle-rank-bound/replay.py b/research/bit-single-role-idle-rank-bound/replay.py new file mode 100644 index 0000000000..ce0803bda1 --- /dev/null +++ b/research/bit-single-role-idle-rank-bound/replay.py @@ -0,0 +1,76 @@ +"""Reconstruct the two idle-pair rank certificates from pinned BIT inputs.""" +from argparse import ArgumentParser +import gzip +from hashlib import sha1, sha256 +import json +from pathlib import Path +import runpy +from shutil import copyfile +from tempfile import TemporaryDirectory + +HERE = Path(__file__).resolve().parent +BIT = "research/paired-query-only-bit/" + + +def unique(raw): + def keyed(items): + result = dict(items) + assert len(result) == len(items), "duplicate JSON key" + return result + return json.loads(raw, object_pairs_hook=keyed) + + +def index_sources(records): + paths = {record["path"]: record for record in records} + assert len(paths) == len(records), "duplicate source path" + return paths + + +def reject(fn, value): + try: + fn(value) + except AssertionError: + return + raise AssertionError("duplicate control accepted") + + +def run(root): + manifest = unique((HERE / "SOURCES.json").read_bytes()) + pins = index_sources(manifest["files"]) + reject(unique, b'{"a":1,"a":2}') + reject(index_sources, [{"path": "same"}, {"path": "same"}]) + files = { + BIT + "EFREE-CALLER.json.gz": "preflight/EFREE-CALLER.json.gz", + BIT + "retained/inputs/BIT-NATIVE-WORD.json.gz": "native/inputs/WORD.json.gz", + BIT + "EFREE-RESULT.json": "native/inputs/INVOICE.json", + } + assert set(files) == {name for name, pin in pins.items() if pin["usage"] == "input"} + with TemporaryDirectory(prefix="idle-rank-replay-") as scratch: + temp = Path(scratch) + for source, dest in files.items(): + data = (root / source).read_bytes() + pin = pins[source] + assert sha256(data).hexdigest() == pin["sha256"], source + assert sha1(f"blob {len(data)}\0".encode() + data).hexdigest() == pin["git_blob"], source + unique(gzip.decompress(data) if source.endswith(".gz") else data) + target = temp / dest + target.parent.mkdir(parents=True, exist_ok=True) + target.write_bytes(data) + copyfile(HERE / "rank_gate.py", temp / "preflight/rank_gate.py") + primary = runpy.run_path(str(temp / "preflight/rank_gate.py"))["run"]() + assert unique(json.dumps(primary)) == unique((HERE / "PRIMARY.json").read_bytes()) + result = runpy.run_path(str(HERE / "verify.py"))["audit"](temp / "preflight", temp / "native", None) + assert unique(json.dumps(result)) == unique(gzip.decompress((HERE / "RESULT.json.gz").read_bytes())) + return { + "primary_rank_two": primary["rank_counts"][2], + "independent_rank_two": result["rank"]["disjoint_pair_rank_two"], + "whole_realizable_upper": result["whole_realizable_upper"], + "shortfall": result["shortfall_lower"], + } + + +if __name__ == "__main__": + assert __debug__ + parser = ArgumentParser(description=__doc__) + parser.add_argument("--root", type=Path, default=Path.cwd()) + print(json.dumps(run(parser.parse_args().root), sort_keys=True)) diff --git a/research/bit-single-role-idle-rank-bound/verify.py b/research/bit-single-role-idle-rank-bound/verify.py new file mode 100644 index 0000000000..d8902b6acc --- /dev/null +++ b/research/bit-single-role-idle-rank-bound/verify.py @@ -0,0 +1,379 @@ +"""Independent GF(128) rank and literal invoice audit for BIT idle pairs.""" + +from argparse import ArgumentParser +from collections import Counter +from fractions import Fraction as Q +from functools import cache +import gzip +from hashlib import sha256 +from itertools import combinations +import json +from pathlib import Path + +TARGET = Q(10018846261809, 2500000000000000) +PINS = { + "preflight/EFREE-CALLER.json.gz": "757b3523798f840bdb02028b23708c3416627a99ea09e7a3c4bcdc5cd0c7ce4b", + "native/inputs/WORD.json.gz": "51203e7fc75ba10bd3ac3f8e675759f47e13d262bea66b6600d1e515095cad78", + "native/inputs/INVOICE.json": "a46b6c6040f75184cab5467656811ad988c216e3bc8e44d595a5015b6e49620b", +} + + +def unique(items): + out = dict(items) + assert len(out) == len(items), "duplicate JSON key" + return out + + +def load_inputs(preflight, native, repo): + if repo is None: + paths = (preflight / "EFREE-CALLER.json.gz", native / "inputs/WORD.json.gz", + native / "inputs/INVOICE.json") + else: + source = repo / "research/paired-query-only-bit" + paths = (source / "EFREE-CALLER.json.gz", source / "retained/inputs/BIT-NATIVE-WORD.json.gz", + source / "EFREE-RESULT.json") + data = {} + for (name, expected), path in zip(PINS.items(), paths, strict=True): + blob = path.read_bytes() + assert sha256(blob).hexdigest() == expected, f"changed source {name}" + if path.suffix == ".gz": + blob = gzip.decompress(blob) + data[name] = json.loads(blob, object_pairs_hook=unique) + return list(data.values()) + + +class GF128: + # X generates all nonzero elements in F2[X]/(X^7 + X + 1). + # Verifying the complete cycle proves that the quotient is a field. + polynomial = 0x83 + + def __init__(self): + self.powers = [1] + for _ in range(127): + x = self.powers[-1] << 1 + self.powers.append(x ^ self.polynomial if x & 128 else x) + assert self.powers[-1] == 1 and set(self.powers[:-1]) == set(range(1, 128)) + self.logs = {x: i for i, x in enumerate(self.powers[:-1])} + + def mul(self, x, y): + if not x or not y: + return 0 + return self.powers[(self.logs[x] + self.logs[y]) % 127] + + def product(self, values): + result = 1 + for value in values: + result = self.mul(result, value) + return result + + +def event_ops(caller, f, probe): + for code, *args in caller["events"]: + if code in ("ADD", "QUERY"): + d, s = args + yield (code, d, s, 1) + elif code == "SWAP": + d, s = args + yield (code, d, s, 1) + elif code == "LOCAL": + stage, s, d = args + yield (code, d, s, probe[stage - 1]) + else: + assert code == "IDLE_ONE" + d, stages = args + yield (code, d, d, f.product(probe[s - 1] for s in stages)) + + +def apply(f, vector, op, transposed=False): + code, d, s, a = op + if code == "SWAP": + vector[d], vector[s] = vector[s], vector[d] + elif code == "IDLE_ONE": + vector[d] = f.mul(a, vector[d]) + elif code == "LOCAL": + if transposed: + vector[s], vector[d] = f.mul(a, vector[s] ^ vector[d]), f.mul(a, vector[d]) + else: + vector[s], vector[d] = f.mul(a, vector[s]), f.mul(a, vector[d] ^ vector[s]) + else: + assert code in ("ADD", "QUERY") + if transposed: + vector[s] ^= vector[d] + else: + vector[d] ^= vector[s] + + +def unit(n, i): + return [int(j == i) for j in range(n)] + + +def evaluate(f, n, ops, omit=()): + columns = [] + for i in range(n): + v = unit(n, i) + for t, op in enumerate(ops): + if t not in omit: + apply(f, v, op) + columns.append(v) + return columns + + +def pair_factors(f, n, ops, i, j): + _, r, _, a = ops[i] + _, s, _, b = ops[j] + left = unit(n, r) + right = unit(n, s) + for t in range(i + 1, j): + apply(f, left, ops[t]) + for t in range(j - 1, i, -1): + apply(f, right, ops[t], transposed=True) + l = next(((u, x) for u, x in enumerate(left) if u != s and x), None) + h = next(((v, x) for v, x in enumerate(right) if v != r and x), None) + if a == 1 or b == 1 or l is None or h is None: + return None + # Minor of the inner difference on rows (l[0], s), columns (r, h[0]). + minor = f.product((a ^ 1, b ^ 1, l[1], h[1])) + assert minor + return {"left_off_axis": l, "right_off_axis": h, "minor": minor} + + +def rank_check(caller): + f = GF128() + n = caller["roles"] + assert n == len(caller["diagonal"]) == 38 and caller["stages"] == 18 + assert caller["native_per_stage"] == 2 and caller["ports"] == 111 + probe = tuple(f.powers[1:19]) + ops = tuple(event_ops(caller, f, probe)) + original = evaluate(f, n, ops) + expected = [] + for j, target in enumerate(caller["diagonal"]): + col = unit(n, j) + col[j] = f.product(probe[s - 1] for s in target["stages"]) + expected.append(col) + assert original == expected + idles = {i: set(e[2]) for i, e in enumerate(caller["events"]) if e[0] == "IDLE_ONE"} + assert len(idles) == 32 + assert evaluate(f, n, ops, (min(idles),)) != original, "omitted paid idle not detected" + toy = (("IDLE_ONE", 0, 0, 2), ("IDLE_ONE", 1, 1, 3)) + assert pair_factors(f, 2, toy, 0, 1) is not None + repeated = (("IDLE_ONE", 0, 0, 2), ("IDLE_ONE", 0, 0, 3)) + assert pair_factors(f, 2, repeated, 0, 1) is None + pairs = [(i, j) for i, j in combinations(idles, 2) if not idles[i] & idles[j]] + assert len(pairs) == 256 + out = [] + for i, j in pairs: + w = pair_factors(f, n, ops, i, j) + assert w is not None, f"inconclusive specialization {i},{j}" + out.append({"removed": [i, j], **w}) + return {"field": "F2[X]/(X^7+X+1)", "q": 1, "probe": probe, + "baseline_coefficients": n * n, "pair_inventory": 496, + "overlapping_masks_outside_scope": 240, "disjoint_pair_rank_two": len(out), + "new_clocks_scanned": 0, "unresolved": 0, "minor_witnesses": out, + "controls": ["omitted old idle", "independent diagonal axes", "repeated diagonal axis"]} + + +def linear_rank(rows): + basis = {} + for row in rows: + v = list(row) + for j in range(len(v)): + x = v[j] + if not x: + continue + if j in basis: + v = [a - x * b for a, b in zip(v, basis[j], strict=True)] + else: + basis[j] = [a / x for a in v] + break + return len(basis) + + +def native_bill(word, drop_move=None): + n = word["public"] + m = word["owned_fields"] + basis = {int(k): tuple(tuple(map(Q, row)) for row in v["B"]) + for k, v in word["frames"].items()} + dims = {int(k): v["dim"] for k, v in word["frames"].items()} + assert all(dims[k] == len(rows) == linear_rank(rows) for k, rows in basis.items()) + + @cache + def move_rank(a, b): + assert dims[a] != dims[b] + assert linear_rank(basis[a] + basis[b]) == max(dims[a], dims[b]) + return abs(dims[a] - dims[b]) + + current = word["start"] + [None] * m + last = current.copy() + rows = [1 << i for i in range(n)] + [0] * m + paid = Counter() + literal = Counter() + contacts = Counter() + + def touch(slot, frame): + assert current[slot] == frame and last[slot] is not None + contacts[last[slot], frame] += 1 + last[slot] = frame + + for t, (op, d, *args) in enumerate(word["program"]): + if op == "MOVE": + if t == drop_move: + continue + a, b = args + assert current[d] == a + paid[move_rank(a, b)] += 1 + literal[a, b] += 1 + current[d] = b + elif op == "SWAP": + s, = args + for seq in (current, last, rows): + seq[d], seq[s] = seq[s], seq[d] + elif op == "INIT": + assert d >= n and current[d] is None + current[d], = args + last[d] = current[d] + rows[d] = 0 + elif op == "ADD": + s, frame = args + touch(d, frame) + if s != d: + touch(s, frame) + rows[d] ^= rows[s] + else: + assert op == "CLEAR" and d >= n + frame, = args + touch(d, frame) + current[d] = last[d] = None + rows[d] = 0 + assert current == word["final"] + [None] * m + expected = [1 << i for i in range(n)] + [0] * m + for i in range(111): + expected[111 + i] ^= 1 << i + assert rows == expected + for d, f in enumerate(word["final"]): + touch(d, f) + assert Counter({(a, b): c for (a, b), c in contacts.items() if a != b}) == literal + assert sum(contacts.values()) == 62474 + targets = Counter() + for a, b in zip(word["start"][222:], word["final"][222:], strict=True): + assert dims[b] > dims[a] + targets[move_rank(a, b)] += 1 + return paid, targets, sum(contacts.values()) + + +def whole_bill(caller, native, invoice): + n_paid, n_target, contacts = native_bill(native) + assert sum(n_paid.values()) == 2871 and sum(n_target.values()) == 437 + assert n_paid == Counter({int(r): c for r, c in invoice["native_paid"].items()}) + assert n_target == Counter({int(r): c for r, c in invoice["native_helpers"].items()}) + ports, body = caller["ports"], caller["body_rank"] + stages = Counter(e[1] for e in caller["events"] if e[0] == "LOCAL") + assert stages == Counter({i: 2 for i in range(1, 19)}) + copies = stages.total() + assert copies == invoice["native_calls"] == 36 and body == 7 + paid = Counter({r: copies * c for r, c in n_paid.items()}) + targets = Counter({r: copies * c for r, c in n_target.items()}) + idle = Counter() + for code, *args in caller["events"]: + if code == "IDLE_ONE": + mask = args[-1] + assert mask and len(mask) == len(set(mask)) + idle[body * len(mask)] += ports + elif code == "QUERY": + paid[1] += ports + paid.update(idle) + for d in caller["diagonal"]: + targets[d["q"] + body * len(d["stages"])] += ports + assert paid == Counter({int(r): c for r, c in invoice["paid"].items()}) + assert targets == Counter({int(r): c for r, c in invoice["targets"].items()}) + signed = {r: targets[r] - paid[r] for r in sorted(targets.keys() | paid.keys())} + assert paid.total() == 107352 and targets.total() == 19950 + assert sum(r * c for r, c in signed.items()) == 1506 + omitted = next(t for t, e in enumerate(native["program"]) if e[0] == "MOVE") + try: + native_bill(native, drop_move=omitted) + except AssertionError: + pass + else: + raise AssertionError("omitted native payment survived") + return {"native_copies": copies, "literal_native_moves": n_paid.total(), + "native_contacts": contacts, "paid": paid, "targets": targets, "rank_surplus": 1506, + "paid_total": paid.total(), "target_total": targets.total(), "idle_hist": idle, + "signed": signed, "omitted_move_control": omitted} + + +def log_unit(x): + t = (x - 1) / (x + 1) + assert 0 <= t <= Q(1, 3) + low = sum(2 * t**(2 * j + 1) / (2 * j + 1) for j in range(72)) + return low, low + 2 * t**145 / (145 * (1 - t * t)) + + +GRID = 10**58 + + +def downward(x): + return Q((x * GRID).__floor__(), GRID) + + +def upward(x): + return Q((x * GRID).__ceil__(), GRID) + + +def exp_at(x, last): + assert 0 <= x < 1 + term, total = Q(1), Q(1) + for j in range(1, last + 1): + term *= -x / j + total += term + return total + + +@cache +def power(r): + m = r.bit_length() - 1 + a, b = log_unit(Q(r, 1 << m)) + c, d = log_unit(Q(2)) + x0 = downward(TARGET * (a + m * c)) + x1 = upward(TARGET * (b + m * d)) + return downward(r * exp_at(x1, 43)), upward(r * exp_at(x0, 42)) + + +def cost(hist): + intervals = [sorted(c * x for x in power(r)) for r, c in hist.items()] + return tuple(sum(row[i] for row in intervals) for i in (0, 1)) + + +def audit(preflight, native, repo): + caller, word, invoice = load_inputs(preflight, native, repo) + assert invoice["caller_sha256"] == PINS["preflight/EFREE-CALLER.json.gz"] + assert invoice["native_source_sha256"] == PINS["native/inputs/WORD.json.gz"] + rank = rank_check(caller) + bill = whole_bill(caller, word, invoice) + net = cost(bill["signed"]) + discount = 1 - power(2)[0] / 2 + free_upper = discount * cost(bill["idle_hist"])[1] + assert net[1] < 0 and net[1] + free_upper > 0 + assert Q(60) < -net[1] < Q(61) and Q(305) < free_upper < Q(306) + return {"target": str(TARGET), "pins": PINS, "rank": rank, "invoice": bill, + "signed_moment_interval": list(map(str, net)), + "shortfall_lower": str(-net[1]), "shortfall_decimal": float(-net[1]), + "whole_free_optimistic_upper": str(free_upper), + "whole_free_upper_decimal": float(free_upper), + "whole_realizable_upper": "0", "physical_sites": 0} + + +def main(): + p = ArgumentParser() + p.add_argument("preflight", type=Path, nargs="?") + p.add_argument("native", type=Path, nargs="?") + p.add_argument("--repo-root", type=Path) + args = p.parse_args() + if args.repo_root is None and (args.preflight is None or args.native is None): + p.error("provide both replay roots or --repo-root") + if args.repo_root is not None and (args.preflight is not None or args.native is not None): + p.error("provide replay roots or --repo-root") + print(json.dumps(audit(args.preflight, args.native, args.repo_root), indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main() 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")