Skip to content

feat(hir-def): retain component EMV2 subclause in the item-tree (REQ-EMV2-PROPAGATION-002, L2/4)#314

Merged
avrabe merged 1 commit into
mainfrom
feat/emv2-itemtree-attach
Jul 1, 2026
Merged

feat(hir-def): retain component EMV2 subclause in the item-tree (REQ-EMV2-PROPAGATION-002, L2/4)#314
avrabe merged 1 commit into
mainfrom
feat/emv2-itemtree-attach

Conversation

@avrabe

@avrabe avrabe commented Jul 1, 2026

Copy link
Copy Markdown
Contributor

What

Layer 2 of 4 of the EMV2 annex→instance foundation (#294). A component's annex EMV2 {** … **} subclause was dropped at item-tree lowering (lower_component_type/impl had no ANNEX_SUBCLAUSE handling — the empty arm at lower.rs:169 is the package-section one). This retains it:

  • New Emv2Subclause { name, model: Emv2Model } stored in an emv2_subclauses arena on ItemTree, referenced from ComponentTypeItem.emv2 / ComponentImplItem.emv2 (Vec<Idx> — the idiomatic nested-item slot; the owning classifier is the item, so L3 looks it up by name).
  • lower_emv2_subclauses walks the component's ANNEX_SUBCLAUSE children (they repeat per AS-5506B → filter, not find), recovers the body via the existing spar_annex::extract_annex_content, and reuses L1 (emv2::parseEmv2Model::from_syntax). Non-EMV2 annex languages stay dropped (case-insensitive name filter).
  • spar-hir-def gains a spar-annex dep — already beneath it via spar-base-db, so acyclic; Emv2Model's Debug/Clone/PartialEq/Eq matches the item structs' derives, so no mirror types and no salsa Hash/Update needed.

Scope

Stops at the item-tree/type level. Does not touch instantiation — the diff to instance.rs/resolver.rs is purely mechanical emv2: Vec::new() additions to hand-built test fixtures. Projecting the retained model onto ComponentInstances is Layer 3; building the Emv2Overlay + wiring spar analyze (the end-to-end ">0 chains" oracle) is Layer 4.

Verification

  • Oracle-first, non-circular (3 tests): parse real AADL → item-tree → assert the lowered model equals L1 parsing the same snippet directly (never a hand-built struct). (a) a system TYPE retains one subclause whose model equals the oracle and has exactly 2 propagations + 3 flows (non-vacuous); (b) a system IMPLEMENTATION retains it on its own list; (c) EMV2 + a non-EMV2 annex retains exactly the EMV2 one (guards the filter). Uses the verbatim OSATE-corpus block L1 pins.
  • cargo test -p spar-hir-def464 + 3 pass; clippy + fmt clean.
  • Mutation on lower_emv2_subclauses: 0 missed (3 caught, 1 unviable).
  • Clean-room verify: GO — a cold agent confirmed all 6 claims (retention in both paths, filter-not-find, non-EMV2 dropped, non-circular + non-vacuous oracle, no instantiation overreach, acyclic dep), and mutation-tested the filter to prove the test is non-vacuous.
  • Traceability: TEST-EMV2-ITEMTREE-ATTACH verifies REQ-EMV2-PROPAGATION-002 (umbrella stays proposed until L4's end-to-end oracle).

🤖 Generated with Claude Code

@github-actions

github-actions Bot commented Jul 1, 2026

Copy link
Copy Markdown

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.

…EMV2-PROPAGATION-002)

Layer 2 of 4 for the EMV2 annex→instance foundation (#294). A component's
`annex EMV2 {** … **}` subclause was dropped at item-tree lowering
(lower_component_type/impl had no ANNEX_SUBCLAUSE arm). This lifts it via the
L1 Emv2Model and retains it:

- New `Emv2Subclause { name, model: Emv2Model }` stored in an `emv2_subclauses`
  arena on ItemTree, referenced from `ComponentTypeItem.emv2` /
  `ComponentImplItem.emv2` (Vec<Idx>, the idiomatic nested-item slot — the
  owning classifier IS the item, so L3 looks it up by name).
- `lower_emv2_subclauses` walks the component's ANNEX_SUBCLAUSE children
  (they REPEAT per AS-5506B, so filter not find), recovers the body via the
  existing `spar_annex::extract_annex_content`, and reuses L1
  (`emv2::parse` → `Emv2Model::from_syntax`). Non-EMV2 annex languages stay
  dropped (case-insensitive name filter).
- spar-hir-def gains a spar-annex dep (already beneath it via spar-base-db —
  no cycle); Emv2Model's Debug/Clone/PartialEq/Eq matches the item structs'
  derives, so no mirror types and no salsa Hash/Update needed.
- The new required field is threaded through EVERY workspace producer of these
  HIR structs: spar-hir-def (AADL lowering + test fixtures), spar-sysml2
  (SysML2→HIR lowering), spar-transform (WIT/wac/wrpc/rust-crate generators),
  and spar-analysis test fixtures — all `emv2: Vec::new()` (no EMV2 annex).

Oracle-first, NON-CIRCULAR (3 tests, spar-hir-def): parse real AADL → item-tree
→ assert the lowered model EQUALS L1 parsing the same snippet directly (never a
hand-built struct). (a) a system TYPE retains one subclause whose model equals
the oracle (2 propagations + 3 flows — non-vacuous); (b) a system
IMPLEMENTATION retains it on its own list; (c) EMV2 + a non-EMV2 annex retains
exactly the EMV2 one (guards the filter). Uses the verbatim OSATE-corpus block
L1 pins. Stops at the item-tree level — no instantiation (that is L3).

Verified workspace-wide: `cargo test --workspace --all-targets --no-run` +
`cargo clippy --workspace --all-targets` clean; spar-hir-def 464 + 3 tests
pass; fmt clean; mutation on lower_emv2_subclauses 0-missed. Clean-room GO.
TEST-EMV2-ITEMTREE-ATTACH verifies REQ-EMV2-PROPAGATION-002 (umbrella stays
proposed until L4's end-to-end oracle).

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
@avrabe avrabe force-pushed the feat/emv2-itemtree-attach branch from bcd70b3 to 6a8419b Compare July 1, 2026 16:45
@codecov

codecov Bot commented Jul 1, 2026

Copy link
Copy Markdown

Codecov Report

❌ Patch coverage is 99.40828% with 1 line in your changes missing coverage. Please review.

Files with missing lines Patch % Lines
crates/spar-hir-def/src/item_tree/lower.rs 95.65% 1 Missing ⚠️

📢 Thoughts on this report? Let us know!

@avrabe avrabe merged commit d8f2cf8 into main Jul 1, 2026
19 checks passed
@avrabe avrabe deleted the feat/emv2-itemtree-attach branch July 1, 2026 18:15
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant