From 489583c5116e6ee0fb9c08a5437e3065fc6a6818 Mon Sep 17 00:00:00 2001 From: igneum-labs <337424239+igneum-labs@users.noreply.github.com> Date: Wed, 7 Oct 2026 19:41:41 +0000 Subject: [PATCH] adv-mixer-3 report: queue 18 withdrawn from build-2 (ledger), SAT k=2 CNF size Co-Authored-By: Claude Fable 5.1 --- docs/analysis/cryptanalysis/report-mixer-3.md | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/docs/analysis/cryptanalysis/report-mixer-3.md b/docs/analysis/cryptanalysis/report-mixer-3.md index c8072af42..e62b89b0f 100644 --- a/docs/analysis/cryptanalysis/report-mixer-3.md +++ b/docs/analysis/cryptanalysis/report-mixer-3.md @@ -253,7 +253,7 @@ under a millisecond on one core. The solver at k = 1 is five orders slower than |---|---|---|---|---|---|---| | 20729 | 1 (smoke, build-1) | 33,873 | 112,328 | SATISFIABLE | 137 s | t = 0x49880000, index 0x20eb79 = target | | 20729 | 1 (queue 08, build-2) | 33,873 | 112,328 | SATISFIABLE | 1,593 s (box at load 500) | the same t | -| 20729 | 2 | pending | pending | running | | | +| 20729 | 2 | 68,624 | 227,767 | not run (the lease was withdrawn before it was granted) | | | 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 @@ -280,7 +280,8 @@ CNF out of the worktree mirror into /srv/builds/_adv-mixer-3/. Both applied befo | Queue 16 (index 20733 k = 2..4) under the sweep lock | build-2 | 19:13 | 7 min | k = 2 was running when killed | | Every adv-mixer-3 process killed | build-1, build-2 | 19:20:51 to 19:21:01 | | main's rule (relayed by the coordinator at 19:20 UTC): no sweep starts except through the build-server lane's `lease pool`; everything hand-started is killed now. Killed by pid file, process group: 03 (sac 20729: k = 5 at 2^24 and the 2^27 rows lost), 09 (sac0: the day 20733 2^28 rows lost), 10 (index 20733 k = 5..8 lost), 04 (sac 20733 k = 5..8 lost), 08 (CaDiCaL on k = 2 for 20729, about 7 min in, lost; k = 3, 4 and day 20733 not started), 16 (index 20733 k = 2..4 lost). Zero processes of this lane remained on either box at 19:21:01 UTC. Nothing of this lane ran until `lease pool` existed | | Re-queue through `lease pool` | build-1 (queue 17: sac 20729 k = 5..8 and 2^27 rows, sac 20733 k = 5..8, index 20733 k = 2..8, sac0 20733 2^28 rows), build-2 (queue 18: CaDiCaL k = 2..4, both days) | 19:24 UTC (relaunched 19:2x after a guard line refused on the first start) | running | `lease pool 48 --min 16` per census (the lease sizes the harness threads to the cores it took), `lease pool 1 --min 1` per CaDiCaL; waits behind the release builds and the class v5 suites, which outrank every sweep tonight | -| v5 yield | both | 19:26, widened 19:31 | | before every lease the driver sleeps while any waiter in `lease status` is owned by class-v5 or labelled v5; both drivers restarted with the rule before their first lease was granted | +| v5 yield | both | 19:26, widened 19:31 | | before every lease the driver sleeps while any waiter in `lease status` is owned by class-v5 or labelled v5; both drivers restarted with the rule before their first lease was granted; refined 19:32 to yield by owner (class-v5, or attack-pass with v5), never to another adv- lane | +| 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 | | 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--k.log and sac--k.log under /srv/builds/_adv-mixer-3/logs/ on build-1, read by this lane | ## The round margin, stated