From fb288b9599be2a3d6da6117ecbc0191f7ef9c3fb Mon Sep 17 00:00:00 2001 From: igneum-labs <337424239+igneum-labs@users.noreply.github.com> Date: Wed, 7 Oct 2026 21:14:46 +0000 Subject: [PATCH] adv-mixer: SAT row final (three CaDiCaL runs, 6,455 s, undecided: bound on solver reach), logs in the branch Internal adversarial pass, not an independent review. Co-Authored-By: Claude Fable 5.1 --- .../adv-mixer/sat-commute-20729-lease.log | 7 ++++++ .../adv-mixer/sat-commute-20729-lease2.log | 8 ++++++ .../logs/adv-mixer/sat-commute-20729.log | 3 +++ docs/analysis/cryptanalysis/report-mixer.md | 25 ++++++++++++++----- 4 files changed, 37 insertions(+), 6 deletions(-) create mode 100644 docs/analysis/cryptanalysis/logs/adv-mixer/sat-commute-20729-lease.log create mode 100644 docs/analysis/cryptanalysis/logs/adv-mixer/sat-commute-20729-lease2.log create mode 100644 docs/analysis/cryptanalysis/logs/adv-mixer/sat-commute-20729.log diff --git a/docs/analysis/cryptanalysis/logs/adv-mixer/sat-commute-20729-lease.log b/docs/analysis/cryptanalysis/logs/adv-mixer/sat-commute-20729-lease.log new file mode 100644 index 000000000..e720b17fe --- /dev/null +++ b/docs/analysis/cryptanalysis/logs/adv-mixer/sat-commute-20729-lease.log @@ -0,0 +1,7 @@ +start 2026-10-07T19:22:46Z via lease pool +lease: holding 1 pool cores (8, waited 0 s): adv-mixer cadical commutation CNF day 20729, 1 h cap +Terminated +Command terminated by signal 15 +wall=1105.77 s maxrss=149688 KB +Terminated +lease: released 1 pool cores after 1106 s, exit 143 diff --git a/docs/analysis/cryptanalysis/logs/adv-mixer/sat-commute-20729-lease2.log b/docs/analysis/cryptanalysis/logs/adv-mixer/sat-commute-20729-lease2.log new file mode 100644 index 000000000..506b1a024 --- /dev/null +++ b/docs/analysis/cryptanalysis/logs/adv-mixer/sat-commute-20729-lease2.log @@ -0,0 +1,8 @@ +start 2026-10-07T20:13:28Z via lease pool, third run +lease: holding 1 pool cores (9, waited 0 s, class adv): adv-mixer cadical commutation CNF day 20729, 1 h cap +c UNKNOWN +Command exited with non-zero status 124 +wall=3600.01 s maxrss=204136 KB +lease: released 1 pool cores after 3600 s, exit 124 +cadical rc=124 (10 sat, 20 unsat, 124 timeout) +end 2026-10-07T21:13:28Z diff --git a/docs/analysis/cryptanalysis/logs/adv-mixer/sat-commute-20729.log b/docs/analysis/cryptanalysis/logs/adv-mixer/sat-commute-20729.log new file mode 100644 index 000000000..85c37bab7 --- /dev/null +++ b/docs/analysis/cryptanalysis/logs/adv-mixer/sat-commute-20729.log @@ -0,0 +1,3 @@ +start 2026-10-07T18:51:32Z +Command terminated by signal 15 +wall=1749.20 s maxrss=162680 KB diff --git a/docs/analysis/cryptanalysis/report-mixer.md b/docs/analysis/cryptanalysis/report-mixer.md index 077430828..2129d59b6 100644 --- a/docs/analysis/cryptanalysis/report-mixer.md +++ b/docs/analysis/cryptanalysis/report-mixer.md @@ -244,8 +244,21 @@ through `lease pool 1` at 20:22 BST the minute the subcommand landed (log sat-co 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. 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. +when main opened box 2 (log sat-commute-20729-lease2.log, core 9) and ran to its full one-hour cap: rc 124, +3,600.01 s wall, 204 MB peak, neither SAT nor UNSAT. + +| Run | Start (BST) | End | Wall | Outcome | +|---|---|---|---|---| +| 1, hand-started | 19:51 | killed 20:20 under the lease rule | 1,749 s | no decision | +| 2, lease pool 1 | 20:22 | released 20:41 for the class v5 census | 1,106 s | no decision | +| 3, lease pool 1 --min 1 | 21:13 | cap 22:13 | 3,600 s | timeout, no decision | + +Verdict for the SAT row: BOUND on solver reach only. 6,455 s of CaDiCaL 3.0.1 on one core did not decide +whether any of the 2^512 states commutes under the two key orders. That is the expected shape: the instance is a +preimage-sized search with about one expected solution, so neither SAT nor UNSAT was reachable in an hour, and +the probabilistic probe (0 agreements in 1,454,080,000 trials over 1024 days) remains the operative evidence. The +model (105,652 variables, 361,188 clauses) is kept in the branch logs by its log and on box 2 as the CNF for a +longer solve if one is ever worth the pool time; it would not change the fold bound either way. ## Q1 consolidated verdict (internal adversarial pass, not an independent review) @@ -258,7 +271,7 @@ keyed applications between two cache reads costs less than 8 times one applicati | An exact linear or affine relation across the composition | GF(2) kernel 0 (rank 1025 of 1025) at K = 1, 2 and 8 on 16 days; kernel 0 on the 22 address bits at K = 1 and 2 | ruled out exactly (chance survivor 2^-7167) | | A low-degree algebraic form to batch the applications | cube-sums nonzero at every d up to 16 after one application, saturated at 256 of 512 bits after two, on 32 days | ruled out below degree 16; above 16 is owed | | A predictable line index that lets a chip prefetch the read early | address bits predictable only after 1 application (incomplete diffusion, no linear leak); clean from K = 2 | at most 1 of 8 applications hides behind the memory latency | -| An exact commutation witness (SAT model) | 105,652-variable, 361,188-clause instance; cadical 3.0.1 running under a 1 h cap | pending; a timeout bounds solver reach only | +| An exact commutation witness (SAT model) | 105,652-variable, 361,188-clause instance; CaDiCaL 3.0.1, 6,455 s over three runs, no SAT or UNSAT | undecided; bounds solver reach only, the 0-in-1.45e9 probe stands | Priced against the chip model: 0 ops saved per item; 9,360 ops per item stand. What a longer pass would add: an exact algebraic-degree measurement above 16 (the cube test stops at 2^16 points) and a solver run long @@ -303,10 +316,10 @@ No GPU pods used: pod-hours 0. All CPU, nice 10, both boxes. | Q1 deepening queue 13 lineindex + addr linrel | box 1 | 77 s | | Q1 deepening queue 14 linrel + cnf | box 2 | 10 s | | Q1 deepening queue 15 per-K fill + fold-sweep replication | box 2 | 2 min 52 s | -| cadical on the commutation CNF | box 2 | one thread, capped at 1 h | +| cadical on the commutation CNF, three runs | box 2 | one thread: 1,749 s + 1,106 s + 3,600 s = 1.8 core-hours | | Sibling 07-adv-mixer-3-days.sh (owner adv-mixer-3) | box 1 | running | -Total about 0.6 box-hours of the 8-hour first-results budget (ask line 16), plus up to 1 core-hour of cadical. +Total about 0.6 box-hours of the 8-hour first-results budget (ask line 16), plus 1.8 core-hours of cadical. Pod-hours 0. Both boxes ran at load 240 to 555 on 96 cores during the deepening (sibling sweeps, not builds), so wall times above are under heavy sharing. @@ -331,7 +344,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-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 | +| 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; ran to its 1 h cap at 22:13 BST, rc 124, no decision, lease released; pid file sat-commute-20729-lease2.log.pid | 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.