diff --git a/research/fstar-joint-label-census/README.md b/research/fstar-joint-label-census/README.md new file mode 100644 index 0000000000..556f998db1 --- /dev/null +++ b/research/fstar-joint-label-census/README.md @@ -0,0 +1,223 @@ +# Complete joint three-line sub-anchor census + +**The 20 unresolved shareable patterns in PR3031 cannot be realized:** each +contains a declared zero arc with odd anchor parity. A second defect in the +legacy line action generated those inadmissible configurations. The corrected +joint census has **13,449 orbits**, with exactly **seven `box = 2` shapes**; +four are unrealizable and three are Aaron Wang's already-known explicit +realizations. No realization-search remainder survives at this three-line +mask/zero-arc boundary. + +This is a finite exact classification plus a rational rank/valuation argument. +It is not a proof of general F-star, a new decoder construction, a supplier +admission, or a new kappa. In particular, `box = 2` at `v = 3` meets F-star's +threshold `floor(2v/3) = 2`. + +## Assignment and exact sources + +Base: canonical main `18aacb215fc3717b06be8ceb9fca62aeca0d3e99`, priority 6. +This takes the explicit joint-sound-`v=3` follow-up in +[PR3031](https://github.com/CrocSwap/integer-mult-bounds/pull/3031), head +`e75906fc4e8b9f756a9877b2e467f4e564851c7d`. That source warned about per-line +total canonicalization and left 20 shareable patterns not found in its cap. +Its separate `v=5` floor is outside this audit. + +[PR2978](https://github.com/CrocSwap/integer-mult-bounds/pull/2978), head +`12eb7b832de9239a314a7cddf6c6033d618cd8f2`, supplies the audited census and the +three credited decoder witnesses. Only its exact `box_search_kj.py` and +`realize-kj-receipt.json` are retained under [predecessor/](predecessor/), with +origin paths, Git blob IDs and SHA-256 pins in [SOURCES.json](SOURCES.json). +The verifier loads only its two canonicalization definitions, using AST +extraction; it never imports or runs the historical search/dependency tree. +The new census and both exact box checkers are separately implemented here. + +This is a **changed** scope from catalogue card `census-pruning-audit`, whose +F7 parity-pruning starting point already has follow-ups. The handoff-first +override and stopping rule are in [TASK-CARD.md](TASK-CARD.md) and +[TASK.json](TASK.json). Fresh entry overlap checks covered 253 open PRs and +1,858 discussion records, including replies; the sparse checkout limited local +package coverage. PR3031's warning is credited, not claimed as a new discovery. + +## The exact finite domain + +Each of three lines has masks `(a0(t), b0(t))` in `{0,...,7}^2` with +`tau(t) = popcount(a0(t) & b0(t)) >= 1`: **37 raw line types**. The zero-arc +set `Z` is any subset of the six directed off-diagonal pairs satisfying + +```text +(t,s) in Z => popcount(a0(t) & b0(s)) is even. (SG) +``` + +For a kept ordered set `S`, choose `a(t) subset a0(t)` and `b(t) subset b0(t)`. +Require `a(t).b(t) = 1` on `S` and `a(t).b(s) = 0` for every zero arc whose +source precedes its target in `S`. `box` is the largest possible `|S|`. +Full unrestricted masks give `cert_max = 3` for every `Z`: the labels +`a(t) = b(t) = e_t` work even when every off-diagonal arc is zero. + +The allowed symmetry is one **global** permutation of the three shared total +coordinates and one permutation of the three lines. No independent per-line +total relabeling or source/target transposition is included. + +## Two distinct quotient failures + +**1. Per-line total canonicalization loses the joint domain** (PR3031's +observation, now with an exact control). Compare the triples + +```text +((3,3), (3,3), (3,3)) +((3,3), (3,3), (5,5)). +``` + +Each line separately canonicalizes to `(3,3)` in both triples. The first triple +allows all six zero arcs; the second allows only `(0,1)` and `(1,0)`. No global +total permutation identifies these triples. The scope-valid inputs built from +the ten legacy per-line representatives cover only **1,446** of the **13,449** +joint orbits, omitting **12,003**. The corrected census finds `box = 3` on all +those omitted orbits; it does not uncover another `box < 3` shape. + +**2. The line action also moves edges in the wrong direction** (new audit). +The old `canon_config` uses + +```python +npairs[t] = pairs[perm[t]] # pull back line data +nZ = {(perm[t], perm[s]) for (t,s) in Z} # push forward old edges +``` + +These conventions disagree on three-cycles. With new line `t` meaning old line +`perm[t]`, new arc `(t,s)` must mean old arc `(perm[t],perm[s])`; equivalently, +old edges must move by the **inverse** permutation. Here is a minimal control: + +| | Line pairs | Zero arc | Anchor dot product at that arc | +|---|---|---|---| +| Valid input | `((1,3),(3,1),(1,1))` | `(1,0)` | `3 . 3 = 0` | +| Legacy output | `((1,1),(1,3),(3,1))` | `(0,2)` | `1 . 1 = 1` | +| Correct output | `((1,1),(1,3),(3,1))` | `(2,1)` | `3 . 3 = 0` | + +Dots in this table are over `F2`. The original data obey (SG), but their old +"canonical" output violates it. Reproducing the legacy enumeration gives its +exact **3,023** keys and **27** gap candidates. **1,370** keys violate (SG), +including **20** gap candidates. Those 20 are exactly the shareable patterns +left unresolved in PR3031. [RESULTS.json](RESULTS.json) records every affected +source-receipt index and every offending arc; this is an exact exclusion, +independent of search alphabet or cap. The other one of the original 21 +not-found candidates is the already-identified rank-two obstruction below. + +## Complete corrected classification + +[census.py](census.py) enumerates the **9,139** multisets of three raw line +types and all their legal zero-arc subsets. It minimizes the full joint pair +data under the global action, keeping every line permutation attaining the +minimum before minimizing the arc mask. Every ordered configuration is a +permutation of one such multiset, so this covers the domain. + +A separate Burnside calculation uses **ordered** triples, fixed points of all +36 group elements and cycles of their action on the six directed arcs. It does +not use the canonicalizer or multiset reduction. Its identity fixed count is +**450,028** and the sum of fixed counts is **484,164**, giving +`484164 / 36 = 13449` orbits. All 36 counts are in the receipt. + +On **every** orbit, an independent definition-level checker enumerates all +local `(a,b)` label pairs with odd diagonal and all six kept orders. It agrees +with the singleton/chronological checker on all **13,449** full-kept decisions: +**13,442** have `box = 3`, and the following **seven** have `box = 2`. +All seven have **complete `Z`**, with the displayed representatives: + +| `a0` | `b0` | Realizability | Credited witness diagonal `M` | +|---|---|---|---| +| `3,3,3` | `3,3,3` | Impossible | — | +| `3,3,3` | `3,3,7` | Impossible | — | +| `3,3,7` | `3,3,3` | Realized in PR2978 | `8,8,12` | +| `3,3,3` | `3,7,7` | Impossible | — | +| `3,7,7` | `3,3,3` | Realized in PR2978 | `2,12,-4` | +| `3,3,3` | `7,7,7` | Impossible | — | +| `7,7,7` | `3,3,3` | Realized in PR2978 | `-16,24,16` | + +Masks `3` and `7` mean binary `011` and `111`. For each row, labels `1` on +line 0 and `2` on line 1 witness `box >= 2`. One anchor side is confined to +two bits, so `K = A B^T` has rank at most two over `F2`. Keeping all three +lines under complete `Z` would make `K` triangular with unit diagonal after +ordering, giving rank three. Thus `box <= 2` also has a short written proof. + +**Why the four impossible rows have no rational decoder.** Complete `Z` and +nonzero diagonal force `M` to be diagonal of rank three. In a three-total +factorization `M = P Q^T`, every column of both `P` and `Q` must therefore +be nonzero. For each column `j`, the minimum rational 2-adic valuation +`m_j = min_t v2(P_tj)` is finite and attained, hence bit `j` occurs in some +`a0(t)`. Those four rows have `union_t a0(t) = 3`, omitting bit 2: contradiction. +This argument includes PR3031's already-settled `(3,3)^3` obstruction. + +**Why the parity exclusions apply to actual decoders.** For each nondegenerate +total, let `n_j = min_s v2(Q_sj)` and `gamma = min_j(m_j+n_j)`. +Every product term has valuation at least `gamma`. Its reduction after division +by `2^gamma` is odd exactly when `a0_j(t) = b0_j(s) = 1`. Thus the reduction of +`2^-gamma M_ts` is `a0(t).b0(s)` over `F2`. In particular, `M_ts = 0` forces +(SG). Degenerate totals contribute zero. This holds for rational coefficients, +including negative valuations; no bounded integer alphabet is assumed. + +The three realized rows are **not new constructions**. The verifier recomputes +their `P Q^T`, column valuations, `gamma`, anchor masks and zero arcs from +PR2978's exact integer matrices. It separately checks full-support L8 witnesses +of size three, proving `cert = 3` on those three credited examples. +The classification is of anchor/zero-arc shapes, not of every rational matrix +or of every possible `cert` value within a shape. + +## Reproduce and scope of verification + +Python 3.10+ standard library only, no network or solver at replay time: + +```sh +python3 -B research/fstar-joint-label-census/verify.py +python3 scripts/research_package.py --package research/fstar-joint-label-census --check-only +python3.12 scripts/research_package.py --package research/fstar-joint-label-census +``` + +Direct replay recomputes and compares the deterministic receipt without writing +it. `--write` is the explicit regeneration option. Expected principal markers: + +```text +PASS_JOINT_CENSUS ordered=450028 orbits=13449 box3=13442 box2=7 brute=13449 +PASS_LEGACY_AUDIT states=3023 invalid=1370 candidates=27 invalid_candidates=20 +PASS_REALIZATION_CLASSIFICATION shapes=7 realized=3 impossible=4 +``` + +Controls include both legacy quotient failures, direct versus optimized group +actions, all 384 line/arc-mask transforms, all 36 transforms of 80 deterministic +joint states, a valid diagonal witness, rejected broken-diagonal and forward-arc +witnesses, and the passing reversed-order control. The verifier uses explicit +exceptions, so checks stay enabled under Python optimization. Source pins bind +both retained predecessor files; the historical selected record and catalogue +are provenance only. + +This does **not** replay PR3031's separate `v=5` proof, larger-`v` censuses, +selected suppliers, physical costs, moments, native compilers or Lean. The +`v=3` defects and exclusions do not by themselves invalidate those separate +results. Source retention and passing metadata are distinct from independent +human review or mathematical admission. + +## Open next questions + +1. **Independently audit PR3031's separate `v=5` enumerator and blocking proof.** + It uses raw types, so the two `v=3` defects alone do not refute it. Inspect + its actual group action and small definition-level controls first. That + source/replay is outside this package; it needs its own overlap check. +2. **Larger joint domains (`v >= 4`).** Use global coordinate relabeling and + zero-arc/column-attainment screens before a bounded census. This would test + a remaining box-completeness boundary; it needs a new budget and does not + follow from the three-line classification. See [TASK.json](TASK.json). + +## Credit and license + +F-star, `cert(M)`, L8 labels and the cost-to-certificate implication are +DreamingOfClouds' work in +[PR1590](https://github.com/CrocSwap/integer-mult-bounds/pull/1590), with the +source's stated Claude assistance. Aaron Wang (`navinor`), with opencode +assistance, supplied the anchor/box machinery and lineage, PR2978's census and +all three realized witnesses, and PR3031's per-line-canonicalization warning, +rank-two exclusion and explicit follow-up. Their source files and attribution +are preserved. This package adds the consistent global census, independent +counts and checkers, the second line-action counterexample, and exact exclusion +of the remaining 20 patterns. + +Prepared by **Arham Tahir with substantial OpenAI Codex assistance**. No +independent human or Lean review is claimed. New work and retained repository +sources are Apache-2.0; the repository [LICENSE](../../LICENSE) applies. diff --git a/research/fstar-joint-label-census/RESULTS.json b/research/fstar-joint-label-census/RESULTS.json new file mode 100644 index 0000000000..19720438fe --- /dev/null +++ b/research/fstar-joint-label-census/RESULTS.json @@ -0,0 +1,1509 @@ +{ + "box2_orbits": 7, + "box3_orbits": 13442, + "brute_oracle_checks": 13449, + "burnside_fixed_counts": [ + 450028, + 5344, + 5344, + 1, + 1, + 5344, + 3556, + 764, + 764, + 1, + 1, + 764, + 3556, + 764, + 764, + 1, + 1, + 764, + 64, + 16, + 16, + 82, + 82, + 16, + 64, + 16, + 16, + 82, + 82, + 16, + 3556, + 764, + 764, + 1, + 1, + 764 + ], + "chronological_fallbacks": 99, + "controls": { + "action_samples": 80, + "line_action_failure": { + "correct": { + "Z": [ + [ + 2, + 1 + ] + ], + "pairs": [ + [ + 1, + 1 + ], + [ + 1, + 3 + ], + [ + 3, + 1 + ] + ] + }, + "input": { + "Z": [ + [ + 1, + 0 + ] + ], + "pairs": [ + [ + 1, + 3 + ], + [ + 3, + 1 + ], + [ + 1, + 1 + ] + ] + }, + "legacy": { + "Z": [ + [ + 0, + 2 + ] + ], + "pairs": [ + [ + 1, + 1 + ], + [ + 1, + 3 + ], + [ + 3, + 1 + ] + ] + } + }, + "per_line_loss": { + "allowed_Z_masks": [ + 63, + 5 + ], + "first": [ + [ + 3, + 3 + ], + [ + 3, + 3 + ], + [ + 3, + 3 + ] + ], + "second": [ + [ + 3, + 3 + ], + [ + 3, + 3 + ], + [ + 5, + 5 + ] + ] + }, + "witness_rejections": 2 + }, + "domain": { + "lines": 3, + "tau_min": 1, + "totals": 3 + }, + "gap_shapes": [ + { + "Z": [ + [ + 0, + 1 + ], + [ + 0, + 2 + ], + [ + 1, + 0 + ], + [ + 1, + 2 + ], + [ + 2, + 0 + ], + [ + 2, + 1 + ] + ], + "box": 2, + "pairs": [ + [ + 3, + 3 + ], + [ + 3, + 3 + ], + [ + 3, + 3 + ] + ], + "status": "unrealizable: diagonal rank three requires three nondegenerate totals; each P-column minimum must be attained", + "witness": null + }, + { + "Z": [ + [ + 0, + 1 + ], + [ + 0, + 2 + ], + [ + 1, + 0 + ], + [ + 1, + 2 + ], + [ + 2, + 0 + ], + [ + 2, + 1 + ] + ], + "box": 2, + "pairs": [ + [ + 3, + 3 + ], + [ + 3, + 3 + ], + [ + 3, + 7 + ] + ], + "status": "unrealizable: diagonal rank three requires three nondegenerate totals; each P-column minimum must be attained", + "witness": null + }, + { + "Z": [ + [ + 0, + 1 + ], + [ + 0, + 2 + ], + [ + 1, + 0 + ], + [ + 1, + 2 + ], + [ + 2, + 0 + ], + [ + 2, + 1 + ] + ], + "box": 2, + "pairs": [ + [ + 3, + 3 + ], + [ + 3, + 3 + ], + [ + 7, + 3 + ] + ], + "status": "realized: predecessor integer P,Q replayed; box=2, cert=3", + "witness": { + "M": [ + [ + 8, + 0, + 0 + ], + [ + 0, + 8, + 0 + ], + [ + 0, + 0, + 12 + ] + ], + "P": [ + [ + -1, + -3, + 0 + ], + [ + 1, + -1, + -2 + ], + [ + 3, + 3, + 3 + ] + ], + "Q": [ + [ + 1, + -3, + 2 + ], + [ + 3, + -1, + -2 + ], + [ + 3, + -1, + 2 + ] + ], + "cert_witness": [ + [ + 1, + 2, + 4 + ], + [ + 1, + 2, + 4 + ], + [ + 0, + 1, + 2 + ] + ], + "gamma": 0 + } + }, + { + "Z": [ + [ + 0, + 1 + ], + [ + 0, + 2 + ], + [ + 1, + 0 + ], + [ + 1, + 2 + ], + [ + 2, + 0 + ], + [ + 2, + 1 + ] + ], + "box": 2, + "pairs": [ + [ + 3, + 3 + ], + [ + 3, + 7 + ], + [ + 3, + 7 + ] + ], + "status": "unrealizable: diagonal rank three requires three nondegenerate totals; each P-column minimum must be attained", + "witness": null + }, + { + "Z": [ + [ + 0, + 1 + ], + [ + 0, + 2 + ], + [ + 1, + 0 + ], + [ + 1, + 2 + ], + [ + 2, + 0 + ], + [ + 2, + 1 + ] + ], + "box": 2, + "pairs": [ + [ + 3, + 3 + ], + [ + 7, + 3 + ], + [ + 7, + 3 + ] + ], + "status": "realized: predecessor integer P,Q replayed; box=2, cert=3", + "witness": { + "M": [ + [ + 2, + 0, + 0 + ], + [ + 0, + 12, + 0 + ], + [ + 0, + 0, + -4 + ] + ], + "P": [ + [ + -1, + 3, + 0 + ], + [ + 3, + -3, + 3 + ], + [ + -1, + 1, + 1 + ] + ], + "Q": [ + [ + 1, + 1, + 0 + ], + [ + 3, + 1, + 2 + ], + [ + 3, + 1, + -2 + ] + ], + "cert_witness": [ + [ + 1, + 2, + 4 + ], + [ + 1, + 2, + 4 + ], + [ + 0, + 1, + 2 + ] + ], + "gamma": 0 + } + }, + { + "Z": [ + [ + 0, + 1 + ], + [ + 0, + 2 + ], + [ + 1, + 0 + ], + [ + 1, + 2 + ], + [ + 2, + 0 + ], + [ + 2, + 1 + ] + ], + "box": 2, + "pairs": [ + [ + 3, + 7 + ], + [ + 3, + 7 + ], + [ + 3, + 7 + ] + ], + "status": "unrealizable: diagonal rank three requires three nondegenerate totals; each P-column minimum must be attained", + "witness": null + }, + { + "Z": [ + [ + 0, + 1 + ], + [ + 0, + 2 + ], + [ + 1, + 0 + ], + [ + 1, + 2 + ], + [ + 2, + 0 + ], + [ + 2, + 1 + ] + ], + "box": 2, + "pairs": [ + [ + 7, + 3 + ], + [ + 7, + 3 + ], + [ + 7, + 3 + ] + ], + "status": "realized: predecessor integer P,Q replayed; box=2, cert=3", + "witness": { + "M": [ + [ + -16, + 0, + 0 + ], + [ + 0, + 24, + 0 + ], + [ + 0, + 0, + 16 + ] + ], + "P": [ + [ + -3, + -1, + -3 + ], + [ + 3, + -3, + -3 + ], + [ + 1, + 3, + -3 + ] + ], + "Q": [ + [ + 3, + 1, + 2 + ], + [ + 3, + -3, + -2 + ], + [ + 1, + 3, + -2 + ] + ], + "cert_witness": [ + [ + 1, + 2, + 4 + ], + [ + 1, + 2, + 4 + ], + [ + 0, + 1, + 2 + ] + ], + "gamma": 0 + } + } + ], + "global_orbits": 13449, + "legacy": { + "legacy_candidates": 27, + "line_types": 10, + "omitted_valid_orbits": 12003, + "represented_valid_orbits": 1446, + "scope_inconsistent_candidates": [ + { + "Z": [ + [ + 0, + 1 + ], + [ + 1, + 0 + ] + ], + "odd_anchor_zero_arcs": [ + [ + 0, + 1 + ], + [ + 1, + 0 + ] + ], + "pairs": [ + [ + 1, + 1 + ], + [ + 3, + 5 + ], + [ + 7, + 3 + ] + ], + "source_record_index": 0 + }, + { + "Z": [ + [ + 0, + 1 + ], + [ + 1, + 0 + ] + ], + "odd_anchor_zero_arcs": [ + [ + 0, + 1 + ], + [ + 1, + 0 + ] + ], + "pairs": [ + [ + 1, + 1 + ], + [ + 3, + 5 + ], + [ + 7, + 7 + ] + ], + "source_record_index": 1 + }, + { + "Z": [ + [ + 0, + 1 + ], + [ + 1, + 0 + ] + ], + "odd_anchor_zero_arcs": [ + [ + 0, + 1 + ], + [ + 1, + 0 + ] + ], + "pairs": [ + [ + 3, + 1 + ], + [ + 3, + 5 + ], + [ + 7, + 3 + ] + ], + "source_record_index": 2 + }, + { + "Z": [ + [ + 0, + 1 + ], + [ + 1, + 0 + ], + [ + 2, + 1 + ] + ], + "odd_anchor_zero_arcs": [ + [ + 0, + 1 + ], + [ + 1, + 0 + ] + ], + "pairs": [ + [ + 3, + 1 + ], + [ + 3, + 5 + ], + [ + 7, + 3 + ] + ], + "source_record_index": 3 + }, + { + "Z": [ + [ + 0, + 1 + ], + [ + 1, + 0 + ] + ], + "odd_anchor_zero_arcs": [ + [ + 0, + 1 + ], + [ + 1, + 0 + ] + ], + "pairs": [ + [ + 3, + 1 + ], + [ + 3, + 5 + ], + [ + 7, + 7 + ] + ], + "source_record_index": 4 + }, + { + "Z": [ + [ + 0, + 1 + ], + [ + 1, + 0 + ], + [ + 2, + 1 + ] + ], + "odd_anchor_zero_arcs": [ + [ + 0, + 1 + ], + [ + 1, + 0 + ] + ], + "pairs": [ + [ + 3, + 1 + ], + [ + 3, + 5 + ], + [ + 7, + 7 + ] + ], + "source_record_index": 5 + }, + { + "Z": [ + [ + 0, + 1 + ], + [ + 0, + 2 + ], + [ + 1, + 0 + ] + ], + "odd_anchor_zero_arcs": [ + [ + 0, + 1 + ], + [ + 1, + 0 + ] + ], + "pairs": [ + [ + 3, + 5 + ], + [ + 3, + 5 + ], + [ + 7, + 3 + ] + ], + "source_record_index": 11 + }, + { + "Z": [ + [ + 0, + 1 + ], + [ + 0, + 2 + ], + [ + 1, + 0 + ], + [ + 2, + 0 + ] + ], + "odd_anchor_zero_arcs": [ + [ + 0, + 1 + ], + [ + 1, + 0 + ] + ], + "pairs": [ + [ + 3, + 5 + ], + [ + 3, + 5 + ], + [ + 7, + 3 + ] + ], + "source_record_index": 12 + }, + { + "Z": [ + [ + 0, + 1 + ], + [ + 1, + 0 + ] + ], + "odd_anchor_zero_arcs": [ + [ + 0, + 1 + ], + [ + 1, + 0 + ] + ], + "pairs": [ + [ + 3, + 5 + ], + [ + 3, + 5 + ], + [ + 7, + 3 + ] + ], + "source_record_index": 13 + }, + { + "Z": [ + [ + 0, + 1 + ], + [ + 1, + 0 + ], + [ + 1, + 2 + ] + ], + "odd_anchor_zero_arcs": [ + [ + 0, + 1 + ], + [ + 1, + 0 + ] + ], + "pairs": [ + [ + 3, + 5 + ], + [ + 3, + 5 + ], + [ + 7, + 3 + ] + ], + "source_record_index": 14 + }, + { + "Z": [ + [ + 0, + 1 + ], + [ + 1, + 0 + ], + [ + 1, + 2 + ], + [ + 2, + 1 + ] + ], + "odd_anchor_zero_arcs": [ + [ + 0, + 1 + ], + [ + 1, + 0 + ] + ], + "pairs": [ + [ + 3, + 5 + ], + [ + 3, + 5 + ], + [ + 7, + 3 + ] + ], + "source_record_index": 15 + }, + { + "Z": [ + [ + 0, + 1 + ], + [ + 1, + 0 + ], + [ + 2, + 0 + ] + ], + "odd_anchor_zero_arcs": [ + [ + 0, + 1 + ], + [ + 1, + 0 + ] + ], + "pairs": [ + [ + 3, + 5 + ], + [ + 3, + 5 + ], + [ + 7, + 3 + ] + ], + "source_record_index": 16 + }, + { + "Z": [ + [ + 0, + 1 + ], + [ + 1, + 0 + ], + [ + 2, + 1 + ] + ], + "odd_anchor_zero_arcs": [ + [ + 0, + 1 + ], + [ + 1, + 0 + ] + ], + "pairs": [ + [ + 3, + 5 + ], + [ + 3, + 5 + ], + [ + 7, + 3 + ] + ], + "source_record_index": 17 + }, + { + "Z": [ + [ + 0, + 1 + ], + [ + 0, + 2 + ], + [ + 1, + 0 + ] + ], + "odd_anchor_zero_arcs": [ + [ + 0, + 1 + ], + [ + 1, + 0 + ] + ], + "pairs": [ + [ + 3, + 5 + ], + [ + 3, + 5 + ], + [ + 7, + 7 + ] + ], + "source_record_index": 18 + }, + { + "Z": [ + [ + 0, + 1 + ], + [ + 0, + 2 + ], + [ + 1, + 0 + ], + [ + 2, + 0 + ] + ], + "odd_anchor_zero_arcs": [ + [ + 0, + 1 + ], + [ + 1, + 0 + ] + ], + "pairs": [ + [ + 3, + 5 + ], + [ + 3, + 5 + ], + [ + 7, + 7 + ] + ], + "source_record_index": 19 + }, + { + "Z": [ + [ + 0, + 1 + ], + [ + 1, + 0 + ] + ], + "odd_anchor_zero_arcs": [ + [ + 0, + 1 + ], + [ + 1, + 0 + ] + ], + "pairs": [ + [ + 3, + 5 + ], + [ + 3, + 5 + ], + [ + 7, + 7 + ] + ], + "source_record_index": 20 + }, + { + "Z": [ + [ + 0, + 1 + ], + [ + 1, + 0 + ], + [ + 1, + 2 + ] + ], + "odd_anchor_zero_arcs": [ + [ + 0, + 1 + ], + [ + 1, + 0 + ] + ], + "pairs": [ + [ + 3, + 5 + ], + [ + 3, + 5 + ], + [ + 7, + 7 + ] + ], + "source_record_index": 21 + }, + { + "Z": [ + [ + 0, + 1 + ], + [ + 1, + 0 + ], + [ + 1, + 2 + ], + [ + 2, + 1 + ] + ], + "odd_anchor_zero_arcs": [ + [ + 0, + 1 + ], + [ + 1, + 0 + ] + ], + "pairs": [ + [ + 3, + 5 + ], + [ + 3, + 5 + ], + [ + 7, + 7 + ] + ], + "source_record_index": 22 + }, + { + "Z": [ + [ + 0, + 1 + ], + [ + 1, + 0 + ], + [ + 2, + 0 + ] + ], + "odd_anchor_zero_arcs": [ + [ + 0, + 1 + ], + [ + 1, + 0 + ] + ], + "pairs": [ + [ + 3, + 5 + ], + [ + 3, + 5 + ], + [ + 7, + 7 + ] + ], + "source_record_index": 23 + }, + { + "Z": [ + [ + 0, + 1 + ], + [ + 1, + 0 + ], + [ + 2, + 1 + ] + ], + "odd_anchor_zero_arcs": [ + [ + 0, + 1 + ], + [ + 1, + 0 + ] + ], + "pairs": [ + [ + 3, + 5 + ], + [ + 3, + 5 + ], + [ + 7, + 7 + ] + ], + "source_record_index": 24 + } + ], + "scope_inconsistent_states": 1370, + "states": 3023 + }, + "raw_line_type_multisets": 9139, + "raw_ordered_states": 450028, + "schema_version": 1, + "source_pins": 2 +} diff --git a/research/fstar-joint-label-census/SOURCES.json b/research/fstar-joint-label-census/SOURCES.json new file mode 100644 index 0000000000..5ef0522d60 --- /dev/null +++ b/research/fstar-joint-label-census/SOURCES.json @@ -0,0 +1,45 @@ +{ + "schema_version": 1, + "base_commit": "18aacb215fc3717b06be8ceb9fca62aeca0d3e99", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + } + ], + "archived_sources": [ + { + "repository": "CrocSwap/integer-mult-bounds", + "pr": 2978, + "head": "12eb7b832de9239a314a7cddf6c6033d618cd8f2", + "path": "research/fstar-box-withoutloss-seed7f3a1c/box_search_kj.py", + "vendored_path": "predecessor/box_search_kj.py", + "sha256": "f341925160cc8476dd3484d3ba513a3e1428804fbd9c804e9db62a9c3e3a85f8", + "git_blob": "018c744279eed03ffecfaca528473def2aad60cd", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/12eb7b832de9239a314a7cddf6c6033d618cd8f2/research/fstar-box-withoutloss-seed7f3a1c/box_search_kj.py" + }, + { + "repository": "CrocSwap/integer-mult-bounds", + "pr": 2978, + "head": "12eb7b832de9239a314a7cddf6c6033d618cd8f2", + "path": "research/fstar-box-withoutloss-seed7f3a1c/data/realize-kj-receipt.json", + "vendored_path": "predecessor/realize-kj-receipt.json", + "sha256": "93ec89e6fc2ce60fdcddd1516fd31fd29686fc5efd4dd7b6831e0ed45e006cce", + "git_blob": "829c40d4927dd208a7504ecdd48add36499eb0e1", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/12eb7b832de9239a314a7cddf6c6033d618cd8f2/research/fstar-box-withoutloss-seed7f3a1c/data/realize-kj-receipt.json" + } + ], + "handoff": { + "pr": 3031, + "head": "e75906fc4e8b9f756a9877b2e467f4e564851c7d", + "scope": "Methodological caveat requesting a joint-sound v=3 census; no source from PR3031 executed." + } +} diff --git a/research/fstar-joint-label-census/TASK-CARD.md b/research/fstar-joint-label-census/TASK-CARD.md new file mode 100644 index 0000000000..1e19e87b6f --- /dev/null +++ b/research/fstar-joint-label-census/TASK-CARD.md @@ -0,0 +1,24 @@ +Task: fstar-joint-label-census (handoff-first; census-pruning-audit scope changed). +Base: 18aacb215fc3717b06be8ceb9fca62aeca0d3e99, priority revision 6. +Predecessors: Aaron Wang/navinor PR2978 at 12eb7b832de9239a314a7cddf6c6033d618cd8f2; +PR3031 at e75906fc4e8b9f756a9877b2e467f4e564851c7d, methodological caveat. +Question: enumerate every three-line tau>=1 joint mask/zero-arc configuration +under GLOBAL total permutations and line permutations; compare the 3023-state +legacy census and identify exactly what its quotient omits or identifies. +Changed scope: the catalogue census audit starts with the already-covered F7 +parity prune. This takes PR3031's explicit joint-sound-v3 follow-up instead. +Method/domain: a0,b0 in 0..7 with nonempty intersection on each of three lines; +Z any subset of the six off-diagonal arcs with even anchor dot product. +Use a definition-level exact label/order checker, correct group action and an +independent Burnside orbit count. Check tiny controls and legacy mutants. +Success: corrected counts, a concrete loss witness, and explicit downstream +limits. Stop at that finite classification; no rational realizability census, +F-star proof, new supplier, paid moment, kappa, or frontier update. +Budget: about 60 minutes including review and handoff. Cleanup requested by the +user is separate from the mathematical scope. +Nearest overlap: PR3031 identifies the issue but does not do the corrected +census. PR2978 supplies the flawed census and earlier realized box gap. +Attribution: F-star/L8/cert from DreamingOfClouds PR1590; box machinery and +canonicalization warning from Aaron Wang/navinor. New code: Arham Tahir with +substantial OpenAI Codex assistance. Apache-2.0. +Expected reproduction: python3 -B research/fstar-joint-label-census/verify.py diff --git a/research/fstar-joint-label-census/TASK.json b/research/fstar-joint-label-census/TASK.json new file mode 100644 index 0000000000..d8e07ddf9c --- /dev/null +++ b/research/fstar-joint-label-census/TASK.json @@ -0,0 +1,99 @@ +{ + "schema_version": 1, + "task_id": "census-pruning-audit", + "priority_revision": 6, + "base_commit": "18aacb215fc3717b06be8ceb9fca62aeca0d3e99", + "original_card": { + "id": "census-pruning-audit", + "question": "Does the reported word-census parity-pruning error invalidate a specific exclusion we still rely on, and what bounded repair is justified?", + "starting_points": [ + "research/f7-weight-parity-census-correction/README.md", + "docs/research/research-family-status.md" + ], + "methods": [ + "Independently reconstruct the tiny counterexample and trace one affected exclusion to its exact pruning code.", + "Compare corrected and unpruned enumeration on a small exhaustive domain, then audit the changed pruning implication." + ], + "acceptance_gate": "Pin the old and proposed corrected engines, distinguish a disproved pruning rule from a disproved final bound, and state exactly which downstream exclusions need revalidation. #2973 is an author-checked source archive; neither its new f(7) claim nor all old conclusions are automatically accepted or rejected.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read #2973 error description and MATH.md; manually reconstruct the prefix states of 01021323 before running any large census.", + "scope": "Source-binding orientation only; no full enumeration or mathematical validation." + }, + "first_experiment": "Reconstruct the eight prefix states of 01021323 and compare bit-0 versus Hamming-weight parity budgets independently. Trace the reported false prune to one pinned predecessor (#2542, #2634 or #2691), then test a small exhaustive domain. Stop after a source-impact handoff or corrected-prune proof; a full seven-label replay needs a separate resource budget and a named research decision it can change.", + "bottleneck_link": "An unsound exclusion can wrongly close a mechanism; correcting its dependency boundary is more useful than extending the same census.", + "allowed_variations": [ + "One predecessor pruning rule, one independently exhaustive small domain, or one downstream dependency audit." + ], + "scope_change_triggers": [ + "Launching a larger census before validating the prune and explaining which active decision it changes.", + "Treating a small-domain counterexample to the old rule as a counterexample to every reported seven-label bound." + ], + "overlap_terms": [ + "2973", + "2542", + "2634", + "2691", + "weight parity", + "bit-0", + "01021323", + "census pruning" + ] + }, + "scope_status": "changed", + "actual_scope": "Complete the joint-sound v=3 sub-anchor-mask/zero-arc census requested by PR3031; audit the legacy quotient and classify its 21 not-found candidates.", + "scope_change_reason": "Handoff-first override: the catalogue card starts from the already-audited F7 parity prune. PR3031 explicitly requests a different missing census check, on three-total rational-decoder anchor data.", + "bottleneck_link": "A complete finite classification prevents spending further realization searches on scope-inconsistent quotient artifacts in the F-star/box-completeness line. It does not improve a supplier or a paid moment.", + "budget_minutes": 60, + "stop_rule": "Stop after the finite three-line joint census, independent orbit/label checks and disposition of the existing 27 candidates. No larger v, new decoder search or supplier adoption.", + "outcome": "completed", + "evidence": "RESULTS.json: 450028 ordered states; 13449 global orbits independently counted by Burnside; all 13449 full-box decisions cross-checked by exhaustive label/order enumeration; seven box=2 shapes, four impossible and three credited explicit realizations. Twenty of the 21 legacy not-found candidates violate zero-arc parity; the remaining one fails rank/anchor attainment.", + "author": "Arham Tahir, with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance in source inspection, proof, independent code, checks and writing; no independent human or Lean review.", + "open_questions": [ + { + "question": "Does the v=5 envelope/blocking proof in PR3031 remain valid under its separate raw-type enumerator?", + "why_it_matters": "The two legacy v=3 quotient defects do not themselves affect that separate proof; an independent audit must trace the actual code and certificate.", + "first_step": "Inspect its raw-type and blocking-Z action separately, using definition-level small controls before rerunning the large census.", + "blocked_by": "Outside this package; no v=5 replay or source adoption was performed." + }, + { + "question": "For v>=4, which tau>=1 joint anchor data admit box< v while satisfying rational rank and valuation constraints?", + "why_it_matters": "The v=3 combinatorial and realization remainder is closed here; larger domains remain potentially informative for box completeness and F-star.", + "first_step": "Use a global joint action and apply zero-arc parity/column attainment screens before a bounded v=4 census.", + "blocked_by": "A new budget and overlap check; no inference about all-v F-star follows from the three-line result." + } + ], + "method": "Exact finite enumeration under a global S3 total action and consistent S3 line action, independent Burnside count and definition-level brute label/order oracle.", + "parameter_domain": "v=3, three shared bit positions, a0,b0 in 0..7, tau=popcount(a0&b0)>=1 per line, and arbitrary zero-arc subsets whose anchor dot products are even.", + "handoff_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18981329", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1317#discussioncomment-18985904", + "verification": { + "platform": "macOS-26.3.1-arm64-arm-64bit-Mach-O", + "python_direct": "3.14.7", + "python_registered": "Python 3.12.14", + "commands": [ + "python3 -B research/fstar-joint-label-census/verify.py", + "python3 -O -B research/fstar-joint-label-census/verify.py", + "python3.12 scripts/research_package.py --package research/fstar-joint-label-census", + "python3 scripts/research_package.py --package research/fstar-joint-label-census --check-only" + ], + "outcome": "All passed with identical deterministic receipt; optimized checks remain enabled. Hosted CI and independent human review are separate.", + "export_failure_controls": "In a temporary standalone copy under Python optimization: appended predecessor byte rejected before evaluation; appended receipt byte rejected after replay. Original package unchanged." + }, + "submission_freshness": { + "canonical_main": "18aacb215fc3717b06be8ceb9fca62aeca0d3e99", + "priority_revision": 6, + "overlap_checked_at": "2026-10-17T00:53:59.478350+00:00", + "open_prs": 256, + "discussion_records": 1862, + "remote_pagination_complete": true, + "new_competing_scope_found": false, + "local_coverage": "Sparse checkout: new package, central ledger, and explicitly inspected relevant F-star packages; not a full local code-diff survey." + } +} diff --git a/research/fstar-joint-label-census/VERIFY.json b/research/fstar-joint-label-census/VERIFY.json new file mode 100644 index 0000000000..cc617b381c --- /dev/null +++ b/research/fstar-joint-label-census/VERIFY.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact three-line census, independent Burnside count, exhaustive label/order oracle on every orbit, two legacy quotient counterexamples, all 27 legacy candidate dispositions, three source P,Q realizations, positive and rejecting witness controls, immutable source byte pins and deterministic receipt equality." + } + ] +} diff --git a/research/fstar-joint-label-census/census.py b/research/fstar-joint-label-census/census.py new file mode 100644 index 0000000000..4edd9adba4 --- /dev/null +++ b/research/fstar-joint-label-census/census.py @@ -0,0 +1,208 @@ +"""Independent three-line joint-mask census. Standard library; no legacy imports. + +An arc (t,s) constrains a(t).b(s) only when t precedes s in the kept order. +All permutations below are pullbacks: new line i is old line perm[i]. +""" +from collections import Counter +from itertools import combinations_with_replacement, permutations, product +from math import factorial + +PERMS = tuple(permutations(range(3))) +ARCS = tuple((t, s) for t in range(3) for s in range(3) if t != s) +ARC_INDEX = {edge: i for i, edge in enumerate(ARCS)} +TYPES = tuple((a, b) for a in range(8) for b in range(8) if a & b) + + +def dot(a, b): + return (a & b).bit_count() % 2 + + +def move_mask(mask, perm): + return sum(1 << perm[j] for j in range(3) if mask & (1 << j)) + + +TOTAL_MAPS = tuple(tuple(move_mask(x, p) for x in range(8)) for p in PERMS) +LINE_MAPS = tuple(tuple(sum(1 << i for i, (t, s) in enumerate(ARCS) + if z & (1 << ARC_INDEX[(p[t], p[s])])) + for z in range(64)) for p in PERMS) + + +def allowed_arcs(pairs): + return sum(1 << i for i, (t, s) in enumerate(ARCS) + if dot(pairs[t][0], pairs[s][1]) == 0) + + +def subsets(mask): + value = mask + while True: + yield value + if not value: + return + value = (value - 1) & mask + + +def relabel(pairs, z, line_perm, total_perm): + """Definition-level joint S3 x S3 action; used by independent controls.""" + pp = tuple((move_mask(pairs[t][0], total_perm), + move_mask(pairs[t][1], total_perm)) for t in line_perm) + zz = sum(1 << i for i, (t, s) in enumerate(ARCS) + if z & (1 << ARC_INDEX[(line_perm[t], line_perm[s])])) + return pp, zz + + +def direct_canonical(pairs, z): + return min(relabel(pairs, z, lp, tp) for lp in PERMS for tp in PERMS) + + +def pair_plan(pairs): + """Minimize pair data first, retaining ALL attaining line permutations. + + A total permutation does not change Z. Therefore only line permutations + attaining the smallest pair tuple need be tried for the secondary Z key. + """ + best, attaining = None, set() + for mapping in TOTAL_MAPS: + moved = tuple((mapping[a], mapping[b]) for a, b in pairs) + for i, p in enumerate(PERMS): + key = tuple(moved[t] for t in p) + if best is None or key < best: + best, attaining = key, {i} + elif key == best: + attaining.add(i) + return best, tuple(sorted(attaining)) + + +def canonical_from_plan(plan, z): + pairs, line_maps = plan + return pairs, min(LINE_MAPS[i][z] for i in line_maps) + + +def enumerate_orbits(): + configurations = set() + ordered_count = 0 + multiset_count = 0 + for pairs in combinations_with_replacement(TYPES, 3): + multiset_count += 1 + available = allowed_arcs(pairs) + multiplicity = factorial(3) + for count in Counter(pairs).values(): + multiplicity //= factorial(count) + ordered_count += multiplicity * (1 << available.bit_count()) + plan = pair_plan(pairs) + configurations.update(canonical_from_plan(plan, z) + for z in subsets(available)) + return sorted(configurations), ordered_count, multiset_count + + +def burnside_count(): + """Separate orbit count: no canonicalization and no multiset reduction. + + For each group element, count fixed ordered pair data and invariant subsets + of its allowed arcs. A subset is invariant exactly when it is a union of + cycles of the induced permutation of the six arcs. + """ + fixed = [] + for lp in PERMS: + unseen = set(ARCS) + cycles = [] + while unseen: + e = next(iter(unseen)) + cycle = set() + while e not in cycle: + cycle.add(e) + e = (lp[e[0]], lp[e[1]]) + unseen.difference_update(cycle) + cycles.append(sum(1 << ARC_INDEX[e] for e in cycle)) + ways = [1 << sum(c & z == c for c in cycles) for z in range(64)] + for tp in PERMS: + n = 0 + for pairs in product(TYPES, repeat=3): + if all((move_mask(pairs[lp[t]][0], tp), + move_mask(pairs[lp[t]][1], tp)) == pairs[t] + for t in range(3)): + n += ways[allowed_arcs(pairs)] + fixed.append(n) + if sum(fixed) % 36: + raise ValueError("nonintegral Burnside orbit count") + return sum(fixed) // 36, fixed + + +def submasks(mask): + return tuple(x for x in range(8) if x & ~mask == 0) + + +SUBMASKS = tuple(submasks(mask) for mask in range(8)) +OPTIONS = {(a, b): tuple((x, y) for x in SUBMASKS[a] for y in SUBMASKS[b] + if dot(x, y)) for a, b in TYPES} + + +def witness_valid(pairs, z, witness): + if witness is None: + return False + a, b, order = witness + if sorted(order) != [0, 1, 2] or len(a) != 3 or len(b) != 3: + return False + if any(a[t] & ~pairs[t][0] or b[t] & ~pairs[t][1] + or dot(a[t], b[t]) != 1 for t in range(3)): + return False + pos = {t: i for i, t in enumerate(order)} + return all(not (z & (1 << i)) or pos[t] > pos[s] or not dot(a[t], b[s]) + for i, (t, s) in enumerate(ARCS)) + + +def singleton_witness(pairs, z): + tied = [tuple(1 << j for j in range(3) if a & b & (1 << j)) + for a, b in pairs] + for labels in product(*tied): + # Conflict arcs have equal singleton labels. An order must put the + # target of each such arc before its source. + for order in PERMS: + pos = {t: i for i, t in enumerate(order)} + if all(not (z & (1 << i)) or labels[t] != labels[s] + or pos[t] > pos[s] for i, (t, s) in enumerate(ARCS)): + return labels, labels, order + return None + + +def exact_witness(pairs, z): + """Search in chronological order. Once an a-label is chosen, b(t) only + checks incoming constraints and never affects a later choice of b. + Taking its first valid value is therefore exact, not a greedy relaxation. + """ + a, b = [0] * 3, [0] * 3 + for order in PERMS: + def visit(k): + if k == 3: + return tuple(a), tuple(b), order + t = order[k] + previous = [s for s in order[:k] + if z & (1 << ARC_INDEX[(s, t)])] + for aa in SUBMASKS[pairs[t][0]]: + for bb in SUBMASKS[pairs[t][1]]: + if dot(aa, bb) and all(not dot(a[s], bb) for s in previous): + a[t], b[t] = aa, bb + result = visit(k + 1) + if result is not None: + return result + # Other b(t) values have no effect on future tests. + break + return None + result = visit(0) + if result is not None: + return result + return None + + +def brute_witness(pairs, z): + """Definition-level oracle: all three local (a,b) pairs and all orders. + This is deliberately separate from chronological search and singletons. + """ + for labels in product(*(OPTIONS[p] for p in pairs)): + a = tuple(p[0] for p in labels) + b = tuple(p[1] for p in labels) + for order in PERMS: + if all(not (z & (1 << ARC_INDEX[(order[i], order[j])])) + or (a[order[i]] & b[order[j]]).bit_count() % 2 == 0 + for i in range(3) for j in range(i + 1, 3)): + return a, b, order + return None diff --git a/research/fstar-joint-label-census/predecessor/box_search_kj.py b/research/fstar-joint-label-census/predecessor/box_search_kj.py new file mode 100644 index 0000000000..018c744279 --- /dev/null +++ b/research/fstar-joint-label-census/predecessor/box_search_kj.py @@ -0,0 +1,443 @@ +#!/usr/bin/env python3 +"""KB5j main search: Lemma BPP's without-loss question at tau >= 1. + +The certificate value of a decoder depends on the decoder ONLY through + - the zero-arc digraph Z (M_ts = 0 for t != s), + - the full label supports pi(t), sg(t) (monotone: cert grows with them), + - the sub-anchor masks a0(t), b0(t) (box depends only on these and Z). +Lemma SG (scope identity) forces |a0(t) intersect b0(s)| even on every zero +arc, and Lemma SB gives tau(t) = |a0(t) intersect b0(t)| >= 1 in scope. + +Jobs (smallest instance first; exact arithmetic; every value computed by the +vendored PR 2914 engine or by a function pinned to it by agreement tests): + +A. v = 2 exhaustive: every (a0,b0) pattern with tau >= 1 and every + scope-consistent zero pattern Z. Assert box = cert (= 2) - the machine + check of the written v = 2 repair lemma. Also assert PR 2936's tau = 0 + demonstration (cert = 2 > box = 1) still fails completeness. +B. v = 3 exhaustive (up to line and total relabeling): every scope-consistent + (a0,b0,Z). cert is over-approximated by cert_max(Z) = cert with full labels + pi = sg = 111 (monotone in label freedom), so `cert_max(Z) <= box` PROVES + box = cert for every decoder with that data; `cert_max(Z) > box` is a + counterexample candidate to be realized by an explicit P, Q. +C. Realizable sweep: random exact 3-total decoders (small integer entries, + varied 2-adic valuations) and GL_3(Z) transforms of the fixtures at + v = 3..4, tau >= 1 filter, exact cert vs exact box, plus every attaining + witness projected under Lemma BPP (strict drops and escape classes E1..E4 + recorded). + +Writes data/box-search-kj-receipt.json. Stdlib, deterministic. +Run: python3 -B box_search_kj.py +""" +import importlib.util +import itertools +import json +import os +import random +import sys +import time + +T0 = time.time() +HERE = os.path.dirname(os.path.abspath(__file__)) +sys.path.insert(0, os.path.join(HERE, "predecessor", "pr2963")) +import named_exact as ne # noqa: E402 + +fg = ne.fg +DATA = os.path.join(HERE, "predecessor", "pr2963", "predecessor", "pr2914", + "data") +spec = importlib.util.spec_from_file_location( + "box_attack", + os.path.join(HERE, "predecessor", "pr2963", "predecessor", "pr2936", + "box_attack.py")) +ba = importlib.util.module_from_spec(spec) +spec.loader.exec_module(ba) + + +def log(msg): + print("[%7.1fs] %s" % (time.time() - T0, msg), flush=True) + + +def dot1(x, y): + return bin(x & y).count("1") & 1 + + +def fake_model(v, Z): + """Model dict for the combinatorial space: zero arcs exactly Z (a set of + ordered pairs), every other entry 1, full label supports.""" + M = [[0 if ((t, s) in Z) else 1 for s in range(v)] for t in range(v)] + for t in range(v): + M[t][t] = 1 + arcs = [(t, s) for t in range(v) for s in range(v) + if t != s and (t, s) in Z] + return dict(v=v, P=None, Q=None, M=M, pi=[7] * v, sg=[7] * v, + D=[7] * v, arcs=arcs) + + +def fake_ad(a0, b0): + return dict(gamma=0, m=[0, 0, 0], n=[0, 0, 0], c=[0, 0, 0], + diag=[0] * len(a0), reach=[], cancel=[], + tau=[bin(a0[t] & b0[t]).count("1") for t in range(len(a0))], + a0=list(a0), b0=list(b0)) + + +def box_low3(a0, b0, Z): + """Cheap sufficient test for box = 3 at v = 3: tied-singleton colorings + (a = b = {c(t)}, c(t) tied) whose monochromatic zero-arc digraph is + acyclic, or the raw anchor pair. Returns True if box = 3 is witnessed.""" + v = 3 + tied = [a0[t] & b0[t] for t in range(v)] + choices = [[j for j in range(3) if tied[t] & (1 << j)] for t in range(v)] + for combo in itertools.product(*choices): + col = [1 << c for c in combo] + # conflict edges t->s iff (t,s) in Z and col equal: need acyclic + nodes = 3 + indeg = [0] * nodes + out = [[] for _ in range(nodes)] + for (t, s) in Z: + if col[t] == col[s]: + out[t].append(s) + indeg[s] += 1 + stack = [t for t in range(nodes) if indeg[t] == 0] + seen = 0 + while stack: + t = stack.pop() + seen += 1 + for s in out[t]: + indeg[s] -= 1 + if indeg[s] == 0: + stack.append(s) + if seen == nodes: + return True + mod = fake_model(v, Z) + ad = fake_ad(a0, b0) + if fg.ab_value(mod, list(a0), list(b0)) == 3: + return True + return False + + +def canon_total(a0, b0): + """Canonical representative of (a0, b0) under the 6 total relabelings.""" + best = None + for perm in itertools.permutations(range(3)): + def mv(x): + y = 0 + for j in range(3): + if x & (1 << j): + y |= 1 << perm[j] + return y + key = (mv(a0), mv(b0)) + if best is None or key < best: + best = key + return best + + +def canon_config(pairs, Z): + """Canonical form under line relabeling; pairs is the per-line tuple list + (already total-canonical). Z is a frozenset of ordered pairs.""" + best = None + for perm in itertools.permutations(range(3)): + npairs = tuple(pairs[perm[t]] for t in range(3)) + nZ = frozenset((perm[t], perm[s]) for (t, s) in Z) + key = (npairs, tuple(sorted(nZ))) + if best is None or key < best: + best = key + return best + + +def job_a(): + """v = 2 exhaustive over (a0,b0,Z), tau >= 1: box = cert = 2.""" + checked = 0 + gaps = [] + masks = range(8) + for a00 in masks: + for b00 in masks: + if not (a00 & b00): + continue + for a01 in masks: + for b01 in masks: + if not (a01 & b01): + continue + a0, b0 = [a00, a01], [b00, b01] + pairs = frozenset([(a00, b00), (a01, b01)]) + for z01 in (0, 1): + for z10 in (0, 1): + Z = set() + if z01: + Z.add((0, 1)) + if z10: + Z.add((1, 0)) + if any(dot1(a0[t], b0[s]) != 0 for (t, s) in Z): + continue # Lemma SG inconsistency + Z = frozenset(Z) + mod = fake_model(2, Z) + ad = fake_ad(a0, b0) + ce, cew = fg.cert_exact(mod, max_v=2) + bx, bxw = ba.box_exact_tolerant(mod, ad) + checked += 1 + if ce != bx or bx != 2: + gaps.append(dict(a0=a0, b0=b0, + Z=sorted(Z), cert=ce, + box=bx)) + else: + assert fg.replay_witness(mod, bxw) + assert fg.in_box(mod, ad, bxw)[0] + # PR 2936's tau = 0 demonstration must still break completeness. + P = [(1, 0, 1), (2, 1, 0)] + Q = [(1, 0, 0), (1, 0, 1)] + sub = fg.model(P, Q) + ad = fg.anchor_data(sub) + ce, _ = fg.cert_exact(sub, max_v=2) + bx, _ = ba.box_exact_tolerant(sub, ad) + assert (ce, bx) == (2, 1), (ce, bx) + log("job A: v=2 tau>=1 configs=%d gaps=%d; tau=0 demo cert=%d box=%d" + % (checked, len(gaps), ce, bx)) + print("PASS_KJ_V2 configs=%d box-equals-cert=%d tau0-demo=2/1" + % (checked, checked - len(gaps))) + return checked, gaps + + +def job_b(): + """v = 3 exhaustive over (a0,b0,Z) up to line/total relabeling.""" + mask_pairs = [(a, b) for a in range(8) for b in range(8) if a & b] + ckey = {} + for (a, b) in mask_pairs: + ckey[(a, b)] = canon_total(a, b) + line_types = sorted(set(ckey.values())) + certmax_cache = {} + configs = set() + raw = 0 + for tri in itertools.product(line_types, repeat=3): + pairs = tuple(tri) + a0 = [p[0] for p in pairs] + b0 = [p[1] for p in pairs] + free = [(t, s) for t in range(3) for s in range(3) + if t != s and dot1(a0[t], b0[s]) == 0] + for bits in range(1 << len(free)): + Z = frozenset(free[k] for k in range(len(free)) + if (bits >> k) & 1) + raw += 1 + configs.add(canon_config(pairs, Z)) + log("job B: raw configs %d -> %d canonical (line+total relabeling)" + % (raw, len(configs))) + gaps = [] + exact_runs = 0 + fast = 0 + done = 0 + for (pairs, ztup) in sorted(configs): + a0 = [p[0] for p in pairs] + b0 = [p[1] for p in pairs] + Z = frozenset(ztup) + if Z not in certmax_cache: + mod = fake_model(3, Z) + ce, _ = fg.cert_exact(mod, max_v=3) + certmax_cache[Z] = ce + cm = certmax_cache[Z] + done += 1 + if cm <= 2: + # cert_max itself is <= 2; box <= cert_max always, so a gap needs + # an exact box below cm: run exact box only if cheap witness < cm. + pass + if box_low3(a0, b0, Z): + fast += 1 + assert cm == 3 + continue + exact_runs += 1 + mod = fake_model(3, Z) + ad = fake_ad(a0, b0) + bx, bxw = ba.box_exact_tolerant(mod, ad) + if bx < cm: + gaps.append(dict(a0=a0, b0=b0, Z=sorted(Z), cert_max=cm, box=bx)) + log("job B CANDIDATE: a0=%s b0=%s Z=%s cert_max=%d box=%d" + % (a0, b0, sorted(Z), cm, bx)) + if done % 5000 == 0: + log("job B progress %d/%d exact=%d fast=%d gaps=%d" + % (done, len(configs), exact_runs, fast, len(gaps))) + log("job B done: configs=%d fast-3=%d exact=%d distinct-Z=%d gaps=%d" + % (len(configs), fast, exact_runs, len(certmax_cache), len(gaps))) + print("PASS_KJ_V3 configs=%d box-equals-cert=%d candidates=%d " + "certmax-cache=%d" % (len(configs), len(configs) - len(gaps), + len(gaps), len(certmax_cache))) + return len(configs), gaps + + +def rand_model(rng, v, val_bits=(0, 0, 1, 2)): + """Random small-integer P, Q with mixed 2-adic valuations.""" + def ent(): + if rng.random() < 0.32: + return 0 + mag = rng.choice(val_bits) + return rng.choice((-1, 1)) * (1 << mag) + P = [tuple(ent() for _ in range(3)) for _ in range(v)] + Q = [tuple(ent() for _ in range(3)) for _ in range(v)] + try: + return fg.model(P, Q) + except AssertionError: + return None + + +def probe_witnesses(mod, ad, v): + """Attaining-ish witnesses (hillclimb + random), projected under BPP. + Returns escape/drop records.""" + out = [] + wits = [] + for seed in (1234, 2025, 77, 4242): + _val, wit = fg.cert_hillclimb(mod, iters=80, seed=seed) + if wit is not None and fg.replay_witness(mod, wit): + wits.append(dict(wit, source="hillclimb:%d" % seed)) + rr = random.Random(9000 + 7 * v) + for _ in range(120): + a = [rr.randrange(8) & mod["pi"][t] for t in range(v)] + b = [rr.randrange(8) & mod["sg"][t] for t in range(v)] + wit = dict(a=a, b=b, order=list(range(v)), kept=list(range(v))) + if fg.replay_witness(mod, wit): + wits.append(dict(wit, source="random")) + for wit in wits: + inb, esc = fg.in_box(mod, ad, wit) + val = fg.ab_value(mod, wit["a"], wit["b"]) + pa = [wit["a"][t] & ad["a0"][t] for t in range(v)] + pb = [wit["b"][t] & ad["b0"][t] for t in range(v)] + pval = fg.ab_value(mod, pa, pb) + if inb and pval >= val: + continue + ok1 = all(bin(wit["a"][t] & wit["b"][t] & ad["a0"][t] + & ad["b0"][t]).count("1") % 2 == 1 for t in wit["kept"]) + ok2 = True + kept = set(wit["kept"]) + pos = {t: i for i, t in enumerate(wit["order"])} + for t in kept: + for s in kept: + if t != s and mod["M"][t][s] == 0 \ + and pos.get(t, 99) < pos.get(s, -1): + off = (wit["a"][t] & wit["b"][s]) \ + & ~(ad["a0"][t] & ad["b0"][s]) + if bin(off).count("1") % 2 != 0: + ok2 = False + out.append(dict(source=wit["source"], value=val, + projected_value=pval, + drop=pval < val, cond_i=ok1, cond_ii=ok2, + escape_lines=esc, + a=list(wit["a"]), b=list(wit["b"]), + kept=list(wit["kept"]), order=list(wit["order"]))) + return out + + +def job_c(): + """Realizable random decoders + fixture GL_3(Z) transforms, v = 3..4.""" + rng = random.Random(20261016) + records = [] + gaps = [] + drops = [] + esc_classes = {} + checked = 0 + attempts = 0 + while checked < 320 and attempts < 20000: + attempts += 1 + v = 3 if attempts % 25 else 4 + mod = rand_model(rng, v) + if mod is None: + continue + ad = fg.anchor_data(mod) + if not (fg.tie_parity(mod, ad) and fg.scope_identity(mod, ad)): + continue + if min(ad["tau"]) < 1: + continue + checked += 1 + ce, cew = fg.cert_exact(mod, max_v=v) + bx, bxw = ba.box_exact_tolerant(mod, ad) + assert fg.replay_witness(mod, cew) + assert bxw is None or fg.replay_witness(mod, bxw) + rec = dict(family="random", v=v, tau=list(ad["tau"]), + cert=ce, box=bx, gap=ce - bx, hard=ce < v, + P=[list(p) for p in mod["P"]], + Q=[list(q) for q in mod["Q"]]) + records.append(rec) + if ce > bx: + gaps.append(rec) + log("job C CANDIDATE: v=%d cert=%d box=%d" % (v, ce, bx)) + if v == 3: + for w in probe_witnesses(mod, ad, v): + if w["drop"]: + drops.append(dict(rec, witness=w)) + log("job C DROP at tau>=1: v=%d val=%d proj=%d i=%s ii=%s" + % (v, w["value"], w["projected_value"], + w["cond_i"], w["cond_ii"])) + key = ("E1" if w["cond_i"] and w["cond_ii"] else + "E4" if not w["cond_i"] and not w["cond_ii"] else + "E2" if not w["cond_i"] else "E3") + esc_classes[key] = esc_classes.get(key, 0) + 1 + if checked % 150 == 0: + log("job C progress checked=%d gaps=%d drops=%d" + % (checked, len(gaps), len(drops))) + # fixture transforms at v = 3 (PR 2963's sweep started at v = 4) + spec2 = importlib.util.spec_from_file_location( + "box_search", + os.path.join(HERE, "predecessor", "pr2963", "box_search.py")) + bs = importlib.util.module_from_spec(spec2) + spec2.loader.exec_module(bs) + made = 0 + att = 0 + while made < 40 and att < 800: + att += 1 + fixture = ("tied_min.json", "cex_min_1.json")[att % 2] + mod0 = fg.model(*fg.load_decoder(os.path.join(DATA, fixture))) + U, Uinv = bs.rand_gl3z(rng, steps=2 + att % 5) + mod1 = bs.transform(mod0, U, Uinv) + S = sorted(rng.sample(range(mod1["v"]), 3)) + sub = fg.restrict(mod1, S) + ad = fg.anchor_data(sub) + if not (fg.tie_parity(sub, ad) and fg.scope_identity(sub, ad)): + continue + if min(ad["tau"]) < 1: + continue + made += 1 + ce, cew = fg.cert_exact(sub, max_v=3) + bx, bxw = ba.box_exact_tolerant(sub, ad) + assert fg.replay_witness(sub, cew) + rec = dict(family="fixture-transform", v=3, fixture=fixture, S=S, + tau=list(ad["tau"]), cert=ce, box=bx, gap=ce - bx, + hard=ce < 3, P=[list(p) for p in sub["P"]], + Q=[list(q) for q in sub["Q"]]) + records.append(rec) + if ce > bx: + gaps.append(rec) + log("job C (transform) CANDIDATE: cert=%d box=%d" % (ce, bx)) + for w in probe_witnesses(sub, ad, 3): + if w["drop"]: + drops.append(dict(rec, witness=w)) + log("job C (transform) DROP at tau>=1: val=%d proj=%d" + % (w["value"], w["projected_value"])) + key = ("E1" if w["cond_i"] and w["cond_ii"] else + "E4" if not w["cond_i"] and not w["cond_ii"] else + "E2" if not w["cond_i"] else "E3") + esc_classes[key] = esc_classes.get(key, 0) + 1 + log("job C done: instances=%d (random %d + transforms %d) gaps=%d " + "drops=%d escapes=%s" % (len(records), checked, made, len(gaps), + len(drops), esc_classes)) + print("PASS_KJ_REALIZABLE instances=%d box-violations=%d drops=%d " + "escapes=%s" % (len(records), len(gaps), len(drops), esc_classes)) + return records, gaps, drops, esc_classes + + +def main(): + sys.stdout.reconfigure(encoding="utf-8") + checked, gaps_a = job_a() + nconf, gaps_b = job_b() + records, gaps_c, drops, esc = job_c() + receipt = dict(generator="box_search_kj.py seed 20261016", + job_a=dict(configs=checked, gaps=len(gaps_a), + gap_records=gaps_a), + job_b=dict(configs=nconf, candidates=gaps_b), + job_c=dict(instances=records, gaps=gaps_c, drops=drops, + escape_classes=esc)) + with open(os.path.join(HERE, "data", "box-search-kj-receipt.json"), "w", + encoding="utf-8", newline="\n") as fh: + json.dump(receipt, fh, indent=1, sort_keys=True) + fh.write("\n") + total_gap = len(gaps_a) + len(gaps_b) + len(gaps_c) + print("PASS_KJ_BOX_SEARCH v2-configs=%d v3-configs=%d realizable=%d " + "candidates=%d drops-tau1=%d" + % (checked, nconf, len(records), total_gap, len(drops))) + + +if __name__ == "__main__": + main() diff --git a/research/fstar-joint-label-census/predecessor/realize-kj-receipt.json b/research/fstar-joint-label-census/predecessor/realize-kj-receipt.json new file mode 100644 index 0000000000..829c40d492 --- /dev/null +++ b/research/fstar-joint-label-census/predecessor/realize-kj-receipt.json @@ -0,0 +1,1459 @@ +{ + "counterexamples": [ + { + "P": [ + [ + -1, + -3, + 0 + ], + [ + 1, + -1, + -2 + ], + [ + 3, + 3, + 3 + ] + ], + "Q": [ + [ + 1, + -3, + 2 + ], + [ + 3, + -1, + -2 + ], + [ + 3, + -1, + 2 + ] + ], + "alphabet": "with-zeros", + "attempts": 66, + "box": 2, + "candidate": { + "Z": [ + [ + 0, + 1 + ], + [ + 0, + 2 + ], + [ + 1, + 0 + ], + [ + 1, + 2 + ], + [ + 2, + 0 + ], + [ + 2, + 1 + ] + ], + "a0": [ + 3, + 3, + 7 + ], + "b0": [ + 3, + 3, + 3 + ], + "box": 2, + "cert_max": 3 + }, + "cert": 3, + "cert_witness": { + "a": [ + 1, + 2, + 4 + ], + "b": [ + 1, + 2, + 4 + ], + "kept": [ + 2, + 1, + 0 + ], + "order": [ + 2, + 1, + 0 + ] + }, + "status": "realized" + }, + { + "P": [ + [ + -1, + 3, + 0 + ], + [ + 3, + -3, + 3 + ], + [ + -1, + 1, + 1 + ] + ], + "Q": [ + [ + 1, + 1, + 0 + ], + [ + 3, + 1, + 2 + ], + [ + 3, + 1, + -2 + ] + ], + "alphabet": "with-zeros", + "attempts": 9, + "box": 2, + "candidate": { + "Z": [ + [ + 0, + 1 + ], + [ + 0, + 2 + ], + [ + 1, + 0 + ], + [ + 1, + 2 + ], + [ + 2, + 0 + ], + [ + 2, + 1 + ] + ], + "a0": [ + 3, + 7, + 7 + ], + "b0": [ + 3, + 3, + 3 + ], + "box": 2, + "cert_max": 3 + }, + "cert": 3, + "cert_witness": { + "a": [ + 1, + 2, + 4 + ], + "b": [ + 1, + 2, + 4 + ], + "kept": [ + 2, + 1, + 0 + ], + "order": [ + 2, + 1, + 0 + ] + }, + "status": "realized" + }, + { + "P": [ + [ + -3, + -1, + -3 + ], + [ + 3, + -3, + -3 + ], + [ + 1, + 3, + -3 + ] + ], + "Q": [ + [ + 3, + 1, + 2 + ], + [ + 3, + -3, + -2 + ], + [ + 1, + 3, + -2 + ] + ], + "alphabet": "nonzero", + "attempts": 279, + "box": 2, + "candidate": { + "Z": [ + [ + 0, + 1 + ], + [ + 0, + 2 + ], + [ + 1, + 0 + ], + [ + 1, + 2 + ], + [ + 2, + 0 + ], + [ + 2, + 1 + ] + ], + "a0": [ + 7, + 7, + 7 + ], + "b0": [ + 3, + 3, + 3 + ], + "box": 2, + "cert_max": 3 + }, + "cert": 3, + "cert_witness": { + "a": [ + 1, + 2, + 4 + ], + "b": [ + 1, + 2, + 4 + ], + "kept": [ + 2, + 1, + 0 + ], + "order": [ + 2, + 1, + 0 + ] + }, + "status": "realized" + } + ], + "generator": "realize_kj.py seed 20261017", + "records": [ + { + "alphabet": "big", + "candidate": { + "Z": [ + [ + 0, + 1 + ], + [ + 1, + 0 + ] + ], + "a0": [ + 1, + 3, + 7 + ], + "b0": [ + 1, + 5, + 3 + ], + "box": 2, + "cert_max": 3 + }, + "p_tries": 6000, + "status": "not-found-in-cap" + }, + { + "alphabet": "big", + "candidate": { + "Z": [ + [ + 0, + 1 + ], + [ + 1, + 0 + ] + ], + "a0": [ + 1, + 3, + 7 + ], + "b0": [ + 1, + 5, + 7 + ], + "box": 2, + "cert_max": 3 + }, + "p_tries": 6000, + "status": "not-found-in-cap" + }, + { + "alphabet": "big", + "candidate": { + "Z": [ + [ + 0, + 1 + ], + [ + 1, + 0 + ] + ], + "a0": [ + 3, + 3, + 7 + ], + "b0": [ + 1, + 5, + 3 + ], + "box": 2, + "cert_max": 3 + }, + "p_tries": 6000, + "status": "not-found-in-cap" + }, + { + "alphabet": "big", + "candidate": { + "Z": [ + [ + 0, + 1 + ], + [ + 1, + 0 + ], + [ + 2, + 1 + ] + ], + "a0": [ + 3, + 3, + 7 + ], + "b0": [ + 1, + 5, + 3 + ], + "box": 2, + "cert_max": 3 + }, + "p_tries": 6000, + "status": "not-found-in-cap" + }, + { + "alphabet": "big", + "candidate": { + "Z": [ + [ + 0, + 1 + ], + [ + 1, + 0 + ] + ], + "a0": [ + 3, + 3, + 7 + ], + "b0": [ + 1, + 5, + 7 + ], + "box": 2, + "cert_max": 3 + }, + "p_tries": 6000, + "status": "not-found-in-cap" + }, + { + "alphabet": "big", + "candidate": { + "Z": [ + [ + 0, + 1 + ], + [ + 1, + 0 + ], + [ + 2, + 1 + ] + ], + "a0": [ + 3, + 3, + 7 + ], + "b0": [ + 1, + 5, + 7 + ], + "box": 2, + "cert_max": 3 + }, + "p_tries": 6000, + "status": "not-found-in-cap" + }, + { + "alphabet": "big", + "candidate": { + "Z": [ + [ + 0, + 1 + ], + [ + 0, + 2 + ], + [ + 1, + 0 + ], + [ + 1, + 2 + ], + [ + 2, + 0 + ], + [ + 2, + 1 + ] + ], + "a0": [ + 3, + 3, + 3 + ], + "b0": [ + 3, + 3, + 3 + ], + "box": 2, + "cert_max": 3 + }, + "p_tries": 6000, + "status": "not-found-in-cap" + }, + { + "candidate": { + "Z": [ + [ + 0, + 1 + ], + [ + 0, + 2 + ], + [ + 1, + 0 + ], + [ + 1, + 2 + ], + [ + 2, + 0 + ], + [ + 2, + 1 + ] + ], + "a0": [ + 3, + 3, + 3 + ], + "b0": [ + 3, + 3, + 7 + ], + "box": 2, + "cert_max": 3 + }, + "reason": "bit 2 enters b0 but no a0 line attains m_j", + "status": "unrealizable-column" + }, + { + "P": [ + [ + -1, + -3, + 0 + ], + [ + 1, + -1, + -2 + ], + [ + 3, + 3, + 3 + ] + ], + "Q": [ + [ + 1, + -3, + 2 + ], + [ + 3, + -1, + -2 + ], + [ + 3, + -1, + 2 + ] + ], + "alphabet": "with-zeros", + "attempts": 66, + "box": 2, + "candidate": { + "Z": [ + [ + 0, + 1 + ], + [ + 0, + 2 + ], + [ + 1, + 0 + ], + [ + 1, + 2 + ], + [ + 2, + 0 + ], + [ + 2, + 1 + ] + ], + "a0": [ + 3, + 3, + 7 + ], + "b0": [ + 3, + 3, + 3 + ], + "box": 2, + "cert_max": 3 + }, + "cert": 3, + "cert_witness": { + "a": [ + 1, + 2, + 4 + ], + "b": [ + 1, + 2, + 4 + ], + "kept": [ + 2, + 1, + 0 + ], + "order": [ + 2, + 1, + 0 + ] + }, + "status": "realized" + }, + { + "candidate": { + "Z": [ + [ + 0, + 1 + ], + [ + 0, + 2 + ], + [ + 1, + 0 + ], + [ + 1, + 2 + ], + [ + 2, + 0 + ], + [ + 2, + 1 + ] + ], + "a0": [ + 3, + 3, + 3 + ], + "b0": [ + 3, + 7, + 7 + ], + "box": 2, + "cert_max": 3 + }, + "reason": "bit 2 enters b0 but no a0 line attains m_j", + "status": "unrealizable-column" + }, + { + "P": [ + [ + -1, + 3, + 0 + ], + [ + 3, + -3, + 3 + ], + [ + -1, + 1, + 1 + ] + ], + "Q": [ + [ + 1, + 1, + 0 + ], + [ + 3, + 1, + 2 + ], + [ + 3, + 1, + -2 + ] + ], + "alphabet": "with-zeros", + "attempts": 9, + "box": 2, + "candidate": { + "Z": [ + [ + 0, + 1 + ], + [ + 0, + 2 + ], + [ + 1, + 0 + ], + [ + 1, + 2 + ], + [ + 2, + 0 + ], + [ + 2, + 1 + ] + ], + "a0": [ + 3, + 7, + 7 + ], + "b0": [ + 3, + 3, + 3 + ], + "box": 2, + "cert_max": 3 + }, + "cert": 3, + "cert_witness": { + "a": [ + 1, + 2, + 4 + ], + "b": [ + 1, + 2, + 4 + ], + "kept": [ + 2, + 1, + 0 + ], + "order": [ + 2, + 1, + 0 + ] + }, + "status": "realized" + }, + { + "alphabet": "big", + "candidate": { + "Z": [ + [ + 0, + 1 + ], + [ + 0, + 2 + ], + [ + 1, + 0 + ] + ], + "a0": [ + 3, + 3, + 7 + ], + "b0": [ + 5, + 5, + 3 + ], + "box": 2, + "cert_max": 3 + }, + "p_tries": 6000, + "status": "not-found-in-cap" + }, + { + "alphabet": "big", + "candidate": { + "Z": [ + [ + 0, + 1 + ], + [ + 0, + 2 + ], + [ + 1, + 0 + ], + [ + 2, + 0 + ] + ], + "a0": [ + 3, + 3, + 7 + ], + "b0": [ + 5, + 5, + 3 + ], + "box": 2, + "cert_max": 3 + }, + "p_tries": 6000, + "status": "not-found-in-cap" + }, + { + "alphabet": "big", + "candidate": { + "Z": [ + [ + 0, + 1 + ], + [ + 1, + 0 + ] + ], + "a0": [ + 3, + 3, + 7 + ], + "b0": [ + 5, + 5, + 3 + ], + "box": 2, + "cert_max": 3 + }, + "p_tries": 6000, + "status": "not-found-in-cap" + }, + { + "alphabet": "big", + "candidate": { + "Z": [ + [ + 0, + 1 + ], + [ + 1, + 0 + ], + [ + 1, + 2 + ] + ], + "a0": [ + 3, + 3, + 7 + ], + "b0": [ + 5, + 5, + 3 + ], + "box": 2, + "cert_max": 3 + }, + "p_tries": 6000, + "status": "not-found-in-cap" + }, + { + "alphabet": "big", + "candidate": { + "Z": [ + [ + 0, + 1 + ], + [ + 1, + 0 + ], + [ + 1, + 2 + ], + [ + 2, + 1 + ] + ], + "a0": [ + 3, + 3, + 7 + ], + "b0": [ + 5, + 5, + 3 + ], + "box": 2, + "cert_max": 3 + }, + "p_tries": 6000, + "status": "not-found-in-cap" + }, + { + "alphabet": "big", + "candidate": { + "Z": [ + [ + 0, + 1 + ], + [ + 1, + 0 + ], + [ + 2, + 0 + ] + ], + "a0": [ + 3, + 3, + 7 + ], + "b0": [ + 5, + 5, + 3 + ], + "box": 2, + "cert_max": 3 + }, + "p_tries": 6000, + "status": "not-found-in-cap" + }, + { + "alphabet": "big", + "candidate": { + "Z": [ + [ + 0, + 1 + ], + [ + 1, + 0 + ], + [ + 2, + 1 + ] + ], + "a0": [ + 3, + 3, + 7 + ], + "b0": [ + 5, + 5, + 3 + ], + "box": 2, + "cert_max": 3 + }, + "p_tries": 6000, + "status": "not-found-in-cap" + }, + { + "alphabet": "big", + "candidate": { + "Z": [ + [ + 0, + 1 + ], + [ + 0, + 2 + ], + [ + 1, + 0 + ] + ], + "a0": [ + 3, + 3, + 7 + ], + "b0": [ + 5, + 5, + 7 + ], + "box": 2, + "cert_max": 3 + }, + "p_tries": 6000, + "status": "not-found-in-cap" + }, + { + "alphabet": "big", + "candidate": { + "Z": [ + [ + 0, + 1 + ], + [ + 0, + 2 + ], + [ + 1, + 0 + ], + [ + 2, + 0 + ] + ], + "a0": [ + 3, + 3, + 7 + ], + "b0": [ + 5, + 5, + 7 + ], + "box": 2, + "cert_max": 3 + }, + "p_tries": 6000, + "status": "not-found-in-cap" + }, + { + "alphabet": "big", + "candidate": { + "Z": [ + [ + 0, + 1 + ], + [ + 1, + 0 + ] + ], + "a0": [ + 3, + 3, + 7 + ], + "b0": [ + 5, + 5, + 7 + ], + "box": 2, + "cert_max": 3 + }, + "p_tries": 6000, + "status": "not-found-in-cap" + }, + { + "alphabet": "big", + "candidate": { + "Z": [ + [ + 0, + 1 + ], + [ + 1, + 0 + ], + [ + 1, + 2 + ] + ], + "a0": [ + 3, + 3, + 7 + ], + "b0": [ + 5, + 5, + 7 + ], + "box": 2, + "cert_max": 3 + }, + "p_tries": 6000, + "status": "not-found-in-cap" + }, + { + "alphabet": "big", + "candidate": { + "Z": [ + [ + 0, + 1 + ], + [ + 1, + 0 + ], + [ + 1, + 2 + ], + [ + 2, + 1 + ] + ], + "a0": [ + 3, + 3, + 7 + ], + "b0": [ + 5, + 5, + 7 + ], + "box": 2, + "cert_max": 3 + }, + "p_tries": 6000, + "status": "not-found-in-cap" + }, + { + "alphabet": "big", + "candidate": { + "Z": [ + [ + 0, + 1 + ], + [ + 1, + 0 + ], + [ + 2, + 0 + ] + ], + "a0": [ + 3, + 3, + 7 + ], + "b0": [ + 5, + 5, + 7 + ], + "box": 2, + "cert_max": 3 + }, + "p_tries": 6000, + "status": "not-found-in-cap" + }, + { + "alphabet": "big", + "candidate": { + "Z": [ + [ + 0, + 1 + ], + [ + 1, + 0 + ], + [ + 2, + 1 + ] + ], + "a0": [ + 3, + 3, + 7 + ], + "b0": [ + 5, + 5, + 7 + ], + "box": 2, + "cert_max": 3 + }, + "p_tries": 6000, + "status": "not-found-in-cap" + }, + { + "candidate": { + "Z": [ + [ + 0, + 1 + ], + [ + 0, + 2 + ], + [ + 1, + 0 + ], + [ + 1, + 2 + ], + [ + 2, + 0 + ], + [ + 2, + 1 + ] + ], + "a0": [ + 3, + 3, + 3 + ], + "b0": [ + 7, + 7, + 7 + ], + "box": 2, + "cert_max": 3 + }, + "reason": "bit 2 enters b0 but no a0 line attains m_j", + "status": "unrealizable-column" + }, + { + "P": [ + [ + -3, + -1, + -3 + ], + [ + 3, + -3, + -3 + ], + [ + 1, + 3, + -3 + ] + ], + "Q": [ + [ + 3, + 1, + 2 + ], + [ + 3, + -3, + -2 + ], + [ + 1, + 3, + -2 + ] + ], + "alphabet": "nonzero", + "attempts": 279, + "box": 2, + "candidate": { + "Z": [ + [ + 0, + 1 + ], + [ + 0, + 2 + ], + [ + 1, + 0 + ], + [ + 1, + 2 + ], + [ + 2, + 0 + ], + [ + 2, + 1 + ] + ], + "a0": [ + 7, + 7, + 7 + ], + "b0": [ + 3, + 3, + 3 + ], + "box": 2, + "cert_max": 3 + }, + "cert": 3, + "cert_witness": { + "a": [ + 1, + 2, + 4 + ], + "b": [ + 1, + 2, + 4 + ], + "kept": [ + 2, + 1, + 0 + ], + "order": [ + 2, + 1, + 0 + ] + }, + "status": "realized" + } + ], + "status_counts": { + "not-found-in-cap": 21, + "realized": 3, + "unrealizable-column": 3 + } +} diff --git a/research/fstar-joint-label-census/verify.py b/research/fstar-joint-label-census/verify.py new file mode 100644 index 0000000000..bd5020b54d --- /dev/null +++ b/research/fstar-joint-label-census/verify.py @@ -0,0 +1,257 @@ +#!/usr/bin/env python3 +"""Replay the finite census, independent oracles, source audit and controls. + +Default is read-only. --write explicitly publishes a deterministic receipt. +No predecessor search or solver is run; only its two canonicalizers are loaded. +""" +import argparse +import ast +import hashlib +import itertools +import json +from pathlib import Path +import random + +import census as c + +HERE = Path(__file__).resolve().parent + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def record(pairs, z): + return {"pairs": pairs, "Z": [e for i, e in enumerate(c.ARCS) if z & (1 << i)]} + + +def encode(pairs, edges): + return tuple(map(tuple, pairs)), sum(1 << c.ARC_INDEX[tuple(e)] for e in edges) + + +def source_check(): + sources = json.loads((HERE / "SOURCES.json").read_text()) + for source in sources["archived_sources"]: + raw = (HERE / source["vendored_path"]).read_bytes() + require(hashlib.sha256(raw).hexdigest() == source["sha256"], + "predecessor bytes changed: " + source["vendored_path"]) + return len(sources["archived_sources"]) + + +def legacy_functions(): + path = HERE / "predecessor/box_search_kj.py" + tree = ast.parse(path.read_text()) + # Avoid importing the historical script and its transitive predecessor tree. + names = {"canon_total", "canon_config"} + definitions = [node for node in tree.body + if isinstance(node, ast.FunctionDef) and node.name in names] + require({node.name for node in definitions} == names, "legacy definitions missing") + env = {"itertools": itertools} + exec(compile(ast.Module(body=definitions, type_ignores=[]), str(path), "exec"), env) + return env["canon_total"], env["canon_config"] + + +def controls(configurations, old_total, old_config): + # Identical per-line canonical types can have different joint parities. + equal = ((3, 3), (3, 3), (3, 3)) + rotated = ((3, 3), (3, 3), (5, 5)) + require(tuple(old_total(*p) for p in equal) == + tuple(old_total(*p) for p in rotated), "per-line mutant not reproduced") + require(c.allowed_arcs(equal) != c.allowed_arcs(rotated), "lost joint parity") + require(c.direct_canonical(equal, 0) != c.direct_canonical(rotated, 0), + "global quotient merged distinct joint data") + + # A three-cycle exposes the pushforward/pullback mismatch in canon_config. + pairs = ((1, 3), (3, 1), (1, 1)) + z = 1 << c.ARC_INDEX[(1, 0)] + pp, edges = old_config(pairs, frozenset({(1, 0)})) + legacy = encode(pp, edges) + require(not (z & ~c.allowed_arcs(pairs)), "input must satisfy scope parity") + require(legacy == (((1, 1), (1, 3), (3, 1)), 2), "legacy control drift") + require(legacy[1] & ~c.allowed_arcs(legacy[0]), "invalid legacy output accepted") + correct = c.direct_canonical(pairs, z) + require(correct == (((1, 1), (1, 3), (3, 1)), 32), "correct arc pullback") + + # Definition-level action versus optimized canonicalization, including all + # 36 transforms of deterministic samples and all 64 arc-mask transforms. + rng = random.Random(20261017) + for lp_index, lp in enumerate(c.PERMS): + for mask in range(64): + require(c.relabel(equal, mask, lp, (0, 1, 2))[1] == + c.LINE_MAPS[lp_index][mask], "arc action table mismatch") + samples = rng.sample(configurations, 80) + for key in samples: + require(c.direct_canonical(*key) == key, "not a direct canonical representative") + for lp in c.PERMS: + for tp in c.PERMS: + pp, zz = c.relabel(*key, lp, tp) + require(c.canonical_from_plan(c.pair_plan(pp), zz) == key, + "canonicalizer not invariant under a legal group action") + require(not (zz & ~c.allowed_arcs(pp)), "legal action broke scope") + + diagonal = ((1, 1), (2, 2), (4, 4)) + witness = c.brute_witness(diagonal, 63) + require(c.witness_valid(diagonal, 63, witness), "diagonal positive control") + a, b, order = witness + require(not c.witness_valid(diagonal, 63, ((0,) + a[1:], b, order)), + "broken diagonal witness accepted") + full = ((7, 7),) * 3 + bad_order = ((1, 1, 1), (1, 1, 1), (0, 1, 2)) + require(not c.witness_valid(full, 1, bad_order), "odd forward zero arc accepted") + require(c.witness_valid(full, 1, (bad_order[0], bad_order[1], (1, 0, 2))), + "reverse order control must pass") + return {"per_line_loss": {"first": equal, "second": rotated, + "allowed_Z_masks": [c.allowed_arcs(equal), + c.allowed_arcs(rotated)]}, + "line_action_failure": {"input": record(pairs, z), + "legacy": record(*legacy), + "correct": record(*correct)}, + "action_samples": len(samples), "witness_rejections": 2} + + +def legacy_audit(old_total, old_config, complete): + line_types = sorted({old_total(*p) for p in c.TYPES}) + old_states, represented = set(), set() + for pairs in itertools.product(line_types, repeat=3): + plan = c.pair_plan(pairs) + for z in c.subsets(c.allowed_arcs(pairs)): + edges = frozenset(e for i, e in enumerate(c.ARCS) if z & (1 << i)) + pp, zz = old_config(pairs, edges) + old_states.add(encode(pp, zz)) + represented.add(c.canonical_from_plan(plan, z)) + require(len(old_states) == 3023, "source census fixture not reproduced") + invalid = {key for key in old_states if key[1] & ~c.allowed_arcs(key[0])} + legacy_gaps = {key for key in old_states if c.brute_witness(*key) is None} + require(len(legacy_gaps) == 27, "source candidate fixture not reproduced") + receipt = json.loads((HERE / "predecessor/realize-kj-receipt.json").read_text()) + source_records = receipt["records"] + require({encode(zip(r["candidate"]["a0"], r["candidate"]["b0"]), + r["candidate"]["Z"]) for r in source_records} == legacy_gaps, + "receipt candidate set differs from reproduced legacy gap set") + rejected = [] + for index, item in enumerate(source_records): + p = tuple(zip(item["candidate"]["a0"], item["candidate"]["b0"])) + bad = [tuple(e) for e in item["candidate"]["Z"] + if c.dot(p[e[0]][0], p[e[1]][1])] + if bad: + require(item["status"] == "not-found-in-cap", "unexpected invalid record") + rejected.append({"source_record_index": index, + **record(p, encode(p, item["candidate"]["Z"])[1]), + "odd_anchor_zero_arcs": bad}) + require(len(rejected) == 20, "expected twenty scope-inconsistent candidates") + return {"line_types": len(line_types), "states": len(old_states), + "scope_inconsistent_states": len(invalid), + "represented_valid_orbits": len(represented), + "omitted_valid_orbits": len(set(complete) - represented), + "legacy_candidates": len(legacy_gaps), + "scope_inconsistent_candidates": rejected}, represented + + +def v2(value): + require(value != 0, "valuation of zero") + return (abs(value) & -abs(value)).bit_length() - 1 + + +def realization_check(gaps): + """Check the three credited integer witnesses from their defining P,Q. + Rank/anchor-attainment rules dispose of the four other combinatorial shapes. + """ + source = json.loads((HERE / "predecessor/realize-kj-receipt.json").read_text()) + realized = {} + for item in source["counterexamples"]: + P, Q = item["P"], item["Q"] + M = [[sum(P[t][j] * Q[s][j] for j in range(3)) for s in range(3)] + for t in range(3)] + require(all(M[t][t] for t in range(3)), "zero decoder diagonal") + require(all(M[t][s] == 0 for t, s in c.ARCS), "decoder not diagonal") + m = [min(v2(P[t][j]) for t in range(3) if P[t][j]) for j in range(3)] + n = [min(v2(Q[t][j]) for t in range(3) if Q[t][j]) for j in range(3)] + gamma = min(m[j] + n[j] for j in range(3)) + aa = [sum(1 << j for j in range(3) if P[t][j] and v2(P[t][j]) == m[j]) + for t in range(3)] + bb = [sum(1 << j for j in range(3) if Q[t][j] and + v2(Q[t][j]) == gamma - m[j]) for t in range(3)] + pairs = tuple(zip(aa, bb)) + key = c.direct_canonical(pairs, 63) + require(key in gaps and key not in realized, "duplicate/unknown realized shape") + pi = tuple(sum(1 << j for j in range(3) if P[t][j]) for t in range(3)) + sg = tuple(sum(1 << j for j in range(3) if Q[t][j]) for t in range(3)) + support_pairs = tuple(zip(pi, sg)) + witness = c.brute_witness(support_pairs, 63) + require(c.witness_valid(support_pairs, 63, witness), "cert=3 witness invalid") + require(c.brute_witness(pairs, 63) is None, "box gap lost") + realized[key] = {"P": P, "Q": Q, "M": M, "gamma": gamma, + "cert_witness": witness} + shapes = [] + for pairs, z in gaps: + require(z == 63 and all(a & 3 == 3 and b & 3 == 3 for a, b in pairs), + "gap classification shape changed") + # (a,b)=(1,1),(2,2) on lines 0,1 witnesses box>=2 in either order. + union_a = pairs[0][0] | pairs[1][0] | pairs[2][0] + if union_a != 7: + status = "unrealizable: diagonal rank three requires three nondegenerate totals; each P-column minimum must be attained" + else: + require((pairs, z) in realized, "unresolved rank-three shape") + status = "realized: predecessor integer P,Q replayed; box=2, cert=3" + shapes.append({**record(pairs, z), "box": 2, "status": status, + "witness": realized.get((pairs, z))}) + require(len(realized) == 3 and len(shapes) == 7, "realization classification drift") + return shapes + + +def replay(): + pins = source_check() + configurations, raw, multisets = c.enumerate_orbits() + burnside, fixed = c.burnside_count() + require(burnside == len(configurations), "independent Burnside count mismatch") + require(fixed[0] == raw, "ordered domain count mismatch") + old_total, old_config = legacy_functions() + control_receipt = controls(configurations, old_total, old_config) + gaps, fallback = [], 0 + for pairs, z in configurations: + require(not (z & ~c.allowed_arcs(pairs)), "inadmissible census state") + fast = c.singleton_witness(pairs, z) + if fast is None: + fallback += 1 + fast = c.exact_witness(pairs, z) + brute = c.brute_witness(pairs, z) + require((fast is None) == (brute is None), "independent box decision mismatch") + if fast is None: + gaps.append((pairs, z)) + else: + require(c.witness_valid(pairs, z, fast) and c.witness_valid(pairs, z, brute), + "positive census witness rejected") + legacy, represented = legacy_audit(old_total, old_config, configurations) + require(set(gaps) <= represented, "legacy reduced domain missed a gap shape") + return {"schema_version": 1, "domain": {"totals": 3, "lines": 3, "tau_min": 1}, + "raw_ordered_states": raw, "raw_line_type_multisets": multisets, + "global_orbits": len(configurations), "burnside_fixed_counts": fixed, + "box3_orbits": len(configurations) - len(gaps), "box2_orbits": len(gaps), + "chronological_fallbacks": fallback, "brute_oracle_checks": len(configurations), + "legacy": legacy, "gap_shapes": realization_check(gaps), + "controls": control_receipt, "source_pins": pins} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write", action="store_true", help="write RESULTS.json explicitly") + args = parser.parse_args() + result = replay() + data = json.dumps(result, indent=2, sort_keys=True) + "\n" + path = HERE / "RESULTS.json" + if args.write: + path.write_text(data, encoding="utf-8", newline="\n") + else: + require(path.read_text(encoding="utf-8") == data, "receipt differs; inspect before --write") + digest = hashlib.sha256(data.encode()).hexdigest() + print("PASS_JOINT_CENSUS ordered=%d orbits=%d box3=%d box2=%d brute=%d" % + (result["raw_ordered_states"], result["global_orbits"], result["box3_orbits"], + result["box2_orbits"], result["brute_oracle_checks"])) + print("PASS_LEGACY_AUDIT states=3023 invalid=1370 candidates=27 invalid_candidates=20") + print("PASS_REALIZATION_CLASSIFICATION shapes=7 realized=3 impossible=4") + print("PASS_JOINT_CONTROLS pins=%d digest=%s" % (result["source_pins"], digest)) + + +if __name__ == "__main__": + main()