Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

10 changes: 6 additions & 4 deletions artifacts/requirements.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -2266,10 +2266,12 @@ artifacts:
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.
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.
status: proposed
tags: [emv2, analysis, safety, hir-def, capability]
fields:
Expand Down
30 changes: 30 additions & 0 deletions artifacts/verification.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -3468,6 +3468,36 @@ artifacts:
- type: verifies
target: REQ-EMV2-PROPAGATION-002

- id: TEST-EMV2-ITEMTREE-ATTACH
type: feature
title: EMV2 subclause retained in the item-tree, attached to its component
description: >
Layer 2 of REQ-EMV2-PROPAGATION-002 (GitHub #294): a component's
`annex EMV2 {** … **}` subclause is no longer dropped at item-tree
lowering (previously the empty ANNEX_SUBCLAUSE arm) — it is lifted via the
L1 Emv2Model and stored in a new `emv2_subclauses` arena, referenced from
`ComponentTypeItem.emv2` / `ComponentImplItem.emv2`
(crates/spar-hir-def/src/item_tree). Oracle tests in spar-hir-def
(parse real AADL → item-tree → assert, NON-CIRCULAR by comparing the
lowered model against L1 parsing the same snippet directly): (a) a system
TYPE with an EMV2 annex retains exactly one subclause whose model EQUALS
the L1 oracle (2 propagations, 3 flows — non-vacuous); (b) a system
IMPLEMENTATION with an EMV2 annex retains it on its own `emv2` list;
(c) a component with an EMV2 annex AND a non-EMV2 annex
(behavior_specification) retains EXACTLY the EMV2 one (guards the
case-insensitive name filter; annex subclauses repeat, so lowering
filters rather than finds). Stops at the item-tree/type level — does NOT
touch instantiation (that is layer 3).
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
Expand Down
2 changes: 2 additions & 0 deletions crates/spar-analysis/src/category_check.rs
Original file line number Diff line number Diff line change
Expand Up @@ -86,6 +86,7 @@ mod tests {
property_associations: Vec::new(),
is_public: true,
requires_modes: false,
emv2: Vec::new(),
});
tree
}
Expand Down Expand Up @@ -120,6 +121,7 @@ mod tests {
property_associations: Vec::new(),
is_public: true,
requires_modes: false,
emv2: Vec::new(),
});
tree
}
Expand Down
21 changes: 21 additions & 0 deletions crates/spar-analysis/src/extends_rules.rs
Original file line number Diff line number Diff line change
Expand Up @@ -302,6 +302,7 @@ mod tests {
property_associations: Vec::new(),
is_public: true,
requires_modes: false,
emv2: Vec::new(),
});

