diff --git a/.github/workflows/format-obstructions.yml b/.github/workflows/format-obstructions.yml new file mode 100644 index 0000000000..99a6263d02 --- /dev/null +++ b/.github/workflows/format-obstructions.yml @@ -0,0 +1,27 @@ +name: format-obstructions + +on: + pull_request: + paths: + - 'research/format-obstructions/**' + - '.github/workflows/format-obstructions.yml' + push: + paths: + - 'research/format-obstructions/**' + - '.github/workflows/format-obstructions.yml' + +jobs: + verify: + runs-on: ubuntu-latest + timeout-minutes: 60 + steps: + - uses: actions/checkout@v4 + - uses: actions/setup-python@v5 + with: + python-version: '3.12' + - name: Install the pinned packages (python-sat for the CaDiCaL checks) + run: python -m pip install -r research/format-obstructions/requirements.txt + - name: Replay the certificates, the toy, Theorem P, the #425 word and Theorem S, the pricing context and the E8 label SAT checks + run: python3 -B research/format-obstructions/verify.py --output "$RUNNER_TEMP/format-obstructions-out" + - name: Require an unchanged tree + run: git diff --exit-code diff --git a/research/format-obstructions/NOTICE b/research/format-obstructions/NOTICE new file mode 100644 index 0000000000..d77b237141 --- /dev/null +++ b/research/format-obstructions/NOTICE @@ -0,0 +1,43 @@ +Prepared by DreamingOfClouds with Claude Opus 5.5 (Anthropic), via Claude Code. Apache-2.0. +Inherited files retain their original notices and assistance disclosures. This package claims no exclusive +priority over concurrent work and reports no new kappa. The credits below do not imply review or endorsement. + +What this package contributes: PROOF.md and README.md (the statements and proofs of Theorems A, B, C, P and S, the +clique bound, and their scope), the checks in checks/ (taint replay and Thm A/B/C data on gcert/1 programs, the p = 3 +toy and its exhaustive optimum, the fixed-role cross-Gram computation, the overlap measurements, the replay and the +simulation of PR #425's word, the E8 label SAT instances, the clique numbers, the pricing context), verify.py, +expected.json, SOURCE.json and the small p = 3 program inputs/gcert1-p3-cone-R16.json (local research, not published +upstream). Everything else is vendored byte for byte or re-used as credited below. + +Vendored byte for byte (sha256 in SOURCE.json): + +- gx/gx.py: Jacob Sussman (Anthropic Claude assistance), gcert/1 and the reference checker gx.check1; Apache-2.0, + Copyright 2026 Jacob Sussman, jacobalansussman/wht-power-saving-lean at f010392c (as vendored in PR #327). +- inputs/gcert1-p11-pr193.json.gz: Jacob Sussman's gcert/1 certificate of Avi Eisenberg (ikeboy)'s PR #193 complex + helper (as vendored in research/five-stage-gen4-banks/inputs/complex on main). +- inputs/gcert1-p10-anneal-mw-flow.json.gz: PR #327 (DreamingOfClouds, head 40ed0456), the p = 10 complex program + compiled with PR #304's recipe. Its lineage: icekylinx (PR #144 paired cubes and signed decoder, PR #184 frame flow + and exact lift), Avi Eisenberg (ikeboy) (PR #191/#193/#194), chafreaky / Chafik Boukhalfa (PR #200 operation + frames and complex checker, PR #233 maximum-weight reuse pairs, PR #256 gcert emitter), eumemic (PR #168 modules and + physical frames), DaysSky (PR #162 carrier closure), Jacob Sussman (gcert/1, gx, the five-stage layout of + hcg890's PR #234, the unit convention of gxconv). Their notices are in PR #327 and PR #304. +- inputs/pr425/FULL-WORD.json.gz: PR #425 (jacklightChen / Zhihao Chen, with OpenAI Codex assistance; head e11ccea1), + the mutable-basis Hamming complex word, regenerated with its own hamming_packets.py and hamming_full.py under + Python 3.12 (sha256 e55a0d4a... equals the one in its EXPECTED.json). It builds on Dylan Crow's PR #370 table of + E8 root lines in Construction-A coordinates (with Anthropic Claude assistance) and on Jacob Sussman's E8 complex + unit as published in DaysSky's PR #352. Original notices: PR #425. +- inputs/pricing/cost.py: PR #346 (Louis Harrison), the cost model of PR #310 (Dylan Crow / utcorvusvolat-dotcom, w3 + supplier work); only solve_moment is used. +- inputs/pricing/hist_p10b.json: the five-stage normalised histogram of PR #325 (DreamingOfClouds) as copied from the + math.json that its verification writes (a run output at head 0eca9340, not a committed file); PR #325 builds on #315/#285/#276 (DreamingOfClouds), eumemic's PR #168 generator and source527 + package, chafreaky's PR #200 physical rules, hcg890 and Jacob Sussman's five-stage architecture, and Evan + McKinney's PR #197 completed banks. + +Used as references and not vendored: PR #386 (jacklightChen) for the width m = 64 of its compressed nine-stage windows; +PR #433 (icekylinx, split centres) and PR #442 (DaysSky, idle-axis hosting) for where recent gains came from; +PR #370 (Dylan Crow) for the E8 bit word and its copy loss 72; SovereignSteak's PR #250 and hcg890's PR #234 for the +five-stage ledger D = 4kv - 5 cst. checks/e8lib.py uses the E8 line coordinates of PR #370; checks/sat_e8.py and +checks/families.py are adapted from local research scripts of DreamingOfClouds (Claude assistance). + +The five-stage layout, the frame lemma (Lean) and gx.check1 are Jacob Sussman's. OpenAI: the original complex phase +network of "Integer multiplication below n log n". diff --git a/research/format-obstructions/PROOF.md b/research/format-obstructions/PROOF.md new file mode 100644 index 0000000000..d2e0ffc663 --- /dev/null +++ b/research/format-obstructions/PROOF.md @@ -0,0 +1,404 @@ +# Format obstructions: statements, proofs and the checks behind them + +Labels: **[P]** proved here by hand; **[C]** checked by computer, exactly (F₂, integer or `Fraction` arithmetic, or +SAT); **[M]** a pricer or model output, not a theorem; **[U]** a hypothesis read from upstream and not re-derived +here. `verify.py` runs every [C] and [M] item; §11 maps each statement to its check. + +## 0. Conventions + +- A label space L of dimension m carries a symmetric bilinear form ⟨·,·⟩ over a field F (F₂ with the dot product for + the complex words; ℚ with the E8 form or x ↦ xᵀ(I − J/9)y for the bit words). For a subspace V, V^⊥ is its + orthogonal, rk V = dim V − dim(V ∩ V^⊥) is the rank of the form restricted to V, and V is *nondegenerate* if + V ∩ V^⊥ = 0. If V is nondegenerate then L = V ⊕ V^⊥ and V^⊥ is nondegenerate (L is nondegenerate). +- A pair (port) a has a *label* U_a ⊆ L, nondegenerate of dimension k_a. In every program checked here U_a = ⟨q_a⟩ + with ⟨q_a, q_a⟩ ≠ 0 (k = 1). +- `h` is the window dimension of one invocation, `v` the number of ports, `R` the number of helper registers, + `cst` the copy cost, `m` the dimension of the whole label space of a multi-stage word. + +## 1. The model + +**Frames and steps.** Every register stands at a *frame*, a subspace of L, and changes frame by *steps*. A step +f → g is *nested* if f ⊆ g and a *drop* otherwise. It costs d(f, g) = dim f + dim g − 2 dim(f ∩ g), the rank of the +block (upstream's general frame lemma, Jacob Sussman's `frame_lemma` in the Lean repository; used as a black box and +only for prices, never in Theorems A and B). + +**Gates.** A gate is a free linear addition between registers that all stand at one common frame; each register +first reaches that frame by a step. + +**Data wires.** The source wire x_a starts at U_a. The target wire y_a starts at 0 and every frame it ever occupies +lies inside U_a^⊥. Helper registers ("slots") start at 0. These are the rules E0–E3 of `gx.check1` (see `gx/gx.py`): +`E1` labels (nested steps, equal frame at a gate, x: ⟨q⟩ → full, y: 0 → q^⊥, slots 0 → full), `E2` the scatter cut +(every y at frame 0 when the retained totals are copied), `E3` gate kinds, `E6` the block ledger. + +**Drop-free paths.** A contribution of x_T reaches a register w *drop-free* if there are registers +x_T = r₀, r₁, …, r_k = w and times 0 = t₀ < t₁ < … < t_k such that a gate at time t_i adds r_{i−1} into r_i, and +r_{i−1} takes only nested steps between t_{i−1} and t_i. (A drop of the *receiving* register before the gate does +not matter.) + +**Two semantics in which the statements are checked.** +1. `gx.check1` (gcert/1): the rules above, with the star scatter, plus the exact scalar identity E5. Checked on + three programs: the p = 3 toy (v = 8), the p = 10 complex program of PR #327 (v = 960) and Sussman's p = 11 + program of #193 (v = 1,320). All three are complex-side programs. +2. PR #425's mutable-basis semantics (jacklightChen): gates (adds and dyadic scalings) between registers at the + same current label, nested climbs except the eight centre copies (full → 0), source registers and target + registers may be modified and read, no target feeds a source or helper register, a frame-0 preconditioner + y ← V⁻¹(y − K s) and a cleanup of all source and helper registers at the full frame. The model above contains + this semantics (it never assumed immutable sources); §9 checks it on #425's own word. + +Not covered by any check here: the bit words (their checker is the community's paired-cube checker, not gcert/1), and +the Lean layer. + +## 2. Theorem A (content-frame invariant) [P][C] + +**Statement.** If a register w receives at time t a contribution of x_T along a drop-free path, then +frame(w, t′) ⊇ U_T for every t′ ≥ t until w's next drop. + +**Proof.** Induction along the path x_T = r₀, …, r_k = w of the definition. x_T starts at U_T and takes only nested +steps until t₁, so frame(x_T, t₁) ⊇ U_T. The gate at t₁ puts both registers at one frame F₁ = frame(x_T, t₁) ⊇ U_T, so +r₁ stands at F₁ ⊇ U_T after it. Between t_i and t_{i+1} the register r_i takes only nested steps, so its frame at +t_{i+1} still contains U_T, and the gate at t_{i+1} puts r_{i+1} at that frame. ∎ + +**Corollary A1.** If a drop-free path leads from x_T to y_S, then U_T ⊆ frame(y_S) ⊆ U_S^⊥, so U_T ⊥ U_S. This holds +for any number of hops, any gate kinds (x→x, y→y, s→s, x→y, s→y), any write order, any layout, and for recursive +invocations (a nested invocation is a sub-network; flatten it). + +**Corollary A2.** U_S is nondegenerate and nonzero, so U_S ⊄ U_S^⊥: no drop-free path leads from x_S to y_S. Every +route that delivers x_S to y_S passes a drop. + +**Check [C]** (`checks/certs.py`). Replay the gates of each program and carry, for every register, the set of +sources that reached it drop-free (the scatter, a drop, passes none). At every gate every newly received source port +must lie in the gate's frame (exact F₂ reduction). Result: 110 / 1,081,204 / 2,063,837 gate checks (p = 3 / 10 / 11), +0 violations. The final set of y_S is orthogonal to q_S, never contains S, and has size 4 / 620 / 884. Controls: +cyclically shifting the labels makes 12 of the lossless pairs of the p = 3 program non-orthogonal; corrupting one port +(odd weight kept) is rejected by `gx.check1` at E1 and gives 14 violations in the replay. + +## 3. Theorem B (stage additivity) [P] under hypotheses [U] + +**Rank lemma.** If V₀, …, V_s ⊆ L are pairwise orthogonal then Σ rk V_i ≤ m. +*Proof.* Let B be the list of the union of bases of the V_i (the V_i may overlap in isotropic vectors, so the list may +be dependent). Its Gram matrix is block diagonal with blocks Gram(basis of V_i), so its rank is Σ rk V_i. The Gram +matrix of a list is BᵀQB with B the m × |B| coordinate matrix, so its rank is at most m. ∎ + +**Setting.** Fix a pair a and the stages j = 1, …, s that run an invocation containing it, in time order. Let 𝒯_j be +the targets of stage j (all ports) and M_j = span{U_b : b ∈ 𝒯_j}. Let C_j be the span of the labels U_b of the +ports b that reach Y_a drop-free during stage j (the *correctors* of a; by Cor. A1 C_j ⊆ U_a^⊥). + +- (B1) *Target family.* There is a nondecreasing family of subspaces Ψ(t) with frame(Y_a, t) ⊆ Ψ(t) ⊆ U_a^⊥. (In a + layout with twin gates, Ψ is the frame of the wires tied to Y_a.) +- (B2) *Common cut.* There are times τ₁ < … < τ_s ≤ τ_{s+1} (the end) such that at τ_j every target b ∈ 𝒯_j stands at + the frame Ψ(τ_j), and all gates of stage j precede τ_{j+1}. + In `gx.check1` programs this is E2 (all y at frame 0 at the scatter). + +**Statement.** Put N_j = Ψ(τ_{j+1}) ∩ M_j. Then U_a, N₁, …, N_s are pairwise orthogonal, and C_j ⊆ N_j. Hence +k_a + Σ_j rk C_j ≤ m. + +**Proof.** (i) N_j ⊆ Ψ(τ_{j+1}) ⊆ U_a^⊥. (ii) For j < j′: N_j ⊆ Ψ(τ_{j+1}) ⊆ Ψ(τ_{j′}) by monotonicity, and by (B2) Ψ(τ_{j′}) +is the frame of every target b of stage j′, hence ⊆ U_b^⊥; so N_j ⊥ M_{j′} ⊇ N_{j′}. (iii) C_j ⊆ N_j: a corrector b of a in +stage j has U_b ⊆ frame(Y_a at its arrival) by Theorem A, which lies in Ψ(τ_{j+1}); and U_b ⊆ M_j. The rank of a +subspace is monotone (a principal submatrix has rank at most that of the matrix), so rk C_j ≤ rk N_j. The rank lemma +gives k_a + Σ rk N_j ≤ m. ∎ + +**Corollary B1.** Suppose in every stage the correctors of a span all of U_a^⊥ ∩ (window), of dimension h − 1; this +subspace is nondegenerate (complement of a nondegenerate line), so rk C_j = h − 1. Then +m ≥ 1 + s(h − 1). For the five-stage layout s = 5, for K-stage layouts with twin gates s = 2K + 1: +m ≥ 1 + (2K + 1)(h − 1). If the saving of a data wire is at most k, i.e. D ≤ N_data·k (the ledger of the five-stage +layout, D = 4kv − 5·cst [U]; read from upstream and not derived here), the saving fraction obeys +δ = D/(mW) ≤ (N_data/W)·k/(k + Σ_j rk C_j). + +**Measured neighbourhood ranks [C]** (`checks/certs.py`, `checks/families.py`, `checks/sat_e8.py`, +`checks/mutable425.py`): the span of the drop-free correctors of every target is exactly q^⊥, of dimension h − 1: + +| family | h | ports | correctors per target | rank | +|---|---|---|---|---| +| complex p = 10 (#327) | 20 | 960 | 620 | 19 | +| complex p = 11 (#193) | 22 | 1,320 | 884 | 21 | +| bit, paired cube p = 4, 5, 10, 11 (ℚ, x ↦ xᵀ(I − J/9)y) | 8, 10, 20, 22 | 32 … 1,320 | 15, 39, 339, 435 | 7, 9, 19, 21 | +| E8 bit dual (ℚ⁸, E8 form) | 8 | 120 | 63 | 7 | +| E8 complex (unique h = 9 labelling, §6) | 9 | 120 | 56 | 8 | +| #425's word, final lossless set of each target | 9 | 120 | | 8 | + +The complex p = 10, 11 rows and the #425 row are replayed drop-free correctors (final taint of every target). The bit +and E8 rows are the in-cap neighbourhoods of the family, not replayed correctors: for the paired cube `paired_bit` +computes port 0 only (the automorphism group of the paired cube is transitive on ports, not checked here), for E8 every +line is computed. + +The p = 3 program is degenerate (its ports span a 4-dimensional subspace of F₂⁶; rank 3 ≠ h − 1 = 5) and is not used +for Theorem B. + +Bounds from Cor. B1, against the widths in use: m ≥ 96 / 134 / 172 (p = 10, s = 5 / 7 / 9) against 100 / 140 / 180; +106 (p = 11, s = 5) against 110; 36 (E8 bit dual, s = 5) against 40. For E8 complex at s = 9 the bound is +1 + 9·8 = 73, and **#425's word has m = 73** (the `m` of its report): Theorem B is attained. For the E8 bit dual at +s = 9 the bound is 64; the width of #386 is 64 (reported in #386, not checked here). + +**What (B1)–(B2) are in a layout [U].** In the five-stage layout of Sussman's repository at f010392c +(`Work/Bridge/Net.lean`, `Work/BridgeGeom/Stage.lean`, `Work/BridgeGeom/Net.lean`) the target family of a pair is tied +across the 2K + 1 stages by twin gates, and every stage has a common cut. These facts were read from those files; their +consistency with (B1)–(B2) is not formally verified (see §12). #425's nine-stage word satisfies (B2) at its +scatter (all 120 targets stand at frame 0 at the cut, checked in §9). + +**What Theorem B does not bound.** It bounds m below by a function of the neighbourhood rank. It says nothing about the +helper count R, and nothing about a port family whose correctors span less than q^⊥. + +## 4. Theorem C (drop pricing) [P][C] + +**Statement.** Let a retained total be gathered drop-free from sources P, with root frame f ⊇ V := Σ_{T∈P} U_T +(Theorem A). Its content is delivered to readers Q through a rooted tree of arrays: each non-root array is a copy +taken by a gate at its parent's current frame, and every array may take any steps (drops and climbs, degenerate +frames included). Every reader b reads at a frame ⊆ U_b^⊥. Then the total cost of the drops in the tree is at least +rk(V × U(Q)) = dim V − dim(V ∩ U(Q)^⊥), the rank of the pairing V × U(Q) → F, with U(Q) = Σ_{b∈Q} U_b. + +**Proof.** Attach to every array e a *survivor* S_e ⊆ V, defined along time: at the root S = V; a nested step leaves +S unchanged; a drop f_e → g_e replaces S by S ∩ g_e; a copy starts with the survivor of its parent at the copy time. +By induction S ⊆ frame(e) at all times (at the root V ⊆ f; a nested step enlarges the frame; after a drop S ⊆ g_e; +a copy stands at the parent's frame). A drop costs d(f_e, g_e) ≥ dim f_e − dim(f_e ∩ g_e) ≥ dim S − dim(S ∩ g_e), +because S ⊆ f_e and the map S → f_e/(f_e ∩ g_e) has kernel S ∩ g_e. + +Let a reader b read array e at time t. Its common frame F_b with e lies in U_b^⊥ and contains S_e(t); write S_b = S_e(t), +so S_b ⊥ U_b. For an array e define σ(e) as its survivor at creation and ρ(e) as the intersection of the S_b over +all readers in the subtree of e (ρ(e) = σ(e) if there are none). Claim: cost(subtree of e) ≥ dim σ(e) − dim ρ(e). +Induct over the tree. Along e the survivors form a decreasing chain S₀ = σ(e) ⊇ S₁ ⊇ … ⊇ S_last; e's own drops cost at +least dim S₀ − dim S_last. A child c_i created when the survivor is S(i) ⊇ S_last has cost ≥ dim S(i) − dim ρ(c_i), with +ρ(c_i) ⊆ S(i). Direct readers see survivors ⊇ S_last. Then ρ(e) ⊇ S_last ∩ ⋂ρ(c_i), and the codimension of S_last ∩ ρ(c_i) in +S_last is at most that of ρ(c_i) in S(i); so dim ρ(e) ≥ dim S_last − Σ(dim S(i) − dim ρ(c_i)). Adding up gives the claim. +At the root, ρ ⊆ V ∩ ⋂_b U_b^⊥ = V ∩ U(Q)^⊥. ∎ + +**Corollary C1 (read discipline is worthless when the readers span the window).** If U(Q) is the whole nondegenerate +window then V ∩ U(Q)^⊥ = 0 and the bound is dim V: splitting the readers into classes, reading at nonzero frames, +climbing copies, or any tree is never cheaper than one copy dropped from f to 0 when f = V. The bound is subadditive over +column blocks: rk(V × ΣU(Q_i)) ≤ Σ rk(V × U(Q_i)). + +**Equality [C].** In all three gcert/1 programs every retained total has frame f = V, and the readers (all ports) +span the window, so the star copy meets the bound: p = 10: 20 totals × 18 = 360 = cst; p = 11: 440 = cst. On #425's word +each of the eight centres gathers 57 sources (the drop-free taint before the cut, equal to the support of its root-line +coordinate), which span F₂⁹; the pairing ranks are 9 each, 72 in total, equal to the frames paid (8 × 9). For the E8 bit-dual +decoder M = UUᵀ (9 totals, each read by the 56 ports of its bit, rank_ℚ of the Gram block = 8) the package computes only the +bound, 72; it equals the copy loss #370 reports (nine retained totals at the full frame), which is not replayed here. +For the p = 3 program the port span is degenerate: the bound is 12 and the paid cost 18. + +**The one gain (p = 3 toy) [C]** (`checks/toy.py`). The ports of the p = 3 program span W of dimension 4 with W^⊥ ⊆ W +(radical of dimension 2, nonzero vectors 001111, 110011, 111100). Allow the scatter in cuts; at a cut all y stand at +one common frame g ⊆ ⋂ q^⊥ = W^⊥, copy k costs d(f_k, g), and the cut frames form a chain. Cut 1 at g = 0 for the totals +2–5, the y climb to l = 111100, cut 2 at g = ⟨l⟩ for the totals 0, 1. Result: cst 18 → 16, moves 194 → 192, every +register chain nested, equal frames at every gate, every y inside q^⊥ and avoiding q, block mass R·h + 2v(h − 1), +and `gx.scal` passes (gates and coefficients unchanged). An exhaustive search over all chains of cut frames in W^⊥ +gives optimum 16 (the old format: 18). Control: a common frame outside the radical puts some target outside its q^⊥. +The gain needs W^⊥ ≠ 0, a degenerate port span. In the p = 10 and p = 11 programs (and every family above) the ports +span the nondegenerate window (`window_rank = h`), so g = 0 is forced and the gain is 0. + +## 5. The clique bound [P][C] + +**Statement.** Let K be a set of ports such that for all T ≠ S in K there is a drop-free path from x_T to y_S. Then the +U_T (T ∈ K) are pairwise orthogonal and nondegenerate, so they form an orthogonal direct sum and +Σ_{T∈K} k_T ≤ r, where r is the dimension of the window that contains the labels. If H is the graph of ports joined +by a drop-free route, k_T = k for all T, then k·ω(H) ≤ r. + +**Proof.** Corollary A1 gives pairwise orthogonality; each U_T is nondegenerate, so U_T ∩ Σ_{S≠T} U_S ⊆ U_T ∩ U_T^⊥ = 0. ∎ +The statement is independent of the field, the form and any symmetry of the labels. + +**In the five-stage ledger** (D = 4kv − 5·cst, W = 4v + R, m = 5h): δ = D/(mW) < k/(5h) ≤ 1/(5ω(H)). + +**Instances [C]** (`checks/families.py`, `checks/sat_e8.py`; ω of the in-cap graph of the paired cube, exact maximum +clique): bit side (|S ∩ T| = 1) ω = p for p = 4, 5, 6, 7; complex side (|S ∩ T| ∈ {0, 2}) ω = 8, 8, 12, 12 for p = 4, 5, 6, 7. +For p = 10 complex, 20 ports (five pairwise disjoint transversal 4-sets from the K₅ stars, all four triples each) are +pairwise orthogonal with q·q = 1 and every pair of them is a drop-free pair inside the #327 program itself, so +Σ k_T ≤ 20 = h and k = 1. The E8 in-cap graph (3,360 edges, degree 56) has ω = 8 (8,640 maximal 8-cliques, each an +orthonormal basis): k = 1 needs r ≥ 8, k = 2 needs r ≥ 16 by the bound alone and r ≥ 18 by §6. + +On the bit side ω = p = h/2, so the bound allows k = 2 at r = h; it says nothing against k = 2 there. + +## 6. Labels on the E8 in-cap graph: exact SAT results [C] + +Setting (`checks/sat_e8.py`; CaDiCaL 1.5.3 (`Cadical153`, uniqueness) and 1.9.5 (`cadical195`, planes) through python-sat 1.9.dev15). H is the graph on the 120 E8 root lines +(Hamming coordinates of #370) joining lines with ⟨a, b⟩ = ±1. A *k-dimensional labelling in dimension r* assigns +to every line a nondegenerate k-dimensional subspace A_T of (F₂^r, dot product), with A_S ⊥ A_T on every edge. +By Cor. A1 these are the labels of any word in which H is realised by drop-free correctors. + +**Reduction.** Fix an 8-clique C of H (§5). Its labels are pairwise orthogonal and nondegenerate, hence an +orthogonal direct sum. The window dimension is r ≤ 17, so the complement of the span of C has dimension at most 1 +(k = 2: r − 16) or r − 8 ≤ 1 (k = 1, r ∈ {8, 9}), and is absent or I₁. +- k = 1: the labels are orthonormal; as F₂^r = ⟨C⟩ ⊕ ⟨C⟩^⊥ with ⟨C⟩ of dimension 8 and ⟨C⟩^⊥ absent (r = 8) or a nondegenerate + line ⟨w⟩ with w·w = 1 (r = 9), an isometry of (F₂^r, ·) maps them to e₁, …, e₈. Every other line T has A_T orthogonal to the blocks of the clique members adjacent + to T, i.e. supported on the blocks of the non-adjacent members and on the complement coordinates. +- k = 2: each plane of C is either I₂ (p·p = q·q = 1, p·q = 0) or the hyperbolic plane (every nondegenerate symmetric + plane over F₂ is one of the two); for r = 16 the 8 planes are the whole space, so not all can be hyperbolic (that form + is alternating, the dot product is not); for r = 17 the complement is I₁. Non-clique planes are free of type. + The SAT instance enumerates all 2⁸ type patterns of the clique (255 for r = 16). + +**6.1 Uniqueness at h = 9.** The CNF has the 9 coordinates of every line, u·u = 1, orthogonality on H, and injectivity +of the labels (E0 of `gx.check1`). Enumerated to exhaustion: **exactly one solution** (blocking clause after the first +solution is UNSAT). It is checked independently of the CNF: u·u = 1, orthogonal on all 3,360 edges, injective, and +u_a·u_b = 1 on all 3,780 E8-orthogonal pairs, which is the Gram matrix of Sussman's E8 complex unit (decoder +M = J + (G mod 2)). So every h = 9 labelling of H is, up to an isometry of F₂⁹, Sussman's. Its correctors span rank 8 +for every line. #425's ports satisfy exactly this Gram relation with the word's own root lines (all 120 × 120 entries), +so #425 uses that labelling. Control: the same CNF with h = 8 is UNSAT. + +**6.2 Planes (k = 2).** **UNSAT for r = 16 (255 patterns) and r = 17 (256 patterns).** A labelling in dimension r ≤ 17 +would embed in dimension 17 by padding with zero coordinates (the dot product of F₂^{r+1} restricts to that of F₂^r), so +there is no k = 2 labelling of H in any dimension r ≤ 17: k = 2 needs r ≥ 18. Dimension 18 is attained by the direct sum +of two copies of the 9-dimensional labelling (A_T = ⟨(u_T, 0), (0, u_T)⟩), a split labelling. Controls: the k = 1 +encoder at r = 8 is UNSAT and at r = 9 SAT (rank 9); the k = 2 encoder at r = 18 accepts the direct sum (SAT under the +assumptions that fix it), so the UNSAT results are not an artefact of the encoding. + +This closes the labelling lever only for the **full E8 in-cap graph**: it says nothing about subgraphs, other +decoders or other port sets. + +## 7. Fixed-role B₂ windows: Theorem P [P][C], with its exact scope + +**Scope.** Theorem P concerns layouts in which one helper set runs the same program on the same slots in every stage +and the stage windows are transports of one window (the fixed-role windows of the five-stage layout B₂ of Sussman's +repository, as read). It is stated for F₂ dot-product windows and checked on the complex gcert/1 programs of #327 +(p = 10) and #193 (p = 11) only, and it is **not a general obstruction**. **Compressed windows circumvent it**: #425's +nine-stage complex word has m = 73 = 1 + 9·8 (checked in §9), which attains the width bound of Theorem B and lies below +the s·h = 81 that Theorem P forces for a fixed-role complex layout whose program's slot-carried pairs span, so its +windows do not satisfy (P1)–(P2) together with a spanning program. PR #386's nine-stage bit word (reported m = 64 = +1 + 9·7, h = 8) has a ℚ form; Theorem P is not stated or checked for ℚ forms and nothing is claimed about whether +the analogue would force 72 there. + +**Hypotheses [U].** (P1) Stage j runs the program c on the window W_j = ι_j(F₂^h), where ι_j : (F₂^h, ·) → L is an +isometric embedding (so W_j is nondegenerate of dimension h); in stage j the source T starts at ι_j(⟨q_T⟩) and every +frame of y_S during stage j lies in ι_j(q_S)^⊥. (P2) One helper set runs the *same* program on the *same* slots in +every stage, and slots never drop (nested steps only). Both are read from the layout, not re-derived here. + +**Statement.** For stages j < j′ let K = ι_jᵀι_j′ (h × h over F₂). Let the *slot-carried pairs* be the pairs (T, S) such +that T is in the final set of sources that reached some slot z drop-free in the program and z writes the target y_S. +If the tensors q_T ⊗ q_S over the slot-carried pairs span F₂^{h×h}, then K = 0. Consequently W₁, …, W_s are pairwise +orthogonal, nondegenerate, and m ≥ s·h. + +**Proof.** After stage j the slot z stands at a frame containing ι_j(q_T) for every such T (Theorem A in stage j) and it +never drops. In stage j′ it writes y_S at a frame inside ι_j′(q_S)^⊥ (P1). So ⟨ι_j q_T, ι_j′ q_S⟩ = q_Tᵀ K q_S = 0 for +every slot-carried pair. This is linear in K; if the q_T ⊗ q_S span, K = 0. Pairwise orthogonal nondegenerate +subspaces form a direct sum. ∎ + +**Check [C]** (`checks/pivots.py`). The pairs with q_T·q_S = 0 alone span a space of dimension h² − 1 (their tensors lie +in the hyperplane tr M = Σ M_ii = q_T·q_S = 0; this leaves K = λI), and the full set of slot-carried pairs spans h²: +399 / 400 on the #327 program (3,708 writer slots) and 483 / 484 on #193 (4,125 writer slots). So K = 0; a +slot-carried pair with q_T·q_S = 1 is what excludes K = λI, i.e. two stages with identified windows. By Cor. A1 such a +pair cannot be drop-free within one stage, so T necessarily reached the slot only after the slot wrote y_S. + +A shorter route to K = 0 exists under (P1)–(P2) and rule E1 of `gx.check1` (every slot ends a stage at the full window): +the frame of a slot in stage j′ contains ι_j(F₂^h), so ι_j(F₂^h) ⊥ ι_j′(q_S) for every slot-written S, and the ports of the +slot-written targets span F₂^h (rank 20 and 22, checked). The taint computation above proves the stronger version that +needs only the frames actually reached by taint, so the rank 399/400 should not be overweighted. + +**What the exact part gives, and what is priced [M]** (`checks/pricing.py`, pricer `inputs/pricing/cost.py`, histogram of +#325's p = 10 bit word, pinned root reproduced). If the 2K block pivots were free (m = 1 + 5(h − 1) = 96 instead of +100: each helper wire loses 4 levels, the pair-1 end idle block 2h + 2 → 2h − 2, the pair-2 end idle block of rank 4 +disappears), the saving of the p = 10 bit word would be larger by +3.56 % to +8.11 %, depending on which helper blocks +shrink (largest blocks / mid blocks / 2 → 1 / rank-1 blocks removed: +3.56, +5.75, +6.39, +8.11), and by +1.53, +3.68, ++4.30, +5.99 with 40 extra copy ranks per unit (below). The saving would be unavailable to fixed-role B₂ windows if the +analogue of Theorem P holds for the bit word's programs; that is **not claimed**, since Theorem P is stated and was +computed on complex F₂ programs only and no bit certificate was replayed. Nothing here concerns compressed windows. + +**Measurements for one overlap [C][model]** (`checks/pivots.py`). Suppose two stage windows of a *shared-helper* layout +overlap in one direction w = ι_{j−1}(e) = ι_j(e′) with e·e = e′·e′ = 1. A retained total whose frame is not inside e^⊥ +carries w into stage j and, in the model, pays one extra copy rank there unless e′ lies in its frame. Over all +odd a, b ∈ F₂²⁰ and the 20 retained totals of the #327 program (frames of dimension 18): at most 1 total has a frame +inside a^⊥ and at most 9 frames contain b, so ≥ 20 − 1 − 9 = **10 forced extra copy ranks per overlap**. On the helper +side, for each of the 1,160 candidate directions tried (the 20 unit vectors and the 1,140 weight-3 vectors) at least +5,984 of the 6,515 slots end at a frame not inside e^⊥, and the forward closure of those slots through the gates +contains all 8,435 registers and all 960 targets (their ports have rank 20, so no e′ ⊥ all of them exists). These are +counts in a stated model for one program with shared slots; they say nothing about layouts whose helpers are organised +differently. + +## 8. Non-nested steps on registers [P][M] + +**Proposition N [P].** A register whose chain runs from f₀ to f_end with nested steps except one non-nested step f → g +has total mass (dim f_end − dim f₀) + 2r with r = dim f − dim(f ∩ g). *Proof.* The step costs d(f, g) = r + r′ with +r′ = dim g − dim(f ∩ g); the nested steps cost (dim f − dim f₀) + (dim f_end − dim g); and dim f − dim g = r − r′. ∎ +So a descent of rank r on a register that must still reach its sink costs 2r more than a nested chain with the same +endpoints. A copy of rank r is charged r by the ledger (`gx.check1`: N + tails = R·h + 2v(h − 1) + cst, with the copy +blocks H["c"][dim f] in `cst`). + +By Theorem C the drops that carry a total to its readers cost at least rk(V × U(Q)) however they are arranged, and the +star copy attains it on every family checked; a register descent pays that and then the re-climb. + +**Pricing [M]** (same pricer and histogram as §7). One rank-1 copy in each of the five stages, per 12-normalised unit, +is 60 extra blocks of rank 1 (5 × 12): **−0.2457 %**. One rank-1 register descent in each of the five stages is one +non-nested step of rank d = 2 per stage, 60 extra blocks of rank 2: **−0.4911 %**. Quote ≈ −0.49 %: other blockings of +the same mass give −0.4906 % to −0.4914 % (two rank-1 blocks: −0.4914 %), so the fourth digit is a modelling choice. + +**Two-level words.** A word whose gates are small verified words flattens to a nested-frame network; Theorems A–C apply +to the flattened network unchanged. + +## 9. PR #425's mutable-basis word: Theorems A–C and Theorem S [C][P] + +Input: `inputs/pr425/FULL-WORD.json.gz`, #425's `FULL-WORD.json.gz` (920 registers: 120 sources, 120 targets, +680 helpers; m = 73, h = 9), regenerated with #425's own `hamming_packets.py` and `hamming_full.py` under Python 3.12; +its sha256 equals the one in #425's `EXPECTED.json`. + +**Replay [C]** (`checks/mutable425.py`, the same frame and taint detector as §2). 0 violations of: nested climbs, +common frame at every gate, taint of both gate registers inside the gate frame (Theorem A), target frames inside +q^⊥, target taint orthogonal to its port (Cor. A1), no target feeding a source or helper register. All 120 targets stand at +frame 0 at the scatter ((B2)), and the final lossless set of every target has rank 8 = h − 1 (Theorem B: m ≥ 1 + 9·8 = 73 += m of the word). On the eight centre copies the pairing-rank bound (Theorem C) is 72 and the frames paid are 72. The +same detector in *immutable-source / no-target-read* mode flags 1,640 modifications of sources and 112 reads of +targets in the word as written. Exact scalar replay over ℚ: the helpers and sources are restored, J = I, and with the +frame-0 preconditioner y ← V⁻¹(y − K s) the word is exactly (x, s, y) ↦ (x, s, y + x); omitting the K part is rejected. + +**Theorem S (simulation) [P].** *Hypotheses.* Let 𝒲 be a word with (H1) nested climbs and common-frame gates and +invertible scalings; (H2) no gate has a target as source and a source or helper as destination; (H3) after a frame-0 +preconditioner y ← V⁻¹(y − K s) it acts as (x, s, y) ↦ (x, s, y + x). Let b_x be the number of source registers that are +destinations of some gate and b_y the number of targets that are sources of some gate. +*Statement.* There is a word 𝒲′ with R + b_x + b_y helper registers in which no source is modified and no target is read, +with the same frames at the corresponding gates, that acts as (x, s, g, y) ↦ (x, s, g, y + x) after a frame-0 preconditioner. +*Proof.* For each modified source r add a helper g_r and a gate g_r += x_r at frame ⟨q_r⟩ (g_r climbs from 0, x_r +is already there). For each read target t add a helper g_t, starting at frame 0. Rename every occurrence of x_r and y_t +in every event of 𝒲 to g_r and g_t. Then g_r and g_t follow the frame sequences of x_r and y_t, so every gate has the +frames it had; the real x_r are never modified and the real y_t (t read) never read. After the last event add y_t += g_t +at the frame q_t^⊥ (g_t is inside it, as y_t was). Finally undo, at the full frame and in reverse order, every renamed event +whose destination is not a real target, and add g_r −= x_r. By (H2) these events read, in 𝒲′, only source registers and +helpers (the g's are helpers), so the reverse sequence restores every source and helper register exactly, whatever the +targets hold. Every real target then ends at y_t + (J x)_t + ℓ_t(s, γ), where γ is the initial dirt of the g's and ℓ_t is +linear (it collects the V and K responses, including those that unread targets receive from renamed g_u); the +coefficients of x are those of 𝒲, so J = I. The dirty registers (s and g) stand at frame 0 at the start, so the +preconditioner y ← y − ℓ(s, γ) removes all such terms. ∎ + +*Consequence.* Relative to its own simulation in the immutable-source / no-target-read format, the mutable-basis format +saves at most b_x + b_y ≤ 2v helper registers (at most one per source and one per target). It bounds the helper +count of the simulation, not its price. + +**Check [C].** On #425's word b_x = b_y = 112; the simulation has 904 = 680 + 112 + 112 helpers. The same detector finds 0 +violations in it (immutable mode), z is restored exactly, and after the frame-0 compensation the map is exactly +(x, s, y) ↦ (x, s, y + x); without the compensation it is not. Under the coarse formula of #425's `hamming_full.py` +(reproduced: b = 1.049105 × 10⁻³ for #425's word) the simulation has b = 9.102 × 10⁻⁴ (−13.24 %), below the pre-#425 +word (9.994 × 10⁻⁴). The simulation was not run through `gx.check1`; it was replayed by the detector above. + +## 10. What the theorems bound, and what they do not + +Theorems A–C and the clique bound bound three things: the label dimension k (for a given in-cap graph), the width m +(Theorem B, for a given corrector rank) and the copy rank (Theorem C, for given source and reader spans). **They do not +bound the helper count R, nor the idle and stock costs (the block profile of the helpers),** which is where PR #425 +(mutable-basis packets), #433 (split centres) and #442 gained. #425 keeps m at the Theorem B width and the copy rank at +the Theorem C bound (checked in §9); #433 and #442 are not replayed here. The only family-dependent term in Theorem B is the rank of the +corrector span; it equals h − 1 in every family above, and a family with a smaller rank and a cheap decoder would +change the width bound. + +## 11. Statement → check + +| statement | check (module, function) | pinned facts in `expected.json` | +|---|---|---| +| gx.check1, Thm A, Cor A1/A2, Thm B data, Thm C on three programs | `certs.stage` | `certificates` | +| negative controls (shifted labels, corrupted port) | `certs.controls` | `certificates.p3.controls` | +| toy: 18 → 16, exhaustive optimum, control | `toy.run` | `toy_p3` | +| Theorem P | `pivots.thm_P` | `pivots.thm_P` | +| overlap measurements | `pivots.copy_count`, `pivots.overlap_scan` | `pivots` | +| #425: replay, scalar, Theorem S, controls | `mutable425.run` | `mutable_425` | +| pricing, pivot-free variants, copy/descent units | `pricing.run` | `pricing` | +| neighbourhood ranks, E8 bit dual, ω, 20-clique | `families.*` | `families`, `thmB_table` | +| h = 9 uniqueness, k = 2 planes, calibrations | `sat_e8.*` | `e8_labels` | + +## 12. Scope and open points + +- The correspondence between the model of §1 and each checker is by reading `gx.py` (E0–E7) and #425's `PROOF.txt` §3; + there is no mechanical proof of it and no Lean check. +- (B1)–(B2) and (P1)–(P2) are hypotheses about the layout [U]. +- Theorem P holds for fixed-role B₂ windows only (§7) and is computed on complex programs; the bit words are not replayed. +- The simulation of Theorem S is checked on #425's word only. +- `inputs/pricing/hist_p10b.json` is a copy of the five-stage histogram that #325's verification writes to `math.json` (a + run output at head 0eca9340, not a committed file; its `bit_root` is the pinned root the pricer reproduces). It was not + re-derived from #325's records here. +- Lean: (P1)–(P2) and (B1)–(B2) were read against `Work/Bridge/Net.lean`, `Work/BridgeGeom/Stage.lean` and + `Work/BridgeGeom/Net.lean` (f010392c); the docstrings and lemma statements are consistent with them, but this is not + formally verified. Two points are open: whether the backward stages 1 and 3 count as "the same program", and whether the + stage-j target frames lie in ι_j(q_S)^⊥. +- `inputs/gcert1-p3-cone-R16.json` is a local research program (not published upstream). diff --git a/research/format-obstructions/README.md b/research/format-obstructions/README.md new file mode 100644 index 0000000000..c70124ee07 --- /dev/null +++ b/research/format-obstructions/README.md @@ -0,0 +1,96 @@ +# format-obstructions + +**Exact bounds on window width, copy cost and label dimension (no new κ).** This package states and proves three +theorems about frames and gates (A: drop-free contributions force orthogonal labels; B: stage windows add up; C: a drop +that reaches the readers costs the pairing rank), a clique bound on the label dimension, and a simulation theorem for +PR #425's mutable-basis words (S). Everything that can be checked exactly is checked by one offline driver on pinned +inputs: Sussman's `gx.check1` programs, #425's own word, and exact SAT instances on the E8 in-cap graph. +[PROOF.md](PROOF.md) has the statements, the proofs and the scope of each. + +## Scope + +- **Model.** Registers stand at frames (subspaces of a label space), climb by nested steps, drop at a price + d(f, g), and gates add registers that stand at one common frame. Sources start at their label, targets stay inside + their label's orthogonal. This is the content of the rules E0–E3 of `gx.check1` and of the common-label rule of + #425's conjugation lemma. +- **Checked semantics.** `gx.check1` (gcert/1, vendored unchanged from Jacob Sussman) on three programs: the p = 3 toy, + the p = 10 complex program of #327 and the p = 11 program of #193; and #425's mutable-basis semantics on its own + 920-register word. +- **Not covered.** No bit word is replayed (the bit words use the community's paired-cube checker). No Lean. The multi-stage + statements use hypotheses about the layout that are read from upstream, not re-derived: (B1)–(B2) of Theorem B and + (P1)–(P2) of Theorem P (PROOF.md §3, §7). + +## Results + +| | statement | status | +|---|---|---| +| **Thm A** | A contribution of x_T that reaches a register by a drop-free path forces the register's frame to contain U_T. So a lossless x_T → y_S route needs U_T ⊥ U_S, and there is no lossless x_S → y_S route. | proved; replay of every gate of three programs, 0 violations (1.08 M and 2.06 M gate checks at p = 10, 11) | +| **Thm B** | For a pair a with stages j = 1..s: k_a + Σ_j rk C_j ≤ m (C_j = span of the labels of a's correctors in stage j). With corrector rank h − 1 this gives m ≥ 1 + s(h − 1). | proved under the layout hypotheses (B1)–(B2); rank h − 1 measured on the p = 10, 11 complex programs, the bit paired cubes p = 4, 5, 10, 11, the E8 bit dual (7) and the E8 complex labelling (8); #425's word has m = 73 = 1 + 9·8, so the bound is attained | +| **Thm C** | The drops that carry a total gathered from sources P to readers Q cost at least rk(U(P) × U(Q)), whatever the tree of copies, frames and drops. | proved; the star copy meets it exactly on the p = 10 (360), p = 11 (440) programs, on #425's centres (72, 57 gathered sources per centre). For the E8 bit dual the package computes the bound 72, which equals the copy loss #370 reports (not replayed) | +| **Toy** | The p = 3 program (degenerate port span) admits a split scatter, cst 18 → 16 (exhaustive optimum 16). | exact; gain needs a degenerate port span, 0 on the nondegenerate families | +| **Clique bound** | If every pair in a set K has a drop-free route, the labels on K are orthogonal and nondegenerate: Σ_K k_T ≤ r. | proved; ω = p (bit) and 8, 8, 12, 12 (complex, p = 4..7); 20 ports pairwise lossless inside the p = 10 program, so k = 1; ω = 8 on the E8 in-cap graph | +| **E8 labels** | The h = 9 labelling of the E8 in-cap graph is unique (Sussman's). No k = 2 labelling exists in dimension r ≤ 17 (r = 16: 255 plane-type patterns, r = 17: 256, all UNSAT). | exact SAT (CaDiCaL) with calibrations and a positive control; for the full in-cap graph only | +| **Thm P** | For **fixed-role B₂ windows over F₂** (one helper set, same program, same slots in every stage, slot-carried pairs spanning) the cross-Gram of two stage windows is zero, so m ≥ s·h. | proved under (P1)–(P2); computed on the complex p = 10 and #193 programs only (399/400 and 483/484). **Compressed windows circumvent it**: #425's nine-stage complex word has m = 73 = 1 + 9·8 < 81, at the Theorem B bound. #386's bit word (m = 64) has a ℚ form; Theorem P is not claimed for it. Not a general obstruction. | +| **Prop. N** | A non-nested step of rank r on a register that must still reach its sink costs 2r over the nested chain; a copy of rank r is charged r. | proved; pricing context for the p = 10 bit word: ≈ −0.49 % for a rank-1 register descent in each of the five stages (the fourth digit is a modelling choice) against −0.2457 % for a rank-1 copy in each stage | +| **Thm S** | A mutable-basis word with b_x modified sources and b_y read targets is simulated, in the immutable-source / no-target-read format, with R + b_x + b_y helpers. | proved; exact on #425's word (680 + 112 + 112 = 904), with controls. A bound on helper count, not on price. | +| #425 | Thms A and C and the clique bound hold on #425's word, and its width attains Theorem B. | replay: 0 violations, centre copies 72 = 72 (57 gathered sources per centre), all 120 targets at frame 0 at the cut, rank 8 for every target | + +## What this means for the swarm + +A–C and the clique bound bound **m and the copy rank**, the label dimension for a given in-cap graph, and (through the +five-stage ledger D ≤ N_data·k, read from upstream) **D**. They do +**not** bound the helper count R, nor the idle and stock costs (the block profile of the helpers), which is where +#425, #433 and #442 gained (#425, the one replayed here, keeps m at the Theorem B width and the copy rank at the +Theorem C bound). In the +formats covered here a further κ gain therefore has to come from R or the stock, or from a new port family whose +corrector rank is below h − 1 with a cheap decoder (the only family-dependent term of Theorem B). Nothing here is +a statement about the size of R. + +## Verify + + python -m pip install -r research/format-obstructions/requirements.txt # python-sat 1.9.dev15, networkx 3.7, mpmath 1.3.0, numpy 2.3.5 + python3 -B research/format-obstructions/verify.py --output /tmp/format-obstructions-out # Python 3.11+, tested 3.12 + +No network; `-O` is refused. The driver checks the sha256 pins of `SOURCE.json`, runs 91 independent tasks in a +process pool (`--jobs N`, default the core count), compares the facts with `expected.json`, and requires an unchanged +tree. Runtime: about 90 s wall on 12 cores, about 15 CPU-minutes in total (the CaDiCaL instances are 70 % of it). +It runs: + +- `gx.check1` (with the exact scalar identity) on the three programs; the taint replay of Theorem A at every gate; + Cor. A1, the corrector ranks of Theorem B and the copy bounds of Theorem C; +- the p = 3 toy (nestedness, equal frames, scalar half, exhaustive optimum); +- Theorem P (rank of the cross-Gram constraints), the forced-copy count and the contamination scan; +- #425's word: frame and taint replay, scalar identity over ℚ, the Theorem S conversion and its replay; +- the pinned pricer on the p = 10 bit histogram (root, pivot-free variants, copy and descent units); +- the neighbourhood ranks, the E8 bit-dual decoder, the clique numbers, the 20-clique; +- the SAT checks: uniqueness at h = 9, k = 2 at r = 16 and 17. + +**Negative controls.** Shifted labels (12 non-orthogonal lossless pairs) and a corrupted port (`gx.check1` rejects it at +E1; 14 replay violations); a toy cut frame outside the radical; the immutable/no-target-read detector flags 1,640 +source modifications and 112 target reads on #425's word as written and 0 on the converted word; omitting the K part +of #425's preconditioner and the compensation of the converted word are rejected; k = 1 at r = 8 UNSAT and r = 9 SAT, +h = 8 UNSAT, and the k = 2 encoder at r = 18 accepts the direct sum of two k = 1 solutions. + +## Not checked, or checked only in part + +- The bit side: Theorem P (stated for F₂ windows) and the copy/overlap measurements were computed on complex programs; + the pricing context uses the p = 10 bit histogram. No bit certificate is replayed, and nothing is claimed about + Theorem P for ℚ forms. The bit and E8 rows of the Theorem B table are in-cap neighbourhoods of the family, not replayed + correctors. +- The layout hypotheses (B1)–(B2), (P1)–(P2) and the width m = 64 (#386) are taken from upstream. They were read against + Sussman's `Work/Bridge/Net.lean`, `Work/BridgeGeom/Stage.lean` and `Work/BridgeGeom/Net.lean` (f010392c), whose + statements are consistent with them; **this was read, not formally verified.** Two points are open: whether the + backward stages 1 and 3 count as "the same program", and whether the stage-j target frames lie in ι_j(q_S)^⊥. +- The Theorem S simulation was replayed by the detector of `checks/mutable425.py`, not by `gx.check1`. +- `inputs/pricing/hist_p10b.json` is a copy of the five-stage histogram that #325's verification writes to `math.json` (a + run output at head 0eca9340, not a committed file); the pricing numbers are pricer-model outputs for the p = 10 bit + word, not theorems. +- The overlap measurements are for one program and 1,160 candidate directions. +- `inputs/gcert1-p3-cone-R16.json` is a local research program that is not published upstream. + +## Files + +`verify.py`, `expected.json`, `SOURCE.json`, `requirements.txt`, `PROOF.md`, `NOTICE`; `checks/` (`certs.py`, `toy.py`, +`pivots.py`, `mutable425.py`, `pricing.py`, `families.py`, `sat_e8.py`, `e8lib.py`, `f2.py`); `gx/gx.py` (Sussman, +unchanged); `inputs/` (three gcert/1 programs, `pr425/FULL-WORD.json.gz`, `pricing/cost.py`, `pricing/hist_p10b.json`). +`.github/workflows/format-obstructions.yml` runs the driver on Python 3.12. diff --git a/research/format-obstructions/SOURCE.json b/research/format-obstructions/SOURCE.json new file mode 100644 index 0000000000..bf19b313c9 --- /dev/null +++ b/research/format-obstructions/SOURCE.json @@ -0,0 +1,12 @@ +{ + "description": "Pinned inputs of research/format-obstructions (sha256). Vendored byte for byte; nothing is fetched at run time.", + "files": { + "gx/gx.py": "6f3dc8bb639933227a8dae181ec4a542e85c7276be9c9e330f49518e7b630b95", + "inputs/gcert1-p3-cone-R16.json": "fe3ad604eec43845747603414222fc6a82ed16168ef64909440c0a72eba97dc9", + "inputs/gcert1-p10-anneal-mw-flow.json.gz": "117d1cf1ad9c0ab3fac42557cf4aa4f7166700e8c005eb3f928b187544f23f49", + "inputs/gcert1-p11-pr193.json.gz": "15251deb0c11e0504d7b297c9786818888a93f08b92b03c6c122784b70488633", + "inputs/pr425/FULL-WORD.json.gz": "e55a0d4a1f1e3daaa082749489c9df2025f6a4fe9576aad2726cf881280f16fb", + "inputs/pricing/cost.py": "d55d2b865d1c3d35e343e1a38c592b9172ed8e2596d1107e34d92e2a80c7d03f", + "inputs/pricing/hist_p10b.json": "d70c58e539141c49453a684d0b01324a08d49f7c28dccd3b5b82472b5a8594a4" + } +} diff --git a/research/format-obstructions/checks/certs.py b/research/format-obstructions/checks/certs.py new file mode 100644 index 0000000000..8966b44c0d --- /dev/null +++ b/research/format-obstructions/checks/certs.py @@ -0,0 +1,157 @@ +"""Theorems A, B, C on gcert/1 certificates (one invocation, window F_2^h, standard dot product). + +For a gcert/1 file: + * gx.check1 (Sussman's reference checker, label half + exact scalar half) must accept it; + * Thm A: replay the gates and carry, for every register, the set of x-sources whose content entered it along + drop-free paths ("taint"; the scatter cut, a drop to frame 0, passes no taint). At EVERY gate each newly + received source port must lie in the gate frame (exact F_2 reduction); + * Cor A1: the lossless set of every target y_S (its final taint) is orthogonal to q_S, and does not contain S; + * Thm B data: N(S) = span{q_T : T in taint(y_S)} and its rank; every y reads every total (co-read); + * Thm C: for every retained total, A_k = span of the ports of its taint; copy price paid = dim f_k; lower bound = + rank of the pairing A_k x span(readers). +""" +import gzip +import json +import sys +import time +from fractions import Fraction as Fr +from pathlib import Path + +ROOT = Path(__file__).resolve().parent.parent +sys.path.insert(0, str(ROOT / "gx")) +sys.path.insert(0, str(ROOT / "checks")) +import gx # noqa: E402 (Jacob Sussman's reference checker, vendored unchanged) +from f2 import dot, pairing_rank, rank # noqa: E402 + + +def load(path): + path = str(path) + op = gzip.open if path.endswith(".gz") else open + with op(path, "rt") as f: + return json.load(f) + + +def replay(c, gate_check=True): + """Taint replay (Thm A). Returns (taint, tot_taint, tot_frame, stats).""" + h, v, R = c["h"], c["v"], c["R"] + nreg = 2 * v + R + ports = c["ports"] + fr = [tuple(f) for f in c["frames"]] + taint = [(1 << r) if r < v else 0 for r in range(nreg)] + stats = dict(gate_checks=0, violations=0, pairs=0) + + def portlist(bits): + while bits: + low = bits & -bits + yield ports[low.bit_length() - 1] + bits ^= low + + def run(gates): + for g in gates: + regs, pairs, _ = gx.gate_regs(g) + for t, s, co in pairs: + stats["pairs"] += 1 + new = taint[s] & ~taint[t] + if gate_check and new: + for q in portlist(new): + stats["gate_checks"] += 1 + if gx.reduce(q, fr[g[1]]) != 0: + stats["violations"] += 1 + taint[t] |= taint[s] + + run(c["A"]) + ret = sorted(c["ret"]) + tot_taint = {k: taint[s] for k, s, f in ret} + tot_frame = {k: f for k, s, f in ret} + run(c["B"]) + return taint, tot_taint, tot_frame, stats + + +def analyse(path, gate_check=True): + c = load(path) + t0 = time.monotonic() + gx.check1(c, scalar=True) + t_check = time.monotonic() - t0 + h, v, R = c["h"], c["v"], c["R"] + ports = c["ports"] + fr = [tuple(f) for f in c["frames"]] + t0 = time.monotonic() + taint, tot_taint, tot_frame, stats = replay(c, gate_check) + t_replay = time.monotonic() - t0 + coread_all = True + for t in range(v): + ks = {k for k, co in gx.scat_row(c, t) if co != 0} + if ks != set(tot_taint): + coread_all = False + + def portlist(bits): + out = [] + while bits: + low = bits & -bits + out.append(ports[low.bit_length() - 1]) + bits ^= low + return out + + perp_ok, self_hit = True, False + ranks, degs = [], [] + for S in range(v): + tb = taint[v + S] + self_hit |= bool(tb >> S & 1) + Ts = [T for T in range(v) if tb >> T & 1] + degs.append(len(Ts)) + perp_ok &= all(dot(ports[T], ports[S]) == 0 for T in Ts) + ranks.append(rank([ports[T] for T in Ts])) + lb = paid = 0 + for k in sorted(tot_taint): + A = portlist(tot_taint[k]) + lb += pairing_rank(A, ports) + paid += len(fr[tot_frame[k]]) + res = dict(file=Path(str(path)).name, h=h, v=v, R=R, cst=c["cst"], check1="PASS", + thmA_gate_checks=stats["gate_checks"], thmA_violations=stats["violations"], + incap_perp=perp_ok, self_lossless=self_hit, incap_deg=[min(degs), max(degs)], + N_rank=[min(ranks), max(ranks)], coread_all=coread_all, window_rank=rank(ports), + copy_lb=lb, copy_paid=paid, seconds=dict(check1=round(t_check, 1), replay=round(t_replay, 1))) + return res, c, taint + + +def controls(c, taint): + """Negative controls on the small certificate c (p = 3).""" + import copy + v = c["v"] + ports = c["ports"] + out = {} + # (1) cyclically shifted labels: the lossless sets are no longer orthogonal -> the Cor A1 test fires + sh = ports[1:] + ports[:1] + bad = sum(1 for S in range(v) for T in range(v) + if taint[v + S] >> T & 1 and dot(sh[T], sh[S])) + out["shifted_labels_nonorthogonal_pairs"] = bad + assert bad > 0, "control failed: shifted labels still orthogonal" + # (2) a corrupted port that still passes E0 (odd weight, distinct): gx.check1 rejects it at E1 and the taint replay + # reports source ports outside the gate frame + used = set(ports) + mask = next(m for m in range(3, 1 << c["h"]) if not bin(m).count("1") & 1 and (ports[0] ^ m) not in used + and (ports[0] ^ m) > 0) + c2 = copy.deepcopy(c) + c2["ports"][0] ^= mask + try: + gx.check1(c2, scalar=True) + raise AssertionError("control failed: gx.check1 accepted a corrupted port") + except AssertionError as e: + if "control failed" in str(e): + raise + out["corrupted_port_check1_rejects"] = str(e).split(":")[0] + _, _, _, st = replay(c2, True) + out["corrupted_port_replay_violations"] = st["violations"] + assert st["violations"] > 0, "control failed: replay saw no violation for a corrupted port" + return out + + +FILES = {"p3": "gcert1-p3-cone-R16.json", "p10": "gcert1-p10-anneal-mw-flow.json.gz", "p11": "gcert1-p11-pr193.json.gz"} + + +def stage(name): + """One certificate: gx.check1, Thm A/B/C data, and (for the small one) the negative controls.""" + res, c, taint = analyse(ROOT / "inputs" / FILES[name], gate_check=True) + if name == "p3": + res["controls"] = controls(c, taint) + return res diff --git a/research/format-obstructions/checks/e8lib.py b/research/format-obstructions/checks/e8lib.py new file mode 100644 index 0000000000..7f982baf0a --- /dev/null +++ b/research/format-obstructions/checks/e8lib.py @@ -0,0 +1,50 @@ +"""The 120 E8 root lines in Construction-A (Hamming) coordinates, and the graphs on them. + +Excerpt of the local research file cxlib.py (DreamingOfClouds, with Anthropic Claude assistance). The coordinates +are those of PR #370 (Dylan Crow): 8 coordinate lines 2e_i and 112 sign lines on the 14 weight-4 blocks of the +extended Hamming code H8. With = (a . b)/2 on the integer representatives: + * the 'in-cap' (lossless-helper) graph of the E8 complex word joins lines with = +-1 (degree 56); + * the E8-orthogonal pairs ( = 0) have degree 63. +""" +import itertools + +V = 120 + + +def _ham(): + g = [(1, 1, 1, 1, 0, 0, 0, 0), (1, 1, 0, 0, 1, 1, 0, 0), (1, 0, 1, 0, 1, 0, 1, 0), (0, 1, 1, 0, 1, 0, 0, 1)] + H = set() + for a in itertools.product((0, 1), repeat=4): + H.add(tuple(sum(a[k] * g[k][i] for k in range(4)) % 2 for i in range(8))) + return sorted(H) + + +H8 = _ham() +BLOCKS = sorted(tuple(i for i in range(8) if w[i]) for w in H8 if sum(w) == 4) +assert len(BLOCKS) == 14 +LINES = [] +for i in range(8): + v = [0] * 8 + v[i] = 2 + LINES.append(tuple(v)) +for c in BLOCKS: + for sg in itertools.product((1, -1), repeat=3): + v = [0] * 8 + v[c[0]] = 1 + for k, s in zip(c[1:], sg): + v[k] = s + LINES.append(tuple(v)) +assert len(LINES) == V + + +def ip(u, v): + return sum(a * b for a, b in zip(u, v)) // 2 + + +G = [[ip(LINES[a], LINES[b]) for b in range(V)] for a in range(V)] +NB = [[b for b in range(V) if abs(G[a][b]) == 1] for a in range(V)] # in-cap (non-orthogonal) neighbours +OR = [[b for b in range(V) if a != b and G[a][b] == 0] for a in range(V)] # E8-orthogonal pairs +assert all(len(x) == 56 for x in NB) and all(len(x) == 63 for x in OR) +assert all(G[a][a] == 2 for a in range(V)) +ORTH_PAIRS = [(a, b) for a in range(V) for b in range(a + 1, V) if G[a][b] == 0] +assert len(ORTH_PAIRS) == V * 63 // 2 diff --git a/research/format-obstructions/checks/f2.py b/research/format-obstructions/checks/f2.py new file mode 100644 index 0000000000..e0cd86171b --- /dev/null +++ b/research/format-obstructions/checks/f2.py @@ -0,0 +1,39 @@ +"""Exact F_2 helpers (vectors are Python ints, the form is the standard dot product mod 2).""" + + +def par(x): + return bin(x).count("1") & 1 + + +def dot(a, b): + return bin(a & b).count("1") & 1 + + +def span_basis(vecs): + """Echelon basis (list of ints, descending pivots) of the F_2 span.""" + basis = [] + for u in vecs: + for b in basis: + if u ^ b < u: + u ^= b + if u: + basis.append(u) + basis.sort(reverse=True) + return basis + + +def rank(vecs): + return len(span_basis(vecs)) + + +def pairing_rank(A, B): + """Rank of the bilinear pairing span(A) x span(B) -> F_2 (dot product).""" + a, b = span_basis(A), span_basis(B) + rows = [] + for x in a: + r = 0 + for j, y in enumerate(b): + if dot(x, y): + r |= 1 << j + rows.append(r) + return rank(rows) diff --git a/research/format-obstructions/checks/families.py b/research/format-obstructions/checks/families.py new file mode 100644 index 0000000000..fae63dfcf0 --- /dev/null +++ b/research/format-obstructions/checks/families.py @@ -0,0 +1,153 @@ +"""Port-family data for Thm B (neighbourhood rank), Thm C (copy lower bound) and the clique bound. + +paired_bit(p) paired cube, bit side: Q labels t_T (indicators of the 3-subset), form x^T (I - J/9) y, so + form(S, T) = |S cap T| - 1 and 'in-cap' = |S cap T| = 1. +e8_bitdual() 120 E8 root lines in Q^8 with the E8 form; in-cap = orthogonal roots; F_2 decoder M = (J + Gram) mod 2 + = U U^T for the 9-bit words U (isomorphism search), its copy lower bound sum_i rank_Q Gram[S_i, S_i]. +e8_complex(u) the unique h = 9 complex labelling (from sat_e8.uniqueness_h9): neighbourhood ranks. +incap_omega clique numbers of the paired-cube in-cap graphs by exact max-clique search. +p10_clique the explicit 20-clique of the complex in-cap graph of the p = 10 program, checked inside the program's + own realised lossless graph. +A neighbourhood N(S) of rank h - 1 equals q_S^perp, which is nondegenerate (its complement q_S is), so its form rank +equals its dimension; we assert this wherever the table uses it. +""" +import itertools +import sys +import time +from fractions import Fraction as Fr +from pathlib import Path + +ROOT = Path(__file__).resolve().parent.parent +sys.path.insert(0, str(ROOT / "checks")) +from certs import load, replay # noqa: E402 +from f2 import dot, span_basis # noqa: E402 + + +def qrank(rows): + M = [[Fr(x) for x in r] for r in rows] + rk = 0 + ncol = len(M[0]) if M else 0 + for col in range(ncol): + piv = next((i for i in range(rk, len(M)) if M[i][col] != 0), None) + if piv is None: + continue + M[rk], M[piv] = M[piv], M[rk] + for i in range(len(M)): + if i != rk and M[i][col] != 0: + f = M[i][col] / M[rk][col] + M[i] = [a - f * b for a, b in zip(M[i], M[rk])] + rk += 1 + return rk + + +def paired_bit(p): + P = [frozenset(2 * i + b for i, b in zip(I, bb)) for I in itertools.combinations(range(p), 3) + for bb in itertools.product((0, 1), repeat=3)] + h = 2 * p + T = P[0] + nb = [S for S in P if len(S & T) == 1] + form = lambda S, U: Fr(len(S & U)) - Fr(len(S) * len(U), 9) # noqa: E731 + assert all(form(S, T) == 0 for S in nb) and form(T, T) == 2 + r = qrank([[1 if i in S else 0 for i in range(h)] for S in nb]) + assert r == h - 1 # N = U^perp, nondegenerate + return dict(p=p, h=h, v=len(P), incap_deg=len(nb), N_rank=r) + + +def _e8_roots(): + Rt = [] + for i, j in itertools.combinations(range(8), 2): + for si in (2, -2): + for sj in (2, -2): + r = [0] * 8 + r[i] = si + r[j] = sj + Rt.append(tuple(r)) + for s in itertools.product((1, -1), repeat=8): + if s.count(-1) % 2 == 0: + Rt.append(s) + lines, seen = [], set() + for r in Rt: + if tuple(-x for x in r) in seen: + continue + seen.add(r) + lines.append(r) + return lines + + +def e8_bitdual(): + import networkx as nx + lines = _e8_roots() + v = len(lines) + assert v == 120 + G = [[sum(a * b for a, b in zip(x, y)) // 4 for y in lines] for x in lines] + assert all(G[i][i] == 2 for i in range(v)) + nb_ranks = set() + for a in range(v): + nb = [lines[b] for b in range(v) if b != a and G[a][b] == 0] + nb_ranks.add((len(nb), qrank(nb))) + off = [[(G[i][j] % 2 == 1) for j in range(v)] for i in range(v)] + lab9 = [frozenset(t) for t in itertools.combinations(range(9), 3)] + \ + [frozenset(range(9)) - frozenset(p) for p in itertools.combinations(range(9), 2)] + G9 = nx.Graph() + G9.add_edges_from((i, j) for i in range(v) for j in range(i + 1, v) if len(lab9[i] & lab9[j]) % 2 == 0) + Goff = nx.Graph() + Goff.add_edges_from((i, j) for i in range(v) for j in range(i + 1, v) if off[i][j]) + iso = next(nx.algorithms.isomorphism.GraphMatcher(Goff, G9).isomorphisms_iter()) + U = [[1 if i in lab9[iso[s]] else 0 for i in range(9)] for s in range(v)] + ok = all((sum(U[i][t] * U[j][t] for t in range(9)) % 2) == ((1 + G[i][j]) % 2) for i in range(v) for j in range(v)) + assert ok + lb, betas = 0, [] + for t in range(9): + S = [s for s in range(v) if U[s][t]] + b = qrank([[G[a][c] for c in S] for a in S]) # pairing rank span(src) x span(readers), src = readers = S + betas.append(b) + lb += b + assert sorted(nb_ranks) == [(63, 7)] + return dict(v=v, h=8, neighbourhood=sorted(nb_ranks), decoder_equals_UUt=ok, totals=9, betas=betas, + copy_lb=lb) + + +def e8_complex(u): + from e8lib import NB, V + ranks = set() + for S in range(V): + N = span_basis([u[T] for T in NB[S]]) + assert all(dot(x, u[S]) == 0 for x in N) + ranks.add(len(N)) + assert ranks == {8} + return dict(v=V, h=9, incap_deg=56, N_rank=8) + + +def incap_omega(p, kind): + import networkx as nx + P = [frozenset(2 * i + b for i, b in zip(I, bb)) for I in itertools.combinations(range(p), 3) + for bb in itertools.product((0, 1), repeat=3)] + pred = (lambda j: j == 1) if kind == "bit" else (lambda j: j in (0, 2)) + G = nx.Graph() + G.add_nodes_from(range(len(P))) + G.add_edges_from((a, b) for a in range(len(P)) for b in range(a + 1, len(P)) if pred(len(P[a] & P[b]))) + t0 = time.monotonic() + cl, w = nx.max_weight_clique(G, weight=None) + return dict(p=p, h=2 * p, kind=kind, omega=w, seconds=round(time.monotonic() - t0, 1)) + + +def p10_clique(path): + """5 pairwise-disjoint transversal 4-sets from the K5 stars, all 4 triples each: 20 ports, pairwise even overlap.""" + c = load(path) + h, v = c["h"], c["v"] + assert h == 20 + ports = c["ports"] + index = {q: i for i, q in enumerate(ports)} + E = list(itertools.combinations(range(5), 2)) + assert len(E) == 10 + sets = [[2 * i + (0 if e[0] == x else 1) for i, e in enumerate(E) if x in e] for x in range(5)] + tri = [sum(1 << c_ for c_ in t) for s in sets for t in itertools.combinations(s, 3)] + assert len(tri) == 20 and len(set(tri)) == 20 + T = [index[q] for q in tri] # all 20 are ports of the program + assert all(dot(a, a) == 1 for a in tri) + assert all(dot(a, b) == 0 for a, b in itertools.combinations(tri, 2)) + taint, _, _, _ = replay(c, gate_check=False) + realised = all(taint[v + S] >> Tt & 1 for S in T for Tt in T if S != Tt) + assert realised + return dict(size=len(T), orthonormal=True, all_pairs_lossless_in_program=realised, window_dim=h, + label_dim_sum_le=h) diff --git a/research/format-obstructions/checks/mutable425.py b/research/format-obstructions/checks/mutable425.py new file mode 100644 index 0000000000..5ac0f815e9 --- /dev/null +++ b/research/format-obstructions/checks/mutable425.py @@ -0,0 +1,360 @@ +"""PR #425's mutable-basis word (jacklightChen / Zhihao Chen): Thms A, B, C and Theorem S, checked exactly. + +Input: inputs/pr425/FULL-WORD.json.gz = #425's FULL-WORD.json.gz (920 registers: 120 sources, 120 targets, 680 helper +registers), regenerated by #425's own hamming_packets.py + hamming_full.py; sha256 equals #425's EXPECTED.json. +Events: ['add', t, s, num, den, frame] (t += (num/den) s with both at 'frame'; frame None marks the centre copy that +drops full -> 0) and ['scale', t, num, den, frame]. Phases: A, cut (8 centre copies), B, cleanup (at the full frame). + +(1) frame + taint replay on the word as written. Thm A (taint of each gate register inside the gate frame), Cor A1 + (target taint orthogonal to its port, target frames inside the hyperplane), no target feeds a z-register + (z = sources + helpers), nested climbs, every gate at one common frame. The same detector, run in 'immutable' + mode, counts the two things the immutable-source / no-target-read format forbids. + Thm C on the 8 centre copies (pairing ranks vs frames paid). Thm B data (neighbourhood rank of every target) and + the common cut (all targets at frame 0 at the scatter). +(2) exact scalar replay over Q: z restored, J = I, V and K; with the frame-0 preconditioner y <- V^-1 (y - K s) the + word is exactly (x, s, y) -> (x, s, y + x). Control: omitting the K part is rejected. +(3) Theorem S: the conversion to the immutable-source / no-target-read format with one helper per modified source and + one per read target. Replayed with the same detector (zero violations) and exactly over Q (after the frame-0 + compensation of the response to the dirty registers). Controls: the same detector flags the unconverted word; + without the compensation the converted word is not (x, s, y) -> (x, s, y + x). +(4) coarse price (the moment of #425's hamming_full.py) of the word and of the converted word. +""" +import copy +import gzip +import json +import sys +from collections import Counter, defaultdict +from fractions import Fraction as Q +from pathlib import Path + +ROOT = Path(__file__).resolve().parent.parent +sys.path.insert(0, str(ROOT / "checks")) +from f2 import pairing_rank, par # noqa: E402 + +V = 120 + + +def basis(vectors): + """Reduced echelon basis (tuple, descending pivots) of the F_2 span of ints.""" + b = {} + for x in vectors: + for p in sorted(b, reverse=True): + if x >> p & 1: + x ^= b[p] + if x: + p = x.bit_length() - 1 + for q in b: + if b[q] >> p & 1: + b[q] ^= x + b[p] = x + return tuple(b[p] for p in sorted(b, reverse=True)) + + +def inside(a, b): + return basis(list(a) + list(b)) == tuple(b) if b else not a + + +def perp(p, F): + return all(par(p & x) == 0 for x in F) + + +def hyper(p): + return basis([x for x in range(1, 512) if par(x & p) == 0]) + + +FULL = basis([1 << i for i in range(9)]) + + +def is_tgt(r): + return V <= r < 2 * V + + +def frame_replay(phases, n, P, immutable, final_frames=True, collect=None): + """phases: [(name, events)]. Returns (cur, taint, kids, viol, stats).""" + cur = [((P[r],) if r < V else ()) for r in range(n)] + taint = [((P[r],) if r < V else ()) for r in range(n)] + kids = defaultdict(list) + viol, stats = Counter(), Counter() + + def climb(r, F): + if not inside(cur[r], F): + viol["non-nested"] += 1 + dr = len(F) - len(cur[r]) + if dr: + kids[r].append(dr) + cur[r] = F + + for ph, evs in phases: + if ph == "cut" and collect is not None: + collect["frames_at_cut"] = {r: cur[r] for r in range(n)} + for e in evs: + if e[0] == "scale": + t = e[1] + F = tuple(e[4]) if e[4] is not None else cur[t] + climb(t, F) + stats["scale"] += 1 + if t < V: + stats["src_modified"] += 1 + if immutable: + viol["source modified"] += 1 + continue + _, t, s = e[:3] + F = e[5] + if F is None: # centre copy: drop full -> 0, the target must stand at frame 0 + if cur[t] != (): + viol["cut-target-not-at-0"] += 1 + stats["cut"] += 1 + continue + F = tuple(F) + climb(t, F) + climb(s, F) + if is_tgt(s) and not is_tgt(t): + viol["target-feeds-z"] += 1 + if is_tgt(s): + stats["target_read"] += 1 + if immutable: + viol["target read"] += 1 + if t < V: + stats["src_modified"] += 1 + if immutable: + viol["source modified"] += 1 + taint[t] = basis(list(taint[t]) + list(taint[s])) + for r in (t, s): + if not inside(taint[r], cur[r]): + viol["ThmA taint not in frame"] += 1 + if is_tgt(r): + if not perp(P[r - V], cur[r]): + viol["target frame not in hyperplane"] += 1 + if not perp(P[r - V], taint[r]): + viol["CorA1 target taint not perp"] += 1 + if ph == "B" and final_frames: + for r in range(n): + climb(r, hyper(P[r - V]) if is_tgt(r) else FULL) + return cur, taint, kids, viol, stats + + +def scalar_replay(evs, n, rows=None): + rows = rows if rows is not None else [{r: Q(1)} for r in range(n)] + for e in evs: + if e[0] == "scale": + q = Q(e[2], e[3]) + rows[e[1]] = {j: q * x for j, x in rows[e[1]].items()} + continue + t, s, q = e[1], e[2], Q(e[3], e[4]) + for j, x in list(rows[s].items()): + z = rows[t].get(j, Q(0)) + q * x + if z: + rows[t][j] = z + else: + rows[t].pop(j, None) + return rows + + +def inv_mat(M): + idx = sorted(M) + k = len(idx) + pos = {r: i for i, r in enumerate(idx)} + a = [[M[r].get(c, Q(0)) for c in idx] + [Q(int(i == j)) for j in range(k)] for i, r in enumerate(idx)] + for col in range(k): + piv = next(i for i in range(col, k) if a[i][col]) + a[col], a[piv] = a[piv], a[col] + q = a[col][col] + a[col] = [x / q for x in a[col]] + for i in range(k): + if i != col and a[i][col]: + f = a[i][col] + a[i] = [x - f * y for x, y in zip(a[i], a[col])] + return {r: {c: a[pos[r]][k + pos[c]] for c in idx if a[pos[r]][k + pos[c]]} for r in idx} + + +def price(local, Rc, m=73, T=8, L=9): + """Coarse complex price of hamming_full.py: root of the moment sum (floats, 80 bisections).""" + W = 7680 + L * Rc + g = Counter({r: z * L * T for r, z in local.items()}) + for r in (16, 8, 32, 8, 48, 8, 48, 32, 16): + g[r] += 240 * T + g[1] += L * Rc + N = sum(g.values()) + lo, hi = 0., .003 + for _ in range(80): + q = (lo + hi) / 2 + mom = sum(r * z / (m * W) * (m / r) ** q for r, z in g.items()) + 32 * m * N / (10 ** 16 * W) * m ** q + if mom < 1: + lo = q + else: + hi = q + return (lo + hi) / 2 + + +def local_hist(kids): + H = Counter() + for r, ks in kids.items(): + for d in ks: + H[d] += 1 + H[9] += 8 # centre copies + return H + + +def run(): + WD = json.load(gzip.open(ROOT / "inputs" / "pr425" / "FULL-WORD.json.gz")) + P, Rr = WD["ports"], WD["root_lines"] + assert len(P) == V and all(par(q) for q in P) + A, B, CUT, CLEAN = WD["A"], WD["B"], WD["cut"], WD["cleanup"] + n = 1 + max(max(e[1], e[2] if e[0] == "add" else 0) for e in A + B + CUT + CLEAN) + R0 = n - 2 * V + centers = WD["centers"] + out = dict(registers=n, helpers=R0, m=WD["report"]["m"], h=WD["report"]["h"], v=WD["report"]["v"]) + assert (n, R0, out["m"], out["h"]) == (920, 680, 73, 9) + # the ports are an admissible E8 labelling in the sense of sat_e8 (u.u = 1, orthogonal on the 3,360 non-orthogonal + # root pairs, Gram 1 on the 3,780 orthogonal pairs), with the word's own root_lines: by the uniqueness result + # of sat_e8.uniqueness_h9 it is Sussman's labelling up to isometry + ip = lambda a, b: sum(int(x) * int(y) for x, y in zip(a, b)) // 2 # noqa: E731 + assert all(sum(int(x) * int(x) for x in Rr[s]) == 4 for s in range(V)) + gram_ok = all(bin(P[s] & P[t]).count("1") % 2 == (1 if s == t else (1 + ip(Rr[s], Rr[t])) % 2) + for s in range(V) for t in range(V)) + assert gram_ok + out["ports_realise_E8_gram"] = gram_ok + + # ---- (1) frame + taint replay, Thm A, Cor A1, Thm B data, Thm C on the centres + cleanFULL = [[e[0], *e[1:-1], list(FULL)] for e in CLEAN] + phases = [("A", A), ("cut", CUT), ("B", B), ("clean", cleanFULL)] + coll = {} + cur, taint, kids, viol, stats = frame_replay(phases, n, P, immutable=False, collect=coll) + assert not viol, dict(viol) + _, _, _, viol_imm, stats_imm = frame_replay(phases, n, P, immutable=True) + out["detector_on_word_as_written"] = dict(sorted(viol_imm.items())) + assert viol_imm == Counter({"source modified": 1640, "target read": 112}), dict(viol_imm) + modsrc = sorted({e[1] for e in A + B if e[1] < V}) + readtg = sorted({e[2] for e in A + B if e[0] == "add" and is_tgt(e[2])}) + out.update(thmA_violations=0, modified_sources=len(modsrc), read_targets=len(readtg), + stats={k: stats[k] for k in ("scale", "cut", "src_modified", "target_read")}) + assert (len(modsrc), len(readtg)) == (112, 112) + # common cut (R2 of Thm B): every target stands at frame 0 at the scatter + at_cut = coll["frames_at_cut"] + out["all_targets_at_frame0_at_cut"] = all(at_cut[V + t] == () for t in range(V)) + assert out["all_targets_at_frame0_at_cut"] + # Thm B data: lossless set of each target = final taint; its rank (= h-1 means N = q^perp) + nr = sorted({len(taint[V + t]) for t in range(V)}) + out["target_neighbourhood_ranks"] = nr + assert nr == [8] and all(perp(P[t], taint[V + t]) for t in range(V)) + assert all(len(basis(list(taint[V + t]) + [P[t]])) == 9 for t in range(V)) # q_t is not in its own lossless span + out["m_min_nine_stages"] = 1 + 9 * max(nr) + assert out["m_min_nine_stages"] == out["m"] == 73 + # Thm C on the eight centre copies: pairing rank of (sources gathered drop-free into the centre before the cut) + # x (targets reading it) against the frames paid. The gathered sources come from a bit-set taint replay of phase A + # and must equal the support of the centre's root-line coordinate. + tm = [(1 << r) if r < V else 0 for r in range(n)] + for e in A: + if e[0] == "add": + tm[e[1]] |= tm[e[2]] + cst_bound = cst_paid = 0 + gathered = [] + for i, c in enumerate(centers): + srcs = [s for s in range(V) if tm[c] >> s & 1] + assert srcs == [s for s in range(V) if int(Rr[s][i]) != 0], "centre taint differs from its root-line support" + assert basis([P[s] for s in srcs]) == coll["frames_at_cut"][c], "sources do not span the centre's frame" + readers = sorted({e[1] - V for e in CUT if e[2] == c}) + cst_bound += pairing_rank([P[s] for s in srcs], [P[t] for t in readers]) + cst_paid += len(coll["frames_at_cut"][c]) + gathered.append(len(srcs)) + out["sources_gathered_per_centre"] = gathered + out.update(cst_bound=cst_bound, cst_paid=cst_paid) + assert cst_bound == cst_paid == WD["report"]["cst"] == 72 + + # ---- (2) exact scalar replay + rows = scalar_replay(A + CUT + B + CLEAN, n) + zok = all(rows[r] == {r: Q(1)} for r in range(n) if not is_tgt(r)) + J_ok = all({j: x for j, x in rows[V + t].items() if j < V} == {t: Q(1)} for t in range(V)) + Vnon = sum(1 for t in range(V) for j, x in rows[V + t].items() if is_tgt(j) and j != V + t) + Knz = sum(1 for t in range(V) for j in rows[V + t] if j >= 2 * V) + Vm = {V + t: {j: x for j, x in rows[V + t].items() if is_tgt(j)} for t in range(V)} + Vi = inv_mat(Vm) + pre_rows = [] + for t in range(V): + row = dict(Vi[V + t]) + for u, a in Vi[V + t].items(): + for j, x in rows[u].items(): + if j >= 2 * V: + row[j] = row.get(j, Q(0)) - a * x + pre_rows.append({j: x for j, x in row.items() if x}) + init = [{r: Q(1)} for r in range(n)] + for t in range(V): + init[V + t] = pre_rows[t] + rows2 = scalar_replay(A + CUT + B + CLEAN, n, init) + ok2 = all(rows2[r] == {r: Q(1)} for r in range(n) if not is_tgt(r)) and \ + all(rows2[V + t] == {V + t: Q(1), t: Q(1)} for t in range(V)) + init3 = [{r: Q(1)} for r in range(n)] + for t in range(V): + init3[V + t] = dict(Vi[V + t]) + rows3 = scalar_replay(A + CUT + B + CLEAN, n, init3) + neg = any(rows3[V + t] != {V + t: Q(1), t: Q(1)} for t in range(V)) + out.update(z_restored=zok, J_is_identity=J_ok, V_offdiag=Vnon, K_nonzeros=Knz, + preconditioned_map_exact=ok2, omit_K_control_rejected=neg) + assert zok and J_ok and ok2 and neg + + # ---- (3) Theorem S + sim, nn = {}, n + for r in modsrc + readtg: + sim[r] = nn + nn += 1 + + def ren(e): + e = list(e) + e[1] = sim.get(e[1], e[1]) + if e[0] == "add": + e[2] = sim.get(e[2], e[2]) + return e + + pre = [["add", sim[r], r, 1, 1, [P[r]]] for r in modsrc] + A1, C1, B1 = [ren(e) for e in A], [ren(e) for e in CUT], [ren(e) for e in B] + final = [["add", t, sim[t], 1, 1, list(hyper(P[t - V]))] for t in readtg] + fwd_z = [e for e in pre + A1 + C1 + B1 if not is_tgt(e[1])][len(pre):] + + def inv(e): + e = copy.deepcopy(e) + if e[0] == "add": + e[3] = -e[3] + e[5] = list(FULL) + else: + e[2], e[3] = e[3], e[2] + e[4] = list(FULL) + return e + + clean1 = [inv(e) for e in reversed(fwd_z)] + [["add", sim[r], r, -1, 1, list(FULL)] for r in modsrc] + phasesS = [("A", pre + A1), ("cut", C1), ("B", B1 + final), ("clean", clean1)] + # the same detector on the converted word; the converted targets g_t must stay inside their hyperplane + # (the detector checks real targets; g_t is a helper, checked separately below) + # g_t follows y_t's frames; the final gate y_t += g_t is at hyper(P_t), so the detector's nestedness test also + # checks that g_t stands inside the hyperplane at that time + curS, taintS, kidsS, violS, statsS = frame_replay(phasesS, nn, P, immutable=True, final_frames=True) + out["detector_on_converted_word"] = dict(sorted(violS.items())) + assert not violS, dict(violS) + rowsS = scalar_replay(pre + A1 + C1 + B1 + final + clean1, nn) + zS = all(rowsS[r] == {r: Q(1)} for r in range(nn) if not is_tgt(r)) + KS = sum(1 for t in range(V) for j in rowsS[V + t] if j >= 2 * V) + initS = [{r: Q(1)} for r in range(nn)] + for t in range(V): + initS[V + t] = {V + t: Q(1)} + for j, x in rowsS[V + t].items(): + if j >= 2 * V: + initS[V + t][j] = -x + rowsS2 = scalar_replay(pre + A1 + C1 + B1 + final + clean1, nn, initS) + okS = all(rowsS2[r] == {r: Q(1)} for r in range(nn) if not is_tgt(r)) and \ + all(rowsS2[V + t] == {V + t: Q(1), t: Q(1)} for t in range(V)) + negS = any(rowsS[V + t] != {V + t: Q(1), t: Q(1)} for t in range(V)) # without the frame-0 compensation + RS = nn - 2 * V + out.update(S_helpers=RS, S_helpers_formula="R + b_x + b_y", S_z_restored=zS, S_K_nonzeros=KS, + S_exact_after_compensation=okS, S_uncompensated_rejected=negS) + assert RS == R0 + len(modsrc) + len(readtg) == 904 and zS and okS and negS + + # ---- (4) coarse price + H0 = local_hist(kids) + b0 = price(H0, R0) + HS = local_hist(kidsS) + bS = price(HS, RS) + rep = WD["report"] + assert abs(b0 - rep["complex_coarse_float"]) < 1e-15 + out.update(local_hist={str(k): v for k, v in sorted(H0.items())}, mass=sum(r * z for r, z in H0.items()), + b=b0, b_pre425=rep["baseline_b"], S_local_hist={str(k): v for k, v in sorted(HS.items())}, + S_mass=sum(r * z for r, z in HS.items()), S_b=bS, S_b_vs_b_percent=round(100 * (bS / b0 - 1), 2)) + return out diff --git a/research/format-obstructions/checks/pivots.py b/research/format-obstructions/checks/pivots.py new file mode 100644 index 0000000000..24c3a87bbb --- /dev/null +++ b/research/format-obstructions/checks/pivots.py @@ -0,0 +1,146 @@ +"""Section 7 of PROOF.md: the 2K block pivots of a shared-helper B_K layout (F_2 windows, gcert/1 programs). + +thm_P (exact). A helper set that runs the SAME gcert/1 program on the SAME slots in every stage: a slot never drops, +so after stage j its frame contains iota_j(q_T) for every source T it touched (Thm A); when it writes y_S in stage +j' > j its frame lies inside iota_j'(q_S)^perp. With K = iota_j^T iota_j' (h x h over F_2) this gives +q_T^T K q_S = 0 for every slot-carried pair (T in taint(z), S in writes(z)). The condition is linear in K; we compute +the rank of {q_T (x) q_S}. Rank h^2 means K = 0, i.e. the stage windows are pairwise orthogonal and m >= s*h. + +copy_count (exact, over ALL odd a, b in F_2^h). Model of ONE overlap w between the helper windows of two stages, +w = iota_{j-1}(e) = iota_j(e') with e.e = e'.e' = 1: a retained total whose frame is not inside e^perp carries w into +stage j; in stage j such a total pays one extra copy rank unless e' lies in its frame. Hence the forced extra copy +rank per overlap is >= (#totals) - (max #totals inside some e^perp) - (max #frames containing some e'). + +overlap_scan (exact on the candidates). The same model on the helper side: slots whose last frame is not inside e^perp +carry w; their forward closure through the gates contaminates registers, and a contaminated target y_S needs +e'.q_S = 0. Candidates: the h unit vectors and the 1,140 weight-3 vectors (h = 20), not all directions. +""" +import sys +from pathlib import Path + +ROOT = Path(__file__).resolve().parent.parent +sys.path.insert(0, str(ROOT / "gx")) +sys.path.insert(0, str(ROOT / "checks")) +import gx # noqa: E402 +from certs import load # noqa: E402 +from f2 import dot, span_basis # noqa: E402 + + +def _taint_and_writes(c): + h, v, R = c["h"], c["v"], c["R"] + nreg = 2 * v + R + taint = [(1 << r) if r < v else 0 for r in range(nreg)] + writes = {} + for g in c["A"] + c["B"]: + regs, pairs, _ = gx.gate_regs(g) + for t, s, co in pairs: + taint[t] |= taint[s] + if 2 * v <= s and v <= t < 2 * v: + writes.setdefault(s, set()).add(t - v) + return taint, writes + + +def thm_P(path): + c = load(path) + gx.check1(c, scalar=False) + h, v, R = c["h"], c["v"], c["R"] + ports = c["ports"] + taint, writes = _taint_and_writes(c) + + def kron(a, b): + out = 0 + for i in range(h): + if a >> i & 1: + out |= b << (h * i) + return out + + def rank_of(only_orth, cap): + basis, used = [], 0 + for z in sorted(writes): + Ts = [T for T in range(v) if taint[z] >> T & 1] + for S in writes[z]: + for T in Ts: + if only_orth and dot(ports[T], ports[S]): + continue + vec = kron(ports[T], ports[S]) + used += 1 + for b_ in basis: + if vec ^ b_ < vec: + vec ^= b_ + if vec: + basis.append(vec) + basis.sort(reverse=True) + if len(basis) == cap: + return len(basis), used + return len(basis), used + + # (a) pairs with q_T . q_S = 0 only: their tensors lie in the trace hyperplane (tr M = sum_i M_ii = q_T . q_S) + r_orth, used_orth = rank_of(True, h * h) + # (b) all slot-carried pairs + r_all, used_all = rank_of(False, h * h) + assert r_orth == h * h - 1 and r_all == h * h, (r_orth, r_all) # K = lambda * I from (a); K = 0 from (b) + # cross-cube slots (descriptive; paired-cube ports only) + cube = [frozenset(i // 2 for i in range(h) if q >> i & 1) for q in ports] + written = sorted({S for z in writes for S in writes[z]}) + written_rank = len(span_basis([ports[S] for S in written])) + assert written_rank == h # the slot-written targets' ports span the window + cross = sum(1 for z in range(2 * v, 2 * v + R) if len({cube[T] for T in range(v) if taint[z] >> T & 1}) > 1) + return dict(file=Path(str(path)).name, h=h, slots=R, writer_slots=len(writes), + rank_orthogonal_pairs_only=r_orth, rank_all_carried_pairs=r_all, h_squared=h * h, + K_solution_dim=h * h - r_all, slot_written_targets_port_rank=written_rank, K_zero_gives_m_ge="s*h, under (P1)-(P2)", cross_cube_slots=cross) + + +def copy_count(path): + c = load(path) + h = c["h"] + fr = [tuple(f) for f in c["frames"]] + F = [fr[f] for k, s, f in sorted(c["ret"])] + best_nc = best_in = 0 + for a in range(1, 1 << h): + if not (bin(a).count("1") & 1): + continue + nc = sum(1 for f in F if all(not dot(b, a) for b in f)) + ins = sum(1 for f in F if gx.reduce(a, f) == 0) + best_nc = max(best_nc, nc) + best_in = max(best_in, ins) + return dict(totals=len(F), frame_dims=sorted({len(f) for f in F}), max_noncarrier_totals=best_nc, + max_totals_containing_b=best_in, forced_extra_copy_per_overlap=len(F) - best_nc - best_in) + + +def overlap_scan(path): + c = load(path) + h, v, R = c["h"], c["v"], c["R"] + nreg = 2 * v + R + ports = c["ports"] + fr = [tuple(f) for f in c["frames"]] + gates = [("A", g) for g in c["A"]] + [("B", g) for g in c["B"]] + regsets = [gx.gate_regs(g)[0] for _, g in gates] + last = {} + for i, (_, g) in enumerate(gates): + for r in regsets[i]: + if r >= 2 * v: + last[r] = g[1] + slots = sorted(last) + + def carriers(e): + return {z for z in slots if any(dot(b, e) for b in fr[last[z]])} + + def closure(C): + bad = set(C) + for i, (_, g) in enumerate(gates): + rs = regsets[i] + if any(r in bad for r in rs): + bad.update(rs) + return bad + + odd = [e for e in range(1, 1 << h) if bin(e).count("1") & 1] + cand = [1 << i for i in range(h)] + [e for e in odd if bin(e).count("1") == 3][:2000] + recs = [] + for e in cand: + C = carriers(e) + bad = closure(C) + ys = [r - v for r in bad if v <= r < 2 * v] + recs.append((len(C), len(bad), len(ys), len(span_basis([ports[S] for S in ys])))) + return dict(h=h, slots=R, slots_with_gates=len(slots), registers=nreg, candidates=len(cand), + min_carriers=min(r[0] for r in recs), min_contaminated_registers=min(r[1] for r in recs), + min_contaminated_targets=min(r[2] for r in recs), min_port_rank_of_contaminated=min(r[3] for r in recs)) diff --git a/research/format-obstructions/checks/pricing.py b/research/format-obstructions/checks/pricing.py new file mode 100644 index 0000000000..84b6a36899 --- /dev/null +++ b/research/format-obstructions/checks/pricing.py @@ -0,0 +1,97 @@ +"""Pricing context for the pivots (PROOF.md section 7) and for non-nested chains (section 8), with the pinned pricer. + +Pricer: inputs/pricing/cost.py (solve_moment), PR #346 (Louis Harrison) from PR #310 (Dylan Crow, utcorvusvolat-dotcom), +vendored unchanged. Input: the normalised five-stage histogram of PR #325's p = 10 bit word (hist_p10b.json: m = 100, +W = 131,760 = 12 * 10,980, deficit D = 24,480; every count is 12 x a per-invocation count) and its pinned bit root +385138454781521/(5 * 10^17). + + * baseline: the pricer reproduces the pinned root. + * pivot-free variants (m = 96 = 1 + 5 (h - 1)): each helper wire loses 4 levels (4 blocks of rank r -> r - 1), the + pair-1 end idle block goes 2h+2 -> 2h-2 and the pair-2 end idle block of rank 4 disappears. Four ways of choosing + which helper blocks shrink bracket the gain. 'forced copies': 40 extra copy rank per unit (4 overlaps x 10, see + pivots.copy_count), modelled as 40 x 12 blocks of rank 18 becoming rank 19. + * non-nested chain (section 8): one rank-1 copy in each of the five stages, per 12-normalised unit, is +60 blocks of rank 1 (5 stages + x 12); a rank-1 register descent is a single non-nested step of frame-lemma rank d = 2, +60 blocks of rank 2. +These are pricer-model outputs for the p = 10 bit word, not theorems. +""" +import collections +import importlib.util +import json +import sys +from pathlib import Path + +from mpmath import mp, mpf + +ROOT = Path(__file__).resolve().parent.parent + + +def run(): + spec = importlib.util.spec_from_file_location("cost", ROOT / "inputs" / "pricing" / "cost.py") + C = importlib.util.module_from_spec(spec) + sys.modules.setdefault("cost", C) + spec.loader.exec_module(C) + mp.dps = 40 + d = json.load(open(ROOT / "inputs" / "pricing" / "hist_p10b.json")) + H0 = collections.Counter({int(k): v for k, v in d["histogram"].items()}) + W = mpf(d["W"]) + m0 = d["m"] + v12 = 960 * 12 + Rs = d["W"] - 4 * v12 + mass0 = sum(r * n for r, n in H0.items()) + D0 = d["W"] * m0 - mass0 + assert (m0, d["W"], D0, d["deficit"]) == (100, 131760, 24480, 24480) + a0 = C.solve_moment(H0, W, m0) + num, den = d["bit_root"].split("/") + pinned = mpf(int(num)) / mpf(int(den)) + # the pinned value is the certified grid point (step 1/den = 2e-18) at or just below the root + assert 0 <= a0 - pinned < mpf(1) / int(den), (a0, pinned) + out = dict(m=m0, W=d["W"], D=D0, root=format(float(a0), ".12e"), pinned_root=format(float(pinned), ".12e")) + + def variant(shrink, extra_copy=0): + H = collections.Counter(H0) + H[42] -= 2 * v12 + H[38] += 2 * v12 + H[4] -= 2 * v12 + for r, cnt in shrink: + H[r] -= cnt + if r > 1: + H[r - 1] += cnt + assert all(c >= 0 for c in H.values()) + if extra_copy: + H[18] -= extra_copy + H[19] += extra_copy + m = 96 + return W * m - sum(r * n for r, n in H.items()), C.solve_moment(H, W, m) + + def spread(ranks): + need = 4 * Rs + res = [] + for r in ranks: + take = min(need, H0[r] - (2 * v12 if r in (4,) else 0)) + res.append((r, take)) + need -= take + if not need: + break + assert need == 0 + return res + + rows = {} + for name, shrink in (("rank-1 blocks removed", [(1, 4 * Rs)]), ("blocks 2->1", [(2, 4 * Rs)]), + ("mid blocks shortened", spread([3, 4, 5, 6, 7, 8, 9, 10, 12, 14])), + ("largest blocks shortened", spread([19, 18, 17, 16, 14, 12, 11, 10]))): + D, a = variant(shrink) + D2, a2 = variant(shrink, extra_copy=40 * 12) + assert D == D0 + rows[name] = dict(zero_cost_percent=format(float((a / a0 - 1) * 100), "+.2f"), + with_40_forced_copy_percent=format(float((a2 / a0 - 1) * 100), "+.2f")) + out["pivot_free_m96"] = rows + + def delta(H): + return format(float((C.solve_moment(H, W, m0) / a0 - 1) * 100), "+.4f") + Hc = collections.Counter(H0) + Hc[1] += 60 + Hd = collections.Counter(H0) + Hd[2] += 60 + out["per_stage_rank1_copy_percent"] = delta(Hc) + out["per_stage_rank1_register_descent_percent"] = delta(Hd) + return out diff --git a/research/format-obstructions/checks/sat_e8.py b/research/format-obstructions/checks/sat_e8.py new file mode 100644 index 0000000000..082d1cbba0 --- /dev/null +++ b/research/format-obstructions/checks/sat_e8.py @@ -0,0 +1,476 @@ +"""Exact SAT checks on the E8 in-cap graph (CaDiCaL through python-sat). + +Model. An 'in-cap labelling' of a graph H on the 120 E8 lines assigns to each line T a nondegenerate k-dimensional +subspace A_T of (F_2^r, standard dot product), with A_S orthogonal to A_T for every edge {S, T} of H. H below is the +E8 non-orthogonal graph (3360 edges, degree 56, clique number 8): the pairs the E8 decoder leaves to lossless +helpers. By Cor. A1 of PROOF.md every such pair needs orthogonal labels. + +Reduction (WLOG, argued in PROOF.md section 6): fix an 8-clique C of H. Its labels are pairwise orthogonal and +nondegenerate, so they form an orthogonal direct sum, and the window splits along them. For k = 1 the 8 labels are +orthonormal and can be taken to be e_1..e_8; for k = 2 each plane is the standard I_2 or the hyperbolic H plane and +the window form is the sum of the 8 plane forms and I on the complement (any non-alternating form of that rank is +isometric to I_r). Every other line T then has A_T supported on the blocks of the clique members not adjacent to T, +plus the complement coordinates. + + (a) uniqueness_h9: k = 1, r = 9, with distinct labels (E0 of gx.check1): exactly ONE labelling, enumerated to + exhaustion, and it is Sussman's (u_S . u_T = 1 on every E8-orthogonal pair, 0 on every in-cap pair). + (b) k2_planes: k = 2, r = 16 and 17: UNSAT for every plane-type pattern of the clique (any port type). +Controls: k = 1, r = 8 is UNSAT and r = 9 SAT (calibration); the k = 2 encoder at r = 18 accepts the direct sum of +two copies of the k = 1 solution (positive control). +""" +import itertools +import sys +import time +from pathlib import Path + +sys.path.insert(0, str(Path(__file__).resolve().parent)) +from e8lib import G, NB, ORTH_PAIRS, V # noqa: E402 +from f2 import dot, span_basis # noqa: E402 + + +# ---------------------------------------------------------------------------------------------------------------- +# (a) k = 1: the admissible labellings at h = 9 (from the local research file satlab.py) +CL = [119, 118, 102, 98, 79, 72, 37, 34] # an 8-clique (Hamming indices) of the in-cap graph + + +class Model: + """CNF of: u: lines -> F_2^h, u.u = 1, u_S.u_T = 0 on in-cap pairs, labels distinct; CL = e_1..e_8.""" + + def __init__(s, h): + s.h = h + s.nv = 0 + s.cl = [] + s.T = s.var() + s.cl.append([s.T]) + s.u = [[None] * h for _ in range(V)] + for S in range(V): + for k in range(h): + if S in CL: + s.u[S][k] = s.T if k == CL.index(S) else -s.T + elif k < 8 and G[S][CL[k]] != 0: + s.u[S][k] = -s.T + else: + s.u[S][k] = s.var() + for S in range(V): + if S not in CL: + s.bil_eq(S, S, 1) + for S in range(V): + for T in NB[S]: + if S < T: + s.bil_eq(S, T, 0) + for S in range(V): + for T in range(S + 1, V): + ds = [s.xor2(s.u[S][k], s.u[T][k]) for k in range(h)] + ds = [x for x in ds if x != -s.T] + s.cl.append(ds) + + def var(s): + s.nv += 1 + return s.nv + + def and2(s, a, b): + if a == -s.T or b == -s.T: + return -s.T + if a == s.T: + return b + if b == s.T: + return a + y = s.var() + s.cl += [[-y, a], [-y, b], [y, -a, -b]] + return y + + def xor2(s, a, b): + if a == -s.T: + return b + if b == -s.T: + return a + if a == s.T: + return -b + if b == s.T: + return -a + y = s.var() + s.cl += [[-y, a, b], [-y, -a, -b], [y, -a, b], [y, a, -b]] + return y + + def xor_eq(s, lits, c): + lits = [x for x in lits if x != -s.T] + n_t = sum(1 for x in lits if x == s.T) + lits = [x for x in lits if x != s.T] + c ^= n_t & 1 + if not lits: + if c: + s.cl.append([]) + return + acc = lits[0] + for x in lits[1:]: + acc = s.xor2(acc, x) + s.cl.append([acc] if c else [-acc]) + + def bil_eq(s, S, T, c): + s.xor_eq([s.and2(s.u[S][k], s.u[T][k]) for k in range(s.h)], c) + + def labels(s, m): + out = [] + for S in range(V): + x = 0 + for k in range(s.h): + lit = s.u[S][k] + b = (lit == s.T) if abs(lit) == s.T else ((m[abs(lit) - 1] > 0) == (lit > 0)) + if b: + x |= 1 << k + out.append(x) + return out + + +def uniqueness_h9(): + from pysat.solvers import Cadical153 + t0 = time.monotonic() + m = Model(9) + sol = Cadical153(bootstrap_with=m.cl) + free = [m.u[S][k] for S in range(V) for k in range(9) if abs(m.u[S][k]) != m.T] + sols = [] + while sol.solve(): + mod = sol.get_model() + sols.append(m.labels(mod)) + sol.add_clause([-x if (mod[abs(x) - 1] > 0) == (x > 0) else x for x in free]) + assert len(sols) <= 5, "more than 5 solutions" + sol.delete() + assert len(sols) == 1, len(sols) + u = sols[0] + # independent verification of the labelling, not through the CNF + assert all(dot(u[S], u[S]) == 1 for S in range(V)) + assert all(dot(u[S], u[T]) == 0 for S in range(V) for T in NB[S]) + assert len(set(u)) == V + assert all(dot(u[a], u[b]) == 1 for a, b in ORTH_PAIRS) # Sussman's Gram: 1 on all 3780 E8-orthogonal pairs + # neighbourhood rank (Thm B data): u_S is orthogonal to N(S) and u_S.u_S = 1, so rank N(S) <= 8 + ranks = {len(span_basis([u[T] for T in NB[S]])) for S in range(V)} + # controls: h = 8 admits no labelling (calibration); the same CNF with the distinctness clauses is satisfiable at 9 + t8 = Model(8) + s8 = Cadical153(bootstrap_with=t8.cl) + unsat8 = not s8.solve() + s8.delete() + assert unsat8, "control failed: an h = 8 labelling exists" + return dict(solutions=len(sols), gram_is_sussman=True, labels_distinct=True, incap_degree=56, + neighbourhood_ranks=sorted(ranks), h8_control_unsat=unsat8, vars=m.nv, clauses=len(m.cl), + seconds=round(time.monotonic() - t0, 1)), u + + +# ---------------------------------------------------------------------------------------------------------------- +# (b) k-dimensional planes on the full in-cap graph (from the local research files plsat.py and plsat2.py) +def _graph(): + adj = [set(NB[a]) for a in range(V)] + return adj + + +def max_clique8(adj): + import networkx as nx + g = nx.Graph() + g.add_nodes_from(range(V)) + g.add_edges_from((a, b) for a in range(V) for b in adj[a] if a < b) + best = max(nx.find_cliques(g), key=len) + return sorted(best) + + +class PlaneModel: + """k-dim planes, form I_r, clique C fixed to coordinate blocks. usage as plsat.py (local research).""" + + def __init__(s, k, r, adj, C, dist=False): + s.k, s.r, s.nv, s.cl = k, r, 1, [[1]] + s.T = 1 + n = len(adj) + s.n = n + idx = {c: i for i, c in enumerate(C)} + s.vec = {} + for T in range(n): + for j in range(k): + if T in idx: + s.vec[T, j] = [s.T if t == k * idx[T] + j else -s.T for t in range(r)] + else: + allowed = set(range(k * len(C), r)) + for c, i in idx.items(): + if c not in adj[T]: + allowed |= set(range(k * i, k * i + k)) + s.vec[T, j] = [s.new() if t in allowed else -s.T for t in range(r)] + for T in range(n): + if T in idx: + continue + for a in range(k): + for b in range(a, k): + s.bil(s.vec[T, a], s.vec[T, b], 1 if a == b else 0) + ne = 0 + for S in range(n): + for T in adj[S]: + if S < T: + for a in range(k): + for b in range(k): + s.bil(s.vec[S, a], s.vec[T, b], 0) + ne += 1 + s.ne = ne + if dist: + assert k == 1 + for S in range(n): + for T in range(S + 1, n): + d = [s.xor2(x, y) for x, y in zip(s.vec[S, 0], s.vec[T, 0])] + d = [x for x in d if x != -s.T] + if s.T in d: + continue + s.cl.append(d) + + def new(s): + s.nv += 1 + return s.nv + + def and2(s, a, b): + T = s.T + if a == -T or b == -T: + return -T + if a == T: + return b + if b == T: + return a + y = s.new() + s.cl += [[-y, a], [-y, b], [y, -a, -b]] + return y + + def xor2(s, a, b): + T = s.T + if a == -T: + return b + if b == -T: + return a + if a == T: + return -b + if b == T: + return -a + y = s.new() + s.cl += [[-y, a, b], [-y, -a, -b], [y, -a, b], [y, a, -b]] + return y + + def xorl(s, lits): + acc = -s.T + for x in lits: + acc = s.xor2(acc, x) + return acc + + def bil(s, u, w, c): + terms = [s.and2(a, b) for a, b in zip(u, w)] + terms = [t for t in terms if t != -s.T] + acc = s.xorl(terms) + if acc == s.T: + if c == 0: + s.cl.append([]) + elif acc == -s.T: + if c == 1: + s.cl.append([]) + else: + s.cl.append([acc] if c else [-acc]) + + def labels(s, mod): + val = lambda x: (x == s.T) if abs(x) == s.T else (mod[abs(x) - 1] > 0) == (x > 0) # noqa: E731 + return {T: [sum(1 << t for t, x in enumerate(s.vec[T, j]) if val(x)) for j in range(s.k)] + for T in range(s.n)} + + +def calibrations(): + """Controls of the encoders: k = 1 (r = 8 UNSAT, r = 9 SAT, rank 9) and the k = 2 positive control at r = 18.""" + cal, C, L1 = _k1_calibration() + cal["k2_positive_control"] = _k2_positive_control(C, L1) + return cal + + +def _k1_calibration(): + """k = 1: r = 8 UNSAT, r = 9 SAT (rank 9, verified independently).""" + from pysat.solvers import Solver + adj = _graph() + C = max_clique8(adj) + out = {} + for r in (8, 9): + m = PlaneModel(1, r, adj, C, dist=False) + with Solver(name="cadical195", bootstrap_with=m.cl) as sol: + ok = sol.solve() + if ok: + L = {T: x[0] for T, x in m.labels(sol.get_model()).items()} + assert all(dot(L[T], L[T]) == 1 for T in range(V)) + assert all(dot(L[S], L[T]) == 0 for S in range(V) for T in adj[S]) + out[f"r{r}"] = dict(sat=True, rank=len(span_basis(list(L.values())))) + sol1 = L + else: + out[f"r{r}"] = dict(sat=False) + assert out["r8"] == dict(sat=False) and out["r9"] == dict(sat=True, rank=9) + return out, C, sol1 + + +def _k2_positive_control(C, L1): + """The k = 2 encoder at r = 18 accepts the direct sum of two copies of a k = 1, r = 9 labelling.""" + from pysat.solvers import Solver + adj = _graph() + m = PlaneModel(2, 18, adj, C) + + def emb(x, copy): + y = 0 + for t in range(9): + if x >> t & 1: + c = 2 * t + copy if t < 8 else 16 + copy + y |= 1 << c + return y + + L2 = {T: [emb(L1[T], 0), emb(L1[T], 1)] for T in range(V)} + # independent check of the direct sum: planes nondegenerate (I_2), orthogonal on all in-cap edges + assert all(dot(L2[T][0], L2[T][0]) == 1 and dot(L2[T][1], L2[T][1]) == 1 and dot(L2[T][0], L2[T][1]) == 0 + for T in range(V)) + assert all(dot(a, b) == 0 for S in range(V) for T in adj[S] for a in L2[S] for b in L2[T]) + assume = [] + for T in range(V): + for j in range(2): + for t, lit in enumerate(m.vec[T, j]): + bit = L2[T][j] >> t & 1 + if abs(lit) == m.T: + assert (lit > 0) == bool(bit), "direct sum violates the support rule of the encoder" + else: + assume.append(lit if bit else -lit) + with Solver(name="cadical195", bootstrap_with=m.cl) as sol: + ok = sol.solve(assumptions=assume) + assert ok, "control failed: encoder rejects the r = 18 direct sum" + return dict(r18_direct_sum_accepted=True, vars=m.nv, clauses=len(m.cl)) + + + +# any-type k = 2 encoder, one pattern of clique plane types (from plsat2.py) +_STATE = {} + + +def _init(): + if not _STATE: + adj = _graph() + _STATE["adj"] = adj + _STATE["C"] = max_clique8(adj) + + +class AnyTypePlanes: + def __init__(s, r, pat): + adj, C = _STATE["adj"], _STATE["C"] + idx = {c: i for i, c in enumerate(C)} + s.r = r + s.nv, s.cl, s.T, s.pat = 1, [[1]], 1, pat + s.vec, s.tau = {}, {} + for T in range(V): + if T in idx: + i = idx[T] + s.vec[T, 0] = [s.T if t == 2 * i else -s.T for t in range(r)] + s.vec[T, 1] = [s.T if t == 2 * i + 1 else -s.T for t in range(r)] + else: + al = set(range(16, r)) + for c, i in idx.items(): + if c not in adj[T]: + al |= {2 * i, 2 * i + 1} + for j in range(2): + s.vec[T, j] = [s.new() if t in al else -s.T for t in range(r)] + s.tau[T] = s.new() + p, q = s.vec[T, 0], s.vec[T, 1] + s.eq(s.form(p, p), -s.tau[T]) # tau = 0: plane I_2 (p.p = q.q = 1, p.q = 0) + s.eq(s.form(q, q), -s.tau[T]) # tau = 1: hyperbolic plane (p.p = q.q = 0, p.q = 1) + s.eq(s.form(p, q), s.tau[T]) + for S in range(V): + for T in adj[S]: + if S < T: + for a in range(2): + for b in range(2): + s.eq(s.form(s.vec[S, a], s.vec[T, b]), -s.T) + + def new(s): + s.nv += 1 + return s.nv + + def and2(s, a, b): + T = s.T + if a == -T or b == -T: + return -T + if a == T: + return b + if b == T: + return a + y = s.new() + s.cl += [[-y, a], [-y, b], [y, -a, -b]] + return y + + def xor2(s, a, b): + T = s.T + if a == -T: + return b + if b == -T: + return a + if a == T: + return -b + if b == T: + return -a + y = s.new() + s.cl += [[-y, a, b], [-y, -a, -b], [y, -a, b], [y, a, -b]] + return y + + def form(s, u, w): + terms = [] + for t in range(s.r): + if t < 16 and s.pat[t // 2] == "H": + terms.append(s.and2(u[t], w[t ^ 1])) + else: + terms.append(s.and2(u[t], w[t])) + acc = -s.T + for x in terms: + acc = s.xor2(acc, x) + return acc + + def eq(s, a, b): + x = s.xor2(a, b) + if x == s.T: + s.cl.append([]) + elif x != -s.T: + s.cl.append([-x]) + + +def _solve_patterns(args): + from pysat.solvers import Solver + r, pats = args + _init() + out = {} + for pat in pats: + f = AnyTypePlanes(r, pat) + with Solver(name="cadical195", bootstrap_with=f.cl) as sol: + out[pat] = sol.solve() + return out + + +def k2_tasks(r, n_chunks=32): + """Split the plane-type patterns of the clique into chunks (one CaDiCaL instance per pattern).""" + assert r in (16, 17) + pats = ["".join(b) for b in itertools.product("IH", repeat=8)] + if r == 16: + pats.remove("H" * 8) # an alternating window form is not the dot product + return [(r, pats[i::n_chunks]) for i in range(n_chunks)], len(pats) + + +def k2_solve(args): + return _solve_patterns(args) + + +def k2_collect(r, parts, npats): + res = {} + for part in parts: + res.update(part) + assert len(res) == npats + assert sum(res.values()) == 0, f"k = 2 planes found at r = {r}" + return dict(r=r, patterns=npats, sat=0) + + +def e8_clique_facts(): + """Clique structure of the in-cap graph: omega = 8, 8640 maximal cliques of size 8 (each is an orthonormal basis).""" + import networkx as nx + adj = _graph() + g = nx.Graph() + g.add_nodes_from(range(V)) + g.add_edges_from((a, b) for a in range(V) for b in adj[a] if a < b) + sizes = {} + for q in nx.find_cliques(g): + sizes[len(q)] = sizes.get(len(q), 0) + 1 + assert max(sizes) == 8 + return dict(vertices=V, edges=g.number_of_edges(), degree=56, omega=max(sizes), maximal_cliques_by_size= + {str(k): sizes[k] for k in sorted(sizes)}) diff --git a/research/format-obstructions/checks/toy.py b/research/format-obstructions/checks/toy.py new file mode 100644 index 0000000000..2d7765dbe8 --- /dev/null +++ b/research/format-obstructions/checks/toy.py @@ -0,0 +1,128 @@ +"""The p = 3 toy: the one place where a read-discipline change beats gx's E2 (all targets at frame 0 at the scatter). + +Instance: inputs/gcert1-p3-cone-R16.json (paired cube p = 3, h = 6, v = 8, R = 16, cst = 18), accepted by gx.check1. +Its 8 ports span W of dimension 4, and the window form restricted to W is DEGENERATE: W^perp (dim 2) lies in W. +Modified rule E2': the scatter is done in cuts. At a cut, all targets stand at ONE common frame g contained in every +target's final q^perp (so g <= W^perp), and copying total k costs d(f_k, g) = dim f + dim g - 2 dim(f cap g). +Exact checks (all F_2 / integer): every register chain is nested, equal frames at every gate, targets stay inside +q^perp and avoid q, the block-mass identity, the scalar half (gates and coefficients unchanged), and the exhaustive +optimum over all chains of cut frames. Control: a cut frame outside the radical is rejected. +""" +import itertools +import sys +from pathlib import Path + +ROOT = Path(__file__).resolve().parent.parent +sys.path.insert(0, str(ROOT / "gx")) +sys.path.insert(0, str(ROOT / "checks")) +import gx # noqa: E402 +from certs import load # noqa: E402 +from f2 import dot, rank # noqa: E402 + + +def span(gens): + b = [] + for u in gens: + for x in b: + if u ^ x < u: + u ^= x + if u: + b.append(u) + b.sort(reverse=True) + return tuple(b) + + +def inside(a, b): + return all(gx.reduce(u, b) == 0 for u in a) + + +def run(): + c = load(ROOT / "inputs" / "gcert1-p3-cone-R16.json") + gx.check1(c) + h, v, R = c["h"], c["v"], c["R"] + nreg = 2 * v + R + ports = c["ports"] + fr = [tuple(f) for f in c["frames"]] + assert not c["ext"] + + def d(f, g): + both = span([x for x in range(1, 1 << h) if gx.reduce(x, f) == 0 and gx.reduce(x, g) == 0]) + return len(f) + len(g) - 2 * len(both) + + # geometry of the ports: W = span, W^perp, radical + W = span(ports) + perpW = [x for x in range(1 << h) if all(dot(x, q) == 0 for q in ports)] + rad_nonzero = sorted(x for x in perpW if x) + assert len(W) == 4 and len(perpW) == 4 and all(gx.reduce(x, W) == 0 for x in perpW) # W^perp lies in W: radical + L = 0b111100 + assert L in rad_nonzero and all(dot(L, q) == 0 for q in ports) + + cur = [fr[s] for s in c["start"]] + mass = 0 + + def climb(r, f): + nonlocal mass + if cur[r] != f: + assert inside(cur[r], f), ("not nested", r) + mass += len(f) - len(cur[r]) + cur[r] = f + + for g in c["A"]: + regs, _, _ = gx.gate_regs(g) + for r in regs: + climb(r, fr[g[1]]) + tot = {k: (s, fr[f]) for k, s, f in c["ret"]} + for k, (s, f) in tot.items(): + assert cur[s] == f + assert all(cur[v + t] == () for t in range(v)) + old_cst = sum(len(f) for _, f in tot.values()) + assert old_cst == c["cst"] == 18 + cut1 = [k for k in tot if gx.reduce(L, tot[k][1]) != 0] # totals not containing l: read at g = 0 + cut2 = [k for k in tot if gx.reduce(L, tot[k][1]) == 0] # totals containing l: read at g = + cst = sum(d(tot[k][1], ()) for k in cut1) + for t in range(v): + climb(v + t, span([L])) # the targets climb to the common frame l + cst += sum(d(tot[k][1], span([L])) for k in cut2) + for g in c["B"]: + regs, _, _ = gx.gate_regs(g) + f = span(list(fr[g[1]]) + [L]) + for r in regs: + climb(r, f) + for r in range(nreg): + fin = fr[c["final"][r]] + climb(r, span(list(fin) + ([L] if r >= v else [])) if r < v or r >= 2 * v else fin) + for t in range(v): + assert inside(cur[v + t], fr[c["final"][v + t]]) and gx.reduce(ports[t], cur[v + t]) != 0 + assert mass == R * h + 2 * v * (h - 1), mass + gx.scal(c) # scalar half: gates and coefficients unchanged + + # exhaustive optimum over all chains of cut frames inside W^perp (targets only climb between cuts) + subs = [()] + [span([x]) for x in rad_nonzero] + [span(rad_nonzero)] + subs = [s for i, s in enumerate(subs) if s not in subs[:i]] + def leq(a, b): + return inside(a, b) + best, best_chain = None, None + old_format = None + for n in range(1, len(subs) + 1): + for chain in itertools.combinations(subs, n): + if not all(leq(a, b) or leq(b, a) for a in chain for b in chain): + continue + total = sum(min(d(f, g) for g in chain) for _, f in tot.values()) + if chain == ((),): + old_format = total + if best is None or total < best: + best, best_chain = total, chain + assert old_format == 18 and best == 16 == cst, (old_format, best, cst) + + # control: a common frame not inside W^perp would put a target outside q^perp + not_rad = [x for x in range(1, 1 << h) if x not in rad_nonzero] + ctrl = all(any(dot(x, q) for q in ports) for x in not_rad) + assert ctrl, "control failed" + # Thm C bound for this instance (degenerate span): lower bound of the pairing ranks + lb = sum(len(f) - 1 for _, f in tot.values()) + # on the nondegenerate families the gain is zero: W^perp = 0 forces g = 0 (window_rank = h in certs.py) + return dict(h=h, v=v, R=R, old_cst=old_cst, new_cst=cst, optimum_over_cut_chains=best, old_format_optimum=old_format, + cut1=sorted(cut1), cut2=sorted(cut2), line=bin(L), radical_nonzero=[bin(x) for x in rad_nonzero], + port_span_dim=len(W), moves_old=R * h + 2 * v * (h - 1) + old_cst, moves_new=mass + cst, + thmC_per_total_bound=lb, D_old=4 * v - 5 * old_cst, D_new=4 * v - 5 * cst, + cut_outside_radical_rejected=ctrl) diff --git a/research/format-obstructions/expected.json b/research/format-obstructions/expected.json new file mode 100644 index 0000000000..44faf6094e --- /dev/null +++ b/research/format-obstructions/expected.json @@ -0,0 +1,545 @@ +{ + "certificates": { + "p10": { + "N_rank": [ + 19, + 19 + ], + "R": 6515, + "check1": "PASS", + "copy_lb": 360, + "copy_paid": 360, + "coread_all": true, + "cst": 360, + "file": "gcert1-p10-anneal-mw-flow.json.gz", + "h": 20, + "incap_deg": [ + 620, + 620 + ], + "incap_perp": true, + "self_lossless": false, + "thmA_gate_checks": 1081204, + "thmA_violations": 0, + "v": 960, + "window_rank": 20 + }, + "p11": { + "N_rank": [ + 21, + 21 + ], + "R": 9412, + "check1": "PASS", + "copy_lb": 440, + "copy_paid": 440, + "coread_all": true, + "cst": 440, + "file": "gcert1-p11-pr193.json.gz", + "h": 22, + "incap_deg": [ + 884, + 884 + ], + "incap_perp": true, + "self_lossless": false, + "thmA_gate_checks": 2063837, + "thmA_violations": 0, + "v": 1320, + "window_rank": 22 + }, + "p3": { + "N_rank": [ + 3, + 3 + ], + "R": 16, + "check1": "PASS", + "controls": { + "corrupted_port_check1_rejects": "E1", + "corrupted_port_replay_violations": 14, + "shifted_labels_nonorthogonal_pairs": 12 + }, + "copy_lb": 12, + "copy_paid": 18, + "coread_all": true, + "cst": 18, + "file": "gcert1-p3-cone-R16.json", + "h": 6, + "incap_deg": [ + 4, + 4 + ], + "incap_perp": true, + "self_lossless": false, + "thmA_gate_checks": 110, + "thmA_violations": 0, + "v": 8, + "window_rank": 4 + } + }, + "e8_labels": { + "calibrations": { + "k2_positive_control": { + "clauses": 605809, + "r18_direct_sum_accepted": true, + "vars": 173825 + }, + "r8": { + "sat": false + }, + "r9": { + "rank": 9, + "sat": true + } + }, + "cliques": { + "degree": 56, + "edges": 3360, + "maximal_cliques_by_size": { + "3": 1120, + "7": 34560, + "8": 8640 + }, + "omega": 8, + "vertices": 120 + }, + "k2_planes": { + "r16": { + "patterns": 255, + "r": 16, + "sat": 0 + }, + "r17": { + "patterns": 256, + "r": 17, + "sat": 0 + } + }, + "uniqueness_h9": { + "clauses": 166685, + "gram_is_sussman": true, + "h8_control_unsat": true, + "incap_degree": 56, + "labels_distinct": true, + "neighbourhood_ranks": [ + 8 + ], + "solutions": 1, + "vars": 42645 + } + }, + "families": { + "e8_bitdual": { + "betas": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8 + ], + "copy_lb": 72, + "decoder_equals_UUt": true, + "h": 8, + "neighbourhood": [ + [ + 63, + 7 + ] + ], + "totals": 9, + "v": 120 + }, + "e8_complex": { + "N_rank": 8, + "h": 9, + "incap_deg": 56, + "v": 120 + }, + "omega": { + "bit_4": { + "h": 8, + "kind": "bit", + "omega": 4, + "p": 4 + }, + "bit_5": { + "h": 10, + "kind": "bit", + "omega": 5, + "p": 5 + }, + "bit_6": { + "h": 12, + "kind": "bit", + "omega": 6, + "p": 6 + }, + "bit_7": { + "h": 14, + "kind": "bit", + "omega": 7, + "p": 7 + }, + "cx_4": { + "h": 8, + "kind": "cx", + "omega": 8, + "p": 4 + }, + "cx_5": { + "h": 10, + "kind": "cx", + "omega": 8, + "p": 5 + }, + "cx_6": { + "h": 12, + "kind": "cx", + "omega": 12, + "p": 6 + }, + "cx_7": { + "h": 14, + "kind": "cx", + "omega": 12, + "p": 7 + } + }, + "p10_clique": { + "all_pairs_lossless_in_program": true, + "label_dim_sum_le": 20, + "orthonormal": true, + "size": 20, + "window_dim": 20 + }, + "paired_bit": { + "10": { + "N_rank": 19, + "h": 20, + "incap_deg": 339, + "p": 10, + "v": 960 + }, + "11": { + "N_rank": 21, + "h": 22, + "incap_deg": 435, + "p": 11, + "v": 1320 + }, + "4": { + "N_rank": 7, + "h": 8, + "incap_deg": 15, + "p": 4, + "v": 32 + }, + "5": { + "N_rank": 9, + "h": 10, + "incap_deg": 39, + "p": 5, + "v": 80 + } + } + }, + "mutable_425": { + "J_is_identity": true, + "K_nonzeros": 14246, + "S_K_nonzeros": 14582, + "S_b": 0.0009102159764952497, + "S_b_vs_b_percent": -13.24, + "S_exact_after_compensation": true, + "S_helpers": 904, + "S_helpers_formula": "R + b_x + b_y", + "S_local_hist": { + "1": 2472, + "2": 896, + "3": 168, + "4": 336, + "5": 392, + "8": 248, + "9": 8 + }, + "S_mass": 10128, + "S_uncompensated_rejected": true, + "S_z_restored": true, + "V_offdiag": 112, + "all_targets_at_frame0_at_cut": true, + "b": 0.001049104978040586, + "b_pre425": 0.000999388595603943, + "cst_bound": 72, + "cst_paid": 72, + "detector_on_converted_word": {}, + "detector_on_word_as_written": { + "source modified": 1640, + "target read": 112 + }, + "h": 9, + "helpers": 680, + "local_hist": { + "1": 2248, + "2": 896, + "3": 168, + "4": 336, + "5": 392, + "8": 24, + "9": 8 + }, + "m": 73, + "m_min_nine_stages": 73, + "mass": 8112, + "modified_sources": 112, + "omit_K_control_rejected": true, + "ports_realise_E8_gram": true, + "preconditioned_map_exact": true, + "read_targets": 112, + "registers": 920, + "sources_gathered_per_centre": [ + 57, + 57, + 57, + 57, + 57, + 57, + 57, + 57 + ], + "stats": { + "cut": 232, + "scale": 644, + "src_modified": 1640, + "target_read": 112 + }, + "target_neighbourhood_ranks": [ + 8 + ], + "thmA_violations": 0, + "v": 120, + "z_restored": true + }, + "pivots": { + "copy_count_p10": { + "forced_extra_copy_per_overlap": 10, + "frame_dims": [ + 18 + ], + "max_noncarrier_totals": 1, + "max_totals_containing_b": 9, + "totals": 20 + }, + "overlap_scan_p10": { + "candidates": 1160, + "h": 20, + "min_carriers": 5984, + "min_contaminated_registers": 8435, + "min_contaminated_targets": 960, + "min_port_rank_of_contaminated": 20, + "registers": 8435, + "slots": 6515, + "slots_with_gates": 6515 + }, + "thm_P": { + "p10": { + "K_solution_dim": 0, + "K_zero_gives_m_ge": "s*h, under (P1)-(P2)", + "cross_cube_slots": 5880, + "file": "gcert1-p10-anneal-mw-flow.json.gz", + "h": 20, + "h_squared": 400, + "rank_all_carried_pairs": 400, + "rank_orthogonal_pairs_only": 399, + "slot_written_targets_port_rank": 20, + "slots": 6515, + "writer_slots": 3708 + }, + "p11": { + "K_solution_dim": 0, + "K_zero_gives_m_ge": "s*h, under (P1)-(P2)", + "cross_cube_slots": 9180, + "file": "gcert1-p11-pr193.json.gz", + "h": 22, + "h_squared": 484, + "rank_all_carried_pairs": 484, + "rank_orthogonal_pairs_only": 483, + "slot_written_targets_port_rank": 22, + "slots": 9412, + "writer_slots": 4125 + } + } + }, + "pricing": { + "D": 24480, + "W": 131760, + "m": 100, + "per_stage_rank1_copy_percent": "-0.2457", + "per_stage_rank1_register_descent_percent": "-0.4911", + "pinned_root": "7.702769095630e-04", + "pivot_free_m96": { + "blocks 2->1": { + "with_40_forced_copy_percent": "+4.30", + "zero_cost_percent": "+6.39" + }, + "largest blocks shortened": { + "with_40_forced_copy_percent": "+1.53", + "zero_cost_percent": "+3.56" + }, + "mid blocks shortened": { + "with_40_forced_copy_percent": "+3.68", + "zero_cost_percent": "+5.75" + }, + "rank-1 blocks removed": { + "with_40_forced_copy_percent": "+5.99", + "zero_cost_percent": "+8.11" + } + }, + "root": "7.702769095630e-04" + }, + "thmB_table": { + "bit_p10": { + "s3": { + "layout_s_times_h": 60, + "m_min": 58 + }, + "s5": { + "layout_s_times_h": 100, + "m_min": 96 + }, + "s7": { + "layout_s_times_h": 140, + "m_min": 134 + }, + "s9": { + "layout_s_times_h": 180, + "m_min": 172 + } + }, + "bit_p11": { + "s3": { + "layout_s_times_h": 66, + "m_min": 64 + }, + "s5": { + "layout_s_times_h": 110, + "m_min": 106 + }, + "s7": { + "layout_s_times_h": 154, + "m_min": 148 + }, + "s9": { + "layout_s_times_h": 198, + "m_min": 190 + } + }, + "complex_p10": { + "s3": { + "layout_s_times_h": 60, + "m_min": 58 + }, + "s5": { + "layout_s_times_h": 100, + "m_min": 96 + }, + "s7": { + "layout_s_times_h": 140, + "m_min": 134 + }, + "s9": { + "layout_s_times_h": 180, + "m_min": 172 + } + }, + "complex_p11": { + "s3": { + "layout_s_times_h": 66, + "m_min": 64 + }, + "s5": { + "layout_s_times_h": 110, + "m_min": 106 + }, + "s7": { + "layout_s_times_h": 154, + "m_min": 148 + }, + "s9": { + "layout_s_times_h": 198, + "m_min": 190 + } + }, + "e8_bit_dual": { + "s3": { + "layout_s_times_h": 24, + "m_min": 22 + }, + "s5": { + "layout_s_times_h": 40, + "m_min": 36 + }, + "s7": { + "layout_s_times_h": 56, + "m_min": 50 + }, + "s9": { + "layout_s_times_h": 72, + "m_min": 64 + } + }, + "e8_complex": { + "s3": { + "layout_s_times_h": 27, + "m_min": 25 + }, + "s5": { + "layout_s_times_h": 45, + "m_min": 41 + }, + "s7": { + "layout_s_times_h": 63, + "m_min": 57 + }, + "s9": { + "layout_s_times_h": 81, + "m_min": 73 + } + } + }, + "toy_p3": { + "D_new": -48, + "D_old": -58, + "R": 16, + "cut1": [ + 2, + 3, + 4, + 5 + ], + "cut2": [ + 0, + 1 + ], + "cut_outside_radical_rejected": true, + "h": 6, + "line": "0b111100", + "moves_new": 192, + "moves_old": 194, + "new_cst": 16, + "old_cst": 18, + "old_format_optimum": 18, + "optimum_over_cut_chains": 16, + "port_span_dim": 4, + "radical_nonzero": [ + "0b1111", + "0b110011", + "0b111100" + ], + "thmC_per_total_bound": 12, + "v": 8 + } +} diff --git a/research/format-obstructions/gx/gx.py b/research/format-obstructions/gx/gx.py new file mode 100644 index 0000000000..6d14c0a976 --- /dev/null +++ b/research/format-obstructions/gx/gx.py @@ -0,0 +1,296 @@ +#!/usr/bin/python3 -I +"""gx.py. OWN code (imports nothing of port-producer, nothing outside). +(1) convert(c0): gcert/0 (port-producer's event list) -> gcert/1, the LEAN-FACING NORMAL FORM: + only the main phase (no read0 / undo / uninj: the invocation theorem derives the dirt gate and the undo + gate from the product), every gate an elementary fan-out or fan-in add, the 4x4 K block written as three + such adds plus a sign carried by one register, the star scatter as a table. +(2) check1(c1): the local decidable conditions of EXTENDED-CERT-SPEC.md on a gcert/1 file: + E0 sizes, E1 labels (nested subspaces by containment, equal frame at a gate), E2 scatter cut, + E3 shape (kinds of gates; X1; S1), E4 bracket rule S2, E5 scalar (x-content replay: hid and X3), + E6 price data (block histograms, N), E7 exterior gauges only (Q2). Raises AssertionError(": ..."). +""" +from fractions import Fraction as Fr +from collections import Counter +from math import lcm + + +def need(c, msg): + if not c: + raise AssertionError(msg) + + +def reduce(u, basis): + """basis: reduced echelon, pivot = leading bit, descending. Returns u modulo the span.""" + for b in basis: + if u >> (b.bit_length() - 1) & 1: + u ^= b + return u + + +def echelon_ok(f): + piv = [b.bit_length() - 1 for b in f] + if any(b == 0 for b in f) or piv != sorted(piv, reverse=True) or len(set(piv)) != len(piv): + return False + return all(not (b >> p & 1) for i, b in enumerate(f) for j, p in enumerate(piv) if i != j) + + +def inside(a, b): + return all(reduce(u, b) == 0 for u in a) + + +def par(x): + return bin(x).count("1") & 1 + + +KJ = [[[1, 2] if i == j else [-1, 2] for j in range(4)] for i in range(4)] + + +def convert(c0): + need(c0["format"] == "gcert/0", "input is not gcert/0") + v, h, R = c0["v"], c0["h"], c0["R"] + ev = c0["events"] + cen = [n for n, e in enumerate(ev) if e[0] == "centre"] + need(cen == list(range(cen[0], cen[0] + len(cen))), "centres are not contiguous: no single scatter cut") + A, B, ret = [], [], [] + neg = set() # x registers currently holding MINUS their value (between the two K blocks) + openq = {} + for n, e in enumerate(ev): + k = e[0] + out = A if n < cen[0] else B + if k in ("read0", "undo", "uninj"): + continue + if k == "inj": + need(e[2] not in neg, "inj reads a negated x register") + out.append(["out", e[3], e[2], [[e[1], 1, 1]], []]) + elif k == "op": + if e[3] == -1: + out.append(["neg", e[5], e[1]]) + else: + need(e[3] == 1, "op ca") + out.append(["out", e[5], e[2], [[e[1], e[4], 1]], []]) + elif k == "centre": + ret.append([e[2], e[1], e[3]]) + elif k == "gread": + hit = set(t for t, _, _ in e[3]) + out.append(["out", e[2], e[1], [[v + t, a, b] for t, a, b in e[3]], [v + t for t in e[4] if t not in hit]]) + elif k == "rread": + out.append(["out", e[2], e[1], [[v + t, a, b] for t, a, b in e[3]], []]) + elif k == "ysh": + out.append(["out", e[4], e[2], [[e[1], e[3], 1]], []]) + elif k == "yw": + out.append(["out", e[4], e[2], [[e[1], e[3][0], e[3][1]]], []]) + elif k == "kd": + out.append(["out", e[3], e[2], [[e[1], -1 if e[2] in neg else 1, 1]], []]) + elif k == "ktr": + q = tuple(e[1]) + need(e[2] == KJ, "ktr matrix is not 1 - J/2") + x1, rest = q[0], list(q[1:]) + if q not in openq: # first block: x := M x, register x1 keeps the sign + out.append(["in", e[3], x1, [[r, 1, 1] for r in rest]]) + out.append(["out", e[3], x1, [[r, -1, 2] for r in rest], []]) + out.append(["in", e[3], x1, [[r, 1, 1] for r in rest]]) + openq[q] = n + neg.add(x1) + else: # second block: the three adds undone in reverse order + out.append(["in", e[3], x1, [[r, -1, 1] for r in rest]]) + out.append(["out", e[3], x1, [[r, 1, 2] for r in rest], []]) + out.append(["in", e[3], x1, [[r, -1, 1] for r in rest]]) + del openq[q] + neg.discard(x1) + else: + raise AssertionError("unknown event kind %r" % k) + need(not openq and not neg, "a K block is not closed") + ext = sorted([z[3], z[1]] for z in c0["gauge"] if z[5]) + c1 = dict(format="gcert/1", derived_from=c0["name"] + " (gcert/0)", p=c0["p"], h=h, v=v, R=R, cst=c0["cst"], + N=c0["N"], ports=c0["ports"], frames=c0["frames"], start=c0["start"], final=c0["final"], + ext=ext, ret=sorted(ret), scat=dict(inside=c0["scat"]["inside"], outside=c0["scat"]["outside"]), + A=A, B=B, blocks=c0["blocks"]) + return c1 + + +def scat_row(c, t): + """the scatter of target t: [(k, coefficient)], from the table or from the star rule""" + sc = c["scat"] + if "table" in sc: + return [(k, Fr(a, b)) for k, a, b in sc["table"][t]] + sin, sout = Fr(*sc["inside"]), Fr(*sc["outside"]) + return [(k, sin if c["ports"][t] >> k & 1 else sout) for k in range(c["h"])] + + +def gate_regs(g): + if g[0] == "neg": + return [g[2]], [], [] + if g[0] == "out": + return [g[2]] + [t for t, _, _ in g[3]] + list(g[4]), [(t, g[2], Fr(a, b)) for t, a, b in g[3]], g[4] + if g[0] == "in": + return [g[2]] + [s for s, _, _ in g[3]], [(g[2], s, Fr(a, b)) for s, a, b in g[3]], [] + raise AssertionError("E0: unknown gate kind %r" % (g[0],)) + + +def check1(c, scalar=True, stats=None): + need(c.get("format") == "gcert/1", "E0: format") + h, v, R = c["h"], c["v"], c["R"] + nreg = 2 * v + R + ports, fr = c["ports"], [tuple(f) for f in c["frames"]] + need(len(ports) == v == len(set(ports)) and all(par(q) and 0 < q < 1 << h for q in ports), "E0: ports") + need(fr[0] == () and fr[1] == tuple(1 << i for i in range(h - 1, -1, -1)), "E0: frames 0 and 1") + need(all(echelon_ok(f) for f in fr) and len(set(fr)) == len(fr), "E0: frame table not reduced echelon / repeats") + dim = [len(f) for f in fr] + start, final = c["start"], c["final"] + need(len(start) == len(final) == nreg, "E0: start / final") + ext = {r: f for r, f in c["ext"]} + for t in range(v): + need(fr[start[t]] == (ports[t],) and final[t] == 1, "E1: x start / final") + f = fr[final[v + t]] + need(start[v + t] == 0 and len(f) == h - 1 and all(par(u & ports[t]) == 0 for u in f), "E1: y start / final") + for r in range(2 * v, nreg): + need(start[r] == ext.get(r, 0) and final[r] == 1, "E1: slot start / final") + cls = lambda r: "x" if r < v else "y" if r < 2 * v else "s" + cur = list(start) + H = {"x": Counter(), "y": Counter(), "s": Counter(), "c": Counter()} + steps = set() + + def climb(r, f, where): + o = cur[r] + if o != f: + if (o, f) not in steps: + need(dim[o] < dim[f] and inside(fr[o], fr[f]), "E1: step not nested (%s, register %d)" % (where, r)) + steps.add((o, f)) + H[cls(r)][dim[f] - dim[o]] += 1 + cur[r] = f + okind = {("x", "s"), ("s", "s"), ("s", "y"), ("x", "y"), ("x", "x"), ("y", "y")} + ysum, piv, ytg = Counter(), set(), set() + inc = 0 + for ph, gates in (("A", c["A"]), ("B", c["B"])): + if ph == "B": # ---- E2: the scatter cut + need(sorted(k for k, _, _ in c["ret"]) == list(range(len(c["ret"]))), "E2: retained totals numbered 0..") + if "table" in c["scat"]: + need(len(c["scat"]["table"]) == v and all(0 <= k < len(c["ret"]) for row in c["scat"]["table"] for k, _, _ in row), + "E2: scatter table") + else: + need(len(c["ret"]) == h, "E2: one retained total per coordinate (star rule)") + for k, s, f in c["ret"]: + need(cls(s) == "s" and cur[s] == f, "E2: retained slot %d is not at its frame" % s) + H["c"][dim[f]] += 1 + need(all(cur[v + t] == 0 for t in range(v)), "E2: a y role left frame 0 before the scatter") + for i, g in enumerate(gates): + regs, pairs, _ = gate_regs(g) + need(all(0 <= r < nreg for r in regs) and len(set(regs)) == len(regs), "E3: registers of gate %s%d" % (ph, i)) + inc += len(regs) + for r in regs: + climb(r, g[1], "%s%d" % (ph, i)) + for t, s, co in pairs: + kd = (cls(s), cls(t)) + need(kd in okind, "E3: gate kind %s -> %s (gate %s%d)" % (kd + (ph, i))) + need(ph == "B" or kd in {("x", "s"), ("s", "s")}, "E3: bank gate before the scatter (gate A%d)" % i) + if kd == ("y", "y"): + ysum[s, t] += co + piv.add(s) + ytg.add(t) + need(ph == "B" or all(cls(r) != "y" for r in regs), "E2: y role named in phase A") + for r in range(nreg): + climb(r, final[r], "final") + need(not (piv & ytg), "E4: a pivot is the target of a gate reading y") + need(all(x == 0 for x in ysum.values()), "E4: y-reads of a (pivot, target) pair do not cancel") + Hs = {k: {str(r): n for r, n in sorted(w.items())} for k, w in H.items()} + need(Hs == c["blocks"], "E6: block histograms") + N = sum(r * n for w in H.values() for r, n in w.items()) + tails = sum(dim[f] for f in ext.values()) + need(N == c["N"] and N + tails == R * h + 2 * v * (h - 1) + c["cst"], "E6: N") + if stats is not None: + stats.update(steps=len(steps), incidences=inc, blocks=sum(sum(w.values()) for w in H.values()), + step_work=sum(dim[a] * dim[b] for a, b in steps), ysh_pairs=len(ysum)) + if scalar: + scal(c, stats) + q2(c) + return True + + +def scal(c, stats=None): + """E5: exact replay of the x-content of every register through A, scatter, B.""" + h, v, R = c["h"], c["v"], c["R"] + nreg = 2 * v + R + reg = [({r: Fr(1)} if r < v else {}) for r in range(nreg)] + den = {"x": 1, "y": 1, "s": 1} + mx = {"x": Fr(0), "y": Fr(0), "s": Fr(0)} + cls = lambda r: "x" if r < v else "y" if r < 2 * v else "s" + + def axpy(t, src, co): + d = reg[t] + for k, u in src.items(): + w = d.get(k, 0) + co * u + if w: + d[k] = w + kk = cls(t) + if w.denominator != 1: + den[kk] = lcm(den[kk], w.denominator) + if abs(w) > mx[kk]: + mx[kk] = abs(w) + else: + d.pop(k, None) + + def run(gates): + for g in gates: + if g[0] == "neg": + reg[g[2]] = {k: -u for k, u in reg[g[2]].items()} + elif g[0] == "out": + src = dict(reg[g[2]]) + for t, a, b in g[3]: + axpy(t, src, Fr(a, b)) + else: + for s, a, b in g[3]: + axpy(g[2], reg[s], Fr(a, b)) + run(c["A"]) + tot = {k: dict(reg[s]) for k, s, _ in c["ret"]} + for t in range(v): + for k, co in scat_row(c, t): + axpy(v + t, tot[k], co) + run(c["B"]) + need(all(reg[t] == {t: 1} for t in range(v)), "E5: an x role is not restored (X3)") + need(all(reg[v + t] == {t: 1} for t in range(v)), "E5: a target does not receive exactly its source (hid)") + if stats is not None: + stats.update(den=dict(den), maxabs={k: str(x) for k, x in mx.items()}, + gates_A=len(c["A"]), gates_B=len(c["B"])) + + +def q2(c): + """E7 (only for files with exterior gauges, rule (2)): for every slot q that starts off the zero frame, the + column of q in the y rows of the product is zero (its dirt is removed in line, the derived dirt gate at + frame 0 does not touch it). Replay with the gauged slots as variables, x = 0.""" + h, v, R = c["h"], c["v"], c["R"] + ext = [r for r, _ in c["ext"]] + if not ext: + return True + reg = [dict() for _ in range(2 * v + R)] + for r in ext: + reg[r] = {r: Fr(1)} + + def axpy(t, src, co): + d = reg[t] + for k, u in src.items(): + w = d.get(k, 0) + co * u + if w: + d[k] = w + else: + d.pop(k, None) + + def run(gates): + for g in gates: + if g[0] == "neg": + reg[g[2]] = {k: -u for k, u in reg[g[2]].items()} + elif g[0] == "out": + src = dict(reg[g[2]]) + for t, a, b in g[3]: + axpy(t, src, Fr(a, b)) + else: + for s, a, b in g[3]: + axpy(g[2], reg[s], Fr(a, b)) + run(c["A"]) + tot = {k: dict(reg[s]) for k, s, _ in c["ret"]} + for t in range(v): + for k, co in scat_row(c, t): + if tot[k]: + axpy(v + t, tot[k], co) + run(c["B"]) + need(all(not reg[v + t] for t in range(v)), "E7: the dirt of an exterior-gauged slot reaches a y role (Q2)") + return True diff --git a/research/format-obstructions/inputs/gcert1-p10-anneal-mw-flow.json.gz b/research/format-obstructions/inputs/gcert1-p10-anneal-mw-flow.json.gz new file mode 100644 index 0000000000..7fa09bc275 Binary files /dev/null and b/research/format-obstructions/inputs/gcert1-p10-anneal-mw-flow.json.gz differ diff --git a/research/format-obstructions/inputs/gcert1-p11-pr193.json.gz b/research/format-obstructions/inputs/gcert1-p11-pr193.json.gz new file mode 100644 index 0000000000..a98026a72f Binary files /dev/null and b/research/format-obstructions/inputs/gcert1-p11-pr193.json.gz differ diff --git a/research/format-obstructions/inputs/gcert1-p3-cone-R16.json b/research/format-obstructions/inputs/gcert1-p3-cone-R16.json new file mode 100644 index 0000000000..8908f77525 --- /dev/null +++ b/research/format-obstructions/inputs/gcert1-p3-cone-R16.json @@ -0,0 +1 @@ +{"format": "gcert/1", "derived_from": "p3 cone-A + B0", "p": 0, "h": 6, "v": 8, "R": 16, "ports": [21, 37, 25, 41, 22, 38, 26, 42], "frames": [[], [32, 16, 8, 4, 2, 1], [21], [37], [25], [41], [22], [38], [26], [42], [37, 21], [25, 3], [41, 3], [38, 12], [21, 12], [37, 12], [22, 12], [21, 12, 3], [37, 21, 12], [38, 22], [37, 12, 3], [38, 22, 12], [37, 21, 12, 3], [41, 25, 3], [37, 21, 3], [21, 15], [42, 25], [37, 22], [51, 15], [38, 15], [38, 21, 15], [37, 22, 15], [35, 16, 9, 6], [33, 18, 11, 4], [33, 18, 8, 7], [34, 17, 11, 4], [33, 17, 8, 4, 3], [33, 16, 8, 5, 2], [34, 16, 10, 4, 1], [34, 16, 8, 6, 1], [32, 17, 8, 5, 2], [32, 17, 9, 4, 2], [33, 16, 9, 4, 2], [32, 18, 8, 6, 1], [32, 18, 10, 4, 1]], "start": [2, 3, 4, 5, 6, 7, 8, 9, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], "final": [1, 1, 1, 1, 1, 1, 1, 1, 40, 37, 41, 42, 43, 39, 44, 38, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], "ext": [], "ret": [[0, 16, 18], [1, 17, 21], [2, 18, 24], [3, 19, 23], [4, 20, 17], [5, 21, 20]], "scat": {"inside": [1, 3], "outside": [-1, 6]}, "A": [["out", 2, 0, [[26, -1, 1]], []], ["out", 2, 0, [[27, 1, 1]], []], ["out", 3, 1, [[16, 1, 1]], []], ["out", 3, 1, [[29, 1, 1]], []], ["out", 4, 2, [[20, 1, 1]], []], ["out", 4, 2, [[24, 1, 1]], []], ["out", 5, 3, [[19, 1, 1]], []], ["out", 5, 3, [[30, -1, 1]], []], ["out", 6, 4, [[22, 1, 1]], []], ["out", 7, 5, [[18, 1, 1]], []], ["out", 7, 5, [[25, -1, 1]], []], ["out", 8, 6, [[23, -1, 1]], []], ["out", 8, 6, [[31, 1, 1]], []], ["out", 9, 7, [[17, 1, 1]], []], ["out", 9, 7, [[21, 1, 1]], []], ["out", 10, 16, [[26, -1, 1]], []], ["out", 11, 20, [[23, -1, 1]], []], ["out", 12, 21, [[19, 1, 1]], []], ["out", 13, 25, [[17, -1, 1]], []], ["out", 14, 27, [[24, 1, 1]], []], ["out", 15, 30, [[29, -1, 1]], []], ["out", 16, 31, [[22, 1, 1]], []], ["out", 6, 4, [[28, 1, 1]], []], ["out", 17, 22, [[20, 1, 1]], []], ["out", 18, 24, [[30, -1, 1]], []], ["out", 19, 28, [[18, 1, 1]], []], ["out", 20, 29, [[25, -1, 1]], []], ["out", 21, 31, [[17, 1, 1]], []], ["out", 22, 22, [[29, -1, 1]], []], ["out", 23, 23, [[19, -1, 1]], []], ["out", 20, 25, [[21, -1, 1]], []], ["out", 24, 26, [[18, -1, 1]], []], ["out", 17, 27, [[20, 1, 1]], []], ["out", 21, 28, [[17, 1, 1]], []], ["out", 18, 30, [[16, -1, 1]], []]], "B": [["out", 8, 6, [[10, -1, 2]], []], ["out", 8, 6, [[9, 1, 2]], []], ["out", 8, 6, [[12, -1, 2]], []], ["out", 8, 6, [[15, 1, 2]], []], ["out", 25, 0, [[9, 1, 2]], []], ["out", 26, 2, [[7, 1, 1]], []], ["out", 27, 4, [[1, -1, 1]], []], ["out", 27, 4, [[11, 1, 2]], []], ["out", 25, 6, [[15, -1, 2]], []], ["out", 28, 13, [[14, -1, 1]], []], ["out", 25, 0, [[6, -1, 1]], []], ["out", 29, 5, [[3, -1, 1]], []], ["out", 26, 7, [[2, -1, 1]], []], ["out", 28, 8, [[14, 1, 1]], []], ["out", 25, 15, [[10, 1, 1]], []], ["out", 30, 0, [[5, 1, 1]], []], ["out", 30, 0, [[10, 1, 2]], []], ["out", 30, 0, [[12, -1, 2]], []], ["out", 30, 0, [[15, 1, 1]], []], ["out", 31, 1, [[8, -1, 2]], []], ["out", 31, 2, [[8, -1, 1]], []], ["out", 31, 2, [[14, -1, 1]], []], ["out", 30, 3, [[10, -1, 1]], []], ["out", 30, 3, [[15, -1, 2]], []], ["out", 31, 4, [[8, -1, 1]], []], ["out", 31, 4, [[14, -1, 1]], []], ["out", 31, 7, [[8, -1, 2]], []], ["out", 31, 7, [[14, -1, 1]], []], ["out", 31, 1, [[4, 1, 1]], []], ["out", 31, 2, [[4, -1, 1]], []], ["out", 31, 2, [[11, -1, 2]], []], ["out", 31, 2, [[14, 1, 2]], []], ["out", 30, 3, [[0, -1, 1]], []], ["out", 30, 3, [[9, -1, 1]], []], ["out", 30, 5, [[0, -1, 1]], []], ["out", 30, 5, [[9, -1, 1]], []], ["out", 31, 7, [[4, -1, 1]], []], ["out", 31, 7, [[11, -1, 1]], []], ["out", 31, 8, [[14, -1, 1]], []], ["out", 30, 12, [[9, 1, 1]], []], ["out", 31, 13, [[14, 1, 1]], []], ["out", 30, 15, [[10, -1, 1]], []], ["out", 32, 1, [[13, 1, 2]], []], ["out", 33, 2, [[14, 1, 2]], []], ["out", 34, 3, [[12, 1, 2]], []], ["out", 32, 4, [[13, -1, 2]], []], ["out", 35, 5, [[6, 1, 1]], []], ["out", 35, 5, [[15, -1, 2]], []], ["out", 33, 2, [[14, -1, 1]], []], ["out", 34, 3, [[0, 1, 1]], []], ["out", 32, 4, [[1, -1, 1]], []], ["out", 32, 4, [[7, 1, 1]], []], ["out", 32, 4, [[11, -1, 2]], []], ["out", 35, 5, [[15, 1, 1]], []], ["out", 35, 6, [[15, -1, 2]], []], ["out", 34, 12, [[9, -1, 1]], []], ["out", 36, 0, [[6, 1, 1]], []], ["out", 37, 3, [[9, 1, 1]], []], ["out", 38, 5, [[15, -1, 1]], []], ["out", 39, 7, [[13, 1, 2]], []], ["out", 36, 0, [[2, 1, 1]], []], ["out", 36, 0, [[6, -1, 1]], []], ["out", 39, 7, [[13, -1, 1]], []], ["out", 1, 3, [[1, -1, 1]], []], ["out", 1, 3, [[2, -1, 1]], []], ["out", 1, 4, [[1, 1, 1]], []], ["out", 1, 4, [[2, -1, 1]], []], ["out", 1, 5, [[0, 1, 1]], []], ["out", 1, 5, [[1, -1, 1]], []], ["out", 1, 7, [[2, 1, 1]], []], ["out", 1, 0, [[3, -1, 1]], []], ["out", 1, 0, [[4, -1, 1]], []], ["out", 1, 0, [[6, 1, 1]], []], ["out", 1, 0, [[7, -1, 1]], []], ["out", 1, 1, [[4, -1, 1]], []], ["out", 1, 1, [[7, -1, 1]], []], ["out", 1, 2, [[4, 1, 1]], []], ["out", 1, 5, [[3, 1, 1]], []], ["out", 1, 5, [[6, -1, 1]], []], ["out", 1, 0, [[1, 1, 1]], []], ["out", 1, 0, [[5, -1, 1]], []], ["out", 1, 3, [[1, 1, 1]], []], ["out", 1, 3, [[2, 1, 1]], []], ["out", 1, 3, [[7, -1, 1]], []], ["out", 1, 4, [[1, 1, 1]], []], ["out", 1, 4, [[7, -1, 1]], []]], "blocks": {"x": {"1": 34, "2": 3}, "y": {"1": 26, "2": 7}, "s": {"1": 50, "2": 2, "3": 14}, "c": {"3": 6}}, "N": 194, "cst": 18} \ No newline at end of file diff --git a/research/format-obstructions/inputs/pr425/FULL-WORD.json.gz b/research/format-obstructions/inputs/pr425/FULL-WORD.json.gz new file mode 100644 index 0000000000..28cb945cff Binary files /dev/null and b/research/format-obstructions/inputs/pr425/FULL-WORD.json.gz differ diff --git a/research/format-obstructions/inputs/pricing/cost.py b/research/format-obstructions/inputs/pricing/cost.py new file mode 100644 index 0000000000..677584c1c6 --- /dev/null +++ b/research/format-obstructions/inputs/pricing/cost.py @@ -0,0 +1,62 @@ +"""Fast exact cost evaluator for a five-stage banked bit core-block word. +Word format (PR249 snapshot): records = int32 six-tuples + MOVE (0, role, old_frame, new_frame, rank, z) + ADD (1, dst, src, coeff, frame, category) + COPY (2, center, temp, copy_frame, target_frame, rank) [paid child of given rank] + ERASE(3, ...) +""" +import json, struct, collections +import numpy as np +from mpmath import mp, mpf, findroot +mp.dps = 50 + +def load_snapshot(d): + s = json.load(open(f'{d}/249-states.json')) + fr = json.load(open(f'{d}/frames.json')) + dim = {int(k): len(v['B']) for k, v in fr['frames'].items()} + rec = np.frombuffer(open(f'{d}/249-records.bin','rb').read(), dtype=' 0: H[int(r[4])] += 1 + copies = rec[rec[:, 0] == 2] + for r in copies: + if r[5] > 0: H[int(r[5])] += 1 + init = s['initial'] + resid = sum(h - dim[init[str(r)]] for r in range(2 * v, n)) + return H, resid, v + +def five_stage(H, resid, v, h=24, stages=5): + m = stages * h + prof = collections.Counter() + for j, c in H.items(): prof[j] += stages * c + for j in (2*h - 2, h - 1, 2*h + 2, 4): prof[j] += 2 * v + W = mpf(4 * v) + mpf(resid) / h + mass = sum(j * c for j, c in prof.items()) + return prof, W, m, W * m - mass + +def solve_moment(prof, W, m, bad=mpf('1e-16')): + calls = sum(prof.values()) + items = [(mpf(j) / m, c) for j, c in prof.items()] + def mu(sv): + t = 1 - sv + return (sum(c * x ** t for x, c in items) + bad * 32 * m * m * calls * (mpf(1) / m) ** t) / W - 1 + return findroot(mu, mpf('0.0007')) + +def evaluate(rec, s, dim, h=24): + H, resid, v = local_profile(rec, s, dim, h) + prof, W, m, deficit = five_stage(H, resid, v, h) + sv = solve_moment(prof, W, m) + return dict(saving=sv, kappa_approx=sv / (1 + sv), W=W, deficit=deficit, m=m, + calls=sum(prof.values()), local=dict(sorted(H.items())), resid=resid) + +if __name__ == '__main__': + import sys + s, fr, dim, rec = load_snapshot(sys.argv[1]) + r = evaluate(rec, s, dim) + print({k: (float(v) if hasattr(v, 'real') and not isinstance(v, dict) else v) for k, v in r.items() if k != 'local'}) diff --git a/research/format-obstructions/inputs/pricing/hist_p10b.json b/research/format-obstructions/inputs/pricing/hist_p10b.json new file mode 100644 index 0000000000..f1ec3796b4 --- /dev/null +++ b/research/format-obstructions/inputs/pricing/hist_p10b.json @@ -0,0 +1 @@ +{"m": 100, "W": 131760, "histogram": {"1": 1284000, "10": 14880, "11": 4800, "12": 60360, "13": 120, "14": 20640, "16": 57600, "17": 152160, "18": 58800, "19": 23040, "2": 548940, "3": 363900, "38": 23040, "4": 104580, "42": 23040, "5": 65520, "6": 60360, "7": 38400, "8": 9840, "9": 17580}, "deficit": 24480, "bit_root": "385138454781521/500000000000000000", "kappa": "0.000769684039383334"} \ No newline at end of file diff --git a/research/format-obstructions/requirements.txt b/research/format-obstructions/requirements.txt new file mode 100644 index 0000000000..98c7bf4d74 --- /dev/null +++ b/research/format-obstructions/requirements.txt @@ -0,0 +1,4 @@ +python-sat==1.9.dev15 +networkx==3.7 +mpmath==1.3.0 +numpy==2.3.5 diff --git a/research/format-obstructions/verify.py b/research/format-obstructions/verify.py new file mode 100644 index 0000000000..10c5e574a2 --- /dev/null +++ b/research/format-obstructions/verify.py @@ -0,0 +1,213 @@ +#!/usr/bin/env python3 +"""Format obstructions: run every exact check behind PROOF.md, offline, from pinned inputs. + +usage: python3 -B research/format-obstructions/verify.py [--output DIR] [--jobs N] + +Requires Python 3.11+ (tested: 3.12) and the pinned packages of requirements.txt (python-sat for the CaDiCaL checks, +networkx, mpmath, numpy). Assertions must stay enabled (-O is refused). No network. The independent stages run in +a process pool; the result facts are compared with expected.json (every number below is pinned there). + +Stages (see README.md for what each one establishes): + certificates gx.check1 (Sussman's reference checker, vendored unchanged) on three gcert/1 programs, then Thm A (taint + replay, every gate), Cor A1, Thm B data (neighbourhood rank), Thm C (copy lower bound vs. paid); + negative controls on the small program. + toy_p3 the one read-discipline gain (cst 18 -> 16) and its exhaustive optimum; control. + pivots Theorem P (cross-Gram forced to zero), the copy count and the contamination scan of PROOF.md section 7. + mutable_425 PR #425's mutable-basis word: Thm A/B/C replays, exact scalar identity, Theorem S conversion; controls. + pricing the pinned pricer on the p = 10 bit histogram (pivot-free variants, copy and descent units). + families neighbourhood ranks and copy bounds for the port families, clique numbers, the explicit 20-clique. + e8_labels SAT: uniqueness of the h = 9 labelling, k = 2 planes UNSAT at r = 16, 17; calibrations and controls. +""" +import argparse +import hashlib +import importlib +import importlib.metadata as md +import json +import multiprocessing as mp +import os +import sys +import tempfile +import time +import traceback +from concurrent.futures import ProcessPoolExecutor, as_completed +from pathlib import Path + +if sys.flags.optimize: + raise SystemExit("Assertions must remain enabled: run without -O") +sys.dont_write_bytecode = True +os.environ["PYTHONDONTWRITEBYTECODE"] = "1" +ROOT = Path(__file__).resolve().parent +sys.path.insert(0, str(ROOT / "checks")) +sys.path.insert(0, str(ROOT / "gx")) + +PINNED_PACKAGES = {"python-sat": "1.9.dev15", "networkx": "3.7", "mpmath": "1.3.0", "numpy": "2.3.5"} +P10 = str(ROOT / "inputs" / "gcert1-p10-anneal-mw-flow.json.gz") +P11 = str(ROOT / "inputs" / "gcert1-p11-pr193.json.gz") + + +def sha(path): + return hashlib.sha256(Path(path).read_bytes()).hexdigest() + + +def package_files(): + return sorted(p.relative_to(ROOT).as_posix() for p in ROOT.rglob("*") if p.is_file() and "__pycache__" not in p.parts) + + +def integrity(): + pins = json.loads((ROOT / "SOURCE.json").read_text())["files"] + for rel, want in pins.items(): + assert sha(ROOT / rel) == want, "pinned input changed: " + rel + return len(pins) + + +def tasks(): + """(id, module, function, args). Long tasks first.""" + t = [ + ("cert_p11", "certs", "stage", ("p11",)), + ("cert_p10", "certs", "stage", ("p10",)), + ("overlap_p10", "pivots", "overlap_scan", (P10,)), + ("copy_count_p10", "pivots", "copy_count", (P10,)), + ("omega_cx_7", "families", "incap_omega", (7, "cx")), + ("thmP_p11", "pivots", "thm_P", (P11,)), + ("thmP_p10", "pivots", "thm_P", (P10,)), + ("cert_p3", "certs", "stage", ("p3",)), + ("toy_p3", "toy", "run", ()), + ("mutable_425", "mutable425", "run", ()), + ("pricing", "pricing", "run", ()), + ("e8_bitdual", "families", "e8_bitdual", ()), + ("p10_clique", "families", "p10_clique", (P10,)), + ("h9_unique", "sat_e8", "uniqueness_h9", ()), + ("calibrations", "sat_e8", "calibrations", ()), + ("e8_cliques", "sat_e8", "e8_clique_facts", ()), + ] + for p in (4, 5, 10, 11): + t.append((f"bit_p{p}", "families", "paired_bit", (p,))) + for p in (4, 5, 6, 7): + t.append((f"omega_bit_{p}", "families", "incap_omega", (p, "bit"))) + if p != 7: + t.append((f"omega_cx_{p}", "families", "incap_omega", (p, "cx"))) + sat = importlib.import_module("sat_e8") + npats = {} + for r in (16, 17): + chunks, n = sat.k2_tasks(r, 32) + npats[r] = n + for i, ch in enumerate(chunks): + t.append((f"k2_r{r}_{i}", "sat_e8", "k2_solve", (ch,))) + return t, npats + + +def work(spec): + mod, fn, args = spec + sys.dont_write_bytecode = True + t0 = time.monotonic() + out = getattr(importlib.import_module(mod), fn)(*args) + return out, time.monotonic() - t0 + + +def strip_seconds(x): + if isinstance(x, dict): + return {k: strip_seconds(v) for k, v in x.items() if k != "seconds"} + if isinstance(x, list): + return [strip_seconds(v) for v in x] + return x + + +def assemble(res, npats): + import families + import sat_e8 + f = {} + f["certificates"] = {k: res[f"cert_{k}"] for k in ("p3", "p10", "p11")} + f["toy_p3"] = res["toy_p3"] + f["pivots"] = dict(thm_P={"p10": res["thmP_p10"], "p11": res["thmP_p11"]}, copy_count_p10=res["copy_count_p10"], + overlap_scan_p10=res["overlap_p10"]) + f["mutable_425"] = res["mutable_425"] + f["pricing"] = res["pricing"] + u_res, u = res["h9_unique"] + fam = dict(paired_bit={str(p): res[f"bit_p{p}"] for p in (4, 5, 10, 11)}, e8_bitdual=res["e8_bitdual"], + e8_complex=families.e8_complex(u), p10_clique=res["p10_clique"], + omega={f"{k}_{p}": res[f"omega_{k}_{p}"] for p in (4, 5, 6, 7) for k in ("bit", "cx") + if f"omega_{k}_{p}" in res}) + f["families"] = fam + k2 = {} + for r in (16, 17): + parts = [res[f"k2_r{r}_{i}"] for i in range(32)] + k2[f"r{r}"] = sat_e8.k2_collect(r, parts, npats[r]) + f["e8_labels"] = dict(uniqueness_h9=u_res, calibrations=res["calibrations"], cliques=res["e8_cliques"], + k2_planes=k2) + # Thm B table, derived from the measured neighbourhood ranks: m >= 1 + s * rank N versus the layout widths s * h + tb = {} + for name, h, rank in (("complex_p10", 20, f["certificates"]["p10"]["N_rank"]), + ("complex_p11", 22, f["certificates"]["p11"]["N_rank"]), + ("bit_p10", 20, [fam["paired_bit"]["10"]["N_rank"]] * 2), + ("bit_p11", 22, [fam["paired_bit"]["11"]["N_rank"]] * 2), + ("e8_bit_dual", 8, [fam["e8_bitdual"]["neighbourhood"][0][1]] * 2), + ("e8_complex", 9, [fam["e8_complex"]["N_rank"]] * 2)): + assert rank == [h - 1, h - 1], (name, rank) + tb[name] = {f"s{s}": dict(m_min=1 + s * (h - 1), layout_s_times_h=s * h) for s in (3, 5, 7, 9)} + f["thmB_table"] = tb + return f + + +def main(): + ap = argparse.ArgumentParser(description=__doc__, formatter_class=argparse.RawDescriptionHelpFormatter) + ap.add_argument("--output", type=Path, help="new directory (outside the package) for facts.json / verification.json") + ap.add_argument("--jobs", type=int, default=max(1, min(12, (os.cpu_count() or 2)))) + ap.add_argument("--write-expected", action="store_true", help="maintenance: rewrite expected.json from this run") + args = ap.parse_args() + assert sys.version_info >= (3, 11), "Python 3.11+ required" + for pkg, ver in PINNED_PACKAGES.items(): + got = md.version(pkg) + assert got == ver, f"{pkg}=={ver} required, found {got} (python3 -m pip install -r requirements.txt)" + out = args.output or Path(tempfile.mkdtemp(prefix="format-obstructions-")) + if args.output: + assert not out.resolve().is_relative_to(ROOT) and not out.exists(), "output must be new and outside the package" + out.mkdir(parents=True) + before = package_files() + npins = integrity() + T0 = time.monotonic() + tk, npats = tasks() + res, secs = {}, {} + print(f"[{time.monotonic() - T0:6.1f}s] {npins} pinned inputs verified; {len(tk)} tasks on {args.jobs} workers", flush=True) + ctx = mp.get_context("spawn") + with ProcessPoolExecutor(max_workers=args.jobs, mp_context=ctx) as ex: + fut = {ex.submit(work, (m, fn, a)): tid for tid, m, fn, a in tk} + for f in as_completed(fut): + tid = fut[f] + try: + res[tid], secs[tid] = f.result() + except BaseException: + traceback.print_exc() + raise SystemExit(f"FAILED task {tid}") + if not tid.startswith("k2_") or len([k for k in res if k.startswith("k2_")]) % 16 == 0: + print(f"[{time.monotonic() - T0:6.1f}s] done {tid} ({secs[tid]:.1f}s)", flush=True) + facts = assemble(res, npats) + wall = time.monotonic() - T0 + norm = json.loads(json.dumps(strip_seconds(facts), sort_keys=True)) + exp_path = ROOT / "expected.json" + if args.write_expected: + exp_path.write_text(json.dumps(norm, indent=1, sort_keys=True) + "\n") + print("expected.json written") + else: + want = json.loads(exp_path.read_text()) + assert norm == want, "facts differ from expected.json: " + ", ".join( + k for k in sorted(set(norm) | set(want)) if norm.get(k) != want.get(k)) + after = package_files() + if args.write_expected: + after = [x for x in after if x != "expected.json"] + assert after == [x for x in before if not (args.write_expected and x == "expected.json")], \ + "the package tree changed during the run" + stage_secs = {} + for tid, s in secs.items(): + key = "k2_planes" if tid.startswith("k2_") else tid + stage_secs[key] = round(stage_secs.get(key, 0.0) + s, 1) + report = dict(status="PASS", python=sys.version.split()[0], packages=PINNED_PACKAGES, pinned_inputs=npins, + tasks=len(tk), jobs=args.jobs, wall_seconds=round(wall, 1), cpu_seconds_sum=round(sum(secs.values()), 1), + stage_cpu_seconds=dict(sorted(stage_secs.items(), key=lambda kv: -kv[1]))) + (out / "facts.json").write_text(json.dumps(facts, indent=1, sort_keys=True) + "\n") + (out / "verification.json").write_text(json.dumps(report, indent=1) + "\n") + print(json.dumps(report), flush=True) + print(f"PASS: all format-obstruction checks, wall {wall:.1f}s (output in {out})", flush=True) + + +if __name__ == "__main__": + main() diff --git a/research/joint-dual/SOURCE.json b/research/joint-dual/SOURCE.json index e3a8386b17..e1fbf9c5aa 100644 --- a/research/joint-dual/SOURCE.json +++ b/research/joint-dual/SOURCE.json @@ -3,9 +3,9 @@ "base_pr57_commit": "cd350f76c9bc01489ec83568bded532cb69be938", "base_pr58_commit": "bc2f7ed4c20dc18898305ab17165c0c995cbb804", "files": { - "Makefile": "768131bd4ce18433f6abccdc9812a38c92e11220e3a1019c6d95334b42f529d1", + "Makefile": "cd0fb59dc078d1fdf54a163ea13bb3660d03c8fe69c1a7f99fc8e5f476a3d5c2", "NOTICE": "b49022cb4104d90b182e4c335f670faf45529025b15db77bf0291835083c28bd", - "README.md": "d104c31d5b7e0d3a8d011a0e3517ab615e5b499b3dc05684f7ad3cadcd28bdae", + "README.md": "b81f8035b859007add6693c6d860371c9100a6766e494045495a28a457a5fcb9", "certificates/joint-dual-compiler.json": "516c4d85158553dabd0a98216a064b2a7397957a9d5dd0df1d6e5aec53a4e805", "certificates/joint-dual-profiles-23.json": "159fa8fee175fc1d24f63e72d3c2f1dc9f4fcd78b938c5e7d2f735fd0fd37209", "certificates/joint-dual-profiles-25.json": "8d190ce42d097e828c5756918c52f2963df576cf4c6600b0fc7f2b7fdb6ad223",