feat(hir-def): project component EMV2 model onto instances (REQ-EMV2-PROPAGATION-002, L3/4)#315
Merged
Merged
Conversation
Rivet verification gate✅ 20/20 passed
Filter: Failed artifacts(none) Updated automatically by |
Codecov Report❌ Patch coverage is
📢 Thoughts on this report? Let us know! |
…PROPAGATION-002) Layer 3 of 4 for the EMV2 annex→instance foundation (#294). During instantiation, the EMV2 model retained on a component's classifier (L2) is projected onto the corresponding ComponentInstance so a later layer can build the Emv2Overlay (which is keyed by ComponentInstanceIdx). - `SystemInstance` gains a SIDE-TABLE `emv2_models: FxHashMap<ComponentInstanceIdx, Vec<Emv2Model>>` (+ an `emv2_for(idx)` accessor), mirroring the existing property_maps side-tables. Deliberately a side-table rather than a ComponentInstance field: that keeps the ~103 ComponentInstance constructors untouched and pays only the ~56 SystemInstance literals (mostly test fixtures) — the blast-radius lesson from L2. - `Builder::project_emv2(idx, type_loc, impl_loc)` reads `.emv2` off the classifier item(s) and clones `tree.emv2_subclauses[..].model`, UNIONing the component's TYPE and IMPLEMENTATION subclauses (direct only). Called at the two production ComponentInstance alloc sites: the main recursive path (type ∪ impl) and the type-only leaf subcomponent (type only). The anonymous (classifier-less) site projects nothing. - Projection happens AT instantiation time by necessity: `Analysis::analyze` receives only `&SystemInstance`, which holds no back-reference to the item-tree/scope — L4 cannot re-read `.emv2` later. - Extends-chain EMV2 inheritance is DEFERRED (features inherit via collect_type_chain_features; EMV2 intentionally does not yet — flagged in the field doc-comment). Oracle-first, full pipeline (hand-authored AADL → item-tree → instantiate → assert), NON-VACUOUS exact counts (a bare `== item-tree model` would only prove the clone ran): (a) EMV2 on the TYPE, root is the IMPLEMENTATION → root carries it (2 propagations + 1 flow), exercising the main path's type∪impl union; (b) a type-only leaf `sub : device Sensor` carries the device type's model (1 propagation + 1 flow) while the EMV2-less root is empty — the distinct leaf alloc site a main-path-only projection would miss; (c) no annex ⇒ empty. Verified workspace-wide (the L2 lesson): `cargo test --workspace --all-targets --no-run` 0 errors; `cargo clippy --workspace` 0 real warnings (the project_emv2 nested if-let collapsed to a let-chain); spar-hir-def 467 tests pass; fmt clean; mutation on project_emv2 0-missed (2 caught, 2 unviable). Stops at instance projection — no Emv2Overlay, no analysis wiring (that is L4). TEST-EMV2-INSTANCE-PROJECT verifies REQ-EMV2-PROPAGATION-002. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
81244b6 to
7e674a7
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What
Layer 3 of 4 of the EMV2 annex→instance foundation (#294). During instantiation, the EMV2 model retained on a component's classifier (L2) is now projected onto the corresponding
ComponentInstance, so Layer 4 can build theEmv2Overlay(keyed byComponentInstanceIdx).SystemInstancegains a side-tableemv2_models: FxHashMap<ComponentInstanceIdx, Vec<Emv2Model>>+ anemv2_for(idx)accessor, mirroring the existingproperty_mapsside-tables. Deliberately a side-table, not aComponentInstancefield — that keeps ~103ComponentInstanceconstructors untouched and pays only ~56SystemInstanceliterals (mostly test fixtures). (Blast-radius lesson from L2.)Builder::project_emv2(idx, type_loc, impl_loc)clonestree.emv2_subclauses[..].model, unioning the component's TYPE and IMPLEMENTATION subclauses (direct only), called at the two production alloc sites (main recursive path = type∪impl; type-only leaf = type only).Analysis::analyzereceives only&SystemInstance, which has no back-reference to the item-tree — L4 can't re-read.emv2later.Verification
== item-tree modelwould only prove the clone ran): (a) EMV2 on the TYPE, root is the IMPLEMENTATION → root carries it (2 props + 1 flow), exercising the main path's type∪impl union; (b) a type-only leafsub : device Sensorcarries the device type's model (1 prop + 1 flow) while the EMV2-less root is empty — the distinct leaf alloc site a main-path-only projection would miss; (c) no annex ⇒ empty.cargo test --workspace --all-targets --no-run0 errors;cargo clippy --workspace0 real warnings (the nestedif letcollapsed to a let-chain); spar-hir-def 467 tests pass; fmt clean; mutation onproject_emv20-missed (2 caught, 2 unviable).TEST-EMV2-INSTANCE-PROJECTverifiesREQ-EMV2-PROPAGATION-002(umbrella staysproposeduntil L4's end-to-end oracle).Scope
Stops at instance projection — no
Emv2Overlay, no analysis wiring. Layer 4 builds the overlay fromemv2_for+ wiresspar analyze(the end-to-end ">0 propagation chains" oracle that closes #294 and flips the requirement toimplemented).🤖 Generated with Claude Code