let ext_ct = tree.component_types.alloc(ComponentTypeItem {
Expand All @@ -316,6 +317,7 @@ mod tests {
property_associations: Vec::new(),
is_public: true,
requires_modes: false,
emv2: Vec::new(),
});

tree.packages.alloc(Package {
Expand Down Expand Up @@ -433,6 +435,7 @@ mod tests {
property_associations: Vec::new(),
is_public: true,
requires_modes: false,
emv2: Vec::new(),
});

let ext_ct = tree.component_types.alloc(ComponentTypeItem {
Expand All @@ -447,6 +450,7 @@ mod tests {
property_associations: Vec::new(),
is_public: true,
requires_modes: false,
emv2: Vec::new(),
});

tree.packages.alloc(Package {
Expand Down Expand Up @@ -510,6 +514,7 @@ mod tests {
property_associations: Vec::new(),
is_public: true,
requires_modes: false,
emv2: Vec::new(),
});

let ext_ct = tree.component_types.alloc(ComponentTypeItem {
Expand All @@ -524,6 +529,7 @@ mod tests {
property_associations: Vec::new(),
is_public: true,
requires_modes: false,
emv2: Vec::new(),
});

tree.packages.alloc(Package {
Expand Down Expand Up @@ -588,6 +594,7 @@ mod tests {
property_associations: Vec::new(),
is_public: true,
requires_modes: false,
emv2: Vec::new(),
});

let ext_ct = tree.component_types.alloc(ComponentTypeItem {
Expand All @@ -602,6 +609,7 @@ mod tests {
property_associations: Vec::new(),
is_public: true,
requires_modes: false,
emv2: Vec::new(),
});

tree.packages.alloc(Package {
Expand Down Expand Up @@ -645,6 +653,7 @@ mod tests {
property_associations: Vec::new(),
is_public: true,
requires_modes: false,
emv2: Vec::new(),
});

tree.packages.alloc(Package {
Expand Down Expand Up @@ -692,6 +701,7 @@ mod tests {
property_associations: Vec::new(),
is_public: true,
requires_modes: false,
emv2: Vec::new(),
});

tree.packages.alloc(Package {
Expand Down Expand Up @@ -734,6 +744,7 @@ mod tests {
property_associations: Vec::new(),
is_public: true,
requires_modes: false,
emv2: Vec::new(),
});

tree.packages.alloc(Package {
Expand Down Expand Up @@ -774,6 +785,7 @@ mod tests {
property_associations: Vec::new(),
is_public: true,
requires_modes: false,
emv2: Vec::new(),
});

let ci_idx = tree.component_impls.alloc(ComponentImplItem {
Expand All @@ -792,6 +804,7 @@ mod tests {
property_associations: Vec::new(),
is_public: true,
requires_modes: false,
emv2: Vec::new(),
});

tree.packages.alloc(Package {
Expand Down Expand Up @@ -833,6 +846,7 @@ mod tests {
property_associations: Vec::new(),
is_public: true,
requires_modes: false,
emv2: Vec::new(),
});

let ci_idx = tree.component_impls.alloc(ComponentImplItem {
Expand All @@ -851,6 +865,7 @@ mod tests {
property_associations: Vec::new(),
is_public: true,
requires_modes: false,
emv2: Vec::new(),
});

tree.packages.alloc(Package {
Expand Down Expand Up @@ -893,6 +908,7 @@ mod tests {
property_associations: Vec::new(),
is_public: true,
requires_modes: false,
emv2: Vec::new(),
});

tree.packages.alloc(Package {
Expand Down Expand Up @@ -933,6 +949,7 @@ mod tests {
property_associations: Vec::new(),
is_public: true,
requires_modes: false,
emv2: Vec::new(),
});

tree.packages.alloc(Package {
Expand Down Expand Up @@ -977,6 +994,7 @@ mod tests {
property_associations: Vec::new(),
is_public: true,
requires_modes: false,
emv2: Vec::new(),
});

tree.packages.alloc(Package {
Expand Down Expand Up @@ -1039,6 +1057,7 @@ mod tests {
property_associations: Vec::new(),
is_public: true,
requires_modes: false,
emv2: Vec::new(),
});

let ext_ct = tree.component_types.alloc(ComponentTypeItem {
Expand All @@ -1053,6 +1072,7 @@ mod tests {
property_associations: Vec::new(),
is_public: true,
requires_modes: false,
emv2: Vec::new(),
});

tree.packages.alloc(Package {
Expand Down Expand Up @@ -1096,6 +1116,7 @@ mod tests {
property_associations: Vec::new(),
is_public: true,
requires_modes: false,
emv2: Vec::new(),
});

tree.packages.alloc(Package {
Expand Down
9 changes: 9 additions & 0 deletions crates/spar-analysis/src/legality.rs
Original file line number Diff line number Diff line change
Expand Up @@ -587,6 +587,7 @@ mod tests {
property_associations: Vec::new(),
is_public: true,
requires_modes: false,
emv2: Vec::new(),
});

let ci_idx = tree.component_impls.alloc(ComponentImplItem {
Expand All @@ -605,6 +606,7 @@ mod tests {
property_associations: Vec::new(),
is_public: true,
requires_modes: false,
emv2: Vec::new(),
});

tree.packages.alloc(Package {
Expand Down Expand Up @@ -736,6 +738,7 @@ mod tests {
property_associations: Vec::new(),
is_public: true,
requires_modes: false,
emv2: Vec::new(),
});

tree.packages.alloc(Package {
Expand Down Expand Up @@ -843,6 +846,7 @@ mod tests {
property_associations: Vec::new(),
is_public: true,
requires_modes: false,
emv2: Vec::new(),
});

tree.packages.alloc(Package {
Expand Down Expand Up @@ -990,6 +994,7 @@ mod tests {
property_associations: Vec::new(),
is_public: true,
requires_modes: false,
emv2: Vec::new(),
});
tree.packages.alloc(Package {
name: Name::new("Pkg"),
Expand Down Expand Up @@ -1461,6 +1466,7 @@ mod tests {
property_associations: Vec::new(),
is_public: true,
requires_modes: false,
emv2: Vec::new(),
});

tree.packages.alloc(Package {
Expand Down Expand Up @@ -1545,6 +1551,7 @@ mod tests {
property_associations: Vec::new(),
is_public: true,
requires_modes: false,
emv2: Vec::new(),
});

let ci_idx = tree.component_impls.alloc(ComponentImplItem {
Expand All @@ -1563,6 +1570,7 @@ mod tests {
property_associations: Vec::new(),
is_public: true,
requires_modes: false,
emv2: Vec::new(),
});

tree.packages.alloc(Package {
Expand Down Expand Up @@ -1612,6 +1620,7 @@ mod tests {
property_associations: Vec::new(),
is_public: true,
requires_modes: false,
emv2: Vec::new(),
});

tree.packages.alloc(Package {
Expand Down
8 changes: 8 additions & 0 deletions crates/spar-analysis/src/naming_rules.rs
Original file line number Diff line number Diff line change
Expand Up @@ -325,6 +325,7 @@ mod tests {
property_associations: Vec::new(),
is_public: true,
requires_modes: false,
emv2: Vec::new(),
});

tree.packages.alloc(Package {
Expand Down Expand Up @@ -379,6 +380,7 @@ mod tests {
property_associations: Vec::new(),
is_public: true,
requires_modes: false,
emv2: Vec::new(),
});

tree.packages.alloc(Package {
Expand Down Expand Up @@ -504,6 +506,7 @@ mod tests {
property_associations: Vec::new(),
is_public: true,
requires_modes: false,
emv2: Vec::new(),
});

tree.packages.alloc(Package {
Expand Down Expand Up @@ -552,6 +555,7 @@ mod tests {
property_associations: Vec::new(),
is_public: true,
requires_modes: false,
emv2: Vec::new(),
});

tree.packages.alloc(Package {
Expand Down Expand Up @@ -598,6 +602,7 @@ mod tests {
property_associations: Vec::new(),
is_public: true,
requires_modes: false,
emv2: Vec::new(),
});

tree.packages.alloc(Package {
Expand Down Expand Up @@ -832,6 +837,7 @@ mod tests {
property_associations: Vec::new(),
is_public: true,
requires_modes: false,
emv2: Vec::new(),
});

// Subcomponents
Expand Down Expand Up @@ -882,6 +888,7 @@ mod tests {
property_associations: Vec::new(),
is_public: true,
requires_modes: false,
emv2: Vec::new(),
});

// Property set with unique names
Expand Down Expand Up @@ -1004,6 +1011,7 @@ mod tests {
property_associations: Vec::new(),
is_public: true,
requires_modes: false,
emv2: Vec::new(),
});

tree.packages.alloc(Package {
Expand Down
1 change: 1 addition & 0 deletions crates/spar-hir-def/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@ description = "HIR definitions and name resolution for AADL analysis"
[dependencies]
spar-syntax.workspace = true
spar-base-db.workspace = true
spar-annex.workspace = true
salsa.workspace = true
rowan.workspace = true
la-arena = "0.3"
Expand Down
Loading
Loading