diff --git a/artifacts/sw-architecture.yaml b/artifacts/sw-architecture.yaml new file mode 100644 index 0000000..76c2dfc --- /dev/null +++ b/artifacts/sw-architecture.yaml @@ -0,0 +1,207 @@ +# SW Architecture Components (ASPICE SWE.2) +# +# System: Synth — WebAssembly-to-ARM Cortex-M AOT compiler +# +# Software architecture decomposition mapping to the Rust crate structure. +# Each component is allocated from one or more technical requirements (sw-req). +# +# Format: rivet generic-yaml + +artifacts: + - id: SWA-001 + type: sw-arch-component + title: synth-cli (CLI entry point) + description: > + CLI entry point providing synth compile, synth verify, and synth disasm + subcommands. Parses command-line arguments, reads input files (.wasm, + .wat, .wit, TOML/YAML configuration), orchestrates the synthesis + pipeline, and writes output artifacts. + status: implemented + tags: [cli, entry-point] + links: + - type: allocated-from + target: TR-001 + - type: allocated-from + target: TR-003 + fields: + component-type: software + crate: synth-cli + + - id: SWA-002 + type: sw-arch-component + title: synth-core (shared types and error handling) + description: > + Shared types, error handling, and the Backend trait used across + all crates. Defines the internal IR, target profile structures, + and common configuration types for input/output format support. + status: implemented + tags: [core, types, shared] + links: + - type: allocated-from + target: TR-001 + - type: allocated-from + target: TR-004 + fields: + component-type: software + crate: synth-core + + - id: SWA-003 + type: sw-arch-component + title: synth-frontend (WASM/WAT parsing) + description: > + WebAssembly and WAT input parsing, validation, and IR construction. + Handles Component Model binary format, core module extraction, + and WIT interface type definitions. Validates input files and + produces descriptive error messages for malformed inputs. + status: implemented + tags: [frontend, parsing, wasm] + links: + - type: allocated-from + target: TR-001 + fields: + component-type: software + crate: synth-frontend + + - id: SWA-004 + type: sw-arch-component + title: synth-synthesis (WASM to ARM instruction selection) + description: > + Pattern-matching instruction selector that maps WebAssembly operations + to ARM Thumb-2 instruction sequences. Includes register allocation + using the virtual stack model and integration with the verification + infrastructure for per-compilation validation. + status: implemented + tags: [synthesis, instruction-selection] + links: + - type: allocated-from + target: TR-001 + - type: allocated-from + target: TR-005 + fields: + component-type: software + crate: synth-synthesis + + - id: SWA-005 + type: sw-arch-component + title: synth-backend (ARM encoding and ELF generation) + description: > + ARM Thumb-2 machine code encoder, ELF binary builder, vector table + generator, linker script support, and MPU configuration. Produces + bare-metal ELF binaries, raw binary, HEX/BIN, and disassembly + output formats. + status: implemented + tags: [backend, arm-encoding, elf] + links: + - type: allocated-from + target: TR-001 + - type: allocated-from + target: TR-002 + - type: allocated-from + target: TR-004 + fields: + component-type: software + crate: synth-backend + + - id: SWA-006 + type: sw-arch-component + title: synth-verify (Z3 SMT translation validation) + description: > + Z3 SMT-based translation validation using bit-vector reasoning with + configurable timeouts. Verifies each compilation preserves WebAssembly + semantics by checking that the ARM instruction sequence produces + results equivalent to the WASM specification. + status: implemented + tags: [verification, z3, smt] + links: + - type: allocated-from + target: TR-005 + fields: + component-type: software + crate: synth-verify + + - id: SWA-007 + type: sw-arch-component + title: synth-analysis (SSA and control flow analysis) + description: > + Static analysis passes including SSA construction, control flow + analysis, dependency graph building, and data flow analysis. + Provides analysis results consumed by the synthesis and optimization + stages. + status: implemented + tags: [analysis, ssa, control-flow] + links: + - type: allocated-from + target: TR-001 + fields: + component-type: software + crate: synth-analysis + + - id: SWA-008 + type: sw-arch-component + title: synth-abi (Component Model ABI) + description: > + WebAssembly Component Model canonical ABI implementation for + lift/lower operations. Handles WIT interface type definitions + and ensures ABI compatibility for component composition. + status: implemented + tags: [abi, component-model] + links: + - type: allocated-from + target: TR-001 + fields: + component-type: software + crate: synth-abi + + - id: SWA-009 + type: sw-arch-component + title: synth-memory (portable memory abstraction) + description: > + Portable memory abstraction layer supporting Zephyr RTOS, Linux, + and bare-metal environments. Handles linear memory allocation, + bounds check generation, MPU region mapping, and memory layout + configuration for target-specific flash/RAM sizes. + status: implemented + tags: [memory, abstraction, mpu] + links: + - type: allocated-from + target: TR-001 + - type: allocated-from + target: TR-004 + fields: + component-type: software + crate: synth-memory + + - id: SWA-010 + type: sw-arch-component + title: synth-opt (peephole optimizer) + description: > + Peephole optimization framework for local instruction sequence + optimization. Implements pattern-based rewrites that preserve + semantics (verified via Z3 SMT) while reducing code size and + improving execution performance. + status: implemented + tags: [optimization, peephole] + links: + - type: allocated-from + target: TR-001 + fields: + component-type: software + crate: synth-opt + + - id: SWA-011 + type: sw-arch-component + title: synth-test (WAST to Robot Framework test generator) + description: > + WAST-to-Robot-Framework test generator for Renode ARM emulation + tests. Generates test cases from WebAssembly test suite files + and integrates with the Bazel build system via rules_renode. + status: implemented + tags: [test-generation, renode, bazel] + links: + - type: allocated-from + target: TR-002 + - type: allocated-from + target: TR-003 + fields: + component-type: software + crate: synth-test diff --git a/artifacts/sw-verification.yaml b/artifacts/sw-verification.yaml new file mode 100644 index 0000000..f606b85 --- /dev/null +++ b/artifacts/sw-verification.yaml @@ -0,0 +1,108 @@ +# SW Verification Artifacts (ASPICE SWE.6) +# +# System: Synth — WebAssembly-to-ARM Cortex-M AOT compiler +# +# Software-level verification measures tracing to technical requirements (sw-req). +# +# Format: rivet generic-yaml + +artifacts: + - id: SWVER-001 + type: sw-verification + title: WASM/WAT/WIT input parsing tests + description: > + Unit and integration tests verifying correct parsing of WebAssembly + binary (.wasm), text format (.wat), and WIT interface definition + (.wit) files. Includes tests for malformed input rejection with + descriptive error messages, Component Model binary validation, and + target specification file parsing (TOML/YAML). + status: implemented + tags: [parsing, input-formats, unit-tests] + links: + - type: verifies + target: TR-001 + fields: + method: automated-test + steps: + run: "cargo test -p synth-cli -p synth-core -p synth-abi" + coverage: "Input format parsing and validation" + + - id: SWVER-002 + type: sw-verification + title: ELF output and binary format validation + description: > + Tests verifying ELF binary generation, including readelf validation + of generated files, vector table layout correctness, linker script + processing, DWARF debug information generation, and Renode boot + tests confirming binaries execute on Cortex-M4 targets. Also covers + disassembly output and verification artifact generation. + status: implemented + tags: [elf, output-formats, integration-tests] + links: + - type: verifies + target: TR-002 + fields: + method: automated-test + steps: + run: "cargo test -p synth-backend && bazel test //tests/..." + coverage: "ELF generation, binary formats, Renode boot" + + - id: SWVER-003 + type: sw-verification + title: Toolchain integration and CLI tests + description: > + Tests verifying CLI interface compatibility with standard embedded + workflows, including synth compile/verify/disasm subcommands, output + file compatibility with ARM toolchain utilities (objdump, readelf), + and Bazel build system integration tests that exercise the full + build pipeline. + status: implemented + tags: [toolchain, cli, integration] + links: + - type: verifies + target: TR-003 + fields: + method: automated-test + steps: + run: "cargo test -p synth-cli && bazel build //crates:synth" + coverage: "CLI interface and toolchain compatibility" + + - id: SWVER-004 + type: sw-verification + title: Target configuration and synthesis settings tests + description: > + Tests verifying target architecture configuration including CPU + variant selection, FPU capability detection, MPU region mapping, + memory layout configuration (flash/RAM sizes, stack sizes), + optimization level settings, and safety mode configuration + (hardware vs software bounds checking, trap handling strategy). + status: implemented + tags: [configuration, targets, settings] + links: + - type: verifies + target: TR-004 + fields: + method: automated-test + steps: + run: "cargo test -p synth-backend -p synth-synthesis -p synth-memory" + coverage: "Target profiles, MPU config, memory layout" + + - id: SWVER-005 + type: sw-verification + title: Verification infrastructure integration tests + description: > + Tests verifying the verification infrastructure itself: Z3 SMT + translation validation with bit-vector reasoning and configurable + timeouts, Rocq proof compilation (188 Qed), and proptest + property-based testing integration. Ensures all three verification + backends produce correct results and integrate into the build. + status: implemented + tags: [z3, rocq, proptest, verification-infra] + links: + - type: verifies + target: TR-005 + fields: + method: automated-test + steps: + run: "cargo test -p synth-verify && bazel test //coq:verify_proofs" + coverage: "Z3 SMT suite, Rocq proof compilation, proptest" diff --git a/artifacts/verification.yaml b/artifacts/verification.yaml index 46711b1..580d25e 100644 --- a/artifacts/verification.yaml +++ b/artifacts/verification.yaml @@ -70,6 +70,10 @@ artifacts: target: FR-006 - type: verifies target: FR-002 + - type: verifies + target: FR-003 + - type: verifies + target: FR-007 fields: method: formal-verification preconditions: @@ -86,16 +90,29 @@ artifacts: instruction encoding, integration tests for the synthesis pipeline, and end-to-end tests compiling WASM to ARM and verifying output. Includes tests for ELF generation, vector table layout, MPU - configuration, and calling convention correctness. + configuration, calling convention correctness, ABI lift/lower, + memory management, peephole optimization, and function call synthesis. status: implemented tags: [cargo, unit-tests, integration-tests] links: + - type: verifies + target: FR-001 - type: verifies target: FR-002 + - type: verifies + target: FR-003 + - type: verifies + target: FR-004 - type: verifies target: FR-005 + - type: verifies + target: FR-007 - type: verifies target: FR-008 + - type: verifies + target: NFR-002 + - type: verifies + target: NFR-005 fields: method: automated-test steps: @@ -110,16 +127,24 @@ artifacts: execute them on an emulated Cortex-M4 target using Renode. Validates that compiled code boots correctly, produces expected output, and handles traps properly on realistic hardware emulation. Uses the - WAST-to-Robot-Framework test generator (synth-test crate). + WAST-to-Robot-Framework test generator (synth-test crate). Exercises + memory management, function call dispatch, and target-specific code + generation end-to-end. status: implemented tags: [renode, emulation, end-to-end, cortex-m4] links: - type: verifies target: FR-002 + - type: verifies + target: FR-003 + - type: verifies + target: FR-004 - type: verifies target: FR-005 - type: verifies target: FR-008 + - type: verifies + target: NFR-001 fields: method: simulation preconditions: @@ -136,7 +161,8 @@ artifacts: Property-based testing using proptest to verify instruction encoding correctness, synthesis rule semantics, and edge-case handling with randomly generated inputs. Covers instruction encoding round-trips, - arithmetic overflow behavior, and bounds check generation. + arithmetic overflow behavior, bounds check generation, and input + validation for WebAssembly modules. status: implemented tags: [proptest, property-based, fuzzing] links: @@ -144,8 +170,51 @@ artifacts: target: FR-002 - type: verifies target: FR-005 + - type: verifies + target: NFR-002 + - type: verifies + target: NFR-005 fields: method: automated-test steps: run: "cargo test --workspace (proptest cases included)" coverage: "Property-based verification of instruction semantics" + + - id: VER-007 + type: sys-verification + title: CI quality gates (clippy, fmt, deny warnings) + description: > + Continuous integration pipeline enforcing code quality through + cargo clippy with deny-warnings, cargo fmt --check for consistent + formatting, and workspace-wide compilation with no warnings. Ensures + maintainability standards are met on every pull request. + status: implemented + tags: [ci, clippy, fmt, quality] + links: + - type: verifies + target: NFR-003 + fields: + method: automated-test + steps: + run: "cargo clippy --workspace --all-targets -- -D warnings && cargo fmt --check" + coverage: "All crates, all targets" + + - id: VER-008 + type: sys-verification + title: Cross-platform CI and Bazel hermetic build + description: > + CI builds and tests running on Linux and macOS, combined with Bazel + hermetic builds that ensure reproducibility across platforms. Bazel + bzlmod configuration pins all toolchain versions (Rust 1.88, Rocq 9) + for deterministic cross-platform builds. Cross-compilation tests + verify ARM target code generation from both host platforms. + status: implemented + tags: [ci, portability, bazel, cross-platform] + links: + - type: verifies + target: NFR-004 + fields: + method: automated-test + steps: + run: "bazel build //crates:synth && bazel test //tests/..." + coverage: "Hermetic build on Linux and macOS"