igneum-network/igneum
1
0
Fork 0
Code Issues Pull requests Releases Activity

adv-mixer: SAT row final (three CaDiCaL runs, 6,455 s, undecided: bound on solver reach), logs in the branch

Browse source 
Internal adversarial pass, not an independent review.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
This commit is contained in:
igneum-labs 2026-10-07 21:14:46 +00:00
parent eac9a75ada
commit fb288b9599
4 changed files with 37 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
docs/analysis/cryptanalysis/logs/adv-mixer/sat-commute-20729-lease.log Normal file
View file

@ -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

8
docs/analysis/cryptanalysis/logs/adv-mixer/sat-commute-20729-lease2.log Normal file
View file

@ -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

3
docs/analysis/cryptanalysis/logs/adv-mixer/sat-commute-20729.log Normal file
View file

@ -0,0 +1,3 @@
start 2026-10-07T18:51:32Z
Command terminated by signal 15
wall=1749.20 s maxrss=162680 KB

25
docs/analysis/cryptanalysis/report-mixer.md
View file

@ -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.