attack-pass F2: k = 3 and 4 lines closed at the solver cap (no trail under 29 to 35 and 39 to 47 differential, 24 to 28 linear); row PASS effort-bounded

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>

docs/analysis/attack-pass-2026-10.md

@@ -22,7 +22,7 @@ against the log before quoting it to the project lead.
 | # | Attack | Gate (same as 1.4) | Result so far | Status |
 |---|---|---|---|---|
 | F1 | Shadow block compressibility and shortcut search | no compression of the shadow block beyond the honest compiler's simplification, measured against that compiler on the same program; the 27 repetitions never fewer than 27x (coordinator's ruling 7 Oct 2026, 12:3x UK; the plan's gate (1) and row F1 carry the same) | 10^4 and 10^5 class v4 programs: saved instructions mean 0.62%, max 5.078% at 10^5 (1 of 100,000 over 5%, 0 over 10%); nothing folds or dedupes across the 27 passes; every saving is local peephole algebra that clang -O3 removes from the honest kernel too (IR counts match on the worst programs), so against the compiler the compression is 0; 0 mismatches in 2 x 10^5 differential and verifier checks, z3 window proofs 0 counterexamples. AP-F1-1 routed to the v5 list as a shadow redundancy bound. Record `docs/analysis/attack-pass/f1-shadow.md` | PASS; AP-F1-1 on the v5 list |
-| F2 | Mixer round margin (SAT/MILP, 1 to 4 keyed applications) | no distinguisher or shortcut beyond 2 of the 8 applications | one application characterised (differential weight 10 to 12, linear 1, verified on the real code on three days); two applications: no trail at or below weight 20 to 24 within 7,200 s per job, the MSB and LSB families die at two; rotational-XOR no bias at one application; the multiply layer folds on 0 of 2^20 inputs, k applications cost k; k = 3, 4 general jobs closing on the box. Record `docs/analysis/attack-pass/f2-mixer.md` | PASS (effort-bounded; k = 3, 4 lines pending) |
+| F2 | Mixer round margin (SAT/MILP, 1 to 4 keyed applications) | no distinguisher or shortcut beyond 2 of the 8 applications | one application characterised (differential weight 10 to 12, linear 1, verified on the real code on three days); two applications: no trail at or below weight 20 to 24 within 7,200 s per job, the MSB and LSB families die at two; rotational-XOR no bias at one application; the multiply layer folds on 0 of 2^20 inputs, k applications cost k; three applications: no differential trail at or below weight 29 to 35 and no linear at or below 24 to 28, four: 39 to 47 and 24, every job at its 7,200 s cap. Record `docs/analysis/attack-pass/f2-mixer.md` | PASS (effort-bounded) |
 | F3 | Chained cache j+1 bound and storage-vs-recompute curve | no derivation under j+1 blocks; curve monotone; f=1 point unchanged | 0 of 64 and 0 of 1,024 lines under j+1 (exhaustive closure search, cross-checked by exhaustive pebbling at 10 lines, 10,240 pairs, 0 mismatches); both planted broken chains fire; curve monotone at both op counts; f=1 point 9,360 ops per item unchanged. Record `docs/analysis/attack-pass/f3-cache.md` | PASS |
 | F4 | Weak-day census over 2^24 day keys | fraction of days with gain over 1.1x under 2^-20 | PASS against M2 (DSP-bound datapath): 0 of 2^28 days over 1.1x; planted weak days fire; every ROT and RC class 0. Bound finding AP-F4-1 on M1 (LUT adders): 5,476 of 2^24 days (3.26e-4) over 1.1x as the tail of a sum, no weak class; worst public-calendar day 29,337 at 1.121x, at most 12.1% more rate that day for a per-day LUT FPGA, 0 for any chip; redraw rule (NAF sum under 163 rejected) routed to the next class. Record `docs/analysis/attack-pass/f4-weakday.md` | PASS (v4); AP-F4-1 routed to the next class |
 | F5 | Chip-model sweep + AWS F2 FPGA hour | evidence row 17 holds across the sweep; FPGA row under 27 M reads/s/W | sweep: 2.1x at k=1 GDDR7 reproduces, 3.2x at k=0.5, 4.1x at k=0.3 (matches ledger M32); FPGA row 2.3 to 2.9 G/s, 10 to 20 M reads/s/W (literature). FINDING: the k=0.33 figure is framed as the X9's measured core (M32) and a "measured class" (ladder branch §5a); the X9 was withdrawn before launch and never benchmarked. F2 hour SKIPPED: no AWS account | FIXED-AND-PASSED (sweep PASS; AP-F5-1 fixed and re-gated 7 Oct 2026: chip section re-run 2.1x at k=1 unchanged, identity grep 0 hits, site lane concurred); F2 hour SKIPPED-BY-DECISION (the project lead, 7 Oct 2026, 09:5x UK; plan 4.2 row F5 is the sweep only at 3714c2a0; the FPGA row stays the JEDEC-ceiling model row labelled unmeasured) |

