feat(annex): semantic EMV2 model — typed error-propagations projection (REQ-EMV2-PROPAGATION-002, L1/4)

artifacts/requirements.yaml

@@ -2263,6 +2263,13 @@ artifacts:
       work"), re-scoped from v0.21.0 → v0.22.0 and from `bug` to a feature.
       Oracle: the two repro models (relay_transport, bundled OSATE
       network_protocol_pkg) each produce > 0 chains; no-annex model yields 0.
+      LAYER STATUS (4-PR foundation, user-directed v0.23.0 headline
+      2026-07-01): L1 (semantic EMV2 model in spar-annex — Emv2Model lifting
+      the CST into typed propagations/flows) LANDED, verified by
+      TEST-EMV2-SEMANTIC-MODEL; L2 (item-tree attach), L3 (instance
+      projection), L4 (overlay populate + analyze-path wiring + end-to-end
+      > 0-chains oracle) remain. Requirement flips proposed → implemented when
+      L4 closes the end-to-end oracle.
     status: proposed
     tags: [emv2, analysis, safety, hir-def, capability]
     fields:

artifacts/verification.yaml

@@ -3437,6 +3437,37 @@ artifacts:
       - type: satisfies
         target: REQ-EMV2-PROPAGATION-001
 
+  - id: TEST-EMV2-SEMANTIC-MODEL
+    type: feature
+    title: EMV2 semantic model — typed projection of the error-propagations subclause
+    description: >
+      Layer 1 of REQ-EMV2-PROPAGATION-002 (GitHub #294): the semantic model
+      that lifts an EMV2 subclause's flat Rowan CST into typed structs
+      (crates/spar-annex/src/emv2/model.rs — Emv2Model::from_syntax).
+      Oracle tests (parse a real annex body → assert the typed model, NEVER a
+      hand-built struct): (a) in/out propagations carry direction + the
+      declared {TypeSet}; (b) an error SOURCE flow captures its origin point +
+      types; (c) an error SINK flow captures its point; (d) an error PATH
+      captures BOTH the incoming and outgoing points via the landmark walk
+      (points are un-wrapped bare tokens in the grammar); (e) a dotted feature
+      path `bus.access` is recovered whitespace-free; (f) `not` negation is
+      captured; (g) a multi-element {A, B, C} type set yields all three;
+      (h) a VERBATIM block from the bundled OSATE corpus
+      (network_protocol_pkg.aadl) with propagation-KIND points (`bindings`,
+      `connection`) plus a source + sink + path together; (i) a subclause with
+      only error types yields an empty model. This is the parse-driven
+      building block the later layers (item-tree attach, instance projection,
+      overlay population) consume; it does NOT yet reach SystemInstance.
+    fields:
+      method: automated-test
+      steps:
+        - run: cargo test -p spar-annex --lib model
+    status: passing
+    tags: [emv2, analysis, safety, v0.23.0, annex]
+    links:
+      - type: verifies
+        target: REQ-EMV2-PROPAGATION-002
+
   - id: TEST-WRPC-BINDING
     type: feature
     title: wrpc-binding honors per-connection Actual_Connection_Binding

crates/spar-annex/src/emv2/mod.rs

@@ -15,11 +15,13 @@
 
 mod grammar;
 mod lexer;
+pub mod model;
 mod parser;
 pub mod syntax_kind;
 
 use std::mem;
 
+pub use model::{Emv2Model, ErrorFlow, ErrorFlowKind, ErrorPropagation, PropagationDirection};
 pub use syntax_kind::{Emv2Kind, Emv2Language, Emv2SyntaxNode, Emv2SyntaxToken};
 
 use crate::{AnnexDiagnostic, AnnexNode, AnnexParseResult, AnnexParser, Severity, Span};