adv-mixer-3 report: SAT ladder closed on both days (k=1 solved, k=2..4 timeout), totals at the close, nothing running

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

docs/analysis/cryptanalysis/logs/adv-mixer-3/18-adv-mixer-3-lease-sat.log

@@ -28,3 +28,6 @@ wall=3600.02 s maxrss=163992 KB
 == cnf day 20733 k=4 2026-10-08T02:05:10Z
 t0=0x12345678 target index (low 22 bits of s[0]) = 0x20534f
 cnf: vars=136782 clauses=454243 written to /srv/builds/_adv-mixer-3/cnf/d20733-k4.cnf
+cadical rc=0 (10 sat, 20 unsat, 124 timeout)
+wall=3600.04 s maxrss=173856 KB
+end 2026-10-08T03:05:10Z

docs/analysis/cryptanalysis/logs/adv-mixer-3/sat-20733-k4.log

@@ -1 +1,5 @@
 lease: holding 1 pool cores (62, waited 0 s, class adv): adv-mixer-3 cadical 20733 k4
+c UNKNOWN
+Command exited with non-zero status 124
+wall=3600.04 s maxrss=173856 KB
+lease: released 1 pool cores after 3600 s, exit 124

docs/analysis/cryptanalysis/report-mixer-3.md

@@ -31,7 +31,7 @@ Plant rule: a tool is trusted once it has fired on a known-failed shape. Which s
 | Q4 | single-bit linear correlations, random states, 2^26 samples | k = 0 (the identity, fired: c = 1.0 on the diagonal) | no cell beyond 6 sigma (band 0.00073) | day 20729 k = 1..7 and day 20733 k = 1..8: worst c between 0.00055 and 0.00062 (z 4.5 to 5.1; the expected maximum of 262,144 normals is 4.8), 0 cells beyond 6 sigma on every row; day 20729 k = 8 running | PASS from k = 1 (BOUND) |
 | Q4b | t-bit linear correlations on the round-0 input, 2^26 samples | k = 0 (fired: c = 1.0, t bit 0 to s[8] bit 0) | no cell beyond 6 sigma | both days, k = 1..8: worst c 0.00046 to 0.00059 (z 3.7 to 4.9 over 16,384 cells), 0 cells beyond 6 sigma | PASS from k = 1 (BOUND) |
 | Q5 | rotational-XOR, rotations 1, 8, 16, 2^22 samples | `weak0` at k = 1 (fired: 740 zero-difference words of 2^20 at r = 1, 245 at r = 16) | no zero-difference word above 2 of N, no repeated difference above 3 | both days, k = 1, 2, 3, 4 at 2^22 samples: 0 zero-difference words at every rotation (random expects about 0.001), most frequent per-word difference multiplicity 3 (the birthday expectation at 2^22 draws of 32 bits) | PASS from k = 1 (BOUND: the XOR constants and the odd multiply kill the rotational property inside one application) |
-| Q6 | SAT (CaDiCaL) on the round-0 input: find t with a given 22-bit index after k applications | k = 1 solved and verified | solve inside one hour per k, time against the honest 2^10 x k x 130 ops | k = 1: SATISFIABLE in 137 s wall on build-1 (load about 160) and 1,593 s on build-2 (load about 500), the same model t = 0x49880000 both times, verified to the target 0x20eb79 through the real code; k = 2: TIMEOUT at the one-hour cap (68,624 vars, 227,767 clauses); k = 3: TIMEOUT (103,375 vars, 343,206 clauses); k = 4: TIMEOUT (138,126 vars, 458,645 clauses). Honest: 2^10 trials is under a millisecond at every k | PASS at k = 1..4 on day 20729 (BOUND: no SAT shortcut, the solver loses to brute force at k = 1 and does not return at k = 2, 3 or 4 inside an hour); day 20733 k = 2 and 3 TIMEOUT too; k = 4 RUNNING under the cap |
+| Q6 | SAT (CaDiCaL) on the round-0 input: find t with a given 22-bit index after k applications | k = 1 solved and verified | solve inside one hour per k, time against the honest 2^10 x k x 130 ops | k = 1: SATISFIABLE in 137 s wall on build-1 (load about 160) and 1,593 s on build-2 (load about 500), the same model t = 0x49880000 both times, verified to the target 0x20eb79 through the real code; k = 2: TIMEOUT at the one-hour cap (68,624 vars, 227,767 clauses); k = 3: TIMEOUT (103,375 vars, 343,206 clauses); k = 4: TIMEOUT (138,126 vars, 458,645 clauses). Honest: 2^10 trials is under a millisecond at every k | PASS on both days, k = 1..4 (BOUND: no SAT shortcut, the solver loses to brute force at k = 1 and does not return at k = 2, 3 or 4 inside an hour on either day) |
 | Q7 | days: 20733 on every row, 8 fixed day indices on Q1 and Q2 (queue 07, run by the sibling adv-mixer from the shared queue) | as above | as above | day 20733: every row above; all eight days complete (index uniform at k = 2, 3, 4, 8; sac clean at k = 2, 3, 4 on every day); ten days in all show the same margin | PASS (BOUND) |
 | GPU | any GPU row | n/a | n/a | no GPU on either box | BLOCKED |
 
@@ -298,7 +298,7 @@ under a millisecond on one core. The solver at k = 1 is five orders slower than
 | 20729 | 4 | 138,126 | 458,645 | TIMEOUT at the one-hour cap (status 124), 175 MB | 3,600 s | none |
 | 20733 | 2 | 67,944 | 225,543 | TIMEOUT at the one-hour cap (status 124), 139 MB | 3,600 s | none |
 | 20733 | 3 | 102,363 | 339,893 | TIMEOUT at the one-hour cap (status 124), 164 MB | 3,600 s | none |
