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

[avrabe]

What

Layer 1 of 4 for the EMV2 annex→instance integration foundation (#294, REQ-EMV2-PROPAGATION-002 — the user-directed v0.23 headline). The EMV2 parser already produces a lossless Rowan CST, but downstream fault-propagation analysis (the Emv2Overlay, empty today → "0 chains" for every real model) needs a semantic view. This adds crates/spar-annex/src/emv2/model.rs: Emv2Model::from_syntax lifting the CST into typed structs — ErrorPropagation (feature/kind, direction, negation, type set) and ErrorFlow (source/sink/path with incoming + outgoing points and types).

Scope correction (from the umbrella requirement)

#294's premise — that the fault tree and STPA bridge already read the annex — is false: those passes emit structural output and hardcode "ServiceFailure". The annex is parsed but dropped at item-tree lowering and never threaded through instantiation. This is a 4-layer foundation; this PR is layer 1 (the parse-driven semantic model), and does not yet reach SystemInstance (layers 2–4: item-tree attach → instance projection → overlay populate + analyze-path wiring + end-to-end >0-chains oracle).

Oracle-first

12 tests parse real annex bodies → assert the typed model (never a hand-built struct — the exact circularity that hides the bug today). Includes a verbatim block from the bundled OSATE corpus (network_protocol_pkg.aadl) with propagation-kind points (bindings, connection) plus a source + sink + path together, and targeted cases for the landmark-walk edges (bare source stops at ;, when guard ends the point, a path's outgoing type set doesn't leak into the flow's incoming error_types).

Handles the grammar asymmetry: ERROR_PROPAGATION wraps its port in a FEATURE_OR_PP_REF node, but flow propagation-points are bare token sequences recovered by a landmark-driven walk (flow keyword → incoming point, -> → outgoing, {/when/if/; → end).

Verification

• cargo test -p spar-annex --lib model → 12 pass; clippy + fmt clean.
• Mutation (full-file): 0-missed except one documented equivalent survivor (k == IDENT && name.is_empty() — a flow's first token is always its name IDENT, so &&/|| never diverge on reachable input).
• Traceability: TEST-EMV2-SEMANTIC-MODEL verifies REQ-EMV2-PROPAGATION-002.

🤖 Generated with Claude Code

[github-actions]

Rivet verification gate

✅ 20/20 passed

	count
Passed	20
Failed	0
Skipped (no steps)	0

Filter: (and (= type "feature") (or (has-tag "v093") (has-tag "v0100")))

Failed artifacts

(none)

_{Updated automatically by tools/post_verification_comment.py. Source of truth: artifacts/verification.yaml.}

[codecov]

Codecov Report

❌ Patch coverage is 99.36508% with 2 lines in your changes missing coverage. Please review.

Files with missing lines	Patch %	Lines
crates/spar-annex/src/emv2/model.rs	99.36%	2 Missing ⚠️

📢 Thoughts on this report? Let us know!