mirror of
https://github.com/ratspeak/C6-Reticulum-ASM
synced 2026-08-12 18:07:18 -04:00
cda7dae845
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".
|
||
|---|---|---|
| .. | ||
| x25519-field.md | ||