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/fixed-port-connector-reset/README.md b/research/fixed-port-connector-reset/README.md new file mode 100644 index 0000000000..a7d5ecf7a9 --- /dev/null +++ b/research/fixed-port-connector-reset/README.md @@ -0,0 +1,164 @@ +# Return the original port in a five-source connector reset + +**Exact local result; no new κ.** At unit operation prices the restored +fixed-port connector costs **67 operations** with one owned zero row +before charging for that row. The unchanged restored connector costs +**74**. With a fixed additional provision price ρ ≥ 0 the exact +five-source comparison is **min(74, 67 + ρ)**: provision must cost +strictly less than seven units for a saving. On the retained width-16 +fixture, the complete declared fixed-port bill is **35,060** versus +**40,754** for the original restored connector, a saving of **5,694 +tariff units**. The existing retargeted solution costs 34,944 where +moving the child ports is legal. + +## Contract + +Over F₂ let z be the original arbitrary dirty connector and w one owned +width-L row supplied zero and returned zero. All n sources xⱼ are +immutable; every nonempty mask m has a distinct arbitrary dirty target +yₘ. Return z unchanged and add Aₘ(∑ⱼ∈ₘ Bⱼ xⱼ) to yₘ. The complete +child calls Bⱼ: z += Bⱼ xⱼ and Aₘ: yₘ += Aₘ z always use physical z, +restore their private scratch and heads, and leave other public rows +untouched. The targets are never read or observed during the word. The +maps are arbitrary linear maps, including singular and noncommuting +maps; the word must work for all of them. + +The only extra data operations are F: w += z, G: z += w, and at most +one Z: z := 0. Their positive complete prices are f, g and r. The +uniform prices for a source call and readout are b and a. Row provision +is separate. Without the auxiliary there is no legal reset that preserves +an arbitrary z, so the original #2063 comparator applies. The model +does not bundle operations, use outputs as storage or retarget a child. + +## Exact price of saving and restoring the port + +Let N = 2ⁿ − 1. Save the old z in w, clear z, and traverse the reflected +Gray path from 0 through all N nonzero masks. Toggle the entering source +and read the corresponding output once at each vertex. To leave z at +zero, either close the path with its single final source toggle or +reset z. Then use G and F to return z to its old value and w to zero. + +| Word | Save and clear | End of walk | B | A | F | G | Z | +| --- | --- | --- | ---: | ---: | ---: | ---: | ---: | +| Closed | F, G | One source toggle | N+1 | N | 2 | 2 | 0 | +| Entry reset | F, Z | One source toggle | N+1 | N | 2 | 1 | 1 | +| Exit reset | F, G | Z | N | N | 2 | 2 | 1 | + +All three include the final G, F. Each readout uses z at its intended +mask and never has to cancel a contribution from old z. No map is +commuted, inverted or moved to w. + +**Lower bound, including interleaved moves and repeated readouts.** +Specialize to scalar identity maps with independent source bits and an +independent original connector bit. Let α = (α_z, α_w) be the +coefficients of that original bit in the two rows. The pair cannot +become 00: the source bits are independent and no output can be read +back. The clean combination s = α_w z + α_z w starts and ends at 0. +Both F and G preserve s while changing coordinates. A B call can +toggle one source bit in s or do nothing. A legal Z can only send s to +0: it requires α_w = 1 and then puts α_z = 0 and z = 0. + +If k ≥ 1 targets each receive exactly one readout, those readouts need +α = 01 and k distinct nonzero masks in s. At least k B calls are needed +to create them, and the other targets need at least two readouts each, +so A ≥ 2N − k. If there are exactly k B calls, each must produce one +of those distinct nonzero masks for the first time; the single reset +must occur after the last one to return s to zero. With no B left, +all k once-read targets must already have been read before that reset. + +The coefficient path must go from 10 through 01 and back to 10. Entering +01 takes F and then either G or Z; returning takes G and F. Thus a word +without a reset needs at least k+1 B and two F, two G. A word with a +reset and at least k+1 B needs at least two F and one G. A word with a +reset and exactly k B still needs two F and two G because its reset is +used for closure, after the path has already entered 01. This yields + +```text +price >= b k + a (2N - k) + 2f + g + min(b+g, b+r, g+r). +``` + +For a ≥ b this bound is minimized at k=N, and the three Gray words +attain its minimum. This proves the exact price among all legal words +using at least one once-read target, without assuming a single clean +excursion. A word without any once-read target needs at least 2N A and +n B because every source must influence its own one-source mask. For +five sources at unit prices this lower bound is also 67, so the +wrapped optimum is global in that tariff. Paying ρ for any word using +w then gives the exact optional-provision comparison above. At general +prices the no-singleton bound need not settle the global optimum. + +## Pinned width-16 comparison + +The retained #1954 fixture uses five source permutations and 31 +permuted 13-tap readout maps. All 36 maps fix the all-ones vector. +Restricting every row to that one-dimensional subspace gives exactly +the identity test above, even for a word chosen specifically for these +maps. The lower bound does not transfer to every fixed map instance. +For example, two complementary projections used as the two source +maps and as the first two readouts (with identity for the combined +mask) let three outputs share one clean value. A ten-operation +fixed-port word there beats the generic eleven-operation once-read +bound at two sources. The replay checks all 4,096 inputs to this example. + +Keep #5372's charge of 26,704 for the shared tables and original rows, +403 for mask descriptors, and 58 for allocation, 16 storage cells and +16 initial zero writes. The complete source and readout prices are 29 +and 221. Charge each extra full-row XOR or reset 16 operations or +writes plus the same 13-unit action descriptor. The entry-reset word +costs 7,895 in actions (32×29 + 31×221 + 4×29). No word without a +once-read target can beat the action bill, since 62×221 + 5×29 is +13,847. Adding all retained fixed charges gives 35,060. This exact +total comparison stipulates those charges as fixed for the auxiliary +route. It does not optimize other layout or compilation tariffs. + +The original restored comparator is 40,754 by repricing all 16 of +#2063's exact profiles and retaining the original common charges. +Retargeting the children instead would avoid the four port actions +and cost 34,944, as in #5372. The wrapper costs 116 more and is useful +only when those ports must stay fixed. + +## Verification + +Run with CPython 3.12 from a clean checkout or the official Git-free +export (which includes the three declared inputs): + +```sh +python3.12 -I -B research/fixed-port-connector-reset/verify.py +``` + +[RESULT.json](RESULT.json) records 24 symbolic Gray words, 12 exact +shortest-word checks for one or two sources, the fixed-map counterexample, +and each of the three literal words on all 608 width-16 input basis +columns. The latter use the pinned fixture maps and a separate +dense-matrix target oracle. Seven controls reject lost dirty values, +incorrect closure or return, unpaid zero initialization, or a second +reset. The three comparison inputs are checked against the hashes in +[SOURCES.json](SOURCES.json). + +## Open next questions + +A multiplication caller still has to supply the fixed ports, an owned +zero row outside the child scratch, complete prices for its moves, +reset or closing call, and the full layout, tape, stock and recursive +bill. The width-16 tariff is a checked local instance. No physical +supplier, selected caller or changed κ follows. A useful next step is +to pin one actual caller and account for that row for the entire +interval before attempting a larger construction. + +## Credit + +Nick Petalas's [#7324](https://github.com/CrocSwap/integer-mult-bounds/pull/7324) +at `fd573cfe4e9714706b01f0534584e6f5032dc858` supplies the disposable +reset and open Gray schedule. Ross Richardson's +[#934](https://github.com/CrocSwap/integer-mult-bounds/pull/934) lineage +supplies the generic dirty connector, Adam Gall's +[#2063](https://github.com/CrocSwap/integer-mult-bounds/pull/2063) its exact +restored tariff, Cinna Davis's +[#1954](https://github.com/CrocSwap/integer-mult-bounds/pull/1954) the +fixture, and Ali Romman's +[#5372](https://github.com/CrocSwap/integer-mult-bounds/pull/5372) the +paid clean-row Gray cycle and retained invoice. +[#2182](https://github.com/CrocSwap/integer-mult-bounds/pull/2182) is a +separate fixed-port precedent with a second arbitrary dirty row and +paired readouts. OpenAI Codex and ChatGPT Pro materially assisted the +proof, adversarial review and exact replay. Apache-2.0. diff --git a/research/fixed-port-connector-reset/RESULT.json b/research/fixed-port-connector-reset/RESULT.json new file mode 100644 index 0000000000..3f0b72f6f6 --- /dev/null +++ b/research/fixed-port-connector-reset/RESULT.json @@ -0,0 +1,201 @@ +{ + "fixed_singular_counterexample_inputs": 4096, + "fixture": { + "all_witness_counts": { + "closed": { + "A": 31, + "B": 32, + "F": 2, + "G": 2, + "Z": 0 + }, + "entry_reset": { + "A": 31, + "B": 32, + "F": 2, + "G": 1, + "Z": 1 + }, + "exit_reset": { + "A": 31, + "B": 31, + "F": 2, + "G": 2, + "Z": 1 + } + }, + "basis_columns_per_word": 608, + "call_bill": 7895, + "charged_entry_reset_invoice": { + "action_descriptors": 871, + "allocation_release_descriptors": 26, + "fresh_row_cells": 16, + "mask_control_descriptors": 403, + "output_updates": 6448, + "shared_map_table_bits": 26112, + "shared_row_cells": 592, + "source_updates": 512, + "wrapper_reset_writes": 16, + "wrapper_row_xors": 48, + "zero_writes": 16 + }, + "dirty_comparator": 40754, + "fixed_map_identity_line_count": 36, + "mutations_rejected": 7, + "premium_vs_retargeting": 116, + "retargeted_comparator": 34944, + "saving_vs_dirty": 5694, + "total": 35060 + }, + "scope": "exact declared fixed-port connector model; no new kappa", + "small_exact_costs": [ + { + "minimum": 29, + "n": 1, + "prices_B_A_F_G_Z": [ + 2, + 5, + 3, + 7, + 20 + ], + "required_singleton": 1 + }, + { + "minimum": 23, + "n": 1, + "prices_B_A_F_G_Z": [ + 2, + 5, + 3, + 7, + 1 + ], + "required_singleton": 1 + }, + { + "minimum": 27, + "n": 1, + "prices_B_A_F_G_Z": [ + 7, + 9, + 2, + 3, + 1 + ], + "required_singleton": 1 + }, + { + "minimum": 7, + "n": 1, + "prices_B_A_F_G_Z": [ + 1, + 1, + 1, + 1, + 1 + ], + "required_singleton": 1 + }, + { + "minimum": 43, + "n": 2, + "prices_B_A_F_G_Z": [ + 2, + 5, + 3, + 7, + 20 + ], + "required_singleton": 1 + }, + { + "minimum": 37, + "n": 2, + "prices_B_A_F_G_Z": [ + 2, + 5, + 3, + 7, + 1 + ], + "required_singleton": 1 + }, + { + "minimum": 59, + "n": 2, + "prices_B_A_F_G_Z": [ + 7, + 9, + 2, + 3, + 1 + ], + "required_singleton": 1 + }, + { + "minimum": 11, + "n": 2, + "prices_B_A_F_G_Z": [ + 1, + 1, + 1, + 1, + 1 + ], + "required_singleton": 1 + }, + { + "minimum": 43, + "n": 2, + "prices_B_A_F_G_Z": [ + 2, + 5, + 3, + 7, + 20 + ], + "required_singleton": 3 + }, + { + "minimum": 37, + "n": 2, + "prices_B_A_F_G_Z": [ + 2, + 5, + 3, + 7, + 1 + ], + "required_singleton": 3 + }, + { + "minimum": 59, + "n": 2, + "prices_B_A_F_G_Z": [ + 7, + 9, + 2, + 3, + 1 + ], + "required_singleton": 3 + }, + { + "minimum": 11, + "n": 2, + "prices_B_A_F_G_Z": [ + 1, + 1, + 1, + 1, + 1 + ], + "required_singleton": 3 + } + ], + "symbolic_witnesses": 24, + "unit_original": 74, + "unit_provision_break_even": 7, + "unit_with_owned_zero": 67 +} diff --git a/research/fixed-port-connector-reset/SOURCES.json b/research/fixed-port-connector-reset/SOURCES.json new file mode 100644 index 0000000000..555e893ad1 --- /dev/null +++ b/research/fixed-port-connector-reset/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": "bc1a3a0982948426f7611a63630e9fcfd03e0906", + "path": "research/clean-connector-per-mask-seede54e/verify.py", + "sha256": "8685db5771326f22fd4136879a2852b7505a9d483a474a8d62ea33869bd80617", + "usage": "input" + }, + { + "git_blob": "ed0379b63721d9ea790a79af9677005111614765", + "path": "research/connector-all-tariff-optimum/RESULT.json", + "sha256": "15b015913dda14b7516bb4aeee798ab9a4593d5bbd59d4813ec8911e89b6c83a", + "usage": "input" + }, + { + "git_blob": "d06dacdedf95ac55f6317344e5ecdfb2048816d8", + "path": "research/clean-connector-gray-optimum/RESULT.json", + "sha256": "7f21f666bdeb56a8cb90c69f6feceac35cfdf8579714ba0bd76d464c5cc655d9", + "usage": "input" + } + ], + "schema_version": 1 +} diff --git a/research/fixed-port-connector-reset/TASK.json b/research/fixed-port-connector-reset/TASK.json new file mode 100644 index 0000000000..35d4ed6b61 --- /dev/null +++ b/research/fixed-port-connector-reset/TASK.json @@ -0,0 +1,62 @@ +{ + "actual_scope": "All nonzero masks for a fixed-port restored F2 connector, an owned zero row returned zero, two directed row XORs, at most one reset, and positive uniform child prices. Exact five-source unit result and a pinned width-16 tariff fixture. No physical caller or kappa claim.", + "ai_assistance": "OpenAI Codex and ChatGPT Pro materially assisted formulation, adversarial proof review, and exact replay.", + "author": "Clear1nsight", + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "bottleneck_link": "Charge preservation of the original dirty connector before importing a reset-based map schedule into any supplier.", + "budget_minutes": 60, + "evidence": "A two-row clean-form invariant gives an arbitrary-word lower bound; three exact Gray words attain it for uniform readout price at least source price. The exact unit five-source wrapped bill is 67 before provision. Full pinned fixture costs 35060, down 5694 in its declared tariff.", + "open_questions": [ + { + "blocked_by": "No selected supplier binding, full stock/routing cost, or native compiler integration is supplied here.", + "first_step": "Pin one caller and bind the row lifetime, port layout, both XORs, reset or closing toggle, and child-call prices to its compiler and tape.", + "question": "Which actual multiplication caller can supply and return the matching clean row at its existing fixed ports?", + "why_it_matters": "The local price margin cannot change kappa without a compatible physical caller and complete recursive invoice." + } + ], + "original_card": { + "acceptance_gate": "State which fixed-alphabet premise changes and charge its implementation; do not declare it free. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "allowed_variations": [ + "Choose one additional operation and a small source count for its first counterexample." + ], + "bottleneck_link": "A new legal connector operation could change recursive interface cost; a larger census in the same alphabet is a separate side result.", + "first_experiment": "Add exactly one legally priced operation and test a tiny dirty-input instance before enumerating larger cases.", + "first_step": { + "command": [ + "python3", + "-B", + "research/universal-connector-boundary/verify.py" + ], + "expected": "PASS_UNIVERSAL_CONNECTOR_BOUNDARY", + "inspect": "Reproduce the 945-pairing control, then read Exact interface to list the allowed calls.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "id": "connector-alphabet-change", + "methods": [ + "Construct and charge a legal extra operation on a minimal instance.", + "Prove a target-specific bound after adding one specified operation family." + ], + "overlap_terms": [ + "universal connector", + "source-toggle", + "connector alphabet" + ], + "question": "Does one explicit extension of the connector alphabet offer a favorable completed budget?", + "scope_change_triggers": [ + "Keeping the alphabet and only increasing the source count; record this as a changed assignment.", + "Extending a source-count census without naming a supplier/interface decision it could change; audit #2973 pruning concerns before relying on the affected predecessor exclusions." + ], + "starting_points": [ + "docs/research/research-family-status.md", + "research/universal-connector-boundary/README.md", + "certificates/selected-result.json" + ] + }, + "outcome": "completed", + "priority_revision": 8, + "schema_version": 1, + "scope_change_reason": "Restore the original fixed physical connector using one paid clean row, two directed XOR operations and at most one reset. #7324 consumes the connector; #5372 retargets the child calls.", + "scope_status": "changed", + "stop_rule": "One restore contract; small finite shortest-word tests at n<=2; all basis columns of the retained length-16 fixture. Do not start recursive integration without a named caller and complete physical bill.", + "task_id": "connector-alphabet-change" +} diff --git a/research/fixed-port-connector-reset/VERIFY.json b/research/fixed-port-connector-reset/VERIFY.json new file mode 100644 index 0000000000..1755ac4f45 --- /dev/null +++ b/research/fixed-port-connector-reset/VERIFY.json @@ -0,0 +1,23 @@ +{ + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "checks": "Exact witnesses and small shortest words, fixed-map limit control, pinned 16-bit fixture basis and complete tariff.", + "timeout_seconds": 45 + } + ], + "inputs": [ + "research/clean-connector-per-mask-seede54e/verify.py", + "research/connector-all-tariff-optimum/RESULT.json", + "research/clean-connector-gray-optimum/RESULT.json" + ], + "python": "3.12", + "requirements": [], + "schema_version": 1, + "status": "ready" +} diff --git a/research/fixed-port-connector-reset/verify.py b/research/fixed-port-connector-reset/verify.py new file mode 100644 index 0000000000..48d31663b5 --- /dev/null +++ b/research/fixed-port-connector-reset/verify.py @@ -0,0 +1,274 @@ +"""Exact fixed-port restoration witnesses and source-bound controls. Apache-2.0.""" + +from argparse import ArgumentParser +from collections import Counter +from hashlib import sha256 +from heapq import heappop, heappush +from itertools import product +import json +from pathlib import Path +from runpy import run_path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +FIXTURE = "research/clean-connector-per-mask-seede54e/verify.py" +BASELINE = "research/connector-all-tariff-optimum/RESULT.json" +RETARGET = "research/clean-connector-gray-optimum/RESULT.json" +KINDS = "BAFGZ" +MODES = ("closed", "entry_reset", "exit_reset") + + +def require(ok, detail): + if not ok: + raise ValueError(detail) + + +def json_at(path): + return json.loads(path.read_text(encoding="utf-8")) + + +def input_paths(): + pins = {row["path"]: row["sha256"] for row in json_at(HERE / "SOURCES.json")["files"] + if row["usage"] == "input"} + require(set(pins) == {FIXTURE, BASELINE, RETARGET}, "unexpected source closure") + for name, digest in pins.items(): + require(sha256((ROOT / name).read_bytes()).hexdigest() == digest, f"changed input: {name}") + + +def gray_word(n, mode): + require(n >= 1 and mode in MODES, "invalid wrapper") + vertices = [0] + for i in range(n): + vertices += [x | (1 << i) for x in reversed(vertices)] + word = [("F", 0), ("Z" if mode == "entry_reset" else "G", 0)] + for u, v in zip(vertices, vertices[1:]): + bit = u ^ v + require(bit.bit_count() == 1, "nonedge in Gray path") + word.extend((("B", bit.bit_length() - 1), ("A", v))) + terminal = vertices[-1] + require(terminal.bit_count() == 1, "closed Gray path needs one closing toggle") + word.append(("Z", 0) if mode == "exit_reset" else ("B", terminal.bit_length() - 1)) + return word + [("G", 0), ("F", 0)] + + +def execute(word, sources, old_z, outputs, backing_w, b_map, a_map, *, zero_owned=True): + """All child calls use z, never w. Allocation clears arbitrary backing contents.""" + z, w = old_z, (0 if zero_owned else backing_w) + y = list(outputs) + resets = 0 + for op, arg in word: + if op == "B" and 0 <= arg < len(sources): + z ^= b_map(arg, sources[arg]) + elif op == "A" and 1 <= arg <= len(y): + y[arg - 1] ^= a_map(arg, z) + elif op == "F": + w ^= z + elif op == "G": + z ^= w + elif op == "Z": + resets += 1 + require(resets <= 1, "second reset") + z = 0 + else: + raise ValueError(f"unknown fixed-port operation: {(op, arg)}") + return z, w, tuple(y) + + +def counts(word): + c = Counter(op for op, _ in word) + return dict(zip(KINDS, (c[op] for op in KINDS))) + + +def best_singleton(n, prices): + b, a, f, g, r = prices + return ((1 << n) - 1) * (a + b) + 2 * f + g + min(b + g, b + r, g + r) + + +def symbolic_replay(): + total = 0 + for n in range(1, 9): + targets = tuple(range(1, 1 << n)) + source = tuple(1 << j for j in range(n)) + old = 1 << n + for mode in MODES: + word = gray_word(n, mode) + result = execute(word, source, old, (0,) * len(targets), 0, lambda j, x: x, lambda m, z: z) + expected = dict(zip(KINDS, (len(targets) + (mode != "exit_reset"), len(targets), + 2, 1 + (mode != "entry_reset"), int(mode != "closed")))) + require(result == (old, 0, targets) and counts(word) == expected, "symbolic wrapper") + require(Counter(i for op, i in word if op == "A") == Counter(targets), "literal singleton calls") + total += 1 + return total + + +def exact_small(n, singleton, prices): + """Dijkstra over exact coefficients with one distinguished once-read target. + + Other targets may be read any number of times. In the chosen target's row, + zero means unread: its only legal read produces the required nonzero mask. + """ + b, a, f, g, r = prices + masks = tuple(range(1, 1 << n)) + old = 1 << n + start = (old, 0, (0,) * len(masks), False) + dist, heap = {start: 0}, [(0, start)] + while heap: + cost, state = heappop(heap) + if cost != dist[state]: + continue + z, w, ys, reset = state + if (z, w, ys) == (old, 0, masks): + return cost + edges = [(b, (z ^ (1 << j), w, ys, reset)) for j in range(n)] + edges.extend(((f, (z, w ^ z, ys, reset)), (g, (z ^ w, w, ys, reset)))) + if not reset and w & old: + edges.append((r, (0, w, ys, True))) + for i, m in enumerate(masks): + if m != singleton or (ys[i] == 0 and z == m): + dest = ys[:i] + (ys[i] ^ z,) + ys[i + 1:] + edges.append((a, (z, w, dest, reset))) + for weight, dest in edges: + new = cost + weight + if dest not in dist or new < dist[dest]: + dist[dest] = new + heappush(heap, (new, dest)) + raise ValueError("no endpoint in finite state graph") + + +def exact_controls(): + reports = [] + # The three strict minimizers and a unit tie. Uniform source/readout + # prices make masks 1 and 3 representatives of both weights at n=2. + price_vectors = ((2, 5, 3, 7, 20), (2, 5, 3, 7, 1), (7, 9, 2, 3, 1), (1, 1, 1, 1, 1)) + for n, m in ((1, 1), (2, 1), (2, 3)): + for p in price_vectors: + found = exact_small(n, m, p) + require(found == best_singleton(n, p), "small exact optimum mismatch") + reports.append({"n": n, "required_singleton": m, "prices_B_A_F_G_Z": p, "minimum": found}) + return reports + + +def fixed_map_control(): + # On these particular singular maps the three A calls can share one + # connector value. This rebuts an unrestricted fixed-instance lower bound. + word = [("F", 0), ("G", 0), ("B", 0), ("B", 1), ("A", 1), ("A", 2), + ("A", 3), ("Z", 0), ("G", 0), ("F", 0)] + for x, y, old, a, b, c in product(range(4), repeat=6): + p, q = x & 1, y & 2 + got = execute(word, (x, y), old, (a, b, c), 0, + lambda j, v: v & (1 << j), lambda m, v: v & m) + require(got == (old, 0, (a ^ p, b ^ q, c ^ p ^ q)), "fixed singular-map control") + require(len(word) == 10 < best_singleton(2, (1,) * 5), "control must be cheaper") + return 4**6 + + +def dense(rows, value): + return sum(((r & value).bit_count() & 1) << i for i, r in enumerate(rows)) + + +def fixture_replay(): + source = run_path(str(ROOT / FIXTURE)) + length, masks = source["L"], source["MASKS"] + require(length == 16 and masks == tuple(range(1, 32)), "fixture identity") + b_map = lambda j, x: source["permute"](x, source["B_MAPS"][j]) + a_map = lambda m, z: source["apply_output_map"](z, m - 1) + ones = (1 << length) - 1 + require(all(b_map(j, ones) == ones for j in range(5)) and + all(a_map(m, ones) == ones for m in masks), "the fixture lost the common identity line") + + b_rows = [tuple(1 << col for col in p) for p in source["B_MAPS"]] + kernel = source["a_rows"]() + a_rows = {m: tuple(sum(1 << p[i] for i in range(length) if r & (1 << i)) for r in kernel) + for m, p in zip(masks, source["Q_MAPS"], strict=True)} + + def expected(xs, old, out): + images = [dense(r, x) for r, x in zip(b_rows, xs, strict=True)] + result = list(out) + for m in masks: + total = 0 + for j, v in enumerate(images): + if m & (1 << j): + total ^= v + result[m - 1] ^= dense(a_rows[m], total) + return old, 0, tuple(result) + + words = {mode: gray_word(5, mode) for mode in MODES} + rows = 5 + 1 + len(masks) + 1 + for column in range(rows * length): + inputs = [0] * rows + inputs[column // length] = 1 << (column % length) + xs, old, out, backing = inputs[:5], inputs[5], inputs[6:-1], inputs[-1] + want = expected(xs, old, out) + for word in words.values(): + got = execute(word, xs, old, out, backing, b_map, a_map) + require(got == want, f"literal fixture basis column {column}") + + old, out, backing = ones, (0,) * len(masks), ones + xs = (1, 2, 4, 8, 16) + want = expected(xs, old, out) + entry, closed = words["entry_reset"], words["closed"] + mutants = (("missing save", entry[1:], True), + ("missing entry reset", entry[:1] + entry[2:], True), + ("missing close", closed[:-3] + closed[-2:], True), + ("missing restore", entry[:-2] + entry[-1:], True), + ("dirty release", entry[:-1], True), + ("missing allocation zeroing", entry, False)) + for label, word, zero in mutants: + require(execute(word, xs, old, out, backing, b_map, a_map, zero_owned=zero) != want, label) + try: + execute([("Z", 0)] + entry, xs, old, out, backing, b_map, a_map) + except ValueError as exc: + require(str(exc) == "second reset", "wrong reset rejection") + else: + raise ValueError("second reset accepted") + + ref = json_at(ROOT / RETARGET) + retained = ref["invoice"] + n = counts(entry) + actions = sum(n.values()) + invoice = {k: retained[k] for k in ("shared_map_table_bits", "shared_row_cells", + "mask_control_descriptors", "allocation_release_descriptors", + "fresh_row_cells", "zero_writes")} + invoice.update(source_updates=n["B"] * length, output_updates=n["A"] * length * 13, + wrapper_row_xors=(n["F"] + n["G"]) * length, + wrapper_reset_writes=n["Z"] * length, action_descriptors=actions * 13) + a, b = length * 13 + 13, length + 13 + call_bill = sum(n[op] * (a if op == "A" else b) for op in KINDS) + profiles = json_at(ROOT / BASELINE)["pareto_profiles"] + require(len(profiles) == 16 and all(len(v) == 36 for v in profiles), "retained tariff frontier") + dirty = invoice["shared_map_table_bits"] + invoice["shared_row_cells"] + dirty += min(sum(v[i] * (b if i < 5 else a) for i in range(36)) for v in profiles) + price = sum(invoice.values()) + require((call_bill, price, dirty, ref["new_clean_cost"]) == (7895, 35060, 40754, 34944), + "complete fixed-port tariff comparison") + require(call_bill == best_singleton(5, (b, a, b, b, b)) < 62 * a + 5 * b, + "fixture requires a global call-price comparison") + return {"basis_columns_per_word": rows * length, "fixed_map_identity_line_count": 36, + "mutations_rejected": len(mutants) + 1, "all_witness_counts": {k: counts(v) for k, v in words.items()}, + "charged_entry_reset_invoice": invoice, "call_bill": call_bill, "total": price, + "dirty_comparator": dirty, "retargeted_comparator": ref["new_clean_cost"], + "saving_vs_dirty": dirty - price, "premium_vs_retargeting": price - ref["new_clean_cost"]} + + +def replay(): + input_paths() + unit = best_singleton(5, (1,) * 5) + require(unit == 62 + 5 == 67, "global unit cost with an owned zero row") + return {"scope": "exact declared fixed-port connector model; no new kappa", + "symbolic_witnesses": symbolic_replay(), "small_exact_costs": exact_controls(), + "fixed_singular_counterexample_inputs": fixed_map_control(), + "unit_with_owned_zero": unit, "unit_original": 74, + "unit_provision_break_even": 74 - unit, "fixture": fixture_replay()} + + +if __name__ == "__main__": + parser = ArgumentParser(description=__doc__) + parser.add_argument("--write-result", type=Path, help="write a new exact receipt") + args = parser.parse_args() + result = json.dumps(replay(), indent=2, sort_keys=True) + "\n" + if args.write_result: + with args.write_result.open("x", encoding="utf-8") as f: + f.write(result) + else: + require((HERE / "RESULT.json").read_text(encoding="utf-8") == result, "changed exact receipt") + print("PASS_FIXED_PORT_CONNECTOR_RESET unit=67 baseline=74 break_even=7 fixture=35060 saving=5694 no_new_kappa") 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")