Docs

Coverage

“Proof” names the Rust test or the live Demo tab that exercises the model. Live tabs replay their proof firmware in the browser; register proofs hold MMIO behavior with no Arduino consumer. “Source” tells you what that firmware is: the real Arduino library, or a bare-metal image written straight against FSP registers.

Proof inventory

Snapshot core core/ra4m1-periph-wasm: 127 tests (37 legacy CPU/system + 90 R4 proofs). Small core core/ra4m1-core: 90 R4 proofs (89 mirror + EK zero-boot). Always run single-threaded — shared globals (SYS, INSTRUCTION_COUNT, UART buffer) flake in parallel.

cargo test --manifest-path core/ra4m1-periph-wasm/Cargo.toml --lib -- --test-threads=1
cargo test --manifest-path core/ra4m1-core/Cargo.toml --lib -- --test-threads=1
cargo build --manifest-path Cargo.toml

R4 proofs (src/ra4m1.rs, both cores)

Boot and clock: ra4m1_boots_from_zero, clock_stub_accepts_boot_writes. GPIO and timers: ra4m1_map_port_output_retained, ra4m1_map_gpt_counts_and_matches, ra4m1_map_agt_counts, ra4m1_map_elc_routes_software_event. Analog and time: ra4m1_map_adc_converts_channel, ra4m1_map_dac_output_retained, ra4m1_map_rtc_ticks_seconds, ra4m1_map_crc_and_doc, ra4m1_map_opamp_follower_and_acmp. Firmware end-to-end: ra4m1_firmware_blinky_via_mmio, ra4m1_arduino_blink_boots, ra4m1_arduino_blink_toggles_led, ra4m1_wire_ok, ra4m1_spi_ok, ra4m1_can_ok, ra4m1_dtc_ok, ra4m1_analogwave_ok, ra4m1_pwm_ok, ra4m1_analogwrite_ok, ra4m1_tone_ok, ra4m1_softserial_ok, ra4m1_matrix_ok, ra4m1_analog_ok, ra4m1_mtx_ok. Buses and storage: ra4m1_map_sci_tx_reaches_console, ra4m1_map_sci_echo_path, ra4m1_map_sci_spi_loopback, ra4m1_map_spi_loopback, ra4m1_map_i2c_eeprom, ra4m1_map_i2c_slave, ra4m1_wire_slave_ok, ra4m1_map_spi_slave, ra4m1_spi_slave_ok, ra4m1_map_sd_card, ra4m1_sd_ok, ra4m1_map_can_loopback, ra4m1_map_can_fifo, ra4m1_can_fifo_ok, ra4m1_map_can_errors, ra4m1_can_error_ok, ra4m1_map_dtc_repeat. USB: ra4m1_map_usb_tx_reaches_capture, ra4m1_usb_enumerates_cdc, ra4m1_usb_serial_hello, ra4m1_usb_cdc_echo, ra4m1_map_ctsu_measures, ra4m1_map_usb_suspend_resume, ra4m1_usb_hid_keyboard, ra4m1_usb_suspend_resume_ok, ra4m1_map_usb_msc_mock. System and misc: ra4m1_map_dmac_mem_to_mem, ra4m1_map_dataflash_program_erase, ra4m1_eeprom_ok, ra4m1_ite_add_imm_preserves_flags, ra4m1_map_icu_pin_irq, ra4m1_attach_interrupt, ra4m1_serial1_echo, ra4m1_map_extra_channels, ra4m1_rtc_firmware, ra4m1_map_rtc_alarm, ra4m1_wdt_refresh, ra4m1_wdt_expire, ra4m1_opamp_firmware, ra4m1_map_ctsu_mutual, ra4m1_ctsu_mutual_ok, ra4m1_map_can1_loopback, ra4m1_can1_ok, ra4m1_map_dac8, ra4m1_dac8_ok, ra4m1_map_tsn, ra4m1_map_slcdc, ra4m1_map_kint, ra4m1_kint_ok, ra4m1_map_ssi, ra4m1_ssi_ok, ra4m1_component_gpio_pins, ra4m1_component_can_frame, ra4m1_component_ssi_bridge, ra4m1_component_spi_exchange, ra4m1_component_i2c_exchange, ra4m1_component_dma_queue, ra4m1_component_sci_wdt_rtc, ra4m1_rtc_alarm_ok, ra4m1_map_can_busoff_recovery, ra4m1_can_busoff_ok, ra4m1_ek_ra4m1_zero_boot_p106_led, ra4m1_map_ssi1, ra4m1_map_gpt_protect_dma.

Known quirks

• Run tests with --test-threads=1: shared SYS, instruction count, and UART buffer flake in parallel.
• rx_inject raises BRDY like hardware; CCPL is a strobe; CFIFO OUT drains are single bytes.
• RIIC: ST auto-sets MST/TRS; TDRE+TXI fire on START; enables fire latched flags; the first RXI read is a dummy; restart-write has no completion event.
• Virtual time runs on instruction count; ADC converts instantly; CAN loopback needs self-test mode; I2C slave jig lives at 0x50; SPI loopback is a test jig (open bus reads 0xFF); DTC transfers complete in the CPU run loop while staged.
• GPT compares are crossing-detected; unprogrammed all-ones compares are bounded by the period so they never false-fire on wrap.
• PORT and PFS are separate instances keyed by an explicit flag; PWM pins follow GPT latches only when PFS PSEL selects a GPT function.
• PCNTR1 word is PDR low half + PODR high half (settled against the FSP disassembly: turnLed tristates with a 16-bit mask, so direction is low). Level readers use the high half; stale levels on tristated rails never decode.
• Arduino-lib matrix on-windows are ~15 instructions wide, so the heart proof reconstructs from a GPIO write-trace jig (same idea as the USB TX capture), not chunk sampling.
• DTC repeat/block length reads CRAL (R_DTC doubles length into CRAL+CRAH, so a programmed 24 reads back 0x1818).
• Sub-word reads return unmasked packs in JS — mask with % 256. Data registers (ICDRR/SPDR) are never polled; a read would eat the firmware's byte.
• D13 is P111 (PORT1 bit 11), not bit 13.

Build and test

Top workspace builds Minima only; WiFi is parked and excluded. demo/pkg/ + demo/fw/ are generated (git-ignored); only index.html, docs.html, about.html, app.js, styles.css, build.sh are tracked.

./demo/build.sh
python3 -m http.server -d demo 8901
cargo build --manifest-path Cargo.toml

Vendored firmware (core/blinky/r4*.bin) is built with arduino-cli 1.6.0 and committed; the Pages workflow rebuilds pkg+fw and publishes demo/.