- TARGET_C6 register block + linker script (load into 0x4086c410, the same
upper-half HP_SRAM bootloader region esp-idf uses; loading to 0x40800000
collides with ROM flash-loader scratch and silently aborts the segment
copy with "Calculated 0xef stored 0xff").
- USB-Serial/JTAG as the early-bring-up uart_* backend (ADR-0010 refines
ADR-0004; the C6's mask ROM provides the CDC-ACM stack so we just push
bytes to a 1-byte FIFO with WR_DONE flush).
- TARGET_C6 paths in clock_init / clock_now_ticks / clock_delay_us /
uart_init / uart_tx_byte / uart_rx_byte / uart_rx_available.
- clock_init disables TG0 / LP / Super watchdogs (key 0x50D83AA1) so the
polling main loop survives.
- Makefile image/flash/monitor targets default DIO @ 40 MHz (QIO @ 80 MHz
hangs on the Feather's factory flash configuration).
- Hardware demo passed end-to-end: KISS-framed Reticulum packet over USB-C
produces kiss.rx_frame + packet.parsed; short payload produces rejected;
SHA-256 KAT trigger emits FIPS 180-4 §B.1 vector ba7816bf...20015ad.
- qemu-virt suite still 124/124 green.
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.
Walks every src/**/*.S, parses each function's @stack annotation and
its call/tail/jal outgoing edges, builds a call graph rooted at
_reset, and reports the deepest cumulative stack along any reachable
path. Fails the build if the deepest path exceeds STACK_SIZE from
src/include/config.S.
Cycles are flagged as recursion (recursion is forbidden today; allowing
it needs a separate ADR). Functions reachable from _reset whose .S is
absent are reported as warnings.
Wired into 'make ci': registry → stack → test. Current binary:
deepest path _reset → _main → log_event → log_hex = 48 bytes,
well under STACK_SIZE = 16384.
OQ-4 resolved in docs/open-questions.md.
154 tests, all green.
Lays the verifier-loop infrastructure that every subsequent function
goes through. Every change is wired to make ci.
Tooling (tools/):
- parse_spec.py validates the ADR-0007 spec block on every .S file
(required fields, @function ↔ basename, @module ↔ directory, @adrs ↔
Accepted ADRs, @verify/@tests path existence, unbounded-cycles ↔
not-required-ct).
- check_registry.py cross-checks FUNCTIONS.md against src/ — every
registered global has a source file (and vice versa), every
depends-on resolves, status disagreements raise warnings.
Test harness (tests/harness/):
- log_parser.py parses the ADR-0004 log line format with selectors.
- target.py: Target ABC + NullTarget loopback + Emu/Hw skeletons
that detect tool availability and raise TargetUnavailable until
wired (deferred until there's a binary to drive end-to-end).
- oracle.py: pure-Python KISS encode/decode reference + RNS.Packet
shim for differential testing.
- verify.py + verify_cli.py + ./verify wrapper: the dispatcher.
Runs spec-validate, pytest, and the @verify-pointed tool
(kat-only, .saw, .tla, .py); reports pass/fail/skip/not-implemented.
Build chain (toolchain/):
- qemu-virt.ld: DRAM @ 0x80000000, __global_pointer$ anchored,
16 KiB stack reserved at top. C6 linker script lands with hardware
bring-up.
- versions.lock pinned to riscv64-elf-binutils 2.46 + qemu 11.0 +
Python 3.12 + RNS 1.2 (per ADR-0008).
Includes (src/include/):
- psabi.S with the RISC-V ABI register aliases (ADR-0001).
- config.S with capacity constants (stack, ring buffers, KISS frame).
- regs.S with the qemu-virt NS16550A UART addresses; C6 stub with
.error until populated.
ADR-0008: bundles four decisions surfaced during bring-up:
1. Rename verify/ → proofs/ to free ./verify for the dispatcher.
2. Adopt vanilla riscv64-elf-binutils (homebrew) over the Espressif
crosstool-NG fork; -march=rv32imac -mabi=ilp32.
3. Log timestamps are 8 hex digits emitted by log_hex(width=8).
4. Spec-block prefix is # (RISC-V GAS line comment), not ;;.
ADR-0006/0007 status lines flagged as partially superseded; ADR-0004
flagged as refined. ADR index updated. parse_spec accepts both ;; and
# prefixes during the transition. open-questions.md tracks OQ-1..OQ-3
as resolved by ADR-0008 and OQ-4 (check_stack.py) deferred.
make ci: 51 tests, all green.
