diff --git a/README.md b/README.md index bef7471..7278d99 100644 --- a/README.md +++ b/README.md @@ -74,8 +74,12 @@ synth compile examples/wat/simple_add.wat --cortex-m -o firmware.elf # Disassemble the result synth disasm firmware.elf +``` + +To use Z3 translation validation, rebuild with the `verify` feature (requires Z3 on your system): -# Formally verify the translation +```bash +cargo build --release -p synth-cli --features verify synth verify examples/wat/simple_add.wat firmware.elf ``` diff --git a/artifacts/cross-compilation.yaml b/artifacts/cross-compilation.yaml index 079b784..6c8fab9 100644 --- a/artifacts/cross-compilation.yaml +++ b/artifacts/cross-compilation.yaml @@ -35,8 +35,10 @@ artifacts: tags: [cross-compilation, kiln-builtins, stub, bare-metal, phase-1] links: - type: derives-from + target: BR-003 + - type: refines target: CC-004 - - type: derives-from + - type: refines target: SL-003 - type: refines target: KB-001 @@ -68,6 +70,8 @@ artifacts: tags: [cross-compilation, bazel, hermetic, kiln-builtins] links: - type: derives-from + target: BR-003 + - type: refines target: XC-001 - type: refines target: CC-005 @@ -96,6 +100,8 @@ artifacts: tags: [cross-compilation, linker, detection, cli] links: - type: derives-from + target: BR-004 + - type: refines target: SL-001 - type: refines target: CC-005 @@ -127,8 +133,10 @@ artifacts: tags: [cross-compilation, cli, pipeline, single-command] links: - type: derives-from + target: BR-004 + - type: refines target: CC-007 - - type: derives-from + - type: refines target: SL-TR-002 - type: refines target: TR-003 @@ -157,10 +165,12 @@ artifacts: tags: [cross-compilation, linker-script, board-profile] links: - type: derives-from + target: BR-003 + - type: refines target: SL-002 - - type: derives-from + - type: refines target: TP-002 - - type: derives-from + - type: refines target: TP-003 - type: refines target: SL-TR-001 @@ -193,6 +203,8 @@ artifacts: tags: [cross-compilation, testing, renode, ci, phase-1] links: - type: derives-from + target: BR-001 + - type: refines target: CC-006 - type: refines target: E2E-VER-001 @@ -220,8 +232,10 @@ artifacts: tags: [cross-compilation, testing, zephyr, qemu, phase-2] links: - type: derives-from + target: BR-003 + - type: refines target: ZI-001 - - type: derives-from + - type: refines target: ZI-005 - type: refines target: VER-005 @@ -246,8 +260,10 @@ artifacts: tags: [cross-compilation, testing, hardware, stm32, phase-3] links: - type: derives-from + target: BR-003 + - type: refines target: TP-002 - - type: derives-from + - type: refines target: ZI-006 - type: refines target: VER-005 @@ -272,8 +288,10 @@ artifacts: tags: [cross-compilation, testing, hardware, nrf52840, phase-3] links: - type: derives-from + target: BR-003 + - type: refines target: TP-003 - - type: derives-from + - type: refines target: ZI-006 - type: refines target: VER-005 @@ -334,10 +352,10 @@ artifacts: status: planned tags: [cross-compilation, weak-symbol, memory-base, bare-metal] links: - - type: derives-from - target: KB-TR-005 - type: derives-from target: SL-003 + - type: refines + target: KB-TR-005 fields: req-type: functional priority: must diff --git a/artifacts/gale-integration.yaml b/artifacts/gale-integration.yaml index 84bb8c6..9706eb6 100644 --- a/artifacts/gale-integration.yaml +++ b/artifacts/gale-integration.yaml @@ -34,12 +34,12 @@ artifacts: status: draft tags: [gale, zephyr, co-deployment, integration] links: - - type: derives-from - target: ZI-001 - type: derives-from target: BR-001 - type: derives-from target: BR-003 + - type: refines + target: ZI-001 - type: traces-to target: gale:SYSREQ-SEM-001 - type: traces-to @@ -69,10 +69,12 @@ artifacts: tags: [gale, target-triple, compatibility, cortex-m] links: - type: derives-from + target: BR-003 + - type: refines target: TP-001 - - type: derives-from + - type: refines target: TP-004 - - type: derives-from + - type: refines target: TP-005 - type: traces-to target: gale:STKH-001 @@ -104,9 +106,9 @@ artifacts: links: - type: derives-from target: BR-001 - - type: derives-from + - type: refines target: FR-008 - - type: derives-from + - type: refines target: ZI-003 - type: traces-to target: CM-005 @@ -140,8 +142,10 @@ artifacts: tags: [gale, wit, component-model, kernel-objects, phase-2] links: - type: derives-from + target: BR-003 + - type: refines target: CM-002 - - type: derives-from + - type: refines target: FR-001 - type: traces-to target: gale:SWREQ-KILN-001 @@ -174,7 +178,7 @@ artifacts: links: - type: derives-from target: BR-001 - - type: derives-from + - type: refines target: FR-006 - type: traces-to target: gale:SYSREQ-KILN-002 @@ -212,9 +216,9 @@ artifacts: links: - type: derives-from target: GI-004 - - type: derives-from + - type: refines target: KB-TR-001 - - type: derives-from + - type: refines target: KB-TR-002 fields: req-type: functional diff --git a/artifacts/loom-integration.yaml b/artifacts/loom-integration.yaml index b50f3f5..345af98 100644 --- a/artifacts/loom-integration.yaml +++ b/artifacts/loom-integration.yaml @@ -32,8 +32,10 @@ artifacts: tags: [loom, optimization, pipeline, integration] links: - type: derives-from + target: BR-002 + - type: refines target: FR-002 - - type: derives-from + - type: refines target: FR-007 fields: req-type: interface @@ -58,8 +60,10 @@ artifacts: tags: [loom, optimization, compat] links: - type: derives-from + target: BR-002 + - type: refines target: FR-002 - - type: derives-from + - type: refines target: FR-007 - type: satisfies target: LI-001 @@ -90,6 +94,8 @@ artifacts: tags: [loom, api, interface] links: - type: derives-from + target: BR-002 + - type: refines target: LI-001 fields: req-type: interface @@ -113,6 +119,8 @@ artifacts: tags: [loom, feature-gate, ux] links: - type: derives-from + target: BR-004 + - type: refines target: LI-001 fields: req-type: functional @@ -144,8 +152,10 @@ artifacts: tags: [loom, architecture, cli] links: - type: allocated-from + target: TR-003 + - type: traces-to target: LI-001 - - type: allocated-from + - type: traces-to target: LI-003 fields: component-type: software @@ -168,6 +178,8 @@ artifacts: tags: [loom, architecture, optimization] links: - type: allocated-from + target: TR-004 + - type: traces-to target: LI-002 fields: component-type: software @@ -185,7 +197,7 @@ artifacts: # --------------------------------------------------------------------------- - id: LI-VER-001 - type: sw-verification + type: sys-verification title: Loom integration CLI test description: > Verify that the --loom flag produces the expected error when the @@ -199,7 +211,7 @@ artifacts: - type: verifies target: LI-004 fields: - method: test + method: automated-test verification-criteria: > 1. synth compile --loom input.wat exits with error mentioning loom feature when compiled without --features loom. @@ -209,7 +221,7 @@ artifacts: produces valid ARM ELF that passes Renode emulation tests. - id: LI-VER-002 - type: sw-verification + type: sys-verification title: Loom semantic equivalence description: > Verify that loom-optimized WASM modules produce functionally diff --git a/artifacts/verification.yaml b/artifacts/verification.yaml index 580d25e..4ca4253 100644 --- a/artifacts/verification.yaml +++ b/artifacts/verification.yaml @@ -218,3 +218,225 @@ artifacts: steps: run: "bazel build //crates:synth && bazel test //tests/..." coverage: "Hermetic build on Linux and macOS" + + # --------------------------------------------------------------------------- + # Target platform verification (TP-001..TP-008) + # --------------------------------------------------------------------------- + + - id: VER-TP-001 + type: sys-verification + title: Cortex-M4F target support verification + description: > + Renode emulation tests validate that synth produces correct + bare-metal ELF binaries for the Cortex-M4F target. The Renode + platform (synth_cortex_m.repl) emulates Cortex-M4 at 0x0 flash + / 0x20000000 SRAM. Tests in tests/renode/cortex_m_test.robot + compile WASM to ARM, load ELF via sysbus LoadELF, and verify + execution results via register inspection. + status: implemented + tags: [target-platforms, cortex-m4, renode, verification] + links: + - type: verifies + target: TP-001 + - type: verifies + target: TP-008 + fields: + method: simulation + evidence: + - tests/renode/cortex_m_test.robot + - tests/renode/synth_cortex_m.repl + steps: + run: "bazel test //tests/renode:cortex_m_test" + coverage: "Cortex-M4F ELF boot and execution on Renode emulation" + + - id: VER-TP-002 + type: sys-verification + title: Board profile and memory layout verification + description: > + Unit tests in synth-backend verify correct board profiles for + STM32F407 (TP-002) and nRF52840 (TP-003). Tests confirm flash + base addresses (0x08000000 for STM32, 0x00000000 for nRF52840), + RAM layout, MPU region counts, and FPU capabilities. Also tests + Cortex-M7 (TP-004) and M33 (TP-005) target specification + construction and hardware capability reporting. + status: implemented + tags: [target-platforms, board-profile, unit-tests, verification] + links: + - type: verifies + target: TP-002 + - type: verifies + target: TP-003 + - type: verifies + target: TP-004 + - type: verifies + target: TP-005 + fields: + method: automated-test + steps: + run: "cargo test -p synth-backend -- hardware_capabilities" + coverage: "STM32F407, nRF52840, Cortex-M7, Cortex-M33 profiles" + + - id: VER-TP-003 + type: sys-verification + title: Vector table and startup code verification + description: > + Tests verifying vector table generation (TP-006) and MPU region + allocation (TP-007). Unit tests confirm correct Thumb-mode + addresses in the vector table, Reset_Handler initializes R11 + to 0x20000000, FPU enable code writes CPACR, and MPU allocator + produces valid region configurations for power-of-2 sizes with + correct RBAR/RASR register values. + status: implemented + tags: [target-platforms, vector-table, mpu, verification] + links: + - type: verifies + target: TP-006 + - type: verifies + target: TP-007 + fields: + method: automated-test + steps: + run: "cargo test -p synth-backend -- vector_table mpu" + coverage: "Vector table layout, startup code, MPU region allocation" + + # --------------------------------------------------------------------------- + # Zephyr integration verification (ZI-001..ZI-010) + # --------------------------------------------------------------------------- + + - id: VER-ZI-001 + type: sys-verification + title: Zephyr CMake and AAPCS integration verification + description: > + The examples/zephyr-poc/ project demonstrates Zephyr CMake build + integration (ZI-001) and AAPCS calling convention compliance + (ZI-002). The project includes synth-compiled assembly via + target_sources and calls synth functions from C using extern + declarations. Evidence that .syntax unified / .thumb / .global + directives work with the Zephyr SDK arm-none-eabi-gcc assembler. + status: implemented + tags: [zephyr, cmake, aapcs, verification] + links: + - type: verifies + target: ZI-001 + - type: verifies + target: ZI-002 + fields: + method: inspection + evidence: + - examples/zephyr-poc/CMakeLists.txt + - examples/zephyr-poc/prj.conf + - examples/zephyr-poc/src/ + steps: + run: "Review zephyr-poc project structure and build integration" + coverage: "CMake integration, AAPCS calling convention, assembly directives" + + - id: VER-ZI-002 + type: sys-verification + title: Zephyr configuration and linker script verification + description: > + Verification of Zephyr prj.conf configuration (ZI-004), + linker script generation (ZI-008), and Meld runtime integration + (ZI-009). Evidence from examples/zephyr-poc/prj.conf demonstrates + required Kconfig settings. Unit tests in synth-backend verify + LinkerScriptGenerator produces valid scripts with ENTRY, + .isr_vector KEEP, .data AT> FLASH, and Meld section support. + status: implemented + tags: [zephyr, configuration, linker-script, verification] + links: + - type: verifies + target: ZI-004 + - type: verifies + target: ZI-008 + - type: verifies + target: ZI-009 + fields: + method: automated-test + evidence: + - examples/zephyr-poc/prj.conf + steps: + run: "cargo test -p synth-backend -- linker_script" + coverage: "Linker script generation, Meld sections, Zephyr config" + + - id: VER-ZI-003 + type: sys-verification + title: Zephyr calculator application verification + description: > + The examples/zephyr-calculator/ project demonstrates a complete + Zephyr application (ZI-005) integrating synth-compiled calculator + functions (add, subtract, multiply, divide, modulo). Includes + CMakeLists.txt, prj.conf, calculator.wat source, and C + application code calling synth-compiled functions via extern + declarations. + status: implemented + tags: [zephyr, calculator, example, verification] + links: + - type: verifies + target: ZI-005 + fields: + method: inspection + evidence: + - examples/zephyr-calculator/CMakeLists.txt + - examples/zephyr-calculator/prj.conf + - examples/zephyr-calculator/calculator.wat + - examples/zephyr-calculator/src/ + steps: + run: "Review zephyr-calculator project structure" + coverage: "Calculator WASM-to-Zephyr integration" + + - id: VER-ZI-004 + type: sys-verification + title: Bounds checking strategy verification + description: > + Unit tests in synth-memory verify bounds checking strategy + selection for Zephyr targets (ZI-010). Tests confirm + SoftwareBoundsChecker traps on out-of-bounds, MaskingBoundsChecker + wraps for power-of-2 sizes, and MpuBoundsChecker delegates to + hardware. Also covers the Memory Domain integration design + (ZI-003) via the MemoryPlatform trait architecture. + status: implemented + tags: [zephyr, bounds-checking, memory, verification] + links: + - type: verifies + target: ZI-003 + - type: verifies + target: ZI-010 + fields: + method: automated-test + steps: + run: "cargo test -p synth-memory" + coverage: "Bounds checking strategies, memory platform abstraction" + + # --------------------------------------------------------------------------- + # Canonical ABI verification (CM-TR-001..CM-TR-004) + # --------------------------------------------------------------------------- + + - id: VER-CM-001 + type: sw-verification + title: Canonical ABI type layout and lift/lower unit tests + description: > + Comprehensive unit tests in synth-abi verifying canonical ABI + compliance for CM-TR-001 (type layout), CM-TR-002 (primitive + lift/lower), CM-TR-003 (compound lift/lower), and CM-TR-004 + (Memory trait). Tests include roundtrip verification for all + WIT type families (primitives, strings in UTF-8/UTF-16/Latin-1, + records, variants, options, results, enums, flags, lists) and + Memory trait bounds checking. + status: implemented + tags: [canonical-abi, synth-abi, unit-tests, verification] + links: + - type: verifies + target: CM-TR-001 + - type: verifies + target: CM-TR-002 + - type: verifies + target: CM-TR-003 + - type: verifies + target: CM-TR-004 + fields: + method: automated-test + steps: + run: "cargo test -p synth-abi" + coverage: > + 28+ tests: roundtrip primitives, string encoding (UTF-8, + UTF-16, Latin-1), records, variants, options, results, enums, + flags, lists, memory bounds checking