Skip to content

Commit e39f065

Browse files
avrabeclaude
andauthored
feat(insight): spar-insight crate + Tier 1 CTF discrepancy detection (Track G v0.9.0) (#178)
New crate spar-insight: ingests Zephyr CTF traces (Tier 1 of the Gale tracing strategy from project memory), extracts per-probe-point timing distributions, and compares to Spar_Trace::Expected_BCET/WCET/Mean declarations from v0.7.0 Track A. Rules-based discrepancy detection: - WcetViolated (Error): observed.max > Expected_WCET - BcetUnderestimated (Warn): observed.min < Expected_BCET - MeanDrift (Info): |observed.mean - Expected_Mean| > 20% - MissingProbe (Info): trace has data for an undeclared probe - UnobservedProbe (Warn): model declares Expected_* with no trace data Formal-statistics foundation (Hoeffding etc.) is deferred per project memory's R3 proof-assistant deferral. CLI: spar insight verify-trace --root Pkg::Sys.Impl --trace trace.ctf model.aadl New requirements: REQ-INSIGHT-{001,002}. Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent 0eb41b5 commit e39f065

15 files changed

Lines changed: 1616 additions & 1 deletion

File tree

Cargo.lock

Lines changed: 13 additions & 0 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

Cargo.toml

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -19,6 +19,7 @@ members = [
1919
"crates/spar-verify-macros",
2020
"crates/spar-verify",
2121
"crates/spar-wasm",
22+
"crates/spar-insight",
2223
]
2324

2425
[workspace.package]
@@ -42,6 +43,7 @@ spar-sysml2 = { path = "crates/spar-sysml2" }
4243
spar-transform = { path = "crates/spar-transform" }
4344
spar-variants = { path = "crates/spar-variants" }
4445
spar-codegen = { path = "crates/spar-codegen" }
46+
spar-insight = { path = "crates/spar-insight" }
4547
rowan = "0.16"
4648
salsa = "0.26"
4749
la-arena = "0.3"

artifacts/requirements.yaml

Lines changed: 36 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1459,4 +1459,40 @@ artifacts:
14591459
status: planned
14601460
tags: [network, tsn, wctt, v081]
14611461

1462+
# ── Track G: spar-insight discrepancy assistant (v0.9.0) ──────────
1463+
1464+
- id: REQ-INSIGHT-001
1465+
type: requirement
1466+
title: Tier 1 CTF ingestion + per-probe timing distributions
1467+
description: >
1468+
spar-insight ingests Tier 1 CTF traces from Zephyr (`k_sem_give`,
1469+
`k_sem_take`, `k_timer_expiry` plus `probe_point_enter` /
1470+
`probe_point_exit` markers) and produces a per-probe-point timing
1471+
distribution (min / max / mean over the observed
1472+
enter→exit durations) comparable to the
1473+
`Spar_Trace::Expected_BCET` / `Expected_WCET` / `Expected_Mean`
1474+
predictions declared on AADL components. Tier 1 of the Gale
1475+
tracing strategy in the project memory; full binary CTF +
1476+
babeltrace2 ingestion is a v0.9.x follow-up.
1477+
status: implemented
1478+
tags: [insight, trace, ctf, tier1, v090]
1479+
1480+
- id: REQ-INSIGHT-002
1481+
type: requirement
1482+
title: Rules-based discrepancy detection (5 kinds)
1483+
description: >
1484+
Rules-based discrepancy detection emits structured diagnostics
1485+
keyed by probe id: `WcetViolated` (Error,
1486+
observed.max > Expected_WCET), `BcetUnderestimated` (Warn,
1487+
observed.min < Expected_BCET), `MeanDrift` (Info,
1488+
|observed.mean − Expected_Mean| > 20% of Expected_Mean),
1489+
`MissingProbe` (Info, trace samples for an undeclared probe),
1490+
and `UnobservedProbe` (Warn, declared `Expected_*` with no trace
1491+
samples). Wired into the CLI as
1492+
`spar insight verify-trace --root Pkg::Sys.Impl --trace trace.ctf
1493+
model.aadl`. The formal-statistics layer (Hoeffding bounds, etc.)
1494+
is deferred per project memory's R3 proof-assistant deferral.
1495+
status: implemented
1496+
tags: [insight, trace, cli, v090]
1497+
14621498
# Research findings tracked separately in research/findings.yaml

artifacts/verification.yaml

Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1923,3 +1923,32 @@ artifacts:
19231923
target: REQ-TSN-001
19241924
- type: satisfies
19251925
target: REQ-NETWORK-001
1926+
1927+
- id: TEST-INSIGHT-DISCREPANCY
1928+
type: feature
1929+
title: spar-insight CTF parser + 5-kind discrepancy detection
1930+
description: >
1931+
Unit + integration tests in crates/spar-insight covering Tier 1
1932+
CTF text parsing (timestamp / event-name / payload, blank +
1933+
comment lines, malformed-line rejection), Zephyr event
1934+
classification (`k_sem_give`, `k_sem_take`, `k_timer_expiry`,
1935+
`probe_point_enter` / `probe_point_exit`, fallthrough to
1936+
`Custom`), enter/exit pairing for per-probe timing extraction
1937+
(clean pairing, orphan dropping, independent probes), and the
1938+
rules-based discrepancy detector (`WcetViolated`,
1939+
`BcetUnderestimated`, `MeanDrift`, `UnobservedProbe`,
1940+
`MissingProbe`) end-to-end against an instantiated
1941+
`SystemInstance` whose Brake.Impl declares
1942+
`Spar_Trace::Expected_BCET / Expected_WCET / Expected_Mean`.
1943+
Also exercises `DiscrepancyReport::to_json` / `to_text`.
1944+
fields:
1945+
method: automated-test
1946+
steps:
1947+
- run: cargo test -p spar-insight
1948+
status: passing
1949+
tags: [v0.9.0, insight, trace, ctf, tier1]
1950+
links:
1951+
- type: satisfies
1952+
target: REQ-INSIGHT-001
1953+
- type: satisfies
1954+
target: REQ-INSIGHT-002

crates/spar-cli/Cargo.toml

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,7 @@ spar-solver.workspace = true
2323
spar-render.workspace = true
2424
spar-codegen.workspace = true
2525
spar-variants.workspace = true
26+
spar-insight.workspace = true
2627
etch.workspace = true
2728
la-arena.workspace = true
2829
rowan.workspace = true

crates/spar-cli/src/insight.rs

Lines changed: 141 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,141 @@
1+
//! `spar insight verify-trace` subcommand — Track G v0.9.0.
2+
//!
3+
//! Wraps `spar_insight::analyze` over a parsed AADL model + a textual
4+
//! Zephyr CTF trace and prints the [`DiscrepancyReport`] as JSON
5+
//! (default) or text.
6+
7+
use std::fs;
8+
use std::process;
9+
10+
use spar_hir_def::instance::SystemInstance;
11+
use spar_hir_def::{GlobalScope, HirDefDatabase, Name, file_item_tree};
12+
use spar_insight::{analyze, parse_ctf};
13+
14+
use crate::parse_root_ref;
15+
16+
pub fn cmd_insight(args: &[String]) {
17+
if args.is_empty() {
18+
eprintln!("Usage: spar insight <subcommand> [options] <file...>");
19+
eprintln!();
20+
eprintln!("Subcommands:");
21+
eprintln!(
22+
" verify-trace --root Pkg::Type.Impl --trace trace.ctf [--format text|json] <file...>"
23+
);
24+
process::exit(1);
25+
}
26+
match args[0].as_str() {
27+
"verify-trace" => cmd_verify_trace(&args[1..]),
28+
other => {
29+
eprintln!("Unknown insight subcommand: {other}");
30+
process::exit(1);
31+
}
32+
}
33+
}
34+
35+
fn cmd_verify_trace(args: &[String]) {
36+
let mut root: Option<String> = None;
37+
let mut trace_path: Option<String> = None;
38+
let mut format: Option<String> = None;
39+
let mut files: Vec<String> = Vec::new();
40+
41+
let mut i = 0;
42+
while i < args.len() {
43+
match args[i].as_str() {
44+
"--root" => {
45+
i += 1;
46+
if i >= args.len() {
47+
eprintln!("--root requires a value (Package::Type.Impl)");
48+
process::exit(1);
49+
}
50+
root = Some(args[i].clone());
51+
}
52+
"--trace" => {
53+
i += 1;
54+
if i >= args.len() {
55+
eprintln!("--trace requires a path");
56+
process::exit(1);
57+
}
58+
trace_path = Some(args[i].clone());
59+
}
60+
"--format" => {
61+
i += 1;
62+
if i >= args.len() {
63+
eprintln!("--format requires a value (text|json)");
64+
process::exit(1);
65+
}
66+
format = Some(args[i].clone());
67+
}
68+
s if s.starts_with('-') => {
69+
eprintln!("Unknown option: {s}");
70+
process::exit(1);
71+
}
72+
s => files.push(s.to_string()),
73+
}
74+
i += 1;
75+
}
76+
77+
let root = root.unwrap_or_else(|| {
78+
eprintln!("--root Package::Type.Impl is required");
79+
process::exit(1);
80+
});
81+
let trace_path = trace_path.unwrap_or_else(|| {
82+
eprintln!("--trace <path> is required");
83+
process::exit(1);
84+
});
85+
if files.is_empty() {
86+
eprintln!("Missing AADL file argument(s)");
87+
process::exit(1);
88+
}
89+
90+
let (pkg_name, type_name, impl_name) = parse_root_ref(&root);
91+
92+
let db = HirDefDatabase::default();
93+
let mut trees = Vec::new();
94+
for file_path in &files {
95+
let source = fs::read_to_string(file_path).unwrap_or_else(|e| {
96+
eprintln!("Cannot read {file_path}: {e}");
97+
process::exit(1);
98+
});
99+
let parsed = spar_syntax::parse(&source);
100+
if !parsed.ok() {
101+
for err in parsed.errors() {
102+
let (line, col) = spar_base_db::offset_to_line_col(&source, err.offset);
103+
eprintln!("{file_path}:{line}:{col}: {}", err.msg);
104+
}
105+
eprintln!("Cannot verify-trace: parse errors in {file_path}");
106+
process::exit(1);
107+
}
108+
let sf = spar_base_db::SourceFile::new(&db, file_path.clone(), source);
109+
trees.push(file_item_tree(&db, sf));
110+
}
111+
let scope = GlobalScope::from_trees(trees);
112+
let instance = SystemInstance::instantiate(
113+
&scope,
114+
&Name::new(&pkg_name),
115+
&Name::new(&type_name),
116+
&Name::new(&impl_name),
117+
);
118+
119+
let trace_src = fs::read_to_string(&trace_path).unwrap_or_else(|e| {
120+
eprintln!("Cannot read trace {trace_path}: {e}");
121+
process::exit(1);
122+
});
123+
let events = match parse_ctf(&trace_src) {
124+
Ok(e) => e,
125+
Err(e) => {
126+
eprintln!("Cannot parse trace {trace_path}: {e}");
127+
process::exit(1);
128+
}
129+
};
130+
131+
let report = analyze(&events, &instance);
132+
let want_text = format.as_deref() == Some("text");
133+
if want_text {
134+
print!("{}", report.to_text());
135+
} else {
136+
println!("{}", report.to_json());
137+
}
138+
if report.has_errors() {
139+
process::exit(1);
140+
}
141+
}

crates/spar-cli/src/main.rs

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
mod assertion;
22
mod diff;
3+
mod insight;
34
mod lsp;
45
mod moves;
56
mod refactor;
@@ -44,6 +45,7 @@ fn main() {
4445
"generate" => cmd_sysml2_generate(&args[2..]),
4546
"lsp" => cmd_lsp(),
4647
"moves" => moves::cmd_moves_dispatch(&args[2..]),
48+
"insight" => insight::cmd_insight(&args[2..]),
4749
other => {
4850
eprintln!("Unknown command: {other}");
4951
process::exit(1);
@@ -68,6 +70,7 @@ fn print_usage() {
6870
eprintln!(
6971
" moves Hypothetical-rebinding oracle (verify a move under the migration overlay)"
7072
);
73+
eprintln!(" insight Discrepancy assistant: compare CTF traces to Expected_BCET/WCET/Mean");
7174
eprintln!(" lsp Start Language Server Protocol server (stdin/stdout)");
7275
eprintln!();
7376
eprintln!("Options:");
@@ -95,6 +98,9 @@ fn print_usage() {
9598
eprintln!(
9699
" moves enumerate --root Package::Type.Impl --component <fqn> [--target-filter <s>] [--format text|json] <file...>"
97100
);
101+
eprintln!(
102+
" insight verify-trace --root Package::Type.Impl --trace trace.ctf [--format text|json] <file...>"
103+
);
98104
}
99105

100106
fn cmd_lsp() {
@@ -1680,7 +1686,7 @@ fn is_safe_generated_path(path: &str) -> bool {
16801686
&& !path.starts_with('\\')
16811687
}
16821688

1683-
fn parse_root_ref(s: &str) -> (String, String, String) {
1689+
pub(crate) fn parse_root_ref(s: &str) -> (String, String, String) {
16841690
// Expected format: Package::Type.Impl
16851691
let parts: Vec<&str> = s.splitn(2, "::").collect();
16861692
if parts.len() != 2 {

crates/spar-insight/Cargo.toml

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
[package]
2+
name = "spar-insight"
3+
version.workspace = true
4+
edition.workspace = true
5+
license.workspace = true
6+
repository.workspace = true
7+
description = "Statistical-discrepancy assistant: compares observed CTF timing traces to spar's Expected_BCET/WCET/Mean model predictions"
8+
9+
[dependencies]
10+
serde = { workspace = true, features = ["derive"] }
11+
serde_json = { workspace = true }
12+
spar-hir-def.workspace = true
13+
14+
[dev-dependencies]
15+
pretty_assertions = "1"
16+
spar-syntax.workspace = true
17+
spar-base-db.workspace = true

0 commit comments

Comments
 (0)