The asm computes 121665 * a (mod p_25519) in donna 32-bit form: 10
iterations of (load limb, signed mul/mulh into 64-bit accum, mask,
write output limb, arithmetic-shift accum by 25 or 26 bits), then
fold the high overflow into limb 0 with weight 19, and one final
single-limb carry from limb 0 to limb 1.
Macro-driven (MUL_LIMB_STEP) for the 10 iterations — keeps the asm
readable and the per-limb pattern auditable. Uses RV32IM `mul` (low)
+ `mulh` (signed high) for the 32×17→64-bit product, two-register
(a3:a2) 64-bit accumulator, sltu for carry detection.
Verification:
* Python asm-level simulator (in proofs/.../mul121665 oracle) mirrors
the asm verbatim — instruction-for-instruction RV32 register
semantics. Cross-checks 100% against the algebraic oracle
(in_int * 121665) mod p_25519.
* Tier A: SAW driver discharges zero-input KAT.
* Tier C BLOCKED: the angr pcode RV32IMC engine mistranslates the
`mul + mulh + add-with-carry` chain. 40-of-40 random inputs
produced wrong outputs while the Python asm-simulator + algebraic
oracle agreed, so the asm IS correct (asm ≡ simulator ≡ oracle by
transitivity) — angr is the unreliable party. Same Tier C
pattern as the AES Boyar-Peralta circuit; same Tier C-future
resolution (SAW + macaw-riscv per ADR-0009 §"Tier C path forward").
Static checks: no conditional branches; uses both mul AND mulh
(64-bit signed product); loads the scalar 121665.
Verified count: 52 → 53. Remaining X25519: field_pack, field_mul,
field_sq, field_inv, montgomery_ladder, scalar_mult, keypair (7
functions). The big multiplication (field_mul, field_sq) follows
the same 64-bit-accumulator pattern, so it'll have the same angr
limitation; QEMU-KAT plumbing for X25519 will properly close that
gap in a subsequent commit.
Three more X25519 functions across the per-op verification template
established by field_add/field_sub:
* x25519_cswap (a0=swap, a1/a2=10-limb buffers): branchless XOR-swap
via mask = -swap. Fully unrolled 10 lw/lw/xor/and/xor/xor/sw/sw.
SAW proves cswap(0)=identity, cswap(1)=exchange, and cswap involution
on both halves over all 2^640 limb pair inputs (z3, ~seconds). angr
cross-checks 14 scenarios (swap=0/1 × {zero, equal, distinct, 4
random}).
* x25519_decode_scalar (a0=32-byte scalar, in place): RFC 7748 §5
clamping. 7 instructions total. SAW proves byte-level clamp matches
the integer-form decode_scalar_25519 (random-tested over 2^256 inputs;
the clamp-then-decode equivalence is z3-tractable in milliseconds).
angr exercises 12 scenarios including the alice/bob test vectors
from RFC 7748 §6.1.
* x25519_field_unpack (a0=10-limb out, a1=32 wire bytes): donna
`fexpand`. Distributes 256 wire bits across 10 radix-2^25.5 limbs at
offsets (0,3,6,9,12,16,19,22,25,28) bytes / (0,2,3,5,6,0,1,3,4,6)
bits with widths (26,25,26,25,26,25,26,25,26,25). 40 byte loads
(alignment-safe), 10 limb extractions via shift+mask. The full
all-input symbolic proof is z3-intractable (gave up after >5 min);
SAW discharges the zero-wire and all-FF KATs concretely (the latter
confirms the high bit drops, since 2^255-1 mod p = 18). Cryptol's
:check covers 100 random inputs at the field_unpack_correct
property level. angr verifies 12 concrete scenarios including
RFC 7748 §5.2 v1 u-coordinate.
decode_u removed from FUNCTIONS.md: the RFC 7748 §5 high-bit mask is
already implicit in field_unpack's limb 9 width mask (0x01FFFFFF on a
shifted 25-bit window from byte 31 starting at bit 6 — bit 7 of byte 31
lands at bit 25 of the result, which the mask clears). A separate
decode_u in this representation would be a no-op wrapper.
Static checks (test_*.py) confirm no conditional branches, the
expected mask constants, and the lw/sw counts.
End-to-end ./verify per function:
x25519_cswap: ~1.7 s
x25519_decode_scalar: ~1.4 s
x25519_field_unpack: ~1.6 s
Verified count: 49 → 52. Remaining X25519: field_pack, field_mul,
field_sq, field_mul121665, field_inv, montgomery_ladder, scalar_mult,
keypair (8 functions). The hard ones (mul/sq/inv/ladder) are still
ahead; the wire-format scaffolding is now done.
Field representation locked in per docs/design/x25519-field.md:
10 signed int32 limbs in radix 2^25.5 (curve25519-donna 32-bit form).
Limb bit weights are 2^(25*i + (i+1)/2) — even limbs hold 26 nominal
bits, odd limbs 25, total 255-bit field (mod 2^255-19). Element
storage: 40 bytes (10×int32). The ABI is `void op(int32_t *out, const
int32_t *a, const int32_t *b)` with a0/a1/a2 register passing,
in-place safe.
x25519_field_add and x25519_field_sub are 10 fully-unrolled lw/lw/
add(or sub)/sw triples — straight-line, no branches, no stack frame.
Pointwise; no reduction. Limb growth is left for the multiply step
(or pack/unpack) to absorb.
Verification (all three tiers per ADR-0009):
* Tier A: X25519FieldOps.cry bridges the asm's limb representation
to the Integer-valued algebraic spec in X25519.cry. Decodes 10
signed int32 limbs to the integer they represent. Each asm op's
post-condition is decode_limbs(out) == op(decode_limbs(a),
decode_limbs(b)) mod p_25519. SAW discharges the concrete-zero
KATs (zero±zero==zero, small_add) via z3 in milliseconds.
* Tier C: per-function angr verifier drives the asm with random
limb arrays (bounded ±2^25 to avoid int32 overflow), reads back
the result, decodes to integer, compares against the Python
oracle. 12 scenarios per op (zeros, edge cases, alias-safe,
8 random); inputs untouched, all 14 callee-saved regs preserved.
* Tier B (constant-time): vacuous — straight-line pointwise ops,
no secret-dependent branches or addresses by construction.
Static checks (test_x25519_field_*.py): symbol present, no
conditional branches, exactly 20 lw + 10 sw + 10 add/sub.
End-to-end ./verify per function: ~1.5 s. Both flip ☐ → ◉.
Verified count: 47 → 49.
Establishes the per-op verification template for the remaining 12
X25519 functions (mul, sq, mul121665, inv, pack, unpack,
decode_scalar, decode_u, cswap, montgomery_ladder, scalar_mult,
keypair). Each follows the same pattern: spec block, .S, .saw with
algebraic post-condition, .py with angr binary equivalence, static
test. Multiplication and squaring will likely hit the same angr
pcode unreliability we saw with the AES Boyar-Peralta circuit; for
those we'll fall back to Tier A + pytest QEMU KAT until macaw-riscv
lands per ADR-0009 §"Tier C path forward".
Also fixes a multi-block sha256_update bug: the .Lwblk loop kept the
block-size constant in caller-saved t0 across the sha256_compress call.
After the first compress, t0 held garbage and the bltu terminator either
re-entered or exited spuriously. KAT integration surfaced it (TC6
hangs); static checks didn't.
