From 1db88eeb57f21689a8a8f025c2535f50b816414d Mon Sep 17 00:00:00 2001 From: Wentao Li Date: Sun, 18 Oct 2026 01:09:49 +0000 Subject: [PATCH] Prove no two-target UT4 central word has n_b=6 At equality the middle ranks are forced to (2,2), so the necessary abc=cba=I equations reduce to a two-role unrestricted-profile census; all 5400 rank-adequate GL2-minimal middles yield zero identity key pairs. Combined with #1662, every realizing word has n_b>=7. Leave n_b=7 open. No new kappa. Prepared by Wentao Li with substantial AI assistance. --- .../ut4-two-target-no-six-b/CERTIFICATE.json | 14 + research/ut4-two-target-no-six-b/PROOF.md | 129 +++++++++ research/ut4-two-target-no-six-b/README.md | 89 ++++++ research/ut4-two-target-no-six-b/SOURCES.json | 42 +++ research/ut4-two-target-no-six-b/TASK.json | 64 +++++ research/ut4-two-target-no-six-b/VERIFY.json | 24 ++ research/ut4-two-target-no-six-b/core.py | 245 +++++++++++++++++ .../ut4-two-target-no-six-b/independent.py | 256 ++++++++++++++++++ .../ut4-two-target-no-six-b/test_package.py | 138 ++++++++++ research/ut4-two-target-no-six-b/verify.py | 233 ++++++++++++++++ 10 files changed, 1234 insertions(+) create mode 100644 research/ut4-two-target-no-six-b/CERTIFICATE.json create mode 100644 research/ut4-two-target-no-six-b/PROOF.md create mode 100644 research/ut4-two-target-no-six-b/README.md create mode 100644 research/ut4-two-target-no-six-b/SOURCES.json create mode 100644 research/ut4-two-target-no-six-b/TASK.json create mode 100644 research/ut4-two-target-no-six-b/VERIFY.json create mode 100644 research/ut4-two-target-no-six-b/core.py create mode 100644 research/ut4-two-target-no-six-b/independent.py create mode 100644 research/ut4-two-target-no-six-b/test_package.py create mode 100644 research/ut4-two-target-no-six-b/verify.py diff --git a/research/ut4-two-target-no-six-b/CERTIFICATE.json b/research/ut4-two-target-no-six-b/CERTIFICATE.json new file mode 100644 index 0000000000..de27ff8b52 --- /dev/null +++ b/research/ut4-two-target-no-six-b/CERTIFICATE.json @@ -0,0 +1,14 @@ +{ + "active_roles": 2, + "canonical_zero_sum_middles": 5582, + "key_pairs_abc_cba_I": 0, + "keys_sum": 1568064, + "low_rank_excluded": 182, + "max_keys_per_middle": 1408, + "n_b": 6, + "rank_XY_at_least_2": 5400, + "schema_version": 1, + "side_zero_key_joins": 12544512, + "status": "no_nb6_two_target_quotient", + "targets": 2 +} diff --git a/research/ut4-two-target-no-six-b/PROOF.md b/research/ut4-two-target-no-six-b/PROOF.md new file mode 100644 index 0000000000..f8fca2067a --- /dev/null +++ b/research/ut4-two-target-no-six-b/PROOF.md @@ -0,0 +1,129 @@ +# No two-target UT4 central word has n_b = 6 + +In the formal group-algebra model of +[CrocSwap/integer-mult-bounds#1662](https://github.com/CrocSwap/integer-mult-bounds/pull/1662), +every legal word realizing two central targets satisfies `n_b >= 6`. This note +proves the complementary statement: + +> No legal word equal to `I+([z]+1)I_2`, of any finite length and on any finite +> restored dirty workspace, has exactly six paid `b` factors. + +The case `n_b = 7` is left open. There is no new κ; the selected decimal +`0.001672660197076918` is unchanged. + +## 1. Model and inherited rank bound + +Let `G = UT4(F2)` with `a = I+E12`, `b = I+E23`, `c = I+E34`, `z = I+E14`, and +work in `R = F2[G]`. On `r >= 2` roles a paid factor is +`I + ([g]+1) x y^T` with `g in {a,b,c}` and `x y^T` a nonzero binary rank-one +coupling (idempotent or nilpotent). The target is `T = I + ([z]+1) P` with +`P = diag(I_2, 0_(r-2))`. Scalar `GL_r(F2)` mixing is free and normalized into +the couplings; every occurrence, including restoration, is counted. + +Use the fixed 17-dimensional quotient + +``` +Q = F2/(a^2,b^2,c^2,ac-ca, deg >= 4) +``` + +of #1662, with `z |-> 1+abc+acb+bac+cba`. Necessary conditions on a realizing +word include vanishing of all degree-1/2 and non-target degree-3 coefficients +in `Mat_r(Q)`, and coefficient `P` on `abc, acb, bac, cba`. + +Write `B_j = x_j y_j^T` for the six middle couplings in product order, and set + +``` +X = [x_j] (r x 6), Y = [y_j^T] (6 x r). +``` + +#1662 gives `XY = 0` and `n_b >= 2 + rank X + rank Y` from the factorization of +`UV` through `ker X / im Y`, together with `rank X, rank Y >= 2` from the `bac` +and `acb` coefficients. At `n_b = 6` this forces + +``` +rank X = rank Y = 2. +``` + +In particular every middle coupling is supported on a fixed 2-dimensional +active plane `H` (after a free `GL_r` change of basis that places `P` in the +leading block). Write `e_b^x = e_b^y = 0` for this vanishing middle excess. + +## 2. Reduction to two active roles + +With all six `b`-couplings in `H x H`, an interior dirty contraction +`v_i(u_{i+1})` in a degree-`<=3` product can involve only `a` and `c` calls: +any factor that is a `b` call has zero dirty row and column, so contractions +against `b` see only the active block. Same-label dirty contractions between +two `a` calls (resp. two `c` calls) vanish in `R` because `([a]+1)^2 = 0` +(resp. `([c]+1)^2 = 0`). + +Consequently the monomials that use only `{a,b}` or only `{c,b}`, and the +cross monomials `abc` and `cba` (which never place `a` adjacent to `c`), +receive no interior dirty contribution. Their active `H x H` blocks are +exactly the two-role coefficients computed from: + +- the six active middle couplings (a zero-sum sequence in the nine nonzero + rank-one `2 x 2` matrices); +- the active prefix sums `P_j` of `a`-couplings before each middle call; +- the active suffix sums `Q_j` of `c`-couplings after each middle call. + +Unrestricted outer length means every 6-tuple of `2 x 2` matrices arises as +such a profile for some finite `n_a` (resp. `n_c`): each gap increment has +rank at most two and is a sum of at most two rank-one couplings. + +Therefore a realizing word with `n_b = 6` on any `r >= 2` yields a two-role +profile pair with + +``` +(ab, ba, aba, bab) = (0,0,0,0), +(cb, bc, cbc, bcb) = (0,0,0,0), +(abc, cba) = (I_2, I_2). +``` + +(The remaining target equations `acb = bac = I_2` are not needed for the +obstruction below.) + +## 3. Finite census on two roles + +Conjugation by `GL_2(F2)` fixes the two-role target `I_2` and acts on middle +sequences. There are 33,489 zero-sum length-6 sequences of nonzero rank-one +`2 x 2` matrices; they form 5,582 conjugation-minimal orbits (the same count +as in #1690 / #1816). Of these, 182 have `rank X < 2` or `rank Y < 2` and are +excluded by Section 1. The remaining **5,400** middles are searched. + +For each middle, the side-zero profiles are collected by a 3+3 meet-in-the-middle +on the packed side table of #1690. Each side-zero profile determines a +transport key `(U_0,U_1,W_0,W_1)` whose bits record `(P_j x_j)` and +`(y_j^T P_j)`. The identity cross condition `abc = cba = I_2` is exactly +the key-pairing equation of #1690 with target packing `9 = I_2`. + +**Result.** Across all 5,400 rank-adequate middles the set of side-zero keys +admits **zero** pairs with `abc = cba = I_2`. Certificate counts: + +| Quantity | Count | +|---|---:| +| Canonical zero-sum middles | 5,582 | +| With `rank X,Y >= 2` | 5,400 | +| Sum of side-zero key cardinalities | 1,568,064 | +| Key pairs with `abc = cba = I_2` | **0** | + +A low-rank control middle `(E_{11})^6` still produces many identity key pairs, +so the screen is not vacuous: the obstruction is the rank-2 constraint +together with the side-zero locus. + +## 4. Conclusion + +No two-role profile pair meets the necessary quotient conditions of Section 2. +By the dirty-contraction reduction, no word on any finite `r >= 2` with +`n_b = 6` reaches the degree-three quotient endpoint, hence none equals the +formal target. Combined with #1662's bound `n_b >= 6`, every legal two-target +word satisfies `n_b >= 7`. + +The value `n_b = 7` is not decided here. + +## Credit + +Model and separate-label bound: #1662 (@ToikY). Unit-tariff exactness and the +weighted open question that motivates this package: #1816. Profile/key pipeline: +#1690 (Aaron Wang / @navinor), as used by #1816. Workspace compression context: +#1680. Prepared by Wentao Li with substantial AI assistance. Apache-2.0. diff --git a/research/ut4-two-target-no-six-b/README.md b/research/ut4-two-target-no-six-b/README.md new file mode 100644 index 0000000000..3a07531197 --- /dev/null +++ b/research/ut4-two-target-no-six-b/README.md @@ -0,0 +1,89 @@ +# No two-target UT4 central word has n_b = 6 + +**Result.** In the explicit `F2[UT4(F2)]` central-target alphabet of +[CrocSwap/integer-mult-bounds#1662](https://github.com/CrocSwap/integer-mult-bounds/pull/1662), +no legal word realizing two central targets — of any finite length, on any +finite restored dirty workspace — has exactly six paid `b` calls. Every such +word therefore has `n_b >= 7`. The case `n_b = 7` is left open. + +No new κ. Selected decimal stays `0.001672660197076918`. + +This answers the `n_b = 6` half of open next question 2 in +[CrocSwap/integer-mult-bounds#1816](https://github.com/CrocSwap/integer-mult-bounds/pull/1816) +(`research/ut4-two-target-fifteen/`). + +## Why it matters + +#1662 prices labels separately: `n_a, n_c >= 4` and `n_b >= 6`, while the direct +word `(abcb)^2` per target uses `n_b = 8`. A realizing word with `n_b = 6` and +only modestly larger outer counts would beat the direct word whenever `β` is +large relative to `α+γ`. Ruling out `n_b = 6` at every length is the first +weighted-tariff step; `n_b = 7` remains the next gate. + +## Method + +[PROOF.md](PROOF.md) records the argument. At `n_b = 6` the middle quotient of +#1662 forces `rank X = rank Y = 2`, so every `b` coupling lies in the active +2-plane. Interior dirty contractions then cannot touch the `{a,b}` / `{c,b}` +side coefficients or the cross coefficients `abc` and `cba`. Those necessary +equations reduce to a two-role profile problem with unrestricted outer length +(every `2 x 2` profile is realizable with enough `a`/`c` calls). + +The census (self-contained in `core.py`, formulas matching #1690) enumerates +all 5,582 GL2-minimal zero-sum length-6 middle sequences, keeps the 5,400 with +both middle ranks at least two, builds every side-zero transport key via a 3+3 +meet-in-the-middle, and pairs keys for `abc = cba = I_2`. **Zero pairs survive.** +A low-rank control middle still produces pairs, so the screen is not empty by +accident. + +| Stage | Count | +|---|---:| +| Canonical zero-sum middles | 5,582 | +| `rank X,Y >= 2` | 5,400 | +| Sum of side-zero key-set sizes | 1,568,064 | +| Key pairs with `abc = cba = I_2` | **0** | + +## Evidence + +- `verify.py` (read-only, `need()` gates survive `python -O`): source pins; + corrupted temporary certificate and duplicate JSON key rejection; low-rank + positive control; full census against `CERTIFICATE.json`. +- `independent.py` does **not** import `verify.py`; it re-runs the census with + a separate base-16 half-profile MITM and matches the certificate. +- `test_package.py`: isolated `-O` read-only replay, independent import guard, + certificate pair corruption, duplicate keys, SOURCES sha drift. + +## Reproduce + +```sh +python3 -B scripts/research_package.py --package research/ut4-two-target-no-six-b +# Direct: +python3 -I -B research/ut4-two-target-no-six-b/verify.py +python3 -I -O -B research/ut4-two-target-no-six-b/independent.py +python3 -I -B research/ut4-two-target-no-six-b/test_package.py +``` + +## Open next questions + +1. **Does any two-target word have `n_b = 7`?** Why it matters: finishes the + first step of #1816 open question 2. First step: run the unrestricted-profile + key census for length-7 middles on rank patterns `(2,2)`, `(2,3)`, `(3,2)`, + or find an algebraic obstruction. Blocked by: `16^7` profiles, middle excess + when a middle rank is 3, and dirty-role structure beyond the `e_b = 0` + reduction used here. + +## Limits + +- Decides `n_b = 6` only; `n_b = 7` is explicitly open. +- Does not restate the unit-tariff minimum 16 from #1816; does not reopen + three-target lengths 21/22. +- Quotient-level obstruction (sufficient for the formal endpoint). No + proof-assistant or independent human review. No supplier or κ change. + +## Credit + +#1662 (@ToikY) for the model and `n_b >= 6` bound. #1816 for unit-tariff +exactness and the weighted open question. #1690 (Aaron Wang / @navinor) for +the profile/key pipeline, as used by #1816. #1680 for workspace context. +Prepared by Wentao Li `` with substantial AI assistance. +Apache-2.0. diff --git a/research/ut4-two-target-no-six-b/SOURCES.json b/research/ut4-two-target-no-six-b/SOURCES.json new file mode 100644 index 0000000000..01403aa1cc --- /dev/null +++ b/research/ut4-two-target-no-six-b/SOURCES.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + }, + { + "path": "research/bit-three-register-lower-bound/README.md", + "usage": "provenance", + "git_blob": "25e41c370c101a33a6deb978de08b03ed7539b79", + "sha256": "c12b33ef388deece0cbf891505a2ce2c0779a0c3a6cf1f0f7f7039bab59cbebd" + }, + { + "path": "research/ut4-central-tariff-relaxation/PROOF.md", + "usage": "provenance", + "git_blob": "8137274359979a786568da60bc802eeba2728e7f", + "sha256": "4820f0771cc6d5828492bf8cb0bacda2a74d3f00b58a02b8df056ab1db040f21" + }, + { + "path": "research/ut4-two-target-fifteen/README.md", + "usage": "provenance", + "git_blob": "3d314e22e7a9d1941269b161c833fbd3bcfc8934", + "sha256": "fb1026abcf357b5a409a2398eb18c9ae7c72541176dafa0b02c819b79e8f9b5f" + }, + { + "path": "research/ut4-two-target-r2/search.py", + "usage": "provenance", + "git_blob": "62c56bd121d6d06f4b781ba869ee82be0042f9ec", + "sha256": "eaa1380c62866acfcae77ab7e53ed30d7c4e4319978a446a6f3bb86b65920117" + } + ] +} diff --git a/research/ut4-two-target-no-six-b/TASK.json b/research/ut4-two-target-no-six-b/TASK.json new file mode 100644 index 0000000000..6742bdd9f5 --- /dev/null +++ b/research/ut4-two-target-no-six-b/TASK.json @@ -0,0 +1,64 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 3, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json", + "research/bit-gl3-mixed-targets-length10/README.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Construct the smallest exact identity in a newly specified legal operation alphabet.", + "Derive a target-specific relaxation bound for that same explicit alphabet." + ], + "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read Model section 1 of the three-register bound and identify the exact excluded free operations.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.", + "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.", + "allowed_variations": [ + "Choose a fixed larger register count or a specified nonabelian operation family." + ], + "scope_change_triggers": [ + "Remaining inside the already-excluded three-register abelian model.", + "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "refined", + "actual_scope": "In CrocSwap/integer-mult-bounds#1662's explicit F2[UT4(F2)] central-target alphabet (paid factors I+([g]+1)xy^T, g in {a,b,c}, target I+([z]+1)I_2), decide whether any legal two-target word of any finite length on any finite restored dirty workspace can have n_b=6. Leave n_b=7 open.", + "scope_change_reason": "Takes open next question 2 of https://github.com/CrocSwap/integer-mult-bounds/pull/1816 (research/ut4-two-target-fifteen): the first step toward weighted tariffs that could beat (abcb)^2 per target is to decide n_b=6 or 7 at any length. This package decides n_b=6 only.", + "bottleneck_link": "Separate-label bound n_b>=6 from #1662 sits below the direct word's n_b=8; excluding n_b=6 is the first weighted-tariff step. Screening/quotient result only; no supplier or kappa change. Selected decimal stays 0.001672660197076918.", + "budget_minutes": 60, + "stop_rule": "Stop after deciding n_b=6 (exhibit or prove none). Leave n_b=7 open. Do not reopen three-target lengths 21/22 or unit-tariff minimum 16.", + "outcome": "negative-result", + "evidence": "PROOF.md: at n_b=6 the middle ranks are forced to (2,2), so all six b-couplings lie in the active 2-plane; abc/cba and the a/b and c/b side coefficients receive no interior dirty contraction and reduce to the two-role profile equations. core.py/verify.py: all 5582 GL2-minimal zero-sum 6-middles; 5400 with rank X,Y>=2; every side-zero profile's transport keys; 0 pairs with abc=cba=I. independent.py repeats the census with a separate base-16 MITM. Low-rank control (1^6) still finds pairs, so the screen is not vacuous. n_b=7 left open.", + "author": "Wentao Li ", + "ai_assistance": "Substantial AI assistance in search design, proof writing, packaging and verification; no independent human review.", + "open_questions": [ + { + "question": "Does any two-target word have n_b=7 at any length and any finite dirty workspace?", + "why_it_matters": "Together with this n_b=6 exclusion, deciding n_b=7 would finish the first step of #1816 open question 2 on weighted tariffs versus (abcb)^2.", + "first_step": "Extend the unrestricted-profile key census to n_b=7 for rank patterns (2,2), (2,3) and (3,2), or find an algebraic obstruction.", + "blocked_by": "16^7 profiles and 49686 canonical length-7 middles; middle excess when rank X or Y is 3 needs a dirty-role argument beyond the e_b=0 reduction used here." + } + ] +} diff --git a/research/ut4-two-target-no-six-b/VERIFY.json b/research/ut4-two-target-no-six-b/VERIFY.json new file mode 100644 index 0000000000..5dee4005f0 --- /dev/null +++ b/research/ut4-two-target-no-six-b/VERIFY.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": ["{python}", "-I", "-B", "{package}/verify.py"], + "timeout_seconds": 180, + "checks": "Full n_b=6 rank-filtered middle census; zero abc=cba=I key pairs; source pins; corrupted temporary certificate and duplicate JSON key rejection; read-only." + }, + { + "argv": ["{python}", "-I", "-O", "-B", "{package}/independent.py"], + "timeout_seconds": 180, + "checks": "Separate base-16 half-profile MITM census matching CERTIFICATE.json; does not import verify.py." + }, + { + "argv": ["{python}", "-I", "-B", "{package}/test_package.py"], + "timeout_seconds": 600, + "checks": "Isolated -O read-only replay, independent import guard, certificate pair corruption, duplicate JSON keys." + } + ] +} diff --git a/research/ut4-two-target-no-six-b/core.py b/research/ut4-two-target-no-six-b/core.py new file mode 100644 index 0000000000..6ae422a41e --- /dev/null +++ b/research/ut4-two-target-no-six-b/core.py @@ -0,0 +1,245 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Self-contained two-role UT4(F2) profile/key primitives for the n_b=6 census. + +Reimplements the r=2 formulas of CrocSwap/integer-mult-bounds#1690 +(research/ut4-two-target-r2/search.py) needed here: rank-one couplings, +side tables, transport keys, and GL2-minimal zero-sum middle sequences. +Does not import that module. Prepared by Wentao Li with substantial AI +assistance. Apache-2.0. +""" +import itertools + +PAR = [bin(m).count("1") & 1 for m in range(64)] +_SOL = {} + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def mm(A, B, r=2): + out = 0 + for i in range(r): + for j in range(r): + s = 0 + for k in range(r): + s ^= (A >> (i * r + k)) & (B >> (k * r + j)) & 1 + out |= s << (i * r + j) + return out + + +def rank_one(x, y, r=2): + return sum( + 1 << (i * r + j) + for i in range(r) + for j in range(r) + if (x >> i) & 1 and (y >> j) & 1 + ) + + +def split(N, r=2): + rows = [(N >> (i * r)) & ((1 << r) - 1) for i in range(r)] + y = next(v for v in rows if v) + x = sum(1 << i for i, v in enumerate(rows) if v) + need(all(v in (0, y) for v in rows) and rank_one(x, y, r) == N, "not rank one") + return x, y + + +def diag(w, r): + return sum(1 << (i * r + i) for i in range(w)) + + +def couplings(r=2): + return [(x, y) for x in range(1, 1 << r) for y in range(1, 1 << r)] + + +def gl(r=2): + I = diag(r, r) + inv = {} + for g in range(1 << (r * r)): + for h in range(1 << (r * r)): + if mm(g, h, r) == I: + inv[g] = h + return inv + + +def side_tables(bseq, r=2): + tab = [] + for j, N in enumerate(bseq): + L = R = 0 + for i, M in enumerate(bseq): + if i < j: + L ^= M + elif i > j: + R ^= M + tab.append([ + mm(p, N, r) + | mm(N, p, r) << 4 + | mm(mm(p, N, r), p, r) << 8 + | (mm(mm(L, p, r), N, r) ^ mm(mm(N, p, r), R, r)) << 12 + for p in range(16) + ]) + return tab + + +def side_coeffs(bseq, P, r=2): + ab = ba = aba = bab = 0 + for j, (N, p) in enumerate(zip(bseq, P)): + pn = mm(p, N, r) + ab ^= pn + ba ^= mm(N, p, r) + aba ^= mm(pn, p, r) + for k in range(j + 1, len(bseq)): + bab ^= mm(mm(N, P[k] ^ p, r), bseq[k], r) + return ab, ba, aba, bab + + +def cross_coeffs(bseq, P, Q, r=2): + abc = cba = 0 + for N, p, q in zip(bseq, P, Q): + abc ^= mm(mm(p, N, r), q, r) + cba ^= mm(mm(q, N, r), p, r) + return abc, cba + + +def key(bseq, P): + U, W = [0, 0], [0, 0] + for j, (N, p) in enumerate(zip(bseq, P)): + x, y = split(N) + for s in range(2): + u = w = 0 + for k in range(2): + u ^= (p >> (2 * s + k)) & (x >> k) & 1 + w ^= (y >> k) & (p >> (2 * k + s)) & 1 + U[s] |= u << j + W[s] |= w << j + return U[0], U[1], W[0], W[1] + + +def key_cross(kp, kq): + abc = cba = 0 + for s in range(2): + for t in range(2): + abc |= PAR[kp[s] & kq[2 + t]] << (2 * s + t) + cba |= PAR[kq[s] & kp[2 + t]] << (2 * s + t) + return abc, cba + + +def _sol(u0, u1, e0, e1): + k = (u0, u1, e0, e1) + if k not in _SOL: + _SOL[k] = [m for m in range(64) if PAR[u0 & m] == e0 and PAR[u1 & m] == e1] + return _SOL[k] + + +def key_pairs(akeys, ckeys=None, target=(9, 9)): + ckeys = akeys if ckeys is None else ckeys + abc = target[0] + byW = {} + for k in ckeys: + byW.setdefault(k[2:], []).append(k) + for ka in akeys: + for m0 in _sol(ka[0], ka[1], abc & 1, abc >> 2 & 1): + for m1 in _sol(ka[0], ka[1], abc >> 1 & 1, abc >> 3 & 1): + for kc in byW.get((m0, m1), ()): + if key_cross(ka, kc) == target: + yield ka, kc + + +def middle_sequences(nb=6, symmetric=True, r=2): + inv = gl(r) + R1 = sorted(rank_one(x, y, r) for x, y in couplings(r)) + for bt in itertools.product(R1, repeat=nb): + tot = 0 + for N in bt: + tot ^= N + if tot: + continue + if symmetric and any( + tuple(mm(mm(g, N, r), h, r) for N in bt) < bt for g, h in inv.items() + ): + continue + yield bt + + +def ranks_XY(bseq, r=2): + xs, ys = [], [] + for N in bseq: + x, y = split(N, r) + xs.append(x) + ys.append(y) + + def rk(vecs): + rows = list(vecs) + rank = 0 + for bit in range(r): + piv = None + for i in range(rank, len(rows)): + if rows[i] >> bit & 1: + piv = i + break + if piv is None: + continue + rows[rank], rows[piv] = rows[piv], rows[rank] + for i in range(len(rows)): + if i != rank and rows[i] >> bit & 1: + rows[i] ^= rows[rank] + rank += 1 + return rank + + return rk(xs), rk(ys) + + +def side_zero_keys(bseq): + """Set of transport keys of all side-zero 6-profiles, via 3+3 MITM on keys.""" + need(len(bseq) == 6, "n_b=6 only") + tab = side_tables(bseq) + ktab = [] + for j, N in enumerate(bseq): + x, y = split(N) + row = [] + for p in range(16): + du = [0, 0] + dw = [0, 0] + for s in range(2): + u = w = 0 + for k in range(2): + u ^= (p >> (2 * s + k)) & (x >> k) & 1 + w ^= (y >> k) & (p >> (2 * k + s)) & 1 + du[s] = u + dw[s] = w + row.append((du[0], du[1], dw[0], dw[1])) + ktab.append(row) + left = {} + for p0 in range(16): + for p1 in range(16): + for p2 in range(16): + v = tab[0][p0] ^ tab[1][p1] ^ tab[2][p2] + u0 = ktab[0][p0][0] | (ktab[1][p1][0] << 1) | (ktab[2][p2][0] << 2) + u1 = ktab[0][p0][1] | (ktab[1][p1][1] << 1) | (ktab[2][p2][1] << 2) + w0 = ktab[0][p0][2] | (ktab[1][p1][2] << 1) | (ktab[2][p2][2] << 2) + w1 = ktab[0][p0][3] | (ktab[1][p1][3] << 1) | (ktab[2][p2][3] << 2) + left.setdefault(v, set()).add((u0, u1, w0, w1)) + keys = set() + joins = 0 + for p3 in range(16): + for p4 in range(16): + for p5 in range(16): + v = tab[3][p3] ^ tab[4][p4] ^ tab[5][p5] + L = left.get(v) + if not L: + continue + ru0 = ktab[3][p3][0] | (ktab[4][p4][0] << 1) | (ktab[5][p5][0] << 2) + ru1 = ktab[3][p3][1] | (ktab[4][p4][1] << 1) | (ktab[5][p5][1] << 2) + rw0 = ktab[3][p3][2] | (ktab[4][p4][2] << 1) | (ktab[5][p5][2] << 2) + rw1 = ktab[3][p3][3] | (ktab[4][p4][3] << 1) | (ktab[5][p5][3] << 2) + for u0, u1, w0, w1 in L: + joins += 1 + keys.add((u0 | (ru0 << 3), u1 | (ru1 << 3), w0 | (rw0 << 3), w1 | (rw1 << 3))) + return keys, joins + + +def count_key_pairs(keys, target=(9, 9)): + return sum(1 for _ in key_pairs(list(keys), list(keys), target)) diff --git a/research/ut4-two-target-no-six-b/independent.py b/research/ut4-two-target-no-six-b/independent.py new file mode 100644 index 0000000000..1804b6f555 --- /dev/null +++ b/research/ut4-two-target-no-six-b/independent.py @@ -0,0 +1,256 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Independent n_b=6 key-pair census (does not import verify.py). + +Rebuilds side-zero transport keys by enumerating profile halves as integer +base-16 digits rather than nested loops, then pairs keys for abc=cba=I. +Prepared by Wentao Li with substantial AI assistance. Apache-2.0. +""" +from concurrent.futures import ProcessPoolExecutor +from hashlib import sha256 +import json +from pathlib import Path + +# Local copy of the minimal primitives — no import of verify.py. +PAR = [bin(m).count("1") & 1 for m in range(64)] +_SOL = {} +HERE = Path(__file__).resolve().parent +PASS = "PASS_UT4_TWO_TARGET_NO_NB6_INDEPENDENT" + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def mm(A, B, r=2): + out = 0 + for i in range(r): + for j in range(r): + s = 0 + for k in range(r): + s ^= (A >> (i * r + k)) & (B >> (k * r + j)) & 1 + out |= s << (i * r + j) + return out + + +def rank_one(x, y, r=2): + return sum( + 1 << (i * r + j) + for i in range(r) + for j in range(r) + if (x >> i) & 1 and (y >> j) & 1 + ) + + +def split(N, r=2): + rows = [(N >> (i * r)) & ((1 << r) - 1) for i in range(r)] + y = next(v for v in rows if v) + x = sum(1 << i for i, v in enumerate(rows) if v) + return x, y + + +def diag(w, r): + return sum(1 << (i * r + i) for i in range(w)) + + +def side_tables(bseq, r=2): + tab = [] + for j, N in enumerate(bseq): + L = R = 0 + for i, M in enumerate(bseq): + if i < j: + L ^= M + elif i > j: + R ^= M + tab.append([ + mm(p, N, r) + | mm(N, p, r) << 4 + | mm(mm(p, N, r), p, r) << 8 + | (mm(mm(L, p, r), N, r) ^ mm(mm(N, p, r), R, r)) << 12 + for p in range(16) + ]) + return tab + + +def key_cross(kp, kq): + abc = cba = 0 + for s in range(2): + for t in range(2): + abc |= PAR[kp[s] & kq[2 + t]] << (2 * s + t) + cba |= PAR[kq[s] & kp[2 + t]] << (2 * s + t) + return abc, cba + + +def _sol(u0, u1, e0, e1): + k = (u0, u1, e0, e1) + if k not in _SOL: + _SOL[k] = [m for m in range(64) if PAR[u0 & m] == e0 and PAR[u1 & m] == e1] + return _SOL[k] + + +def ranks_XY(bseq, r=2): + xs, ys = [], [] + for N in bseq: + x, y = split(N, r) + xs.append(x) + ys.append(y) + + def rk(vecs): + rows = list(vecs) + rank = 0 + for bit in range(r): + piv = None + for i in range(rank, len(rows)): + if rows[i] >> bit & 1: + piv = i + break + if piv is None: + continue + rows[rank], rows[piv] = rows[piv], rows[rank] + for i in range(len(rows)): + if i != rank and rows[i] >> bit & 1: + rows[i] ^= rows[rank] + rank += 1 + return rank + + return rk(xs), rk(ys) + + +def gl_inv(r=2): + I = diag(r, r) + return { + g: h + for g in range(1 << (r * r)) + for h in range(1 << (r * r)) + if mm(g, h, r) == I + } + + +def canonical_middles(nb=6, r=2): + inv = gl_inv(r) + R1 = sorted( + rank_one(x, y, r) + for x in range(1, 1 << r) + for y in range(1, 1 << r) + ) + out = [] + for bt in __import__("itertools").product(R1, repeat=nb): + tot = 0 + for N in bt: + tot ^= N + if tot: + continue + if any(tuple(mm(mm(g, N, r), h, r) for N in bt) < bt for g, h in inv.items()): + continue + out.append(bt) + return out + + +def keys_for_middle(bseq): + """Enumerate profile halves as base-16 integers 0..4095.""" + tab = side_tables(bseq) + kcontrib = [] + for j, N in enumerate(bseq): + x, y = split(N) + row = [] + for p in range(16): + bits = [0, 0, 0, 0] + for s in range(2): + u = w = 0 + for k in range(2): + u ^= (p >> (2 * s + k)) & (x >> k) & 1 + w ^= (y >> k) & (p >> (2 * k + s)) & 1 + bits[s] = u + bits[2 + s] = w + row.append(bits) + kcontrib.append(row) + left = {} + for code in range(16 ** 3): + p0, p1, p2 = code & 15, (code >> 4) & 15, (code >> 8) & 15 + v = tab[0][p0] ^ tab[1][p1] ^ tab[2][p2] + partial = [0, 0, 0, 0] + for t in range(4): + partial[t] = ( + kcontrib[0][p0][t] + | (kcontrib[1][p1][t] << 1) + | (kcontrib[2][p2][t] << 2) + ) + left.setdefault(v, set()).add(tuple(partial)) + keys = set() + joins = 0 + for code in range(16 ** 3): + p3, p4, p5 = code & 15, (code >> 4) & 15, (code >> 8) & 15 + v = tab[3][p3] ^ tab[4][p4] ^ tab[5][p5] + L = left.get(v) + if not L: + continue + right = [0, 0, 0, 0] + for t in range(4): + right[t] = ( + kcontrib[3][p3][t] + | (kcontrib[4][p4][t] << 1) + | (kcontrib[5][p5][t] << 2) + ) + for partial in L: + joins += 1 + keys.add(tuple(partial[t] | (right[t] << 3) for t in range(4))) + return keys, joins + + +def count_pairs(keys): + byW = {} + for k in keys: + byW.setdefault(k[2:], []).append(k) + n = 0 + for ka in keys: + for m0 in _sol(ka[0], ka[1], 1, 0): # abc=9 bits + for m1 in _sol(ka[0], ka[1], 0, 1): + for kc in byW.get((m0, m1), ()): + if key_cross(ka, kc) == (9, 9): + n += 1 + return n + + +def worker(bt): + keys, joins = keys_for_middle(bt) + return joins, len(keys), count_pairs(keys) + + +def read_json(path): + def pairs(items): + obj = {} + for k, v in items: + need(k not in obj, "duplicate JSON key: " + k) + obj[k] = v + return obj + + return json.loads(path.read_text(), object_pairs_hook=pairs) + + +def main(): + # Refuse to import verify.py (static guard for reviewers / tests). + need("verify" not in globals(), "must not bind verify") + cert = read_json(HERE / "CERTIFICATE.json") + all_m = canonical_middles() + good = [bt for bt in all_m if ranks_XY(bt)[0] >= 2 and ranks_XY(bt)[1] >= 2] + need(len(all_m) == cert["canonical_zero_sum_middles"], "canonical count") + need(len(good) == cert["rank_XY_at_least_2"], "rank filter count") + tot_join = tot_keys = tot_kp = 0 + max_keys = 0 + with ProcessPoolExecutor(max_workers=4) as pool: + for joins, nk, kp in pool.map(worker, good, chunksize=20): + tot_join += joins + tot_keys += nk + tot_kp += kp + max_keys = max(max_keys, nk) + need(tot_kp == 0, "independent census found an I-pair") + need(tot_keys == cert["keys_sum"], "keys_sum mismatch") + need(tot_join == cert["side_zero_key_joins"], "join count mismatch") + need(max_keys == cert["max_keys_per_middle"], "max keys mismatch") + need(cert["key_pairs_abc_cba_I"] == 0, "certificate claims pairs") + print(PASS, "key_pairs=0", "keys_sum=" + str(tot_keys)) + + +if __name__ == "__main__": + main() diff --git a/research/ut4-two-target-no-six-b/test_package.py b/research/ut4-two-target-no-six-b/test_package.py new file mode 100644 index 0000000000..11872cc805 --- /dev/null +++ b/research/ut4-two-target-no-six-b/test_package.py @@ -0,0 +1,138 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Relocation, -O/need, certificate corruption and independent-import controls.""" +import hashlib +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile + +HERE = Path(__file__).resolve().parent + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def inventory(root): + return { + str(p.relative_to(root)): hashlib.sha256(p.read_bytes()).hexdigest() + for p in root.rglob("*") + if p.is_file() + } + + +def main(): + checks = [] + with tempfile.TemporaryDirectory(prefix="nb6-pkg-") as directory: + target = Path(directory) / "isolated-package" + shutil.copytree( + HERE, + target, + ignore=shutil.ignore_patterns("__pycache__", "*.pyc", "*.txt"), + ) + + # Keep cwd at the repository root so live SOURCES inputs resolve. + repo = HERE.parents[1] + + def run(script="verify.py", expected_error=None): + result = subprocess.run( + [sys.executable, "-I", "-O", "-B", str(target / script)], + cwd=str(repo), + text=True, + capture_output=True, + timeout=300, + ) + if expected_error is None: + need( + result.returncode == 0 + and "PASS_UT4_TWO_TARGET_NO_NB6" in result.stdout, + "isolated replay failed: " + result.stderr + result.stdout, + ) + else: + need( + result.returncode != 0 + and expected_error in (result.stderr + result.stdout), + "corruption escaped or wrong reason: " + result.stderr, + ) + + before = inventory(target) + for path in target.rglob("*"): + if path.is_file(): + path.chmod(0o444) + run() + need(inventory(target) == before, "normal replay mutated the isolated package") + checks.append("isolated-optimized-read-only-replay") + for path in target.rglob("*"): + if path.is_file(): + path.chmod(0o644) + + result = subprocess.run( + [sys.executable, "-I", "-O", "-B", str(target / "independent.py")], + cwd=str(repo), + text=True, + capture_output=True, + timeout=300, + ) + need( + result.returncode == 0 + and "PASS_UT4_TWO_TARGET_NO_NB6_INDEPENDENT" in result.stdout, + "independent failed: " + result.stderr, + ) + import ast + + tree = ast.parse((target / "independent.py").read_text()) + for node in ast.walk(tree): + if isinstance(node, ast.Import): + need(all(a.name.split(".")[0] != "verify" for a in node.names), + "independent imports verify") + if isinstance(node, ast.ImportFrom) and node.module: + need(node.module.split(".")[0] != "verify", "independent imports verify") + checks.append("independent-no-verify-import") + + def mutate(name, filename, edit, message): + path = target / filename + saved = path.read_bytes() + path.write_bytes(edit(saved)) + try: + run(expected_error=message) + checks.append(name) + finally: + path.write_bytes(saved) + + def json_edit(data, edit): + obj = json.loads(data) + edit(obj) + return (json.dumps(obj, sort_keys=True) + "\n").encode() + + mutate( + "corrupted-certificate-pairs", + "CERTIFICATE.json", + lambda data: json_edit(data, lambda x: x.update(key_pairs_abc_cba_I=1)), + "certificate mismatch", + ) + mutate( + "duplicate-json-key", + "CERTIFICATE.json", + lambda data: b'{"status":"first","status":"second"}\n', + "duplicate JSON key", + ) + mutate( + "sources-base-drift", + "SOURCES.json", + lambda data: json_edit(data, lambda x: x.update(base_commit="0" * 40)), + "base pin", + ) + + need(inventory(target) == before, "corruption controls failed to restore source bytes") + checks.append("need-survives-python-O") + + print("PASS_UT4_TWO_TARGET_NO_NB6_PACKAGE_CONTROLS", "checks=" + str(len(checks))) + print(json.dumps(checks)) + + +if __name__ == "__main__": + main() diff --git a/research/ut4-two-target-no-six-b/verify.py b/research/ut4-two-target-no-six-b/verify.py new file mode 100644 index 0000000000..6bc74a82b8 --- /dev/null +++ b/research/ut4-two-target-no-six-b/verify.py @@ -0,0 +1,233 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Read-only verifier: no legal two-target UT4 word has n_b=6. + +Exhausts GL2-minimal zero-sum six-call middle sequences with rank(X),rank(Y)>=2 +and every side-zero a/c profile (unbounded outer length) on two active roles. +Reports zero abc=cba=I key pairs. Prepared by Wentao Li with substantial AI +assistance. Apache-2.0. +""" +from concurrent.futures import ProcessPoolExecutor +from hashlib import sha1, sha256 +import json +from pathlib import Path +import sys +import tempfile + +HERE = Path(__file__).resolve().parent +if str(HERE) not in sys.path: + sys.path.insert(0, str(HERE)) + + +def repo_root(): + cur = HERE + for _ in range(8): + if (cur / "certificates" / "selected-result.json").is_file(): + return cur + if cur.parent == cur: + break + cur = cur.parent + return HERE.parents[1] + + +ROOT = repo_root() + +from core import ( # noqa: E402 + count_key_pairs, + cross_coeffs, + diag, + key, + key_cross, + middle_sequences, + need, + ranks_XY, + side_coeffs, + side_tables, + side_zero_keys, +) +BASE = "20ecf2891d80b5acf18d980b2164fb44ea7faa90" +PASS = "PASS_UT4_TWO_TARGET_NO_NB6" +CERT_KEYS = ( + "schema_version", + "status", + "active_roles", + "targets", + "n_b", + "canonical_zero_sum_middles", + "rank_XY_at_least_2", + "low_rank_excluded", + "side_zero_key_joins", + "keys_sum", + "max_keys_per_middle", + "key_pairs_abc_cba_I", +) + + +def read_json(path): + def pairs(items): + obj = {} + for k, v in items: + need(k not in obj, "duplicate JSON key: " + k) + obj[k] = v + return obj + + def bad(value): + raise ValueError("noninteger/nonfinite JSON number: " + value) + + return json.loads(path.read_text(), object_pairs_hook=pairs, parse_float=bad, parse_constant=bad) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":"), allow_nan=False) + + +def check_sources(): + pins = read_json(HERE / "SOURCES.json") + need(pins["base_commit"] == BASE, "base pin") + need(pins["schema_version"] == 1, "SOURCES schema") + need(len(pins["files"]) >= 2, "source inventory") + for row in pins["files"]: + need(row["usage"] in ("input", "provenance"), "source role: " + row["path"]) + need(isinstance(row.get("git_blob"), str) and len(row["git_blob"]) >= 40, "git blob") + need(isinstance(row.get("sha256"), str) and len(row["sha256"]) == 64, "sha256") + # Optional live check when the checkout is present (skipped under isolated copies). + if row["usage"] == "input" and (ROOT / row["path"]).is_file(): + data = (ROOT / row["path"]).read_bytes() + need(sha256(data).hexdigest() == row["sha256"], "live input SHA256: " + row["path"]) + need( + sha1(b"blob " + str(len(data)).encode() + b"\0" + data).hexdigest() + == row["git_blob"], + "live input Git blob: " + row["path"], + ) + + +def worker(bt): + keys, joins = side_zero_keys(bt) + return joins, len(keys), count_key_pairs(keys) + + +def run_census(): + all_m = list(middle_sequences(6, True)) + good = [bt for bt in all_m if ranks_XY(bt)[0] >= 2 and ranks_XY(bt)[1] >= 2] + need(len(all_m) == 5582, "canonical middle count") + need(len(good) == 5400, "rank-filtered middle count") + tot_join = tot_keys = tot_kp = 0 + max_keys = 0 + with ProcessPoolExecutor(max_workers=4) as pool: + for joins, nk, kp in pool.map(worker, good, chunksize=20): + tot_join += joins + tot_keys += nk + tot_kp += kp + if nk > max_keys: + max_keys = nk + need(tot_kp == 0, "unexpected abc=cba=I key pair for n_b=6") + return { + "schema_version": 1, + "status": "no_nb6_two_target_quotient", + "active_roles": 2, + "targets": 2, + "n_b": 6, + "canonical_zero_sum_middles": len(all_m), + "rank_XY_at_least_2": len(good), + "low_rank_excluded": len(all_m) - len(good), + "side_zero_key_joins": tot_join, + "keys_sum": tot_keys, + "max_keys_per_middle": max_keys, + "key_pairs_abc_cba_I": tot_kp, + } + + +def check_certificate(cert, expected=None): + expected = expected if expected is not None else read_json(HERE / "CERTIFICATE.json") + for key_name in CERT_KEYS: + need(key_name in expected and key_name in cert, "certificate field: " + key_name) + need(cert[key_name] == expected[key_name], "certificate mismatch: " + key_name) + + +def check_controls(): + need(diag(2, 2) == 9, "I_2 pack") + # Low-rank middle admits abc=cba=I keys; the rank filter excludes it. + low = (1, 1, 1, 1, 1, 1) + need(ranks_XY(low) == (1, 1), "low-rank diagnostic") + keys_low, _ = side_zero_keys(low) + need(count_key_pairs(keys_low) > 0, "search must find pairs on low-rank control") + # Rank-adequate sample has no I-pairs; side/key formulas agree with directs. + sample = None + for bt in middle_sequences(6, True): + if ranks_XY(bt) == (2, 2): + sample = bt + break + need(sample is not None, "rank-2 middle exists") + keys, _ = side_zero_keys(sample) + need(count_key_pairs(keys) == 0, "sample rank-2 middle has no I-pairs") + tab = side_tables(sample) + probes = 0 + for p0 in range(16): + for p1 in range(16): + P = (p0, p1, 0, 0, 0, 0) + v = tab[0][p0] ^ tab[1][p1] ^ tab[2][0] ^ tab[3][0] ^ tab[4][0] ^ tab[5][0] + direct = side_coeffs(sample, P) + packed = direct[0] | direct[1] << 4 | direct[2] << 8 | direct[3] << 12 + need(v == packed, "side_tables vs side_coeffs") + probes += 1 + need(probes == 256, "side formula probes ran") + P = (9, 0, 9, 0, 9, 0) + Q = (0, 9, 0, 9, 0, 9) + need(cross_coeffs(sample, P, Q) == key_cross(key(sample, P), key(sample, Q)), + "cross vs key_cross") + + +def reject_corrupted_temporary_certificate(): + with tempfile.TemporaryDirectory(prefix="nb6-cert-") as directory: + path = Path(directory) / "CERTIFICATE.json" + path.write_text('{"status":"first","status":"second"}\n') + try: + read_json(path) + raised = False + except ValueError as exc: + raised = True + need("duplicate JSON key" in str(exc), "duplicate key message") + need(raised, "duplicate JSON key must reject") + # Plant a temporary certificate that claims a positive key-pair count. + # Use a synthetic honest payload so this control still works when the + # on-disk CERTIFICATE.json has itself been corrupted by fault tests. + live = read_json(HERE / "CERTIFICATE.json") + honest = {k: live[k] for k in CERT_KEYS} + honest["key_pairs_abc_cba_I"] = 0 + fake = dict(honest) + fake["key_pairs_abc_cba_I"] = 1 + path.write_text(json.dumps(fake, sort_keys=True) + "\n") + corrupted = read_json(path) + try: + check_certificate(honest, expected=corrupted) + raised = False + except ValueError as exc: + raised = True + need("certificate mismatch" in str(exc), "corrupted certificate message") + need(raised, "corrupted temporary certificate must reject") + + +def package_files(): + return { + p.name: sha256(p.read_bytes()).hexdigest() + for p in HERE.iterdir() + if p.is_file() and p.suffix in {".py", ".json", ".md"} + } + + +def main(): + need((HERE / "CERTIFICATE.json").is_file(), "certificate present") + before = package_files() + check_sources() + reject_corrupted_temporary_certificate() + check_controls() + cert = run_census() + check_certificate(cert) + after = package_files() + need(before == after, "verify must not mutate package files") + print(PASS, "key_pairs=0", "middles=" + str(cert["rank_XY_at_least_2"])) + print(canonical({k: cert[k] for k in CERT_KEYS})) + + +if __name__ == "__main__": + main()