diff --git a/artifacts/architecture.yaml b/artifacts/architecture.yaml new file mode 100644 index 0000000..235287f --- /dev/null +++ b/artifacts/architecture.yaml @@ -0,0 +1,147 @@ +# Architecture Components (ASPICE SYS.3) +# +# System: Synth — WebAssembly-to-ARM Cortex-M AOT compiler +# +# Key architectural components mapping to the crate structure. +# Each component is allocated from one or more system requirements. +# +# Format: rivet generic-yaml + +artifacts: + - id: ARCH-001 + type: system-arch-component + title: 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. Entry point for the synthesis + pipeline. + status: implemented + tags: [frontend, parsing, wasm] + links: + - type: allocated-from + target: FR-001 + - type: allocated-from + target: FR-002 + fields: + component-type: software + interfaces: + inputs: [".wasm files", ".wat files", ".wit files"] + outputs: ["internal IR"] + crates: ["synth-cli", "synth-core"] + + - id: ARCH-002 + type: system-arch-component + title: Synthesis (WASM to ARM instruction selection) + description: > + Pattern-matching instruction selector that maps WebAssembly operations + to ARM Thumb-2 instruction sequences. Includes peephole optimizer + for local optimizations and register allocation using the virtual + stack model. + status: implemented + tags: [synthesis, instruction-selection, arm] + links: + - type: allocated-from + target: FR-002 + - type: allocated-from + target: FR-005 + - type: allocated-from + target: FR-007 + fields: + component-type: software + interfaces: + inputs: ["internal IR", "target profile"] + outputs: ["ARM instruction sequences"] + crates: ["synth-synthesis"] + + - id: ARCH-003 + type: system-arch-component + title: Backend (ARM encoding, 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 ready for flashing to Cortex-M targets. + status: implemented + tags: [backend, arm-encoding, elf] + links: + - type: allocated-from + target: FR-002 + - type: allocated-from + target: FR-003 + - type: allocated-from + target: FR-005 + - type: allocated-from + target: FR-008 + fields: + component-type: software + interfaces: + inputs: ["ARM instruction sequences", "memory layout", "linker script"] + outputs: ["ELF binary", "raw binary", "disassembly"] + crates: ["synth-backend"] + + - id: ARCH-004 + type: system-arch-component + title: Verification (Z3 SMT + Rocq proofs) + description: > + Dual verification strategy combining runtime Z3 SMT translation + validation (53 tests) with mechanized Rocq proofs (188 Qed / 52 + Admitted). Z3 validates per-compilation correctness of instruction + selection. Rocq proofs provide once-and-for-all correctness + guarantees for synthesis rules. + status: implemented + tags: [verification, z3, rocq, formal-methods] + links: + - type: allocated-from + target: FR-006 + - type: allocated-from + target: FR-008 + fields: + component-type: software + interfaces: + inputs: ["WASM ops", "ARM instruction sequences", "synthesis rules"] + outputs: ["verification verdicts", "proof artifacts"] + crates: ["synth-verify"] + proof-directory: "coq/Synth/" + + - id: ARCH-005 + type: system-arch-component + title: Memory (portable memory abstraction) + description: > + Portable memory abstraction layer supporting Zephyr RTOS, Linux, + and bare-metal environments. Handles linear memory allocation, + bounds check generation, and MPU region mapping for hardware- + assisted memory protection. + status: implemented + tags: [memory, abstraction, mpu] + links: + - type: allocated-from + target: FR-003 + - type: allocated-from + target: FR-008 + fields: + component-type: software + interfaces: + inputs: ["memory configuration", "target profile"] + outputs: ["memory layout", "bounds check code", "MPU configuration"] + crates: ["synth-memory"] + + - id: ARCH-006 + type: system-arch-component + title: ABI (Component Model ABI) + description: > + WebAssembly Component Model canonical ABI implementation for + lift/lower operations. Ensures ABI compatibility with Meld (fuser) + and Kiln (runtime) for the __meld_dispatch_import bridge interface. + status: implemented + tags: [abi, component-model, interop] + links: + - type: allocated-from + target: FR-001 + - type: allocated-from + target: FR-004 + fields: + component-type: software + interfaces: + inputs: ["WIT interface types", "component imports/exports"] + outputs: ["lowered ABI calls", "import dispatch stubs"] + crates: ["synth-abi"] diff --git a/artifacts/nonfunctional-requirements.yaml b/artifacts/nonfunctional-requirements.yaml new file mode 100644 index 0000000..a05871e --- /dev/null +++ b/artifacts/nonfunctional-requirements.yaml @@ -0,0 +1,110 @@ +# Non-Functional Requirements (ASPICE SYS.2) +# +# System: Synth — WebAssembly-to-ARM Cortex-M AOT compiler +# +# Derived from: docs/requirements/REQUIREMENTS.md Section 4 (Non-Functional Requirements) +# +# Format: rivet generic-yaml + +artifacts: + - id: NFR-001 + type: system-req + title: Performance targets + description: > + Synth shall achieve compilation speed no worse than 10x slower than + LLVM, generated code at least 80% of native performance, code size + less than 120% of native equivalent, startup time under 100ms for + typical embedded applications, and memory footprint under 512KB for + the synthesizer runtime. + status: draft + tags: [performance, nonfunctional] + links: + - type: derives-from + target: BR-002 + fields: + req-type: performance + priority: must + verification-criteria: > + Benchmark suite comparing generated code against hand-written native; + code size measurement on reference embedded applications. + + - id: NFR-002 + type: system-req + title: Reliability + description: > + Synth shall handle all valid WebAssembly inputs without crashing, + produce deterministic output (same input yields same output), provide + comprehensive error handling, achieve greater than 99% correctness on + the WebAssembly test suite, and support continuous fuzzing integration. + status: draft + tags: [reliability, determinism, nonfunctional] + links: + - type: derives-from + target: BR-001 + - type: derives-from + target: BR-002 + fields: + req-type: constraint + priority: must + verification-criteria: > + No panics on fuzzed inputs; deterministic output verified by + compiling same input on different machines and comparing ELF bytes. + + - id: NFR-003 + type: system-req + title: Maintainability + description: > + Synth shall be written in Rust for memory safety, use a modular + architecture with pluggable backends, have a comprehensive test suite + (unit, integration, end-to-end), clear code documentation, and a + CI/CD pipeline with automated testing. + status: draft + tags: [maintainability, nonfunctional] + links: + - type: derives-from + target: BR-004 + fields: + req-type: constraint + priority: should + verification-criteria: > + Workspace builds with zero clippy warnings; test suite covers + all crates; CI pipeline runs on every PR. + + - id: NFR-004 + type: system-req + title: Portability + description: > + Synth shall run on Linux, macOS, and Windows, support cross-compilation, + have minimal dependencies, and provide a container-based distribution + option. + status: draft + tags: [portability, nonfunctional] + links: + - type: derives-from + target: BR-004 + fields: + req-type: constraint + priority: should + verification-criteria: > + CI builds and tests pass on Linux and macOS; Bazel hermetic + build reproduces on both platforms. + + - id: NFR-005 + type: system-req + title: Security + description: > + Synth shall minimize unsafe Rust to isolated audited modules, validate + all WebAssembly input files, perform bounds checking in the synthesizer + itself, support regular security audits, and maintain a CVE response + process. + status: draft + tags: [security, nonfunctional] + links: + - type: derives-from + target: BR-001 + fields: + req-type: safety + priority: must + verification-criteria: > + Cargo clippy with deny warnings; no unsafe outside of clearly + marked modules; input validation fuzz testing. diff --git a/artifacts/stakeholder-requirements.yaml b/artifacts/stakeholder-requirements.yaml new file mode 100644 index 0000000..b15bac9 --- /dev/null +++ b/artifacts/stakeholder-requirements.yaml @@ -0,0 +1,68 @@ +# Stakeholder Requirements (ASPICE SYS.1) +# +# System: Synth — WebAssembly-to-ARM Cortex-M AOT compiler +# +# Derived from: docs/requirements/REQUIREMENTS.md Section 2 (Business Requirements) +# +# Format: rivet generic-yaml + +artifacts: + - id: BR-001 + type: stakeholder-req + title: Safety-critical qualification + description: > + Synth shall support qualification for safety-critical domains + including automotive (ISO 26262), medical (IEC 62304), and industrial + (IEC 61508). This includes generating qualification artifacts, supporting + formal verification of synthesis correctness, providing traceability from + WebAssembly to native code, enabling deterministic reproducible builds, + and supporting qualified tool chain integration. + status: draft + tags: [safety, qualification, certification] + fields: + priority: must + source: REQUIREMENTS.md + + - id: BR-002 + type: stakeholder-req + title: Competitive performance + description: > + Synth shall synthesize code achieving at least 80% of hand-written + native performance. This includes AOT compilation for deterministic + execution, hardware-accelerated bounds checking (MPU/PMP), XIP + (execute-in-place) for flash-constrained systems, and minimal code + size overhead (less than 20% vs native). + status: draft + tags: [performance, optimization] + fields: + priority: must + source: REQUIREMENTS.md + + - id: BR-003 + type: stakeholder-req + title: Multi-target support + description: > + Synth shall support major embedded architectures including ARM + Cortex-M (M3, M4, M7, M33, M55) and RISC-V (RV32IMAC, RV32GC, + RV64GC). The architecture shall be extensible for additional targets + with target-specific optimization opportunities and hardware feature + detection. + status: draft + tags: [targets, arm, riscv] + fields: + priority: must + source: REQUIREMENTS.md + + - id: BR-004 + type: stakeholder-req + title: Developer experience + description: > + Synth shall provide a simple CLI interface for synthesis, integration + with standard toolchains (Clang, Rust, GCC), clear error messages and + diagnostics, documentation and examples, and profiling and optimization + guidance. + status: draft + tags: [usability, tooling] + fields: + priority: should + source: REQUIREMENTS.md diff --git a/artifacts/system-requirements.yaml b/artifacts/system-requirements.yaml new file mode 100644 index 0000000..7fc4502 --- /dev/null +++ b/artifacts/system-requirements.yaml @@ -0,0 +1,188 @@ +# System Requirements (ASPICE SYS.2) +# +# System: Synth — WebAssembly-to-ARM Cortex-M AOT compiler +# +# Derived from: docs/requirements/REQUIREMENTS.md Section 3 (Functional Requirements) +# +# Each system requirement derives from one or more stakeholder requirements. +# +# Format: rivet generic-yaml + +artifacts: + - id: FR-001 + type: system-req + title: Component Model support + description: > + Synth shall parse WebAssembly Component Model binary format, validate + component structure and interfaces, support WIT definitions, handle + component composition (shared-everything and shared-nothing), support + canonical ABI lowering and lifting, and multi-memory proposal support + for isolation. + status: draft + tags: [component-model, parsing] + links: + - type: derives-from + target: BR-003 + fields: + req-type: functional + priority: must + verification-criteria: > + Parse and validate Component Model binaries; round-trip canonical + ABI lowering and lifting for all WIT interface types. + + - id: FR-002 + type: system-req + title: Synthesis pipeline + description: > + Synth shall implement a multi-phase synthesis pipeline consisting of + analysis (dependency graph, memory layout, call graph, data flow, + hardware capability detection), optimization (dead code elimination, + inlining, constant propagation, bounds check optimization), synthesis + (instruction selection, register allocation, MPU/PMP mapping, XIP + binary generation), and verification (SMT translation validation, + bounds checking verification, CFI verification). + status: draft + tags: [synthesis, pipeline, core] + links: + - type: derives-from + target: BR-002 + - type: derives-from + target: BR-003 + fields: + req-type: functional + priority: must + verification-criteria: > + End-to-end compilation of WASM modules to ARM ELF binaries; + generated code passes Renode emulation tests. + + - id: FR-003 + type: system-req + title: Memory management + description: > + Synth shall synthesize linear memory allocation and bounds checking + code, support multi-memory with hardware protection region mapping + (MPU for ARM, PMP for RISC-V), generate MPU/PMP configuration code, + and fall back to software checks when hardware protection is + unavailable. + status: draft + tags: [memory, mpu, safety] + links: + - type: derives-from + target: BR-001 + - type: derives-from + target: BR-002 + fields: + req-type: functional + priority: must + verification-criteria: > + Memory bounds checks verified via Z3 SMT; MPU configuration + validated on Cortex-M4 target via Renode emulation. + + - id: FR-004 + type: system-req + title: Direct function calls + description: > + Synth should devirtualize component imports/exports when possible, + replace indirect calls with direct calls for known targets, inline + component boundaries for shared-everything linking, and optimize + calling conventions for the target architecture. + status: draft + tags: [optimization, calling-convention] + links: + - type: derives-from + target: BR-002 + fields: + req-type: functional + priority: should + verification-criteria: > + Benchmark showing call overhead reduction compared to indirect + dispatch. + + - id: FR-005 + type: system-req + title: Target-specific optimizations + description: > + Synth shall implement target-specific optimizations including + Thumb-2 instruction selection, FPU detection and optimization, + MPU configuration, and XIP support for ARM Cortex-M targets. + Future targets include RISC-V with compressed instructions, + bit manipulation, vector extension, and PMP configuration. + status: draft + tags: [arm, optimization, thumb2] + links: + - type: derives-from + target: BR-002 + - type: derives-from + target: BR-003 + fields: + req-type: functional + priority: must + verification-criteria: > + Generated Thumb-2 code executes correctly on Cortex-M4 target; + FPU instructions used when target profile includes VFP. + + - id: FR-006 + type: system-req + title: Formal verification + description: > + Synth shall support formal verification of synthesis correctness + through mechanized proofs in Rocq (Coq), SMT-based translation + validation via Z3, and memory safety proofs covering linear memory + bounds, component isolation, and MPU/PMP configuration correctness. + status: draft + tags: [verification, formal-methods, rocq, z3] + links: + - type: derives-from + target: BR-001 + fields: + req-type: functional + priority: must + verification-criteria: > + All i32 operations have T1 result-correspondence proofs in Rocq; + Z3 translation validation passes for all compiled test cases. + + - id: FR-007 + type: system-req + title: Optimization framework + description: > + Synth should implement peephole optimization and link-time + optimization including cross-component optimization, dead code + elimination across boundaries, constant propagation through + component interfaces, and function specialization. + status: draft + tags: [optimization, peephole, lto] + links: + - type: derives-from + target: BR-002 + fields: + req-type: functional + priority: should + verification-criteria: > + Peephole optimizations preserve semantics (verified by Z3 SMT); + code size reduction measurable on benchmark suite. + + - id: FR-008 + type: system-req + title: Safety guarantees + description: > + Synth shall maintain WebAssembly safety properties in generated code + including memory bounds checking (explicit or hardware-assisted), + control-flow integrity (typed indirect calls), module/component + isolation, stack protection, and deterministic traps. For embedded + targets, WCET analysis support, real-time determinism (no GC, no JIT), + stack overflow detection, and hardware fault integration shall be + provided. + status: draft + tags: [safety, bounds-checking, cfi] + links: + - type: derives-from + target: BR-001 + - type: derives-from + target: BR-002 + fields: + req-type: safety + priority: must + verification-criteria: > + Bounds checks present for all memory access instructions; + CFI preserved through control flow translation; stack overflow + detection verified on Cortex-M4 via Renode. diff --git a/artifacts/technical-requirements.yaml b/artifacts/technical-requirements.yaml new file mode 100644 index 0000000..96e74a2 --- /dev/null +++ b/artifacts/technical-requirements.yaml @@ -0,0 +1,118 @@ +# Technical Requirements (ASPICE SWE.1) +# +# System: Synth — WebAssembly-to-ARM Cortex-M AOT compiler +# +# Derived from: docs/requirements/REQUIREMENTS.md Section 5 (Technical Requirements) +# +# These are software-level requirements derived from system requirements. +# +# Format: rivet generic-yaml + +artifacts: + - id: TR-001 + type: sw-req + title: Input format support + description: > + Synth shall accept WebAssembly Component Model binary (.wasm), + WebAssembly text format (.wat), WIT interface definitions (.wit), + and configuration files for synthesis options (TOML/YAML) as inputs. + Target specification files shall define the target architecture and + available hardware features. + status: draft + tags: [input, formats] + links: + - type: derives-from + target: FR-001 + - type: derives-from + target: FR-002 + fields: + req-type: functional + priority: must + verification-criteria: > + Successfully parse .wasm, .wat, and .wit files; reject malformed + inputs with descriptive error messages. + + - id: TR-002 + type: sw-req + title: Output format support + description: > + Synth shall produce ELF binaries for bare-metal targets, raw binary + and HEX/BIN formats for flash programming, textual assembly (.s files), + DWARF debug information, and verification artifacts (Rocq proof + traces, SMT validation logs). + status: draft + tags: [output, elf, formats] + links: + - type: derives-from + target: FR-002 + - type: derives-from + target: FR-005 + fields: + req-type: functional + priority: must + verification-criteria: > + Generated ELF files pass readelf validation; binaries boot on + Cortex-M4 target via Renode emulation. + + - id: TR-003 + type: sw-req + title: Toolchain integration + description: > + Synth should integrate with Clang/LLVM and Rust toolchains, support + CMake and Cargo build systems, and provide a CLI interface compatible + with standard embedded development workflows. + status: draft + tags: [toolchain, integration] + links: + - type: derives-from + target: FR-002 + fields: + req-type: interface + priority: should + verification-criteria: > + CLI interface documented; output compatible with standard + ARM toolchain (objdump, readelf, gdb). + + - id: TR-004 + type: sw-req + title: Synthesis configuration + description: > + Synth shall accept configuration specifying target architecture + (CPU, variant, features), memory configuration (flash/RAM sizes, + MPU/PMP regions, stack sizes), optimization settings (size/speed/ + balanced, inline threshold, unroll limits), and safety settings + (hardware/software bounds checking, stack overflow detection, trap + handling strategy). + status: draft + tags: [configuration, targets] + links: + - type: derives-from + target: FR-005 + - type: derives-from + target: FR-003 + fields: + req-type: functional + priority: must + verification-criteria: > + Target profiles correctly select instruction sets; MPU region + count matches target specification. + + - id: TR-005 + type: sw-req + title: Verification infrastructure + description: > + Synth shall integrate Z3 for SMT-based translation validation with + bit-vector reasoning and configurable timeouts, Rocq for mechanized + correctness proofs of synthesis rules, and property-based testing + (proptest) for randomized verification of instruction semantics. + status: draft + tags: [verification, z3, rocq, proptest] + links: + - type: derives-from + target: FR-006 + fields: + req-type: functional + priority: must + verification-criteria: > + Z3 validation passes for all compiled test cases; Rocq proofs + compile without errors (188 Qed); proptest suites pass. diff --git a/artifacts/verification.yaml b/artifacts/verification.yaml new file mode 100644 index 0000000..46711b1 --- /dev/null +++ b/artifacts/verification.yaml @@ -0,0 +1,151 @@ +# Verification Artifacts (ASPICE SYS.5) +# +# System: Synth — WebAssembly-to-ARM Cortex-M AOT compiler +# +# Key verification activities and their traceability to system requirements. +# +# Format: rivet generic-yaml + +artifacts: + - id: VER-001 + type: sys-verification + title: Rocq T1 result-correspondence proofs + description: > + 39 Qed proofs in Rocq establishing result-correspondence between + WebAssembly instruction semantics and the compiled ARM instruction + sequences. Each proof shows that for a given WASM operation, the + compiled ARM code produces the exact same result value. Covers all + i32 arithmetic, division, comparison, bit-manipulation, and + shift/rotate operations. + status: implemented + tags: [rocq, formal-verification, t1-proofs] + links: + - type: verifies + target: FR-006 + - type: verifies + target: FR-008 + fields: + method: formal-verification + preconditions: + - Rocq 9 installed (via Nix or local) + - coq/Synth/ proof suite compiles + steps: + build: "bazel test //coq:verify_proofs" + coverage: "39 Qed — see coq/STATUS.md for full matrix" + + - id: VER-002 + type: sys-verification + title: Rocq T2 existence proofs + description: > + 95 Qed proofs in Rocq establishing existence — that the compiled ARM + instruction sequence terminates and produces some result for each + covered WASM operation. Weaker than T1 (no value correspondence) but + covers more operations including i64 and conversion instructions. + status: implemented + tags: [rocq, formal-verification, t2-proofs] + links: + - type: verifies + target: FR-006 + fields: + method: formal-verification + preconditions: + - Rocq 9 installed (via Nix or local) + steps: + build: "bazel test //coq:verify_proofs" + coverage: "95 Qed — see coq/STATUS.md for full matrix" + + - id: VER-003 + type: sys-verification + title: Z3 SMT translation validation + description: > + 53 Z3 SMT-based translation validation tests that verify each + compilation preserves WebAssembly semantics. Uses bit-vector + reasoning to check that the ARM instruction sequence produces + results equivalent to the WASM specification for all possible + input values. + status: implemented + tags: [z3, smt, translation-validation] + links: + - type: verifies + target: FR-006 + - type: verifies + target: FR-002 + fields: + method: formal-verification + preconditions: + - Z3 solver available + steps: + run: "cargo test -p synth-verify" + coverage: "53 SMT verification tests" + + - id: VER-004 + type: sys-verification + title: Cargo workspace tests + description: > + 526+ tests across the Rust workspace covering unit tests for + 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. + status: implemented + tags: [cargo, unit-tests, integration-tests] + links: + - type: verifies + target: FR-002 + - type: verifies + target: FR-005 + - type: verifies + target: FR-008 + fields: + method: automated-test + steps: + run: "cargo test --workspace" + coverage: "526+ tests across all crates" + + - id: VER-005 + type: sys-verification + title: Renode ARM emulation tests + description: > + End-to-end tests that compile WASM modules to ARM ELF binaries and + 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). + status: implemented + tags: [renode, emulation, end-to-end, cortex-m4] + links: + - type: verifies + target: FR-002 + - type: verifies + target: FR-005 + - type: verifies + target: FR-008 + fields: + method: simulation + preconditions: + - Renode emulator available + - Bazel with rules_renode configured + steps: + run: "bazel test //tests/..." + coverage: "End-to-end ARM Cortex-M4 emulation" + + - id: VER-006 + type: sys-verification + title: Proptest property-based testing + description: > + 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. + status: implemented + tags: [proptest, property-based, fuzzing] + links: + - type: verifies + target: FR-002 + - type: verifies + target: FR-005 + fields: + method: automated-test + steps: + run: "cargo test --workspace (proptest cases included)" + coverage: "Property-based verification of instruction semantics" diff --git a/rivet.yaml b/rivet.yaml new file mode 100644 index 0000000..d47ddd2 --- /dev/null +++ b/rivet.yaml @@ -0,0 +1,52 @@ +project: + name: synth + version: "0.1.0" + description: > + WebAssembly-to-ARM Cortex-M AOT compiler with mechanized correctness + proofs in Rocq. Produces bare-metal ELF binaries for embedded targets + with formal verification via Z3 SMT and Rocq proof suites. + schemas: + - common + - stpa + - aspice + - dev + +sources: + - path: artifacts + format: generic-yaml + - path: safety/stpa + format: stpa-yaml + +docs: + - docs + +commits: + format: trailers + trailers: + Implements: satisfies + Fixes: fixes + Verifies: verifies + Trace: traces-to + exempt-types: + - chore + - style + - ci + - docs + - build + traced-paths: + - crates/ + - coq/ + - safety/ + +externals: + kiln: + git: https://github.com/pulseengine/kiln.git + path: /Volumes/Home/git/pulseengine/kiln + ref: main + prefix: kiln + + meld: + git: https://github.com/pulseengine/meld.git + path: /Volumes/Home/git/pulseengine/meld + ref: main + prefix: meld