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-paired-schedule-bound/PROOF.md b/research/bit-paired-schedule-bound/PROOF.md new file mode 100644 index 0000000000..850aa430cd --- /dev/null +++ b/research/bit-paired-schedule-bound/PROOF.md @@ -0,0 +1,141 @@ +# Paired BIT schedule bound at the fixed target + +Keep the exact 38-role clean endpoint in the selected #7001 paired BIT +caller, its 18 independent body variables, the retained native invoice +per LOCAL, and the rank-one QUERY and body-only distinct-stage IDLE +tariffs. Allow arbitrary placement and invertible constant bases and +additional auxiliary roles initialized and restored to zero. The native +count and its stage multiplicities may vary. The signed paid moment is +strictly negative at κ = 0.0040075385047236 throughout this family. + +## Rank conditions + +Normalize each factor at q=1 and all body variables equal to 1, and +conjugate its derivative by the accumulated constant prefix. The +target stage derivatives E_s are the pinned diagonal projections on +public space A. A LOCAL contributes a rank-two stage projector P +and a square-zero rank-one head defect N with PN=NP=N. QUERY gives +a square-zero rank-one head defect. An IDLE serving s gives a rank-one +stage projector. + +Let n be the number of LOCALs and q_count the number of QUERYs. +The complete head derivative factors as UV with n+q_count rank-one +terms and restricts to the identity on A. V embeds A into the +fixed space of VU, so rank(I−VU)≤n+q_count−38. Each diagonal +pairing of VU is zero by square-zero, forcing q_count≥39−n. + +A stage is saturated when its serving ranks sum to rank(E_s). +In a saturated stage, the images of all its projectors form a +direct sum equal to im(E_s), by the full ambient rank and the exact +clean restriction. They annihilate one another, since E_s is the +identity on that sum. Each LOCAL head defect stays inside the +column and row support of E_s. The head terms of any a same-stage +LOCALs give a principal identity block of size a in I−VU. + +The 81 opposite-arm pairs have the same two common root coordinates, +0 and 19, in their diagonal E_s supports. For opposite stages with a +and b LOCALs, the principal block of I−VU has diagonal blocks I_a +and I_b. Both cross blocks factor through the two root coordinates, +so the Schur complement has rank at least b−2. If a and b denote +the actual largest multiplicities in the two arms, then at full +saturation + +```text +q_count ≥ max(0, 39−n, 38−n+max(a,b,a+b−2)). +``` + +## The price of IDLE masks + +Write f(r)=r^(1−κ). For fixed per-stage demands d_s, nested masks +{ s : d_s ≥ j } minimize the moment. For every k their k longest +lengths sum to ∑ min(k,d_s), an upper bound for any k masks. +Concavity of f gives the cost lower bound. + +Each saturated IDLE projector crossing arms has its image and row on +the two root coordinates. At most two cross incidences can serve a +stage. Splitting a mask of x left stages and y right stages costs +111[f(7x)+f(7y)−f(7(x+y))]. By concavity and the decrease of f(r)/r, +this is at most h(x+y), with h=111[2f(7)−f(14)]/2. Consequently the +optimal separate-arm bill minus 36h is a lower bound for any +grouping. The computation encloses all powers and sums with outward +rounding to 22 decimal places. + +## Higher multiplicities + +The nine half-ranks in each arm are 2 through 10. At saturation +a half-idle demand at capacity c has bounds max(0,c−a)≤d≤c if the +arm's largest LOCAL multiplicity is a. Given n_arm LOCALs, the +sum of the half-demands is 54−n_arm. + +To minimize the separate-arm bill, start with the lower demands. +Allocate the remaining increments in order of increasing depth +among all columns, respecting their caps. At every mask length +cutoff k, the marginal increase in ∑ min(k,2d) is first two, +possibly one, then zero. This same allocation maximizes the +sum for every k, giving the least nested cost. The table relaxes +actual maxima a,b to upper bounds only for this IDLE price. It +charges the QUERY lower bound for the declared actual maxima. + +There are 331 feasible count/max cells per arm. Across the +108,832 paired cells with max(a,b)≥3, the highest directed signed +upper is −28.3066209237471478769601. For exactly 36 LOCALs it is +−46.0926684363776335553730. The 272 legal ordered one-slot transfers +also fail individually. All two-slot transfers introducing a higher +multiplicity are included in the grouped bound. + +## Zero, one or two LOCALs per stage + +Here write m=36−n. At saturation with a stage retaining two LOCALs, +the head identity block gives q_count≥m+4. Suppose each arm has a +stage with two LOCALs and two cross IDLE incidences. In each such +stage the cross IDLE images and rows span the two root spaces. +Both LOCAL defects then have column and row only on the private +coordinates of that arm. The four terms across the two arms +give a four-by-four identity minor, requiring q_count≥m+6. +Thus at q_count=m+4 at least one arm has at most one cross +incidence per stage retaining two LOCALs. The total is at most +min(36,27+m). + +The original IDLE masks attain the separate-arm nested minimum. +Each additional incidence increases it by at least +δ=111[f(63)−f(56)]. Two additional incidences and one paid QUERY +per retirement cost at least 2.92315928489496 more than the saved +net native moment. This exceeds h. Hence the upper at q_count=m+4 +is greatest at m=0 using 27h and is below −2.36106060201144. +With q_count≥m+5 the extra 111 units dominate all 36 cross +incidences. If every stage has at most one LOCAL, the first 18 +retirements increase the nested separate-arm minimum by four +rank-63 masks. At q_count≥m+3 and with all 36 cross incidences +granted the upper there is below −28.64227303907207. Each further +retirement only decreases this upper. + +## Extra incidence and excessive native count + +Every stage needs at least rank(E_s) serving dimensions. If any +stage has excess, there are at least 217−2n IDLE incidences +for n≤108. Grant arbitrary grouping into masks of up to 18 stages +and charge only q_count≥max(0,39−n). Concavity permits a lower bill +using full masks and one remainder. Across 0≤n≤108 the best +signed upper is −161.1964987524476534781450. For n≥109, even +granting every IDLE and QUERY free, the root productive moment +minus the native net debit is strictly negative and decreases +with n. + +The remaining mechanisms change the native invoice, the endpoint, +the LOCAL or QUERY operator, the IDLE tariff, or the recursive +admission proof. The replay authenticates the exact #7001 caller, +receipt and interval engine, reconstructs the original paid and +productive profiles, and checks the exact integer price cells. +It also compares the greedy allocation against 96 small +bounded-demand fixtures. + +Credit DreamingOfClouds, CubeJerry, zxv and the retained #7001 +authors for the paired BIT source. [#7160](https://github.com/CrocSwap/integer-mult-bounds/pull/7160) +supplies independent-stage saturation and the 36-LOCAL rank bound. +[#6984](https://github.com/CrocSwap/integer-mult-bounds/pull/6984), +[#6800](https://github.com/CrocSwap/integer-mult-bounds/pull/6800) +and [#6825](https://github.com/CrocSwap/integer-mult-bounds/pull/6825) +supply related fixed-window and rank-factorization methods. The +two-LOCAL retirement argument was independently audited in Round 7. +OpenAI Codex and subagents materially assisted the proof, replay +and independent rank and price checks. diff --git a/research/bit-paired-schedule-bound/README.md b/research/bit-paired-schedule-bound/README.md new file mode 100644 index 0000000000..38bff49c0b --- /dev/null +++ b/research/bit-paired-schedule-bound/README.md @@ -0,0 +1,37 @@ +# Paired BIT schedule bound at the fixed target + +**NO VERIFIED GAIN.** On the exact #7001 paired BIT endpoint, every +LOCAL count and stage multiplicity fails the signed paid-moment test +at κ = 0.0040075385047236 under the retained per-LOCAL invoice and +rank-one QUERY and distinct-stage IDLE tariffs. The bound allows arbitrary +invertible scalar bases and clean auxiliary roles restored to zero. +[Proof](PROOF.md) · [Directed receipt](RECEIPT.json) + +## Clean replay + +Run from the repository root with CPython 3.12 and assertions enabled. + +```sh +python3.12 -B scripts/research_package.py --package research/bit-paired-schedule-bound +``` + +The verifier authenticates the paired caller, frozen invoice and retained +interval code. It reconstructs the original counts and covers 81 exact +opposite-arm support pairs, 108,832 relaxed higher-multiplicity price +cells, and every possible native count. Separate inequalities cover +zero-to-two LOCALs, excess stage incidence and counts above saturation. +A small brute-force control checks bounded-demand mask packing. + +## Open next questions + +The next supplier change needs a lower native net debit or a changed +head/body endpoint. Start by pinning a changed native charge and pricing +it against the complete paired target, including every setup, transport +and restoration. A positive relaxed price still needs an all-width +operator, physical replay and the larger BIT atom and tape admission. + +This result extends [#7160](https://github.com/CrocSwap/integer-mult-bounds/pull/7160) +from a fixed 36-LOCAL rank bound to arbitrary multiplicities and a +complete target-moment obstruction for this alphabet. The proof credits +the paired source and related head-rank precedents. OpenAI Codex and +subagents materially assisted. Apache-2.0. diff --git a/research/bit-paired-schedule-bound/RECEIPT.json b/research/bit-paired-schedule-bound/RECEIPT.json new file mode 100644 index 0000000000..567062861d --- /dev/null +++ b/research/bit-paired-schedule-bound/RECEIPT.json @@ -0,0 +1,39 @@ +{ + "above_saturated_native_cap_maximum": "-8369.4606944275198565329965", + "best_one_slot": [ + 18, + 10 + ], + "dependencies": { + "EFREE-CALLER.json.gz": "757b3523798f840bdb02028b23708c3416627a99ea09e7a3c4bcdc5cd0c7ce4b", + "EFREE-RESULT.json": "a46b6c6040f75184cab5467656811ad988c216e3bc8e44d595a5015b6e49620b", + "retained/inputs/independent_interval.py": "9293f567aa4afd9b4e618f1cddd3cf66eea51c5e194e3c578e7a8f4db6e04a57" + }, + "lower_multiplicity_saturated": { + "at_least_one_extra_query": "-94.1134477296328029670842", + "minimum_queries_with_two_local_stage": "-2.3610606020114406897430", + "no_two_local_stage": "-28.6422730390720785911148" + }, + "max_for_36": "-46.0926684363776335553730", + "native_counts_considered": 109, + "one_slot_upper": "-74.8227702474738125629074", + "opposite_stage_pairs": 81, + "ordered_one_slot_transfers": 272, + "per_arm_tables": [ + 331, + 331 + ], + "saturated_higher_multiplicity_maximum": "-28.3066209237471478769601", + "saturated_higher_multiplicity_price_cells": 108832, + "saturated_maximizing_cell": [ + 3, + 2, + 26, + 15, + 0 + ], + "target": "10018846261809/2500000000000000", + "unsaturated_maximizing_locals": 37, + "unsaturated_maximum": "-161.1964987524476534781450", + "water_fill_toy_controls": 96 +} diff --git a/research/bit-paired-schedule-bound/SOURCES.json b/research/bit-paired-schedule-bound/SOURCES.json new file mode 100644 index 0000000000..276fd040e1 --- /dev/null +++ b/research/bit-paired-schedule-bound/SOURCES.json @@ -0,0 +1,36 @@ +{ + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "files": [ + { + "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8", + "path": "certificates/selected-result.json", + "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1", + "usage": "provenance" + }, + { + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "path": "docs/research/agent-task-catalog.json", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81", + "usage": "provenance" + }, + { + "git_blob": "f022272a8d51ede841778dec76e2bfb24b614d04", + "path": "research/paired-query-only-bit/EFREE-CALLER.json.gz", + "sha256": "757b3523798f840bdb02028b23708c3416627a99ea09e7a3c4bcdc5cd0c7ce4b", + "usage": "input" + }, + { + "git_blob": "575f76487f9999ecc3e7b1b70f9f71bc582ef8a8", + "path": "research/paired-query-only-bit/EFREE-RESULT.json", + "sha256": "a46b6c6040f75184cab5467656811ad988c216e3bc8e44d595a5015b6e49620b", + "usage": "input" + }, + { + "git_blob": "30ae586ea0714513802930561b6223065f377573", + "path": "research/paired-query-only-bit/retained/inputs/independent_interval.py", + "sha256": "9293f567aa4afd9b4e618f1cddd3cf66eea51c5e194e3c578e7a8f4db6e04a57", + "usage": "input" + } + ], + "schema_version": 1 +} diff --git a/research/bit-paired-schedule-bound/TASK.json b/research/bit-paired-schedule-bound/TASK.json new file mode 100644 index 0000000000..c92a9239e2 --- /dev/null +++ b/research/bit-paired-schedule-bound/TASK.json @@ -0,0 +1,64 @@ +{ + "actual_scope": "Exact selected #7001 clean paired endpoint, arbitrary LOCAL stage multiplicity and scalar chronology, fixed native invoice, rank-one QUERY and distinct-stage IDLE tariff.", + "ai_assistance": "Substantial OpenAI Codex and subagent assistance with proof, replay and independent rank and price audits.", + "author": "ToikY", + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "bottleneck_link": "Every raw BIT schedule in the stated family loses directed moment at the campaign target, so a stronger provider or changed interface is needed.", + "budget_minutes": 30, + "evidence": "Exact paired invoice reconstruction, 81 root support intersections, 108832 directed relaxed higher-multiplicity cells, 272 one-slot transfers, 96 exhaustive small packing fixtures and all other count classes bounded analytically.", + "open_questions": [ + { + "blocked_by": "All-width native and restored ownership proof, explicit transport and larger BIT atom and tape admission.", + "first_step": "Pin a literal native debit change and reprice the complete paired invoice with every added charge.", + "question": "Can a changed native provider reduce the per-LOCAL debit while preserving the same paired target?", + "why_it_matters": "A reduction changes the binding raw moment beyond this schedule bound." + } + ], + "original_card": { + "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. 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 a fixed larger register count or a specified nonabelian operation family." + ], + "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.", + "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "id": "bit-new-register-model", + "methods": [ + "Construct the smallest exact identity in a newly specified legal operation alphabet.", + "Derive a target-specific relaxation bound for that same explicit alphabet." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ], + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "scope_change_triggers": [ + "Remaining inside the already-excluded three-register abelian model.", + "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result." + ], + "starting_points": [ + "docs/research/research-family-status.md", + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json", + "research/bit-gl3-mixed-targets-length10/README.md", + "docs/research/community-efficient1000-review.md" + ] + }, + "outcome": "negative-result", + "priority_revision": 8, + "schema_version": 1, + "scope_change_reason": "Determine whether changing LOCAL count, stage assignment and IDLE grouping can reach the exact campaign target in the retained paired caller alphabet.", + "scope_status": "changed", + "stop_rule": "Stop when the signed upper bound is strictly negative for every native count and incidence class. Build only on a positive fully charged class.", + "task_id": "bit-new-register-model" +} diff --git a/research/bit-paired-schedule-bound/VERIFY.json b/research/bit-paired-schedule-bound/VERIFY.json new file mode 100644 index 0000000000..85fa21159a --- /dev/null +++ b/research/bit-paired-schedule-bound/VERIFY.json @@ -0,0 +1,23 @@ +{ + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "checks": "Recount exact paired BIT costs and verify every directed schedule-family bound and mask-packing control.", + "timeout_seconds": 60 + } + ], + "inputs": [ + "research/paired-query-only-bit/EFREE-CALLER.json.gz", + "research/paired-query-only-bit/EFREE-RESULT.json", + "research/paired-query-only-bit/retained/inputs/independent_interval.py" + ], + "python": "3.12", + "requirements": [], + "schema_version": 1, + "status": "ready" +} diff --git a/research/bit-paired-schedule-bound/verify.py b/research/bit-paired-schedule-bound/verify.py new file mode 100644 index 0000000000..8512491756 --- /dev/null +++ b/research/bit-paired-schedule-bound/verify.py @@ -0,0 +1,222 @@ +"""Certify the target-moment bound for redistributed paired BIT LOCALs.""" + +import argparse +from collections import Counter +from fractions import Fraction +import gzip +from hashlib import sha256 +from importlib.util import module_from_spec, spec_from_file_location +from itertools import product +import json +from pathlib import Path + +TARGET = Fraction("0.0040075385047236") +SCALE = 10**22 +PINS = { + "EFREE-CALLER.json.gz": "757b3523798f840bdb02028b23708c3416627a99ea09e7a3c4bcdc5cd0c7ce4b", + "EFREE-RESULT.json": "a46b6c6040f75184cab5467656811ad988c216e3bc8e44d595a5015b6e49620b", + "retained/inputs/independent_interval.py": "9293f567aa4afd9b4e618f1cddd3cf66eea51c5e194e3c578e7a8f4db6e04a57", +} + + +def read(root, path): + raw = (root / path).read_bytes() + if sha256(raw).hexdigest() != PINS[path]: + raise ValueError(f"SHA-256 mismatch: {path}") + return raw + + +def water_fill(caps, minimum, total): + demand = list(minimum) + increments = sorted((depth, j) for j, cap in enumerate(caps) + for depth in range(demand[j], cap)) + needed = total - sum(demand) + if not 0 <= needed <= len(increments): + return None + for _, j in increments[:needed]: + demand[j] += 1 + return demand + + +def packed(demand, body, ports): + return Counter({r: c*ports for r, c in Counter( + body * sum(x >= k for x in demand) for k in range(1, max(demand, default=0)+1) + ).items()}) + + +def run(root): + caller = json.loads(gzip.decompress(read(root, "EFREE-CALLER.json.gz"))) + receipt = json.loads(read(root, "EFREE-RESULT.json")) + relative = "retained/inputs/independent_interval.py" + read(root, relative) + spec = spec_from_file_location("retained_interval", root / relative) + price = module_from_spec(spec) + spec.loader.exec_module(price) + + def fixed(text): + value = Fraction(text)*SCALE + assert value.denominator == 1 + return value.numerator + + def show(value): + sign = "-" if value < 0 else "" + whole, tail = divmod(abs(value), SCALE) + return f"{sign}{whole}.{tail:022d}" + + powers = {} + + def moment(hist, side): + total = 0 + for rank, count in hist.items(): + rank = int(rank) + if rank not in powers: + b = price.bounds_text(price.power(rank, 1-TARGET)) + powers[rank] = fixed(b["lower"]), fixed(b["upper"]) + total += powers[rank][side]*count + return total + + roles, body, ports = (caller[k] for k in ("roles", "body_rank", "ports")) + assert (roles, body, ports) == (38, 7, 111) + stages = range(1, 19) + arms = (range(1, 10), range(10, 19)) + target = {s: {i for i, row in enumerate(caller["diagonal"]) if s in row["stages"]} for s in stages} + assert all(row["q"] == 1 for row in caller["diagonal"]) + assert all(target[s] & target[t] == {0,19} for s in arms[0] for t in arms[1]) + caps = [sorted(len(target[s])//2 for s in arm) for arm in arms] + assert caps[0] == caps[1] == list(range(2,11)) + assert all(len(target[s]) % 2 == 0 for s in stages) + events = caller["events"] + assert Counter(e[1] for e in events if e[0] == "LOCAL") == {s:2 for s in stages} + assert sum(e[0] == "QUERY" for e in events) == 4 + idle = Counter(body*len(e[2]) for e in events if e[0] == "IDLE_ONE") + root_idle = Counter({r:c*ports for r,c in idle.items()}) + native_p = Counter({int(r):c for r,c in receipt["native_paid"].items()}) + native_t = Counter({int(r):c for r,c in receipt["native_helpers"].items()}) + root_t = Counter(1+body*len(row["stages"]) for row in caller["diagonal"]) + root_t = Counter({r:c*ports for r,c in root_t.items()}) + full_p = Counter({r:36*c for r,c in native_p.items()}) + root_idle + Counter({1:4*ports}) + full_t = Counter({r:36*c for r,c in native_t.items()}) + root_t + assert full_p == Counter({int(r):c for r,c in receipt["paid"].items()}) + assert full_t == Counter({int(r):c for r,c in receipt["targets"].items()}) + + native_debit = moment(native_p,0)-moment(native_t,1) + native_debit_upper = moment(native_p,1)-moment(native_t,0) + root_credit = moment(root_t,1) + cross_credit = 18*(moment({7:2*ports},1)-moment({14:ports},0)) + + def upper(n, q, idle_debit, cross): + return root_credit - n*native_debit - q*ports*SCALE - idle_debit + cross + + def rebate(incidences): + doubled = moment({7:2*ports},1)-moment({14:ports},0) + return (incidences*doubled+1)//2 + + baseline = upper(36,4,moment(root_idle,0),0) + arm_step = moment({63:ports},0)-moment({56:ports},1) + penalty = ports*SCALE + 2*arm_step - native_debit_upper + assert penalty > rebate(1) > 0 + original_degrees = [len(target[s])-4 for s in stages] + assert packed(original_degrees[:9],body,ports)+packed(original_degrees[9:],body,ports) == root_idle + increased = [x+2 for x in original_degrees] + assert packed(increased[:9],body,ports)+packed(increased[9:],body,ports) == ( + root_idle + Counter({63:4*ports}) + ) + lower_multiplicity = { + "minimum_queries_with_two_local_stage": baseline+rebate(27), + "at_least_one_extra_query": baseline+rebate(36)-ports*SCALE, + "no_two_local_stage": ( + baseline+18*native_debit_upper+rebate(36) + -17*ports*SCALE-moment({63:4*ports},0) + ), + } + assert max(lower_multiplicity.values()) < 0 + + toy_caps, toy_min = (1,3,4,4), (0,0,2,1) + toy = list(product(*(range(lo,hi+1) for lo,hi in zip(toy_min,toy_caps,strict=True)))) + for total in range(sum(toy_min),sum(toy_caps)+1): + best = water_fill(toy_caps,toy_min,total) + for level in range(1,max(toy_caps)+1): + assert sum(min(level,d) for d in best) == max( + sum(min(level,d) for d in candidate) for candidate in toy if sum(candidate)==total + ) + + def arm_table(cap): + table = {} + for biggest in range(max(cap)+1): + minimum = [max(0,c-biggest) for c in cap] + for n in range(biggest,sum(cap)+1): + demand = water_fill(cap,minimum,sum(cap)-n) + if demand is not None: + table[biggest,n] = moment(packed([2*x for x in demand],body,ports),0) + return table + + left, right = map(arm_table, caps) + by_total = {} + checked = 0 + for (a,n), v in left.items(): + for (b,m), w in right.items(): + if max(a,b) < 3: + continue + checked += 1 + q = max(0,39-n-m,38-n-m+max(a,b,a+b-2)) + row = (upper(n+m,q,v+w,cross_credit),a,b,n,m,q) + if n+m not in by_total or row > by_total[n+m]: + by_total[n+m] = row + assert checked <= 160000 and max(by_total.values())[0] < 0 + + # Non-saturation: one additional stage incidence, with every mask + # allowed to occupy all 18 stages and arbitrary individual degrees. + total_cap = sum(map(sum,caps)) + unsaturated = [] + for n in range(total_cap+1): + count = 2*(total_cap-n)+1 + full, rem = divmod(count,18) + hist = Counter({126:ports*full}) + if rem: + hist[7*rem] = ports + unsaturated.append((upper(n,max(0,39-n),moment(hist,0),0),n)) + assert max(unsaturated)[0] < 0 + excess_native_count_upper = upper(total_cap+1,0,0,0) + assert native_debit > 0 and excess_native_count_upper < 0 + + # Recount all one-slot reallocations. For two slots the whole-family + # bound above already covers all changed multiplicities. + d = original_degrees + cases = [] + for src in range(18): + for dst in range(18): + if src == dst or d[dst] < 2: + continue + moved = d[:] + moved[src] += 2 + moved[dst] -= 2 + tariff = moment(packed(moved[:9],body,ports)+packed(moved[9:],body,ports),0) + cases.append((upper(36,5,tariff,cross_credit),src+1,dst+1)) + assert max(cases)[0] < 0 + return dict(target=str(TARGET), dependencies=PINS, opposite_stage_pairs=81, + native_counts_considered=total_cap+1, per_arm_tables=[len(left),len(right)], + saturated_higher_multiplicity_price_cells=checked, + saturated_higher_multiplicity_maximum=show(max(by_total.values())[0]), + saturated_maximizing_cell=list(max(by_total.values())[1:]), + max_for_36=show(by_total[36][0]), + unsaturated_maximum=show(max(unsaturated)[0]), + unsaturated_maximizing_locals=max(unsaturated)[1], + ordered_one_slot_transfers=len(cases), + one_slot_upper=show(max(cases)[0]), + best_one_slot=list(max(cases)[1:]), + water_fill_toy_controls=len(toy), + above_saturated_native_cap_maximum=show(excess_native_count_upper), + lower_multiplicity_saturated={name:show(value) + for name,value in lower_multiplicity.items()}) + + +if __name__ == "__main__": + if not __debug__: + raise RuntimeError("Use CPython 3.12 with assertions enabled") + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("package", nargs="?", type=Path, default=Path(__file__).resolve().parent.parent / "paired-query-only-bit") + receipt = json.dumps(run(parser.parse_args().package), indent=2, sort_keys=True) + "\n" + expected = Path(__file__).resolve().with_name("RECEIPT.json").read_bytes() + if receipt.encode() != expected: + raise ValueError("exact paid-moment receipt mismatch") + print("PASS_BIT_PAIRED_SCHEDULE_BOUND") 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")