From aab8be2e08d373fb33be886438716ed649c5ceaf Mon Sep 17 00:00:00 2001 From: ToikY <27568617+ToikY@users.noreply.github.com> Date: Wed, 11 Nov 2026 00:43:24 -0800 Subject: [PATCH 1/3] Reuse selected replay navigation for hosted checks Reuse the exact documentation blob carried by #7161 at bb36fc65ee0b161229169505f4840c436c5ca2b9, following #7147 and #7156. --- docs/ci-verification.md | 19 ++++++++++++++++++- 1 file changed, 18 insertions(+), 1 deletion(-) 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). From f59cf773c6038d72bc3b5aeae204cbe1923b34bf Mon Sep 17 00:00:00 2001 From: ToikY <27568617+ToikY@users.noreply.github.com> Date: Wed, 11 Nov 2026 00:43:32 -0800 Subject: [PATCH 2/3] Verify formal paired BIT QUERY 349 removal --- .../HEAD-REPLAY-price.json | 126 ++++++++++ .../HEAD-REPLAY-price.py | 151 ++++++++++++ .../HEAD-REPLAY.json | 217 ++++++++++++++++++ .../HEAD-REPLAY.py | 118 ++++++++++ .../README.md | 42 ++++ .../SOURCES.json | 36 +++ .../TASK.json | 77 +++++++ .../VERIFY.json | 27 +++ .../verify.py | 51 ++++ 9 files changed, 845 insertions(+) create mode 100644 research/paired-bit-query349-formal-caller/HEAD-REPLAY-price.json create mode 100644 research/paired-bit-query349-formal-caller/HEAD-REPLAY-price.py create mode 100644 research/paired-bit-query349-formal-caller/HEAD-REPLAY.json create mode 100644 research/paired-bit-query349-formal-caller/HEAD-REPLAY.py create mode 100644 research/paired-bit-query349-formal-caller/README.md create mode 100644 research/paired-bit-query349-formal-caller/SOURCES.json create mode 100644 research/paired-bit-query349-formal-caller/TASK.json create mode 100644 research/paired-bit-query349-formal-caller/VERIFY.json create mode 100644 research/paired-bit-query349-formal-caller/verify.py diff --git a/research/paired-bit-query349-formal-caller/HEAD-REPLAY-price.json b/research/paired-bit-query349-formal-caller/HEAD-REPLAY-price.json new file mode 100644 index 0000000000..7f7bf780b3 --- /dev/null +++ b/research/paired-bit-query349-formal-caller/HEAD-REPLAY-price.json @@ -0,0 +1,126 @@ +{ + "cases_extra_rank_one_per_changed_native": { + "0": { + "derivative_bound_on_initial_bracket": [ + "-77753321321009469963034707487/200000000000000000000000", + "-1931991500533442173247560521819/5000000000000000000000000" + ], + "net_removed_rank_one": 111, + "raw_crossing_bracket": [ + "41388676593/10000000000000", + "8277735319/2000000000000" + ], + "target_margin": [ + "254480503904263230680005677/5000000000000000000000000", + "254480503904263230680046183/5000000000000000000000000" + ] + }, + "1": { + "derivative_bound_on_initial_bracket": [ + "-77753321321009469963034707487/200000000000000000000000", + "-1931991500533442173247560521819/5000000000000000000000000" + ], + "net_removed_rank_one": 93, + "raw_crossing_bracket": [ + "40924136423/10000000000000", + "5115517053/1250000000000" + ], + "target_margin": [ + "164480503904263230680005677/5000000000000000000000000", + "164480503904263230680046183/5000000000000000000000000" + ] + }, + "2": { + "derivative_bound_on_initial_bracket": [ + "-77753321321009469963034707487/200000000000000000000000", + "-1931991500533442173247560521819/5000000000000000000000000" + ], + "net_removed_rank_one": 75, + "raw_crossing_bracket": [ + "40459683031/10000000000000", + "40459683033/10000000000000" + ], + "target_margin": [ + "74480503904263230680005677/5000000000000000000000000", + "74480503904263230680046183/5000000000000000000000000" + ] + }, + "3": { + "derivative_bound_on_initial_bracket": [ + "-77753321321009469963034707487/200000000000000000000000", + "-1931991500533442173247560521819/5000000000000000000000000" + ], + "net_removed_rank_one": 57, + "raw_crossing_bracket": [ + "39995316387/10000000000000", + "9998829097/2500000000000" + ], + "target_margin": [ + "-15519496095736769319994323/5000000000000000000000000", + "-15519496095736769319953817/5000000000000000000000000" + ] + } + }, + "native_helpers": { + "2": 1, + "4": 25, + "6": 1, + "8": 410 + }, + "native_paid": { + "1": 1386, + "2": 1253, + "3": 62, + "4": 47, + "5": 9, + "6": 104, + "7": 10 + }, + "paid": { + "1": 50340, + "2": 45108, + "3": 2232, + "4": 1692, + "5": 324, + "6": 3744, + "7": 804, + "14": 444, + "21": 444, + "28": 444, + "35": 444, + "42": 444, + "49": 444, + "56": 444 + }, + "pins": { + "EFREE-CALLER.json.gz": "757b3523798f840bdb02028b23708c3416627a99ea09e7a3c4bcdc5cd0c7ce4b", + "EFREE-RESULT.json": "a46b6c6040f75184cab5467656811ad988c216e3bc8e44d595a5015b6e49620b", + "retained/inputs/BIT-NATIVE-WORD.json.gz": "51203e7fc75ba10bd3ac3f8e675759f47e13d262bea66b6600d1e515095cad78" + }, + "predecessor_crossing_bracket": [ + "19262696967/5000000000000", + "7705078787/2000000000000" + ], + "predecessor_crossing_overlaps_public_receipt": true, + "predecessor_target_margin": [ + "-300519496095736769319994323/5000000000000000000000000", + "-300519496095736769319953817/5000000000000000000000000" + ], + "productive": { + "2": 36, + "4": 900, + "6": 36, + "8": 15204, + "15": 444, + "22": 444, + "29": 444, + "36": 444, + "43": 444, + "50": 444, + "57": 444, + "64": 444, + "127": 222 + }, + "scope": "Raw paid-profile crossing only; excludes any unpriced costs of literal changed native word, compiler/tape, and full theorem.", + "target": "10018846261809/2500000000000000" +} diff --git a/research/paired-bit-query349-formal-caller/HEAD-REPLAY-price.py b/research/paired-bit-query349-formal-caller/HEAD-REPLAY-price.py new file mode 100644 index 0000000000..80daf21f4d --- /dev/null +++ b/research/paired-bit-query349-formal-caller/HEAD-REPLAY-price.py @@ -0,0 +1,151 @@ +"""Census of literal paired BIT invoice and directed raw price crossings.""" +from collections import Counter +from fractions import Fraction as Q +from functools import cache +from importlib.util import module_from_spec, spec_from_file_location +import json +from pathlib import Path +import sys + +TARGET = Q("0.0040075385047236") +SCALE = 10**25 + + +def enc_q(x, ceil): + p = x*SCALE + n,d = p.numerator,p.denominator + return Q(-((-n)//d) if ceil else n//d, SCALE) + + +def out(interval): + return list(map(str, interval)) + + +def round_out(lo, hi): + return enc_q(lo, False), enc_q(hi, True) + + +@cache +def log_reduced(x): + z = (x-1)/(x+1) + lo = 2*sum(z**(2*i+1)/(2*i+1) for i in range(31)) + return round_out(lo, lo+2*z**63/(63*(1-z*z))) + + +@cache +def log_rank(r): + e = r.bit_length()-1 + l2,h2 = log_reduced(Q(2)) + l,h = log_reduced(Q(r, 2**e)) + return l+e*l2, h+e*h2 + + +def alternating(x): + assert 0 <= x < 1 + t = s = Q(1) + for i in range(1,19): + t = -t*x/i + s += t + return s-t, s + + +@cache +def power(r,k): + l,h = log_rank(r) + return round_out(r*alternating(k*h)[0], r*alternating(k*l)[1]) + + +def dot(coefficients, evaluator): + lo = hi = Q(0) + for rank,count in coefficients.items(): + a,b = evaluator(rank) + if count < 0: + a,b = b,a + lo += count*a + hi += count*b + return lo,hi + + +def crossing(signed, lo, hi): + assert dot(signed, lambda r:power(r,lo))[0]>0 + assert dot(signed, lambda r:power(r,hi))[1]<0 + def derivative_bound(r): + ll,lh = log_rank(r) + return -lh*power(r,lo)[1], -ll*power(r,hi)[0] + derivative = dot(signed, derivative_bound) + assert derivative[1] < 0 + while hi-lo > Q(1,10**13): + m = (lo+hi)/2 + a,b = dot(signed,lambda r:power(r,m)) + if a>0: + lo=m + elif b<0: + hi=m + else: + raise RuntimeError("insufficient interval separation") + assert dot(signed,lambda r:power(r,lo))[0]>0 + assert dot(signed,lambda r:power(r,hi))[1]<0 + # Outward decimal grid also gets independent sign checks. + grid=10**13 + lo=Q((lo*grid).numerator//(lo*grid).denominator,grid) + hi=Q(-((-hi*grid).numerator//(hi*grid).denominator),grid) + assert dot(signed,lambda r:power(r,lo))[0]>0 + assert dot(signed,lambda r:power(r,hi))[1]<0 + return out((lo,hi)),out(round_out(*derivative)) + + +def integer_hist(d): + return Counter({int(r): n for r,n in d.items()}) + + +def price(root): + spec=spec_from_file_location("endpoint", Path(__file__).with_name("HEAD-REPLAY.py")) + endpoint=module_from_spec(spec) + spec.loader.exec_module(endpoint) + caller=endpoint.load(root, "EFREE-CALLER.json.gz") + result=endpoint.load(root, "EFREE-RESULT.json") + source=endpoint.load(root, "retained/inputs/BIT-NATIVE-WORD.json.gz") + dims={int(i): c["dim"] for i,c in source["frames"].items()} + paid0=Counter(abs(dims[a]-dims[b]) for op,_,*rest in source["program"] + if op=="MOVE" for a,b in (rest,)) + helper0=Counter(abs(dims[a]-dims[b]) for a,b in + zip(source["start"][222:], source["final"][222:], strict=True)) + assert paid0==integer_hist(result["native_paid"]) + assert helper0==integer_hist(result["native_helpers"]) + n=caller["ports"] + count=Counter(e[0] for e in caller["events"]) + paid=Counter({r:c*count["LOCAL"] for r,c in paid0.items()}) + productive=Counter({r:c*count["LOCAL"] for r,c in helper0.items()}) + for op,*rest in caller["events"]: + if op=="QUERY": + paid[1]+=n + elif op=="IDLE_ONE": + paid[caller["body_rank"]*len(rest[1])]+=n + for spec in caller["diagonal"]: + productive[spec["q"]+caller["body_rank"]*len(spec["stages"])]+=n + assert paid==integer_hist(result["paid"]) + assert productive==integer_hist(result["targets"]) + signed=productive.copy() + signed.subtract(paid) + base=crossing(signed,Q(".0038"),Q(".0043")) + old_cert=tuple(map(Q,result["raw_crossing"])) + assert Q(base[0][0])<=old_cert[1] and old_cert[0]<=Q(base[0][1]) + cases={} + for extra in range(4): + new=signed.copy() + new[1]+=n-extra*caller["stages"] + interval,derivative=crossing(new,Q(".0038"),Q(".0043")) + cases[extra]={"net_removed_rank_one":new[1]-signed[1], + "raw_crossing_bracket":interval, + "derivative_bound_on_initial_bracket":derivative, + "target_margin":out(dot(new,lambda r:power(r,TARGET)))} + return {"pins":endpoint.PINS,"target":str(TARGET),"native_paid":paid0,"native_helpers":helper0, + "paid":paid,"productive":productive,"predecessor_crossing_bracket":base[0], + "predecessor_target_margin":out(dot(signed,lambda r:power(r,TARGET))), + "predecessor_crossing_overlaps_public_receipt":True, + "cases_extra_rank_one_per_changed_native":cases, + "scope":"Raw paid-profile crossing only; excludes any unpriced costs of literal changed native word, compiler/tape, and full theorem."} + + +if __name__=="__main__": + print(json.dumps(price(Path(sys.argv[1])),sort_keys=True,indent=2)) diff --git a/research/paired-bit-query349-formal-caller/HEAD-REPLAY.json b/research/paired-bit-query349-formal-caller/HEAD-REPLAY.json new file mode 100644 index 0000000000..2c1e3ad0e3 --- /dev/null +++ b/research/paired-bit-query349-formal-caller/HEAD-REPLAY.json @@ -0,0 +1,217 @@ +{ + "changed_second_locals": [ + 5, + 17, + 29, + 41, + 53, + 65, + 77, + 89, + 101, + 395, + 453, + 497, + 541, + 585, + 629, + 673, + 717, + 761 + ], + "coefficients_per_direction": 1444, + "events": 798, + "modes": { + "candidate": { + "forward_mismatches": [], + "reverse_mismatches": [] + }, + "predecessor": { + "forward_mismatches": [], + "reverse_mismatches": [] + }, + "retain_query_349": { + "forward_mismatches": [ + [ + 19, + 20 + ], + [ + 19, + 21 + ], + [ + 19, + 22 + ], + [ + 19, + 23 + ], + [ + 19, + 24 + ], + [ + 19, + 25 + ], + [ + 19, + 26 + ], + [ + 19, + 27 + ], + [ + 19, + 28 + ], + [ + 19, + 29 + ], + [ + 19, + 30 + ], + [ + 19, + 31 + ], + [ + 19, + 32 + ], + [ + 19, + 33 + ], + [ + 19, + 34 + ], + [ + 19, + 35 + ], + [ + 19, + 36 + ], + [ + 19, + 37 + ] + ], + "reverse_mismatches": [ + [ + 19, + 20 + ], + [ + 19, + 21 + ], + [ + 19, + 22 + ], + [ + 19, + 23 + ], + [ + 19, + 24 + ], + [ + 19, + 25 + ], + [ + 19, + 26 + ], + [ + 19, + 27 + ], + [ + 19, + 28 + ], + [ + 19, + 29 + ], + [ + 19, + 30 + ], + [ + 19, + 31 + ], + [ + 19, + 32 + ], + [ + 19, + 33 + ], + [ + 19, + 34 + ], + [ + 19, + 35 + ], + [ + 19, + 36 + ], + [ + 19, + 37 + ] + ] + }, + "revert_first_changed_local": { + "forward_mismatches": [ + [ + 19, + 19 + ], + [ + 19, + 20 + ] + ], + "reverse_mismatches": [ + [ + 19, + 19 + ], + [ + 19, + 20 + ] + ] + } + }, + "pins": { + "EFREE-CALLER.json.gz": "757b3523798f840bdb02028b23708c3416627a99ea09e7a3c4bcdc5cd0c7ce4b", + "EFREE-RESULT.json": "a46b6c6040f75184cab5467656811ad988c216e3bc8e44d595a5015b6e49620b", + "retained/inputs/BIT-NATIVE-WORD.json.gz": "51203e7fc75ba10bd3ac3f8e675759f47e13d262bea66b6600d1e515095cad78" + }, + "query_to_add": 349, + "source_urls": { + "EFREE-CALLER.json.gz": "https://raw.githubusercontent.com/CrocSwap/integer-mult-bounds/e54523517d0f03e58352e647c403a5af3e525a57/research/paired-query-only-bit/EFREE-CALLER.json.gz", + "EFREE-RESULT.json": "https://raw.githubusercontent.com/CrocSwap/integer-mult-bounds/e54523517d0f03e58352e647c403a5af3e525a57/research/paired-query-only-bit/EFREE-RESULT.json", + "retained/inputs/BIT-NATIVE-WORD.json.gz": "https://raw.githubusercontent.com/CrocSwap/integer-mult-bounds/e54523517d0f03e58352e647c403a5af3e525a57/research/paired-query-only-bit/retained/inputs/BIT-NATIVE-WORD.json.gz" + } +} diff --git a/research/paired-bit-query349-formal-caller/HEAD-REPLAY.py b/research/paired-bit-query349-formal-caller/HEAD-REPLAY.py new file mode 100644 index 0000000000..bb06e2e37b --- /dev/null +++ b/research/paired-bit-query349-formal-caller/HEAD-REPLAY.py @@ -0,0 +1,118 @@ +"""Independent exact matrix action for the paired BIT caller and inverse.""" +from collections import Counter +import gzip +from hashlib import sha256 +import json +from pathlib import Path +import sys + +PINS = { + "EFREE-CALLER.json.gz": "757b3523798f840bdb02028b23708c3416627a99ea09e7a3c4bcdc5cd0c7ce4b", + "EFREE-RESULT.json": "a46b6c6040f75184cab5467656811ad988c216e3bc8e44d595a5015b6e49620b", + "retained/inputs/BIT-NATIVE-WORD.json.gz": "51203e7fc75ba10bd3ac3f8e675759f47e13d262bea66b6600d1e515095cad78", +} +CANONICAL = "e54523517d0f03e58352e647c403a5af3e525a57" +SOURCE = f"https://raw.githubusercontent.com/CrocSwap/integer-mult-bounds/{CANONICAL}/research/paired-query-only-bit" + + +def load(root, key): + raw = (root / key).read_bytes() + if sha256(raw).hexdigest() != PINS[key]: + raise ValueError(f"sha256 mismatch: {key}") + return json.loads(gzip.decompress(raw) if key.endswith(".gz") else raw) + + +def run(w, changed_locals, new_query, reverse=False): + # A row maps a Laurent body monomial and q parity to all 38 coefficients, + # stored together in a bitmask. Every operation is over F2. + zero = (0,) * w["stages"] + rows = [{(0, zero): 1 << i} for i in range(w["roles"])] + steps = list(enumerate(w["events"])) + + def shift(row, q=0, stages=(), sign=1): + deltas = set(stages) + return {(parity ^ q, tuple(a + sign * ((i + 1) in deltas) + for i, a in enumerate(powers))): bits + for (parity, powers), bits in row.items()} + + def add(left, right): + output = dict(left) + for monomial, bits in right.items(): + coefficient = output.pop(monomial, 0) ^ bits + if coefficient: + output[monomial] = coefficient + return output + + for index, (op, *args) in (reversed(steps) if reverse else steps): + if op == "SWAP": + x, y = args + rows[x], rows[y] = rows[y], rows[x] + elif op == "IDLE_ONE": + x, stages = args + rows[x] = shift(rows[x], stages=stages, sign=-1 if reverse else 1) + elif op in ("ADD", "QUERY"): + y, x = args + rows[y] = add(rows[y], shift(rows[x], q=int(op == "QUERY" and index != new_query))) + elif op == "LOCAL": + stage, x, y = args + new = index in changed_locals + if reverse: + bx = shift(rows[x], stages=(stage,), sign=-1, q=int(new)) + by = shift(rows[y], stages=(stage,), sign=-1) + rows[x] = bx + rows[y] = add(by, shift(bx, q=int(not new))) + else: + rows[y] = shift(add(rows[y], shift(rows[x], q=int(not new))), stages=(stage,)) + rows[x] = shift(rows[x], q=int(new), stages=(stage,)) + else: + raise ValueError(op) + + wrong = [] + for i, spec in enumerate(w["diagonal"]): + expected = shift({(0, zero): 1 << i}, q=spec["q"], stages=spec["stages"], + sign=-1 if reverse else 1) + residue = add(rows[i], expected) + touched = 0 + for mask in residue.values(): + touched |= mask + for j in range(w["roles"]): + if touched >> j & 1: + wrong.append((i, j)) + return wrong + + +def main(root): + w = load(root, "EFREE-CALLER.json.gz") + result = load(root, "EFREE-RESULT.json") + load(root, "retained/inputs/BIT-NATIVE-WORD.json.gz") + order = Counter() + changed = [] + for i, (op, *args) in enumerate(w["events"]): + if op == "LOCAL": + stage, x, y = args + order[stage] += 1 + if order[stage] == 2: + assert (x, y) == (20, 19) + changed.append(i) + assert order == dict.fromkeys(range(1, 19), 2) + assert w["events"][349] == ["QUERY", 19, 20] and w["ports"] == 111 + assert result["caller_sha256"] == PINS["EFREE-CALLER.json.gz"] + assert result["native_source_sha256"] == PINS["retained/inputs/BIT-NATIVE-WORD.json.gz"] + modes = {} + for label, locals_, query in ( + ("predecessor", [], None), + ("candidate", changed, 349), + ("revert_first_changed_local", changed[1:], 349), + ("retain_query_349", changed, None), + ): + modes[label] = {"forward_mismatches": run(w, locals_, query), + "reverse_mismatches": run(w, locals_, query, reverse=True)} + assert not any(modes["predecessor"].values()) and not any(modes["candidate"].values()) + assert all(modes["revert_first_changed_local"].values()) and all(modes["retain_query_349"].values()) + return {"pins": PINS, "source_urls": {p:f"{SOURCE}/{p}" for p in PINS}, + "events": len(w["events"]), "coefficients_per_direction": w["roles"] ** 2, + "changed_second_locals": changed, "query_to_add": 349, "modes": modes} + + +if __name__ == "__main__": + print(json.dumps(main(Path(sys.argv[1])), sort_keys=True, indent=2)) diff --git a/research/paired-bit-query349-formal-caller/README.md b/research/paired-bit-query349-formal-caller/README.md new file mode 100644 index 0000000000..9e14a6d0f8 --- /dev/null +++ b/research/paired-bit-query349-formal-caller/README.md @@ -0,0 +1,42 @@ +# Remove QUERY 349 in the formal paired BIT caller + +**κ change 0%.** In the exact #7001 38-role caller, change the second LOCAL at each of 18 stages and replace QUERY 349 with an ordinary ADD. The predecessor and the changed caller have the same specified diagonal on all arbitrary input coefficients, forward and reverse. The changed LOCAL needs a new physical provider. This package verifies the formal identity and reconstructs its conditional raw price. + +## Exact caller change + +Let q be the split head involution and D_s the commuting body action of stage s. The retained LOCAL on source x and destination y is `(D_s x, D_s(y+q x))`. Replace it at the second LOCAL of each stage by `(D_s qx, D_s(x+y))`. The pinned events use source 20 and destination 19 at all 18 changed calls. Replace the q-dependent QUERY at event 349 with the ordinary ADD using the same operands. All other events remain literal. + +The verifier propagates Laurent monomials in all 18 body variables and q parity, with q²=1, over F₂. Each monomial carries a 38-bit mask of the contributing input columns. It checks every coefficient of the prescribed output diagonal, including cancellation and body powers. Reverse uses the inverse LOCAL formulas and negates all body powers. Both directions match all 1,444 coefficients. Reverting the first changed LOCAL causes two mismatches in each direction. Keeping QUERY 349 causes 18 in each direction. The old caller is the positive control. A changed source byte is rejected before decompression. + +## Raw price and scope + +Reconstruct the old native paid histogram from literal MOVE rank differences and its productive helper histogram from endpoint ranks. Reconstruct the caller invoice from literal LOCAL, QUERY, IDLE and diagonal events. Both histograms match the authenticated predecessor. The raw crossing agrees with its public interval. + +| Extra rank-one jobs per changed LOCAL | Raw target margin, rounded | Directed raw crossing | +|---:|---:|---:| +| 0 | +50.89610078085 | [0.0041388676593, 0.0041388676595] | +| 1 | +32.89610078085 | [0.0040924136423, 0.0040924136424] | +| 2 | +14.89610078085 | [0.0040459683031, 0.0040459683033] | +| 3 | −3.10389921915 | [0.0039995316387, 0.0039995316388] | + +The exact trial κ is `10018846261809/2500000000000000`. The table charges each added rank-one job and deletes the 111 paid jobs at QUERY 349. Logarithms use an outward rational atanh series with a geometric remainder, and exponentials use even/odd alternating partial sums. The derivative enclosure gives uniqueness in the checked raw interval. All values are raw component prices. They do not certify stock, a changed provider, fixed-tape compiler admission, or a multiplication bound. + +With the old physical provider held opaque, the needed input correction at each changed LOCAL is q on all 111 independent source lanes. Its first derivative at q=1 has rank 111, so a fixed-wiring retrofit by rank-one head jobs pays at least that many jobs. A rebuilt provider can change the internal head/body decomposition, which is the open case. A full candidate also needs a compatible admitted complex supplier. No benchmark or selected record changes. + +## Clean replay + +From a clean checkout of this branch with CPython 3.12 and assertions: + +```sh +python3.12 -B scripts/research_package.py --package research/paired-bit-query349-formal-caller +``` + +The package authenticates its three in-tree inputs by full path at canonical commit `e54523517d0f03e58352e647c403a5af3e525a57`. It needs no external dependencies or generated predecessor files. It regenerates and compares both JSON receipts byte for byte. + +## Open next questions + +Can a rebuilt native provide the changed input phase without a separate head job on each source lane? Start at the port-0 source and backup path in the exact #6726 native word. Test whether a live, already-paid nested source frame can supply part of the new ingress. Keep all helper rows and physical output gauges fixed. Establish the exact source-row equation, restoration and complete price before testing more ports. The original three-port retag already exceeds the whole-call allowance in the [Round 12 discussion](https://github.com/CrocSwap/integer-mult-bounds/discussions/7111#discussioncomment-19537983). + +## Credit + +Credit [#6726](https://github.com/CrocSwap/integer-mult-bounds/pull/6726) for the 111-port native word, [#6834](https://github.com/CrocSwap/integer-mult-bounds/pull/6834) for the inherited paired BIT invoice, [#6980](https://github.com/CrocSwap/integer-mult-bounds/pull/6980) for the query-only schedule and [#7001](https://github.com/CrocSwap/integer-mult-bounds/pull/7001) for the literal E-free caller and full predecessor profile. [#7113](https://github.com/CrocSwap/integer-mult-bounds/pull/7113) is a directed-cost predecessor. The new caller identity and independent replay were prepared for ToikY with material assistance from OpenAI Codex and subagents. Apache-2.0. diff --git a/research/paired-bit-query349-formal-caller/SOURCES.json b/research/paired-bit-query349-formal-caller/SOURCES.json new file mode 100644 index 0000000000..ca7fdf53d2 --- /dev/null +++ b/research/paired-bit-query349-formal-caller/SOURCES.json @@ -0,0 +1,36 @@ +{ + "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/EFREE-CALLER.json.gz", + "usage": "input", + "git_blob": "f022272a8d51ede841778dec76e2bfb24b614d04", + "sha256": "757b3523798f840bdb02028b23708c3416627a99ea09e7a3c4bcdc5cd0c7ce4b" + }, + { + "path": "research/paired-query-only-bit/EFREE-RESULT.json", + "usage": "input", + "git_blob": "575f76487f9999ecc3e7b1b70f9f71bc582ef8a8", + "sha256": "a46b6c6040f75184cab5467656811ad988c216e3bc8e44d595a5015b6e49620b" + }, + { + "path": "research/paired-query-only-bit/retained/inputs/BIT-NATIVE-WORD.json.gz", + "usage": "input", + "git_blob": "b718d6b2848215ad785022106dfa9f871a3d1c0c", + "sha256": "51203e7fc75ba10bd3ac3f8e675759f47e13d262bea66b6600d1e515095cad78" + } + ] +} diff --git a/research/paired-bit-query349-formal-caller/TASK.json b/research/paired-bit-query349-formal-caller/TASK.json new file mode 100644 index 0000000000..96be0b8f6a --- /dev/null +++ b/research/paired-bit-query349-formal-caller/TASK.json @@ -0,0 +1,77 @@ +{ + "schema_version": 1, + "task_id": "bit-helper-contract", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "original_card": { + "id": "bit-helper-contract", + "question": "Can a changed G20 helper path or independent-target split improve the complete BIT moment without losing its physical endpoint?", + "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" + ], + "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." + ], + "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.", + "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." + }, + "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.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "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." + ], + "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." + ], + "overlap_terms": [ + "G20", + "helper split", + "5679", + "5708", + "independent target" + ], + "existing_checks": [ + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "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.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Exact #7001 paired BIT caller endpoint with a changed second LOCAL at every stage and QUERY 349 replaced by ADD.", + "scope_change_reason": "The lead changed from helper split to a literal caller phase reassignment intended to remove one full QUERY.", + "bottleneck_link": "QUERY 349 costs 111 rank-one children. The exact caller identity makes a smaller raw component bill possible if a changed physical LOCAL meets the directed budget.", + "budget_minutes": 60, + "stop_rule": "Verify the literal predecessor, exact candidate, both endpoint reversions and the independently reconstructed raw profile. Stop before a larger physical build unless the paid native bound clears.", + "outcome": "partial", + "evidence": "All 1,444 coefficients in both directions. Predecessor, reverted LOCAL, retained QUERY and source mutation controls. Independent raw price reconstruction. No new kappa.", + "author": "ToikY", + "ai_assistance": "OpenAI Codex and subagents materially assisted search, proof and independent replay.", + "open_questions": [ + { + "question": "Can the 111-port changed LOCAL be built without a per-port head debit?", + "why_it_matters": "The formal endpoint can reduce the raw BIT price only if the changed provider fits the paid and fixed-tape budgets.", + "first_step": "At the port-0 source/backup path, test a live already-paid nested source frame with exact source-row support and return, retaining output gauges and every helper.", + "blocked_by": "No complete physical native, stock, compiler or composed bound has been verified." + } + ] +} diff --git a/research/paired-bit-query349-formal-caller/VERIFY.json b/research/paired-bit-query349-formal-caller/VERIFY.json new file mode 100644 index 0000000000..5e97169f1e --- /dev/null +++ b/research/paired-bit-query349-formal-caller/VERIFY.json @@ -0,0 +1,27 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/paired-query-only-bit/EFREE-CALLER.json.gz", + "research/paired-query-only-bit/EFREE-RESULT.json", + "research/paired-query-only-bit/retained/inputs/BIT-NATIVE-WORD.json.gz", + "research/paired-bit-query349-formal-caller/HEAD-REPLAY.py", + "research/paired-bit-query349-formal-caller/HEAD-REPLAY-price.py", + "research/paired-bit-query349-formal-caller/HEAD-REPLAY.json", + "research/paired-bit-query349-formal-caller/HEAD-REPLAY-price.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Authenticate the exact #7001 inputs and replay both formal caller directions, raw tariff and three failure controls." + } + ] +} diff --git a/research/paired-bit-query349-formal-caller/verify.py b/research/paired-bit-query349-formal-caller/verify.py new file mode 100644 index 0000000000..1eea392769 --- /dev/null +++ b/research/paired-bit-query349-formal-caller/verify.py @@ -0,0 +1,51 @@ +"""Replay both signed caller orientations and the directed raw price.""" + +from importlib.util import module_from_spec, spec_from_file_location +import json +from pathlib import Path +from tempfile import TemporaryDirectory + +PACKAGE = Path(__file__).resolve().parent +BIT = PACKAGE.parent / "paired-query-only-bit" + + +def source_module(filename): + spec = spec_from_file_location(filename, PACKAGE / filename) + module = module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +def verify_receipt(receipt, filename): + expected = (PACKAGE / filename).read_text() + actual = json.dumps(receipt, sort_keys=True, indent=2) + "\n" + if actual != expected: + raise ValueError(f"regenerated receipt differs: {filename}") + + +def main(): + if not __debug__: + raise RuntimeError("Run with assertions enabled") + endpoint = source_module("HEAD-REPLAY.py") + verify_receipt(endpoint.main(BIT), "HEAD-REPLAY.json") + verify_receipt(source_module("HEAD-REPLAY-price.py").price(BIT), "HEAD-REPLAY-price.json") + + key = "EFREE-CALLER.json.gz" + raw = bytearray((BIT / key).read_bytes()) + raw[-1] ^= 1 + with TemporaryDirectory() as directory: + mutated = Path(directory) + (mutated / key).write_bytes(raw) + try: + endpoint.load(mutated, key) + except ValueError as error: + if str(error) != f"sha256 mismatch: {key}": + raise + else: + raise ValueError("accepted changed caller source") + + print("PASS_PAIRED_BIT_QUERY349_FORMAL_CALLER coefficients=1444x2 stages=18 controls=3 no_new_kappa") + + +if __name__ == "__main__": + main() From 7aadacf803deffd79b14a09fd8ccef1429a7ff23 Mon Sep 17 00:00:00 2001 From: ToikY <27568617+ToikY@users.noreply.github.com> Date: Wed, 11 Nov 2026 16:16:29 -0800 Subject: [PATCH 3/3] Reuse the pinned historical replay repair The guide already includes the #7000/#7001 navigation from #7147/#7156. Reuse d2e54af81f9dda6487636b79d4964a2385d89b2b from #7257, also verified in #7339, to run the historical audit at its inspected snapshot. Credit to unpaidmoon for the audit, Dennis for the historical gate, and Matarener for the pinned snapshot precedent. --- .../historical-selected-replay-gap/README.md | 6 +- .../SOURCES.json | 60 +++++++++--------- .../VERIFY.json | 31 +-------- .../historical-selected-replay-gap/verify.py | 63 ++++++++++++++----- 4 files changed, 82 insertions(+), 78 deletions(-) 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")