requirements.yaml

# STPA-Derived Safety Requirements for Spar
#
# These requirements are derived from the STPA analysis (analysis.yaml).
# Each addresses one or more Unsafe Control Actions (UCAs) by specifying
# concrete implementation requirements.
#
# Traceability:
#   analysis.yaml  →  requirements.yaml  →  architecture.yaml  →  validation.yaml
#   (hazards/UCAs)    (what to implement)    (how implemented)     (proof it works)

artifacts:

  # ══════════════════════════════════════════════════════════════════════
  # Parser Safety Requirements (from UCA-1, UCA-2, CC-1)
  # ══════════════════════════════════════════════════════════════════════

  - id: STPA-REQ-001
    type: requirement
    title: Unrecognized syntax must produce diagnostic
    description: >
      When the parser encounters a token sequence that does not match
      any AADL v2.2 grammar production, it must emit an error diagnostic
      with the source location (file, offset). The parser must not
      silently skip tokens without producing a CST error node.
    status: implemented
    tags: [safety, parser, stpa]
    traces-to: [CC-1]
    mitigates: [H-5]

  - id: STPA-REQ-002
    type: requirement
    title: Annex content must produce diagnostic when unparseable
    description: >
      When annex library or annex subclause content cannot be parsed
      by the registered annex parser, spar must emit a warning diagnostic
      indicating which annex was not processed. The annex content must
      not be silently dropped.
    status: implemented
    tags: [safety, parser, annex, stpa]
    traces-to: [CC-1]
    mitigates: [H-5, H-1]

  - id: STPA-REQ-003
    type: requirement
    title: Parser coverage test for all AADL productions
    description: >
      The parser test suite must contain at least one test for each
      AADL v2.2 grammar production rule (approximately 80 productions).
      Each test must verify that a valid input produces the expected
      CST structure and that an invalid input produces an error diagnostic.
    status: implemented
    tags: [safety, parser, testing, stpa]
    traces-to: [CC-1]
    mitigates: [H-5]

  # ══════════════════════════════════════════════════════════════════════
  # Model Builder Safety Requirements (from UCA-3, UCA-4, UCA-5, CC-2-4)
  # ══════════════════════════════════════════════════════════════════════

  - id: STPA-REQ-004
    type: requirement
    title: Lowering exhaustiveness check
    description: >
      The CST-to-ItemTree lowering must match on all SyntaxKind variants
      that represent semantic AADL constructs. Any unhandled variant must
      produce a warning diagnostic "unhandled construct: {kind}". This
      should be enforced via a #[deny(unreachable_patterns)] attribute
      or explicit wildcard with diagnostic emission.
    status: implemented
    tags: [safety, model, stpa]
    traces-to: [CC-2]
    mitigates: [H-3]

  - id: STPA-REQ-005
    type: requirement
    title: Unit conversion factor validation
    description: >
      Unit conversion factors in standard_properties.rs must be validated
      against AS5506 Appendix A values. The test suite must include
      explicit tests for every unit type (Time, Size, Data_Rate) verifying
      that conversion between all unit pairs produces correct results.
      Example: 1 ms = 1_000 us = 1_000_000 ns.
    status: implemented
    tags: [safety, properties, units, stpa]
    traces-to: [CC-3]
    mitigates: [H-6]

  - id: STPA-REQ-006
    type: requirement
    title: Property type validation during lowering
    description: >
      When lowering a property association, the property expression
      must be validated against the declared property type. Type
      mismatches (e.g., string value for integer property) must produce
      an error diagnostic.
    status: implemented
    tags: [safety, properties, stpa]
    traces-to: [CC-3]
    mitigates: [H-6]

  - id: STPA-REQ-007
    type: requirement
    title: Ambiguous name resolution warning
    description: >
      When multiple classifiers in different packages match a reference
      and the reference is not fully qualified, the resolver must emit
      a warning listing all candidates and which one was selected.
    status: implemented
    tags: [safety, resolution, stpa]
    traces-to: [CC-4]
    mitigates: [H-3]

  # ══════════════════════════════════════════════════════════════════════
  # Instance Builder Safety Requirements (from UCA-6-9, CC-5-8)
  # ══════════════════════════════════════════════════════════════════════

  - id: STPA-REQ-008
    type: requirement
    title: Modal subcomponent instantiation completeness
    description: >
      All subcomponents must be instantiated regardless of their
      in_modes filtering. Modal membership must be tracked as metadata
      on each instance, not used to exclude instances from the tree.
      Analyses can then filter by mode as needed.
    status: implemented
    tags: [safety, instance, modes, stpa]
    traces-to: [CC-5]
    mitigates: [H-3]

  - id: STPA-REQ-009
    type: requirement
    title: Array dimension validation
    description: >
      Array dimension expressions must evaluate to positive integers
      (>= 1). Zero or negative dimensions must produce an error
      diagnostic. Non-integer dimensions must produce an error.
    status: implemented
    tags: [safety, instance, arrays, stpa]
    traces-to: [CC-6]
    mitigates: [H-3]

  - id: STPA-REQ-010
    type: requirement
    title: Array connection index bounds checking
    description: >
      Connection patterns referencing array indices (e.g., sub[i] -> sub[i+1])
      must be validated against the declared array dimension. Out-of-bounds
      indices must produce an error diagnostic.
    status: implemented
    tags: [safety, instance, arrays, stpa]
    traces-to: [CC-6]
    mitigates: [H-3]

  - id: STPA-REQ-011
    type: requirement
    title: Feature group member matching by name
    description: >
      When tracing connections through feature groups, members must be
      matched by name (not by index position). inverse_of must reverse
      direction but preserve name-based matching.
    status: implemented
    tags: [safety, instance, connections, stpa]
    traces-to: [CC-7]
    mitigates: [H-3, H-1]

  - id: STPA-REQ-012
    type: requirement
    title: Circular containment detection
    description: >
      Before recursive instantiation, build the classifier reference
      graph and check for cycles. If a cycle is detected, emit an
      error diagnostic naming the cycle path and abort instantiation.
      Maximum recursion depth limit of 100 levels as a backup.
    status: implemented
    tags: [safety, instance, stpa]
    traces-to: [CC-8]
    mitigates: [H-3]

  - id: STPA-REQ-013
    type: requirement
    title: Unresolved connection endpoint diagnostic
    description: >
      After semantic connection tracing, any connection endpoint that
      does not resolve to a valid feature instance must produce a
      warning diagnostic with the connection name and unresolved path.
    status: implemented
    tags: [safety, instance, connections, stpa]
    traces-to: [CC-7]
    mitigates: [H-3]

  # ══════════════════════════════════════════════════════════════════════
  # Analysis Engine Safety Requirements (from UCA-10-13, CC-9-12)
  # ══════════════════════════════════════════════════════════════════════

  - id: STPA-REQ-014
    type: requirement
    title: Automatic analysis registration
    description: >
      All implemented analysis passes must be registered with
      AnalysisRunner by default. The register_all() function must use
      compile-time or inventory-based discovery to prevent omission.
      An integration test must verify the count of registered analyses
      matches the count of Analysis trait implementations.
    status: implemented
    tags: [safety, analysis, stpa]
    traces-to: [CC-9]
    mitigates: [H-1]

  - id: STPA-REQ-015
    type: requirement
    title: Typed property accessors for analyses
    description: >
      Analysis passes must access property values through typed accessor
      functions (e.g., get_period() -> Option<Duration>) that perform
      unit conversion and type validation. Direct string parsing of
      property values in analysis code is prohibited.
    status: implemented
    tags: [safety, analysis, properties, stpa]
    traces-to: [CC-10]
    mitigates: [H-1, H-6]

  - id: STPA-REQ-016
    type: requirement
    title: Severity assignment criteria documentation
    description: >
      Each analysis rule must document its severity assignment rationale
      in code comments. Error = confirmed standard violation or guaranteed
      runtime failure. Warning = likely defect. Info = suggestion.
    status: implemented
    tags: [safety, analysis, stpa]
    traces-to: [CC-11]
    mitigates: [H-1]

  - id: STPA-REQ-017
    type: requirement
    title: Modal-aware analysis
    description: >
      Analyses that read property values (scheduling, latency, resource
      budget) must evaluate properties per system operation mode when
      modal property associations exist. The analysis must report
      the worst-case mode or report per-mode results.
    status: implemented
    tags: [safety, analysis, modes, stpa]
    traces-to: [CC-12]
    mitigates: [H-1]

  - id: STPA-REQ-018
    type: requirement
    title: Intentional no-connection annotation
    description: >
      Engineers must be able to annotate ports as intentionally
      unconnected (e.g., via a property SPAR_Properties::Intentionally_Unconnected).
      Connectivity analysis must suppress warnings for annotated ports
      to reduce false positives and alert fatigue.
    status: implemented
    tags: [safety, analysis, false-positive, stpa]
    traces-to: [CC-12]
    mitigates: [H-2]

  # ══════════════════════════════════════════════════════════════════════
  # Output Safety Requirements (from UCA-14-16, CC-13-14)
  # ══════════════════════════════════════════════════════════════════════

  - id: STPA-REQ-019
    type: requirement
    title: Serialization round-trip test
    description: >
      An integration test must serialize every spar-hir public type to
      JSON, deserialize it back, and verify structural equality. This
      test must run on a non-trivial AADL model with instances, arrays,
      modes, properties, and connections.
    status: implemented
    tags: [safety, output, serde, stpa]
    traces-to: [CC-13]
    mitigates: [H-4]

  - id: STPA-REQ-020
    type: requirement
    title: No error diagnostic suppression
    description: >
      The CLI and WASM output formatters must transmit all error-severity
      diagnostics to the user. Filtering by severity must only be available
      via explicit user flag (--min-severity). The default must show all
      severities.
    status: implemented
    tags: [safety, output, stpa]
    traces-to: [CC-14]
    mitigates: [H-1]

  - id: STPA-REQ-021
    type: requirement
    title: SVG topology verification test
    description: >
      An integration test must verify that the SVG graph output contains
      the correct number of nodes and edges matching the instance model.
      Node labels must match component instance names. Edge connections
      must match the connection instances.
    status: implemented
    tags: [safety, output, rendering, stpa]
    traces-to: [CC-13]
    mitigates: [H-4]

  # ══════════════════════════════════════════════════════════════════════
  # Cross-Cutting Safety Requirements
  # ══════════════════════════════════════════════════════════════════════

  - id: STPA-REQ-022
    type: requirement
    title: Analysis coverage documentation
    description: >
      Spar must maintain a COMPLIANCE.md documenting which AADL standard
      sections are covered by analyses, which legality rules are implemented,
      and known gaps. This must be updated when new analyses are added.
    status: implemented
    tags: [safety, documentation, stpa]
    traces-to: [SC-1]
    mitigates: [H-1]

  - id: STPA-REQ-023
    type: requirement
    title: Regression test for each closed issue
    description: >
      When a bug or false negative is discovered and fixed, a regression
      test must be added that reproduces the original defect and verifies
      the fix. This prevents re-introduction of known-bad behavior.
    status: implemented
    tags: [safety, testing, stpa]
    traces-to: [SC-1]
    mitigates: [H-1]

  # ══════════════════════════════════════════════════════════════════════
  # Timing and Scheduling Safety Requirements (from UCA-11, CC-10)
  # ══════════════════════════════════════════════════════════════════════

  - id: STPA-REQ-024
    type: requirement
    title: Independent verification — RMA/EDF cross-check
    description: >
      The scheduling analysis must cross-check results between Rate
      Monotonic Analysis (RMA) and Earliest Deadline First (EDF)
      schedulability tests. When a task set is not guaranteed schedulable
      under RMA but would be schedulable under EDF (utilization <= 100%),
      the analysis must report this discrepancy so engineers can consider
      alternative scheduling policies or perform response-time analysis.
    status: implemented
    tags: [safety, scheduling, stpa]
    traces-to: [CC-10]
    mitigates: [H-1]

  - id: STPA-REQ-025
    type: requirement
    title: Sensitivity analysis — timing margin perturbation
    description: >
      The scheduling analysis must perform a sensitivity check by
      perturbing execution times by +10% and checking if the
      schedulability conclusion changes. If nominal utilization passes
      the schedulability bound but perturbed utilization exceeds it,
      the analysis must emit a warning indicating thin timing margins.
    status: implemented
    tags: [safety, scheduling, stpa]
    traces-to: [CC-10]
    mitigates: [H-1]

  - id: STPA-REQ-026
    type: requirement
    title: Explicit Deadline property validation
    description: >
      When a thread has a Period property but no explicit Deadline
      property, the scheduling analysis must emit an info diagnostic
      noting that the implicit deadline equals the period. This
      encourages engineers to explicitly set Deadline for
      constrained-deadline task sets where deadline < period.
    status: implemented
    tags: [safety, scheduling, stpa]
    traces-to: [CC-10]
    mitigates: [H-1]

  - id: STPA-REQ-027
    type: requirement
    title: Execution time range validation
    description: >
      The scheduling analysis must validate Compute_Execution_Time
      ranges: (1) min must not exceed max in a range expression,
      (2) worst-case execution time must not exceed the period.
      Violations produce error diagnostics since they indicate
      specification errors or guaranteed deadline misses.
    status: implemented
    tags: [safety, scheduling, stpa]
    traces-to: [CC-10]
    mitigates: [H-1, H-6]

  - id: STPA-REQ-028
    type: requirement
    title: Multi-processor communication overhead awareness
    description: >
      The latency analysis must detect when an end-to-end flow crosses
      processor boundaries and no inter-processor communication overhead
      property (Transmission_Time or SPAR_Properties::Inter_Processor_Overhead)
      is specified. In such cases, the analysis must emit an info diagnostic
      warning that the latency estimate may understate actual delay.
    status: implemented
    tags: [safety, latency, multi-processor, stpa]
    traces-to: [CC-10]
    mitigates: [H-1]

  - id: STPA-REQ-029
    type: requirement
    title: Clock drift margin advisory
    description: >
      When processor utilization exceeds 80%, the scheduling analysis
      must emit an advisory noting that clock drift between processors
      may cause period jitter that increases effective utilization.
      Engineers should consider adding a timing margin via
      SPAR_Properties::Clock_Drift_Margin.
    status: implemented
    tags: [safety, scheduling, timing, stpa]
    traces-to: [CC-10]
    mitigates: [H-1]

  - id: STPA-REQ-030
    type: requirement
    title: Interrupt and context-switch overhead advisory
    description: >
      When threads are bound to a processor but no Context_Switch_Time
      or Interrupt_Overhead property is set on any thread, the scheduling
      analysis must emit an info diagnostic advising that WCET values
      may underestimate actual execution time if overhead is not already
      included in Compute_Execution_Time.
    status: implemented
    tags: [safety, scheduling, overhead, stpa]
    traces-to: [CC-10]
    mitigates: [H-1]

  - id: STPA-REQ-031
    type: requirement
    title: Shared resource blocking time advisory
    description: >
      When two or more threads share a processor but no Priority or
      Concurrency_Control_Protocol property is set, the scheduling
      analysis must emit an info diagnostic advising that priority
      inversion blocking time should be accounted for in
      Compute_Execution_Time if threads share resources.
    status: implemented
    tags: [safety, scheduling, contention, stpa]
    traces-to: [CC-10]
    mitigates: [H-1]

  # ══════════════════════════════════════════════════════════════════════
  # SysML v2 Lowering Safety Requirements (from UCA-17 to UCA-20, CC-15 to CC-17)
  # ══════════════════════════════════════════════════════════════════════

  - id: STPA-REQ-032
    type: requirement
    title: SysML v2 lowering diagnostic for unhandled constructs
    description: >
      The SysML v2 lower_node function must not silently drop unrecognized
      SyntaxKind variants. The wildcard arm `_ => {}` must be replaced
      with explicit arms for known non-semantic kinds and a catch-all that
      emits a warning diagnostic "unhandled SysML v2 construct: {kind}".
      This mirrors the AADL lowering exhaustiveness (STPA-REQ-004).
    status: not-implemented
    tags: [safety, sysml2, lowering, stpa]
    traces-to: [CC-15]
    mitigates: [H-7]

  - id: STPA-REQ-033
    type: requirement
    title: SysML v2 category inference validation
    description: >
      After SysML v2 lowering, the inferred AADL component category must
      be validated against the features present in the lowered component.
      If a component has thread-like properties (Period, Dispatch_Protocol)
      it must not be classified as system. A test suite must cover all
      category inference paths with at least one test per SysML v2
      construct type (part def, action def, state def, etc.).
    status: not-implemented
    tags: [safety, sysml2, category, stpa]
    traces-to: [CC-16]
    mitigates: [H-7, H-1]

  - id: STPA-REQ-034
    type: requirement
    title: SysML v2 subcomponent category propagation
    description: >
      When lowering SysML v2 part usages and ref usages to AADL
      subcomponents, the subcomponent category must be inferred from
      the referenced type definition's category, not hardcoded to
      ComponentCategory::System. When the referenced type is not
      available, a warning diagnostic must be emitted.
    status: not-implemented
    tags: [safety, sysml2, category, stpa]
    traces-to: [CC-16]
    mitigates: [H-7, H-3]

  - id: STPA-REQ-035
    type: requirement
    title: SysML v2 typed property lowering for numeric constraints
    description: >
      When lowering SysML v2 constraint usages and attribute usages that
      carry numeric values with units (e.g., "10 ms"), the lowering must
      produce typed PropertyExpr values (IntegerLit/RealLit with unit
      annotation), not Opaque strings. Only expressions that genuinely
      cannot be parsed should use PropertyExpr::Opaque.
    status: not-implemented
    tags: [safety, sysml2, properties, stpa]
    traces-to: [CC-17]
    mitigates: [H-7, H-6]

  - id: STPA-REQ-036
    type: requirement
    title: SysML v2 lowering coverage test suite
    description: >
      The SysML v2 lowering test suite must contain at least one test
      for each of the 14+ lowering rules, verifying that the produced
      AADL ItemTree has the correct category, features, subcomponents,
      connections, and property associations. A golden model test must
      verify end-to-end lowering of a non-trivial SysML v2 model.
    status: partial
    tags: [safety, sysml2, testing, stpa]
    traces-to: [CC-15, CC-16]
    mitigates: [H-7]

  # ══════════════════════════════════════════════════════════════════════
  # Verification Pipeline Safety Requirements (from UCA-21, UCA-22, CC-18, CC-19)
  # ══════════════════════════════════════════════════════════════════════

  - id: STPA-REQ-037
    type: requirement
    title: Verification tool availability check
    description: >
      Bazel verification rules (verus_verify, lean_verify) must perform
      an explicit tool availability check before running verification.
      If the tool binary is not found on PATH or at the configured path,
      the rule must fail with a clear error message, not produce a
      cached success artifact. The check must use `which` or equivalent
      and verify the tool version meets minimum requirements.
    status: not-implemented
    tags: [safety, codegen, verification, bazel, stpa]
    traces-to: [CC-18]
    mitigates: [H-8]

  - id: STPA-REQ-038
    type: requirement
    title: Generated BUILD files must include verification targets
    description: >
      The workspace_gen.rs code generator must produce verus_verify
      and/or lean_verify targets in per-crate BUILD.bazel files when
      generating code that includes verification annotations. An
      integration test must verify that generated BUILD.bazel files
      contain at least one verification target per generated crate.
    status: not-implemented
    tags: [safety, codegen, verification, bazel, stpa]
    traces-to: [CC-19]
    mitigates: [H-8]

  - id: STPA-REQ-039
    type: requirement
    title: Verification log content validation
    description: >
      Bazel verification rules must validate that the proof log artifact
      contains actual verification output (not empty or error-only).
      The verus_verify rule must check that the log contains a
      "verification results" summary line. The lean_verify rule must
      check that the log contains "All proofs verified." A log that
      contains only error messages must cause the rule to fail.
    status: not-implemented
    tags: [safety, codegen, verification, bazel, stpa]
    traces-to: [CC-18]
    mitigates: [H-8]

  # ══════════════════════════════════════════════════════════════════════
  # STPA-Sec: Security Requirements (from security.yaml analysis)
  # ══════════════════════════════════════════════════════════════════════

  - id: STPA-SEC-REQ-001
    type: requirement
    title: Language-specific identifier sanitization for generated code
    description: >
      The code generation pipeline must sanitize all model-derived names
      using language-specific rules before interpolation. Rust: reject
      names that are Rust keywords (even after r# prefix handling) and
      validate against Rust identifier grammar. WIT: reject names that
      collide with WIT built-in types (string, list, option, result,
      bool, u8-u64, s8-s64, f32, f64, char). Lean4: reject names that
      collide with Lean4 tactics (simp, omega, exact, apply, intro).
      TOML: escape quotes and special characters in string values.
      Starlark: reject Python/Starlark keywords.
    status: implemented
    tags: [security, codegen, stpa-sec]
    traces-to: [CC-SEC-1]
    mitigates: [H-SEC-1]

  - id: STPA-SEC-REQ-002
    type: requirement
    title: Property value validation before code generation
    description: >
      Before generating code, timing properties must be validated against
      physical plausibility bounds: Period must be in range [1 us, 1 hr],
      WCET must be in range [1 ns, Period], Deadline must be in range
      [WCET, Period]. Properties outside these bounds must produce error
      diagnostics and halt code generation. Default value substitution
      (the current 10ms/1ms fallback) must emit a warning diagnostic
      rather than proceeding silently.
    status: not-implemented
    tags: [security, codegen, stpa-sec]
    traces-to: [CC-SEC-2]
    mitigates: [H-SEC-2]

  - id: STPA-SEC-REQ-003
    type: requirement
    title: Output path confinement for generated files
    description: >
      The codegen pipeline must canonicalize all generated file paths
      and verify that each resolved path is a descendant of the output
      directory. If any generated path would escape the output directory
      (via .., symlinks, or absolute paths), codegen must emit an error
      and skip that file. This check must occur after all path component
      construction, including process name and thread name interpolation.
    status: not-implemented
    tags: [security, codegen, filesystem, stpa-sec]
    traces-to: [CC-SEC-3]
    mitigates: [H-SEC-6]

  - id: STPA-SEC-REQ-004
    type: requirement
    title: SysML v2 lowering diagnostic for unhandled syntax kinds
    description: >
      The wildcard match arm in lower_node (lower.rs) must emit a warning
      diagnostic for any SyntaxKind that is not whitespace, punctuation,
      or a known structural wrapper. The diagnostic must include the
      SyntaxKind name, source offset, and parent context. A golden-file
      test must verify that all semantic SysML v2 constructs produce
      either a lowered AADL item or a diagnostic.
    status: partial
    tags: [security, sysml2, lowering, stpa-sec]
    traces-to: [CC-SEC-4]
    mitigates: [H-SEC-3]

  - id: STPA-SEC-REQ-005
    type: requirement
    title: Exact version pins in generated dependency specifications
    description: >
      Generated Cargo.toml files must use exact version pins (e.g.,
      wit-bindgen = "=0.36.0") instead of semver ranges. Generated
      BUILD.bazel files must reference content-addressed artifacts
      where possible. A Cargo.lock must be generated alongside the
      workspace Cargo.toml. Process names must be checked against a
      reserved list of common crate names (serde, tokio, rand, etc.)
      and must be prefixed with "aadl_" if they collide.
    status: not-implemented
    tags: [security, codegen, supply-chain, stpa-sec]
    traces-to: [CC-SEC-5]
    mitigates: [H-SEC-4]

  - id: STPA-SEC-REQ-006
    type: requirement
    title: Verification coverage scope annotations
    description: >
      Generated Kani harnesses must include a doc comment specifying
      which properties are verified (e.g., "base case: no interference")
      and which are not (e.g., "does NOT verify multi-task interference").
      Generated Lean4 proofs must include a comment block listing
      assumptions. Harness function names must include scope qualifiers
      (e.g., verify_{name}_no_deadline_miss_base_case). The codegen
      must also generate a coverage_manifest.json listing each
      verification artifact and its scope.
    status: not-implemented
    tags: [security, verification, stpa-sec]
    traces-to: [CC-SEC-6]
    mitigates: [H-SEC-5]

  - id: STPA-SEC-REQ-007
    type: requirement
    title: Bazel rules must use argument lists instead of shell interpolation
    description: >
      The verus_verify and wasm_component Bazel rules must be refactored
      to use ctx.actions.run with explicit argument lists instead of
      ctx.actions.run_shell with format string interpolation. Source file
      paths must never be concatenated into shell command strings. If
      run_shell is unavoidable (e.g., for piping), all interpolated paths
      must be shell-quoted using shlex or equivalent escaping.
    status: not-implemented
    tags: [security, build, bazel, stpa-sec]
    traces-to: [CC-SEC-7]
    mitigates: [H-SEC-1, H-SEC-4]

  - id: STPA-SEC-REQ-008
    type: requirement
    title: WASM component provenance verification
    description: >
      The wasm_component Bazel rule must parse cargo build's
      --message-format=json output to extract the exact path of the
      produced .wasm artifact, instead of using find to locate it.
      The rule must verify that the .wasm file was produced by the
      current build invocation (via Bazel's action dependency graph,
      not filesystem timestamps). Content hashing of the core module
      should be logged for audit.
    status: not-implemented
    tags: [security, build, wasm, stpa-sec]
    traces-to: [CC-SEC-8]
    mitigates: [H-SEC-1, H-SEC-2]

  - id: STPA-SEC-REQ-009
    type: requirement
    title: Resource limits on code generation output
    description: >
      The codegen pipeline must enforce configurable limits: maximum
      number of generated files (default: 10,000), maximum total output
      size (default: 100 MB), maximum components per model (default:
      100,000). When a limit is exceeded, codegen must emit an error
      diagnostic and halt. These limits must be configurable via CLI
      flags (--max-files, --max-output-size, --max-components).
    status: not-implemented
    tags: [security, codegen, resource-limits, stpa-sec]
    traces-to: [SC-SEC-6]
    mitigates: [H-SEC-7]

  - id: STPA-SEC-REQ-010
    type: requirement
    title: Generated code compilation verification test
    description: >
      The CI pipeline must include an integration test that runs
      spar codegen on a representative AADL model, then compiles
      all generated Rust code with cargo check (and ideally cargo
      clippy). This test verifies that generated code is syntactically
      valid Rust. A second test must verify that generated WIT files
      pass wasm-tools component wit validation.
    status: partial
    tags: [security, codegen, testing, stpa-sec]
    traces-to: [CC-SEC-1, CC-SEC-2]
    mitigates: [H-SEC-1, H-SEC-2]

  - id: STPA-SEC-REQ-011
    type: requirement
    title: SysML v2 category inference audit logging
    description: >
      The infer_category function must emit an info diagnostic for
      every part def it classifies, stating the inferred category
      and the evidence used (e.g., "part def 'Monitor' classified
      as system: no action/state usages found"). Engineers must be
      able to override the inference via a SysML v2 annotation or
      comment convention (e.g., `/* @aadl-category: thread */`).
    status: not-implemented
    tags: [security, sysml2, lowering, stpa-sec]
    traces-to: [CC-SEC-4]
    mitigates: [H-SEC-3]

  - id: STPA-SEC-REQ-012
    type: requirement
    title: Cross-reference analysis results with proof inputs
    description: >
      When both spar analyze and spar codegen --verify are run on the
      same model, the timing properties used by the analysis engine
      must be compared with the timing constants embedded in generated
      proofs. Any discrepancy (e.g., analysis uses 5ms period but
      proof uses default 10ms) must be reported as an error. This
      cross-reference should be implemented as a post-codegen
      validation step.
    status: not-implemented
    tags: [security, verification, consistency, stpa-sec]
    traces-to: [CC-SEC-2, CC-SEC-6]
    mitigates: [H-SEC-2, H-SEC-5]