diff --git a/research/r439-late-entrance-census-seed09/PROOF.md b/research/r439-late-entrance-census-seed09/PROOF.md new file mode 100644 index 0000000000..5cb6c71a8b --- /dev/null +++ b/research/r439-late-entrance-census-seed09/PROOF.md @@ -0,0 +1,109 @@ +# Why a REJECT is sound + +The verifier checks every computational step. The argument below is written out by hand; it is not formalised. + +## Setting + +**The word.** A word is in the bitE8/1+mut format, with v = 111 and R = 439. +- Its registers are sources x (0..v−1), targets y (v..2v−1) and helpers s (2v..). +- Its sections are D, A, the scatter (nine COPY snapshots of the retained totals, added into targets at frame 0, then erased), B and C. +- Frames are closed label lists, so frame a ⊆ frame b exactly when its labels are included. Engine 2 checks closure for every frame. +- A gate first climbs each operand to its frame. Frames never descend. + +**The raw word.** W0 = (A, scatter, B) maps z = (x, s) to Uz, and y to y + x + Ks. Here V = I and J = I, checked on every word. + +**The cut σ.** This is the moment right after the scatter. At σ every target is still at frame 0 (`xcheck_p.py:269`). Each target ends at its t⊥ (`final[v+t]`). + +**An entrance.** It is given by: +- a support c, a nonzero set of helpers inside some class I(V) of #1253's closure L; +- a pivot p ∈ c with start[p] = E, where E is a nonzero frame inside V; +- the gauge q ^= p for each q ∈ c \ {p}, applied at frame E before A; +- optional source donors x_s ^= p, where the line of s lies in E. + +The **pivot coefficient** of a value w is π_c(w) = |d(w) ∩ c| + |x(w) ∩ D_S| mod 2, where d is the helper part and x the source part. The **response** is ρ = Kc + 1_{D_S}, and T = supp ρ: +- the entrance is a **kernel entrance** (the #1179 case) if T = ∅; +- it is **late-compensated** if T ≠ ∅ and the missing compensation is supplied after σ. + +## The class LC-fav + +These are the premises. +- **P1.** The word data are unchanged: lines, frames (new closed frames may be appended), start except start[p], final, A with its gates and frames, ret, and the COPY centres and ranks. Scatter rows may gain snapshot terms, which only enlarges the class. +- **P2.** Before A there is only D′ at frame 0, then the gauge at the single frame E. There are no other gates and no new wires before σ. +- **P3.** Targets stay at frame 0 until the scatter. +- **P4.** After σ, anything is allowed that satisfies all of these: + - it is a finite sequence of common-frame, invertible F2 operations with monotone frames; + - fresh registers may be used if they are restored; + - B and C may be replaced arbitrarily; + - there is no new COPY, descent or reset; + - the endpoint is (x, y, s) ↦ (x, y + x, s) on all 661 columns, and every register reaches its final frame. +- **P5.** Exactly one helper (p) starts at a nonzero frame. + +**Lemma 1 (cone; the dependency-path argument of #1128 PROOF.md §1).** A value at frame U depends only on registers whose frames lay inside U along the dependency path. The scatter's COPY descent is the only exception. +- So D′ and every register at frame 0 before σ have π_c = 0. +- So every contribution of D′ to a helper or a target is x-free and has zero coefficient on the pivot input s_p. (D′ need not restore z; the proof uses only this property, applied to the full pre-A change of coordinates Γ′ = gauge ∘ D′.) + +**Lemma 2 (monotone span; the dual of #1128 PROOF.md §2's erasure invariant).** Fix U = t⊥. Let Σ(τ) be the span of the values of the registers whose frame lies in U after τ post-scatter steps. Then Σ(τ′) ⊆ Σ(τ) ⊕ Fresh for τ′ ≥ τ. +- A step at a frame f ⊆ U only mixes registers that are already in the set. +- A step at a frame f ⊄ U removes its operands from the set for good, because frames never descend. + +**W_t.** Let G_t be the set of values at σ of every register r ≠ v+t whose frame at σ lies in t⊥, together with the nine snapshots. Then W_t is the set of helper parts d(u) of the F2 combinations u of G_t with x(u) = 0. This is the y-free form; the y-zero form gives the same spaces on these words. + +**Theorem.** In LC-fav, if the endpoint holds, then every t ∈ T has some u ∈ W_t with u · c = 1. + +**Frames at σ.** A is fixed and E ⊆ V ⊆ F_q for every q ∈ c (E lies inside every first-contact frame of the support, and inside each donor's first A frame). So under the entrance every register reaches σ at its raw frame, and the register sets in Lemma 2 are the same for the raw and the modified word. + +**Proof.** +1. Target t ends at U = t⊥. By Lemma 2, its final value y_t + x_t lies in the span at σ of the modified registers, raw_r(σ) + δ_r. The fresh part is zero, because the final value has no fresh coordinate. +2. In the same way, the raw end value y_t + x′_t + K_t s′ lies in Σ_raw(σ). +3. Let Δ be their difference. Then Δ has no x part in the original coordinates, and π_c(Δ) = ρ_t. +4. Write the modified σ-values as raw_r(σ) + δ_r + σ_r, where δ_r is D′'s contribution and σ_r collects the snapshot terms that P1 lets scatter rows gain (σ_r = 0 for non-targets). Then Δ = Σ (a_r + b_r) raw_r(σ) + Σ a_r δ_r + Σ a_r σ_r. + - The δ terms carry no x part and no pivot, by Lemma 1. + - The σ terms are sums of snapshots, which are generators in G_t; fold them into u. + - So u = Σ (a_r + b_r) raw_r(σ) + Σ a_r σ_r has x(u) = 0 and π_c(u) = ρ_t = 1, and lies in span G_t. +5. The term for r = t is raw_t(σ). Modulo y, it is the sum of t's snapshots, so it lies in G_t. +6. Hence d(u) ∈ W_t and d(u) · c = 1. ∎ + +So a support is **rejected** in LC-fav if some t ∈ T has W_t ⊆ c⊥. Adding pivot-free dirt to the generators cannot change this, so the verdict does not depend on the choice of D′. + +## Narrower classes + +**A6** is the post-scatter program B ++ C left unchanged, plus inserted target reads [F, v+t, [r]]. Here r is one of: +- a z register; +- a snapshot (at σ only); +- a target that has received no inserted read (a read-only relay). + +Raw gates keep their frames, and actual frames contain the raw frames. So every read needs cur_t ∪ cur_r ⊆ F ⊆ next_t ∩ next_r, computed from the raw frames. The span of every value read this way contains every reachable compensation. This makes A6's REJECT sound for the A6 class. + +Both engines sweep insertion points through B only. That is enough: on all five words C is entirely at FULL and touches no target, and no target ends at FULL (the verifier asserts this). A register r not yet raised by C still holds its end-of-B value with next_r = FULL, so a read during C has the same value and legality as a read at τ = |B|. Once r is at FULL it lies outside t⊥ and cannot be read. + +A6 is contained in LC-fav, so an LC-fav REJECT is also an A6 REJECT. The verifier checks that every A6 space lies inside the LC-fav space. + +**A6R** is A6 plus storage relays, where a target that received inserted reads may itself be read later. +- Stored content keeps a frame tag: the join of the frames that delivered it. +- A read of u delivers u's whole value, which lies in the span of the stored entries whose tags fit the read frame. +- Restoring the relay is ignored, so A6R over-approximates. It is used only to show that the triple is **not** excluded once storage relays are allowed. + +**The scout prototype's strict class.** It allows a read when the reading register's frame lies in t's next frame, with no check on the register being read (the carrier). That class is not physical; it is reported only to explain the scout's numbers. On these words its results equal LC-fav's. + +## What the classes exclude + +- a changed A, changed pre-scatter frame paths, or gates and wires before σ; +- targets leaving frame 0 before the scatter; +- a new or changed COPY, and scatter changes beyond added snapshot terms; +- gauge shears after A, or at more than one frame (the #1253 out-of-scope list); +- source-dependent basis changes other than the donor shear; +- several simultaneous entrances (see below); +- recursive interfaces, hosting and pricing. + +Several entrances need a joint test, which is not run here: for every t, the vector (K_t · c_i)_i must lie in {(u · c_i)_i : u ∈ W_t}. + +## Not sufficient + +LC-fav admits the triple {444, 470, 578}, but that is not a construction. +- Under A6 the triple is rejected: only 150 and 197 of its 8 targets are coverable. +- Under A6R (storage relays, restoration ignored) all 8 are coverable. +- If only targets in T may store content, just 4 of the 8 are coverable. + +So, within A6R (B ++ C fixed, insertion-only target reads), covering all 8 targets needs storage relays outside T, which must later be restored. The broader class LC-fav also allows a rewritten B or C and fresh restored registers, which A6R does not model. The triple is therefore **OPEN**, and this package hands it on. + +A positive answer would at most save the pivot's first climb, i.e. the local −H1 (−H2 + H1 for p = 578). Width-8 hosting cancels it with +H1 (#1179, #1253), and the bit side does not bind. So no κ follows either way. diff --git a/research/r439-late-entrance-census-seed09/README.md b/research/r439-late-entrance-census-seed09/README.md new file mode 100644 index 0000000000..70fbf661e7 --- /dev/null +++ b/research/r439-late-entrance-census-seed09/README.md @@ -0,0 +1,175 @@ +# Late-compensated helper entrances on the R439 bit word: a scoped census + +**Scoped negative result with one open survivor. No construction and no new κ.** + +- Track: 00–19 (bit supplier), assignment seed 9, drawn with the OS CSPRNG via Python `secrets`. +- Card: `bit-helper-contract`, with the scope **refined** in [TASK.json](TASK.json). +- Base: `0b1cccf8`. The selected record frontier1094 is complex-bound and is unchanged. + +## The question + +The inherited H2/K interface requires every helper to start at frame 0, so that a frame-0 prefix D can supply all dirt compensation (N = K). + +An **entrance** lets one helper start at a nonzero frame E instead: a pivot p, plus the gauge q ^= p on a support c. This changes the response by ρ = Kc, so the targets in T = supp ρ need extra compensation. + +What merged work settles and what it leaves open: +- #1179 found the kernel entrance 444+470, which has T = ∅. +- #1253 proved that this is the only kernel entrance among the common-frame entrances of all 366 closure classes. +- #1128 (PROOF §4) leaves "compensation moved after A" open. +- #1179 states that its condition K e_J = 0 is "not a statement about arbitrary later compensation". + +This package **narrows** that open case. It looks at compensation **after the scatter**, with A and the scatter fixed and one entrance at a time. +- Inputs: every support of #1253's closure (4,954 supports from 5,548 (V, c) pairs) plus 5,212 enumerated source-donor entrances, of which 5,059 have a legal entrance frame. +- Words: the selected PR589 word and the four merged star words (#1062, #1122, #1188, #1208). +- Outcome: the case reduces to one open triple. + +The broader case of #1128 §4, compensation after A but before the scatter, is not covered. + +## The test + +For each target t, W_t is the **dirt-only space**: the helper parts of every F2 combination, with zero source part, of the values t could legally read after the scatter. A support c is admitted only if every t ∈ T has some u ∈ W_t with u·c = 1. Otherwise it is **rejected**. + +The test is run in three classes: + +| Class | What t may read | What a REJECT proves | +|---|---|---| +| **LC-fav** | any register whose frame at the scatter cut lies in t's final frame t⊥, plus the nine COPY snapshots | Rejection for the **whole class** of post-scatter programs with monotone frames under the stated premises ([PROOF.md](PROOF.md)). This is the necessary test. | +| **A6** | B ++ C unchanged, plus inserted target reads with a carrier check and read-only relays | Rejection for A6, which is contained in LC-fav. | +| **A6R** | A6 plus storage relays (a target that received reads may be read later); relay restoration is ignored | Nothing: A6R is an over-approximation, used only to show that a survivor is *not* excluded. | + +The carrier check requires the reading register and the register being read to both fit inside the gate's frame. + +The scout's prototype class (`strict_proto`) is kept for traceability only. It has no carrier check, so it is not physical, and on these words it gives the same results as LC-fav. + +## Results ([RESULT.json](RESULT.json); identical on all five words) + +| | LC-fav | A6 | +|---|---|---| +| Supports admitted | 2: 444+470 (T = ∅, #1179's kernel pair) and **444+470+578** (\|T\| = 8) | 1: 444+470 (T = ∅) | +| Single helpers | 0 / 439 | 0 / 439 | +| New pairs | 0 / 1,569 | 0 / 1,569 | +| Source donors (5,212 enumerated, 5,059 placeable) | 0 kernel, 0 late | 0 kernel, 0 late | +| Linear relaxation (366 classes) | one nonzero class (frame 79's line), kernel {444+470, 578}, 84 rows kept | one nonzero class, kernel {444+470}, 94 rows kept | +| max dim W_t | 5 | 4 | +| K incidences covered | 98 / 18,085 | 47 / 18,085 | + +**Apart from the kernel pair:** +- No late-compensated entrance exists in A6. +- In the sound LC-fav class, only the triple **444+470+578** survives. Its targets are 113, 118, 150, 153, 192, 197, 214 and 219. + +**The triple is OPEN.** +- A6 covers only 150 and 197. +- A6R covers all 8. +- A6R restricted to relays inside T covers 150, 153, 192 and 197. + +So, within A6R (B ++ C fixed, insertion-only target reads), covering all 8 targets needs storage relays outside T, which must later be restored. LC-fav also allows a rewritten B or C and fresh restored registers, which A6R does not model. That remains open (open question 1). + +**Why so little survives.** Every W_t is a *coordinate* subspace, spanned by at most 5 unit vectors e_j (at most 4 in A6). A target can therefore compensate a support only where the support meets that small set of helpers. Only 98 of the 18,085 nonzero K incidences (47 in A6) fall inside these sets. + +## Two engines + +**Engine 1** ([census.py](census.py)) computes: +- the raw replay, K, the first contacts and the closure L; +- W_t in every class; +- the parity census of every support; +- the per-class linear relaxation, with a check that it contains every admitted support; +- the source donors and A6R. + +**Engine 2** ([engine2.py](engine2.py)) shares no code with engine 1. It uses: +- a set-valued replay; +- rational-annihilator geometry, which also checks that every frame is closed, so that label inclusion equals rational containment; +- a closure that also equals #1253's `CERTIFICATE.json`; +- a kernel method for LC-fav and per-pair change points for A6. + +It agrees with engine 1 on K, the closure, every W_t (LC-fav and A6) and every **support verdict**. The source-donor census, the relaxation, the scout class and A6R are computed by engine 1 alone. + +## Controls + +Recorded in RESULT.json; [test_package.py](test_package.py) has 20 tests. + +- **A realisable late entrance, on a synthetic word.** + - `W_syn` is PR589 with target 150's compensation of helper 470 moved after the scatter: three B reads into 150 (149 at frame 0, then 149 and 470 at frame 323), with 470 dropped from D's row 150. + - On `W_syn` the census admits 444+470 as a *late* entrance (T = {150}) in LC-fav and A6. + - The built witness passes the merged `wlib.replay`: + - start[444] = 79, with the shear at the head of A and its inverse at the end of C; + - three post-scatter reads into 150; + - D′ = PR589's D without 444, i.e. `W_syn`'s D minus 444 with 470 restored at row 150. + - Without its late reads, the witness fails replay at register 150. + - Its late reads undo `W_syn`'s own moved compensation, so after B it carries the same values as #1179's prefix entrance on PR589. It is a check that an admission can be realised, not a new construction. + - `W_syn` with D left unedited also fails at 150. + - Both words are rebuilt in code and checked by canonical sha256. +- **Mutations that flip verdicts.** + - Flipping one K bit rejects 444+470. + - Letting register 77 be read at FULL admits the triple in A6. + - Emptying target 150's reads rejects the triple. +- **Binding.** A flipped word byte is rejected by its digest, and so is a wrong pin. +- **Structure.** All frames are closed, and a frame with a dropped label is detected. Reads during C reduce to reads at the end of B: C is entirely at FULL and touches no target. +- **Sanity checks of the census itself** (true by construction): + - with every unit vector added to every W_t, all supports are admitted; + - the kernel pair (T = ∅) is admitted; + - clearing K's column 578 admits 578. + +## Scope + +**Covered.** For each single common-frame entrance on these five words, with A and the scatter fixed, no pre-scatter wires, and the endpoint required on all 661 columns: +- the LC-fav REJECTs hold for the whole post-scatter class; +- the A6 REJECTs hold for insertion-only compensation. + +**Not covered:** +- a changed A; +- targets leaving frame 0 before the scatter; +- a new COPY, or scatter changes beyond added snapshot terms; +- gauge shears after A or at several frames; +- source-dependent basis changes other than the donor shear; +- several simultaneous entrances; +- recursive interfaces and hosting. + +**No κ.** The bit side does not bind. An entrance would at most save the pivot's first climb (−H1), which width-8 hosting cancels with +H1 (#1179, #1253). + +## Reproduce + +```sh +python3 -I -B research/r439-late-entrance-census-seed09/verify.py # about 3 min; PASS_R439_LATE_ENTRANCE_CENSUS +python3 -I -B -m unittest discover -s research/r439-late-entrance-census-seed09 -p test_package.py +python3 scripts/research_package.py --package research/r439-late-entrance-census-seed09 --check-only +python3.12 scripts/research_package.py --package research/r439-late-entrance-census-seed09 +``` + +- `--no-a6r` skips the A6R runs and stops before RESULT.json is checked. +- Requirements: standard-library Python 3.10 or later. +- Tested on Python 3.12.15 and 3.14.8 (macOS 26.5, arm64). + +## Open next questions + +1. **Can the triple 444+470+578 be realised in LC-fav?** It is the only support that survives the sound test. + - Why it matters: at the cut, helper 470 carries s_470 + x₇₇ at frame 79. Within A6R its 8 targets can be covered only through relays outside T. A rewritten B in which the targets read 470 and source 77 directly is not excluded. + - First step: record which reads A6R uses for each target, build a candidate word (relays first, then a rewritten B reading 77 directly), and test it with `wlib.replay` and #1179's literal stream checks. + - Blocked by: restoring the relay targets, or a legal rewritten B. +2. **Do simultaneous entrances admit late compensation where single ones do not?** + - Why it matters: this census is one entrance at a time. The joint test requires (K_t·c_i)_i ∈ {(u·c_i)_i : u ∈ W_t} for every t. + - First step: run the joint test over pairs of disjoint supports in the same class V. + - Blocked by: none. +3. **Does a different scatter enlarge W_t enough to admit a late single entrance?** + - Why it matters: the coordinate W_t of at most 5 helpers is a property of this scatter. Adding snapshot terms is already inside the class and changes nothing. + - First step: move one retained total to another helper and recompute W_t. + - Blocked by: pricing the changed COPY with #1128 §5's argument. + +## Relation to earlier work and credit + +- **#1128** (aliromman): the width-seven boundary obstruction. This package narrows the case its PROOF §4 names. Lemma 1 is its §1 dependency-path argument, and Lemma 2 is the dual of its §2 erasure invariant. +- **#1179** (adamgall): the kernel pair 444+470. Its literal stream checks are proposed for a future witness of the triple; they are not run here. +- **#1253** (mightyOil): the all-support common-frame kernel entrances and the closure L. Its certificate is reproduced here. +- **#1194** (woklerx) and **#1311** (Arham-Tahir64): the semantic-D contract. +- **The star words:** #1062 (thakrarsagar), #1122 and #1188 (bitplane) and #1208 (ToikY). Their helper-star D comes from #967 (theon199), built on #915/#926 (bitplane). +- **The R439 word and its checker:** eumemic (#543/#555), including the scatter and `xcheck_p.py`. DreamingOfClouds (#589) supplied the two A-section transports and `wlib.py`. +- **The helper-470/source-77 boundary** behind the survivor: #1043 (aliromman, open), #1079 (bbMisk / Hanson Sun) and #1256 (RossRichardson). +- **Kernel-entrance precedents:** #254 (Dugongue) and #382 (chafreaky). +- **Different mechanisms:** open #1810 (RossRichardson; dirty workspace on B) and open #1580/#1592 (Arham-Tahir64; terminal star compensation). + +Prepared by Sagar Thakrar (thakrarsagar) with substantial AI assistance from Claude (Anthropic) via Claude Code. +- Parallel read-only scout and judge subagents selected the question. +- Reader subagents and a synthesizer audited the scout's criterion. They found the triple the scout had missed and the missing carrier check in the scout's strict class, and they specified the classes. +- The engines, the proof note and the controls were then written fresh. +- A post-PR adversarial review corrected the witness description, the scope of the open triple, the citations and the controls (second commit). + +No claim was posted to Discussions. New material is Apache-2.0. diff --git a/research/r439-late-entrance-census-seed09/RESULT.json b/research/r439-late-entrance-census-seed09/RESULT.json new file mode 100644 index 0000000000..86589678e9 --- /dev/null +++ b/research/r439-late-entrance-census-seed09/RESULT.json @@ -0,0 +1,983 @@ +{ + "certificate_1253": { + "path": "research/r439-kernel-entrance-closure/CERTIFICATE.json", + "sha256": "f08b9de12089687fe6c0c6b2eb985d0e6a883b72fa4f08ded11d34d875f48909" + }, + "controls": { + "flipped_byte": "rejected by the word digest", + "frame_closure": "all frames closed (label inclusion = rational containment); a dropped label is detected", + "mutations": { + "flip_K_bit": "444+470 rejected after flipping K[target 112, helper 470]", + "relax_next_77": "444+470+578 admitted by A6 when register 77 may be read at FULL", + "sanity_zero_K_column": "578 admitted (T empty) after clearing column 578" + }, + "sanity_kernel_pair": "444+470: K e_J = 0 (the #1179 entrance), so admitted in every class", + "sanity_pre_A_window": "with every unit vector added to every W_t, 4954/4954 supports are admitted", + "synthetic": { + "admitted_A6": [ + [ + [ + 444, + 470 + ], + 1 + ] + ], + "admitted_LC_fav": [ + [ + [ + 444, + 470 + ], + 1 + ], + [ + [ + 444, + 470, + 578 + ], + 7 + ] + ], + "kernel_pair_T": [ + 150 + ], + "negative": "W_syn with the unedited D fails replay at register 150", + "note": "the late reads undo W_syn's own moved compensation, so after B the witness carries the same values as #1179's prefix entrance on PR589: a realisable late entrance, not a new construction", + "synthetic_paid": { + "1": 1323, + "2": 1344, + "3": 82, + "4": 45, + "5": 100, + "6": 11, + "7": 18 + }, + "witness_paid": { + "1": 1322, + "2": 1344, + "3": 82, + "4": 45, + "5": 100, + "6": 11, + "7": 18 + }, + "witness_replay": "PASS", + "witness_sha256": "cf7aa7a94141fd18623e0ce489f67d86c725f17ec0856bbc23b4700d66c5d00a", + "witness_without_late_reads": "fails replay at register 150", + "word_sha256": "a33bf677cb43b26f27e18bf29b5618ded5a17d04987ddb71d8ce4f2de4401ea1" + } + }, + "inputs": { + "PR1062": { + "path": "research/r439-bsection-stars-seed01/candidate.json.gz", + "sha256": "b452d2c2b0b2a546d1105b1da9769aa78e5c54d6f00e97b30c77e3f54ce445ee" + }, + "PR1122": { + "path": "research/r439-abc-semantic-bridge/inputs/candidate.json.gz", + "sha256": "2b09a7a3851cdf2a7f19350d1555cf75788d001c9507a37e459cd931881ee066" + }, + "PR1188": { + "path": "research/r439-gl5-shortest/candidate.json.gz", + "sha256": "4e7904d01ebdbfc60a26472b4e0d2e813c19c2fe1a4bb8ab390c12746a1da359" + }, + "PR1208": { + "path": "research/r439-abc-zrewrite-seed16/CANDIDATE-WORD.json", + "sha256": "66b34404f39f5f612c2aaadd53ae33eb9f5993ec2065c82e23d7467cce03a226" + }, + "PR589": { + "path": "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz", + "sha256": "e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f" + } + }, + "scope": "Scoped census: late (post-scatter) compensation of single common-frame entrances on fixed A/scatter; no change to A or the scatter, no pre-scatter wires, one entrance at a time; no construction and no new kappa", + "status": "PASS_R439_LATE_ENTRANCE_CENSUS", + "summary": { + "A6_late": [], + "LC_fav_late": [ + [ + 444, + 470, + 578 + ] + ], + "new_pairs_admitted": 0, + "singles_admitted": 0, + "source_donors_late": 0, + "supports": 4954, + "triple_status": "OPEN" + }, + "words": { + "PR1062": { + "K_column_weights": [ + 8, + 68 + ], + "K_nonzeros": 18085, + "N_equals_K": true, + "classes": { + "A6": { + "admitted": [ + [ + [ + 444, + 470 + ], + 0 + ] + ], + "coordinate_subspaces": true, + "covered_K_incidences": 47, + "dim_W": { + "0": 50, + "1": 35, + "2": 12, + "3": 13, + "4": 1 + }, + "relax366": [ + { + "dim_V": 1, + "kernel": [ + [ + 444, + 470 + ] + ], + "rows_kept": 94 + } + ], + "source_donors": { + "enumerated": 5212, + "kernel": 0, + "late": 0, + "placeable": 5059 + } + }, + "LC_fav": { + "admitted": [ + [ + [ + 444, + 470 + ], + 0 + ], + [ + [ + 444, + 470, + 578 + ], + 8 + ] + ], + "coordinate_subspaces": true, + "covered_K_incidences": 98, + "dim_W": { + "0": 15, + "1": 40, + "2": 28, + "3": 22, + "4": 4, + "5": 2 + }, + "relax366": [ + { + "dim_V": 1, + "kernel": [ + [ + 444, + 470 + ], + [ + 578 + ] + ], + "rows_kept": 84 + } + ], + "source_donors": { + "enumerated": 5212, + "kernel": 0, + "late": 0, + "placeable": 5059 + } + }, + "strict_proto": { + "admitted": [ + [ + [ + 444, + 470 + ], + 0 + ], + [ + [ + 444, + 470, + 578 + ], + 8 + ] + ], + "coordinate_subspaces": true, + "covered_K_incidences": 98, + "dim_W": { + "0": 15, + "1": 40, + "2": 28, + "3": 22, + "4": 4, + "5": 2 + } + } + }, + "closure": { + "meeting_pairs": 549, + "plane_pairs": 11628, + "size": 366, + "supports": 4954 + }, + "engines_agree": true, + "gates": { + "A": 2075, + "B": 578, + "C": 2440, + "D": 1195 + }, + "late_survivors": { + "444,470,578": { + "A6R_T_only_covered": [ + 150, + 153, + 192, + 197 + ], + "A6R_covered": [ + 113, + 118, + 150, + 153, + 192, + 197, + 214, + 219 + ], + "A6_covered": [ + 150, + 197 + ], + "T": [ + 113, + 118, + 150, + 153, + 192, + 197, + 214, + 219 + ] + } + } + }, + "PR1122": { + "K_column_weights": [ + 8, + 68 + ], + "K_nonzeros": 18085, + "N_equals_K": true, + "classes": { + "A6": { + "admitted": [ + [ + [ + 444, + 470 + ], + 0 + ] + ], + "coordinate_subspaces": true, + "covered_K_incidences": 47, + "dim_W": { + "0": 50, + "1": 35, + "2": 12, + "3": 13, + "4": 1 + }, + "relax366": [ + { + "dim_V": 1, + "kernel": [ + [ + 444, + 470 + ] + ], + "rows_kept": 94 + } + ], + "source_donors": { + "enumerated": 5212, + "kernel": 0, + "late": 0, + "placeable": 5059 + } + }, + "LC_fav": { + "admitted": [ + [ + [ + 444, + 470 + ], + 0 + ], + [ + [ + 444, + 470, + 578 + ], + 8 + ] + ], + "coordinate_subspaces": true, + "covered_K_incidences": 98, + "dim_W": { + "0": 15, + "1": 40, + "2": 28, + "3": 22, + "4": 4, + "5": 2 + }, + "relax366": [ + { + "dim_V": 1, + "kernel": [ + [ + 444, + 470 + ], + [ + 578 + ] + ], + "rows_kept": 84 + } + ], + "source_donors": { + "enumerated": 5212, + "kernel": 0, + "late": 0, + "placeable": 5059 + } + }, + "strict_proto": { + "admitted": [ + [ + [ + 444, + 470 + ], + 0 + ], + [ + [ + 444, + 470, + 578 + ], + 8 + ] + ], + "coordinate_subspaces": true, + "covered_K_incidences": 98, + "dim_W": { + "0": 15, + "1": 40, + "2": 28, + "3": 22, + "4": 4, + "5": 2 + } + } + }, + "closure": { + "meeting_pairs": 549, + "plane_pairs": 11628, + "size": 366, + "supports": 4954 + }, + "engines_agree": true, + "gates": { + "A": 1706, + "B": 578, + "C": 2071, + "D": 1195 + }, + "late_survivors": { + "444,470,578": { + "A6R_T_only_covered": [ + 150, + 153, + 192, + 197 + ], + "A6R_covered": [ + 113, + 118, + 150, + 153, + 192, + 197, + 214, + 219 + ], + "A6_covered": [ + 150, + 197 + ], + "T": [ + 113, + 118, + 150, + 153, + 192, + 197, + 214, + 219 + ] + } + } + }, + "PR1188": { + "K_column_weights": [ + 8, + 68 + ], + "K_nonzeros": 18085, + "N_equals_K": true, + "classes": { + "A6": { + "admitted": [ + [ + [ + 444, + 470 + ], + 0 + ] + ], + "coordinate_subspaces": true, + "covered_K_incidences": 47, + "dim_W": { + "0": 50, + "1": 35, + "2": 12, + "3": 13, + "4": 1 + }, + "relax366": [ + { + "dim_V": 1, + "kernel": [ + [ + 444, + 470 + ] + ], + "rows_kept": 94 + } + ], + "source_donors": { + "enumerated": 5212, + "kernel": 0, + "late": 0, + "placeable": 5059 + } + }, + "LC_fav": { + "admitted": [ + [ + [ + 444, + 470 + ], + 0 + ], + [ + [ + 444, + 470, + 578 + ], + 8 + ] + ], + "coordinate_subspaces": true, + "covered_K_incidences": 98, + "dim_W": { + "0": 15, + "1": 40, + "2": 28, + "3": 22, + "4": 4, + "5": 2 + }, + "relax366": [ + { + "dim_V": 1, + "kernel": [ + [ + 444, + 470 + ], + [ + 578 + ] + ], + "rows_kept": 84 + } + ], + "source_donors": { + "enumerated": 5212, + "kernel": 0, + "late": 0, + "placeable": 5059 + } + }, + "strict_proto": { + "admitted": [ + [ + [ + 444, + 470 + ], + 0 + ], + [ + [ + 444, + 470, + 578 + ], + 8 + ] + ], + "coordinate_subspaces": true, + "covered_K_incidences": 98, + "dim_W": { + "0": 15, + "1": 40, + "2": 28, + "3": 22, + "4": 4, + "5": 2 + } + } + }, + "closure": { + "meeting_pairs": 549, + "plane_pairs": 11628, + "size": 366, + "supports": 4954 + }, + "engines_agree": true, + "gates": { + "A": 1626, + "B": 578, + "C": 1991, + "D": 1195 + }, + "late_survivors": { + "444,470,578": { + "A6R_T_only_covered": [ + 150, + 153, + 192, + 197 + ], + "A6R_covered": [ + 113, + 118, + 150, + 153, + 192, + 197, + 214, + 219 + ], + "A6_covered": [ + 150, + 197 + ], + "T": [ + 113, + 118, + 150, + 153, + 192, + 197, + 214, + 219 + ] + } + } + }, + "PR1208": { + "K_column_weights": [ + 8, + 68 + ], + "K_nonzeros": 18085, + "N_equals_K": true, + "classes": { + "A6": { + "admitted": [ + [ + [ + 444, + 470 + ], + 0 + ] + ], + "coordinate_subspaces": true, + "covered_K_incidences": 47, + "dim_W": { + "0": 50, + "1": 35, + "2": 12, + "3": 13, + "4": 1 + }, + "relax366": [ + { + "dim_V": 1, + "kernel": [ + [ + 444, + 470 + ] + ], + "rows_kept": 94 + } + ], + "source_donors": { + "enumerated": 5212, + "kernel": 0, + "late": 0, + "placeable": 5059 + } + }, + "LC_fav": { + "admitted": [ + [ + [ + 444, + 470 + ], + 0 + ], + [ + [ + 444, + 470, + 578 + ], + 8 + ] + ], + "coordinate_subspaces": true, + "covered_K_incidences": 98, + "dim_W": { + "0": 15, + "1": 40, + "2": 28, + "3": 22, + "4": 4, + "5": 2 + }, + "relax366": [ + { + "dim_V": 1, + "kernel": [ + [ + 444, + 470 + ], + [ + 578 + ] + ], + "rows_kept": 84 + } + ], + "source_donors": { + "enumerated": 5212, + "kernel": 0, + "late": 0, + "placeable": 5059 + } + }, + "strict_proto": { + "admitted": [ + [ + [ + 444, + 470 + ], + 0 + ], + [ + [ + 444, + 470, + 578 + ], + 8 + ] + ], + "coordinate_subspaces": true, + "covered_K_incidences": 98, + "dim_W": { + "0": 15, + "1": 40, + "2": 28, + "3": 22, + "4": 4, + "5": 2 + } + } + }, + "closure": { + "meeting_pairs": 549, + "plane_pairs": 11628, + "size": 366, + "supports": 4954 + }, + "engines_agree": true, + "gates": { + "A": 1652, + "B": 577, + "C": 2016, + "D": 1195 + }, + "late_survivors": { + "444,470,578": { + "A6R_T_only_covered": [ + 150, + 153, + 192, + 197 + ], + "A6R_covered": [ + 113, + 118, + 150, + 153, + 192, + 197, + 214, + 219 + ], + "A6_covered": [ + 150, + 197 + ], + "T": [ + 113, + 118, + 150, + 153, + 192, + 197, + 214, + 219 + ] + } + } + }, + "PR589": { + "K_column_weights": [ + 8, + 68 + ], + "K_nonzeros": 18085, + "N_equals_K": true, + "classes": { + "A6": { + "admitted": [ + [ + [ + 444, + 470 + ], + 0 + ] + ], + "coordinate_subspaces": true, + "covered_K_incidences": 47, + "dim_W": { + "0": 50, + "1": 35, + "2": 12, + "3": 13, + "4": 1 + }, + "relax366": [ + { + "dim_V": 1, + "kernel": [ + [ + 444, + 470 + ] + ], + "rows_kept": 94 + } + ], + "source_donors": { + "enumerated": 5212, + "kernel": 0, + "late": 0, + "placeable": 5059 + } + }, + "LC_fav": { + "admitted": [ + [ + [ + 444, + 470 + ], + 0 + ], + [ + [ + 444, + 470, + 578 + ], + 8 + ] + ], + "coordinate_subspaces": true, + "covered_K_incidences": 98, + "dim_W": { + "0": 15, + "1": 40, + "2": 28, + "3": 22, + "4": 4, + "5": 2 + }, + "relax366": [ + { + "dim_V": 1, + "kernel": [ + [ + 444, + 470 + ], + [ + 578 + ] + ], + "rows_kept": 84 + } + ], + "source_donors": { + "enumerated": 5212, + "kernel": 0, + "late": 0, + "placeable": 5059 + } + }, + "strict_proto": { + "admitted": [ + [ + [ + 444, + 470 + ], + 0 + ], + [ + [ + 444, + 470, + 578 + ], + 8 + ] + ], + "coordinate_subspaces": true, + "covered_K_incidences": 98, + "dim_W": { + "0": 15, + "1": 40, + "2": 28, + "3": 22, + "4": 4, + "5": 2 + } + } + }, + "closure": { + "meeting_pairs": 549, + "plane_pairs": 11628, + "size": 366, + "supports": 4954 + }, + "engines_agree": true, + "gates": { + "A": 2075, + "B": 712, + "C": 2574, + "D": 111 + }, + "late_survivors": { + "444,470,578": { + "A6R_T_only_covered": [ + 150, + 153, + 192, + 197 + ], + "A6R_covered": [ + 113, + 118, + 150, + 153, + 192, + 197, + 214, + 219 + ], + "A6_covered": [ + 150, + 197 + ], + "T": [ + 113, + 118, + 150, + 153, + 192, + 197, + 214, + 219 + ] + } + } + } + } +} diff --git a/research/r439-late-entrance-census-seed09/SOURCES.json b/research/r439-late-entrance-census-seed09/SOURCES.json new file mode 100644 index 0000000000..fc31456bcd --- /dev/null +++ b/research/r439-late-entrance-census-seed09/SOURCES.json @@ -0,0 +1,84 @@ +{ + "schema_version": 1, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1", + "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075" + }, + { + "path": "research/bit-kernel-entrance-seed18/README.md", + "usage": "provenance", + "git_blob": "b4d477b28c7d36392b35c105be90b010f7f77dd1", + "sha256": "52597eb69c061a3ec5126b79ee1a4dc8d2edcba33e6ef08230644b6f97dc22e3" + }, + { + "path": "research/bit-width-seven-boundary/PROOF.md", + "usage": "provenance", + "git_blob": "b3bedffde3ee5f1914873ec7918039ab6614678c", + "sha256": "f9fb4706dd523229e8351646c5ef011d8bd16eebc3dd6c35a778b352c123b387" + }, + { + "path": "research/e8-bit-p111-tuned/code/xcheck_p.py", + "usage": "provenance", + "git_blob": "184f5dcf94a486cc7db91ca4db5865916bf26009", + "sha256": "af3decc877e27c00001cf56f50c6c09566e8e101297ab34c7860aed96a06d80e" + }, + { + "path": "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz", + "usage": "input", + "git_blob": "85a4499bf9e4911a705d50567a2c2ef6cf23739a", + "sha256": "e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f" + }, + { + "path": "research/e8-bit-p111-tuned/tune/wlib.py", + "usage": "input", + "git_blob": "0e5f9a26f68cc415b793aa903cf6d105acbc8f03", + "sha256": "a37fdf3cdf5f62945c2a90193401c0e9edc9dd3cda8d8cb36a3b9c329ebe4dbc" + }, + { + "path": "research/r439-abc-semantic-bridge/inputs/candidate.json.gz", + "usage": "input", + "git_blob": "0ab597fefd68bfefecc85d631b172d174bdaeb70", + "sha256": "2b09a7a3851cdf2a7f19350d1555cf75788d001c9507a37e459cd931881ee066" + }, + { + "path": "research/r439-abc-zrewrite-seed16/CANDIDATE-WORD.json", + "usage": "input", + "git_blob": "83fb8ef2286a9aafaff7b5db4386ea65a07126a9", + "sha256": "66b34404f39f5f612c2aaadd53ae33eb9f5993ec2065c82e23d7467cce03a226" + }, + { + "path": "research/r439-bsection-stars-seed01/candidate.json.gz", + "usage": "input", + "git_blob": "9a17b4920334878d6c949191f6931bd97126fe3c", + "sha256": "b452d2c2b0b2a546d1105b1da9769aa78e5c54d6f00e97b30c77e3f54ce445ee" + }, + { + "path": "research/r439-gl5-shortest/candidate.json.gz", + "usage": "input", + "git_blob": "0d4dd2fb241a00cab1b57b17991db82bc06edd91", + "sha256": "4e7904d01ebdbfc60a26472b4e0d2e813c19c2fe1a4bb8ab390c12746a1da359" + }, + { + "path": "research/r439-kernel-entrance-closure/CERTIFICATE.json", + "usage": "input", + "git_blob": "dc231997b791b366d0eef1aa8946aedc687604b0", + "sha256": "f08b9de12089687fe6c0c6b2eb985d0e6a883b72fa4f08ded11d34d875f48909" + }, + { + "path": "research/r439-kernel-entrance-closure/PROOF.md", + "usage": "provenance", + "git_blob": "b3d5e97620851bc00d95b4b9ed8b24448ef725e4", + "sha256": "d0c91dc483feb03c04c6e175836848d11d5ec3444bc246b35722b3c20e48e05d" + } + ] +} diff --git a/research/r439-late-entrance-census-seed09/TASK.json b/research/r439-late-entrance-census-seed09/TASK.json new file mode 100644 index 0000000000..8308bf0444 --- /dev/null +++ b/research/r439-late-entrance-census-seed09/TASK.json @@ -0,0 +1,72 @@ +{ + "schema_version": 1, + "task_id": "bit-helper-contract", + "priority_revision": 3, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "original_card": { + "id": "bit-helper-contract", + "question": "Can one precisely specified helper-mixing word satisfy a replacement for the inherited H2/K interface?", + "starting_points": [ + "research/r439-bsection-stars-seed01/README.md", + "research/r439-copy-path-sharing-barrier/README.md" + ], + "methods": [ + "Derive a replacement interface lemma and price its implementation.", + "Seek an exact dirty-input or chronological-cut counterexample to the proposed replacement." + ], + "acceptance_gate": "A full boundary contract and paid profile; unchanged scalar counts alone are insufficient.", + "first_step": { + "command": [ + "python3", + "-B", + "research/r439-bsection-stars-seed01/verify.py" + ], + "expected": "PASS_R439_BSECTION_STARS", + "inspect": "Compare the two false H2/K flags with the unchanged paid profile in its README.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write one replacement H2/K implication for a single helper-star operation, then try to falsify it on dirty inputs.", + "bottleneck_link": "A legitimate replacement could admit a cheaper bit circuit; scalar savings alone do not alter the selected moment.", + "allowed_variations": [ + "Choose one helper-star or quartet instance; narrow to one boundary implication." + ], + "scope_change_triggers": [ + "Changing only source count or scalar addition count without an interface argument." + ], + "overlap_terms": [ + "H2_D_frame0_targets_from_helpers", + "K_equals_D", + "helper-star" + ] + }, + "scope_status": "refined", + "actual_scope": "One boundary implication of the inherited H2/K interface, tested exactly: can a common-frame helper entrance (#1253's 366 classes, all 4,954 supports, plus source donors) be compensated after the scatter instead of by a frame-0 prefix? Census on the selected PR589 word and the four merged star words (PR1062/1122/1188/1208), in a sound necessary class (LC-fav), the carrier-checked class A6 and A6 with storage relays (A6R).", + "scope_change_reason": "The card asks for a replacement H2/K interface and a falsification on dirty inputs or chronological cuts. Rather than proposing a new contract, this narrows the late-compensation relaxation of the zero-start rule that #1128 (PROOF section 4) and #1179 leave open by name, to compensation after the scatter on fixed A and scatter, one entrance at a time.", + "bottleneck_link": "Scoped negative result on the nonbinding bit side; no kappa. Moving the zero-start rule's compensation after the scatter admits no new entrance in the carrier-checked class A6 and, in the sound class LC-fav, only one open triple. Reason: every dirt-only space W_t is a coordinate subspace of at most 5 helpers (4 in A6), so only 98 (47) of 18,085 K incidences can be repaired late. A positive entrance would only save the pivot's first climb (-H1), which width-8 hosting cancels (#1179, #1253).", + "budget_minutes": 210, + "stop_rule": "Stop once every support of #1253's closure and every enumerated source donor is decided in LC-fav and A6 on all five words (support verdicts by two engines, donors and the relaxation by engine 1), the only LC-fav survivor is classified under A6R, and controls confirm both directions; report an A6R-only survivor as an open handoff.", + "outcome": "completed", + "evidence": "RESULT.json (identical on all five words): 4,954 supports. LC-fav admits only the #1179 kernel pair 444+470 (T empty) and the triple 444+470+578 (T = 8 targets); no single helper, no new pair, 0 of 5,212 enumerated (5,059 placeable) source donors. A6 admits only the kernel pair. Relaxation: one nonzero class (frame 79's line) with kernel {444+470, 578} (LC-fav) and {444+470} (A6), containing every admission. Every W_t is a coordinate subspace, dim <= 5 (LC-fav) and <= 4 (A6); covered K incidences 98 and 47 of 18,085. Triple: A6 covers 150 and 197; A6R(T only) 150, 153, 192, 197; A6R all 8, so it is OPEN. Engine 2 agrees on K, the closure (= #1253's certificate), every W_t and every support verdict. Controls: synthetic word admits 444+470 late at target 150 and its witness replays (and fails without its late reads; it equals #1179's entrance after B); K-bit flip and a relaxed carrier frame flip verdicts; flipped byte rejected; C reduces to the end of B. 20 tests pass.", + "author": "Sagar Thakrar (thakrarsagar)", + "ai_assistance": "Substantial: Claude (Anthropic) via Claude Code. Parallel read-only scout and judge subagents selected the question (both judges ranked it first); reader subagents and a synthesizer audited the scout's criterion (finding the triple the scout missed and the carrier gap in its strict class) and specified the classes; both engines, the proof note and the controls were then written fresh. A post-PR adversarial review corrected the witness description, the scope of the open triple, the citations and the controls (second commit).", + "open_questions": [ + { + "question": "Can the triple 444+470+578 be realised in LC-fav?", + "why_it_matters": "It is the only support surviving the sound test; within A6R its 8 targets are covered only through relays outside T, while a rewritten B reading 470 and source 77 directly is not excluded.", + "first_step": "Record the reads A6R uses per target, build a candidate (relays first, then a rewritten B reading 77 directly) and test it with wlib.replay and #1179's literal stream checks.", + "blocked_by": "Restoring the relay targets, or a legal rewritten B." + }, + { + "question": "Do two or more simultaneous entrances admit late compensation where single ones do not?", + "why_it_matters": "This census is one entrance at a time; the joint test needs (K_t c_i)_i in {(u c_i)_i : u in W_t} for every t.", + "first_step": "Run the joint test over pairs of disjoint supports in the same class V using the W_t spaces in RESULT.json.", + "blocked_by": "None." + }, + { + "question": "Does a different scatter enlarge W_t enough to admit a late single entrance?", + "why_it_matters": "The coordinate W_t of at most 5 helpers is a property of this scatter; added snapshot terms are already inside the class and change nothing.", + "first_step": "Move one retained total to another helper and recompute W_t.", + "blocked_by": "Pricing the changed COPY with #1128 section 5's argument." + } + ] +} diff --git a/research/r439-late-entrance-census-seed09/VERIFY.json b/research/r439-late-entrance-census-seed09/VERIFY.json new file mode 100644 index 0000000000..62ead3faff --- /dev/null +++ b/research/r439-late-entrance-census-seed09/VERIFY.json @@ -0,0 +1,43 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz", + "research/e8-bit-p111-tuned/tune/wlib.py", + "research/r439-abc-semantic-bridge/inputs/candidate.json.gz", + "research/r439-abc-zrewrite-seed16/CANDIDATE-WORD.json", + "research/r439-bsection-stars-seed01/candidate.json.gz", + "research/r439-gl5-shortest/candidate.json.gz", + "research/r439-kernel-entrance-closure/CERTIFICATE.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Byte binding of the PR589 word and the four merged star words, #1253's certificate and the replay library; per word: raw replay and K, first contacts, closure L (366 classes, equal to #1253's certificate), 4,954 supports; per-target dirt-only spaces in LC-fav (necessary test), the scout's strict class and A6, census of every support, linear relaxation per class, 5,212 source-donor entrances; Engine 2 (no shared code) reproduces K, the closure and every LC-fav and A6 space and support verdict; C reduces to the end of B; the relaxation contains every admission; A6R for the triple; controls (synthetic word with a replayed late witness that fails without its late reads, K/frame mutations, frame closure, flipped byte; census sanity checks); all five words identical; RESULT.json byte-identical." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "-m", + "unittest", + "discover", + "-s", + "{package}", + "-p", + "test_package.py" + ], + "timeout_seconds": 300, + "checks": "Byte flips and wrong pins rejected; closure and support counts; K response of the kernel pair and of 578; Engine 2 agreement; LC-fav and A6 census; no single helper; dimension bounds; A6 inside LC-fav; relaxation; pre-A window; K and carrier-frame mutations; dropped reader; synthetic witness replays and a broken witness fails; frame closure; recorded A6R status." + } + ] +} diff --git a/research/r439-late-entrance-census-seed09/census.py b/research/r439-late-entrance-census-seed09/census.py new file mode 100644 index 0000000000..a14205e4af --- /dev/null +++ b/research/r439-late-entrance-census-seed09/census.py @@ -0,0 +1,474 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Engine 1: late-compensated helper entrances on an R439 bit word (bitE8/1+mut), standard library only. + +Notation (README "Definitions"): sources 0..v-1, targets v..2v-1 (target t = register v+t), helpers 2v.. +(helper j = register 2v+j). A value is an int bitmask over the n = 2v+R dirty columns. Frames are closed +label lists, so containment is label-mask inclusion (checked against rational containment by Engine 2). +sigma = the cut right after the scatter; tau = number of B gates applied. +""" +import itertools +from collections import Counter, defaultdict +from fractions import Fraction as Q + + +# ------------------------------------------------------------------------------------------------ rationals +def rref(rows, ncol=8): + m = [[Q(x) for x in r] for r in rows] + rk = 0 + piv = [] + for c in range(ncol): + p = next((i for i in range(rk, len(m)) if m[i][c] != 0), None) + if p is None: + continue + m[rk], m[p] = m[p], m[rk] + pv = m[rk][c] + m[rk] = [a / pv for a in m[rk]] + for i in range(len(m)): + if i != rk and m[i][c] != 0: + f = m[i][c] + m[i] = [a - f * b for a, b in zip(m[i], m[rk])] + piv.append(c) + rk += 1 + return tuple(tuple(r) for r in m[:rk]), piv + + +def nullspace(rows, ncol=8): + b, piv = rref(rows, ncol) if rows else ((), []) + out = [] + for fc in (c for c in range(ncol) if c not in piv): + vec = [Q(0)] * ncol + vec[fc] = Q(1) + for r, pc in zip(b, piv): + vec[pc] = -r[fc] + out.append(tuple(vec)) + return out + + +def dot(a, b): + return sum(x * y for x, y in zip(a, b)) + + +def popcount(x): + return bin(x).count('1') + + +# ------------------------------------------------------------------------------------------------ the word +class Word: + def __init__(self, w): + self.w = w + self.v, self.R = w['v'], w['R'] + self.n = 2 * self.v + self.R + self.lines = w['lines'] + self.mask = [sum(1 << i for i in f) for f in w['frames']] + self.dim = [len(rref([self.lines[i] for i in f])[0]) if f else 0 for f in w['frames']] + self.tperp = [w['final'][self.v + t] for t in range(self.v)] + + def le(self, a, b): + """frame a inside frame b (closed frames: label inclusion).""" + return self.mask[a] & self.mask[b] == self.mask[a] + + def raw(self): + """Raw replay of A, scatter, B from val[r] = 1 << r (no D, no C). + + Returns the sigma state, the snapshots, the end state and K (K[t] = helper bits of raw y_t).""" + v, R, n, w = self.v, self.R, self.n, self.w + val = [1 << r for r in range(n)] + cur = list(w['start']) + for f, d, ss in w['A']: + for r in (d, *ss): + cur[r] = f + a = 0 + for s in ss: + a ^= val[s] + val[d] ^= a + snaps = [val[q] for q in w['ret']] + for t, row in enumerate(w['scatter']): + for k in row: + val[v + t] ^= snaps[k] + if not all(self.dim[cur[v + t]] == 0 for t in range(v)): + raise ValueError('a target leaves frame 0 before the scatter') + sigma_val, sigma_cur = list(val), list(cur) + for f, d, ss in w['B']: + a = 0 + for s in ss: + a ^= val[s] + val[d] ^= a + K = [(val[v + t] >> (2 * v)) & ((1 << R) - 1) for t in range(v)] + if not all(val[v + t] & ((1 << (2 * v)) - 1) == (1 << (v + t)) | (1 << t) for t in range(v)): + raise ValueError('raw word is not y -> y + x + K h (V = I, J = I)') + return dict(sigma_val=sigma_val, sigma_cur=sigma_cur, snaps=snaps, end_val=val, K=K) + + def first_contact(self): + """frame of the first A/B gate touching each helper (all helpers are touched in A).""" + v = self.v + first = {} + for sec in ('A', 'B'): + for f, d, ss in self.w[sec]: + for r in (d, *ss): + if r >= 2 * v and r not in first: + first[r] = (f, sec) + if len(first) != self.R or any(sec != 'A' for _, sec in first.values()): + raise ValueError('every helper must be first touched in A') + return {r: f for r, (f, _) in first.items()} + + def next_frames(self): + """next(r, tau): frame of r's first gate with index >= tau in B ++ C, else final[r].""" + nl = defaultdict(list) + for i, (f, d, ss) in enumerate(self.w['B'] + self.w['C']): + for r in (d, *ss): + nl[r].append((i, f)) + final = self.w['final'] + + def nxt(r, tau): + for i, f in nl.get(r, ()): + if i >= tau: + return f + return final[r] + return nxt + + +# ------------------------------------------------------------------------------------------------ closure L +def closure(word, first): + """distinct first-contact spaces, their nonzero pairwise intersections (#1253's L) and I(V).""" + v, R = word.v, word.R + spaces = {} + for j in range(R): + f = first[2 * v + j] + key = rref([word.lines[i] for i in word.w['frames'][f]])[0] + spaces.setdefault(key, []).append(2 * v + j) + gens = list(spaces) + planes = [g for g in gens if len(g) == 2] + L = set(gens) + meets = 0 + for a, b in itertools.combinations(planes, 2): + inter = nullspace(nullspace(list(a)) + nullspace(list(b))) + if inter: + if len(inter) != 1: + raise ValueError('two distinct planes meet in more than a line') + meets += 1 + L.add(rref(inter)[0]) + + def inside(V, F): + ann = nullspace(list(F)) + return all(dot(u, a) == 0 for u in V for a in ann) + elig = {V: sorted(r for key, regs in spaces.items() if inside(V, key) for r in regs) for V in L} + return dict(L=L, elig=elig, planes=len(planes), lines=len(gens) - len(planes), plane_pairs=len(planes) * (len(planes) - 1) // 2, + meets=meets) + + +def supports(elig): + """every nonzero c inside some I(V): {frozenset of registers: one V}.""" + out = {} + for V, I in elig.items(): + for k in range(1, len(I) + 1): + for S in itertools.combinations(I, k): + out.setdefault(frozenset(S), V) + return out + + +# ------------------------------------------------------------------------------------------------ spans +class Span: + """F2 echelon basis on int bitmasks keyed by leading bit.""" + __slots__ = ('b',) + + def __init__(self): + self.b = {} + + def add(self, x): + b = self.b + while x: + h = x.bit_length() - 1 + if h in b: + x ^= b[h] + else: + b[h] = x + return True + return False + + +def rotate(word, y_free=True): + """dirt to the low R bits, x (and y unless y_free) above: echelon vectors led by a dirt bit are x/y-free.""" + v, R = word.v, word.R + keep = (1 << v) - 1 if y_free else (1 << (2 * v)) - 1 + return lambda x: (x >> (2 * v)) | ((x & keep) << R) + + +def dirt_basis(span, R): + return sorted((x for h, x in span.b.items() if h < R), reverse=True) + + +def canonical(vectors): + """reduced echelon form of a set of bitmasks (for exact comparison between engines).""" + piv = {} + for x in vectors: + while x: + h = x.bit_length() - 1 + if h in piv: + x ^= piv[h] + else: + for k in list(piv): + if (piv[k] >> h) & 1: + piv[k] ^= x + piv[h] = x + break + out = {} + for h in sorted(piv): + x = piv[h] + for k in sorted(piv): + if k != h and (x >> k) & 1 and k in out: + x ^= out[k] + out[h] = x + return sorted(out.values(), reverse=True) + + +def W_fav(word, st, y_free=True): + """LC-fav: generators at sigma = registers (other than t) whose frame lies in t-perp, plus the snapshots.""" + v, R, n = word.v, word.R, word.n + rot = rotate(word, y_free) + out = [] + for t in range(v): + S = Span() + for c in st['snaps']: + S.add(rot(c)) + for r in range(n): + if r != v + t and word.le(st['sigma_cur'][r], word.tperp[t]): + S.add(rot(st['sigma_val'][r])) + out.append(dirt_basis(S, R)) + return out + + +def W_sweep(word, st, mode, y_free=True, next_override=None): + """Union over tau in [0, |B|] of the readable values, for mode 'fav', 'strict' (scout prototype: carrier frame in + t's next frame, no carrier check) or 'A6' (some F with cur_t + cur_r <= F <= next_t and next_r).""" + v, R, n = word.v, word.R, word.n + rot = rotate(word, y_free) + base_next = word.next_frames() + override = next_override or {} + + def nxt(r, tau): + return override[r] if r in override else base_next(r, tau) + val, cur = list(st['sigma_val']), list(st['sigma_cur']) + spans = [Span() for _ in range(v)] + for S in spans: + for c in st['snaps']: + S.add(rot(c)) + + def legal(t, r, tau): + if mode == 'fav': + return word.le(cur[r], word.tperp[t]) + nt = nxt(v + t, tau) + if mode == 'strict': + return word.le(cur[r], nt) + return word.le(cur[r], nt) and word.le(cur[v + t], nxt(r, tau)) + + for t in range(v): + for r in range(n): + if r != v + t and legal(t, r, 0): + spans[t].add(rot(val[r])) + for i, (f, d, ss) in enumerate(word.w['B']): + ops = (d, *ss) + for r in ops: + cur[r] = f + a = 0 + for s in ss: + a ^= val[s] + val[d] ^= a + touched_targets = {r - v for r in ops if v <= r < 2 * v} + for t in range(v): + regs = range(n) if t in touched_targets else ops + for r in regs: + if r != v + t and legal(t, r, i + 1): + spans[t].add(rot(val[r])) + return [dirt_basis(S, R) for S in spans] + + +# ------------------------------------------------------------------------------------------------ census +def response(K, cmask, donors=0): + return [t for t in range(len(K)) if (popcount(K[t] & cmask) + ((donors >> t) & 1)) & 1] + + +def admits(W, T, cmask): + return all(any(popcount(u & cmask) & 1 for u in W[t]) for t in T) + + +def census(word, K, W, sup): + """[(registers, |T|)] admitted by the per-target odd-parity test, kernel pairs (T empty) included.""" + v = word.v + out = [] + for S in sup: + cm = sum(1 << (r - 2 * v) for r in S) + T = response(K, cm) + if admits(W, T, cm): + out.append((tuple(sorted(S)), len(T))) + return sorted(out, key=lambda a: (len(a[0]), a[0])) + + +def coverage(word, K, W): + v, R = word.v, word.R + return sum(1 for t in range(v) for j in range(R) if (K[t] >> j) & 1 and any((u >> j) & 1 for u in W[t])) + + +def relax(word, K, W, elig): + """sound linear superset per class V: drop rows t whose W_t meets I(V); report the kernel of the rest.""" + v = word.v + out = {} + for V, I in elig.items(): + Im = sum(1 << (r - 2 * v) for r in I) + rows = [t for t in range(v) if not any(u & Im for u in W[t])] + piv = {} + kern = [] + for a, r in enumerate(I): + col = sum(((K[t] >> (r - 2 * v)) & 1) << k for k, t in enumerate(rows)) + comb = 1 << a + x = col + while x: + h = x.bit_length() - 1 + if h in piv: + x ^= piv[h][0] + comb ^= piv[h][1] + else: + piv[h] = (x, comb) + break + if not x: + kern.append(tuple(I[b] for b in range(len(I)) if (comb >> b) & 1)) + if kern: + out[V] = dict(kernel=kern, rows_kept=len(rows)) + return out + + +def donors(word, K, W, elig): + """source donors x_s ^= p at the entrance frame (line_s inside V); response K c + 1_{D_S}. + 'placeable' counts the donor sets whose span E_min = span(lines of D_S) lies inside every donor's first A frame + (each donor must sit at the entrance frame before A without descending).""" + v = word.v + lab = {s: rref([word.lines[s]])[0] for s in range(v)} + first_src = {} + for f, d, ss in word.w['A']: + for r in (d, *ss): + if r < v and r not in first_src: + first_src[r] = rref([word.lines[i] for i in word.w['frames'][f]])[0] + + def inside(V, F): + ann = nullspace(list(F)) + return all(dot(u, a) == 0 for u in V for a in ann) + checked, placeable, kernel, late = 0, 0, [], [] + for V, I in elig.items(): + srcs = [s for s in range(v) if inside(lab[s], V)] + for k in range(1, len(srcs) + 1): + for DS in itertools.combinations(srcs, k): + xs = sum(1 << s for s in DS) + emin = rref([word.lines[s] for s in DS])[0] + legal = all(inside(emin, first_src[s]) for s in DS) + for kk in range(1, len(I) + 1): + for J in itertools.combinations(I, kk): + checked += 1 + placeable += legal + cm = sum(1 << (r - 2 * v) for r in J) + T = response(K, cm, xs) + if not T: + kernel.append((DS, J)) + elif admits(W, T, cm): + late.append((DS, J, len(T))) + return dict(checked=checked, placeable=placeable, kernel=kernel, late=late) + + +# ------------------------------------------------------------------------------------------------ A6R (storage relays) +def a6r_coverable(word, st, J, only_targets=None, relays=True): + """A6 plus frame-tagged storage relays (relay restoration ignored: a superset). Values are projected to + (pivot parity on J, x, y); target t is coverable when its stores span a vector with pivot 1 and x = y = 0. + only_targets restricts which targets may receive inserted reads (the A6R(T-only) variant).""" + v, R, n = word.v, word.R, word.n + w = word.w + nxt_frame = word.next_frames() + cmJ = sum(1 << (r - 2 * v) for r in J) + xym = (1 << (2 * v)) - 1 + + def proj(x): + return (popcount((x >> (2 * v)) & cmJ) & 1) | ((x & xym) << 1) + val, cur = list(st['sigma_val']), list(st['sigma_cur']) + store = [dict() for _ in range(v)] # tag mask -> (Span, ordered list) + total = [Span() for _ in range(v)] + merged = {} + cm = [word.mask[c] for c in cur] + nr = [0] * n + + def sub(a, b): + return a & b == a + + def put(t, tag, x): + sp = store[t].get(tag) + if sp is None: + sp = store[t][tag] = (Span(), []) + if sp[0].add(x): + sp[1].append(x) + total[t].add(x) + return True + return False + for t in range(v): + for c in st['snaps']: + put(t, 0, proj(c)) + + def allowed(t): + return only_targets is None or (v + t) in only_targets + + def relay(t, u, work): + if not (allowed(t) and allowed(u)): + return + got = False + for tag, (sp, order) in list(store[u].items()): + key = (t, u, tag) + m = merged.get(key, 0) + if m >= len(order): + continue + F = cm[v + t] | cm[v + u] | tag + if sub(F, nr[v + t]) and sub(F, nr[v + u]): + for x in order[m:]: + got |= put(t, F, x) + merged[key] = len(order) + if got: + work.add(t) + + def step(tau, changed): + regs = range(n) if changed is None else changed + for r in regs: + cm[r] = word.mask[cur[r]] + nr[r] = word.mask[nxt_frame(r, tau)] + work = set() + for t in range(v): + if not allowed(t): + continue + rr = range(n) if (changed is None or (v + t) in changed) else changed + for r in rr: + if r == v + t: + continue + F = cm[v + t] | cm[r] + if sub(F, nr[v + t]) and sub(F, nr[r]): + if put(t, F, proj(val[r])): + work.add(t) + if not relays: + return + for x in [r - v for r in regs if v <= r < 2 * v]: + for y in range(v): + if y != x: + relay(x, y, work) + relay(y, x, work) + while work: + u = work.pop() + for t in range(v): + if t != u: + relay(t, u, work) + step(0, None) + for i, (f, d, ss) in enumerate(w['B']): + ops = (d, *ss) + for r in ops: + cur[r] = f + a = 0 + for s in ss: + a ^= val[s] + val[d] ^= a + step(i + 1, set(ops)) + return [v + t for t in range(v) if 0 in total[t].b] + + +def dims(W): + return dict(sorted(Counter(len(x) for x in W).items())) diff --git a/research/r439-late-entrance-census-seed09/engine2.py b/research/r439-late-entrance-census-seed09/engine2.py new file mode 100644 index 0000000000..5da10d0ce5 --- /dev/null +++ b/research/r439-late-entrance-census-seed09/engine2.py @@ -0,0 +1,240 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Engine 2: an independent recomputation (no code shared with census.py). + +- register values are Python sets of dirty columns (XOR = symmetric difference); +- frame geometry uses rational annihilators (containment = every basis row is orthogonal to the annihilator); +- the closure L is built from annihilators of first-contact spaces; +- W_t (LC-fav) is computed at sigma by a kernel method: eliminate the x part of the generators with combination + tracking, then take the dirt part of every x-free combination; +- W_t (A6) is computed per (target, register) pair by enumerating the change points of cur, next and value, + instead of sweeping time. +Outputs use the same dirt-bit convention as Engine 1 (bit j = helper register 2v + j) for exact comparison. +""" +from fractions import Fraction +from itertools import combinations + + +def _eliminate(rows, width): + """row-reduce rational rows; returns (independent reduced rows, pivot columns).""" + m = [list(map(Fraction, r)) for r in rows] + piv_cols, out, r0 = [], [], 0 + for c in range(width): + k = next((i for i in range(r0, len(m)) if m[i][c]), None) + if k is None: + continue + m[r0], m[k] = m[k], m[r0] + lead = m[r0][c] + m[r0] = [x / lead for x in m[r0]] + for i in range(len(m)): + if i != r0 and m[i][c]: + q = m[i][c] + m[i] = [a - q * b for a, b in zip(m[i], m[r0])] + piv_cols.append(c) + r0 += 1 + return [tuple(r) for r in m[:r0]], piv_cols + + +def annihilator(rows, width=8): + red, piv = _eliminate(rows, width) if rows else ([], []) + ann = [] + for free in range(width): + if free in piv: + continue + vec = [Fraction(0)] * width + vec[free] = Fraction(1) + for row, pc in zip(red, piv): + vec[pc] = -row[free] + ann.append(tuple(vec)) + return ann + + +class Geometry: + def __init__(self, w): + self.lines = w['lines'] + self.rows = [[self.lines[i] for i in f] for f in w['frames']] + self.ann = [annihilator(r) for r in self.rows] + self.memo = {} + + def contained(self, a, b): + key = (a, b) + if key not in self.memo: + self.memo[key] = all(sum(x * y for x, y in zip(u, z)) == 0 for u in self.rows[a] for z in self.ann[b]) + return self.memo[key] + + def closed(self, f, v): + """the frame's label list is exactly the set of live labels in its span.""" + inside = [i for i in range(v) if all(sum(x * y for x, y in zip(self.lines[i], z)) == 0 for z in self.ann[f])] + return inside + + +def replay_sets(w): + v, R = w['v'], w['R'] + n = 2 * v + R + val = [{r} for r in range(n)] + cur = list(w['start']) + versions = [[(0, frozenset(val[r]))] for r in range(n)] # per register: (tau, value) from sigma on + for f, d, ss in w['A']: + for r in (d, *ss): + cur[r] = f + for s in ss: + val[d] = val[d] ^ val[s] + snaps = [frozenset(val[q]) for q in w['ret']] + for t, row in enumerate(w['scatter']): + for k in row: + val[v + t] = val[v + t] ^ snaps[k] + sigma_val = [frozenset(x) for x in val] + sigma_cur = list(cur) + versions = [[(0, sigma_val[r])] for r in range(n)] + frames_hist = [[(0, sigma_cur[r])] for r in range(n)] + for i, (f, d, ss) in enumerate(w['B']): + for r in (d, *ss): + if frames_hist[r][-1][1] != f: + frames_hist[r].append((i + 1, f)) + for s in ss: + val[d] = val[d] ^ val[s] + versions[d].append((i + 1, frozenset(val[d]))) + K = [] + for t in range(v): + y = val[v + t] + if {c for c in y if c < 2 * v} != {t, v + t}: + raise ValueError('raw word is not y -> y + x + K h') + K.append(sum(1 << (c - 2 * v) for c in y if c >= 2 * v)) + return dict(snaps=snaps, sigma_val=sigma_val, sigma_cur=sigma_cur, versions=versions, frames_hist=frames_hist, K=K) + + +def first_contact(w): + v = w['v'] + first = {} + for f, d, ss in w['A'] + w['B']: + for r in (d, *ss): + if r >= 2 * v: + first.setdefault(r, f) + return first + + +def closure_classes(w, first): + """{annihilator-key of V: sorted eligible registers} for L = distinct first spaces and their pairwise meets.""" + geo = Geometry(w) + v = w['v'] + spaces = {} + for r, f in first.items(): + red = tuple(_eliminate(geo.rows[f], 8)[0]) + spaces.setdefault(red, []).append(r) + keys = list(spaces) + members = set(keys) + planes = [k for k in keys if len(k) == 2] + for a, b in combinations(planes, 2): + meet_ann = annihilator(list(a)) + annihilator(list(b)) + meet = annihilator(meet_ann) # the intersection = annihilator of the stacked annihilators + if meet: + members.add(tuple(_eliminate(meet, 8)[0])) + + def inside(V, F): + za = annihilator(list(F)) + return all(sum(x * y for x, y in zip(u, z)) == 0 for u in V for z in za) + return {V: sorted(r for key, regs in spaces.items() if inside(V, key) for r in regs) for V in members} + + +def _xfree_dirt(gens, v): + """dirt parts (bitmask over helpers) of all F2 combinations of gens whose x part (< v) vanishes.""" + piv = {} # pivot x-column -> (x set, dirt mask) + free = [] + for g in gens: + xs = {c for c in g if c < v} + dm = sum(1 << (c - 2 * v) for c in g if c >= 2 * v) + while xs: + p = max(xs) + if p in piv: + xs = xs ^ piv[p][0] + dm ^= piv[p][1] + else: + piv[p] = (xs, dm) + break + if not xs: + free.append(dm) + return free + + +def _basis(vectors): + b = {} + for x in vectors: + while x: + h = x.bit_length() - 1 + if h in b: + x ^= b[h] + else: + b[h] = x + break + return list(b.values()) + + +def W_fav(w, rep, geo): + v, R = w['v'], w['R'] + n = 2 * v + R + tperp = [w['final'][v + t] for t in range(v)] + out = [] + for t in range(v): + gens = list(rep['snaps']) + [rep['sigma_val'][r] for r in range(n) + if r != v + t and geo.contained(rep['sigma_cur'][r], tperp[t])] + out.append(_basis(_xfree_dirt(gens, v))) + # x-free here; note the generators are full values (x, y, dirt); y is projected out (y-free variant) + return out + + +def W_A6(w, rep, geo): + """per pair (t, r): change points = 0 and every tau = i+1 with B[i] touching t or r.""" + v, R = w['v'], w['R'] + n = 2 * v + R + B, C = w['B'], w['C'] + touch = [[] for _ in range(n)] + for i, (f, d, ss) in enumerate(B + C): + for r in (d, *ss): + touch[r].append((i, f)) + + def nxt(r, tau): + for i, f in touch[r]: + if i >= tau: + return f + return w['final'][r] + + def at(hist, tau): + out = hist[0][1] + for k, x in hist: + if k <= tau: + out = x + else: + break + return out + btouch = [{i + 1 for i, _ in touch[r] if i < len(B)} for r in range(n)] + out = [] + for t in range(v): + gens = list(rep['snaps']) + for r in range(n): + if r == v + t: + continue + for tau in sorted({0} | btouch[v + t] | btouch[r]): + ct, cr = at(rep['frames_hist'][v + t], tau), at(rep['frames_hist'][r], tau) + if geo.contained(cr, nxt(v + t, tau)) and geo.contained(ct, nxt(r, tau)): + gens.append(at(rep['versions'][r], tau)) + out.append(_basis(_xfree_dirt(gens, v))) + return out + + +def same_span(a, b): + ba, bb = _basis(a), _basis(b) + return len(ba) == len(bb) == len(_basis(list(a) + list(b))) + + +def admitted(K, W, classes, v): + sup = set() + for I in classes.values(): + for k in range(1, len(I) + 1): + for S in combinations(I, k): + sup.add(S) + out = [] + for S in sup: + cm = sum(1 << (r - 2 * v) for r in S) + T = [t for t in range(v) if bin(K[t] & cm).count('1') % 2] + if all(any(bin(u & cm).count('1') % 2 for u in W[t]) for t in T): + out.append((tuple(S), len(T))) + return sorted(out, key=lambda a: (len(a[0]), a[0])), len(sup) diff --git a/research/r439-late-entrance-census-seed09/test_package.py b/research/r439-late-entrance-census-seed09/test_package.py new file mode 100644 index 0000000000..a67dcbd533 --- /dev/null +++ b/research/r439-late-entrance-census-seed09/test_package.py @@ -0,0 +1,157 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Controls for the late-entrance census (about 40 s). + +Run: python3 -I -B -m unittest discover -s research/r439-late-entrance-census-seed09 -p test_package.py -v +""" +import copy +import json +import sys +import unittest +from pathlib import Path + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +import census as E # noqa: E402 +import engine2 as F # noqa: E402 +import verify as V # noqa: E402 + +RESULT = json.loads((HERE / 'RESULT.json').read_text()) +P = V.load_word(*V.WORDS['PR589']) +W = E.Word(P) +ST = W.raw() +K = ST['K'] +CL = E.closure(W, W.first_contact()) +SUP = E.supports(CL['elig']) +WF = E.W_fav(W, ST) +WA = E.W_sweep(W, ST, 'A6') +v = W.v + + +def cm(regs): + return sum(1 << (r - 2 * v) for r in regs) + + +class Binding(unittest.TestCase): + def test_word_byte_flip_rejected(self): + path, digest = V.WORDS['PR589'] + raw = bytearray((V.ROOT / path).read_bytes()) + raw[100] ^= 1 + with self.assertRaisesRegex(V.Reject, 'B word digest'): + V.load_word(path, digest, bytes(raw)) + + def test_wrong_pin_rejected(self): + path, _ = V.WORDS['PR1188'] + with self.assertRaisesRegex(V.Reject, 'B word digest'): + V.load_word(path, V.WORDS['PR589'][1]) + + +class Structure(unittest.TestCase): + def test_closure_and_supports(self): + self.assertEqual((len(CL['L']), len(SUP), CL['meets']), (366, 4954, 549)) + + def test_K_is_the_raw_response(self): + self.assertEqual(sum(bin(x).count('1') for x in K), 18085) + self.assertEqual(E.response(K, cm((444, 470))), []) # the #1179 kernel pair + self.assertEqual([v + t for t in E.response(K, cm((578,)))], [113, 118, 150, 153, 192, 197, 214, 219]) + + def test_engine2_agrees_on_K_and_spans(self): + rep = F.replay_sets(P) + geo = F.Geometry(P) + self.assertEqual(rep['K'], K) + self.assertTrue(all(F.same_span(a, b) for a, b in zip(WF, F.W_fav(P, rep, geo)))) + self.assertTrue(all(F.same_span(a, b) for a, b in zip(WA, F.W_A6(P, rep, geo)))) + + +class Census(unittest.TestCase): + def test_lc_fav_admits_only_the_kernel_pair_and_the_triple(self): + self.assertEqual(E.census(W, K, WF, SUP), [((444, 470), 0), ((444, 470, 578), 8)]) + + def test_a6_admits_only_the_kernel_pair(self): + self.assertEqual(E.census(W, K, WA, SUP), [((444, 470), 0)]) + + def test_no_single_helper_in_any_class(self): + for X in (WF, WA): + self.assertFalse([s for s, _ in E.census(W, K, X, SUP) if len(s) == 1]) + + def test_dimension_bounds(self): + self.assertEqual(max(len(x) for x in WF), 5) + self.assertEqual(max(len(x) for x in WA), 4) + + def test_a6_inside_lc_fav(self): + self.assertTrue(all(F.same_span(list(a) + list(b), list(b)) for a, b in zip(WA, WF))) + + def test_relaxation_is_a_superset_and_has_one_nonzero_class(self): + rel = E.relax(W, K, WF, CL['elig']) + self.assertEqual(len(rel), 1) + (V0, d), = rel.items() + self.assertEqual(len(V0), 1) + self.assertEqual(sorted(map(tuple, d['kernel'])), [(444, 470), (578,)]) + span = E.Span() + for kv in d['kernel']: + span.add(cm(kv)) + for S, _ in E.census(W, K, WF, SUP): # every LC-fav admission lies in the relaxed kernel + self.assertTrue(set(S) <= set(CL['elig'][V0])) + self.assertFalse(span.add(cm(S))) + + def test_result_records_the_same_census(self): + self.assertEqual(RESULT['summary']['LC_fav_late'], [[444, 470, 578]]) + self.assertEqual(RESULT['summary']['A6_late'], []) + self.assertEqual(RESULT['summary']['singles_admitted'], 0) + self.assertEqual(RESULT['summary']['source_donors_late'], 0) + + +class Controls(unittest.TestCase): + def test_sanity_pre_a_window_admits_everything(self): + allj = [1 << j for j in range(W.R)] + self.assertEqual(len(E.census(W, K, [list(x) + allj for x in WF], SUP)), len(SUP)) + + def test_flipped_K_bit_rejects_the_kernel_pair(self): + Kf = list(K) + Kf[1] ^= 1 << (470 - 2 * v) + self.assertEqual(E.census(W, Kf, WF, [frozenset((444, 470))]), []) + + def test_sanity_cleared_K_column_admits_578(self): + K0 = [x & ~(1 << (578 - 2 * v)) for x in K] + self.assertEqual(E.census(W, K0, WF, [frozenset((578,))]), [((578,), 0)]) + + def test_relaxed_carrier_frame_admits_the_triple_in_a6(self): + full = next(i for i, f in enumerate(P['frames']) if len(f) == v) + Wrel = E.W_sweep(W, ST, 'A6', next_override={77: full}) + self.assertEqual(E.census(W, K, Wrel, [frozenset((444, 470, 578))]), [((444, 470, 578), 8)]) + + def test_dropping_a_reader_breaks_the_admission(self): + # remove every snapshot and carrier contribution to target 150's LC-fav space: the triple is rejected + Wcut = [x if v + t != 150 else [] for t, x in enumerate(WF)] + self.assertEqual(E.census(W, K, Wcut, [frozenset((444, 470, 578))]), []) + + def test_synthetic_witness_replays(self): + wlib = V.load_wlib() + S, Wt = V.synthetic(P) + self.assertEqual((V.canonical_sha(S), V.canonical_sha(Wt)), (V.SYN_SHA, V.WITNESS_SHA)) + wlib.replay(Wt) + no_late = copy.deepcopy(Wt) + no_late['B'] = S['B'] # without its three post-scatter reads + with self.assertRaises(AssertionError): + wlib.replay(no_late) + bad = copy.deepcopy(Wt) + bad['C'] = bad['C'][:-1] # drop the closing shear: the witness must break + with self.assertRaises(AssertionError): + wlib.replay(bad) + + def test_frame_closure_detects_a_dropped_label(self): + bad = copy.deepcopy(P) + f = next(i for i, fr in enumerate(bad['frames']) if len(fr) >= 3) + bad['frames'][f] = bad['frames'][f][1:] + self.assertNotEqual(F.Geometry(bad).closed(f, v), bad['frames'][f]) + + def test_recorded_a6r_status(self): + trip = RESULT['words']['PR589']['late_survivors']['444,470,578'] + self.assertEqual(trip['T'], [113, 118, 150, 153, 192, 197, 214, 219]) + self.assertEqual(trip['A6_covered'], [150, 197]) + self.assertEqual(trip['A6R_T_only_covered'], [150, 153, 192, 197]) + self.assertEqual(trip['A6R_covered'], trip['T']) + self.assertEqual(RESULT['summary']['triple_status'], 'OPEN') + + +if __name__ == '__main__': + unittest.main() diff --git a/research/r439-late-entrance-census-seed09/verify.py b/research/r439-late-entrance-census-seed09/verify.py new file mode 100644 index 0000000000..1ac66a4354 --- /dev/null +++ b/research/r439-late-entrance-census-seed09/verify.py @@ -0,0 +1,345 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Scoped census: late-compensated helper entrances on the R439 bit word (no new kappa). + +Usage: python3 -I -B research/r439-late-entrance-census-seed09/verify.py [--write] + +The inherited H2/K implication says every helper starts at frame 0 so that a frame-0 prefix D can supply all dirt +compensation. #1128 (PROOF section 4) leaves 'compensation moved after A' open and #1179 states that K e_J = 0 is not +about arbitrary later compensation. This script asks, for every support J of a common-frame entrance (#1253's 366 +classes, 4,954 supports) on the selected PR589 word and the four merged star words, whether the entrance can be +compensated after the scatter instead: + + B byte binding of the five words, #1253's certificate and the replay library (sha256 pins); + E1 Engine 1 (census.py): raw replay and K, first contacts, the closure L and I(V), and per target t the dirt-only + space W_t in three classes: LC-fav (the necessary test, PROOF.md theorem), the scout prototype's strict class, + and A6 (fixed raw paths, inserted target reads with a carrier check, read-only relays); the parity census of + every support, the sound linear relaxation per class, and source-donor entrances; + E2 Engine 2 (engine2.py, no shared code): set-valued replay and K, rational-annihilator geometry, the closure + (also equal to #1253's certificate), W_t for LC-fav (kernel method) and A6 (per-pair change points); exact + agreement of every W_t and every verdict; + R A6R (A6 plus frame-tagged storage relays, restoration ignored) for the only late LC-fav survivor; + C controls: a synthetic word whose built late witness replays (and fails without its late reads), K / frame + mutations that flip verdicts, frame closure, a flipped byte; plus sanity checks of the census (pre-A window, + the #1179 kernel pair, a cleared K column) and of the relaxation (a superset of every admission). + +Expected last line: PASS_R439_LATE_ENTRANCE_CENSUS +""" +import argparse +import copy +import gzip +import hashlib +import json +import sys +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +sys.path.insert(0, str(HERE)) +import census as E # noqa: E402 +import engine2 as F # noqa: E402 + +WORDS = { + 'PR589': ('research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz', + 'e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f'), + 'PR1062': ('research/r439-bsection-stars-seed01/candidate.json.gz', + 'b452d2c2b0b2a546d1105b1da9769aa78e5c54d6f00e97b30c77e3f54ce445ee'), + 'PR1122': ('research/r439-abc-semantic-bridge/inputs/candidate.json.gz', + '2b09a7a3851cdf2a7f19350d1555cf75788d001c9507a37e459cd931881ee066'), + 'PR1188': ('research/r439-gl5-shortest/candidate.json.gz', + '4e7904d01ebdbfc60a26472b4e0d2e813c19c2fe1a4bb8ab390c12746a1da359'), + 'PR1208': ('research/r439-abc-zrewrite-seed16/CANDIDATE-WORD.json', + '66b34404f39f5f612c2aaadd53ae33eb9f5993ec2065c82e23d7467cce03a226'), +} +CERT_1253 = ('research/r439-kernel-entrance-closure/CERTIFICATE.json', + 'f08b9de12089687fe6c0c6b2eb985d0e6a883b72fa4f08ded11d34d875f48909') +WLIB = ('research/e8-bit-p111-tuned/tune/wlib.py', 'a37fdf3cdf5f62945c2a90193401c0e9edc9dd3cda8d8cb36a3b9c329ebe4dbc') +SYN_SHA = 'a33bf677cb43b26f27e18bf29b5618ded5a17d04987ddb71d8ce4f2de4401ea1' +WITNESS_SHA = 'cf7aa7a94141fd18623e0ce489f67d86c725f17ec0856bbc23b4700d66c5d00a' +KERNEL_PAIR = (444, 470) +TRIPLE = (444, 470, 578) + + +class Reject(Exception): + """A check failed; the argument is the label of the check.""" + + +def need(ok, label): + if not ok: + raise Reject(label) + + +def sha(data): + return hashlib.sha256(data).hexdigest() + + +def canonical_sha(w): + return sha(json.dumps(w, sort_keys=True, separators=(',', ':')).encode()) + + +def load_word(path, digest, raw=None): + raw = (ROOT / path).read_bytes() if raw is None else raw + need(sha(raw) == digest, 'B word digest: ' + path) + try: + data = gzip.decompress(raw) if raw[:2] == b'\x1f\x8b' else raw + except OSError: + raise Reject('B word does not decompress: ' + path) + try: + w = json.loads(data) + except ValueError: + raise Reject('B word is not JSON: ' + path) + need(w.get('format') == 'bitE8/1+mut' and w.get('h') == 8 and w.get('form') == '/2', 'B word header: ' + path) + return w + + +def load_wlib(): + path, digest = WLIB + need(sha((ROOT / path).read_bytes()) == digest, 'B replay library digest') + sys.path.insert(0, str((ROOT / path).parent)) + import wlib + return wlib + + +def regs(c): + return [list(x) for x in c] + + +# ------------------------------------------------------------------------------------------------ one word +def analyse(name, w, cert_classes, run_a6r=True): + W = E.Word(w) + st = W.raw() + K = st['K'] + first = W.first_contact() + cl = E.closure(W, first) + sup = E.supports(cl['elig']) + full = next(i for i, f in enumerate(w['frames']) if len(f) == W.v) + # A6 inserts reads anywhere in B ++ C; the sweeps stop at the end of B. C is entirely at FULL and touches no target, + # and no target ends at FULL, so a read during C sees the end-of-B value and the same legality as at tau = |B|. + need(all(g[0] == full for g in w['C']) and not any(W.v <= r < 2 * W.v for g in w['C'] for r in (g[1], *g[2])) + and all(w['final'][W.v + t] != full for t in range(W.v)), 'E1 reads during C reduce to the end of B') + Wf, Wfs = E.W_fav(W, st), E.W_sweep(W, st, 'fav') + Wstrict, Wa = E.W_sweep(W, st, 'strict'), E.W_sweep(W, st, 'A6') + need(all(E.canonical(a) == E.canonical(b) for a, b in zip(Wf, Wfs)), 'E1 LC-fav at sigma = union over the sweep') + need(all(E.canonical(a) == E.canonical(b) for a, b in zip(Wf, E.W_fav(W, st, y_free=False))), 'E1 y-free = y-zero') + # the classes are nested: A6 inside LC-fav + need(all(F.same_span(list(a) + list(b), list(b)) for a, b in zip(Wa, Wf)), 'E1 A6 spans inside LC-fav spans') + res = {} + for cls, X in (('LC_fav', Wf), ('strict_proto', Wstrict), ('A6', Wa)): + adm = E.census(W, K, X, sup) + coord = all(all(bin(u).count('1') == 1 for u in E.canonical(x)) for x in X) + res[cls] = dict(admitted=[[list(s), nT] for s, nT in adm], covered_K_incidences=E.coverage(W, K, X), dim_W=E.dims(X), + coordinate_subspaces=coord) + for cls, X in (('LC_fav', Wf), ('A6', Wa)): + rel = E.relax(W, K, X, cl['elig']) + res[cls]['relax366'] = [dict(dim_V=len(V), kernel=regs(d['kernel']), rows_kept=d['rows_kept']) for V, d in + sorted(rel.items(), key=lambda kv: (len(kv[0]), kv[0]))] + # the relaxation is a superset: every admitted support lies in the relaxed kernel of some class containing it + for S, _ in E.census(W, K, X, sup): + cmS = sum(1 << (r - 2 * W.v) for r in S) + ok = False + for V, I in cl['elig'].items(): + if set(S) <= set(I) and V in rel: + span = E.Span() + for kv in rel[V]['kernel']: + span.add(sum(1 << (r - 2 * W.v) for r in kv)) + ok = ok or not span.add(cmS) + need(ok, 'E1 relaxation contains every admitted support: ' + cls) + don = E.donors(W, K, X, cl['elig']) + res[cls]['source_donors'] = dict(enumerated=don['checked'], placeable=don['placeable'], kernel=len(don['kernel']), + late=len(don['late'])) + # Engine 2 + rep = F.replay_sets(w) + geo = F.Geometry(w) + need(rep['K'] == K, 'E2 K agrees') + need(F.first_contact(w) == first, 'E2 first contacts agree') + classes = F.closure_classes(w, first) + need(sorted(map(tuple, classes.values())) == sorted(map(tuple, cl['elig'].values())), 'E2 closure agrees') + need(sorted(map(tuple, classes.values())) == cert_classes, 'E2 closure = #1253 certificate') + Wf2, Wa2 = F.W_fav(w, rep, geo), F.W_A6(w, rep, geo) + need(all(F.same_span(a, b) for a, b in zip(Wf, Wf2)), 'E2 LC-fav spans agree') + need(all(F.same_span(a, b) for a, b in zip(Wa, Wa2)), 'E2 A6 spans agree') + for cls, X in (('LC_fav', Wf2), ('A6', Wa2)): + adm2, nsup = F.admitted(K, X, classes, w['v']) + need(nsup == len(sup) and [[list(s), nT] for s, nT in adm2] == res[cls]['admitted'], 'E2 verdicts agree: ' + cls) + need(all(geo.closed(f, w['v']) == w['frames'][f] for f in range(len(w['frames']))), 'E2 every frame is closed') + # A6R for the late LC-fav survivors + late = [tuple(s) for s, nT in res['LC_fav']['admitted'] if nT > 0] + survivors = {} + for J in late: + cm = sum(1 << (r - 2 * W.v) for r in J) + T = [W.v + t for t in E.response(K, cm)] + entry = dict(T=T) + if run_a6r: + full = set(E.a6r_coverable(W, st, J)) + tonly = set(E.a6r_coverable(W, st, J, only_targets=set(T))) + plain = set(E.a6r_coverable(W, st, J, relays=False)) + entry.update(A6_covered=sorted(set(T) & plain), A6R_covered=sorted(set(T) & full), + A6R_T_only_covered=sorted(set(T) & tonly)) + survivors[','.join(map(str, J))] = entry + dv = [1 << r for r in range(W.n)] + for f, d, ss in w['D']: + a = 0 + for s in ss: + a ^= dv[s] + dv[d] ^= a + N = [(dv[W.v + t] >> (2 * W.v)) & ((1 << W.R) - 1) for t in range(W.v)] + colw = [sum((K[t] >> j) & 1 for t in range(W.v)) for j in range(W.R)] + return dict(gates={k: len(w[k]) for k in 'DABC'}, K_nonzeros=sum(colw), K_column_weights=[min(colw), max(colw)], + N_equals_K=N == K, closure=dict(size=len(cl['L']), plane_pairs=cl['plane_pairs'], meeting_pairs=cl['meets'], + supports=len(sup)), + classes=res, late_survivors=survivors, + engines_agree=True), (W, st, K, cl, sup, Wf, Wa) + + +# ------------------------------------------------------------------------------------------------ controls +def synthetic(P): + """W_syn: three inserted target reads make the {444,470} entrance late-compensable at target 150; the witness + realises it (start[444] = 79, shear at the head of A, its inverse at the end of C, D without 444).""" + S = copy.deepcopy(P) + S['B'] = [[0, 150, [149]]] + P['B'][:37] + [[323, 150, [149]], [323, 150, [470]]] + P['B'][37:] + S['D'] = [[f, d, [s for s in ss if not (d == 150 and s == 470)]] for f, d, ss in P['D']] + Wt = copy.deepcopy(S) + Wt['start'][444] = 79 + Wt['A'] = [[79, 470, [444]]] + S['A'] + Wt['B'] = [[0, 150, [149]]] + S['B'][:38] + [[323, 150, [149]], [323, 150, [470]]] + S['B'][38:] + Wt['C'] = S['C'] + [[1, 470, [444]]] + Wt['D'] = [[f, d, [s for s in ss if s != 444]] for f, d, ss in P['D']] + return S, Wt + + +def controls(P, ctx, wlib): + W, st, K, cl, sup, Wf, Wa = ctx + v = W.v + out = {} + # (a) pre-A window: every helper readable at frame 0 before A -> every support admitted + allj = [1 << j for j in range(W.R)] + pre = [list(x) + allj for x in Wf] + n_pre = len(E.census(W, K, pre, sup)) + need(n_pre == len(sup), 'C pre-A window admits every support') + out['sanity_pre_A_window'] = 'with every unit vector added to every W_t, %d/%d supports are admitted' % (n_pre, len(sup)) + # (b) the #1179 kernel pair: T empty, admitted by every class + cm = sum(1 << (r - 2 * v) for r in KERNEL_PAIR) + need(not E.response(K, cm), 'C kernel pair has T empty') + out['sanity_kernel_pair'] = '444+470: K e_J = 0 (the #1179 entrance), so admitted in every class' + # (c) synthetic word with a built witness + S, Wt = synthetic(P) + need(canonical_sha(S) == SYN_SHA and canonical_sha(Wt) == WITNESS_SHA, 'C synthetic words reproduce their digests') + wlib.replay(S) + wlib.replay(Wt) + late_only = copy.deepcopy(Wt) + late_only['B'] = S['B'] # the witness without its three post-scatter reads + try: + wlib.replay(late_only) + need(False, 'C witness without its late reads must fail replay') + except AssertionError as exc: + need(exc.args and exc.args[0] == 150, 'C witness without its late reads fails at register 150') + Sneg = copy.deepcopy(S) + Sneg['D'] = P['D'] + try: + wlib.replay(Sneg) + need(False, 'C synthetic negative must fail replay') + except AssertionError as exc: + need(exc.args and exc.args[0] == 150, 'C synthetic negative fails at register 150') + SW = E.Word(S) + sst = SW.raw() + sK = sst['K'] + sfirst = SW.first_contact() + ssup = E.supports(E.closure(SW, sfirst)['elig']) + syn_fav = E.census(SW, sK, E.W_fav(SW, sst), ssup) + syn_a6 = E.census(SW, sK, E.W_sweep(SW, sst, 'A6'), ssup) + T_syn = [v + t for t in E.response(sK, cm)] + need(T_syn == [150] and (KERNEL_PAIR, 1) in syn_fav and (KERNEL_PAIR, 1) in syn_a6, 'C synthetic: 444+470 late at 150, admitted') + out['synthetic'] = dict(word_sha256=SYN_SHA, witness_sha256=WITNESS_SHA, kernel_pair_T=T_syn, + admitted_LC_fav=[[list(s), nT] for s, nT in syn_fav], admitted_A6=[[list(s), nT] for s, nT in syn_a6], + witness_replay='PASS', witness_paid=wlib.paid(Wt), synthetic_paid=wlib.paid(S), + witness_without_late_reads='fails replay at register 150', + negative='W_syn with the unedited D fails replay at register 150', + note='the late reads undo W_syn\'s own moved compensation, so after B the witness carries the same ' + 'values as #1179\'s prefix entrance on PR589: a realisable late entrance, not a new construction') + # (d) mutations flip verdicts + Kf = list(K) + Kf[1] ^= 1 << (470 - 2 * v) + need(not any(s == KERNEL_PAIR for s, _ in E.census(W, Kf, Wf, [frozenset(KERNEL_PAIR)])), 'C flipped K bit rejects 444+470') + K0 = [x & ~(1 << (578 - 2 * v)) for x in K] + need(((578,), 0) in E.census(W, K0, Wf, [frozenset((578,))]), 'C zero K column admits 578 (sanity: T empty)') + full = next(i for i, f in enumerate(P['frames']) if len(f) == v) + Wrel = E.W_sweep(W, st, 'A6', next_override={77: full}) + trip = E.census(W, K, Wrel, [frozenset(TRIPLE)]) + need(trip == [(TRIPLE, 8)], 'C relaxing next_77 to FULL admits the triple in A6') + out['mutations'] = dict(flip_K_bit='444+470 rejected after flipping K[target 112, helper 470]', + sanity_zero_K_column='578 admitted (T empty) after clearing column 578', + relax_next_77='444+470+578 admitted by A6 when register 77 may be read at FULL') + # (e) closure: dropping a label from a closed frame breaks closure + bad = copy.deepcopy(P) + f = next(i for i, fr in enumerate(bad['frames']) if len(fr) >= 3) + bad['frames'][f] = bad['frames'][f][1:] + need(F.Geometry(bad).closed(f, v) != bad['frames'][f], 'C a frame with a dropped label is not closed') + out['frame_closure'] = 'all frames closed (label inclusion = rational containment); a dropped label is detected' + path, digest = WORDS['PR589'] + raw = bytearray((ROOT / path).read_bytes()) + raw[100] ^= 1 + try: + load_word(path, digest, bytes(raw)) + need(False, 'C a flipped word byte must be rejected') + except Reject as exc: + need(str(exc).startswith('B word digest'), 'C a flipped word byte is rejected by its digest') + out['flipped_byte'] = 'rejected by the word digest' + return out + + +def main(): + ap = argparse.ArgumentParser(description=__doc__.split('\n\n')[0]) + ap.add_argument('--write', action='store_true') + ap.add_argument('--no-a6r', action='store_true', help='skip the slow A6R runs (partial)') + a = ap.parse_args() + cert_raw = (ROOT / CERT_1253[0]).read_bytes() + need(sha(cert_raw) == CERT_1253[1], 'B #1253 certificate digest') + cert = sorted(tuple(c['eligible_helpers']) for c in json.loads(cert_raw)['classification']['classes']) + wlib = load_wlib() + words = {name: load_word(*pin) for name, pin in WORDS.items()} + results, ctx = {}, None + for name, w in words.items(): + results[name], c = analyse(name, w, cert, run_a6r=not a.no_a6r) + print('%-7s LC-fav %s A6 %s' % (name, results[name]['classes']['LC_fav']['admitted'], results[name]['classes']['A6']['admitted'])) + if name == 'PR589': + ctx = c + first = json.dumps(results['PR589']['classes'], sort_keys=True) + same = {name: json.dumps(r['classes'], sort_keys=True) == first and r['late_survivors'] == results['PR589']['late_survivors'] + for name, r in results.items()} + need(all(same.values()), 'all five words give the same census') + ctrl = controls(words['PR589'], ctx, wlib) + lc = results['PR589']['classes'] + a6r = results['PR589']['late_survivors'].get(','.join(map(str, TRIPLE)), {}) + need(a.no_a6r or {'A6_covered', 'A6R_covered', 'A6R_T_only_covered'} <= set(a6r), 'R A6R computed for the triple') + summary = dict( + supports=results['PR589']['closure']['supports'], + singles_admitted=sum(1 for s, _ in lc['LC_fav']['admitted'] if len(s) == 1), + new_pairs_admitted=sum(1 for s, nT in lc['LC_fav']['admitted'] if len(s) == 2 and nT > 0), + LC_fav_late=[s for s, nT in lc['LC_fav']['admitted'] if nT > 0], + A6_late=[s for s, nT in lc['A6']['admitted'] if nT > 0], + source_donors_late=lc['LC_fav']['source_donors']['late'], + triple_status=('NOT_COMPUTED' if 'A6R_covered' not in a6r else + 'OPEN' if a6r['A6R_covered'] == a6r['T'] else 'EXCLUDED_IN_A6R')) + result = dict(status='PASS_R439_LATE_ENTRANCE_CENSUS', summary=summary, words=results, controls=ctrl, + inputs={k: dict(path=p, sha256=d) for k, (p, d) in WORDS.items()}, + certificate_1253=dict(path=CERT_1253[0], sha256=CERT_1253[1]), + scope='Scoped census: late (post-scatter) compensation of single common-frame entrances on fixed A/scatter; ' + 'no change to A or the scatter, no pre-scatter wires, one entrance at a time; no construction and no new kappa') + text = json.dumps(result, indent=1, sort_keys=True) + '\n' + target = HERE / 'RESULT.json' + if a.no_a6r: + print('PARTIAL (no A6R)') + return + if a.write: + target.write_text(text) + else: + need(target.read_text() == text, 'RESULT.json reproduced byte for byte') + print('summary', json.dumps(summary, sort_keys=True)) + print('PASS_R439_LATE_ENTRANCE_CENSUS') + + +if __name__ == '__main__': + try: + main() + except Reject as exc: + raise SystemExit('FAIL ' + str(exc))