From 03569a2144c2a6373912711cd0f5baabc67e7739 Mon Sep 17 00:00:00 2001 From: igneum-labs <337424239+igneum-labs@users.noreply.github.com> Date: Wed, 7 Oct 2026 19:41:45 +0000 Subject: [PATCH] adv-mixer: cadical lease released for the class v5 census; ledger and SAT row updated Internal adversarial pass, not an independent review. Co-Authored-By: Claude Fable 5.1 --- docs/analysis/cryptanalysis/report-mixer.md | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/docs/analysis/cryptanalysis/report-mixer.md b/docs/analysis/cryptanalysis/report-mixer.md index e36b18854..d08cd78d7 100644 --- a/docs/analysis/cryptanalysis/report-mixer.md +++ b/docs/analysis/cryptanalysis/report-mixer.md @@ -240,8 +240,11 @@ outcome inside the hour: the instance is a preimage-shaped search on a 2^512 spa reach only and is no evidence either way. The CNF stays on box 2 at /srv/builds/_adv-adv-mixer/logs/adv-mixer-commute-20729.cnf (6.8 MB) for a re-queue through `lease pool` once that subcommand exists (at 20:21 BST `lease --help` offered `lease cores` and `lease status` only). Re-queued -through `lease pool 1` at 20:22 BST the minute the subcommand landed (log sat-commute-20729-lease.log); RUNNING -under a fresh one-hour cap; the row lands here. +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. ## Q1 consolidated verdict (internal adversarial pass, not an independent review) @@ -316,6 +319,7 @@ wall times above are under heavy sharing. | 19:3x | drop SIGSTOP yield, run on cores 8-95 only | no yield was ever added; run-box.sh band set to 8-95; direct nohup runs at nice 10 | | 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 | | 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 | ### Kill ledger (main's rule, 20:20 BST) @@ -324,6 +328,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 | 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.