20 KiB
Attack pass F2: the mixer's round margin
Row F2 of docs/plans/cryptanalysis.md section 4.2 (branch cryptanalysis), fed into
docs/analysis/attack-pass-2026-10.md. Run 7 October 2026, 09:00 to [FILL] UK, by the attack-pass sub-agent F2 on
igneum-build-1 (cores 6-11 and 54-59, nice 10, the measure file held shared in chunks under 30 minutes).
1. Target
Commit 924288d1 (worktree igneum-wt-attack, branch attack-pass). The x8 mixer of igneum-pow/src/memhard.rs,
mixer (lines 300 to 313): one application on 16 words of 32 bits is, per word, (s[i] ^ (RC[i] + rk)) * MUL[i]
with MUL[i] odd, then one ChaCha-shaped double round: four column quarter rounds with rotations ROT[0..3],
four diagonal quarter rounds with ROT[4..7]. ROT, MUL, RC are drawn per day from the 64-bit SplitMix64 seed
K[0] | K[1] << 32 by MixParams::with_shape (lines 237 to 258). Under class v3 and v4 (m = 8) an item is 8
dependent cache reads, each preceded by 8 applications with round keys round_key(r * 8 + j), and 8 more after the
last read: 72 applications per item (derive_items_mask, lines 517 to 550). The chip model prices one application
at 128 hoisted operations and an item at 9,360 (docs/analysis/chip-model-v3.md 5.2).
The days modelled: the genesis day 2026-10-03 (ROT = 20 20 19 4 26 3 3 27, as proto-metal/MEMHARD.md line 82
states; the harness reads the same draw from the code) and two other days, 2026-10-04 (ROT = 28 15 9 26 2 2 22 8) and 2027-03-01 (ROT = 31 16 15 15 2 9 19 4). Their full MUL and RC are in the box files
/srv/builds/igneum-wt-attack/target-attack-f2/params/<day>.real.txt.
Known-failed shape (the plan's row): a differential or linear trail, a rotational-XOR relation, or an algebraic fold that distinguishes or shortcuts more than 2 of the 8 applications between dependent reads. Gate: none beyond 2 of 8.
2. Method
Four searches and two checks, every one on the bit-level definition in memhard.rs (the harness calls
igneum_pow::memhard::mixer itself; the SAT models consume one op list whose value evaluator is checked against
the Rust output on 64 applications per day and variant, 9 files, all matching).
| Piece | What it is | Exact or model |
|---|---|---|
| Differential, MSB family | XOR differences; at every multiply each word's difference is 0 or 0x80000000. These are the only word transitions through an odd multiply with probability 1 ((x ^ 2^31) * c = (x * c) ^ 2^31; any other nonzero difference passes with probability at most 1/2, since its lowest active bit below the MSB leaves a carry to chance). Modular addition by Lipmaa-Moriai (exact per adder), XOR and rotation linear |
exact family, trail probabilities exact per operation |
| Differential, general | The same ARX model with every word difference allowed through the multiply: XOR difference to modular difference (each set bit below the MSB is a sign choice, 2^-1 each, exact), times MUL (exact, a circuit on the difference variables), modular back to XOR (a carry chain, one bit per position where the difference bit and the carry differ, exact), the two conversions taken as independent |
Markov trail model; its per-word cost sits 1 to 2 bits above the sampled best transition (section 4.1), so it is a trail model, slightly pessimistic for the attacker |
| Linear, low-bit family | Masks; at every multiply the output mask lies in bits 0 and 1, the only F2-linear output bits of an odd multiply ((cx)_0 = x_0, (cx)_1 = x_1 ^ (c_1 & x_0)). Modular addition by the exact carry-mask automaton (per bit a carry-mask bit; checked against brute force at n = 8 on 500 mask triples, max error 0) |
exact family |
| Linear, general | The same with the multiply as its shift-and-add decomposition (one adder per set bit of MUL, the low known-zero bits of a shifted copy transparent), each adder under the automaton |
trail model; over-optimistic for the attacker (section 4.3) |
| Rotational-XOR | Measured on the real code: for every rotation r in 1..31 and k = 1..4, the per-bit bias of rot_r(M^k(x)) ^ M^k(rot_r(x)) over 2^20 states, the largest |
z |
| The fold | The identities a chip would need to pay less than k x 128 for k applications, each tested on 2^20 random inputs, plus the algebraic argument (section 4.5) | measurement and argument |
Search: for each (model, day, k = 1..4) the weight bound W is probed upward (SAT means a trail of weight at most W
exists, UNSAT means none does in the model), then narrowed to the minimum. A k-application trail restricted to one
application is a valid 1-application trail, so every application is held to the proven k = 1 minimum of the same
model (the Matsui floor in the tables). Solver CaDiCaL 1.9.5 through python-sat 1.9. Every trail found of
measurable weight is measured on the real code before it counts: per application and as a chain, 2^20 to 2^28
samples (attack-f2 verify-diff / verify-lin), with the multiply-layer word transitions counted exactly over all
2^32 inputs (verify-mults). A trail that does not hold is blocked and the solver asked again at the same bound.
Linear trails whose correlation cancels inside one adder's hull are caught first by the exact signed sum over the
adder's carry masks.
What "reaches k applications" means here, two readings: (a) the shortcut reading, the one with a cost consequence: a relation of probability 1 (weight 0) over k applications, which a chip could use to skip work; (b) the distinguisher reading: a trail of weight under 64 over k applications, the usual practical line. For the gate both are reported.
3. Harness
| Item | Path |
|---|---|
| Crate (ground truth: parameters, vectors, verification, RX, fold) | tools/attack/f2-mixer/ (Cargo.toml, src/main.rs), igneum-pow by path, own [workspace] |
| SAT models and the search | tools/attack/f2-mixer/model.py (selftest, search, show) |
| Box queue runner, tables | tools/attack/f2-mixer/run_jobs.sh, tools/attack/f2-mixer/summarise.py |
| Build line (from the crate directory) | IGNEUM_AGENT=attack-f2 bash /Users/joshm/Projects/igneum/tools/build-remote.sh --artefacts "target/release/attack-f2" --out <scratch> -- build --release; binary on the box /srv/builds/igneum-wt-attack/tools/attack/f2-mixer/target/release/attack-f2 (ELF x86-64, sha256 150337ec..., the third build; 12 s incremental) |
| Box scratch (states, trails, logs, venv) | /srv/builds/igneum-wt-attack/target-attack-f2/ (state/, logs/, params/, vectors/, venv/). The brief's path attack-f2/ was wiped within ten minutes by another lane's worktree-root rsync (--delete spares only target-*), so the scratch moved under a target- name, as F1 and F6 did |
| Run lines | venv/bin/python3 model.py selftest --vectors vectors --params-dir params; bash run_jobs.sh jobs.txt 11 (each job `model.py search --kind diff |
| Logs | logs/<model>-<day>-<variant>-k<k>.log per search, logs/rx.<day>.<variant>.log, logs/rx-word.<day>.<variant>.log, logs/fold.<day>.log, logs/summary.md (the tables below), logs/verify*.log |
4. Results
4.1 The harness fires (known pass, known fail)
| Case | Expected | Got | Log |
|---|---|---|---|
Selftest: evaluator against attack-f2 vectors, 3 days x 3 variants, 4 applications x 16 states each |
all match | 9 of 9 files, 64 of 64 applications each | selftest output, logs/selftest.log |
| Selftest: linear add automaton against brute force, n = 8 | exact | 300 random triples and 200 shifted-copy triples, max error 0.00e+00 | same |
| Selftest: Lipmaa-Moriai against brute force, n = 8; both SAT encodings against their rules at n = 32 | exact | max error 0; 0 mismatches of 40 and 40 | same |
| Selftest: the multiply model's word cost against the sampled best transition (word 3, genesis day) | MSB exact; others within a few bits | MSB: weight 0, measured 2^-0 (exact); bit 30: model 2, sampled best 2^-1.00; bits 31+5: model 8, sampled best 2^-6.03; bit 0: model 10, sampled best 2^-8.97 | same |
| Known pass, 0 applications | the identity trail, weight 0 | trivial (input = output, no weights); not run as a job | |
Known fail, rot0 (every rotation 0), differential, k = 1, 2, 4 |
a weight-0 trail (MSB-only differences stay MSB-only when nothing rotates) | weight 0 found at k = 1, 2, 4 (both families); measured probability 1 on the real code (verified_chain -0.0) |
state/diff-msb-2026-10-03-rot0-k{1,2,4}.json, state/diff-general-2026-10-03-rot0-k{1,2}.json |
Known fail, rot0, linear, k = 1, 2, 4 |
a weight-0 trail (LSB masks) | weight 0 at k = 1, 2, 4; measured correlation 1 per application and as a chain | state/lin-low2-2026-10-03-rot0-k{1,2,4}.json, state/lin-general-2026-10-03-rot0-k{1,2}.json |
Known fail, nomul (MUL 1, RC 0, rk 0: the bare double round), rotational-XOR, k = 1 |
a large per-bit bias | max | z |
Known fail, rot0, rotational-XOR |
bias | max | z |
Known fail, nomul, differential k = 1 |
the bare double round's best trail, below the real mixer's | weight 7 found (model), measured 2^-5.0 on the real code | state/diff-general-2026-10-03-nomul-k1.json |
4.2 Differential trails
| Model | Day | Variant | k | Best trail weight found | No trail at or below (model) | Closed | Per-application floor | Verified on the real code (chain; per application) | Solver s |
|---|---|---|---|---|---|---|---|---|---|
| diff/general | 2026-10-03 | real | 1 | 12 | 11 | yes | 0 | 12.011; [11.939] | 186 |
| diff/general | 2026-10-03 | real | 2 | none | 24 | no (timebox) | 12 | 1,739 | |
| diff/general | 2026-10-04 | real | 1 | 10 | 9 | yes | 0 | 10.001; [9.999] | 321 |
| diff/general | 2026-10-04 | real | 2 | none | 20 | no (timebox) | 10 | 663 | |
| diff/general | 2027-03-01 | real | 1 | 12 | 11 | yes | 0 | 12.057; [11.907] | 175 |
| diff/msb | 2026-10-03 | real | 1 | 12 | 11 | yes | 0 | 12.206; [11.972] | 4 |
| diff/msb | 2026-10-03 | real | 2, 3, 4 | none | 512 (the family dies) | yes | 12 | 26, 33, 22 | |
| diff/msb | 2026-10-04 | real | 1 | 10 | 9 | yes | 0 | 10.001; [10.001] | 309 |
| diff/msb | 2026-10-04 | real | 2, 3, 4 | none | 512 | yes | 10 | 20, 33, 44 | |
| diff/msb | 2027-03-01 | real | 1 | 12 | 11 | yes | 0 | 12.057; [11.907] | 3 |
| diff/msb | 2027-03-01 | real | 2, 3, 4 | none | 512 | yes | 12 | 10, 15, 21 | |
| diff/general | 2026-10-03 | nomul (known fail) | 1 | 7 | 6 | yes | 0 | 5.002; [5.003] | 38 |
| diff/general | 2026-10-03 | nomul | 2 | none | 20 | no | 7 | 1,309 | |
| diff/general, diff/msb | 2026-10-03 | rot0 (known fail) | 1, 2, 4 | 0 | yes | 0 | probability 1 | under 1 |
The general model's k = 3 and k = 4 jobs (closed 14:3x UTC, every job at its 7,200 s cap, logs/summary.md):
| Model | Day | k | Best trail found | No trail at or below (model) | Per-application floor | Solver s |
|---|---|---|---|---|---|---|
| diff/general | 2026-10-03 | 3 | none | 35 | 12 | 7,201 (cap) |
| diff/general | 2026-10-03 | 4 | none | 47 | 12 | 7,359 (cap) |
| diff/general | 2026-10-04 | 3 | none | 29 | 10 | 7,350 (cap) |
| diff/general | 2026-10-04 | 4 | none | 39 | 10 | 7,279 (cap) |
| diff/general | 2027-03-01 | 3 | none | 35 | 12 | 7,321 (cap) |
| diff/general | 2027-03-01 | 4 | none | 47 | 12 | 7,284 (cap) |
| lin/general | 2026-10-03 | 3 | none | 24 | 1 | 7,953 (cap) |
| lin/general | 2026-10-03 | 4 | none | 24 | 1 | 7,352 (cap) |
| lin/general | 2026-10-04 | 3 | none | 28 | 1 | 7,373 (cap) |
| lin/general | 2026-10-04 | 4 | none | 24 | 1 | 7,393 (cap) |
| lin/general | 2027-03-01 | 3 | none | 24 | 1 | 7,402 (cap) |
No trail of weight under 32 at three applications (the finding line): the bound reached is 29 to 35 at three and 39 to 47 at four for differentials, 24 to 28 at three and 24 at four for linear masks, all solver-capped, so these are effort bounds, not proofs; they grow with k as the per-application floors predict.
4.3 Linear trails
| Model | Day | Variant | k | Best trail weight found (correlation 2^-w) | No trail at or below | Closed | Verified (chain; per application) | Solver s |
|---|---|---|---|---|---|---|---|---|
| lin/general | 2026-10-03 | real | 1 | 1 | 0 | yes | 0.996; [0.997] | 5 |
| lin/general | 2026-10-03 | real | 2 | none | 20 | no (timebox) | 1,019 | |
| lin/general | 2026-10-04 | real | 1 | 1 | 0 | yes | 0.995; [0.999] | 5 |
| lin/general | 2026-10-04 | real | 2 | none | 24 | no (timebox) | 1,669 | |
| lin/general | 2027-03-01 | real | 1 | 1 | 0 | yes | 1.003; [0.996] | 5 |
| lin/general | 2027-03-01 | real | 2 | none | 20 | no (timebox) | 1,224 | |
| lin/low2 | 2026-10-03, 2026-10-04, 2027-03-01 | real | 1 | 1 | 0 | yes | 0.995 to 1.003 | 4 to 5 |
| lin/low2 | 2027-03-01 | real | 2, 3, 4 | none | 512 (the family dies) | yes | 12, 18, 27 | |
| lin/general | 2026-10-03 | nomul (known fail) | 1 | 1 | 0 | yes | 0.999; [1.003] | 4 |
| lin/general, lin/low2 | 2026-10-03 | rot0 (known fail) | 1, 2, 4 | 0 | yes | correlation 1 | 5 to 10 |
One application carries a weight-1 linear trail (the LSB mask through the prologue and one add, correlation 1/2), the structural residue of 4.5; at two applications no trail at or below weight 20 to 24 exists in the general model within the timebox, and the LSB family dies (no trail at or below 512) from k = 2.
4.4 Rotational-XOR
Per k and day, the largest |z| over all 31 rotations and 512 bits at 2^20 states (15,872 bit tests per k; the noise ceiling of that many tests is about 4.3), and the count of exact rotational pairs.
| Day | k = 1 | k = 2 | k = 3 | k = 4 | Exact pairs | Log |
|---|---|---|---|---|---|---|
| 2026-10-03 | 4.22 (r 19) | 4.29 (r 30) | 4.22 (r 3) | 4.62 (r 27) | 0 | logs/rx.2026-10-03.real.log |
| 2026-10-04 | 4.35 (r 17) | 4.00 (r 19) | 4.24 (r 25) | 4.49 (r 28) | 0 | logs/rx.2026-10-04.real.log |
| 2027-03-01 | 3.96 (r 7) | 4.07 (r 2) | 4.04 (r 28) | 4.17 (r 19) | 0 | logs/rx.2027-03-01.real.log |
2026-10-03, bare double round (nomul) |
134.24 (r 31) | 4.37 | 0 | logs/rx.2026-10-03.nomul.log |
The word-level prologue (x ^ C) * MUL: over 2^20 inputs the most frequent value of rot_r(g(x)) ^ g(rot_r(x))
occurs at most 3 times for every word and every r on all three days (logs/rx-word.<day>.real.log, the
rxw_worst lines), against 2^20 of 2^20 without the multiply. The odd multiply by a random constant is not
rotational to any measurable degree, and one application already shows no per-bit bias. Rotational-XOR does not
reach 1 application.
4.5 The fold of the multiply layer
One application is D o P_rk, with P_rk(s)_i = (s_i ^ (RC_i + rk)) * MUL_i and D the double round (fixed per
day). Multiplication by an odd constant distributes over modular addition and over nothing else in D (XOR,
rotation); the XOR with a constant commutes with XOR and rotation and with nothing else (addition, multiply). A fold
across applications would need one of the identities below. Each was tested on 2^20 random inputs on every day
(logs/fold.<day>.log):
| Identity a chip would need | Holds on | Meaning |
|---|---|---|
(xa ^ Ca) * ma + (xb ^ Cb) * mb = ((xa ^ Ca) + (xb ^ Cb)) * ma for the four column pairs (0,4), (1,5), (2,6), (3,7) |
0 of 1,048,576 for every pair on every day (MUL distinct in every pair) |
the multiply does not fold into the first add of a quarter round; it would if a column pair drew the same MUL (probability 2^-31 per pair per day, the weak-day class of F4) |
(x ^ C) * m = (x * m) ^ (C * m), or = (x * m) ^ C' for any single C' |
0 of 1,048,576; the best single C' agrees on 33 of 1,048,576 (2^-15) |
the constant cannot be moved past the multiply, so application j + 1's prologue cannot share application j's multiply |
| an XOR constant on one word commuting with the bare double round (so the next prologue's constant could be folded back) | 0 of 65,536 for every word | every word's value feeds an add inside the double round |
| the MSB passing the prologue and the add for free; the LSB passing the prologue | 1,048,576 of 1,048,576 each | the structural residue: the only free passages, both moved by the rotations (the family deaths in 4.2 and 4.3) |
So k applications cost k times one application, 128 hoisted operations each (16 multiplies, 32 adds, 32 XORs, 32
rotations with the constants hoisted); chip-model-v3.md 5.2's 9,360 per item stands. The trail weights of 4.2
and 4.3 growing with k is the quantitative side of the same fact: a composition that collapsed to one application's
shape would keep one application's trail weights.
5. Gate and verdict
Gate (plan 4.2 F2, 1.4 (1)): no distinguisher or shortcut beyond 2 of the 8 applications between dependent reads, after the stated search.
| Line of attack | Reach | Verdict |
|---|---|---|
| Differential, general model (Markov on the multiply, exact add rule, SAT) | one application: best trail weight 10 to 12 on three days, verified on the real code; two applications: no trail at or below weight 20 to 24 within 7,200 s per job (not closed); the MSB family dies at two applications on every day | nothing reaches 2 applications below 2^-20 |
| Linear, general model (piling-up, SAT) | one application: weight 1 (the LSB residue); two applications: no trail at or below 20 to 24 within the timebox; the LSB family dies at two | nothing reaches 2 applications below 2^-20 |
| Rotational-XOR | no per-bit bias at one application (max abs z 4.0 to 4.6 at 2^20 states, noise ceiling 4.3); 0 exact pairs; the multiply prologue is rotational on at most 3 of 2^20 inputs; the bare double round fires at 134 | does not reach 1 application |
| Algebraic fold of the multiply layer | every identity a fold needs holds on 0 of 2^20 inputs on every day; k applications cost k | no shortcut |
Verdict: PASS with the effort bound stated: about 60 solver jobs, 2 to 29 minutes each, on three day keys; the reduced-round margin reached is one application fully characterised (weights 10 to 12 differential, 1 linear) and two applications with no trail under weight 20 to 24, three with none under 29 to 35 (differential) and 24 to 28 (linear), four with none under 39 to 47 and 24, against 8 applications between reads, so the margin between what the search reaches and what the construction uses is at least 4 applications at the solver's cap. What this does not do is in section 7; the lower bound is the paid question.
6. Consequences per tier
No shortcut, so no tier moves: a home card, a rig and a pool pay the 72 applications per item the verifier pays;
a chip with a fixed datapath pays them too (the fold test), which is what chip-model-v3.md 5.2's 9,360 ops per
item assumes. mixer_mult stays 8; the verifier measurement of F6 stands unchanged.
7. What this does not do
- It does not bound the mixer from below: the general models are trail models (Markov for the multiply's differential, piling-up for the linear), and the family models are exact only inside their families. The firm's job (funding.md B5 rank 1) is the effort-bounded version of the same search with their tools.
- Three days, not a census: the ROT, MUL, RC classes over 2^24 days are F4's row. One cheap addition for F4 from
this harness: the MSB-family death at k = 2 (
model.py search --kind diff --family msb --apps 2) runs in seconds per day, and a day where it does not die is a weak day of the kind the gate is about. - Differential and linear only, as the row says: no boomerang, no integral or cube property, no related-key (the round keys are public constants).