From 7d76d9a08bb72c7d56fcc8857113fa4168e2d3e9 Mon Sep 17 00:00:00 2001 From: igneum-labs <337424239+igneum-labs@users.noreply.github.com> Date: Wed, 7 Oct 2026 20:13:58 +0000 Subject: [PATCH] adv-mixer: cadical re-queued (third run) through lease pool on box 2 Internal adversarial pass, not an independent review. Co-Authored-By: Claude Fable 5.1 --- docs/analysis/cryptanalysis/report-mixer.md | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/docs/analysis/cryptanalysis/report-mixer.md b/docs/analysis/cryptanalysis/report-mixer.md index b0f05c8d..07743082 100644 --- a/docs/analysis/cryptanalysis/report-mixer.md +++ b/docs/analysis/cryptanalysis/report-mixer.md @@ -243,8 +243,9 @@ that subcommand exists (at 20:21 BST `lease --help` offered `lease cores` and `l through `lease pool 1` at 20:22 BST the minute the subcommand landed (log sat-commute-20729-lease.log), then RELEASED at 20:41 BST on main's order so the class v5 census (owner class-v5, 88 cores, the 0.3.24 critical path) can take box 2's pool: 1,106 s run, no SAT or UNSAT. Two cadical runs total 2,855 s of solving on this instance -with no decision, which is the expected shape for a preimage-sized search. Status: BLOCKED on pool priority, to -be re-queued after the census is confirmed running. +with no decision, which is the expected shape for a preimage-sized search. Re-queued a third time at 21:13 BST +when main opened box 2 (log sat-commute-20729-lease2.log, core 9, cap to 22:13 BST). RUNNING; the row lands +here. ## Q1 consolidated verdict (internal adversarial pass, not an independent review) @@ -320,6 +321,7 @@ wall times above are under heavy sharing. | 20:20 | main: every hand-started sweep is killed by its pid file now and re-queued through `lease pool`; release builds and the class v5 suites outrank sweeps | killed cadical (box 2, 29 min lost, no result) and sibling 07 (box 1, 6 of 56 steps done, claim released); nothing started since; `lease pool` absent at 20:21, so the re-queue waits on it | | 20:22 | `lease pool` live on both boxes (lease sha f814b447) | cadical re-queued the same minute through `lease pool 1 --owner adv-mixer --nice 10`, core 8, 1 h cap | | 20:41 | main: box 2's pool must show 0 adv-* holders for the class v5 census; the yield to a class-v5 waiter is mechanical at shard end from now | released the cadical lease by pid file; nothing held on either box | +| 21:13 | main: box 2 open to adv-* (the class v5 census ended, no pool lease there) | cadical re-queued the same minute as `lease pool 1 --min 1`, core 9 | | 20:4x | pool priority classes (release > v5 > measure > adv, lease sha 5d84d644); a 1-thread holder is never pre-empted; label rule: no "release", "canary", "pair", "v5 gate", "v5 kit" or "measure" in a sweep label | the cadical re-queue keeps its label "adv-mixer cadical commutation CNF day 20729, 1 h cap", which carries none of the reserved words, and goes out as `lease pool 1 --min 1` when main confirms the census is running | | 20:2x | pool rule: a sweep lease asks for at most 48 cores with --min at the least usable; the yield test is by OWNER (refined at 20:3x): yield to a waiter whose owner is class-v5, or whose owner is attack-pass with "v5" in its label, never to a waiter whose owner starts with adv-; on a yield, finish the shard in hand and release; release builds and v5 suites outrank every sweep | adopted for any further lease; the one-core cadical lease is cleared by main to its 21:23 BST cap | @@ -329,7 +331,7 @@ wall times above are under heavy sharing. |---|---|---|---|---|---| | cadical on adv-mixer-commute-20729.cnf | 2 | sat-commute-20729.log.pid | 19:20:41Z | 1,749 s of a 3,600 s cap, no SAT or UNSAT | RE-QUEUED 19:22:46Z (20:22 BST) through `lease pool 1 --owner adv-mixer --nice 10` the minute the subcommand landed; holding 1 pool core, 1 h cap; pid file sat-commute-20729-lease.log.pid | | 07-adv-mixer-3-days.sh (owner adv-mixer-3) | 1 | queue-07-adv-mixer-3-days.sh.log.pid | 19:20:47Z | 50 of 56 steps unrun; the 6 done are in the owner's logs | claim released; owner or next free lane | -| cadical, the leased re-run (lease pool 1, core 8) | 2 | sat-commute-20729-lease.log.pid | 19:41:11Z (20:41 BST), main's order so the class v5 census takes box 2's pool | 1,106 s of a fresh 3,600 s cap, no SAT or UNSAT; 2,494 s of cap lost | re-queue through `lease pool 1 --min 1` after main confirms the census is running; the yield to class-v5 waiters is mechanical from now | +| cadical, the leased re-run (lease pool 1, core 8) | 2 | sat-commute-20729-lease.log.pid | 19:41:11Z (20:41 BST), main's order so the class v5 census takes box 2's pool | 1,106 s of a fresh 3,600 s cap, no SAT or UNSAT; 2,494 s of cap lost | RE-QUEUED 20:13:28Z (21:13 BST) on main's word that box 2 is open: `lease pool 1 --min 1 --owner adv-mixer --nice 10`, core 9, class adv, 1 h cap to 22:13 BST; pid file sat-commute-20729-lease2.log.pid; a 1-thread holder is never pre-empted | Both kills were the wrapper pid from the pid file plus its descendants (one cadical, one adv-mixer-3), TERM then KILL; no process of this lane remained on either box afterwards.