feat: set up rivet SDLC artifact traceability

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"]

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.

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