feat(hir-def): project component EMV2 model onto instances (REQ-EMV2-PROPAGATION-002, L3/4)

artifacts/requirements.yaml

@@ -2269,9 +2269,13 @@ artifacts:
       TEST-EMV2-SEMANTIC-MODEL; L2 (item-tree attach — the component's EMV2
       subclause is retained in an emv2_subclauses arena, referenced from
       ComponentType/ImplItem.emv2) LANDED, verified by
-      TEST-EMV2-ITEMTREE-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.
+      TEST-EMV2-ITEMTREE-ATTACH; L3 (instance projection — the classifier's
+      EMV2 model is projected onto each ComponentInstance at instantiation,
+      stored as a SystemInstance emv2_models side-table with an emv2_for
+      accessor) LANDED, verified by TEST-EMV2-INSTANCE-PROJECT; L4 (overlay
+      populate + analyze-path wiring + end-to-end > 0-chains oracle) remains.
+      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

@@ -3498,6 +3498,40 @@ artifacts:
       - type: verifies
         target: REQ-EMV2-PROPAGATION-002
 
+  - id: TEST-EMV2-INSTANCE-PROJECT
+    type: feature
+    title: EMV2 model projected onto ComponentInstances during instantiation
+    description: >
+      Layer 3 of REQ-EMV2-PROPAGATION-002 (GitHub #294): during
+      instantiation the retained EMV2 model (L2) is projected from each
+      component's classifier (type ∪ impl, direct only) onto the
+      ComponentInstance, stored as a SystemInstance side-table
+      `emv2_models: FxHashMap<ComponentInstanceIdx, Vec<Emv2Model>>` (keyed by
+      instance so L4 can build the Emv2Overlay without re-reading the item-tree,
+      which is unreachable post-instantiation) with an `emv2_for(idx)`
+      accessor. Deliberate side-table (not a ComponentInstance field) to avoid
+      breaking ~103 constructors; extends-chain EMV2 inheritance deferred.
+      Oracle tests in spar-hir-def (full pipeline: hand-authored AADL →
+      item-tree → instantiate → assert, NON-VACUOUS exact counts, since a bare
+      `== item-tree model` would only prove the copy ran): (a) EMV2 on the TYPE,
+      root instance is the IMPLEMENTATION — root carries it (2 propagations +
+      1 flow), exercising the main alloc path's type∪impl union; (b) a type-only
+      leaf subcomponent (`sub : device Sensor` with an EMV2 annex) carries the
+      device type's model (1 propagation + 1 flow) while the EMV2-less root is
+      empty — exercising the distinct leaf alloc site a main-path-only
+      projection would miss; (c) no annex ⇒ empty projection. Stops at
+      instance projection — does NOT build the Emv2Overlay or wire analysis
+      passes (that is layer 4).
+    fields:
+      method: automated-test
+      steps:
+        - run: cargo test -p spar-hir-def --lib emv2_
+    status: passing
+    tags: [emv2, analysis, safety, v0.23.0, hir-def]
+    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-analysis/src/ai_ml/tests.rs

@@ -91,6 +91,7 @@ fn single_component_instance(category: ComponentCategory, props: PropertyMap) ->
         property_maps,
         feature_property_maps: Default::default(),
         connection_property_maps: Default::default(),
+        emv2_models: Default::default(),
         semantic_connections: Vec::new(),
         system_operation_modes: Vec::new(),
     }

crates/spar-analysis/src/arinc653.rs

@@ -549,6 +549,7 @@ mod tests {
                 property_maps: self.property_maps,
                 feature_property_maps: Default::default(),
                 connection_property_maps: Default::default(),
+                emv2_models: Default::default(),
                 semantic_connections: Vec::new(),
                 system_operation_modes: Vec::new(),
             }

crates/spar-analysis/src/binding_check.rs

@@ -304,6 +304,7 @@ mod tests {
                 property_maps: self.property_maps,
                 feature_property_maps: Default::default(),
                 connection_property_maps: Default::default(),
+                emv2_models: Default::default(),
                 semantic_connections: Vec::new(),
                 system_operation_modes: Vec::new(),
             }

crates/spar-analysis/src/binding_rules.rs

@@ -277,6 +277,7 @@ mod tests {
                 property_maps: self.property_maps,
                 feature_property_maps: Default::default(),
                 connection_property_maps: Default::default(),
+                emv2_models: Default::default(),
                 semantic_connections: Vec::new(),
                 system_operation_modes: Vec::new(),
             }