-| 20733 | 4 | the same shape, the day's constants | | running from 02:05 UTC, one-hour cap | | |
+| 20733 | 4 | 136,782 | 454,243 | TIMEOUT at the one-hour cap (status 124), 174 MB | 3,600 s | none |
 
 Reading: the one-application model is a 32-variable problem with 112 k clauses of ripple-carry adders (16
 constant multiplies of up to 32 adders each dominate). CaDiCaL needs minutes on it where the honest search needs
@@ -332,6 +332,7 @@ CNF out of the worktree mirror into /srv/builds/_adv-mixer-3/. Both applied befo
 | Queue 17 reordered | build-1 | 00:1x | the restarted 2^27 row's first 10 min | at 4 cores a sac 2^27 row (2^36 applications) is about 3 hours, so the cheaper sac0 day 20733 2^28 rows (2^33 applications) now run first and the two 2^27 rows last; the driver was restarted on the new order |
 | Queue 17 finished | build-1 | 01:3x | | every harness row of this lane is in: the last row (sac 20729 k = 3 at 2^27) landed on a 24-core lease; no process of this lane remains on build-1 |
 | Queue 07 (the eight random days) claimed and run by this lane | build-1 | 01:19 to 02:17 | 58 min | the last unclaimed file on the shared queue; six day-20730 rows had been run by adv-mixer and were skipped; 50 rows under 32-core leases, no pre-emption; no process of this lane remains on build-1 |
+| Queue 18 finished | build-2 | 03:05 | 4 single-core hours (one per row, k = 2, 3, 4 of day 20733, plus k = 4 of 20729 earlier) | the last row (day 20733 k = 4) timed out at the cap at 03:05 UTC; no process of this lane remains on either box |
 | Queue 18 withdrawn from build-2 | build-2 | 19:35 | 0 (no lease was ever granted) | main's order: every adv-* waiter leaves box 2 until the class v5 census runs; the SAT rows k = 2..4 re-queue there afterwards |
 | Priority classes in the lease (release > v5 > measure > adv) | build-1 | 19:42 | | queue 17 killed and re-submitted once under the ranked tool as `lease pool 32 --min 16` (an adv holder at 32 threads or fewer is never pre-empted); waiting on free cores at 19:43 UTC; still waiting at 19:57 behind eleven adv-class waiters |
 | Queue 18 unclaimed on the shared queue | build-2 | 19:58 | | box 2 is closed to adv-* leases until the class v5 census runs; the claim was released so whichever lane has time when it reopens can run the SAT rows (CaDiCaL at ~/adv-mixer-3-tools/cadical/build/cadical on both boxes; the file is self-contained) |
@@ -339,12 +340,13 @@ CNF out of the worktree mirror into /srv/builds/_adv-mixer-3/. Both applied befo
 | Pre-emption at any size (lease sha ce30e357) | both | 21:21, applied 22:2x | | a release or v5 waiter that has waited 120 s pre-empts adv holders of any size with SIGTERM; both drivers now wrap every shard in run_shard (retry the same lease line until the log carries a result, log each PREEMPTED line with its time, skip rows already done). Queue 17 restarted while waiting on its sac 20729 k = 8 lease (nothing lost); queue 18 restarted on CaDiCaL k = 3 about 15 min into its hour (that partial solve lost, restarted from zero) |
 | Queue 07 (8 random days) | build-1 | 18:5x | running | claimed and run by the sibling lane adv-mixer from the shared queue; its logs are index-<day>-k<k>.log and sac-<day>-k<k>.log under /srv/builds/_adv-mixer-3/logs/ on build-1, read by this lane |
 
-Totals at 00:05 UTC on 8 October: about 3.0 wall-hours of sweep time on the two boxes (build-1 about 1.9, build-2
-about 1.1; every sweep ran beside other lanes on boxes at load 100 to 600 on 96 cores, so these are loaded-box
-hours, not core-hours) plus 4 single-core CaDiCaL hours; pod-hours 0 (no GPU on either box). Under the 8-hour
-reading line.
+Totals at the close, 03:10 UTC on 8 October: about 5.0 wall-hours of harness sweep time on the two boxes (build-1
+about 3.9 including queue 17's leased rows and queue 07's 58 minutes, build-2 about 1.1; every sweep ran beside
+other lanes on boxes at load 100 to 600 on 96 cores, so these are loaded-box hours, not core-hours) plus 8
+single-core CaDiCaL hours (k = 1 twice, k = 2, 3, 4 on each day); pod-hours 0 (no GPU on either box). Under the
+8-hour reading line on wall time.
 
-Partial rows, named: Q3 k = 8 was killed at 19:20 UTC and not re-queued (k = 2..7 are clean on both days); Q2 at 2^27 (k = 2, 3) and Q2b day 20733 at 2^28 are done; Q6 day 20733 k = 2..4 in queue 18; Q7 is complete on all eight days; multi-bit linear masks and a MILP trail bound were not attempted.
+Partial rows, named: Q3 k = 8 was killed at 19:20 UTC and not re-queued (k = 2..7 are clean on both days); Q2 at 2^27 (k = 2, 3) and Q2b day 20733 at 2^28 are done; Q6 is complete on both days; Q7 is complete on all eight days; multi-bit linear masks and a MILP trail bound were not attempted.
 
 ## The round margin, stated