diff --git a/research/compact-agreement-set-seed29/README.md b/research/compact-agreement-set-seed29/README.md new file mode 100644 index 0000000000..76462d2804 --- /dev/null +++ b/research/compact-agreement-set-seed29/README.md @@ -0,0 +1,175 @@ +# Exact raw agreement set for compact dirty-control selected-bit updates + +**Adversarial mathematical audit with an independent finite checker. No new +kappa; the selected record, production predicates and `upstream/` are +unchanged.** For the compact dirty-control selected-bit operation of +[`notes/compact-control-movement.tex`](../../notes/compact-control-movement.tex) +("Guards and deterministic repair"), this package computes the exact set `AG` +of states where the complete routine already equals the ideal selected-bit XOR +map and restores every dirty temporary, on complete bounded domains, and +compares it with the three published sufficient guards: + +| Guard | Source | +| --- | --- | +| `G0` original temporary+target guard (plus `u` nonsaturation for the later source) | the source note, "Guards and deterministic repair" | +| `G1` expanded source-control predicate (last `u` digit keeps its complete range) | [`research/compact-carry-repair-audit`](../compact-carry-repair-audit/README.md) | +| `H` two-pass guard (1), source dependent | [`research/compact-late-guard-audit-seed73`](../compact-late-guard-audit-seed73/README.md) | + +This is an **independent check of the two cited guard claims**, explicitly +identified as such, plus a new exact census those packages left open: the +seed73 README states its guard "is not the global exact agreement set" and +leaves that set uncharacterized. + +## Result + +1. **Sufficiency of all three guards is independently confirmed on complete + domains.** No state admitted by `G0`, `G1` or `H` fails the ideal map or + restoration in any of the 47 enumerated cells. Both published failure + fixtures reproduce exactly under the independent interpreter: the + carry-repair fixture `(x,y,t,u,b)=(16,4224,0,1,2)` returns `y=4752` against + ideal `y=4240` with every temporary restored, and the late-guard fixture + `(2,124,1,0,7)` returns the correct `y=126` while corrupting the temporary + `1 -> 5`. +2. **The raw agreement set is strictly larger than every guard, everywhere.** + Overall `|AG| / total = 11880712 / 24074240 = 49.35%`, against guard + densities of at most 14.06% (`G0`, early `K=6,G=1`), 7.03% (`G1`) and + 44.83% (`H`). Example cells (later source): + + | Cell | AG | `G0` | `G1` | `H` | + | --- | ---: | ---: | ---: | ---: | + | `n=2, K=5, G=1` | 39.55% | 1.562% | 3.125% | 18.750% | + | `n=2, K=4, G=2` | 58.42% | empty | empty | 44.824% | + | `n=3, K=3, G=1` | 19.83% | empty | empty | 7.031% | + + Smallest agreement states every guard rejects are recorded per cell in + [RESULT.json](RESULT.json) (`ag_outside_all`, `ag_outside_all_active`), for + example `[y,t,u,c]=[0,1,0,0]` and the nonzero-source `[0,1,0,1]` at + `n=2,K=3,G=1`: the saturated temporary digit is never loaded (`a_i = 0`), + so the feared carry cannot fire and the map is exactly correct as written. + The guards are safe repair envelopes, not the agreement set. This witness + class is exactly the class the open + [PR1603](https://github.com/CrocSwap/integer-mult-bounds/pull/1603) guard + (inactive saturated digits) is designed to admit; the census also contains + agreement states with internal `u`-load carries and cancellations between + individually inexact subcalls, which that PR's discussion says remain + outside its guard. +3. **The seed73 closed form (2) is independently verified.** `H`'s exact + good-address fraction matches the enumerated count at every one of the 21 + later-source cells (the checker requires exact integer agreement). +4. **Inclusions hold as claimed**: `G0 => G1 => H` on every cell (no witness), + and the original guard's target condition `2B <= g < 2^(K-1) - 2B` is + *empty* for `K <= G+3`; `G0`/`G1` only engage at `K >= G+4`, which is why + several small cells report empty guards. + +## Domain and method + +`verify.py` transcribes the note's four packed updates directly (whole-slot +modular rotations for the target, whole-field rotations for the compact +temporaries) and both source orders; no predecessor interpreter is imported. +For each geometry `(n,K,G)` and each selected offset `rho`, it enumerates the +complete invariant fiber: selected source bits `c`, full target `y` (its low +`rho` bits are spectators), compact temporaries `t`, compact controls `u`; +the dirty back field `b` and `x`'s unselected bits are spectators by +construction and are checked on samples. 47 cells, 24,074,240 states: +`n in {2,3}`, `K in {3,4,5,6}`, `G in {1,2}`, every `rho` for `n=2,K<=5` and +the boundary offsets for `K=6` and `n=3,K=5`, both source orders except the +one later-source-infeasible cell. + +Controls: both published fixtures above (fidelity); a sign-flipped unloading +must be caught by the restoration check inside the guarded domain (witness +`[y,t,c,t_bad]=[4240,0,0,1]`); low target bits and arbitrary dirty back-field +values must not change any result (256 states times 4 dirty values). + +## Reproduce + +From the repository root, Python 3.10+, standard library only: + +```sh +python3 -B research/compact-agreement-set-seed29/verify.py +``` + +Expected: + +```text +PASS_COMPACT_AGREEMENT_SET: 24074240 states; 11880712 raw agreements; 47 cells; 2 fixtures; 2 controls +``` + +The checker verifies the pinned hashes in [SOURCES.json](SOURCES.json) before +running, compares its receipt with [RESULT.json](RESULT.json), and writes no +artifacts. `--write /new/path.json` regenerates a receipt and refuses to +overwrite an existing file. Checks use explicit exceptions and also run with +`python3 -O`; no mathematical check relies on Python `assert`. The default +replay takes a few minutes; the manifest timeout is 600 s. + +## What is not checked + +- The exceptional repair itself (scan, radix sort under `TS^-1`, record keys), + its cost charges, and the complete-range invariant after row splitting + (`docs/audit.md` lines 114-116) remain open; this audit covers the *raw* + map before any repair. +- The production predicate and its callers are untouched; no adoption of a + larger agreement envelope is proposed. +- `n <= 3`, `K <= 6`, `G <= 2` only. Larger geometries, the highest-bit + completion beyond the elementary XOR, and a proof-assistant formalization + are outside this package. Transcription fidelity rests on the source note, + the two reproduced fixtures, and the pinned-source hashes, not on a formal + semantics. +- The stronger sufficient guard of the concurrent open + [PR1603](https://github.com/CrocSwap/integer-mult-bounds/pull/1603) + (`research/compact-late-carry-guard`, not present in this base commit) is + **not** transcribed or tested here; only the three guards whose definitions + are in this base are checked. +- No kappa, packing-cap or a < D/E claim: this is a source-bound audit of one + named condition, so whole-construction budgets do not apply. + +## Open next questions + +- **Characterize `AG` structurally.** The census shows the exact agreement set + exceeds every digit-local guard; the seed73 proof characterizes agreement + only inside the nonsaturated-`t` domain, and open + [PR1603](https://github.com/CrocSwap/integer-mult-bounds/pull/1603) proves a + maximal invariant agreement core only for `n=1`, with a handoff asking for + the `n>1` enumeration. This package supplies that enumeration layer at + `n=2,3`; a carry-state description of the enumerated set is still missing. + *Why it matters:* a repair envelope priced on `AG` rather than on a + sufficient guard would shrink the exceptional-repair workload. *First step:* + classify the `AG \ H` states at `n=2,K=4,G=1` by which guard clause fails + (never-loaded saturation vs internal `u`-load carry vs subcall + cancellation), then test any proposed digit-local formula on the next + geometry. *Blocked by:* nothing computational; a plausible predicate form is + the missing ingredient. +- **Price the repair envelope change.** *Why it matters:* `docs/audit.md` + asks independent verification to preserve the scan and radix-sort charges + including full record payload and destination keys; those charges scale with + the number of repaired records. *First step:* implement the `TS^-1` sort + repair at `n=2,K=5,G=1` and count repaired records under `G0`/`G1`/`H` + versus a hypothetical `AG`-based predicate. *Blocked by:* the note does not + fully specify the tape cost model of the repair. +- **Larger-geometry falsification first.** *Why it matters:* all three guard + sufficiency proofs are parameter-generic, but the finite checks stop at + `n=3`. *First step:* seed-randomized falsification search for sufficiency + counterexamples at `n=4..6`, `K=6`, `G=2` (the seed73 geometry family), + starting at boundary guards. *Blocked by:* complete enumeration is + infeasible there, so only bounded search, not a complete domain. + +## Credit + +Aaron Wang, with help from opencode. Apache-2.0; same repository licenses. +Source semantics: `notes/compact-control-movement.tex`. Guards, fixtures and +the density formula are prior work: the two-pass guard `H` and its density are +[Hanson Sun's PR1247](https://github.com/CrocSwap/integer-mult-bounds/pull/1247), +independently re-derived in `research/compact-late-guard-audit-seed73` (which +also supplied fixture 2); `G1` and fixture 1 are +`research/compact-carry-repair-audit`, following +[Sagar Thakrar's PR1475](https://github.com/CrocSwap/integer-mult-bounds/pull/1475) +and the one-pass fact of PR1219. The concurrent open +[PR1603](https://github.com/CrocSwap/integer-mult-bounds/pull/1603) (inactive +saturated digits, `research/compact-late-carry-guard`, with its claim and +handoff in +[discussion 1588](https://github.com/CrocSwap/integer-mult-bounds/discussions/1588)) +is independent concurrent work on the same family: its stronger sufficient +guard and `n=1` maximality result are not reproduced here, and this census is +an answer to the `n>1` enumeration its handoff requests. +`scripts/audit_compact_controls.py` is pinned as the source-bound checker of +record; this package shares no code with it. The live overlap search and its +coverage are recorded in [TASK.json](TASK.json). diff --git a/research/compact-agreement-set-seed29/RESULT.json b/research/compact-agreement-set-seed29/RESULT.json new file mode 100644 index 0000000000..064a5e9cb2 --- /dev/null +++ b/research/compact-agreement-set-seed29/RESULT.json @@ -0,0 +1,1836 @@ +{ + "cells": [ + { + "G": 1, + "G0_admitted": 0, + "G0_violation": null, + "K": 3, + "ag": 5664, + "ag_outside_G0": [ + 0, + 0, + 0 + ], + "ag_outside_G0_active": [ + 0, + 0, + 1 + ], + "n": 2, + "order": "early", + "rho": 0, + "total": 8192 + }, + { + "G": 1, + "G0_admitted": 0, + "G0_violation": null, + "K": 3, + "ag": 2832, + "ag_outside_G0": [ + 0, + 0, + 0 + ], + "ag_outside_G0_active": [ + 0, + 0, + 1 + ], + "n": 2, + "order": "early", + "rho": 1, + "total": 4096 + }, + { + "G": 1, + "G0_admitted": 0, + "G0_violation": null, + "K": 3, + "ag": 1416, + "ag_outside_G0": [ + 0, + 0, + 0 + ], + "ag_outside_G0_active": [ + 0, + 0, + 1 + ], + "n": 2, + "order": "early", + "rho": 2, + "total": 2048 + }, + { + "G": 1, + "G0_admitted": 0, + "G0_not_G1": null, + "G0_violation": null, + "G1_admitted": 0, + "G1_not_H": null, + "G1_violation": null, + "H_admitted": 6144, + "H_count_formula": 6144, + "H_fraction": [ + 3, + 16 + ], + "H_violation": null, + "K": 3, + "ag": 12672, + "ag_outside_G0": [ + 0, + 0, + 0, + 0 + ], + "ag_outside_G1": [ + 0, + 0, + 0, + 0 + ], + "ag_outside_H": [ + 0, + 1, + 0, + 0 + ], + "ag_outside_all": [ + 0, + 1, + 0, + 0 + ], + "ag_outside_all_active": [ + 0, + 1, + 0, + 1 + ], + "n": 2, + "order": "late", + "rho": 0, + "total": 32768 + }, + { + "G": 1, + "G0_admitted": 0, + "G0_not_G1": null, + "G0_violation": null, + "G1_admitted": 0, + "G1_not_H": null, + "G1_violation": null, + "H_admitted": 3072, + "H_count_formula": 3072, + "H_fraction": [ + 3, + 16 + ], + "H_violation": null, + "K": 3, + "ag": 6336, + "ag_outside_G0": [ + 0, + 0, + 0, + 0 + ], + "ag_outside_G1": [ + 0, + 0, + 0, + 0 + ], + "ag_outside_H": [ + 0, + 1, + 0, + 0 + ], + "ag_outside_all": [ + 0, + 1, + 0, + 0 + ], + "ag_outside_all_active": [ + 0, + 1, + 0, + 1 + ], + "n": 2, + "order": "late", + "rho": 1, + "total": 16384 + }, + { + "G": 1, + "G0_admitted": 0, + "G0_not_G1": null, + "G0_violation": null, + "G1_admitted": 0, + "G1_not_H": null, + "G1_violation": null, + "H_admitted": 1536, + "H_count_formula": 1536, + "H_fraction": [ + 3, + 16 + ], + "H_violation": null, + "K": 3, + "ag": 3168, + "ag_outside_G0": [ + 0, + 0, + 0, + 0 + ], + "ag_outside_G1": [ + 0, + 0, + 0, + 0 + ], + "ag_outside_H": [ + 0, + 1, + 0, + 0 + ], + "ag_outside_all": [ + 0, + 1, + 0, + 0 + ], + "ag_outside_all_active": [ + 0, + 1, + 0, + 1 + ], + "n": 2, + "order": "late", + "rho": 2, + "total": 8192 + }, + { + "G": 2, + "G0_admitted": 0, + "G0_violation": null, + "K": 3, + "ag": 23584, + "ag_outside_G0": [ + 0, + 0, + 0 + ], + "ag_outside_G0_active": [ + 0, + 0, + 1 + ], + "n": 2, + "order": "early", + "rho": 0, + "total": 32768 + }, + { + "G": 2, + "G0_admitted": 0, + "G0_violation": null, + "K": 3, + "ag": 11792, + "ag_outside_G0": [ + 0, + 0, + 0 + ], + "ag_outside_G0_active": [ + 0, + 0, + 1 + ], + "n": 2, + "order": "early", + "rho": 1, + "total": 16384 + }, + { + "G": 2, + "G0_admitted": 0, + "G0_violation": null, + "K": 3, + "ag": 5896, + "ag_outside_G0": [ + 0, + 0, + 0 + ], + "ag_outside_G0_active": [ + 0, + 0, + 1 + ], + "n": 2, + "order": "early", + "rho": 2, + "total": 8192 + }, + { + "G": 2, + "G0_admitted": 0, + "G0_not_G1": null, + "G0_violation": null, + "G1_admitted": 0, + "G1_not_H": null, + "G1_violation": null, + "H_admitted": 211968, + "H_count_formula": 211968, + "H_fraction": [ + 207, + 512 + ], + "H_violation": null, + "K": 3, + "ag": 277376, + "ag_outside_G0": [ + 0, + 0, + 0, + 0 + ], + "ag_outside_G1": [ + 0, + 0, + 0, + 0 + ], + "ag_outside_H": [ + 0, + 3, + 0, + 0 + ], + "ag_outside_all": [ + 0, + 3, + 0, + 0 + ], + "ag_outside_all_active": [ + 0, + 3, + 0, + 1 + ], + "n": 2, + "order": "late", + "rho": 0, + "total": 524288 + }, + { + "G": 2, + "G0_admitted": 0, + "G0_not_G1": null, + "G0_violation": null, + "G1_admitted": 0, + "G1_not_H": null, + "G1_violation": null, + "H_admitted": 105984, + "H_count_formula": 105984, + "H_fraction": [ + 207, + 512 + ], + "H_violation": null, + "K": 3, + "ag": 138688, + "ag_outside_G0": [ + 0, + 0, + 0, + 0 + ], + "ag_outside_G1": [ + 0, + 0, + 0, + 0 + ], + "ag_outside_H": [ + 0, + 3, + 0, + 0 + ], + "ag_outside_all": [ + 0, + 3, + 0, + 0 + ], + "ag_outside_all_active": [ + 0, + 3, + 0, + 1 + ], + "n": 2, + "order": "late", + "rho": 1, + "total": 262144 + }, + { + "G": 2, + "G0_admitted": 0, + "G0_not_G1": null, + "G0_violation": null, + "G1_admitted": 0, + "G1_not_H": null, + "G1_violation": null, + "H_admitted": 52992, + "H_count_formula": 52992, + "H_fraction": [ + 207, + 512 + ], + "H_violation": null, + "K": 3, + "ag": 69392, + "ag_outside_G0": [ + 0, + 0, + 0, + 0 + ], + "ag_outside_G1": [ + 0, + 0, + 0, + 0 + ], + "ag_outside_H": [ + 0, + 3, + 0, + 0 + ], + "ag_outside_all": [ + 0, + 3, + 0, + 0 + ], + "ag_outside_all_active": [ + 0, + 3, + 0, + 1 + ], + "n": 2, + "order": "late", + "rho": 2, + "total": 131072 + }, + { + "G": 1, + "G0_admitted": 0, + "G0_violation": null, + "K": 4, + "ag": 46208, + "ag_outside_G0": [ + 0, + 0, + 0 + ], + "ag_outside_G0_active": [ + 0, + 0, + 1 + ], + "n": 2, + "order": "early", + "rho": 0, + "total": 65536 + }, + { + "G": 1, + "G0_admitted": 0, + "G0_violation": null, + "K": 4, + "ag": 23104, + "ag_outside_G0": [ + 0, + 0, + 0 + ], + "ag_outside_G0_active": [ + 0, + 0, + 1 + ], + "n": 2, + "order": "early", + "rho": 1, + "total": 32768 + }, + { + "G": 1, + "G0_admitted": 0, + "G0_violation": null, + "K": 4, + "ag": 11552, + "ag_outside_G0": [ + 0, + 0, + 0 + ], + "ag_outside_G0_active": [ + 0, + 0, + 1 + ], + "n": 2, + "order": "early", + "rho": 2, + "total": 16384 + }, + { + "G": 1, + "G0_admitted": 0, + "G0_violation": null, + "K": 4, + "ag": 5776, + "ag_outside_G0": [ + 0, + 0, + 0 + ], + "ag_outside_G0_active": [ + 0, + 0, + 1 + ], + "n": 2, + "order": "early", + "rho": 3, + "total": 8192 + }, + { + "G": 1, + "G0_admitted": 0, + "G0_not_G1": null, + "G0_violation": null, + "G1_admitted": 0, + "G1_not_H": null, + "G1_violation": null, + "H_admitted": 49152, + "H_count_formula": 49152, + "H_fraction": [ + 3, + 16 + ], + "H_violation": null, + "K": 4, + "ag": 102912, + "ag_outside_G0": [ + 0, + 0, + 0, + 0 + ], + "ag_outside_G1": [ + 0, + 0, + 0, + 0 + ], + "ag_outside_H": [ + 0, + 1, + 0, + 0 + ], + "ag_outside_all": [ + 0, + 1, + 0, + 0 + ], + "ag_outside_all_active": [ + 0, + 1, + 0, + 1 + ], + "n": 2, + "order": "late", + "rho": 0, + "total": 262144 + }, + { + "G": 1, + "G0_admitted": 0, + "G0_not_G1": null, + "G0_violation": null, + "G1_admitted": 0, + "G1_not_H": null, + "G1_violation": null, + "H_admitted": 24576, + "H_count_formula": 24576, + "H_fraction": [ + 3, + 16 + ], + "H_violation": null, + "K": 4, + "ag": 51456, + "ag_outside_G0": [ + 0, + 0, + 0, + 0 + ], + "ag_outside_G1": [ + 0, + 0, + 0, + 0 + ], + "ag_outside_H": [ + 0, + 1, + 0, + 0 + ], + "ag_outside_all": [ + 0, + 1, + 0, + 0 + ], + "ag_outside_all_active": [ + 0, + 1, + 0, + 1 + ], + "n": 2, + "order": "late", + "rho": 1, + "total": 131072 + }, + { + "G": 1, + "G0_admitted": 0, + "G0_not_G1": null, + "G0_violation": null, + "G1_admitted": 0, + "G1_not_H": null, + "G1_violation": null, + "H_admitted": 12288, + "H_count_formula": 12288, + "H_fraction": [ + 3, + 16 + ], + "H_violation": null, + "K": 4, + "ag": 25728, + "ag_outside_G0": [ + 0, + 0, + 0, + 0 + ], + "ag_outside_G1": [ + 0, + 0, + 0, + 0 + ], + "ag_outside_H": [ + 0, + 1, + 0, + 0 + ], + "ag_outside_all": [ + 0, + 1, + 0, + 0 + ], + "ag_outside_all_active": [ + 0, + 1, + 0, + 1 + ], + "n": 2, + "order": "late", + "rho": 2, + "total": 65536 + }, + { + "G": 1, + "G0_admitted": 0, + "G0_not_G1": null, + "G0_violation": null, + "G1_admitted": 0, + "G1_not_H": null, + "G1_violation": null, + "H_admitted": 6144, + "H_count_formula": 6144, + "H_fraction": [ + 3, + 16 + ], + "H_violation": null, + "K": 4, + "ag": 12864, + "ag_outside_G0": [ + 0, + 0, + 0, + 0 + ], + "ag_outside_G1": [ + 0, + 0, + 0, + 0 + ], + "ag_outside_H": [ + 0, + 1, + 0, + 0 + ], + "ag_outside_all": [ + 0, + 1, + 0, + 0 + ], + "ag_outside_all_active": [ + 0, + 1, + 0, + 1 + ], + "n": 2, + "order": "late", + "rho": 3, + "total": 32768 + }, + { + "G": 2, + "G0_admitted": 0, + "G0_violation": null, + "K": 4, + "ag": 205952, + "ag_outside_G0": [ + 0, + 0, + 0 + ], + "ag_outside_G0_active": [ + 0, + 0, + 1 + ], + "n": 2, + "order": "early", + "rho": 0, + "total": 262144 + }, + { + "G": 2, + "G0_admitted": 0, + "G0_violation": null, + "K": 4, + "ag": 102976, + "ag_outside_G0": [ + 0, + 0, + 0 + ], + "ag_outside_G0_active": [ + 0, + 0, + 1 + ], + "n": 2, + "order": "early", + "rho": 1, + "total": 131072 + }, + { + "G": 2, + "G0_admitted": 0, + "G0_violation": null, + "K": 4, + "ag": 51488, + "ag_outside_G0": [ + 0, + 0, + 0 + ], + "ag_outside_G0_active": [ + 0, + 0, + 1 + ], + "n": 2, + "order": "early", + "rho": 2, + "total": 65536 + }, + { + "G": 2, + "G0_admitted": 0, + "G0_violation": null, + "K": 4, + "ag": 25744, + "ag_outside_G0": [ + 0, + 0, + 0 + ], + "ag_outside_G0_active": [ + 0, + 0, + 1 + ], + "n": 2, + "order": "early", + "rho": 3, + "total": 32768 + }, + { + "G": 2, + "G0_admitted": 0, + "G0_not_G1": null, + "G0_violation": null, + "G1_admitted": 0, + "G1_not_H": null, + "G1_violation": null, + "H_admitted": 1880064, + "H_count_formula": 1880064, + "H_fraction": [ + 459, + 1024 + ], + "H_violation": null, + "K": 4, + "ag": 2450176, + "ag_outside_G0": [ + 0, + 0, + 0, + 0 + ], + "ag_outside_G1": [ + 0, + 0, + 0, + 0 + ], + "ag_outside_H": [ + 0, + 3, + 0, + 0 + ], + "ag_outside_all": [ + 0, + 3, + 0, + 0 + ], + "ag_outside_all_active": [ + 0, + 3, + 0, + 1 + ], + "n": 2, + "order": "late", + "rho": 0, + "total": 4194304 + }, + { + "G": 2, + "G0_admitted": 0, + "G0_not_G1": null, + "G0_violation": null, + "G1_admitted": 0, + "G1_not_H": null, + "G1_violation": null, + "H_admitted": 940032, + "H_count_formula": 940032, + "H_fraction": [ + 459, + 1024 + ], + "H_violation": null, + "K": 4, + "ag": 1225088, + "ag_outside_G0": [ + 0, + 0, + 0, + 0 + ], + "ag_outside_G1": [ + 0, + 0, + 0, + 0 + ], + "ag_outside_H": [ + 0, + 3, + 0, + 0 + ], + "ag_outside_all": [ + 0, + 3, + 0, + 0 + ], + "ag_outside_all_active": [ + 0, + 3, + 0, + 1 + ], + "n": 2, + "order": "late", + "rho": 1, + "total": 2097152 + }, + { + "G": 2, + "G0_admitted": 0, + "G0_not_G1": null, + "G0_violation": null, + "G1_admitted": 0, + "G1_not_H": null, + "G1_violation": null, + "H_admitted": 470016, + "H_count_formula": 470016, + "H_fraction": [ + 459, + 1024 + ], + "H_violation": null, + "K": 4, + "ag": 612544, + "ag_outside_G0": [ + 0, + 0, + 0, + 0 + ], + "ag_outside_G1": [ + 0, + 0, + 0, + 0 + ], + "ag_outside_H": [ + 0, + 3, + 0, + 0 + ], + "ag_outside_all": [ + 0, + 3, + 0, + 0 + ], + "ag_outside_all_active": [ + 0, + 3, + 0, + 1 + ], + "n": 2, + "order": "late", + "rho": 2, + "total": 1048576 + }, + { + "G": 2, + "G0_admitted": 0, + "G0_not_G1": null, + "G0_violation": null, + "G1_admitted": 0, + "G1_not_H": null, + "G1_violation": null, + "H_admitted": 235008, + "H_count_formula": 235008, + "H_fraction": [ + 459, + 1024 + ], + "H_violation": null, + "K": 4, + "ag": 306272, + "ag_outside_G0": [ + 0, + 0, + 0, + 0 + ], + "ag_outside_G1": [ + 0, + 0, + 0, + 0 + ], + "ag_outside_H": [ + 0, + 3, + 0, + 0 + ], + "ag_outside_all": [ + 0, + 3, + 0, + 0 + ], + "ag_outside_all_active": [ + 0, + 3, + 0, + 1 + ], + "n": 2, + "order": "late", + "rho": 3, + "total": 524288 + }, + { + "G": 1, + "G0_admitted": 32768, + "G0_violation": null, + "K": 5, + "ag": 373248, + "ag_outside_G0": [ + 0, + 0, + 0 + ], + "ag_outside_G0_active": [ + 0, + 0, + 1 + ], + "n": 2, + "order": "early", + "rho": 0, + "total": 524288 + }, + { + "G": 1, + "G0_admitted": 16384, + "G0_violation": null, + "K": 5, + "ag": 186624, + "ag_outside_G0": [ + 0, + 0, + 0 + ], + "ag_outside_G0_active": [ + 0, + 0, + 1 + ], + "n": 2, + "order": "early", + "rho": 1, + "total": 262144 + }, + { + "G": 1, + "G0_admitted": 8192, + "G0_violation": null, + "K": 5, + "ag": 93312, + "ag_outside_G0": [ + 0, + 0, + 0 + ], + "ag_outside_G0_active": [ + 0, + 0, + 1 + ], + "n": 2, + "order": "early", + "rho": 2, + "total": 131072 + }, + { + "G": 1, + "G0_admitted": 4096, + "G0_violation": null, + "K": 5, + "ag": 46656, + "ag_outside_G0": [ + 0, + 0, + 0 + ], + "ag_outside_G0_active": [ + 0, + 0, + 1 + ], + "n": 2, + "order": "early", + "rho": 3, + "total": 65536 + }, + { + "G": 1, + "G0_admitted": 2048, + "G0_violation": null, + "K": 5, + "ag": 23328, + "ag_outside_G0": [ + 0, + 0, + 0 + ], + "ag_outside_G0_active": [ + 0, + 0, + 1 + ], + "n": 2, + "order": "early", + "rho": 4, + "total": 32768 + }, + { + "G": 1, + "G0_admitted": 32768, + "G0_not_G1": null, + "G0_violation": null, + "G1_admitted": 65536, + "G1_not_H": null, + "G1_violation": null, + "H_admitted": 393216, + "H_count_formula": 393216, + "H_fraction": [ + 3, + 16 + ], + "H_violation": null, + "K": 5, + "ag": 829440, + "ag_outside_G0": [ + 0, + 0, + 0, + 0 + ], + "ag_outside_G1": [ + 0, + 0, + 0, + 0 + ], + "ag_outside_H": [ + 0, + 1, + 0, + 0 + ], + "ag_outside_all": [ + 0, + 1, + 0, + 0 + ], + "ag_outside_all_active": [ + 0, + 1, + 0, + 1 + ], + "n": 2, + "order": "late", + "rho": 0, + "total": 2097152 + }, + { + "G": 1, + "G0_admitted": 8192, + "G0_not_G1": null, + "G0_violation": null, + "G1_admitted": 16384, + "G1_not_H": null, + "G1_violation": null, + "H_admitted": 98304, + "H_count_formula": 98304, + "H_fraction": [ + 3, + 16 + ], + "H_violation": null, + "K": 5, + "ag": 207360, + "ag_outside_G0": [ + 0, + 0, + 0, + 0 + ], + "ag_outside_G1": [ + 0, + 0, + 0, + 0 + ], + "ag_outside_H": [ + 0, + 1, + 0, + 0 + ], + "ag_outside_all": [ + 0, + 1, + 0, + 0 + ], + "ag_outside_all_active": [ + 0, + 1, + 0, + 1 + ], + "n": 2, + "order": "late", + "rho": 2, + "total": 524288 + }, + { + "G": 1, + "G0_admitted": 2048, + "G0_not_G1": null, + "G0_violation": null, + "G1_admitted": 4096, + "G1_not_H": null, + "G1_violation": null, + "H_admitted": 24576, + "H_count_formula": 24576, + "H_fraction": [ + 3, + 16 + ], + "H_violation": null, + "K": 5, + "ag": 51840, + "ag_outside_G0": [ + 0, + 0, + 0, + 0 + ], + "ag_outside_G1": [ + 0, + 0, + 0, + 0 + ], + "ag_outside_H": [ + 0, + 1, + 0, + 0 + ], + "ag_outside_all": [ + 0, + 1, + 0, + 0 + ], + "ag_outside_all_active": [ + 0, + 1, + 0, + 1 + ], + "n": 2, + "order": "late", + "rho": 4, + "total": 131072 + }, + { + "G": 1, + "G0_admitted": 36864, + "G0_violation": null, + "K": 6, + "ag": 187520, + "ag_outside_G0": [ + 0, + 0, + 0 + ], + "ag_outside_G0_active": [ + 0, + 0, + 1 + ], + "n": 2, + "order": "early", + "rho": 4, + "total": 262144 + }, + { + "G": 1, + "G0_admitted": 18432, + "G0_violation": null, + "K": 6, + "ag": 93760, + "ag_outside_G0": [ + 0, + 0, + 0 + ], + "ag_outside_G0_active": [ + 0, + 0, + 1 + ], + "n": 2, + "order": "early", + "rho": 5, + "total": 131072 + }, + { + "G": 1, + "G0_admitted": 36864, + "G0_not_G1": null, + "G0_violation": null, + "G1_admitted": 73728, + "G1_not_H": null, + "G1_violation": null, + "H_admitted": 196608, + "H_count_formula": 196608, + "H_fraction": [ + 3, + 16 + ], + "H_violation": null, + "K": 6, + "ag": 416256, + "ag_outside_G0": [ + 0, + 0, + 0, + 0 + ], + "ag_outside_G1": [ + 0, + 0, + 0, + 0 + ], + "ag_outside_H": [ + 0, + 1, + 0, + 0 + ], + "ag_outside_all": [ + 0, + 1, + 0, + 0 + ], + "ag_outside_all_active": [ + 0, + 1, + 0, + 1 + ], + "n": 2, + "order": "late", + "rho": 4, + "total": 1048576 + }, + { + "G": 1, + "G0_admitted": 18432, + "G0_not_G1": null, + "G0_violation": null, + "G1_admitted": 36864, + "G1_not_H": null, + "G1_violation": null, + "H_admitted": 98304, + "H_count_formula": 98304, + "H_fraction": [ + 3, + 16 + ], + "H_violation": null, + "K": 6, + "ag": 208128, + "ag_outside_G0": [ + 0, + 0, + 0, + 0 + ], + "ag_outside_G1": [ + 0, + 0, + 0, + 0 + ], + "ag_outside_H": [ + 0, + 1, + 0, + 0 + ], + "ag_outside_all": [ + 0, + 1, + 0, + 0 + ], + "ag_outside_all_active": [ + 0, + 1, + 0, + 1 + ], + "n": 2, + "order": "late", + "rho": 5, + "total": 524288 + }, + { + "G": 1, + "G0_admitted": 0, + "G0_violation": null, + "K": 3, + "ag": 140000, + "ag_outside_G0": [ + 0, + 0, + 0 + ], + "ag_outside_G0_active": [ + 0, + 0, + 1 + ], + "n": 3, + "order": "early", + "rho": 0, + "total": 262144 + }, + { + "G": 1, + "G0_admitted": 0, + "G0_violation": null, + "K": 3, + "ag": 70000, + "ag_outside_G0": [ + 0, + 0, + 0 + ], + "ag_outside_G0_active": [ + 0, + 0, + 1 + ], + "n": 3, + "order": "early", + "rho": 1, + "total": 131072 + }, + { + "G": 1, + "G0_admitted": 0, + "G0_violation": null, + "K": 3, + "ag": 35000, + "ag_outside_G0": [ + 0, + 0, + 0 + ], + "ag_outside_G0_active": [ + 0, + 0, + 1 + ], + "n": 3, + "order": "early", + "rho": 2, + "total": 65536 + }, + { + "G": 1, + "G0_admitted": 0, + "G0_not_G1": null, + "G0_violation": null, + "G1_admitted": 0, + "G1_not_H": null, + "G1_violation": null, + "H_admitted": 147456, + "H_count_formula": 147456, + "H_fraction": [ + 9, + 128 + ], + "H_violation": null, + "K": 3, + "ag": 415872, + "ag_outside_G0": [ + 0, + 0, + 0, + 0 + ], + "ag_outside_G1": [ + 0, + 0, + 0, + 0 + ], + "ag_outside_H": [ + 0, + 1, + 0, + 0 + ], + "ag_outside_all": [ + 0, + 1, + 0, + 0 + ], + "ag_outside_all_active": [ + 0, + 1, + 0, + 1 + ], + "n": 3, + "order": "late", + "rho": 0, + "total": 2097152 + }, + { + "G": 1, + "G0_admitted": 0, + "G0_not_G1": null, + "G0_violation": null, + "G1_admitted": 0, + "G1_not_H": null, + "G1_violation": null, + "H_admitted": 73728, + "H_count_formula": 73728, + "H_fraction": [ + 9, + 128 + ], + "H_violation": null, + "K": 3, + "ag": 207936, + "ag_outside_G0": [ + 0, + 0, + 0, + 0 + ], + "ag_outside_G1": [ + 0, + 0, + 0, + 0 + ], + "ag_outside_H": [ + 0, + 1, + 0, + 0 + ], + "ag_outside_all": [ + 0, + 1, + 0, + 0 + ], + "ag_outside_all_active": [ + 0, + 1, + 0, + 1 + ], + "n": 3, + "order": "late", + "rho": 1, + "total": 1048576 + }, + { + "G": 1, + "G0_admitted": 0, + "G0_not_G1": null, + "G0_violation": null, + "G1_admitted": 0, + "G1_not_H": null, + "G1_violation": null, + "H_admitted": 36864, + "H_count_formula": 36864, + "H_fraction": [ + 9, + 128 + ], + "H_violation": null, + "K": 3, + "ag": 103968, + "ag_outside_G0": [ + 0, + 0, + 0, + 0 + ], + "ag_outside_G1": [ + 0, + 0, + 0, + 0 + ], + "ag_outside_H": [ + 0, + 1, + 0, + 0 + ], + "ag_outside_all": [ + 0, + 1, + 0, + 0 + ], + "ag_outside_all_active": [ + 0, + 1, + 0, + 1 + ], + "n": 3, + "order": "late", + "rho": 2, + "total": 524288 + }, + { + "G": 1, + "G0_admitted": 65536, + "G0_violation": null, + "K": 5, + "ag": 2371808, + "ag_outside_G0": [ + 0, + 0, + 0 + ], + "ag_outside_G0_active": [ + 0, + 0, + 1 + ], + "n": 3, + "order": "early", + "rho": 4, + "total": 4194304 + } + ], + "controls": { + "guarded_exact_states": 2048, + "sign_flip_witness": [ + 4240, + 0, + 0, + 1 + ] + }, + "domain": [ + [ + 2, + 3, + 1, + [ + 0, + 1, + 2 + ], + [ + 0, + 1, + 2 + ] + ], + [ + 2, + 3, + 2, + [ + 0, + 1, + 2 + ], + [ + 0, + 1, + 2 + ] + ], + [ + 2, + 4, + 1, + [ + 0, + 1, + 2, + 3 + ], + [ + 0, + 1, + 2, + 3 + ] + ], + [ + 2, + 4, + 2, + [ + 0, + 1, + 2, + 3 + ], + [ + 0, + 1, + 2, + 3 + ] + ], + [ + 2, + 5, + 1, + [ + 0, + 1, + 2, + 3, + 4 + ], + [ + 0, + 2, + 4 + ] + ], + [ + 2, + 6, + 1, + [ + 4, + 5 + ], + [ + 4, + 5 + ] + ], + [ + 3, + 3, + 1, + [ + 0, + 1, + 2 + ], + [ + 0, + 1, + 2 + ] + ], + [ + 3, + 5, + 1, + [ + 4 + ], + [] + ] + ], + "fixtures": { + "carry_repair_fixture": { + "c": 1, + "ideal": 4240, + "input": [ + 16, + 4224, + 0, + 1, + 2 + ], + "t_out": 0, + "u_out": 1, + "y_out": 4752 + }, + "late_guard_fixture": { + "c": 1, + "ideal": 126, + "input": [ + 2, + 124, + 1, + 0, + 7 + ], + "t_out": 5, + "u_out": 0, + "y_out": 126 + } + }, + "spectators": { + "spectator_states": 256 + }, + "status": "PASS_COMPACT_AGREEMENT_SET" +} diff --git a/research/compact-agreement-set-seed29/SOURCES.json b/research/compact-agreement-set-seed29/SOURCES.json new file mode 100644 index 0000000000..5d671991f8 --- /dev/null +++ b/research/compact-agreement-set-seed29/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1", + "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075" + }, + { + "path": "notes/compact-control-movement.tex", + "usage": "input", + "git_blob": "06b6a9ef24245ac7b724c53a204635415b402357", + "sha256": "b963c3d2f4e1b7059aa289bb4b4ac89b688920bcf42f5b20d7698cdef0132cc6" + }, + { + "path": "scripts/audit_compact_controls.py", + "usage": "input", + "git_blob": "22da5574cb160fafab359a0a41bfe86db5a3bc34", + "sha256": "c3513cd6b41a20bc33b392d66c1536f0a5fcaa76088848361a3aef64074fa989" + } + ] +} diff --git a/research/compact-agreement-set-seed29/TASK.json b/research/compact-agreement-set-seed29/TASK.json new file mode 100644 index 0000000000..053a807aad --- /dev/null +++ b/research/compact-agreement-set-seed29/TASK.json @@ -0,0 +1,83 @@ +{ + "schema_version": 1, + "task_id": "supplier-boundary-audit", + "priority_revision": 3, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "original_card": { + "id": "supplier-boundary-audit", + "question": "Does one selected supplier obligation follow from its actual source-bound checks?", + "starting_points": [ + "certificates/selected-result.json", + "research/owner-boundary-audit/README.md" + ], + "methods": [ + "Trace one hypothesis through the source, checker and complete caller.", + "Construct one semantically invalid but superficially well-formed fixture and test rejection." + ], + "acceptance_gate": "Pin the current sources and one obligation; the historical owner audit is an example, not evidence of a current bug.", + "first_step": { + "command": [ + "python3", + "-B", + "research/owner-boundary-audit/verify.py" + ], + "expected": "PASS_PR626_NEXT_TOUCH_BOUNDARY_AUDIT", + "inspect": "Identify why the timing-only omission passes but the full production controller still rejects it.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Choose one current supplier obligation and trace whether its acceptance depends on an independent check.", + "bottleneck_link": "Closing a current acceptance gap or proof obligation strengthens reliability even without changing kappa.", + "allowed_variations": [ + "Audit one named current condition using a new semantic counterexample." + ], + "scope_change_triggers": [ + "Reporting the historical timing-only diagnostic as a new current acceptance bug." + ], + "overlap_terms": [ + "owner boundary", + "bridge omission", + "hosting" + ] + }, + "scope_status": "refined", + "actual_scope": "One named current condition of the selected-bit supplier's compact dirty-control operation (notes/compact-control-movement.tex, 'Guards and deterministic repair'): the exact raw agreement-and-restoration set of the earlier-source and later-source routines, computed on complete bounded domains (n in {2,3}, K in {3,4,5,6}, G in {1,2}, 47 cells, 24,074,240 fiber states) and compared with the published sufficient guards G0 (source note), G1 (research/compact-carry-repair-audit) and H (research/compact-late-guard-audit-seed73). Independent sufficiency check of all three guards plus smallest semantic counterexamples to their necessity.", + "scope_change_reason": "The card asks for one named current obligation traced through its source-bound checks, with an allowed variation of auditing one named condition using a new semantic counterexample. Refined from the card's generic wording to this specific condition: the sampled acceptance of the packed selected-bit operation (docs/audit.md records only 4,500 sampled triples) left the exact agreement set uncharacterized, and research/compact-late-guard-audit-seed73 explicitly states its guard is not the global exact agreement set. The card's premise (audit one supplier obligation; no construction) is unchanged.", + "bottleneck_link": "Source-bound reliability of the selected bit supplier's exceptional-repair/restoration condition. A repair envelope priced on the true agreement set rather than a sufficient guard would reduce exceptional-repair work; no kappa or packing-cap change is claimed and the a < D/E and whole-construction budgets do not apply to an audit.", + "budget_minutes": 60, + "stop_rule": "One bounded pivot maximum; kill any route whose optimistic budget misses the target. Stop when one named condition is audited with complete-domain evidence, positive fixtures and failure controls, or when the smallest falsifying instance is recorded. No kappa target is set for this audit.", + "outcome": "completed", + "evidence": "research/compact-agreement-set-seed29/verify.py (independent stdlib interpreter and census), RESULT.json (receipt: 24,074,240 states; 11,880,712 raw agreements; 47 cells), README.md. Sufficiency of G0/G1/H holds on every enumerated cell (zero violations); the exact agreement set strictly exceeds every guard everywhere (49.35% overall versus guard maxima 14.06%/7.03%/44.83%); seed73's closed form (2) matches the enumerated H counts exactly at all 21 later-source cells; both published failure fixtures (16,4224,0,1,2 and 2,124,1,0,7) reproduce exactly; mutated-unloading and spectatorship controls behave as required.", + "ai_assistance": "Substantial AI assistance: task selection, transcription, implementation, verification and writing were done with help from opencode. Contributor: Aaron Wang.", + "open_questions": [ + { + "question": "Characterize the exact raw agreement set AG structurally: which states outside every digit-local guard are nevertheless exactly correct, and is a digit-local predicate possible at all?", + "why_it_matters": "A repair envelope priced on AG rather than a sufficient guard would shrink the exceptional-repair workload the scan and radix sort must pay for.", + "first_step": "Classify the AG \\ H states at n=2,K=4,G=1 by which guard clause fails (never-loaded saturation vs systematic source-dependent region) and test any proposed predicate on the next geometry.", + "blocked_by": "No computational blocker; a plausible predicate form is the missing ingredient." + }, + { + "question": "Price the repair-envelope change: how many records does the TS^-1 sort repair move under G0/G1/H versus a hypothetical AG-based predicate?", + "why_it_matters": "docs/audit.md lines 114-116 ask independent verification to preserve the scan and radix-sort charges including full record payload and destination keys; those charges scale with repaired records.", + "first_step": "Implement the repair at n=2,K=5,G=1 and count repaired records per predicate, then price the difference with the pinned engines' charges.", + "blocked_by": "The note does not fully specify the tape cost model of the repair." + }, + { + "question": "Do the three sufficiency claims survive beyond n<=3? A bounded falsification-first search at n=4..6, K=6, G=2 (the seed73 geometry family).", + "why_it_matters": "The guard proofs are parameter-generic but every finite check, including this one, stops at small n; a counterexample would invalidate a currently accepted condition.", + "first_step": "Seed-randomized search for sufficiency counterexamples at boundary guards, smallest instances first.", + "blocked_by": "Complete enumeration is infeasible there, so only bounded search, not a complete domain." + } + ], + "overlap": { + "checked_at": "2026-10-14T10:54:51Z", + "coverage": "find_overlap.py complete pagination: 482 open PRs and 458 discussion records at 10:53-10:55 UTC, plus local READMEs, TASK metadata and the PR ledger", + "nearest": [ + "research/compact-carry-repair-audit (closed local package; G1 and fixture 1; independent check here)", + "research/compact-late-guard-audit-seed73 (closed local package; H, closed form (2) and fixture 2; independent check here)", + "https://github.com/CrocSwap/integer-mult-bounds/pull/1603 and discussion 1588 (open concurrent work in the same family: stronger sufficient guard with inactive saturated digits, n=1 maximality, handoff requesting the n>1 enumeration this census supplies)", + "research/compact-boundary-cancellation-seed51 (adjacent: repair/boundary cancellation, different question)" + ], + "open_work_found_on_object": "Open PR1603 (research/compact-late-carry-guard) works the same family with a stronger sufficient guard; it is credited and positioned in the README rather than duplicated: this package computes the exact raw agreement set and independently checks G0/G1/H, which PR1603 does not." + }, + "author": "Aaron Wang" +} diff --git a/research/compact-agreement-set-seed29/VERIFY.json b/research/compact-agreement-set-seed29/VERIFY.json new file mode 100644 index 0000000000..f11dfb82ce --- /dev/null +++ b/research/compact-agreement-set-seed29/VERIFY.json @@ -0,0 +1,21 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "notes/compact-control-movement.tex", + "scripts/audit_compact_controls.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Independently transcribed four-update gadget and both source orders; complete-fiber census of the raw agreement set at 47 cells (24,074,240 states); sufficiency of guards G0/G1/H with smallest-violation search; exact agreement of H counts with the seed73 closed form (2); inclusions G0=>G1=>H; both published failure fixtures reproduced exactly; sign-flipped unloading must break restoration inside the guarded domain; low-rho-bit and dirty-back-field spectatorship controls; pinned source hashes verified. Receipt compared with RESULT.json; no artifacts written." + } + ] +} diff --git a/research/compact-agreement-set-seed29/verify.py b/research/compact-agreement-set-seed29/verify.py new file mode 100644 index 0000000000..b37e4607f6 --- /dev/null +++ b/research/compact-agreement-set-seed29/verify.py @@ -0,0 +1,476 @@ +#!/usr/bin/env python3 +"""Exact raw agreement-set census for the compact dirty-control selected-bit map. + +Independent stdlib transcription of notes/compact-control-movement.tex +("Guards and deterministic repair"): the four-update scalar gadget packed as +whole-slot rotations, the earlier-source and later-source routines, and the +elementary highest-bit XOR. No predecessor interpreter is imported. + +For each complete bounded geometry the checker enumerates every state of the +invariant fiber (selected source bits c, full target y modulo its untouched low +rho bits, compact temporaries t, compact controls u) and computes the exact +set AG of states where the complete routine equals the ideal selected-bit XOR +map and restores u, t exactly. It then tests, independently and on complete +domains, the sufficiency of the published guards + + G0 original temporary+target guard (plus u nonsaturation for later source) + G1 compact-carry-repair-audit expanded predicate (last u digit free) + H compact-late-guard-audit-seed73 two-pass guard (source dependent) + +and records smallest states each guard misses (AG without the guard) and +smallest counterexamples if any guard admits a state outside AG. It reproduces +both published failure fixtures as fidelity controls and runs a mutated-program +control that must be rejected. + +No kappa change. This audits one named condition; it does not modify the +production predicate, the selected record, or any upstream file. +""" + +import argparse +import hashlib +import json +from pathlib import Path +from fractions import Fraction as Q + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + +STATUS = "PASS_COMPACT_AGREEMENT_SET" + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +# ---------------------------------------------------------------------- +# Independent transcription of the source note. + +def step_E(z, y, t, n, K, G, rho): + """One earlier-source block: four packed updates on (y, t). + + z is the n-bit control word (selected source bits, or u parities). + All arithmetic is the literal packed arithmetic of the note: target + updates are modular rotations of the whole f*K-bit slot; temporary + updates are modular rotations of the whole n*G-bit compact field. + """ + ymask = (1 << ((n + 1) * K)) - 1 + tmask = (1 << (n * G)) - 1 + D = (1 << G) - 1 + # R1: y += sum_i 2*z_i*t_i*2^{j_i} + off = 0 + for i in range(n): + if (z >> i) & 1: + off += (2 * ((t >> (i * G)) & D)) << (rho + i * K) + y = (y + off) & ymask + # T1: t += pack of current selected target bits + off = 0 + for i in range(n): + off += ((y >> (rho + i * K)) & 1) << (i * G) + t = (t + off) & tmask + # R2: y += sum_i z_i*(1-2*t_i)*2^{j_i} with post-T1 digits + off = 0 + for i in range(n): + if (z >> i) & 1: + off += (1 - 2 * ((t >> (i * G)) & D)) << (rho + i * K) + y = (y + off) & ymask + # T2: t -= pack of (current selected target bits xor z) + off = 0 + for i in range(n): + off += (((y >> (rho + i * K)) & 1) ^ ((z >> i) & 1)) << (i * G) + t = (t - off) & tmask + return y, t + + +def step_E_with_b(z, y, t, b, n, K, G, rho): + """Faithful swap-sandwich realization; the back field must return.""" + ymask = (1 << ((n + 1) * K)) - 1 + tmask = (1 << (n * G)) - 1 + D = (1 << G) - 1 + off = 0 + for i in range(n): + if (z >> i) & 1: + off += (2 * ((t >> (i * G)) & D)) << (rho + i * K) + y = (y + off) & ymask + off = 0 + for i in range(n): + off += ((y >> (rho + i * K)) & 1) << (i * G) + b, t = t, b + b = (b + off) & tmask + t, b = b, t + off = 0 + for i in range(n): + if (z >> i) & 1: + off += (1 - 2 * ((t >> (i * G)) & D)) << (rho + i * K) + y = (y + off) & ymask + off = 0 + for i in range(n): + off += (((y >> (rho + i * K)) & 1) ^ ((z >> i) & 1)) << (i * G) + b, t = t, b + b = (b - off) & tmask + t, b = b, t + return y, t, b + + +def parity_word(u, n, G): + z = 0 + for i in range(n): + z |= ((u >> (i * G)) & 1) << i + return z + + +def run_late(c, y, t, u, n, K, G, rho): + """Later source: E(u parities), load c into u, E(new parities), unload.""" + fmask = (1 << (n * G)) - 1 + z = parity_word(u, n, G) + y, t = step_E(z, y, t, n, K, G, rho) + load = 0 + for i in range(n): + load |= ((c >> i) & 1) << (i * G) + u = (u + load) & fmask + z = parity_word(u, n, G) + y, t = step_E(z, y, t, n, K, G, rho) + u = (u - load) & fmask + return y, t, u + + +def ideal_y(y, c, n, K, rho): + off = 0 + for i in range(n): + off |= ((c >> i) & 1) << (rho + i * K) + return y ^ off + + +# ---------------------------------------------------------------------- +# Published guard predicates, transcribed from the cited packages. + +def guard_temp_target(y, t, n, K, G, rho): + """G0's temporary and target conditions (all i < n).""" + D = (1 << G) - 1 + B = 1 << G + A = 1 << (K - 1) + for i in range(n): + if ((t >> (i * G)) & D) > B - 2: + return False + g = (y >> (rho + i * K + 1)) & ((1 << (K - 1)) - 1) + if not (2 * B <= g < A - 2 * B): + return False + return True + + +def guard_G0_late(y, t, u, n, K, G, rho): + """Original later source: G0 plus every u digit nonsaturated.""" + if not guard_temp_target(y, t, n, K, G, rho): + return False + D = (1 << G) - 1 + B = 1 << G + for i in range(n): + if ((u >> (i * G)) & D) == B - 1: + return False + return True + + +def guard_G1_late(y, t, u, n, K, G, rho): + """Expanded predicate: last source-control digit keeps its complete range.""" + if not guard_temp_target(y, t, n, K, G, rho): + return False + D = (1 << G) - 1 + B = 1 << G + for i in range(n - 1): + if ((u >> (i * G)) & D) == B - 1: + return False + return True + + +def guard_H(y, t, u, c, n, K, G, rho): + """compact-late-guard-audit-seed73 two-pass guard (1).""" + D = (1 << G) - 1 + B = 1 << G + A = 1 << (K - 1) + for i in range(n): + if ((t >> (i * G)) & D) > B - 2: + return False + for i in range(n - 1): + ui = (u >> (i * G)) & D + ci = (c >> i) & 1 + if ui + ci >= B: + return False + g = (y >> (rho + i * K + 1)) & ((1 << (K - 1)) - 1) + if g + ((ui & 1) | ci) * ((t >> (i * G)) & D) >= A: + return False + return True + + +def H_fraction(n, K, G): + """Closed form (2) of compact-late-guard-audit-seed73.""" + B = 1 << G + A = 1 << (K - 1) + return ((B - 1) / Q(B)) ** n * ( + Q(1) - Q(1, 2 * B) - Q((3 * B - 2) * (B - 2), 8 * A * B) + ) ** (n - 1) + + +# ---------------------------------------------------------------------- +# Domain: (n, K, G, early rhos, late rhos). f = n+1 wide slot. + +DOMAIN = [ + (2, 3, 1, (0, 1, 2), (0, 1, 2)), + (2, 3, 2, (0, 1, 2), (0, 1, 2)), + (2, 4, 1, (0, 1, 2, 3), (0, 1, 2, 3)), + (2, 4, 2, (0, 1, 2, 3), (0, 1, 2, 3)), + (2, 5, 1, (0, 1, 2, 3, 4), (0, 2, 4)), + (2, 6, 1, (4, 5), (4, 5)), + (3, 3, 1, (0, 1, 2), (0, 1, 2)), + (3, 5, 1, (4,), ()), +] + + +def census_early(n, K, G, rho): + ycount = 1 << ((n + 1) * K - rho) + tcount = (1 << G) ** n + total = ag = g0_adm = 0 + viol = None # smallest state admitted by G0 but outside AG + waste = None # smallest AG state rejected by G0 + waste_active = None # smallest such state with c != 0 + for t in range(tcount): + for c in range(1 << n): + for yr in range(ycount): + y = yr << rho + y2, t2 = step_E(c, y, t, n, K, G, rho) + ok = (y2 == ideal_y(y, c, n, K, rho)) and (t2 == t) + gd = guard_temp_target(y, t, n, K, G, rho) + total += 1 + if ok: + ag += 1 + if not gd: + key = [y, t, c] + if waste is None or key < waste: + waste = key + if c and (waste_active is None or key < waste_active): + waste_active = key + if gd: + g0_adm += 1 + if not ok: + key = [y, t, c] + if viol is None or key < viol: + viol = key + return { + "total": total, "ag": ag, + "G0_admitted": g0_adm, "G0_violation": viol, + "ag_outside_G0": waste, "ag_outside_G0_active": waste_active, + } + + +def census_late(n, K, G, rho): + ycount = 1 << ((n + 1) * K - rho) + tcount = (1 << G) ** n + total = ag = 0 + adm = {"G0": 0, "G1": 0, "H": 0} + viol = {"G0": None, "G1": None, "H": None} + waste = {"G0": None, "G1": None, "H": None, "all": None, "all_active": None} + inc01 = inc1H = None # inclusion witnesses + for t in range(tcount): + for u in range(tcount): + for c in range(1 << n): + for yr in range(ycount): + y = yr << rho + y2, t2, u2 = run_late(c, y, t, u, n, K, G, rho) + ok = (y2 == ideal_y(y, c, n, K, rho)) and (t2 == t) and (u2 == u) + g0 = guard_G0_late(y, t, u, n, K, G, rho) + g1 = guard_G1_late(y, t, u, n, K, G, rho) + gh = guard_H(y, t, u, c, n, K, G, rho) + total += 1 + if ok: + ag += 1 + if not (gh or g0 or g1): + key = [y, t, u, c] + if waste["all"] is None or key < waste["all"]: + waste["all"] = key + if c and (waste["all_active"] is None + or key < waste["all_active"]): + waste["all_active"] = key + for name, gd in (("G0", g0), ("G1", g1), ("H", gh)): + if gd: + adm[name] += 1 + if not ok: + key = [y, t, u, c] + if viol[name] is None or key < viol[name]: + viol[name] = key + elif ok: + key = [y, t, u, c] + if waste[name] is None or key < waste[name]: + waste[name] = key + if g0 and not g1 and inc01 is None: + inc01 = [y, t, u, c] + if g1 and not gh and inc1H is None: + inc1H = [y, t, u, c] + return { + "total": total, "ag": ag, + "G0_admitted": adm["G0"], "G1_admitted": adm["G1"], "H_admitted": adm["H"], + "G0_violation": viol["G0"], "G1_violation": viol["G1"], "H_violation": viol["H"], + "ag_outside_G0": waste["G0"], "ag_outside_G1": waste["G1"], + "ag_outside_H": waste["H"], + "ag_outside_all": waste["all"], "ag_outside_all_active": waste["all_active"], + "G0_not_G1": inc01, "G1_not_H": inc1H, + } + + +# ---------------------------------------------------------------------- +# Fidelity and failure controls. + +def published_fixtures(): + """Both published counterexamples must reproduce exactly.""" + out = {} + # research/compact-carry-repair-audit: n=2,K=5,rho=4,G=1, later source. + n, K, G, rho = 2, 5, 1, 4 + x, y, t, u, b = 16, 4224, 0, 1, 2 + c = ((x >> rho) & 1) | (((x >> (rho + K)) & 1) << 1) + y2, t2, u2 = run_late(c, y, t, u, n, K, G, rho) + out["carry_repair_fixture"] = { + "input": [x, y, t, u, b], "c": c, + "y_out": y2, "t_out": t2, "u_out": u2, + "ideal": ideal_y(y, c, n, K, rho), + } + require(y2 == 4752, "published fixture 16,4224,0,1,2 must give y=4752") + require(ideal_y(y, c, n, K, rho) == 4240, "published fixture ideal must be 4240") + require(t2 == 0 and u2 == 1, "published fixture restores temporaries") + # research/compact-late-guard-audit-seed73: n=2,K=6,rho=1,G=2. + n, K, G, rho = 2, 6, 2, 1 + x, y, t, u, b = 2, 124, 1, 0, 7 + c = ((x >> rho) & 1) | (((x >> (rho + K)) & 1) << 1) + y2, t2, u2 = run_late(c, y, t, u, n, K, G, rho) + out["late_guard_fixture"] = { + "input": [x, y, t, u, b], "c": c, + "y_out": y2, "t_out": t2, "u_out": u2, + "ideal": ideal_y(y, c, n, K, rho), + } + require(y2 == 126, "published fixture 2,124,1,0,7 must give y=126") + require(t2 == 5, "published fixture must corrupt temporary 1 -> 5") + require(u2 == 0, "published fixture restores the compact control") + return out + + +def mutant_controls(): + """A sign-flipped unloading must break restoration inside the guarded domain.""" + n, K, G, rho = 2, 5, 1, 4 # G0's target guard is nonempty for K > G+3 + D = (1 << G) - 1 + tmask = (1 << (n * G)) - 1 + ycount = 1 << ((n + 1) * K - rho) + exact = 0 + sign_err = None + for t in range((1 << G) ** n): + for c in range(1 << n): + for yr in range(ycount): + y = yr << rho + if not guard_temp_target(y, t, n, K, G, rho): + continue + y1, t1 = step_E(c, y, t, n, K, G, rho) + exact += 1 + require(y1 == ideal_y(y, c, n, K, rho) and t1 == t, + "guarded early domain must be exact") + off = 0 + for i in range(n): + off += (((y1 >> (rho + i * K)) & 1) ^ ((c >> i) & 1)) << (i * G) + t_bad = (t1 + off) & tmask # add instead of subtract at T2 + if t_bad != t and sign_err is None: + sign_err = [y, t, c, t_bad] + require(sign_err is not None, "sign-flipped unload must be caught by restoration") + return {"guarded_exact_states": exact, "sign_flip_witness": sign_err} + + +def spectator_controls(): + """Low rho target bits and the dirty back field must not affect results.""" + n, K, G, rho = 2, 4, 1, 2 + lowmask = (1 << rho) - 1 + checked = 0 + for t in range((1 << G) ** n): + for u in range((1 << G) ** n): + for c in range(1 << n): + y = 0b101010101010 + y2, t2, u2 = run_late(c, y, t, u, n, K, G, rho) + for low in (0, 1, 3, 7): + yb = (y & ~lowmask) | (low & lowmask) + y3, t3, u3 = run_late(c, yb, t, u, n, K, G, rho) + require(y3 >> rho == y2 >> rho and t3 == t2 and u3 == u2, + "low target bits must be spectators") + require(y3 & lowmask == yb & lowmask, + "low target bits must be preserved") + for dirty in (0, 5, 15, (1 << (n * G)) - 1): + _, _, be = step_E_with_b( + parity_word(u, n, G), yb, t, dirty, n, K, G, rho) + require(be == dirty, "back field must return untouched") + checked += 1 + return {"spectator_states": checked} + + +# ---------------------------------------------------------------------- + +def verify_sources(): + manifest = json.loads((HERE / "SOURCES.json").read_text(encoding="utf-8")) + for entry in manifest["files"]: + path = ROOT / entry["path"] + digest = hashlib.sha256(path.read_bytes()).hexdigest() + require(digest == entry["sha256"], + "source pin mismatch: " + entry["path"]) + + +def compute(): + verify_sources() + receipts = {"fixtures": published_fixtures(), + "controls": mutant_controls(), + "spectators": spectator_controls()} + cells = [] + for (n, K, G, early_rhos, late_rhos) in DOMAIN: + for rho in early_rhos: + r = census_early(n, K, G, rho) + r.update({"n": n, "K": K, "G": G, "rho": rho, "order": "early"}) + require(r["G0_violation"] is None, + "G0 sufficiency violated (early) at %s" % ((n, K, G, rho),)) + cells.append(r) + for rho in late_rhos: + r = census_late(n, K, G, rho) + r.update({"n": n, "K": K, "G": G, "rho": rho, "order": "late"}) + for name in ("G0", "G1", "H"): + require(r[name + "_violation"] is None, + "%s sufficiency violated (late) at %s" % (name, (n, K, G, rho))) + require(r["G0_not_G1"] is None, "original guard must imply G1") + expected = H_fraction(n, K, G) * r["total"] + require(expected.denominator == 1 and r["H_admitted"] == expected.numerator, + "H count must match closed form (2) at %s" % ((n, K, G, rho),)) + r["H_fraction"] = [H_fraction(n, K, G).numerator, + H_fraction(n, K, G).denominator] + r["H_count_formula"] = expected.numerator + cells.append(r) + receipt = { + "status": STATUS, + "domain": [[n, K, G, list(e), list(l)] for (n, K, G, e, l) in DOMAIN], + "cells": cells, + **receipts, + } + return json.loads(json.dumps(receipt)) + + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument("--write", metavar="PATH") + ap.add_argument("--check", metavar="PATH") + args = ap.parse_args() + receipt = compute() + if args.write: + target = Path(args.write) + require(not target.exists(), "refusing to overwrite " + str(target)) + target.write_text(json.dumps(receipt, indent=1, sort_keys=True) + "\n", + encoding="utf-8") + else: + target = Path(args.check) if args.check else HERE / "RESULT.json" + expected = json.loads(target.read_text(encoding="utf-8")) + require(receipt == expected, "receipt mismatch against " + str(target)) + totals = sum(c["total"] for c in receipt["cells"]) + ags = sum(c["ag"] for c in receipt["cells"]) + print("%s: %d states; %d raw agreements; %d cells; 2 fixtures; 2 controls" + % (STATUS, totals, ags, len(receipt["cells"]))) + return 0 + + +if __name__ == "__main__": + raise SystemExit(main())