crates/spar-analysis/src/bus_bandwidth.rs

@@ -577,6 +577,7 @@ mod tests {
                 property_maps: self.property_maps,
                 feature_property_maps: Default::default(),
                 connection_property_maps: Default::default(),
+                emv2_models: Default::default(),
                 semantic_connections: Vec::new(),
                 system_operation_modes: Vec::new(),
             }
@@ -1328,6 +1329,7 @@ mod tests {
                 property_maps: b.property_maps,
                 feature_property_maps: Default::default(),
                 connection_property_maps: Default::default(),
+                emv2_models: Default::default(),
                 semantic_connections: Vec::new(),
                 system_operation_modes: vec![som],
             }
@@ -1380,6 +1382,7 @@ mod tests {
                 property_maps: b.property_maps,
                 feature_property_maps: Default::default(),
                 connection_property_maps: Default::default(),
+                emv2_models: Default::default(),
                 semantic_connections: Vec::new(),
                 system_operation_modes: vec![som],
             }

crates/spar-analysis/src/classifier_match.rs

@@ -445,6 +445,7 @@ mod tests {
                 property_maps: FxHashMap::default(),
                 feature_property_maps: Default::default(),
                 connection_property_maps: Default::default(),
+                emv2_models: Default::default(),
                 semantic_connections: Vec::new(),
                 system_operation_modes: Vec::new(),
             }

crates/spar-analysis/src/completeness.rs

@@ -226,6 +226,7 @@ mod tests {
                 property_maps: FxHashMap::default(),
                 feature_property_maps: Default::default(),
                 connection_property_maps: Default::default(),
+                emv2_models: Default::default(),
                 semantic_connections: Vec::new(),
                 system_operation_modes: Vec::new(),
             }

crates/spar-analysis/src/connection_rules.rs

@@ -279,6 +279,7 @@ mod tests {
                 property_maps: FxHashMap::default(),
                 feature_property_maps: Default::default(),
                 connection_property_maps: Default::default(),
+                emv2_models: Default::default(),
                 semantic_connections: Vec::new(),
                 system_operation_modes: Vec::new(),
             }

crates/spar-analysis/src/connectivity.rs

@@ -524,6 +524,7 @@ mod tests {
                 property_maps: FxHashMap::default(),
                 feature_property_maps: Default::default(),
                 connection_property_maps: Default::default(),
+                emv2_models: Default::default(),
                 semantic_connections: Vec::new(),
                 system_operation_modes: Vec::new(),
             }

crates/spar-analysis/src/direction_rules.rs

@@ -413,6 +413,7 @@ mod tests {
                 property_maps: FxHashMap::default(),
                 feature_property_maps: Default::default(),
                 connection_property_maps: Default::default(),
+                emv2_models: Default::default(),
                 semantic_connections: Vec::new(),
                 system_operation_modes: Vec::new(),
             }

crates/spar-analysis/src/emv2_analysis.rs

@@ -376,6 +376,7 @@ mod tests {
                 property_maps: self.property_maps,
                 feature_property_maps: Default::default(),
                 connection_property_maps: Default::default(),
+                emv2_models: Default::default(),
                 semantic_connections: Vec::new(),
                 system_operation_modes: Vec::new(),
             }

crates/spar-analysis/src/emv2_propagation.rs

@@ -538,6 +538,7 @@ mod tests {
                 property_maps: self.property_maps,
                 feature_property_maps: Default::default(),
                 connection_property_maps: Default::default(),
+                emv2_models: Default::default(),
                 semantic_connections: self.semantic_connections,
                 system_operation_modes: Vec::new(),
             }

crates/spar-analysis/src/emv2_stpa_bridge.rs

@@ -531,6 +531,7 @@ mod tests {
                 property_maps: self.property_maps,
                 feature_property_maps: Default::default(),
                 connection_property_maps: Default::default(),
+                emv2_models: Default::default(),
                 semantic_connections: Vec::new(),
                 system_operation_modes: Vec::new(),
             }

crates/spar-analysis/src/feature_group_check.rs

@@ -486,6 +486,7 @@ mod tests {
                 property_maps: FxHashMap::default(),
                 feature_property_maps: Default::default(),
                 connection_property_maps: Default::default(),
+                emv2_models: Default::default(),
                 semantic_connections: Vec::new(),
                 system_operation_modes: Vec::new(),
             }

crates/spar-analysis/src/flow_check.rs

