friction: emv2_propagation reports 0 chains for all real models — AADL .emv2 annex not ingested into the propagation overlay

[avrabe]

What I was trying to do: Get EMV2 fault-propagation chains to analyse for spar/relay_transport.aadl — the forge/replay/jam link threats reaching the channel's AEAD/anti-replay sinks — to mechanize the STPA-Sec mitigation story (SH-FORGE/SH-STALE/SH-JAM ↔ SSC-AUTH/SSC-FRESH/SSC-JAM) as an AADL fault-propagation counterpart.

Tool + version: Unknown command: --version

What happened: spar analyze always reports

emv2_propagation: EMV2 propagation: 0 chain(s), 0 local flow(s) analysed

for any real AADL model, regardless of how the EMV2 error flows are declared. Root cause is documented in the source — crates/spar-analysis/src/emv2_propagation.rs:128:

// Because EMV2 annex data is not yet integrated into SystemInstance,
// callers supply this overlay when constructing analysis inputs.
// Production code will eventually populate this from the parsed .emv2
// annex subclause; in the interim, tests build it programmatically.

So the AADL annex EMV2 {** ... **} (error source/sink/path + propagation) is parsed for the fault tree and the EMV2→STPA bridge (both work — they report sources/SPFs/hazards), but it is not fed into the Emv2Overlay that compute_error_propagation consumes. On the spar analyze path that overlay is empty, so the propagation analysis is effectively a no-op for real models.

Repro (two independent models, both 0 chains):

# 1. relay's transport model (error sources on the bus)
spar analyze --root Relay_Transport::SecureTransport.Link spar/relay_transport.aadl

# 2. spar's OWN bundled OSATE example, using the canonical bindings/connection
#    bus-binding idiom — also 0 chains:
spar analyze --root network_protocol_pkg::MySystem.basic \
  test-data/interop/osate-examples/LargeExamplesforEMV2TR/network_protocol_pkg.aadl

I also tried moving the sources to port out-propagations (error source frame_out {...} on a port that IS in a semantic connection to the sink port) — still 0 chains, consistent with the overlay never being populated from the annex.

Workaround used: None at the model level — no AADL change can produce chains until the annex→overlay ingestion lands. Relying on the fault tree + EMV2→STPA bridge (which DO read the annex) for the mitigation evidence in the interim.

Impact: emv2_propagation is non-functional for real .aadl input — propagation chains and local flows are always empty. Blocks using AADL fault-propagation to mechanize a documented mitigation story (the relay-transport secure-channel use case, pulseengine/relay#180).