diff --git a/docs/analysis/cryptanalysis/report-mixer-3.md b/docs/analysis/cryptanalysis/report-mixer-3.md index bb6be717..faa27f43 100644 --- a/docs/analysis/cryptanalysis/report-mixer-3.md +++ b/docs/analysis/cryptanalysis/report-mixer-3.md @@ -276,7 +276,8 @@ CNF out of the worktree mirror into /srv/builds/_adv-mixer-3/. Both applied befo | Queue 01 and 02 killed | build-1, build-2 | 18:57, 18:58 | 15 min, 11 min | the one-sweep-per-box rule; re-queued as 10 | | Queue 10 (index 20729 k = 5..8, 20733 k = 5..8) under the sweep lock | build-1 | 19:00 | 21 min | 20729 k = 5..8 done; 20733 k = 5 was running when killed | | 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 runs until `lease pool` exists; the lost rows are queue 17, written in the lease form | +| 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 | | 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 diff --git a/tools/attack/adv-mixer-3/queue/07-adv-mixer-3-days.sh b/tools/attack/adv-mixer-3/queue/07-adv-mixer-3-days.sh index d25aaea5..b3920422 100644 --- a/tools/attack/adv-mixer-3/queue/07-adv-mixer-3-days.sh +++ b/tools/attack/adv-mixer-3/queue/07-adv-mixer-3-days.sh @@ -1,17 +1,17 @@ #!/usr/bin/env bash # adv-mixer-3 queue file (owner: adv-mixer-3). Self-contained: binary, args, logs. Runs at nice 10 on cores 8-95 via run-box.sh. set -uo pipefail -X=/srv/builds/_adv-mixer-3/bin/x-lock.sh; L=/srv/builds/_adv-mixer-3/logs; mkdir -p "$L" +X="/srv/builds/_adv-mixer-3/bin/x-lock.sh days"; L=/srv/builds/_adv-mixer-3/logs; mkdir -p "$L" echo "start $(hostname) $(date -u +%FT%TZ) $(sha256sum $X)" # eight day indices drawn from SplitMix64(0x6164762d6d697833) mod 100000 + 20729, fixed here for d in 20730 20745 21057 23311 27406 33333 50000 99999; do for k in 2 3 4 8; do echo "== index day $d k=$k $(date -u +%FT%TZ)" - $X index --day $d --apps $k --threads 88 > "$L/index-$d-k$k.log" 2>&1; grep -E 'chi2=|verdict' "$L/index-$d-k$k.log" + $X index --day $d --apps $k --threads {cores} > "$L/index-$d-k$k.log" 2>&1; grep -E 'chi2=|verdict' "$L/index-$d-k$k.log" done for k in 2 3 4; do echo "== sac day $d k=$k $(date -u +%FT%TZ)" - $X sac --day $d --apps $k --states 2^24 --threads 88 > "$L/sac-$d-k$k.log" 2>&1; grep -E 'holes=|verdict' "$L/sac-$d-k$k.log" + $X sac --day $d --apps $k --states 2^24 --threads {cores} > "$L/sac-$d-k$k.log" 2>&1; grep -E 'holes=|verdict' "$L/sac-$d-k$k.log" done done echo "end $(date -u +%FT%TZ)" diff --git a/tools/attack/adv-mixer-3/queue/10-adv-mixer-3-index-rest.sh b/tools/attack/adv-mixer-3/queue/10-adv-mixer-3-index-rest.sh deleted file mode 100644 index 0ec6f443..00000000 --- a/tools/attack/adv-mixer-3/queue/10-adv-mixer-3-index-rest.sh +++ /dev/null @@ -1,11 +0,0 @@ -#!/usr/bin/env bash -# adv-mixer-3 queue file (owner: adv-mixer-3). The index census rows k = 5..8 of days 20729 and 20733 (their first -# queue files were killed at 18:58 UTC under the one-sweep-per-box rule); every run takes the per-box sweep lock. -set -uo pipefail -X=/srv/builds/_adv-mixer-3/bin/x-lock.sh; L=/srv/builds/_adv-mixer-3/logs; mkdir -p "$L" -echo "start $(hostname) $(date -u +%FT%TZ)" -for d in 20729 20733; do for k in 5 6 7 8; do - echo "== index day $d k=$k $(date -u +%FT%TZ)" - $X index --day $d --apps $k --threads 88 > "$L/index-$d-k$k.log" 2>&1; echo "rc=$?"; grep -E 'chi2=|verdict' "$L/index-$d-k$k.log" -done; done -echo "end $(date -u +%FT%TZ)" diff --git a/tools/attack/adv-mixer-3/queue/16-adv-mixer-3-index-20733-k234.sh b/tools/attack/adv-mixer-3/queue/16-adv-mixer-3-index-20733-k234.sh deleted file mode 100644 index 7ecd670b..00000000 --- a/tools/attack/adv-mixer-3/queue/16-adv-mixer-3-index-20733-k234.sh +++ /dev/null @@ -1,11 +0,0 @@ -#!/usr/bin/env bash -# adv-mixer-3 queue file (owner: adv-mixer-3). The index census rows k = 2, 3, 4 of day 20733 (lost to the kill of -# queue 02 at 18:58 UTC); every run takes the per-box sweep lock. -set -uo pipefail -X=/srv/builds/_adv-mixer-3/bin/x-lock.sh; L=/srv/builds/_adv-mixer-3/logs; mkdir -p "$L" -echo "start $(hostname) $(date -u +%FT%TZ)" -for k in 2 3 4; do - echo "== index day 20733 k=$k $(date -u +%FT%TZ)" - $X index --day 20733 --apps $k --threads 88 > "$L/index-20733-k$k.log" 2>&1; echo "rc=$?"; grep -E 'chi2=|verdict' "$L/index-20733-k$k.log" -done -echo "end $(date -u +%FT%TZ)" diff --git a/tools/attack/adv-mixer-3/queue/17-adv-mixer-3-lease-rest.sh b/tools/attack/adv-mixer-3/queue/17-adv-mixer-3-lease-rest.sh index 620467d8..bb1aaadf 100644 --- a/tools/attack/adv-mixer-3/queue/17-adv-mixer-3-lease-rest.sh +++ b/tools/attack/adv-mixer-3/queue/17-adv-mixer-3-lease-rest.sh @@ -4,19 +4,15 @@ # Runs only when /srv/builds/_bin/lease has the pool subcommand. Adjust LEASE if its syntax differs. set -uo pipefail X=/srv/builds/_adv-mixer-3/bin/adv-mixer-3; X2=$X-v2; L=/srv/builds/_adv-mixer-3/logs; C=/srv/builds/_adv-mixer-3/cnf; S=$HOME/adv-mixer-3-tools/cadical/build/cadical -T=${THREADS:-32} -lease() { /srv/builds/_bin/lease pool "$T" --label "adv-mixer-3 $1" --owner adv-mixer-3 --nice 10 -- "${@:2}"; } -/srv/builds/_bin/lease --help 2>&1 | grep -q "lease pool" || { echo "no lease pool subcommand yet; refusing to start"; exit 3; } -echo "start $(hostname) $(date -u +%FT%TZ) threads=$T" -for k in 5 6 7 8; do echo "== sac day 20729 k=$k $(date -u +%FT%TZ)"; lease "sac 20729 k$k" $X sac --day 20729 --apps $k --states 2^24 --threads $T > "$L/sac-20729-k$k.log" 2>&1; grep -E 'holes=|verdict' "$L/sac-20729-k$k.log"; done -for k in 5 6 7 8; do echo "== sac day 20733 k=$k $(date -u +%FT%TZ)"; lease "sac 20733 k$k" $X sac --day 20733 --apps $k --states 2^24 --threads $T > "$L/sac-20733-k$k.log" 2>&1; grep -E 'holes=|verdict' "$L/sac-20733-k$k.log"; done -for k in 2 3 4 5 6 7 8; do echo "== index day 20733 k=$k $(date -u +%FT%TZ)"; lease "index 20733 k$k" $X index --day 20733 --apps $k --threads $T > "$L/index-20733-k$k.log" 2>&1; grep -E 'chi2=|verdict' "$L/index-20733-k$k.log"; done -for k in 2 3; do echo "== sac day 20729 k=$k 2^27 $(date -u +%FT%TZ)"; lease "sac 20729 k$k n27" $X sac --day 20729 --apps $k --states 2^27 --threads $T > "$L/sac-20729-k$k-n27.log" 2>&1; grep -E 'holes=|verdict' "$L/sac-20729-k$k-n27.log"; done -for k in 2 3; do echo "== sac0 day 20733 k=$k 2^28 $(date -u +%FT%TZ)"; lease "sac0 20733 k$k n28" $X2 sac0 --day 20733 --apps $k --states 2^28 --threads $T > "$L/sac0-20733-k$k-n28.log" 2>&1; grep -E 'holes=|verdict' "$L/sac0-20733-k$k-n28.log"; done -for d in 20729 20733; do for k in 2 3 4; do - [ $d = 20729 ] && [ $k = 1 ] && continue - echo "== cnf day $d k=$k $(date -u +%FT%TZ)"; $X cnf --day $d --apps $k --t0 0x12345678 --out "$C/d$d-k$k.cnf" > "$L/cnf-$d-k$k.log" 2>&1; grep -E 'target|cnf:' "$L/cnf-$d-k$k.log" - lease "cadical $d k$k" /usr/bin/time -f "wall=%e s maxrss=%M KB" timeout 3600 $S -q "$C/d$d-k$k.cnf" > "$L/sat-$d-k$k.log" 2>&1; echo "cadical rc=$? (10 sat, 20 unsat, 124 timeout)"; grep -E '^s |wall=' "$L/sat-$d-k$k.log" - if grep -q '^s SATISFIABLE' "$L/sat-$d-k$k.log"; then TT=$($X model --file "$L/sat-$d-k$k.log" | sed 's/.*t=\(0x[0-9a-f]*\).*/\1/'); echo "model $TT"; $X verify --day $d --apps $k --t $TT; fi -done; done +T=${THREADS:-48} +# the lease hands the command the cores it took: {cores} is the count, so every harness run sizes its threads from it +lease() { /srv/builds/_bin/lease pool "$T" --min 16 --label "adv-mixer-3 $1" --owner adv-mixer-3 -- "${@:2}"; } +lease1() { /srv/builds/_bin/lease pool 1 --min 1 --label "adv-mixer-3 $1" --owner adv-mixer-3 -- "${@:2}"; } +echo "start $(hostname) $(date -u +%FT%TZ) lease pool up to $T cores, min 16" +for k in 5 6 7 8; do echo "== sac day 20729 k=$k $(date -u +%FT%TZ)"; lease "sac 20729 k$k" $X sac --day 20729 --apps $k --states 2^24 --threads {cores} > "$L/sac-20729-k$k.log" 2>&1; grep -E 'holes=|verdict' "$L/sac-20729-k$k.log"; done +for k in 5 6 7 8; do echo "== sac day 20733 k=$k $(date -u +%FT%TZ)"; lease "sac 20733 k$k" $X sac --day 20733 --apps $k --states 2^24 --threads {cores} > "$L/sac-20733-k$k.log" 2>&1; grep -E 'holes=|verdict' "$L/sac-20733-k$k.log"; done +for k in 2 3 4 5 6 7 8; do echo "== index day 20733 k=$k $(date -u +%FT%TZ)"; lease "index 20733 k$k" $X index --day 20733 --apps $k --threads {cores} > "$L/index-20733-k$k.log" 2>&1; grep -E 'chi2=|verdict' "$L/index-20733-k$k.log"; done +for k in 2 3; do echo "== sac day 20729 k=$k 2^27 $(date -u +%FT%TZ)"; lease "sac 20729 k$k n27" $X sac --day 20729 --apps $k --states 2^27 --threads {cores} > "$L/sac-20729-k$k-n27.log" 2>&1; grep -E 'holes=|verdict' "$L/sac-20729-k$k-n27.log"; done +for k in 2 3; do echo "== sac0 day 20733 k=$k 2^28 $(date -u +%FT%TZ)"; lease "sac0 20733 k$k n28" $X2 sac0 --day 20733 --apps $k --states 2^28 --threads {cores} > "$L/sac0-20733-k$k-n28.log" 2>&1; grep -E 'holes=|verdict' "$L/sac0-20733-k$k-n28.log"; done echo "end $(date -u +%FT%TZ)" + diff --git a/tools/attack/adv-mixer-3/queue/18-adv-mixer-3-lease-sat.sh b/tools/attack/adv-mixer-3/queue/18-adv-mixer-3-lease-sat.sh new file mode 100644 index 00000000..ff3e223e --- /dev/null +++ b/tools/attack/adv-mixer-3/queue/18-adv-mixer-3-lease-sat.sh @@ -0,0 +1,18 @@ +#!/usr/bin/env bash +# adv-mixer-3 queue file (owner: adv-mixer-3). The SAT rows (k = 2..4, both days) lost to the 19:20 UTC kill, every run through the build-server +# lane's pool lease (main's rule, 7 October 2026): `lease pool --label --owner adv-mixer-3 -- cmd`. +# Runs only when /srv/builds/_bin/lease has the pool subcommand. Adjust LEASE if its syntax differs. +set -uo pipefail +X=/srv/builds/_adv-mixer-3/bin/adv-mixer-3; X2=$X-v2; L=/srv/builds/_adv-mixer-3/logs; C=/srv/builds/_adv-mixer-3/cnf; S=$HOME/adv-mixer-3-tools/cadical/build/cadical +T=${THREADS:-48} +# the lease hands the command the cores it took: {cores} is the count, so every harness run sizes its threads from it +lease() { /srv/builds/_bin/lease pool "$T" --min 16 --label "adv-mixer-3 $1" --owner adv-mixer-3 -- "${@:2}"; } +lease1() { /srv/builds/_bin/lease pool 1 --min 1 --label "adv-mixer-3 $1" --owner adv-mixer-3 -- "${@:2}"; } +echo "start $(hostname) $(date -u +%FT%TZ) lease pool up to $T cores, min 16" +for d in 20729 20733; do for k in 2 3 4; do + [ $d = 20729 ] && [ $k = 1 ] && continue + echo "== cnf day $d k=$k $(date -u +%FT%TZ)"; $X cnf --day $d --apps $k --t0 0x12345678 --out "$C/d$d-k$k.cnf" > "$L/cnf-$d-k$k.log" 2>&1; grep -E 'target|cnf:' "$L/cnf-$d-k$k.log" + lease1 "cadical $d k$k" /usr/bin/time -f "wall=%e s maxrss=%M KB" timeout 3600 $S -q "$C/d$d-k$k.cnf" > "$L/sat-$d-k$k.log" 2>&1; echo "cadical rc=$? (10 sat, 20 unsat, 124 timeout)"; grep -E '^s |wall=' "$L/sat-$d-k$k.log" + if grep -q '^s SATISFIABLE' "$L/sat-$d-k$k.log"; then TT=$($X model --file "$L/sat-$d-k$k.log" | sed 's/.*t=\(0x[0-9a-f]*\).*/\1/'); echo "model $TT"; $X verify --day $d --apps $k --t $TT; fi +done; done +echo "end $(date -u +%FT%TZ)" diff --git a/tools/attack/adv-mixer-3/x-lock.sh b/tools/attack/adv-mixer-3/x-lock.sh index 766ef18b..3421f9cc 100755 --- a/tools/attack/adv-mixer-3/x-lock.sh +++ b/tools/attack/adv-mixer-3/x-lock.sh @@ -1,6 +1,8 @@ #!/usr/bin/env bash -# adv-mixer-3: run one harness command under the per-box sweep lock (build-server lane rule of 7 October 2026, -# 18:5x UTC: one bounded sweep per box at a time across all lanes, nice 10, cores 8 to 95, up to 88 threads). -# Usage: x-lock.sh [v2] +# adv-mixer-3: run one harness command through the build-server lane's pool lease (main's rule, 7 October 2026, 19:2x UTC: +# no sweep starts on a box except through `lease pool`). Up to 48 free cores of the bounded pool, at least 16; the lease +# pins the command to the cores it took at nice 10 and replaces {cores} in the arguments with the count taken. +# Usage: x-lock.sh [v2]