@@ -309,6 +309,7 @@ mod tests {
                 property_maps: FxHashMap::default(),
                 feature_property_maps: Default::default(),
                 connection_property_maps: Default::default(),
+                emv2_models: Default::default(),
                 semantic_connections: Vec::new(),
                 system_operation_modes: Vec::new(),
             }

crates/spar-analysis/src/flow_rules.rs

@@ -510,6 +510,7 @@ mod tests {
                 property_maps: FxHashMap::default(),
                 feature_property_maps: Default::default(),
                 connection_property_maps: Default::default(),
+                emv2_models: Default::default(),
                 semantic_connections: Vec::new(),
                 system_operation_modes: Vec::new(),
             }

crates/spar-analysis/src/hierarchy.rs

@@ -230,6 +230,7 @@ mod tests {
                 property_maps: FxHashMap::default(),
                 feature_property_maps: Default::default(),
                 connection_property_maps: Default::default(),
+                emv2_models: Default::default(),
                 semantic_connections: Vec::new(),
                 system_operation_modes: Vec::new(),
             }

crates/spar-analysis/src/latency.rs

@@ -616,6 +616,7 @@ mod tests {
                 property_maps: self.property_maps,
                 feature_property_maps: Default::default(),
                 connection_property_maps: Default::default(),
+                emv2_models: Default::default(),
                 semantic_connections: Vec::new(),
                 system_operation_modes: Vec::new(),
             }

crates/spar-analysis/src/legality.rs

@@ -547,6 +547,7 @@ mod tests {
                 property_maps: FxHashMap::default(),
                 feature_property_maps: Default::default(),
                 connection_property_maps: Default::default(),
+                emv2_models: Default::default(),
                 semantic_connections: Vec::new(),
                 system_operation_modes: Vec::new(),
             }

crates/spar-analysis/src/memory_budget.rs

@@ -250,6 +250,7 @@ mod tests {
                 property_maps: self.property_maps,
                 feature_property_maps: Default::default(),
                 connection_property_maps: Default::default(),
+                emv2_models: Default::default(),
                 semantic_connections: Vec::new(),
                 system_operation_modes: Vec::new(),
             }

crates/spar-analysis/src/modal.rs

@@ -159,6 +159,7 @@ mod tests {
             property_maps: FxHashMap::default(),
             feature_property_maps: Default::default(),
             connection_property_maps: Default::default(),
+            emv2_models: Default::default(),
             semantic_connections: Vec::new(),
             system_operation_modes: soms,
         }

crates/spar-analysis/src/modal_rules.rs

@@ -335,6 +335,7 @@ mod tests {
                 property_maps: FxHashMap::default(),
                 feature_property_maps: Default::default(),
                 connection_property_maps: Default::default(),
+                emv2_models: Default::default(),
                 semantic_connections: Vec::new(),
                 system_operation_modes: Vec::new(),
             }

crates/spar-analysis/src/mode_check.rs

@@ -291,6 +291,7 @@ mod tests {
                 property_maps: FxHashMap::default(),
                 feature_property_maps: Default::default(),
                 connection_property_maps: Default::default(),
+                emv2_models: Default::default(),
                 semantic_connections: Vec::new(),
                 system_operation_modes: Vec::new(),
             }

crates/spar-analysis/src/mode_reachability.rs

@@ -703,6 +703,7 @@ mod tests {
                 property_maps: FxHashMap::default(),
                 feature_property_maps: Default::default(),
                 connection_property_maps: Default::default(),
+                emv2_models: Default::default(),
                 semantic_connections: Vec::new(),
                 system_operation_modes: Vec::new(),
             }

crates/spar-analysis/src/mode_rules.rs

@@ -248,6 +248,7 @@ mod tests {
                 property_maps: FxHashMap::default(),
                 feature_property_maps: Default::default(),
                 connection_property_maps: Default::default(),
+                emv2_models: Default::default(),
                 semantic_connections: Vec::new(),
                 system_operation_modes: Vec::new(),
             }

crates/spar-analysis/src/property_rules.rs

@@ -446,6 +446,7 @@ mod tests {
                 property_maps: self.property_maps,
                 feature_property_maps: Default::default(),
                 connection_property_maps: Default::default(),
+                emv2_models: Default::default(),
                 semantic_connections: Vec::new(),
                 system_operation_modes: Vec::new(),
             }

crates/spar-analysis/src/regression_tests.rs

