Skip to content

feat(emv2): error-propagation traversal across AADL connection graph (v0.10.x)#225

Merged
avrabe merged 6 commits into
mainfrom
feat/v0.10.x-emv2-propagation
May 17, 2026
Merged

feat(emv2): error-propagation traversal across AADL connection graph (v0.10.x)#225
avrabe merged 6 commits into
mainfrom
feat/v0.10.x-emv2-propagation

Conversation

@avrabe
Copy link
Copy Markdown
Contributor

@avrabe avrabe commented May 14, 2026

Summary

  • Closes the single biggest gap vs OSATE/HAMR: EMV2 error-propagation traversal now walks the AADL semantic connection graph to compute which downstream components inherit each declared error type (structural fault tree + cut sets were already present)
  • New emv2_propagation.rs module: Emv2Overlay carries in/out propagation and flow declarations; compute_error_propagation returns ErrorPropagationReport with chains, local flows, and diagnostics; analysis only, no codegen
  • Wired into register_all / register_all_except_wctt; adds REQ-EMV2-PROPAGATION-001 + TEST-EMV2-PROPAGATION to artifact YAML files

Example chain from test fixture

Single-hop test (emv2_propagation_single_hop): component sensor (Device) declares out propagation { BadValue }, component controller (Process) declares in propagation { BadValue }, one semantic connection between them. Result:

ErrorPropagationChain {
    origin: sensor,
    error_type: "BadValue",
    downstream: [controller],
    via_connections: [c_0_1],
}

Test plan

  • cargo test -p spar-analysis emv2_propagation — 6 tests pass (single-hop, 3-hop chain, cycle detection, path-flow isolation, case-insensitive match, no-connection baseline)
  • cargo clippy -p spar-analysis -- -D warnings — clean
  • cargo fmt --check — clean
  • rivet validate — YAML parse error at line 1615 of verification.yaml is pre-existing (confirmed against main), not introduced by this PR

🤖 Generated with Claude Code

…(v0.10.x)

Introduces emv2_propagation.rs — a new analysis module that walks the
semantic connection graph to compute which downstream components inherit
each declared error type.  The Emv2Overlay carries in/out propagation and
flow declarations (not yet integrated into SystemInstance); compute_error_
propagation returns ErrorPropagationReport with chains, local_flows, and
diagnostics.  Cycle detection tracks (component, error_type) pairs.  6 unit
tests cover single-hop, 3-hop chain, cycle, path-flow isolation, case-
insensitive matching, and no-connection baseline.  Wired into register_all /
register_all_except_wctt.  Adds REQ-EMV2-PROPAGATION-001 + TEST-EMV2-
PROPAGATION to artifact YAML files.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
@avrabe avrabe enabled auto-merge (squash) May 14, 2026 17:19
avrabe and others added 2 commits May 15, 2026 12:12
Two surgical fixes surfaced by the gate after smithy resumed:

1. crates/spar-analysis/src/emv2_propagation.rs:487 — clippy
   `let_and_return`: dropped the bound `idx` and returned `alloc(...)`
   directly. Pure refactor, no behavior change.
2. crates/spar-analysis/src/tests.rs:1640 — `test_register_all_count`
   expected 30 passes; the new emv2_propagation pass makes it 31.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
# Conflicts:
#	artifacts/requirements.yaml
#	artifacts/verification.yaml
@github-actions
Copy link
Copy Markdown

github-actions Bot commented May 15, 2026

Rivet verification gate

17/17 passed

count
Passed 17
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.

@codecov
Copy link
Copy Markdown

codecov Bot commented May 16, 2026

Codecov Report

❌ Patch coverage is 98.08612% with 8 lines in your changes missing coverage. Please review.

Files with missing lines Patch % Lines
crates/spar-analysis/src/emv2_propagation.rs 98.31% 7 Missing ⚠️
crates/spar-analysis/src/lib.rs 50.00% 1 Missing ⚠️

📢 Thoughts on this report? Let us know!

@avrabe avrabe merged commit 3323fe5 into main May 17, 2026
17 of 18 checks passed
@avrabe avrabe deleted the feat/v0.10.x-emv2-propagation branch May 17, 2026 02:09
avrabe added a commit that referenced this pull request May 20, 2026
v0.10.0 ships:

**Mermaid emission (M1 + M2 + M3)**
- spar-mermaid foundation crate with `emit_flowchart` (#220)
- `spar emit --format mermaid` CLI subcommand (#222)
- `emit_class_diagram` + `emit_requirement_diagram` + matching CLI
  flags `--format mermaid-class` / `mermaid-req` (#228)

**Soundness deepening**
- Lean 4 sorry-free proofs of end-to-end latency monotonicity and
  ARINC 653 partition isolation, alongside the pre-existing RTA / EDF /
  Network Calculus proofs (#223)
- Kani BMC harnesses on generated-code AADL contract preservation
  (thread Period, port Direction, bus access right) — spar's
  Logika-equivalent strategy for verified codegen (#224)

**Safety analysis**
- EMV2 error-propagation traversal across the AADL connection graph
  (closes the #1 gap vs OSATE/HAMR in safety-case reviews) (#225)

**Verification infrastructure**
- Rivet-driven verification gate that executes every artifact's
  `fields.steps[].run` commands and posts a sticky PR comment with
  pass/fail counts and failed artifact IDs (#221)
- Workflow tuning: gate timeout 30→60 min for future Mathlib-heavy
  workloads; TEST-PROOF-* stay on sorry-grep until lake cache lands
  (#227, #229, #230)

**Chore**
- Pruned stale dev artifacts (.playwright-mcp logs + dashboard-render
  PNGs) and tightened gitignore (#226)

Bumps Cargo.toml + vscode-spar/package.json from 0.9.3 → 0.10.0.
The release workflow's `check-versions` job enforces tag/Cargo/vsix
agreement, so these must move together with the v0.10.0 tag push.

Co-authored-by: Claude Opus 4.7 <noreply@anthropic.com>
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