- 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.
Installs the full Godmode verifier stack — Cryptol 3.5.0, SAW 1.5,
Binsec 0.11.1, angr 9.2.213 + pypcode 3.3.3, TLA+ Tools 2.19,
Sail 0.20.1 + sail-riscv 4d5530b, fiat-crypto 412e8af, GHC 9.6.7,
cabal 3.10.3.0, Coq 9.1.1 — symlinked into toolchain/local/bin via
the new install.sh, with Python deps in toolchain/venv. ADR-0009
codifies the per-tier responsibility (A=algorithmic Cryptol/SAW,
B=ct Binsec/Rel, C=binary-equivalence angr+pcode, D=state-machine
TLA+, E=ISA reference Sail) and the comma-separated @verify path
syntax the dispatcher now consumes. The Tier C-future path (true
SAW-on-RV32 via macaw-riscv + a forked saw-script) is documented;
GHC + cabal are pre-installed against that day.
sha256_init flips from tested to verified — first crypto function
to clear the new bar. Cryptol model proves the FIPS 180-4 §5.3.3
IVs, LE serialisation, and word_to_le_bytes bijection over [32];
SAW driver discharges them via z3; angr proves the RV32IMC binary
writes the 8 IV words LE, zeros length_bits + block_len, leaves the
partial-block buffer + pad untouched, and preserves all 14 callee-
saved registers, returning within a bounded basic-block budget.
End-to-end ./verify sha256_init runs in ~3 s.
Cleanup found while sweeping: state/ files have no verifiable
function so are skipped by parse_spec; @ct accepts an optional
parenthesized rationale (matches existing AES annotations); five
AES @tests fields pointed at non-existent per-function test files
and now point at the combined ones that actually exercise them.
Word-by-word copy from .data's LMA (__data_load_start) to its VMA
(__data_start..__data_end). On qemu-virt LMA == VMA so the loop is
identity; on the C6 it pulls flash → SRAM. Same asm shape, target-
selected behaviour driven entirely by the linker script.
toolchain/qemu-virt.ld: defines __data_load_start = LOADADDR(.data)
so the symbol resolves at link time on either target.
Static disassembly checks: three auipc/addi pairs for the bounds,
matched lw/sw word pair, two increments per iteration, ret, no
callee-saved writes.
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.
Local-only repo for the pure-asm RISC-V port of Reticulum to the
Adafruit ESP32-C6 Feather. Documentation-only initial commit:
foundation for a multi-year, formally-verified, agent-driven build.
- CLAUDE.md: operating instructions and binding workflow
- MASTER_PLAN.md: vision, scope, milestone roadmap, risk register
- FUNCTIONS.md: function registry (single source of truth)
- docs/adr/0001-0007: architecture decisions, all Accepted
- docs/milestones/milestone-1.md: active milestone spec
- toolchain/, verify/, tests/, src/, references/: scaffolded with READMEs