@@ -121,6 +121,7 @@ impl TestInstanceBuilder {
             property_maps: self.property_maps,
             feature_property_maps: Default::default(),
             connection_property_maps: Default::default(),
+            emv2_models: Default::default(),
             semantic_connections: Vec::new(),
             system_operation_modes: Vec::new(),
         }

crates/spar-analysis/src/resource_budget.rs

@@ -372,6 +372,7 @@ mod tests {
                 property_maps: self.property_maps,
                 feature_property_maps: Default::default(),
                 connection_property_maps: Default::default(),
+                emv2_models: Default::default(),
                 semantic_connections: Vec::new(),
                 system_operation_modes: Vec::new(),
             }

crates/spar-analysis/src/rta.rs

@@ -738,6 +738,7 @@ mod tests {
                 property_maps: self.property_maps,
                 feature_property_maps: Default::default(),
                 connection_property_maps: Default::default(),
+                emv2_models: Default::default(),
                 semantic_connections: Vec::new(),
                 system_operation_modes: Vec::new(),
             }

crates/spar-analysis/src/scheduling.rs

@@ -626,6 +626,7 @@ mod tests {
                 property_maps: self.property_maps,
                 feature_property_maps: Default::default(),
                 connection_property_maps: Default::default(),
+                emv2_models: Default::default(),
                 semantic_connections: Vec::new(),
                 system_operation_modes: Vec::new(),
             }

crates/spar-analysis/src/subcomponent_rules.rs

@@ -240,6 +240,7 @@ mod tests {
                 property_maps: FxHashMap::default(),
                 feature_property_maps: Default::default(),
                 connection_property_maps: Default::default(),
+                emv2_models: Default::default(),
                 semantic_connections: Vec::new(),
                 system_operation_modes: Vec::new(),
             }

crates/spar-analysis/src/tests.rs

@@ -174,6 +174,7 @@ impl TestInstanceBuilder {
             property_maps: self.property_maps,
             feature_property_maps: Default::default(),
             connection_property_maps: Default::default(),
+            emv2_models: Default::default(),
             semantic_connections: Vec::new(),
             system_operation_modes: Vec::new(),
         }

crates/spar-analysis/src/weight_power.rs

@@ -544,6 +544,7 @@ mod tests {
                 property_maps: self.property_maps,
                 feature_property_maps: Default::default(),
                 connection_property_maps: Default::default(),
+                emv2_models: Default::default(),
                 semantic_connections: Vec::new(),
                 system_operation_modes: Vec::new(),
             }
@@ -1244,6 +1245,7 @@ mod tests {
                 property_maps: b.property_maps,
                 feature_property_maps: Default::default(),
                 connection_property_maps: Default::default(),
+                emv2_models: Default::default(),
                 semantic_connections: Vec::new(),
                 system_operation_modes: vec![som],
             }
@@ -1323,6 +1325,7 @@ mod tests {
                 property_maps: b.property_maps,
                 feature_property_maps: Default::default(),
                 connection_property_maps: Default::default(),
+                emv2_models: Default::default(),
                 semantic_connections: Vec::new(),
                 system_operation_modes: vec![som],
             }

crates/spar-analysis/src/wrpc_binding.rs

@@ -381,6 +381,7 @@ mod tests {
                 property_maps: self.property_maps,
                 feature_property_maps: Default::default(),
                 connection_property_maps: self.connection_property_maps,
+                emv2_models: Default::default(),
                 semantic_connections: Vec::new(),
                 system_operation_modes: Vec::new(),
             }

crates/spar-cli/src/assertion/mod.rs

@@ -550,6 +550,7 @@ mod tests {
             property_maps,
             feature_property_maps: Default::default(),
             connection_property_maps: Default::default(),
+            emv2_models: Default::default(),
             semantic_connections: Vec::new(),
             system_operation_modes: Vec::new(),
         }
@@ -838,6 +839,7 @@ mod tests {
             property_maps: FxHashMap::default(),
             feature_property_maps: Default::default(),
             connection_property_maps: Default::default(),
+            emv2_models: Default::default(),
             semantic_connections: Vec::new(),
             system_operation_modes: Vec::new(),
         };

crates/spar-cli/src/diff.rs

@@ -935,6 +935,7 @@ mod tests {
                     property_maps: self.property_maps,
                     feature_property_maps: Default::default(),
                     connection_property_maps: Default::default(),
+                    emv2_models: Default::default(),
                     semantic_connections: Vec::new(),
                     system_operation_modes: Vec::new(),
                 }