diff --git a/docs/ci-verification.md b/docs/ci-verification.md index 63ba3e9aa8..52b62d0481 100644 --- a/docs/ci-verification.md +++ b/docs/ci-verification.md @@ -1,8 +1,25 @@ # CI verification -## Current selected-family replay: #6030 +## Current selected-family replay: #7000 with #7001 The [selected record](../certificates/selected-result.json) binds conditional +κ = 0.00363005817 to the [application review](research/pr-intake-evidence/pr7000-application/PROOF-REVIEW.md), +[validation receipts](research/pr-intake-evidence/pr7000-application/VALIDATION.json), +and [explicit source closure](../certificates/frontier7000-source.json). +`make frontier7000-verify` follows that exact-source selected replay. The review +reuses eleven authenticated preceding executions and records seven fresh serial +application, scalar and complete native-catalogue executions. The earlier +monolithic timeout is retained separately and is not completed coverage. +Consult the receipts for exact commands, source heads and limits. + +The five inherited framework assumptions remain. No complete uniform word, +literal multiplier execution, independent human proof or formal-kernel proof +is asserted. Routine research submissions do not need to rerun this +selected-family replay. The sections below preserve historical checkpoints. + +## Historical selected-family replay: #6030 + +The [historical checkpoint](../certificates/checkpoints/frontier6030.json) binds conditional κ = 0.003125804 to the [proof review](research/pr-intake-evidence/pr6030-audit/PROOF-REVIEW.md), [validation receipts](research/pr-intake-evidence/pr6030-audit/VALIDATION.json), and [explicit source closure](../certificates/frontier6030-source.json). diff --git a/research/bit-generalized-summary-support/PROOF.md b/research/bit-generalized-summary-support/PROOF.md new file mode 100644 index 0000000000..2b6429ba19 --- /dev/null +++ b/research/bit-generalized-summary-support/PROOF.md @@ -0,0 +1,120 @@ +# Generalized support bound for selected BIT summary descents + +Fix the paired #7001 native word, its rational chart catalogue and +its monotone source flow. The only new downward transports are +collectors descending to chart zero. A new collector can use +earlier descended values. Take its main-coordinate row modulo +the span of those earlier values and all retained summary rows. +Co-chart XOR, zero initialization and monotone transport preserve +support on the original lines contained in the current chart +in this quotient. Subtract earlier rows in chronological order +to obtain supported innovations without changing the span of +all rows available for recovery. Timing and recovery are otherwise +overgranted. + +The nine literal summary rows projected onto 111 original main +coordinates generate a binary code C of dimension nine. Its +minimum nonzero weight is 48 and its minimum support union for +a two-dimensional subspace is 75. The 111 coordinate functionals +are distinct and nonzero on C. The replay verifies these facts +from the pinned word and checks all catalogue capacities and +2,862 public monotone MOVEs. + +## Paid rank budget + +Let k of the nine summary rows be replaced, at the target +κ=0.0040075385047236, and write p=1−κ. Require at least 5/3 +net paid units per native copy. This is a relaxation of the +full target deficit per 36 repeated copies. The cost of the +k old descents is k·7^p. All catalogue ranks are at most eight. +For total new rank R, the cost is at least R·8^(−κ). +If R≥7k−1, the saving is at most +7^(−κ)+(7k−1)(7^(−κ)−8^(−κ)), which is at most +1+62κ/7 by the mean value theorem and log(8/7)≤1/7. +This is strictly below 5/3. Therefore R≤7k−2. + +## Two support tests + +Choose linear XOR recovery for the k independent summary +rows modulo the retained rows. Cancel the coefficients of +the k−t highest-rank collectors in those recovery equations. +At least t independent target combinations remain. Select +a t-dimensional subspace of their codeword representatives +in C. Every column outside the union of the remaining +collectors is zero in this subspace. + +The support union must have size at least d_t, the minimum +support of a t-dimensional subspace of C. For t≥2, +averaging the two-dimensional subspaces gives the bound +ceil((2^t−1)·75/(3·2^(t−2))). Indeed, a nonzero coordinate +functional on a t-space occurs in a fraction +3·2^(t−2)/(2^t−1) of its two-dimensional subspaces. +Distinct nonzero columns also give d_t≥112−2^(9−t), +since the kernel of restriction to a t-space has dimension +9−t. Use the larger lower bound. + +There is a second necessary condition on the sum I of +the remaining collectors' support sizes. A rank-t linear +map of the original nine-dimensional column space can +repeat an output column at most 2^(9−t) times. At least +112−2^(9−t) output columns are nonzero. With N remaining +collectors, each nonzero column incident to at most h +collectors is the sum of at most h of the N coefficient +vectors. There are at most sum(j=1..h, binomial(N,j)) +possible subsets. Thus for each h≥0 the number of columns +incident to more than h collectors is at least + +```text +max(0, 112−2^(9−t) − 2^(9−t)·sum(j=1..h, binomial(N,j))). +``` + +Summing these bounds over h bounds I below. The catalogue +capacities bound I above, even with overlapping charts +overcounted. This argument also permits a collector to +use only part of the support of its chart. + +## Exact enumeration and pair test + +Enumerate sorted rank histograms within R≤7k−2. Keep only +profiles whose tail after dropping k−1 collectors can +cover 48 lines. This precondition is necessary. The +enumeration exhausts 18, 74, 270 and 782 histograms for +k=6,7,8,9. The two support tests leave zero, zero, one and +three profiles, respectively. + +The k=8 profile has nine rank-six transports. Two k=9 +profiles have ten rank-six transports or one rank-seven +and nine rank-six transports. In each of these three +profiles there are k+1 transports. Cancel every transport +except a chosen pair of rank-six collectors. This imposes +k−1 homogeneous conditions on k target coefficients and +leaves a nonzero codeword supported in the union of that +pair. Equal masks cover at most 30 lines and fail immediately. +For every one of the 16,110 distinct pairs, the columns +outside that union have rank nine. Hence no nonzero +codeword can be supported in the pair and all three +profiles fail. + +The final profile has ten rank-six collectors and one rank-one +collector. Cancel eight rank-six collectors and retain any two +rank-six collectors plus the rank-one collector. The eight +conditions leave a nonzero codeword. Its support must lie in +the union of the pair and at most one extra coordinate, since +each rank-one chart contains at most one original line. A +repeated pair plus one line covers at most 31 coordinates. + +For a distinct pair, let D be the matrix of columns outside +the pair. The condition requires rank(D)<9 or a column whose +deletion drops rank. The verifier tracks the input columns in +each row reduction. Each dependent column yields a relation +with its own last nonzero index. These relations form a basis +of the column kernel, so a column lies in some relation exactly +when it appears in a basis relation. Deleting a column lowers +rank precisely when it lies in no relation. All 16,110 matrices +have rank nine and zero such columns. A separate direct codeword +enumeration over the same pairs also finds zero with uncovered +weight at most one. This excludes the last profile. The extra +line is allowed to differ arbitrarily between pairs in the test. + +The exclusion leaves smaller paid savings, changed chart spaces, +nonmonotone transports and new target contracts open. diff --git a/research/bit-generalized-summary-support/README.md b/research/bit-generalized-summary-support/README.md new file mode 100644 index 0000000000..0779c12333 --- /dev/null +++ b/research/bit-generalized-summary-support/README.md @@ -0,0 +1,46 @@ +# Generalized support bounds for joint BIT summary replacements + +**NO VERIFIED GAIN.** On the exact selected paired #7001 word, +no six- through nine-summary replacement under the fixed monotone +catalogue can save the target 5/3 paid units per native copy. +The final profile has ten rank-six collectors and one rank-one +collector. It fails even with an arbitrary extra line. + +The summary code has minimum two-dimensional support 75 and +111 distinct nonzero columns. The proof combines generalized +support, column incidence and a projected rank test on all +16,110 distinct rank-six chart pairs. [Proof](PROOF.md) + +## Replay + +Use a clean checkout and CPython 3.12. + +```sh +python3.12 -B scripts/research_package.py --package research/bit-generalized-summary-support +``` + +The verifier reconstructs the weights and chart masks from the +canonical pinned BIT word, exhausts the four histogram domains, +and checks all pair exclusions by rank of the uncovered columns, +including the effect of deleting any one column. Positive and +negative projection controls run from the same word. +The exact dependency is the existing selected BIT word. [Selected BIT package](../paired-query-only-bit/README.md) + +## Scope and credit + +[#7146](https://github.com/CrocSwap/integer-mult-bounds/pull/7146) +covers up to four summaries and the five-summary target scope. +This package covers larger joint changes with different support +bounds. Ali Romman's #5421 supplied the owned relations. +DreamingOfClouds, zxv, CubeJerry and the retained authors supplied +the native and paired-controller lineage. Substantial OpenAI Codex +and subagent assistance. Apache-2.0. + +## Open next questions + +Can an existing public MOVE be redirected to import a summary +row across a nonmonotone chart change? Start with a nested, +equal-paid-rank redirect in the literal word. Check source +availability, exact output rows and restoration before recomputing +the paid and ordinary invoices. This proof fixes monotone public +transport, so that changed source flow is outside its scope. diff --git a/research/bit-generalized-summary-support/RECEIPT.json b/research/bit-generalized-summary-support/RECEIPT.json new file mode 100644 index 0000000000..743fa9b24a --- /dev/null +++ b/research/bit-generalized-summary-support/RECEIPT.json @@ -0,0 +1,125 @@ +{ + "dependencies": { + "research/paired-query-only-bit/retained/inputs/BIT-NATIVE-WORD.json.gz": "51203e7fc75ba10bd3ac3f8e675759f47e13d262bea66b6600d1e515095cad78" + }, + "profiles": { + "6": { + "survivors": [], + "tested": 18 + }, + "7": { + "survivors": [], + "tested": 74 + }, + "8": { + "survivors": [ + [ + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ] + ], + "tested": 270 + }, + "9": { + "survivors": [ + [ + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 1 + ], + [ + 7, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ] + ], + "tested": 782 + } + }, + "rank_six_pair_complement_ranks": { + "9": 16110 + }, + "rank_six_pair_deletion_rank_drops": { + "0": 16110 + }, + "remaining_profiles": [], + "required_support_by_dimension": { + "1": 48, + "2": 75, + "3": 88, + "4": 94, + "5": 97, + "6": 104, + "7": 108, + "8": 110, + "9": 111 + }, + "status": "PASS_GENERALIZED_BIT_SUMMARY_SUPPORT", + "weights": { + "d1": 48, + "d2": 75, + "distinct_columns": 111, + "enumerated_pairs": 130305, + "maximum_column_multiplicity": 1, + "minimizing_subspaces": 216, + "status": "PASS_GENERALIZED_SUMMARY_SUPPORT", + "union_weight_histogram": { + "75": 648, + "76": 2466, + "77": 4236, + "78": 4494, + "79": 5715, + "80": 10692, + "81": 14526, + "82": 12462, + "83": 10452, + "84": 14700, + "85": 16098, + "86": 10854, + "87": 6408, + "88": 6315, + "89": 5418, + "90": 2790, + "91": 972, + "92": 252, + "93": 42, + "111": 765 + }, + "word_sha256": "51203e7fc75ba10bd3ac3f8e675759f47e13d262bea66b6600d1e515095cad78", + "zero_columns": 0 + } +} diff --git a/research/bit-generalized-summary-support/SOURCES.json b/research/bit-generalized-summary-support/SOURCES.json new file mode 100644 index 0000000000..d7caabea2b --- /dev/null +++ b/research/bit-generalized-summary-support/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8", + "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/paired-query-only-bit/retained/inputs/BIT-NATIVE-WORD.json.gz", + "usage": "input", + "git_blob": "b718d6b2848215ad785022106dfa9f871a3d1c0c", + "sha256": "51203e7fc75ba10bd3ac3f8e675759f47e13d262bea66b6600d1e515095cad78" + } + ] +} diff --git a/research/bit-generalized-summary-support/TASK.json b/research/bit-generalized-summary-support/TASK.json new file mode 100644 index 0000000000..81e26678e9 --- /dev/null +++ b/research/bit-generalized-summary-support/TASK.json @@ -0,0 +1,77 @@ +{ + "actual_scope": "On the exact selected #7001 native word, test six through nine simultaneous owned-summary replacements at the fixed moonshot target. Keep other summary rows, chart catalogue, chart-zero descent and monotone source flow fixed.", + "ai_assistance": "Substantial OpenAI Codex and subagent assistance, including a separate exact re-enumeration and proof review.", + "author": "ToikY", + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "bottleneck_link": "A gain of at least 5/3 paid units per native copy is necessary to fund the selected paired BIT deficit at the fixed target. This excludes all six- through nine-summary profiles in the stated scope.", + "budget_minutes": 20, + "evidence": "d2=75 and 111 distinct nonzero columns. All 16,110 rank-six pair complements have rank nine after any single-column deletion. The four profiles left by the arithmetic and incidence screens are excluded.", + "open_questions": [ + { + "blocked_by": "Exact producer and consumer rows, chart legality, restoration and full price remain open.", + "first_step": "Screen equal-rank nested redirects of a literal public MOVE for an exact useful row at the summary cut.", + "question": "Can a cost-neutral existing public MOVE redirect supply an otherwise unsupported summary row?", + "why_it_matters": "A nonmonotone source-flow change is outside the fixed-catalogue monotone exclusion." + } + ], + "original_card": { + "acceptance_gate": "A full boundary contract and paid profile; unchanged scalar counts alone are insufficient. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "existing_checks": [ + { + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "status": "reviewed" + } + ], + "first_experiment": "First read #5679/#5708 and their audits as pending component proposals. Choose one uncovered helper group/cut on an exact word; compare arbitrary-input native action, targets, owned storage, both orientations and full signed bill. Stop if the gain is only a scalar count or repaid by lost targets. Do not rerun the frozen #5609 common-frame domain without changing its hypothesis.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "id": "bit-helper-contract", + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "overlap_terms": [ + "G20", + "helper split", + "5679", + "5708", + "independent target" + ], + "question": "Can a changed G20 helper path or independent-target split improve the complete BIT moment without losing its physical endpoint?", + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "research/g20-helper-split/README.md", + "research/g20-conjugation-admission/README.md" + ] + }, + "outcome": "negative-result", + "priority_revision": 8, + "schema_version": 1, + "scope_change_reason": "Test the necessary support and charged rank profiles of larger joint descents after #7146 closed the smaller scopes.", + "scope_status": "refined", + "stop_rule": "Exhaust at most 4,096 rank histograms per k for k=6 through 9. Check all 16,110 distinct rank-six chart pairs, allowing arbitrary single-coordinate padding for the final profile.", + "task_id": "bit-helper-contract" +} diff --git a/research/bit-generalized-summary-support/VERIFY.json b/research/bit-generalized-summary-support/VERIFY.json new file mode 100644 index 0000000000..7b03c032d2 --- /dev/null +++ b/research/bit-generalized-summary-support/VERIFY.json @@ -0,0 +1,21 @@ +{ + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "checks": "Authenticate the literal word, verify rational chart spaces and monotone moves, enumerate the code and all two-dimensional supports, exhaust the rank profiles, and check all 16,110 projected chart pairs under every single-column deletion.", + "timeout_seconds": 60 + } + ], + "inputs": [ + "research/paired-query-only-bit/retained/inputs/BIT-NATIVE-WORD.json.gz" + ], + "python": "3.12", + "requirements": [], + "schema_version": 1, + "status": "ready" +} diff --git a/research/bit-generalized-summary-support/bounds.py b/research/bit-generalized-summary-support/bounds.py new file mode 100644 index 0000000000..8a2f349133 --- /dev/null +++ b/research/bit-generalized-summary-support/bounds.py @@ -0,0 +1,52 @@ +"""Exact necessary rank and support bounds for the fixed catalogue.""" +from fractions import Fraction +from itertools import combinations_with_replacement +from math import comb + +CAP = 4096 +TARGET = Fraction("0.0040075385047236") +CAPACITY = {1: 1, 2: 2, 4: 12, 6: 30, 7: 62, 8: 111} +RANKS = sorted(CAPACITY) + + +def ceil(q): + return -(-q.numerator // q.denominator) + + +def profiles(k): + limit = 7 * k - 2 + for largest in RANKS: + tail_ranks = [r for r in RANKS if r <= largest] + capacity = [0] + for m in range(1, limit + 1): + capacity.append(max(capacity[m-r] + CAPACITY[r] for r in tail_ranks if r <= m)) + + def finish(i, remaining, support, tail): + if support + capacity[remaining] < 48: + return + if i == len(tail_ranks): + if support >= 48: + yield tuple(tail) + return + rank = tail_ranks[i] + for count in range(remaining // rank + 1): + yield from finish(i + 1, remaining - count * rank, + support + count * CAPACITY[rank], [*tail, *([rank] * count)]) + + for first in combinations_with_replacement([r for r in RANKS if r >= largest], k - 1): + remaining = limit - sum(first) - largest + if remaining < 0: + break + for tail in finish(0, remaining, CAPACITY[largest], []): + yield (*reversed(first), largest, *reversed(tail)) + + +def incidence_lower(collectors, dimension): + fiber = 2**(9 - dimension) + nonzero = 112 - fiber + represented = total = 0 + for degree in range(collectors + 1): + if degree: + represented += comb(collectors, degree) + total += max(0, nonzero - fiber * represented) + return total diff --git a/research/bit-generalized-summary-support/catalogue.py b/research/bit-generalized-summary-support/catalogue.py new file mode 100644 index 0000000000..bf5ed940af --- /dev/null +++ b/research/bit-generalized-summary-support/catalogue.py @@ -0,0 +1,71 @@ +"""Pinned rational chart capacities and monotone support check.""" +from collections import Counter +from fractions import Fraction +import gzip +import json + + +def rational_rank(matrix): + rows = [list(map(Fraction, row)) for row in matrix] + rank = 0 + for column in range(8): + pivot = next((i for i in range(rank, len(rows)) if rows[i][column]), None) + if pivot is None: + continue + rows[rank], rows[pivot] = rows[pivot], rows[rank] + scale = rows[rank][column] + rows[rank] = [x / scale for x in rows[rank]] + for i in range(rank + 1, len(rows)): + scale = rows[i][column] + if scale: + rows[i] = [x - scale * y for x, y in zip(rows[i], rows[rank], strict=True)] + rank += 1 + return rank + + +def scan(path): + # The package's read_rows authenticates the same live input before this scan. + word = json.loads(gzip.decompress(path.read_bytes())) + frames = {int(i): frame for i, frame in word["frames"].items()} + lines = [tuple(map(Fraction, frames[i]["B"][0])) for i in word["start"][:111]] + masks = {} + capacities = Counter() + for index, frame in frames.items(): + basis = frame["B"] + annihilator = [tuple(map(Fraction, row)) for row in frame["A"]] + rank = frame["dim"] + assert len(basis) == rational_rank(basis) == rank + assert len(annihilator) == rational_rank(annihilator) == 8 - rank + assert all(sum(x*y for x,y in zip(a,b,strict=True)) == 0 + for a in annihilator for b in basis) + support = sum(1 << i for i, line in enumerate(lines) + if all(not sum(x*y for x,y in zip(line, row, strict=True)) for row in annihilator)) + masks[index] = support + capacities[rank] = max(capacities[rank], support.bit_count()) + + cur = word["start"] + [None] * word["owned_fields"] + public = 0 + for op, r, *args in word["program"]: + if op == "MOVE": + a, b = args + assert cur[r] == a + if r < word["public"]: + assert frames[a]["dim"] < frames[b]["dim"] and masks[a] & ~masks[b] == 0 + public += 1 + else: + assert frames[a]["dim"] == 7 and b == 0 + cur[r] = b + elif op == "ADD": + assert cur[r] == cur[args[0]] == args[1] + elif op == "INIT": + assert cur[r] is None + cur[r] = args[0] + elif op == "CLEAR": + assert cur[r] == args[0] + cur[r] = None + else: + assert op == "SWAP" + other = args[0] + cur[r], cur[other] = cur[other], cur[r] + assert public == 2862 and cur == word["final"] + [None] * word["owned_fields"] + return dict(capacities), sorted({masks[i] for i, frame in frames.items() if frame["dim"] == 6}) diff --git a/research/bit-generalized-summary-support/verify.py b/research/bit-generalized-summary-support/verify.py new file mode 100644 index 0000000000..0eebc99443 --- /dev/null +++ b/research/bit-generalized-summary-support/verify.py @@ -0,0 +1,96 @@ +"""Reconstruct generalized code support and projected catalogue bounds.""" +from collections import Counter +from fractions import Fraction +from itertools import combinations +import json +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent +SOURCE = "research/paired-query-only-bit/retained/inputs/BIT-NATIVE-WORD.json.gz" +sys.path.insert(0, str(HERE)) +import bounds +import catalogue +import weights + + +def projection(values): + """Return the rank and number of columns whose deletion lowers it.""" + pivots = {} + dependencies = 0 + count = 0 + for count, value in enumerate(values, 1): + support = 1 << (count - 1) + while value: + index = value.bit_length() - 1 + if index not in pivots: + pivots[index] = value, support + break + pivot, provenance = pivots[index] + value ^= pivot + support ^= provenance + else: + dependencies |= support + return len(pivots), count - dependencies.bit_count() + + +def verify(path): + weight = weights.audit(path) + assert (weight["d1"], weight["d2"], weight["distinct_columns"], weight["zero_columns"]) == (48, 75, 111, 0) + capacities, masks = catalogue.scan(path) + assert capacities == {0: 0, **bounds.CAPACITY} + assert len(masks) == 180 + assert 1 + 62 * bounds.TARGET / 7 < Fraction(5, 3) + distances = {1: 48} + for t in range(2, 10): + avg = bounds.ceil(Fraction((2**t - 1) * 75, 3 * 2**(t-2))) + distances[t] = max(avg, 111 - (2**(9-t) - 1)) + + profiles = {} + for k in range(6, 10): + tested, survivors = set(), [] + for row in bounds.profiles(k): + assert len(tested) < bounds.CAP and row not in tested + assert row == tuple(sorted(row, reverse=True)) + tested.add(row) + if len(row) < k: + continue + for t in range(1, k + 1): + tail = row[k-t:] + available = sum(capacities[r] for r in tail) + if available < max(distances[t], bounds.incidence_lower(len(tail), t)): + break + else: + survivors.append(row) + profiles[k] = dict(tested=len(tested), survivors=survivors) + + assert not profiles[6]["survivors"] and not profiles[7]["survivors"] + assert set(profiles[8]["survivors"]) == {(6,) * 9} + assert set(profiles[9]["survivors"]) == {(6,) * 10, (6,) * 10 + (1,), (7,) + (6,) * 9} + + rows = weights.read_rows(path) + columns = [sum(((row >> i) & 1) << j for j, row in enumerate(rows)) for i in range(111)] + + def uncovered(mask): + return projection(col for i, col in enumerate(columns) if not (mask >> i) & 1) + + assert uncovered(0) == (9, 0) and uncovered(rows[0])[0] < 9 + singleton = rows[0] & -rows[0] + assert uncovered(rows[0] ^ singleton) == (9, 1) + projections = Counter(uncovered(a | b) for a, b in combinations(masks, 2)) + assert projections == {(9, 0): 16110} + assert max(mask.bit_count() for mask in masks) == 30 < weight["d1"] - 1 + return dict(status="PASS_GENERALIZED_BIT_SUMMARY_SUPPORT", profiles=profiles, + required_support_by_dimension=distances, weights=weight, + rank_six_pair_complement_ranks={"9": projections[(9, 0)]}, + rank_six_pair_deletion_rank_drops={"0": projections[(9, 0)]}, + remaining_profiles=[], + dependencies={SOURCE: weights.PIN}) + + +if __name__ == "__main__": + if not __debug__: + raise RuntimeError("Use assertions") + result = verify(HERE.parents[1] / SOURCE) + assert json.dumps(result, sort_keys=True, indent=2) + "\n" == (HERE / "RECEIPT.json").read_text() + print(result["status"]) diff --git a/research/bit-generalized-summary-support/weights.py b/research/bit-generalized-summary-support/weights.py new file mode 100644 index 0000000000..e57b167664 --- /dev/null +++ b/research/bit-generalized-summary-support/weights.py @@ -0,0 +1,73 @@ +"""Exact generalized support of the selected owned summary code.""" +from collections import Counter +from hashlib import sha256 +from itertools import combinations +import gzip +import json +from pathlib import Path +import sys + +PIN = "51203e7fc75ba10bd3ac3f8e675759f47e13d262bea66b6600d1e515095cad78" + + +def read_rows(path): + compressed = path.read_bytes() + assert sha256(compressed).hexdigest() == PIN + word = json.loads(gzip.decompress(compressed)) + state = {i: (1 << i if i < 111 else 0) for i in range(word["public"])} + summaries = {} + for opcode, role, *operands in word["program"]: + if opcode == "ADD": + state[role] ^= state[operands[0]] + elif opcode == "SWAP": + other = operands[0] + state[role], state[other] = state[other], state[role] + elif opcode == "INIT": + assert role not in state + state[role] = 0 + elif opcode == "CLEAR": + del state[role] + else: + assert opcode == "MOVE" + source, dest = operands + if role >= word["public"]: + assert dest == 0 and word["frames"][str(source)]["dim"] == 7 + assert role not in summaries + summaries[role] = state[role] + assert set(summaries) == set(range(770, 779)) + return [summaries[i] for i in range(770, 779)] + + +def codewords(rows): + words = [0] + for row in rows: + words += [word ^ row for word in words] + return words + + +def audit(path): + rows = read_rows(path) + words = codewords(rows) + assert len(set(words)) == 512 + assert len(set(codewords([rows[1], *rows[1:]]))) == 256 + d1 = min(word.bit_count() for word in words[1:]) + assert d1 == 48 + pairs = Counter() + for a, b in combinations(words[1:], 2): + pairs[(a | b).bit_count()] += 1 + assert pairs.total() == 130305 + d2 = min(pairs) + assert pairs[d2] % 3 == 0 + columns = Counter(sum(((row >> i) & 1) << r for r, row in enumerate(rows)) + for i in range(111)) + return dict(status="PASS_GENERALIZED_SUMMARY_SUPPORT", word_sha256=PIN, + d1=d1, d2=d2, enumerated_pairs=pairs.total(), + minimizing_subspaces=pairs[d2] // 3, union_weight_histogram=pairs, + zero_columns=columns[0], distinct_columns=len(columns), + maximum_column_multiplicity=max(columns.values())) + + +if __name__ == "__main__": + if not __debug__: + raise RuntimeError("Use assertions") + print(json.dumps(audit(Path(sys.argv[1])), sort_keys=True, indent=2)) 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")