docs/analysis/attack-pass/f2-mixer.md

@@ -101,9 +101,25 @@ are reported.
 | diff/general | 2026-10-03 | nomul | 2 | none | 20 | no | 7 | | 1,309 |
 | diff/general, diff/msb | 2026-10-03 | rot0 (known fail) | 1, 2, 4 | 0 | | yes | 0 | probability 1 | under 1 |
 
-The general model's k = 3 and k = 4 jobs on the three days (7,200 s each) were still running at the Mac's reboot and
+The general model's k = 3 and k = 4 jobs (closed 14:3x UTC, every job at its 7,200 s cap, `logs/summary.md`):
-their lines are appended from `logs/summary.md` when they close; a trail of weight under 32 at k = 3 would be a
+
-finding and is not expected (the per-application floor is 10 to 12).
+| Model | Day | k | Best trail found | No trail at or below (model) | Per-application floor | Solver s |
+|---|---|---|---|---|---|---|
+| diff/general | 2026-10-03 | 3 | none | 35 | 12 | 7,201 (cap) |
+| diff/general | 2026-10-03 | 4 | none | 47 | 12 | 7,359 (cap) |
+| diff/general | 2026-10-04 | 3 | none | 29 | 10 | 7,350 (cap) |
+| diff/general | 2026-10-04 | 4 | none | 39 | 10 | 7,279 (cap) |
+| diff/general | 2027-03-01 | 3 | none | 35 | 12 | 7,321 (cap) |
+| diff/general | 2027-03-01 | 4 | none | 47 | 12 | 7,284 (cap) |
+| lin/general | 2026-10-03 | 3 | none | 24 | 1 | 7,953 (cap) |
+| lin/general | 2026-10-03 | 4 | none | 24 | 1 | 7,352 (cap) |
+| lin/general | 2026-10-04 | 3 | none | 28 | 1 | 7,373 (cap) |
+| lin/general | 2026-10-04 | 4 | none | 24 | 1 | 7,393 (cap) |
+| lin/general | 2027-03-01 | 3 | none | 24 | 1 | 7,402 (cap) |
+
+No trail of weight under 32 at three applications (the finding line): the bound reached is 29 to 35 at three and
+39 to 47 at four for differentials, 24 to 28 at three and 24 at four for linear masks, all solver-capped, so these are
+effort bounds, not proofs; they grow with k as the per-application floors predict.
 
 ### 4.3 Linear trails
 
@@ -176,9 +192,9 @@ after the stated search.
 
 Verdict: PASS with the effort bound stated: about 60 solver jobs, 2 to 29 minutes each, on three day keys; the
 reduced-round margin reached is one application fully characterised (weights 10 to 12 differential, 1 linear) and
-two applications with no trail under weight 20 to 24, against 8 applications between reads, so the margin between
+two applications with no trail under weight 20 to 24, three with none under 29 to 35 (differential) and 24 to 28
-what the search reaches and what the construction uses is 6 applications. The k = 3 and k = 4 general jobs
+(linear), four with none under 39 to 47 and 24, against 8 applications between reads, so the margin between what the
-strengthen this when they close. What this does not do is in section 7; the lower bound is the paid question.
+search reaches and what the construction uses is at least 4 applications at the solver's cap. What this does not do is in section 7; the lower bound is the paid question.
 
 ## 6. Consequences per tier