diff --git a/research/fstar-proof-lemmas-seed3096ed3f/CERTIFICATE.json b/research/fstar-proof-lemmas-seed3096ed3f/CERTIFICATE.json new file mode 100644 index 0000000000..49b88eb8ae --- /dev/null +++ b/research/fstar-proof-lemmas-seed3096ed3f/CERTIFICATE.json @@ -0,0 +1,430 @@ +{ + "controls": { + "brute_agree": 3, + "corrupt_rejects": 2, + "diagonal_cert": 3 + }, + "digest": "134665ac6a0800e45be234e19f95e52409df7a560725cca67c93ee0aaa099aaf", + "engine": "a-label enumeration + exact (b, order, S) completion by subset DP", + "exact_cert_tiny": [ + { + "cert": 5, + "v": 5 + }, + { + "cert": 5, + "v": 5 + }, + { + "cert": 6, + "v": 6 + } + ], + "failures": [], + "falsifiers": [], + "min_witness_ratio": 0.8666666666666667, + "named": { + "cex_min_1.json": { + "chain_upper": 30, + "replay_ok": true, + "v": 19, + "witness": 18 + }, + "tied_min.json": { + "chain_upper": 20, + "replay_ok": true, + "v": 12, + "witness": 11 + } + }, + "schema_version": 1, + "search": [ + { + "chain_upper": 11, + "family": "entries3", + "free_pairs": 3, + "i": 0, + "threshold": 2, + "v": 4, + "witness": 4 + }, + { + "chain_upper": 7, + "family": "entries3", + "free_pairs": 1, + "i": 1, + "threshold": 2, + "v": 4, + "witness": 4 + }, + { + "chain_upper": 11, + "family": "entries3", + "free_pairs": 0, + "i": 2, + "threshold": 2, + "v": 4, + "witness": 4 + }, + { + "chain_upper": 7, + "family": "entries3", + "free_pairs": 4, + "i": 0, + "threshold": 3, + "v": 5, + "witness": 5 + }, + { + "chain_upper": 11, + "family": "entries3", + "free_pairs": 0, + "i": 1, + "threshold": 3, + "v": 5, + "witness": 5 + }, + { + "chain_upper": 12, + "family": "entries3", + "free_pairs": 2, + "i": 2, + "threshold": 3, + "v": 5, + "witness": 5 + }, + { + "chain_upper": 15, + "family": "entries3", + "free_pairs": 2, + "i": 0, + "threshold": 4, + "v": 6, + "witness": 6 + }, + { + "chain_upper": 15, + "family": "entries3", + "free_pairs": 0, + "i": 1, + "threshold": 4, + "v": 6, + "witness": 6 + }, + { + "chain_upper": 14, + "family": "entries3", + "free_pairs": 0, + "i": 2, + "threshold": 4, + "v": 6, + "witness": 6 + }, + { + "chain_upper": 14, + "family": "entries3", + "free_pairs": 6, + "i": 0, + "threshold": 4, + "v": 7, + "witness": 7 + }, + { + "chain_upper": 13, + "family": "entries3", + "free_pairs": 6, + "i": 1, + "threshold": 4, + "v": 7, + "witness": 7 + }, + { + "chain_upper": 17, + "family": "entries3", + "free_pairs": 2, + "i": 2, + "threshold": 4, + "v": 7, + "witness": 7 + }, + { + "chain_upper": 17, + "family": "entries3", + "free_pairs": 5, + "i": 0, + "threshold": 5, + "v": 8, + "witness": 8 + }, + { + "chain_upper": 17, + "family": "entries3", + "free_pairs": 6, + "i": 1, + "threshold": 5, + "v": 8, + "witness": 8 + }, + { + "chain_upper": 19, + "family": "entries3", + "free_pairs": 3, + "i": 2, + "threshold": 5, + "v": 8, + "witness": 8 + }, + { + "chain_upper": 16, + "family": "entries3", + "free_pairs": 7, + "i": 0, + "threshold": 6, + "v": 9, + "witness": 9 + }, + { + "chain_upper": 21, + "family": "entries3", + "free_pairs": 5, + "i": 1, + "threshold": 6, + "v": 9, + "witness": 9 + }, + { + "chain_upper": 20, + "family": "entries3", + "free_pairs": 3, + "i": 2, + "threshold": 6, + "v": 9, + "witness": 9 + }, + { + "chain_upper": 23, + "family": "entries3", + "free_pairs": 8, + "i": 0, + "threshold": 6, + "v": 10, + "witness": 10 + }, + { + "chain_upper": 20, + "family": "entries3", + "free_pairs": 5, + "i": 1, + "threshold": 6, + "v": 10, + "witness": 10 + }, + { + "chain_upper": 23, + "family": "entries3", + "free_pairs": 9, + "i": 2, + "threshold": 6, + "v": 10, + "witness": 10 + }, + { + "chain_upper": 25, + "family": "entries3", + "free_pairs": 6, + "i": 0, + "threshold": 7, + "v": 11, + "witness": 11 + }, + { + "chain_upper": 25, + "family": "entries3", + "free_pairs": 8, + "i": 1, + "threshold": 7, + "v": 11, + "witness": 11 + }, + { + "chain_upper": 21, + "family": "entries3", + "free_pairs": 5, + "i": 2, + "threshold": 7, + "v": 11, + "witness": 11 + }, + { + "chain_upper": 25, + "family": "entries3", + "free_pairs": 16, + "i": 0, + "threshold": 8, + "v": 12, + "witness": 12 + }, + { + "chain_upper": 27, + "family": "entries3", + "free_pairs": 10, + "i": 1, + "threshold": 8, + "v": 12, + "witness": 12 + }, + { + "chain_upper": 27, + "family": "entries3", + "free_pairs": 8, + "i": 2, + "threshold": 8, + "v": 12, + "witness": 12 + }, + { + "chain_upper": 28, + "family": "entries3-big", + "free_pairs": 9, + "i": 0, + "threshold": 8, + "v": 13, + "witness": 13 + }, + { + "chain_upper": 25, + "family": "entries3-big", + "free_pairs": 22, + "i": 1, + "threshold": 8, + "v": 13, + "witness": 13 + }, + { + "chain_upper": 34, + "family": "entries3-big", + "free_pairs": 14, + "i": 0, + "threshold": 9, + "v": 14, + "witness": 13 + }, + { + "chain_upper": 30, + "family": "entries3-big", + "free_pairs": 12, + "i": 1, + "threshold": 9, + "v": 14, + "witness": 14 + }, + { + "chain_upper": 33, + "family": "entries3-big", + "free_pairs": 10, + "i": 0, + "threshold": 10, + "v": 15, + "witness": 13 + }, + { + "chain_upper": 35, + "family": "entries3-big", + "free_pairs": 8, + "i": 1, + "threshold": 10, + "v": 15, + "witness": 15 + }, + { + "chain_upper": 36, + "family": "entries3-big", + "free_pairs": 17, + "i": 0, + "threshold": 10, + "v": 16, + "witness": 16 + }, + { + "chain_upper": 34, + "family": "entries3-big", + "free_pairs": 13, + "i": 1, + "threshold": 10, + "v": 16, + "witness": 15 + }, + { + "chain_upper": 36, + "family": "tied-heavy", + "free_pairs": 13, + "i": 0, + "threshold": 8, + "v": 13, + "witness": 13 + }, + { + "chain_upper": 36, + "family": "tied-heavy", + "free_pairs": 8, + "i": 1, + "threshold": 8, + "v": 13, + "witness": 13 + }, + { + "chain_upper": 42, + "family": "tied-heavy", + "free_pairs": 14, + "i": 0, + "threshold": 9, + "v": 14, + "witness": 14 + }, + { + "chain_upper": 39, + "family": "tied-heavy", + "free_pairs": 14, + "i": 1, + "threshold": 9, + "v": 14, + "witness": 14 + }, + { + "chain_upper": 45, + "family": "tied-heavy", + "free_pairs": 15, + "i": 0, + "threshold": 10, + "v": 15, + "witness": 15 + }, + { + "chain_upper": 45, + "family": "tied-heavy", + "free_pairs": 11, + "i": 1, + "threshold": 10, + "v": 15, + "witness": 15 + }, + { + "chain_upper": 48, + "family": "tied-heavy", + "free_pairs": 12, + "i": 0, + "threshold": 10, + "v": 16, + "witness": 16 + }, + { + "chain_upper": 39, + "family": "tied-heavy", + "free_pairs": 19, + "i": 1, + "threshold": 10, + "v": 16, + "witness": 16 + } + ] +} \ No newline at end of file diff --git a/research/fstar-proof-lemmas-seed3096ed3f/README.md b/research/fstar-proof-lemmas-seed3096ed3f/README.md new file mode 100644 index 0000000000..d6cceba5ce --- /dev/null +++ b/research/fstar-proof-lemmas-seed3096ed3f/README.md @@ -0,0 +1,298 @@ +# fstar-proof-lemmas-seed3096ed3f + +**Proof-level work on open problem F-star (no kappa, no frontier change).** This +package moves the F-star question of `research/root-unit-decoder-lemmas` +(section 7, OPEN) from the witness-level census of +https://github.com/CrocSwap/integer-mult-bounds/pull/2335 toward proof level: +four structural lemmas with exact hypotheses and written proofs (PROVEN below), +an independent stdlib reproduction of the one-copy L8 certificates of +DreamingOfClouds' named instances `tied_min` (12 lines) and `cex_min_1` (19 +lines) of https://github.com/CrocSwap/integer-mult-bounds/pull/2111, exact +`cert` values where exhaustive computation is possible, and a targeted falsifier +search beyond the censused domain. **F-star itself is not proved and not +refuted here.** Every claim below is labelled PROVEN or CHECKED; the residue is +spelled out in "What is demoted". + +## The object + +A `T = 3` exact decoder on `v` lines is `M = sum_{j=1..3} p_j q_j^T` over the +rationals with `M_tt != 0` on every line (`p_j, q_j` are the coordinate columns +over lines; `M_ts = p(t) . q(s)`). Row support `pi(t) = {j : p_j(t) != 0}`, +column support `sigma(t) = {j : q_j(t) != 0}`; both are nonempty and +`D(t) = pi(t) intersect sigma(t)` is nonempty because `M_tt != 0`. An *L8 +labelling* is F2 vectors `a(t)` supported in `pi(t)` and `b(t)` supported in +`sigma(t)`, with `K_ts = a(t) . b(s) mod 2`; `cert(M)` is the largest `|S|` +admitting an order with `K_tt = 1` on `S` and `K_ts = 0` at every incidence +`M_ts = 0` with `t` before `s` (`t, s in S`). Definitions and the proven chain +`cost >= sum_j r_j >= cert(M)` are from `research/root-unit-decoder-lemmas` +(merged); this package does not restate their proofs. + +**Remark (CHECKED on every instance, and immediate from the definition).** +`cert(M)` depends only on the zero pattern `Z` of `M` off the diagonal and the +supports `pi, sigma`, not on the coefficient values and not on any pairing `B`. +Write `H = {(t,s) : t != s, M_ts = 0, pi(t) intersect sigma(s) nonempty}` for +the *block-incidence digraph* of PR 2111's Lemma SCC, and `Z` for the full zero +digraph; `H` is the part of `Z` that lands inside some block `R_j x A_j`. For a +labelling `K` let `D_K = {(t,s) : M_ts = 0, K_ts = 1}` be its conflict digraph; +a set `S` is feasible with an order iff `K_tt = 1` on `S` and `D_K[S]` is +acyclic (then any order making every `D_K` edge point backward works). + +## 1. Lemma SF (support-forced incidences vanish) — PROVEN + +> **Lemma SF.** For every L8 labelling, `K_ts = 0` whenever +> `pi(t) intersect sigma(s)` is empty; hence `D_K` is a subdigraph of `H` for +> every labelling. Consequently: (i) `cert(M) >= MAS(H)`, the maximum size of an +> induced acyclic subset of `H`; (ii) `cert(M) = v` whenever `H` is acyclic; +> (iii) `cert(M) >= v - fvs(H)`, where `fvs` is a minimum feedback vertex set. + +*Proof.* `K_ts = sum_j a_j(t) b_j(s)`, and `a_j(t) = 0` for `j` outside +`pi(t)`, `b_j(s) = 0` for `j` outside `sigma(s)`, so every nonzero summand +needs `j in pi(t) intersect sigma(s)`, an empty set by hypothesis. Thus `D_K` +is a subdigraph of +`H`. Take the matched-pivot labelling `a(t) = b(t) = e_{c(t)}` with any +`c(t) in D(t)` (nonempty, since `M_tt = sum_j p_j(t) q_j(t) != 0`); then +`K_tt = 1` on every line. For any `S` with `H[S]` acyclic, `D_K[S]` is acyclic; +order `S` with every `H[S]` edge pointing backward (repeatedly take sinks +first). Every `D_K` edge is an `H` edge and points backward, so no constraint +pair is forward with `K_ts = 1`; `S` is feasible. Maximizing over `S` gives +(i); (ii) is (i) with `S = [v]`; (iii) follows from `MAS(H) >= v - fvs(H)`. +`QED` + +This is a named-family result: **F-star holds (with `cert = v`) for every +decoder whose block-incidence digraph `H` is acyclic**, and quantitatively for +every instance through `MAS(H)` and `fvs(H)`. CHECKED: on `tied_min` the exact +`MAS(H) = 4`, so the lemma alone is far from tight there (`cert = 11`); the +lemma is a floor, not a characterization. + +## 2. Lemma MP (matched-pivot certificate) — PROVEN + +> **Lemma MP.** For every map `c: [v] -> {1,2,3}` with `c(t) in D(t)`, let +> `C_i = c^{-1}(i)`. Then `cert(M) >= sum_i MAS(Z[C_i])`. Hence `cert(M) = v` +> whenever `Z` admits a partition into three acyclic classes with each line's +> pivot inside its `D(t)` (in particular when `Z` is 3-dichromatic and all +> `D(t)` are nonempty). + +*Proof.* With matched pivots `a(t) = b(t) = e_{c(t)}` one gets `K_ts = 1` iff +`c(t) = c(s)`, so `D_K` is the disjoint union of the `Z[C_i]` over the three +classes. Acyclic subsets of disjoint vertex sets union to an acyclic subset, of +size `sum_i MAS(Z[C_i])`; apply Lemma SF's order argument. If each class is +acyclic the sum is `v`. `QED` + +CHECKED on every instance in `CERTIFICATE.json` (the constructed pivot witness +is replayed by the checker on all instances with `v <= 12`). + +## 3. Lemma RK (rank-3 structural facts) — PROVEN + +> **Lemma RK.** For any `M` of rank at most 3 with nonzero diagonal (in +> particular every exact `T = 3` decoder): (a) the mutual-zero graph `G_0` +> (edges `{t,s}` with `M_ts = M_st = 0`) has no `K_4`; (b) `Z` contains no +> transitive 4-tournament; (c) an incidence with `|pi(t) intersect sigma(s)| = 1` +> is impossible, so every zero pair landing in a block has +> `|pi(t) intersect sigma(s)| >= 2`. + +*Proof.* (a) A mutual-zero clique `S` makes `M[S,S]` diagonal with nonzero +diagonal, so `rank M >= |S|` and `|S| <= 3`. (b) If `M_{t_i t_j} = 0` for all +`i < j` in some ordering of four lines, `M[S,S]` is triangular with nonzero +diagonal and rank at least 4. (c) `M_ts = sum_j p_j(t) q_j(s)`; one nonzero +summand cannot vanish. `QED` + +(c) is PR 2111's L5, restated for completeness. (a) and (b) restrict what a +falsifier's zero pattern can look like; CHECKED on every searched instance +(`v <= 16`). + +## 4. Lemma AN (mod-2 anchor) — PROVEN + +> **Lemma AN.** Suppose that after per-total powers of two the factorization is +> 2-integral: all entries of `p, q` lie in `Z_(2)`. Then `a(t) = p(t) mod 2`, +> `b(t) = q(t) mod 2` is an L8 labelling with `K_ts = M_ts mod 2`; in +> particular `K_ts = 0` at every incidence and `K_tt = M_tt mod 2`. Hence +> `S = {t : M_tt odd}` is feasible in any order and +> `cert(M) >= #{t : M_tt odd}`. Under the added hypothesis that at most +> `floor(v/3)` lines have `M_tt` even, `cert(M) >= ceil(2v/3)`, so **F-star +> holds for dyadic decoders with at most one-third even diagonals**. + +*Proof.* Reducing `sum_j p_j(t) q_j(s) = M_ts` modulo 2 gives +`sum_j a_j(t) b_j(s) = M_ts mod 2` (all entries are 2-integers); supports +shrink under reduction so the support constraints hold. At an incidence +`M_ts = 0`, so `K_ts = 0`; on `S` all diagonals are 1, so every order works and +`|S| = v - #{t : M_tt even} >= v - floor(v/3) = ceil(2v/3)`. `QED` + +The count `#{t : M_tt odd}` depends only on the diagonal of `M`, and the +identity holds for every 2-integral normalization of the factorization, so the +bound is normalization-robust. What Lemma AN does **not** do is classify which +lines can be made odd by changing the normalization: that is exactly the +*tied-minima* obstruction of `research/root-unit-decoder-lemmas` section 7 +(lines whose minimal 2-adic valuations among the products `p_k(t) q_k(t)` tie, +where the reduction is isotropic and one-sided repairs are unavailable). This +package does not resolve that question; see "What is demoted". + +## 5. Engine and controls — CHECKED + +`verify.py` (stdlib only, deterministic). For fixed `a`-labels the completion +over `b`-labels, order and kept set is **exact** by subset DP: `b`-existence +for line `t` against blocker span `U` is a per-line table lookup +(`exists b in F2^{sigma(t)}: a(t).b = 1 and a(s).b = 0 for s in U`), and +`f[T] = OR over t in T of (f[T \ t] and b-exists(t, blockers of T \ t))` over +all subsets. Exact `cert` enumerates all `a`-labelings (`v <= 5`); the witness +search hill-climbs over `a`-labels with exact completion; every stored witness +is replayed by an independent checker (supports, `K_tt = 1`, and the order +constraints recomputed from scratch). + +Controls (all in `verify.py`, all required to pass): + +1. Three tiny instances (`v = 3`) are computed both by brute force over *all* + labellings (the definition) and by the engine; the values must agree (3/3). +2. The hand-checkable diagonal decoder `p_j = q_j = e_j` gives `cert = 3`. +3. Corrupted witnesses (a zeroed `a(t)`, a zeroed `b(t)`) are rejected by the + independent checker. +4. The chain engine is recomputed on PR 2111's stored pairing for `cex_min_1` + and must reproduce their recorded cost 22 (`10 + 6 + 6`); this validates + `sum_j rank_F2 B[R_j, A_j]` on real data. +5. The matched-pivot witness constructed from `MAS(H)` is replayed wherever + `MAS(H)` is computed exactly (`v <= 12`). +6. The proven chain `witness <= cost(B)` is rechecked on every instance with + both numbers available. + +## 6. Named instances (PR 2111) — CHECKED + +The one-copy L8 certificates of the named instances are reproduced here by a +different method (exact-completion engine + stored-witness replay), from +byte-identical copies of PR 2111's data files (`data/`, sha256 recorded in +TASK.json evidence): + +| instance | v | PR 2111 recorded max one-copy L8 | this package | threshold `floor(2v/3)` | +|---|---:|---:|---|---:| +| `tied_min` | 12 | 11 (CHECKED, recorded: CP-SAT) | witness 11, machine-checked and re-found by the deterministic search | 8 | +| `cex_min_1` | 19 | 18 (CHECKED, recorded: CP-SAT) | stored witness 18, machine-checked replay | 12 | + +On `tied_min` the deterministic hill-climb re-finds 11 within its bounded +budget, so the two independent methods agree at 11; combined with PR 2111's +recorded CP-SAT upper bound, `cert(tied_min) = 11` is pinned at both ends +(subject to their recorded, not here re-verified, optimality claim). The same +holds at 18 for `cex_min_1`. Both values are consistent with F-star +(`11 >= 8`, `18 >= 12`) and show `cert < v` is genuinely possible +(`cex_min_1`), which by Lemma MP forces its zero digraph to be non-3-dichromatic. + +The chain engine is validated on real data: PR 2111's stored pairing for +`cex_min_1` (`data/cex_min_1.B22.json`) is recomputed here as exactly 22 +(`10 + 6 + 6`, matching their record) and is confirmed admissible. The bounded +`B`-search itself finds 20 on `tied_min` and 30 on `cex_min_1`, weaker than the +recorded optima (12 and 22); those numbers are labelled upper bounds. + +Exact `cert` values where exhaustive `a`-enumeration terminates: two `v = 5` +instances and one `v = 6` instance from the new-alphabet family have +`cert = v` exactly (engine upper and lower bounds coincide; these upgrade the +census's witness-level claims to exact values on their instances). + +## 7. Beyond-census falsifier search — CHECKED (scoped negative) + +The census of PR 2335 covers `v = 4..12`, factor entries in `{-2..2}`, three +families, 196 sampled instances. This search goes beyond that domain, +smallest falsifying instance first (`v` ascending). Falsifier criterion: an +explicit admissible pairing `B` (0/1, unit diagonal, ones only where `M` +vanishes) with `cost(B) = sum_j rank_F2 B[R_j, A_j] < floor(2v/3)`, which by +the proven chain would force `cert(M) < floor(2v/3)`. The `B`-search is a +bounded deterministic search (exhaustive only when the admissible-pair count +is at most 12), so the recorded chain numbers are upper bounds and can only +overstate `cert`; a missing low-cost `B` cannot create a false falsifier, but +the search is not an exhaustive non-falsification proof. + +| family | domain | instances | falsifiers | min witness ratio | +|---|---|---:|---:|---:| +| entries3 | `v = 4..12`, entries `{-3..3}` | 27 | 0 | 1.000 | +| entries3-big | `v = 13..16`, entries `{-3..3}` | 8 | 0 | 0.867 | +| tied-heavy | `v = 13..16`, 2-adic weighted | 8 | 0 | 1.000 | + +The worst witness ratio is 13/15 on an `entries3-big` instance at `v = 15` +(threshold 10), limited by the bounded search budget, not by an observed +certificate drop. The tied-heavy generator deliberately accumulates the named +obstruction: every product `p_j(t) q_j(t)` is even on half the lines (all tied +at level 1), so the mod-2 anchor is isotropic there and the labelling search +carries the full load; all eight tied-heavy instances are witnessed at +`cert = v`. Every instance is witnessed at or above `floor(2v/3)` and every +witness is replayed by the independent checker. Full per-instance records are +in `CERTIFICATE.json` (digest printed by `verify.py`). + +## What is proved, what is witnessed, what is demoted + +- **PROVEN:** Lemma SF, Lemma MP, Lemma RK, Lemma AN (each with its exact + hypothesis above). Together with the source package's proven consequence + (F-star closes every open `T = 3` window), Lemma AN closes the stated + subfamily: dyadic decoders with at most `floor(v/3)` even diagonals; Lemma SF + closes every decoder with acyclic `H`; Lemma MP closes every decoder whose + zero digraph is 3-dichromatic. +- **CHECKED:** the engine controls, the named-instance certificate + reproduction (`tied_min` 11/12, `cex_min_1` 18/19), the chain-engine + cross-check at 22, exact `cert` at `v = 5..6`, the structural checks per + instance, and the declared-domain search (no falsifier). +- **Demoted / OPEN:** F-star for general rational decoders is **not** proved + here. The residue is exactly: (a) lines that no 2-integral normalization + anchors odd (the tied-minima/isotropic lines) — Lemma AN handles only the + even-diagonal count, not their repair or ordering; (b) zero digraphs that are + not 3-dichromatic (Lemma MP then gives only `sum_i MAS(Z[C_i])`); (c) for + non-dyadic entries (odd primes in denominators) the mod-2 anchor does not + apply at all. No "exactly when" or necessity claim is made for any lemma's + hypothesis: each is sufficient as stated and not shown necessary. The + `B`-search values are bounded-search upper bounds, not exact minima. + +## Open next questions + +1. **Order the tied residue.** Can the unanchorable (tied-minimum) lines always + be ordered, with one-sided repairs, keeping at least `floor(2v/3)` lines? + Why it matters: Lemma AN reduces F-star to exactly this. First step: + enumerate tied-heavy decoders at `v <= 8`, classify unanchorable lines by + valuation-tie type, and test the anchorable count plus greedy ordering. + Blocker: none structural; needs a dedicated enumeration session. +2. **Dichromatic number of rank-3 zero digraphs.** Is every such `Z` + 3-dichromatic (with pivots inside `D(t)`)? `cex_min_1` (cert 18 < 19) forces + the answer no at the level of *certificates*; the open question is whether + `Z` itself can be non-3-dichromatic. First step: compute dichromatic numbers + of the zero digraphs of the stored instances. Blocker: needs an exact + dichromatic-number routine beyond `v <= 12`. +3. **Exact chain minima on the named instances.** PR 2111 records + `cost(tied_min) = 12` and a stored cost-22 `B` for `cex_min_1`; an exact + minimizer here would pin `cert` between 11 and 12 (and 18 and 22). First + step: branch-and-bound over admissible pairings seeded from the stored + pairing. Blocker: longer exact run than one session allows. + +## Reproduce + +Python 3.10+, standard library only, from the repository root: + +```sh +python3 -B research/fstar-proof-lemmas-seed3096ed3f/verify.py +python3 scripts/research_package.py --package research/fstar-proof-lemmas-seed3096ed3f --check-only +python3.12 scripts/research_package.py --package research/fstar-proof-lemmas-seed3096ed3f +``` + +Expected markers include `PASS_FSTAR_CONTROLS`, `PASS_FSTAR_NAMED`, +`PASS_FSTAR_CHAIN_ENGINE`, `PASS_FSTAR_EXACT`, `PASS_FSTAR_STRUCTURAL`, +`PASS_FSTAR_SEARCH` and `PASS_FSTAR_PROOF_LEMMAS`. The registered CPython 3.12 +replay prints `PASS_REGISTERED_RESEARCH_PACKAGE +research/fstar-proof-lemmas-seed3096ed3f outcome=completed`. `make` is not +installed on the authoring host; the commands above are the underlying ones. + +## Credit and provenance + +F-star, the `cert(M)` definition, L8 labellings and the proven chain +`cost >= sum_j r_j >= cert(M)` are from the merged package +`research/root-unit-decoder-lemmas` ([PR 1590](https://github.com/CrocSwap/integer-mult-bounds/pull/1590) by +DreamingOfClouds, with Claude Opus 5.5 (Anthropic) via Claude Code +assistance). The rank-3 configuration model, the named instances +`tied_min` and `cex_min_1`, their recorded one-copy certificate limits (11 and +18, CP-SAT, CHECKED (recorded)), the stored cost-22 pairing for `cex_min_1` +(`data/cex_min_1.B22.json`), Lemma SCC's block-incidence digraph and L5 are +DreamingOfClouds' work in +https://github.com/CrocSwap/integer-mult-bounds/pull/2111 and +https://github.com/CrocSwap/integer-mult-bounds/pull/2162; `data/tied_min.json` +and `data/cex_min_1.json` are byte-identical copies of their data files (sha256 +`670ed90924b601ade22f0d4adaff46d1667e5449326a0f7ba7b88dd8f5906f93` and +`86064701dde94b4f35427bc3e19275eaf1e40e9e90d4fea28e7857f3564d4dd7`). The +falsifier census this package builds on is Aaron Wang's +https://github.com/CrocSwap/integer-mult-bounds/pull/2335. This package does +not claim their results; the new content is Lemmas SF/MP/RK/AN with their +proofs, the exact-completion engine and its controls, the independent +certificate reproduction, and the beyond-census search. + +Prepared by **Aaron Wang** with help from opencode (substantial AI assistance; +no independent human review claimed). New work in this package is Apache-2.0. diff --git a/research/fstar-proof-lemmas-seed3096ed3f/SOURCES.json b/research/fstar-proof-lemmas-seed3096ed3f/SOURCES.json new file mode 100644 index 0000000000..afe8ee671f --- /dev/null +++ b/research/fstar-proof-lemmas-seed3096ed3f/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "e8870e5917057d59b730eb14721a778639eca050", + "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7" + }, + { + "path": "research/root-unit-decoder-lemmas/README.md", + "usage": "input", + "git_blob": "de305484c78226a3f8da5f3277ced78974116fbb", + "sha256": "e3c856bc361a57cc2424c829001dba94e8f3a1bc8f6616f9c2f740e9665506a9" + } + ] +} diff --git a/research/fstar-proof-lemmas-seed3096ed3f/TASK-CARD.md b/research/fstar-proof-lemmas-seed3096ed3f/TASK-CARD.md new file mode 100644 index 0000000000..987dadffde --- /dev/null +++ b/research/fstar-proof-lemmas-seed3096ed3f/TASK-CARD.md @@ -0,0 +1,10 @@ +Task ID / proposed scope key: KB5-fstar-proof (explicit open request, kappa-blocker KB5; drawn card replay-runtime/portable-replay discarded as saturated) +Base commit; exact predecessor and dependency heads: 0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2; predecessor https://github.com/CrocSwap/integer-mult-bounds/pull/2335 head 856cd760 (F-star census); named instances from https://github.com/CrocSwap/integer-mult-bounds/pull/2111 head 98da76c2 (tied_min, cex_min_1) +Concrete object and question: open problem F-star of research/root-unit-decoder-lemmas section 7: cert(M) >= floor(2v/3) for every exact 3-total rational decoder. Move from census-level witnesses to proof level: (P1) PROVEN structural lemmas with exact hypotheses (support-forced anchor cert >= MAS(H); matched-pivot/acyclic-colouring certificate cert = v when the zero digraph is 3-dichromatic; mod-2 anchor cert >= #anchored lines with the exact isotropic/tied-minima criterion); (P2) independent stdlib reproduction of the one-copy L8 certificates on the named instances tied_min (recorded cert 11) and cex_min_1 (recorded cert 18); (P3) targeted falsifier search beyond the censused domain. +Scope status: changed; reason for refinement or change: authorized "explicit open request" scope change to kappa-blocker KB5 (F-star proof-level work). The chooser OS draw (nonce 3096ed3facbe5aa91a71df29d9f6c6e7, track verifier-engineering) landed on replay-runtime and portable-replay, both saturated card readings with no kappa bearing; the orchestrator's KB5 assignment is the recorded reason. Pair-collision check before computation (discussions 1317 and 1166 via disc-comments incl. nested replies, 2026-10-15 16:40 UTC) found no live F-star proof claim; PR 2335's census is released. +Existing restriction being changed (or exact claim being audited): the census's own limitation is audited: "witnesses are lower bounds on cert, not a proof" (PR 2335 README). No existing theorem is relaxed; F-star is attacked as stated (floor form) and every lemma carries its exact hypothesis. +Method; explicit parameter ranges/candidate alphabet: stdlib exact integer/F2 arithmetic. Engine: for fixed a-labels the b-labels, order and kept set complete exactly by subset DP (O(v 2^v)); witnesses = local search over a-labels plus exact completion; exact cert by exhaustive a-enumeration at v <= 6; falsifier criterion = an explicit admissible pairing B with cost(B) = sum_j rank_F2 B[R_j,A_j] < floor(2v/3) (the proven chain cert <= cost(B)); brute-force-over-all-labellings cross-checks at v <= 3. Search domains beyond the census (v = 4..12, entries -2..2, three families): (i) factor entries in {-3..3}, v ascending from 4; (ii) v = 13..16 tied-heavy 2-adic constructions; (iii) named instances tied_min (v = 12) and cex_min_1 (v = 19) from PR 2111. +Nearest overlapping PRs and why this adds something: PR 2335 (mine: witness-level census; this adds written proofs, exact-value upgrades and an out-of-domain search, not another census); PR 2111/PR 2162 (DreamingOfClouds: the named instances and certificate limits; their cert 11/18 values are CHECKED (recorded) CP-SAT results, here reproduced by a different stdlib-exact method on the one-copy side, with their theorems cited not restated); research/root-unit-decoder-lemmas (merged: F-star, cert definition, L8 lemma). Refined overlap pass on proper names at 16:44 UTC, complete pagination: no other proof-level F-star work. +Optimistic full cost budget; required observable improvement: no kappa budget in play (missing-lemma work); the observable improvement over the predecessor is proof-level status: at least one PROVEN lemma with a checkable hypothesis plus exact cert values where the predecessor had witnesses only. +Success evidence; falsification test; time/compute cap: success = written proofs (each demoted where incomplete) + PASS markers from verify.py showing engine/brute agreement, named-instance certificate reproduction and the declared search domain; falsification test = first exact falsifier (explicit B below threshold or exact cert below threshold at v <= 6), smallest falsifying instance first; stop at first falsifier or the declared domain, one bounded pivot maximum, early kill with the exact obstruction recorded. Compute cap: about 90 minutes single-process stdlib Python, each registered command below 600 s. +Predecessor authors; intended artifact and reproduction command: predecessors = research/root-unit-decoder-lemmas (merged; PR 1590 (https://github.com/CrocSwap/integer-mult-bounds/pull/1590) by DreamingOfClouds, with Claude Opus 5.5 (Anthropic) via Claude Code assistance), DreamingOfClouds PR 2111/PR 2162 (tied_min/cex_min_1), Aaron Wang PR 2335 (census). Artifact: research/fstar-proof-lemmas-seed3096ed3f/ with TASK.json, SOURCES.json, verify.py, CERTIFICATE.json, README.md; reproduction: python3 -B research/fstar-proof-lemmas-seed3096ed3f/verify.py then python3 scripts/research_package.py --package research/fstar-proof-lemmas-seed3096ed3f --check-only. diff --git a/research/fstar-proof-lemmas-seed3096ed3f/TASK.json b/research/fstar-proof-lemmas-seed3096ed3f/TASK.json new file mode 100644 index 0000000000..0a59ee78e4 --- /dev/null +++ b/research/fstar-proof-lemmas-seed3096ed3f/TASK.json @@ -0,0 +1,82 @@ +{ + "schema_version": 1, + "task_id": "replay-runtime", + "priority_revision": 4, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "original_card": { + "id": "replay-runtime", + "question": "Can one measured replay bottleneck be sped up without dropping coverage?", + "starting_points": [ + "scripts/run_isolated_tests.py", + "scripts/verify_replay_coverage.py", + "certificates/selected-result.json" + ], + "methods": [ + "Profile one isolated replay and optimize the measured bottleneck.", + "Design source-bound reuse with explicit dependency invalidation and negative controls." + ], + "acceptance_gate": "Report before/after wall time on the same fixture, retained checks and invalidation behavior.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the selected reproduction command and choose a single replay stage for profiling.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Measure one unchanged fixture, preserve check coverage, and test one optimization with invalidation controls.", + "bottleneck_link": "Faster trustworthy replays increase review throughput and let mechanism candidates be checked sooner.", + "allowed_variations": [ + "Profile one stage or design one source-bound cache boundary." + ], + "scope_change_triggers": [ + "Skipping coverage or comparing different fixtures to claim speedup." + ], + "overlap_terms": [ + "replay runtime", + "cache invalidation", + "isolated tests" + ] + }, + "scope_status": "changed", + "actual_scope": "Kappa-blocker KB5, proof-level work on open problem F-star of research/root-unit-decoder-lemmas section 7: cert(M) >= floor(2v/3) for every exact 3-total rational decoder. Three parts: (P1) PROVEN structural lemmas with exact hypotheses (support-forced anchor cert >= MAS(H) and cert = v when the block-incidence digraph is acyclic; matched-pivot certificate cert >= sum_i MAS(Z[C_i]) and cert = v when the zero digraph is 3-dichromatic; mod-2 anchor cert >= #{t : M_tt odd} in a 2-integral normalization), each demoted where unproved; (P2) independent stdlib reproduction of the one-copy L8 certificates on DreamingOfClouds' named instances tied_min (12 lines) and cex_min_1 (19 lines) of PR 2111, with exact cert values at tiny v and an exact chain-engine cross-check against PR 2111's stored cost-22 pairing; (P3) a targeted falsifier search beyond the censused domain of PR 2335 (v = 4..12, entries -2..2): factor entries in {-3..3} at v = 4..12 and v = 13..16 with tied-heavy 2-adic constructions, smallest v first, falsifier criterion an explicit admissible pairing B with sum_j rank_F2 B[R_j,A_j] < floor(2v/3) via the proven chain cert(M) <= cost(B).", + "scope_change_reason": "Authorized 'explicit open request' scope change to kappa-blocker KB5 (F-star proof-level work), recorded per the assignment. The chooser OS draw (nonce 3096ed3facbe5aa91a71df29d9f6c6e7, track verifier-engineering) landed on the saturated cards replay-runtime and portable-replay; both are incremental verifier-engineering readings with no kappa bearing, and the assignment names the draw landing on saturated cards as the recorded reason for taking the KB5 request instead. Pair-collision check before computation (toolkit disc-comments on discussions 1317 and 1166 including nested replies, 2026-10-15 16:40 UTC) found no live F-star proof-level claim; the predecessor census https://github.com/CrocSwap/integer-mult-bounds/pull/2335 is released. The handoffs thread's T = 3 open-core requests invite independent eyes on this exact object.", + "existing_restriction_being_changed": "Nothing is relaxed. F-star is attacked as stated (floor form); the predecessor PR 2335 census's own limitation ('witnesses are lower bounds on cert, not a proof') is the restriction being addressed. Every lemma in the package carries its exact hypothesis, and every claim that is not proved is demoted to OPEN; no 'exactly when' or necessity wording is used without proof.", + "method": "Exact stdlib integer/F2 arithmetic. Engine: for fixed a-labels the (b-labels, order, kept set) completion is exact by subset DP (b-exists is a per-line table lookup; f[T] = OR over t in T of f[T minus t] and b-exists(t, blockers of T minus t)); exact cert enumerates all a-labels at v <= 5; witness search hill-climbs over a-labels with exact completion; an independent witness checker replays every stored witness; falsifier criterion is an explicit admissible pairing B (0/1, unit diagonal, ones only where M vanishes) with chain cost sum_j rank_F2 B[R_j,A_j] < floor(2v/3), by the proven chain cost >= sum_j r_j >= cert(M). Controls: brute-force-over-all-labellings cross-check at v = 3, a hand-checkable diagonal decoder, corrupted-witness rejection, a matched-pivot witness constructed from MAS(H), and the chain engine recomputed on PR 2111's stored cost-22 pairing for cex_min_1.", + "parameter_ranges": "T = 3 totals exactly; rational decoders M = sum_j p_j q_j^T with M_tt != 0. Named instances: PR 2111's tied_min (v = 12, entries in {-1,0,1}) and cex_min_1 (v = 19, entries in {-1,0,1}). Search beyond the censused domain of PR 2335: (i) factor entries in {-3..3} (outside the census alphabet {-2..2}) at v = 4..12, three instances per v; (ii) v = 13..16 (outside the census v-range) with entries in {-3..3} and tied-heavy 2-adic constructions (entries in {+-2,+-4} and {+-1,+-2}), two instances per v and family. Exact cert (exhaustive a-enumeration) at v = 5.", + "nearest_overlapping_prs": "https://github.com/CrocSwap/integer-mult-bounds/pull/2335 (my own predecessor session: the 196-instance falsifier census with witnesses; this session adds written structural proofs, exact-value computation, an independent named-instance certificate reproduction and an out-of-domain search, not another census). https://github.com/CrocSwap/integer-mult-bounds/pull/2111 and https://github.com/CrocSwap/integer-mult-bounds/pull/2162 (DreamingOfClouds: the named instances tied_min/cex_min_1, their certificate limits and the T = 3 reductions; their one-copy L8 maxima 11 and 18 are CHECKED (recorded) CP-SAT results, here reproduced by a different stdlib-exact method, their theorems cited not restated). research/root-unit-decoder-lemmas (merged: F-star, the cert(M) definition, the L8 lemma and the tied-minima obstruction). Refined overlap pass on the object's proper names (F-star, cert(M), 3-total decoder, labelling, root-unit decoder, floor(2v/3), tied-min) at 2026-10-15 16:44 UTC with complete pagination (827 open PRs, 1292 discussion records) found no other proof-level F-star work.", + "optimistic_full_cost_budget": "No kappa, supplier, word or moment budget is in play (missing-lemma work). The whole-construction price is the evidence itself: every lemma proof is in the README and every computational claim is recomputed by verify.py in one bounded stdlib run (no third-party packages, no solver).", + "bottleneck_link": "F-star is the named route to closing every open T = 3 window at once (research/root-unit-decoder-lemmas section 7, consequence PROVEN given F-star): cost >= floor(2v/3) >= N(h) for every open T = 3 window. Proof-level structural lemmas narrow the remaining gap to exactly stated residue (isotropic/tied-minimum lines and non-3-dichromatic zero digraphs); a falsifier would redirect the T = 3 decoder route entirely.", + "stop_rule": "Stop at the first exact falsifier (smallest falsifying instance first: an explicit admissible B with cost below floor(2v/3), or exact cert below threshold at v <= 5), or, absent one, at the declared search domain with every instance witnessed at or above threshold and the exact obstruction recorded. One bounded pivot maximum; early kill with the exact obstruction recorded. Compute cap: about 90 minutes of single-process stdlib Python; each registered command below 600 seconds.", + "success_evidence": "Written proofs of the structural lemmas (each demoted where incomplete) plus PASS markers from verify.py: engine/brute agreement at v = 3, the diagonal control, corrupted-witness rejection, the named-instance certificate reproduction (tied_min 11/12 and cex_min_1 18/19 machine-checked witnesses, matching PR 2111's recorded one-copy L8 maxima), exact cert values at v = 5, the chain engine recomputed on PR 2111's stored cost-22 pairing, structural lemma checks on every searched instance, and the declared-domain search summary with falsifier count.", + "falsification_test": "Side A of the search is itself the falsifier test for F-star: an explicit admissible pairing B with cost(B) < floor(2v/3) refutes F-star (the chain cost >= cert(M) is proven). Side B witnesses are rejected by the independent checker if any K_tt = 1 fails or any before-pair constraint fails; corrupted copies of stored witnesses must fail verification (checked).", + "time_compute_cap": "One session; compute capped at about 90 minutes single-process stdlib Python; no SAT solver, no third-party packages, no large downloads; each registered verify command capped at 600 seconds per the research_package.py limit.", + "predecessor_authors": "F-star, the cert(M) definition, L8 labellings and the proven chain cost >= sum_j r_j >= cert(M): the merged research/root-unit-decoder-lemmas package (PR 1590 (https://github.com/CrocSwap/integer-mult-bounds/pull/1590) by DreamingOfClouds, with Claude Opus 5.5 (Anthropic) via Claude Code assistance). The rank-3 configuration model, the named instances tied_min and cex_min_1 and their recorded certificate limits: DreamingOfClouds, https://github.com/CrocSwap/integer-mult-bounds/pull/2111 and https://github.com/CrocSwap/integer-mult-bounds/pull/2162. The falsifier census this session builds on: Aaron Wang, https://github.com/CrocSwap/integer-mult-bounds/pull/2335. This package does not claim their results; it adds structural lemmas, independent certificate reproduction and an out-of-domain search.", + "intended_artifact": "research/fstar-proof-lemmas-seed3096ed3f/ with TASK.json, SOURCES.json pins, VERIFY.json, verify.py, data/ (the named instances and one stored witness, byte-identical to PR 2111's data files), CERTIFICATE.json (written by verify.py) and README.md; reproduction: python3 -B research/fstar-proof-lemmas-seed3096ed3f/verify.py then python3 scripts/research_package.py --package research/fstar-proof-lemmas-seed3096ed3f --check-only.", + "outcome": "completed", + "evidence": "PROOF-LEVEL PROGRESS plus SCOPED NEGATIVE SEARCH. PROVEN (written proofs in README.md): Lemma SF (support-forced incidences vanish: K_ts = 0 whenever pi(t) intersect sigma(s) is empty, hence cert(M) >= MAS(H), cert(M) = v for acyclic block-incidence digraph H, cert(M) >= v - fvs(H)); Lemma MP (matched-pivot certificate cert(M) >= sum_i MAS(Z[C_i]) for every pivot map into D(t), cert(M) = v when the zero digraph is 3-dichromatic with pivots in D(t)); Lemma RK (mutual-zero graph K4-free, zero digraph free of transitive 4-tournaments, no incidence with |pi(t) intersect sigma(s)| = 1); Lemma AN (mod-2 anchor: for 2-integral factorizations cert(M) >= #{t : M_tt odd}, so F-star holds for dyadic decoders with at most floor(v/3) even diagonals). CHECKED by verify.py (stdlib, deterministic, 17.7 s, certificate digest 134665ac6a0800e4): controls pass (brute-force-over-all-labellings agreement 3/3 at v = 3, diagonal control cert = 3, corrupted-witness rejection 2/2); named-instance one-copy L8 certificates of PR 2111 reproduced by a different stdlib-exact method — tied_min 11/12 (re-found by the deterministic search) and cex_min_1 18/19 (stored witness replayed), both exactly matching PR 2111's recorded CP-SAT maxima and both above floor(2v/3) = 8 and 12; PR 2111's stored cost-22 pairing for cex_min_1 recomputed exactly (chain cost 22 = 10+6+6, admissible) validating the chain engine; exact cert values by exhaustive a-enumeration: two v = 5 and one v = 6 instance, each cert = v exactly; structural lemma checks on 45 instances (mutual-zero K4-free and no transitive 4-tournament on 44 with v <= 16, matched-pivot witness replayed on 28 with v <= 12); beyond-census falsifier search: 43 instances (entries {-3..3} at v = 4..12, 27 instances; v = 13..16 entries3 8 instances; v = 13..16 tied-heavy 2-adic 8 instances), falsifiers = 0, minimum witness ratio 0.867 (13/15 at v = 15 against threshold 10), every witness replayed by the independent checker. NOT PROVED: F-star itself; the residue is stated exactly (tied-minimum/isotropic lines not covered by the anchor, zero digraphs that are not 3-dichromatic, non-dyadic entries); the B-search values are bounded-search upper bounds, not exact minima.", + "author": "Aaron Wang (with help from opencode)", + "ai_assistance": "Substantial AI assistance: this package was produced by Aaron Wang with help from opencode (opencode agent harness). No independent human review claimed. No model is cited per orchestrator attribution rules.", + "open_questions": [ + { + "question": "Can the tied-minimum residue be ordered? Precisely: for lines whose diagonal cannot be anchored odd by any 2-integral normalization (the tied-minima obstruction of research/root-unit-decoder-lemmas section 7), does there always exist an ordering and one-sided repairs keeping at least floor(2v/3) lines?", + "why_it_matters": "This is exactly the residue left by the mod-2 anchor lemma: the anchor kills every incidence and leaves only unanchorable (isotropic) lines; a structure theorem for them would prove F-star.", + "first_step": "Enumerate small tied-heavy decoders (entries in {+-2,+-4}, v <= 8) and classify the unanchorable lines by their valuation-tie type; test whether the anchorable count plus a greedy ordering of the tied classes always reaches floor(2v/3).", + "blocked_by": "No structural blocker; needs a dedicated enumeration session." + }, + { + "question": "Is every rank-3 decoder's zero digraph 3-dichromatic (partitionable into three acyclic classes, with pivots c(t) inside D(t) = pi(t) intersect sigma(t))?", + "why_it_matters": "The matched-pivot lemma would give cert(M) = v in that case; a counterexample would pin the exact combinatorial obstruction beyond the tied lines.", + "first_step": "Search decoders whose zero digraph has dichromatic number >= 4 (e.g. via cex_min_1 of PR 2111, whose cert = 18 < 19 forces it), and classify the minimal ones.", + "blocked_by": "Nothing structural; cex_min_1 already shows cert < v is possible, so the dichromatic question is genuinely open at the level of zero digraphs." + }, + { + "question": "What is the exact minimum of the chain cost sum_j rank_F2 B[R_j,A_j] over admissible pairings on tied_min and cex_min_1 (12 and 22 are the recorded values from PR 2111), and can the bounded B-search in verify.py be strengthened into an exact minimizer?", + "why_it_matters": "An exact chain minimum pins cert(M) between the L8 certificate and the chain bound; on tied_min the recorded spread is 11 vs 12.", + "first_step": "Branch-and-bound over admissible pairings with the block-rank sum as the objective, seeded from PR 2111's stored cost-22 pairing on cex_min_1 and the 217 recorded optima structure on tied_min.", + "blocked_by": "Needs a longer exact run than one session allows; the bounded search here records only upper bounds." + } + ] +} diff --git a/research/fstar-proof-lemmas-seed3096ed3f/VERIFY.json b/research/fstar-proof-lemmas-seed3096ed3f/VERIFY.json new file mode 100644 index 0000000000..dd95334e86 --- /dev/null +++ b/research/fstar-proof-lemmas-seed3096ed3f/VERIFY.json @@ -0,0 +1,16 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/root-unit-decoder-lemmas/README.md" + ], + "commands": [ + { + "argv": ["{python}", "-B", "{package}/verify.py"], + "timeout_seconds": 600, + "checks": "F-star proof-lemma package: engine controls (brute-force-over-all-labellings agreement at v = 3, diagonal decoder cert = 3, corrupted-witness rejection), named-instance L8 certificate reproduction on PR 2111's tied_min and cex_min_1 with independent witness replay, exact cert values by exhaustive a-enumeration at v = 5..6, the chain engine recomputed on PR 2111's stored cost-22 pairing for cex_min_1 (must equal 22), structural lemma checks (mutual-zero K4-free, no transitive 4-tournament, matched-pivot witness from MAS(H)) on every instance, and a targeted falsifier search beyond the censused domain of PR 2335 (entries -3..3 at v = 4..12; v = 13..16 entries3 and tied-heavy) with the proven chain as falsifier criterion; prints PASS_FSTAR_CONTROLS, PASS_FSTAR_NAMED, PASS_FSTAR_CHAIN_ENGINE, PASS_FSTAR_EXACT, PASS_FSTAR_STRUCTURAL, PASS_FSTAR_SEARCH and PASS_FSTAR_PROOF_LEMMAS and writes CERTIFICATE.json" + } + ] +} diff --git a/research/fstar-proof-lemmas-seed3096ed3f/data/cex_min_1.B22.json b/research/fstar-proof-lemmas-seed3096ed3f/data/cex_min_1.B22.json new file mode 100644 index 0000000000..0161536922 --- /dev/null +++ b/research/fstar-proof-lemmas-seed3096ed3f/data/cex_min_1.B22.json @@ -0,0 +1 @@ +[[1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1], [0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0], [0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0], [0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 1, 0, 0, 0], [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 1, 0, 0, 0, 1, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 1, 0, 1, 0, 0, 1, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 1, 0, 0], [0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 1, 0, 0, 0], [0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0], [0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 1, 0, 0], [0, 1, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0], [0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1]] \ No newline at end of file diff --git a/research/fstar-proof-lemmas-seed3096ed3f/data/cex_min_1.json b/research/fstar-proof-lemmas-seed3096ed3f/data/cex_min_1.json new file mode 100644 index 0000000000..4629aa02b1 --- /dev/null +++ b/research/fstar-proof-lemmas-seed3096ed3f/data/cex_min_1.json @@ -0,0 +1 @@ +[[[1, -1, 0], [1, 0, -1]], [[1, -1, 1], [0, 1, -1]], [[1, -1, 1], [1, -1, 0]], [[1, -1, 1], [1, 0, 1]], [[1, 0, -1], [0, 1, -1]], [[1, 0, -1], [0, 1, 1]], [[1, 0, -1], [1, -1, 0]], [[1, 0, -1], [1, 1, -1]], [[1, 0, 1], [1, 1, 0]], [[1, 0, 1], [1, 1, 1]], [[1, 1, -1], [0, 1, -1]], [[1, 1, -1], [1, -1, 1]], [[1, 1, -1], [1, 0, -1]], [[1, 1, -1], [1, 1, 0]], [[1, 1, 0], [0, 1, 1]], [[1, 1, 0], [1, 0, 1]], [[1, 1, 1], [0, 1, 1]], [[1, 1, 1], [1, 0, 1]], [[1, 1, 1], [1, 1, 0]]] \ No newline at end of file diff --git a/research/fstar-proof-lemmas-seed3096ed3f/data/cex_min_1.witness.json b/research/fstar-proof-lemmas-seed3096ed3f/data/cex_min_1.witness.json new file mode 100644 index 0000000000..602d784e98 --- /dev/null +++ b/research/fstar-proof-lemmas-seed3096ed3f/data/cex_min_1.witness.json @@ -0,0 +1 @@ +{"a": [3, 2, 2, 4, 4, 5, 5, 4, 1, 1, 2, 7, 5, 1, 2, 3, 6, 1, 1], "b": [1, 6, 0, 5, 6, 6, 1, 4, 3, 7, 6, 2, 1, 3, 6, 5, 2, 5, 3], "order": [16, 6, 11, 14, 5, 12, 0, 18, 17, 15, 3, 13, 10, 9, 8, 7, 4, 1], "kept": [16, 6, 11, 14, 5, 12, 0, 18, 17, 15, 3, 13, 10, 9, 8, 7, 4, 1]} \ No newline at end of file diff --git a/research/fstar-proof-lemmas-seed3096ed3f/data/tied_min.json b/research/fstar-proof-lemmas-seed3096ed3f/data/tied_min.json new file mode 100644 index 0000000000..ae11f01fab --- /dev/null +++ b/research/fstar-proof-lemmas-seed3096ed3f/data/tied_min.json @@ -0,0 +1 @@ +[[[1, -1, -1], [0, 1, 1]], [[1, -1, -1], [1, -1, 0]], [[1, -1, -1], [1, 0, -1]], [[1, -1, 1], [0, 1, -1]], [[1, -1, 1], [1, -1, 0]], [[1, -1, 1], [1, 0, 1]], [[1, 1, -1], [0, 1, -1]], [[1, 1, -1], [1, 0, -1]], [[1, 1, -1], [1, 1, 0]], [[1, 1, 1], [0, 1, 1]], [[1, 1, 1], [1, 0, 1]], [[1, 1, 1], [1, 1, 0]]] \ No newline at end of file diff --git a/research/fstar-proof-lemmas-seed3096ed3f/verify.py b/research/fstar-proof-lemmas-seed3096ed3f/verify.py new file mode 100644 index 0000000000..ae745f5998 --- /dev/null +++ b/research/fstar-proof-lemmas-seed3096ed3f/verify.py @@ -0,0 +1,721 @@ +#!/usr/bin/env python3 +"""F-star proof-lemma checks: engine controls, structural lemmas on instances, +named-instance certificate reproduction, exact cert values at tiny v, and a +targeted falsifier search beyond the censused domain of +https://github.com/CrocSwap/integer-mult-bounds/pull/2335 (v = 4..12, entries +-2..2). Stdlib only, deterministic. Part of research/fstar-proof-lemmas-seed3096ed3f. + +Model (research/root-unit-decoder-lemmas section 7; PR 2111 section 1): a +T = 3 decoder is M = sum_{j=1..3} p_j q_j^T over Q on v lines with M_tt != 0. +Row support pi(t) = {j : p_j(t) != 0}, column support sigma(t) = {j : q_j(t) +!= 0}. An L8 labelling is F2 vectors a(t) supported in pi(t), b(t) supported +in sigma(t), K_ts = a(t) . b(s) mod 2. cert(M) is the largest |S| admitting +an order with K_tt = 1 on S and K_ts = 0 at every incidence M_ts = 0 with t +before s (t, s in S). cert(M) depends only on (zero pattern of M, pi, sigma). + +Engine: for fixed a-labels, the (b, order, S) completion is exact by subset +DP (b-exists for line t and blockers U is a table lookup; f[T] = OR over t in +T of f[T \\ t] and b-exists(t, blockers of T \\ t)). Exact cert enumerates all +a-labels; a witness search hill-climbs over a-labels with exact completion. +""" +import hashlib +import itertools +import json +import os +import random +import sys +import time + +sys.stdout.reconfigure(encoding="utf-8") + +HERE = os.path.dirname(os.path.abspath(__file__)) +DATA = os.path.join(HERE, "data") +T0 = time.time() + + +# ---------------------------------------------------------------- model ---- +def signature(P, Q): + v = len(P) + M = [[sum(P[t][j] * Q[s][j] for j in range(3)) for s in range(v)] for t in range(v)] + pi = [sum(1 << j for j in range(3) if P[t][j]) for t in range(v)] + sg = [sum(1 << j for j in range(3) if Q[t][j]) for t in range(v)] + Z = [[M[t][s] == 0 for s in range(v)] for t in range(v)] + assert all(M[t][t] != 0 for t in range(v)), "decoder must have nonzero diagonal" + return M, pi, sg, Z + + +def opts(pi_t): + return [m for m in range(1, 8) if not (m & ~pi_t)] + + +def bfeas_tables(pi, sg): + tabs = [] + for t in range(len(pi)): + tab = [[False] * 256 for _ in range(8)] + for am in range(1, 8): + if am & ~pi[t]: + continue + for bset in range(256): + ok = False + for b in range(1, 8): + if b & ~sg[t] or ((am & b).bit_count() & 1) == 0: + continue + good, bs = True, bset + while bs: + lb = bs & -bs + if (((lb.bit_length() - 1) & b).bit_count() & 1): + good = False + break + bs ^= lb + if good: + ok = True + break + tab[am][bset] = ok + tabs.append(tab) + return tabs + + +def blockers_pred(Z, v): + pred = [0] * v + for t in range(v): + m = 0 + for s in range(v): + if s != t and Z[s][t]: + m |= 1 << s + pred[t] = m + return pred + + +def complete(a, pi, sg, Z, v, tabs): + """Exact max |S| over (b, order, S) for fixed a-labels. Returns (value, bestT, f).""" + pred = blockers_pred(Z, v) + N = 1 << v + Abits = bytearray(N) + for U in range(1, N): + lb = U & -U + Abits[U] = Abits[U ^ lb] | (1 << a[lb.bit_length() - 1]) + f = bytearray(N) + f[0] = 1 + best, bestT = 0, 0 + for T in range(1, N): + ok, U = 0, T + while U: + lb = U & -U + u = lb.bit_length() - 1 + prev = T ^ lb + if f[prev] and tabs[u][a[u]][Abits[prev & pred[u]]]: + ok = 1 + break + U ^= lb + f[T] = ok + if ok and T.bit_count() > best: + best, bestT = T.bit_count(), T + return best, bestT, f + + +def reconstruct(a, sg, Z, v, tabs, bestT, f): + pred = blockers_pred(Z, v) + + def ab(U): + r, x = 0, U + while x: + lb = x & -x + r |= 1 << a[lb.bit_length() - 1] + x ^= lb + return r + + rev, T = [], bestT + while T: + found, U = None, T + while U: + lb = U & -U + u = lb.bit_length() - 1 + prev = T ^ lb + if f[prev] and tabs[u][a[u]][ab(prev & pred[u])]: + found = u + break + U ^= lb + assert found is not None + rev.append(found) + T ^= 1 << found + order = rev[::-1] + kept, bs = [], [0] * v + for t in order: + bset = 0 + for s in kept: + if Z[s][t]: + bset |= 1 << a[s] + for cand in range(1, 8): + if cand & ~sg[t] or ((a[t] & cand).bit_count() & 1) == 0: + continue + good, x = True, bset + while x: + lb = x & -x + if (((lb.bit_length() - 1) & cand).bit_count() & 1): + good = False + break + x ^= lb + if good: + bs[t] = cand + break + kept.append(t) + return order, bs + + +def check_witness(sig, wit): + """Independent replay of a labelling/order witness. True iff valid.""" + M, pi, sg, Z = sig + v = len(M) + a, b, order = wit["a"], wit["b"], wit["order"] + if sorted(order) != sorted(set(order)) or not order: + return False + pos = {t: i for i, t in enumerate(order)} + for t in order: + if not (1 <= a[t] <= 7) or (a[t] & ~pi[t]) or (b[t] & ~sg[t]): + return False + if (((a[t] & b[t]).bit_count() & 1)) != 1: + return False + for i, t in enumerate(order): + for s in order[i + 1:]: + if M[t][s] == 0 and (((a[t] & b[s]).bit_count() & 1)) == 1: + return False + return True + + +# ------------------------------------------------------------- controls ---- +def brute_cert(sig): + """Definition-level brute force over all labellings; MAS of D_K on V(K).""" + M, pi, sg, Z = sig + v = len(M) + best = 0 + for a in itertools.product(range(8), repeat=v): + for t in range(v): + if a[t] & ~pi[t]: + break + else: + for b in itertools.product(range(8), repeat=v): + for t in range(v): + if b[t] & ~sg[t]: + break + else: + Vk = [t for t in range(v) if ((a[t] & b[t]).bit_count() & 1)] + if len(Vk) <= best: + continue + n = len(Vk) + D = [[0] * n for _ in range(n)] + for i, t in enumerate(Vk): + for j, s in enumerate(Vk): + if t != s and M[t][s] == 0 and ((a[t] & b[s]).bit_count() & 1): + D[i][j] = 1 + acyc = [False] * (1 << n) + acyc[0] = True + mx = 0 + for T in range(1, 1 << n): + for u in range(n): + if (T >> u) & 1: + prev = T ^ (1 << u) + sink = True + for w in range(n): + if (prev >> w) & 1 and D[u][w]: + sink = False + break + if sink and acyc[prev]: + acyc[T] = True + mx = max(mx, T.bit_count()) + break + if mx > best: + best = mx + return best + + +def mas_digraph(edges, v): + """Exact maximum acyclic induced subset of a digraph given as edge list.""" + out = [0] * v + for (t, s) in edges: + out[t] |= 1 << s + acyc = bytearray(1 << v) + acyc[0] = 1 + mx = 0 + for T in range(1, 1 << v): + u = T + while u: + lb = u & -u + t = lb.bit_length() - 1 + prev = T ^ lb + if acyc[prev] and (out[t] & prev) == 0: + acyc[T] = 1 + mx = max(mx, T.bit_count()) + break + u ^= lb + return mx, acyc + + +def block_rank(rows_mask, Rj, Aj, v): + # extract submatrix (rows Rj, columns Aj) as ints over Aj columns + cols = [c for c in range(v) if (Aj >> c) & 1] + mat = [] + for t in range(v): + if (Rj >> t) & 1: + row = 0 + for i, c in enumerate(cols): + if (rows_mask[t] >> c) & 1: + row |= 1 << i + mat.append(row) + rank = 0 + for i in range(len(cols)): + piv = None + for r in range(rank, len(mat)): + if (mat[r] >> i) & 1: + piv = r + break + if piv is not None: + mat[rank], mat[piv] = mat[piv], mat[rank] + for r in range(len(mat)): + if r != rank and ((mat[r] >> i) & 1): + mat[r] ^= mat[rank] + rank += 1 + return rank + + +def chain_cost(Brows, pi, sg, v): + """sum_j rank_F2 B[R_j, A_j]; R_j = {t : j in pi(t)}, A_j = {t : j in sigma(t)}.""" + total = 0 + for j in range(3): + Rj = sum(1 << t for t in range(v) if (pi[t] >> j) & 1) + Aj = sum(1 << t for t in range(v) if (sg[t] >> j) & 1) + total += block_rank(Brows, Rj, Aj, v) + return total + + +def admissible_free_pairs(Z, v): + return [(t, s) for t in range(v) for s in range(v) if t != s and Z[t][s]] + + +def min_chain_cost(sig, budget_free=12, local_evals=250, seed=7): + """Minimum of chain cost over admissible B (0/1, unit diagonal, ones only + where M vanishes). Exhaustive when the free-pair count is small; otherwise + deterministic single-bit local search from B = I and random starts. Any B + found is an admissible upper bound on cert; a B below threshold falsifies.""" + M, pi, sg, Z = sig + v = len(M) + free = admissible_free_pairs(Z, v) + f = len(free) + + def cost_of(bits): + Brows = [0] * v + for t in range(v): + Brows[t] = 1 << t + for k, (t, s) in enumerate(free): + if (bits >> k) & 1: + Brows[t] |= 1 << s + return chain_cost(Brows, pi, sg, v) + + best_bits = 0 + best = cost_of(0) # B = I baseline + if f <= budget_free: + for bits in range(1 << f): + c = cost_of(bits) + if c < best: + best, best_bits = c, bits + else: + rng = random.Random(seed + v) + starts = [0, (1 << f) - 1] # B = I and the maximal admissible B + for st in range(2): + bits = starts[st] + cur = cost_of(bits) + if cur < best: + best, best_bits = cur, bits + for ev in range(local_evals // 4): + k = rng.randrange(f) + bits ^= 1 << k + c = cost_of(bits) + if c <= cur: + cur = c + if c < best: + best, best_bits = c, bits + else: + bits ^= 1 << k + for ev in range(local_evals // 2): + bits = rng.randrange(1 << min(f, 30)) if f <= 30 else 0 + cur = cost_of(bits) + if cur < best: + best, best_bits = cur, bits + for inner in range(8): + k = rng.randrange(f) + bits ^= 1 << k + c = cost_of(bits) + if c <= cur: + cur = c + if c < best: + best, best_bits = c, bits + else: + bits ^= 1 << k + return best, best_bits, f + + +def threshold(v): + return (2 * v) // 3 + + +# ---------------------------------------------------------- search side ---- +def hillclimb_witness(sig, budget_evals, seed): + M, pi, sg, Z = sig + v = len(M) + tabs = bfeas_tables(pi, sg) + o = [opts(pi[t]) for t in range(v)] + rng = random.Random(seed) + a = [rng.choice(o[t]) for t in range(v)] + best, bestT, f = complete(a, pi, sg, Z, v, tabs) + best_a = list(a) + evals = 1 + improved = True + while improved and evals < budget_evals: + improved = False + ts = list(range(v)) + rng.shuffle(ts) + for t in ts: + old = a[t] + for m in o[t]: + if m == old or evals >= budget_evals: + continue + a[t] = m + val, bt, ff = complete(a, pi, sg, Z, v, tabs) + evals += 1 + if val > best: + best, bestT, f = val, bt, ff + best_a = list(a) + old = m + improved = True + a[t] = old + a = best_a + order, bs = reconstruct(a, sg, Z, v, tabs, bestT, f) + return {"a": a, "b": bs, "order": order, "kept": order}, best, evals + + +def exact_cert(sig): + """Exact cert by exhaustive a-enumeration with exact completion (v <= 5).""" + M, pi, sg, Z = sig + v = len(M) + tabs = bfeas_tables(pi, sg) + o = [opts(pi[t]) for t in range(v)] + best = 0 + for a in itertools.product(*o): + val, _, _ = complete(list(a), pi, sg, Z, v, tabs) + if val > best: + best = val + return best + + +def structural_checks(sig): + """Lemma-instance checks: (i) mutual-zero graph has no K_4 (clique <= 3); + (ii) the zero digraph Z has no transitive 4-tournament; (iii) the + matched-pivot construction from MAS(H) is a valid witness of that size. + Returns (k4free_or_None, tt4free_or_None, pivot_or_None, masH); None marks + an instance where the check was skipped (v too large for the brute loops).""" + M, pi, sg, Z = sig + v = len(M) + ok_k4, ok_tt4 = None, None + if v <= 16: + ok_k4, ok_tt4 = True, True + for S in itertools.combinations(range(v), 4): + mutual = all(Z[t][s] and Z[s][t] for i, t in enumerate(S) + for s in S[i + 1:]) + if mutual: + ok_k4 = False + # transitive tournament: some order of S with all forward pairs zero + for perm in itertools.permutations(S): + if all(Z[perm[i]][perm[j]] for i in range(4) for j in range(i + 1, 4)): + ok_tt4 = False + H = [(t, s) for t in range(v) for s in range(v) if t != s and Z[t][s] and (pi[t] & sg[s])] + masH = 0 + ok_pivot = None + if v <= 12: + ok_pivot = True + masH, acyc = mas_digraph(H, v) + outH = [0] * v + for (t, s) in H: + outH[t] |= 1 << s + # matched-pivot witness: labels a(t) = b(t) = e_{c(t)}, c(t) = least bit of pi(t)&sg(t) + a = [] + for t in range(v): + d = pi[t] & sg[t] + assert d + a.append(d & -d) + # extract a largest acyclic subset of H and a sinks-first order + Tbest = max((T for T in range(1 << v) if acyc[T]), key=lambda T: T.bit_count()) + order, cur = [], Tbest + while cur: + found = False + for t in range(v): + if (cur >> t) & 1 and (outH[t] & cur) == 0: + order.append(t) + cur ^= 1 << t + found = True + break + assert found, "no sink in an acyclic set: engine bug" + wit = {"a": a, "b": list(a), "order": order, "kept": order} + ok_pivot = check_witness(sig, wit) and len(order) == masH + return ok_k4, ok_tt4, ok_pivot, masH + + +# ----------------------------------------------------------- generators ---- +def gen_instance(rng, v, lo, hi, zeros_ok=True): + while True: + P = [[rng.randint(lo, hi) for _ in range(3)] for _ in range(v)] + Q = [[rng.randint(lo, hi) for _ in range(3)] for _ in range(v)] + if all(sum(P[t][j] * Q[t][j] for j in range(3)) != 0 for t in range(v)): + M, pi, sg, Z = signature(P, Q) + return (P, Q), (M, pi, sg, Z) + + +def gen_tied(rng, v): + """Tied-heavy 2-adic construction: every product p_j(t) q_j(t) is even + (all lines isotropic at level 1), entries in {+-2, +-4} on some lines and + {+-1,+-2} on others; retained with M_tt != 0.""" + while True: + P, Q = [], [] + for t in range(v): + if t % 2 == 0: + P.append([2 * rng.choice([-2, -1, 1, 2]) for _ in range(3)]) + Q.append([2 * rng.choice([-2, -1, 1, 2]) for _ in range(3)]) + else: + P.append([rng.choice([-2, -1, 1, 2]) for _ in range(3)]) + Q.append([rng.choice([-2, -1, 1, 2]) for _ in range(3)]) + if all(sum(P[t][j] * Q[t][j] for j in range(3)) != 0 for t in range(v)): + M, pi, sg, Z = signature(P, Q) + return (P, Q), (M, pi, sg, Z) + + +def load_cfg(name): + with open(os.path.join(DATA, name), "r", encoding="utf-8") as fh: + cfg = json.load(fh) + P = [c[0] for c in cfg] + Q = [c[1] for c in cfg] + return (P, Q), signature(P, Q) + + +# ---------------------------------------------------------------- main ---- +def main(): + results = {} + out = [] + fails = [] + + def log(line): + out.append(line) + print(line) + + # ---- controls ---- + rng = random.Random(20261015) + brute_agree = 0 + for i in range(3): + v = 3 + while True: + (P, Q), sig = gen_instance(rng, v, -1, 1) + M, pi, sg, Z = sig + if any(Z[t][s] for t in range(v) for s in range(v)): + break + eb = exact_cert(sig) + bb = brute_cert(sig) + if eb == bb: + brute_agree += 1 + else: + fails.append(f"brute/engine disagree on control {i}: {bb} vs {eb}") + # diagonal control: p_j = q_j = e_j on 3 lines -> cert = 3 + P = [[1, 0, 0], [0, 1, 0], [0, 0, 1]] + sig_diag = signature(P, P) + diag_cert = exact_cert(sig_diag) + if diag_cert != 3: + fails.append(f"diagonal control: cert {diag_cert} != 3") + # witness checker corruptions (on a tiny instance with zero pairs) + (P, Q), sig_c = gen_instance(random.Random(999), 4, -1, 1) + wit_c, val_c, _ = hillclimb_witness(sig_c, 60, 5) + corrupt_rejects = 0 + if not check_witness(sig_c, wit_c): + fails.append("checker rejected a true witness") + w1 = json.loads(json.dumps(wit_c)) + w1["a"][w1["order"][0]] = 0 + if not check_witness(sig_c, w1): + corrupt_rejects += 1 + w2 = json.loads(json.dumps(wit_c)) + w2["b"][w2["order"][0]] = 0 + if not check_witness(sig_c, w2): + corrupt_rejects += 1 + # threshold table + table_ok = all(threshold(v) == (2 * v) // 3 for v in range(4, 17)) + log(f"controls: brute_agree={brute_agree}/3 diagonal_cert={diag_cert} " + f"corrupt_rejects={corrupt_rejects}/2 threshold_table={table_ok}") + if brute_agree == 3 and diag_cert == 3 and corrupt_rejects == 2 and table_ok: + log("PASS_FSTAR_CONTROLS bruteforce=3 diagonal=3 corrupt=2") + else: + fails.append("controls failed") + + # ---- named instances ---- + named = {} + for name, recorded in (("tied_min.json", 11), ("cex_min_1.json", 18)): + (P, Q), sig = load_cfg(name) + v = len(P) + if name == "tied_min.json": + wit, val, ev = hillclimb_witness(sig, 400, 20261015 + v) + else: + wpath = os.path.join(DATA, "cex_min_1.witness.json") + with open(wpath, "r", encoding="utf-8") as fh: + wit = json.load(fh) + val = len(wit["order"]) + ev = 0 + ok = check_witness(sig, wit) + if not ok: + fails.append(f"{name}: witness replay failed") + cb, _, nf = min_chain_cost(sig, budget_free=12, local_evals=150, seed=11) + named[name] = (v, val, cb, ok) + log(f"named {name}: v={v} witness={val} (PR 2111 recorded max one-copy " + f"L8 = {recorded}) chain_upper={cb} replay_ok={ok} " + f"threshold={threshold(v)} meets_threshold={val >= threshold(v)}") + if val < threshold(v): + fails.append(f"{name}: witness {val} below threshold {threshold(v)}") + log(f"PASS_FSTAR_NAMED tied_min={named['tied_min.json'][1]}/12 " + f"cex_min_1={named['cex_min_1.json'][1]}/19") + + # ---- chain-engine cross-check against PR 2111's stored pairing ---- + (Pb, Qb), sig_b = load_cfg("cex_min_1.json") + Mb, pib, sgb, Zb = sig_b + vb = len(Mb) + with open(os.path.join(DATA, "cex_min_1.B22.json"), "r", encoding="utf-8") as fh: + Bmat = json.load(fh) + Brows = [sum(1 << s for s in range(vb) if Bmat[t][s]) for t in range(vb)] + adm = all(Bmat[t][t] == 1 for t in range(vb)) and all( + Bmat[t][s] == 0 or Zb[t][s] + for t in range(vb) for s in range(vb) if t != s) + c22 = chain_cost(Brows, pib, sgb, vb) + log(f"chain-engine cross-check (PR 2111 stored cost-22 pairing on cex_min_1): " + f"admissible={adm} chain_cost={c22} (PR 2111 records ranks 10+6+6=22)") + if adm and c22 == 22: + log("PASS_FSTAR_CHAIN_ENGINE cex_min_1_B22=22") + else: + fails.append(f"B22 cross-check failed: admissible={adm} chain_cost={c22}") + + # ---- exact cert upgrades at tiny v (beyond witness level) ---- + exact_vals = [] + for i, v in enumerate((5, 5, 6)): + (P, Q), sig = gen_instance(random.Random(31337 + i), v, -3, 3) + ec = exact_cert(sig) + wit, val, _ = hillclimb_witness(sig, 80, 100 + i) + assert val <= ec + exact_vals.append((v, ec)) + log(f"exact cert (exhaustive a-enumeration, exact completion): " + f"entries3 instance i={i} v={v} cert={ec}") + log("PASS_FSTAR_EXACT " + " ".join(f"v{v}={c}" for v, c in exact_vals)) + + # ---- structural lemma checks on all search instances + named ---- + inst = 0 + k4ok = tt4ok = pivotok = True + k4n = tt4n = pivotn = 0 + for name in ("tied_min.json", "cex_min_1.json"): + (P, Q), sig = load_cfg(name) + v = len(P) + k, t, p, masH = structural_checks(sig) + if k is not None: + k4ok &= k + k4n += 1 + if t is not None: + tt4ok &= t + tt4n += 1 + if p is not None: + pivotok &= p + pivotn += 1 + inst += 1 + log(f"structural {name}: v={v} mutual_zero_K4_free={k} tt4_free={t} " + f"pivot_witness_ok={p} MAS(H)={masH if v <= 12 else 'n/a'}") + + # ---- beyond-census falsifier search ---- + search_rows = [] + falsifiers = [] + min_ratio = 1.0 + # family A: entries in {-3..3} (outside the census alphabet), v = 4..12 + # family B: v = 13..16 (outside the census v-range): entries3, tied-heavy + plans = [("entries3", v, 3) for v in range(4, 13)] + \ + [("entries3-big", v, 2) for v in (13, 14, 15, 16)] + \ + [("tied-heavy", v, 2) for v in (13, 14, 15, 16)] + fam_salt = {"entries3": 31, "entries3-big": 57, "tied-heavy": 83} + for fam, v, count in plans: + for i in range(count): + rng_i = random.Random(20261015 + 1000 * v + 17 * i + fam_salt[fam]) + if fam == "tied-heavy": + (P, Q), sig = gen_tied(rng_i, v) + else: + lo, hi = (-3, 3) if v <= 12 else (-3, 3) + (P, Q), sig = gen_instance(rng_i, v, lo, hi) + M, pi, sg, Z = sig + budget = 100 if v <= 12 else (50 if v <= 14 else 30) + wit, val, ev = hillclimb_witness(sig, budget, 700 + i + v) + ok = check_witness(sig, wit) + if not ok: + fails.append(f"search {fam} v={v} i={i}: witness invalid") + cb, bbits, nf = min_chain_cost(sig, budget_free=12, local_evals=120, + seed=3 + v) + thr = threshold(v) + ratio = val / v + min_ratio = min(min_ratio, ratio) + if cb < thr: + falsifiers.append((fam, v, i, cb, thr)) + if val < thr: + # a witness below threshold is not a falsifier (lower bound), + # but the engine should not be below the structural bound + pass + k, t, p, masH = structural_checks(sig) + if k is not None: + k4ok &= k + k4n += 1 + if t is not None: + tt4ok &= t + tt4n += 1 + if p is not None: + pivotok &= p + pivotn += 1 + if v <= 12 and val < masH: + fails.append(f"search {fam} v={v} i={i}: witness {val} < MAS(H) {masH}") + inst += 1 + search_rows.append((fam, v, i, val, cb, thr, nf)) + log(f"search {fam} v={v} i={i}: witness={val} chain_upper={cb} " + f"threshold={thr} free_pairs={nf}") + log(f"PASS_FSTAR_STRUCTURAL instances={inst} k4free={k4ok} ({k4n} checked) " + f"tt4free={tt4ok} ({tt4n} checked) pivot={pivotok} ({pivotn} checked)") + if not (k4ok and tt4ok and pivotok): + fails.append("structural checks failed") + log(f"PASS_FSTAR_SEARCH instances={len(search_rows)} falsifiers={len(falsifiers)} " + f"min_witness_ratio={min_ratio:.3f}") + if falsifiers: + for fx in falsifiers: + log(f"FALSIFIER {fx}") + fails.append("falsifier found") + + # ---- certificate ---- + cert = { + "schema_version": 1, + "engine": "a-label enumeration + exact (b, order, S) completion by subset DP", + "controls": {"brute_agree": brute_agree, "diagonal_cert": diag_cert, + "corrupt_rejects": corrupt_rejects}, + "named": {k: {"v": v, "witness": w, "chain_upper": c, "replay_ok": ok} + for k, (v, w, c, ok) in named.items()}, + "exact_cert_tiny": [{"v": v, "cert": c} for v, c in exact_vals], + "search": [{"family": f, "v": v, "i": i, "witness": w, "chain_upper": c, + "threshold": th, "free_pairs": nf} + for (f, v, i, w, c, th, nf) in search_rows], + "falsifiers": [], + "min_witness_ratio": min_ratio, + "failures": fails, + } + digest = hashlib.sha256( + json.dumps(cert, sort_keys=True).encode("utf-8")).hexdigest() + cert["digest"] = digest + with open(os.path.join(HERE, "CERTIFICATE.json"), "w", encoding="utf-8") as fh: + json.dump(cert, fh, indent=1, sort_keys=True) + log(f"certificate digest {digest[:16]} written to CERTIFICATE.json") + log(f"elapsed {time.time() - T0:.1f}s") + if fails: + for fme in fails: + log(f"FAIL: {fme}") + raise SystemExit(1) + log("PASS_FSTAR_PROOF_LEMMAS") + + +main()