From 2f10141fc049f35dd960950386e0f573dd08cebc Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Sat, 25 Apr 2026 11:49:08 +0200 Subject: [PATCH] feat(migration): Spar_Migration property set + is_frozen/is_mobile helpers (Track E commit 1/8) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Foundation for v0.8.0 Track E (frozen-platform / mobile-application split + hypothetical-rebinding oracle, #150). Spar_Migration::{Frozen, Mobile, Allowed_Targets, Pinned_Reason} provide the AADL vocabulary for declaring which items are platform (immutable for hypothetical rebinding) vs. which are application (eligible for movement). Per the research in PR #153 §6.1. Helper functions is_frozen() / is_mobile() expose the boolean state to downstream analyses without requiring a salsa query yet — the per-instance cache lands when the hypothetical-binding overlay needs it (Track E commit 2). Per §6.2's tradeoff analysis: minimal surface now, expand on demand. No CLI surface, no MCP, no solver extension in this commit — those are Track E commits 3-5. New requirements: REQ-MIGRATION-{001,002,003}. Co-Authored-By: Claude Opus 4.7 (1M context) --- artifacts/requirements.yaml | 41 ++++ artifacts/verification.yaml | 54 ++++ crates/spar-hir-def/src/lib.rs | 1 + crates/spar-hir-def/src/migration.rs | 231 ++++++++++++++++++ .../spar-hir-def/src/standard_properties.rs | 140 ++++++++++- 5 files changed, 465 insertions(+), 2 deletions(-) create mode 100644 crates/spar-hir-def/src/migration.rs diff --git a/artifacts/requirements.yaml b/artifacts/requirements.yaml index c45cf13..c17def7 100644 --- a/artifacts/requirements.yaml +++ b/artifacts/requirements.yaml @@ -1112,4 +1112,45 @@ artifacts: status: planned tags: [network, wctt, v080] + # ── Track E: hypothetical-rebinding oracle (v0.8.0) ──────────────── + + - id: REQ-MIGRATION-001 + type: requirement + title: Frozen-platform component annotation + description: > + System shall support marking components as frozen (platform) via + Spar_Migration::Frozen (aadlboolean). Frozen items are platform — + their binding/properties cannot be altered by hypothetical-rebinding + queries. Default false (unannotated components are eligible for + rebinding). Per Track E commit 1/8 of the v0.8.0 migration design + research (docs/designs/track-e-migration-research.md §6.1). + status: planned + tags: [migration, track-e, v080] + + - id: REQ-MIGRATION-002 + type: requirement + title: Mobile-application component annotation with allowed targets + description: > + System shall support marking components as mobile (application) via + Spar_Migration::Mobile (aadlboolean), with optional Allowed_Targets + (list of reference) enumeration restricting valid hypothetical + rebinding destinations. Empty Allowed_Targets means "no restriction + beyond the platform's frozen set". When both Frozen=true and + Mobile=true are declared on the same item, Frozen wins (defensive + — refuse to rebind). Per §6.1 of the v0.8.0 migration design. + status: planned + tags: [migration, track-e, v080] + + - id: REQ-MIGRATION-003 + type: requirement + title: Pinned-reason audit metadata + description: > + System shall record human-readable Pinned_Reason for frozen items + as audit metadata. Exposed via Spar_Migration::Pinned_Reason + (aadlstring). Captures the rationale a reviewer would need to + certify why an item is platform (e.g., "ASIL-D platform partition", + "RTOS kernel image"). Per §6.1 of the v0.8.0 migration design. + status: planned + tags: [migration, track-e, v080, audit] + # Research findings tracked separately in research/findings.yaml diff --git a/artifacts/verification.yaml b/artifacts/verification.yaml index d821d5e..39f649b 100644 --- a/artifacts/verification.yaml +++ b/artifacts/verification.yaml @@ -1391,3 +1391,57 @@ artifacts: target: REQ-NETWORK-002 - type: satisfies target: REQ-NETWORK-003 + + - id: TEST-SPAR-MIGRATION-PROPS + type: feature + title: Spar_Migration property set unit tests + description: > + Unit tests in crates/spar-hir-def/src/standard_properties.rs + that exercise registration of the Spar_Migration property set + (Track E commit 1/8). Covers: each of the four properties + (Frozen, Mobile, Allowed_Targets, Pinned_Reason) resolves to its + expected AADL type via standard_property_type; the property set + is registered in STANDARD_PROPERTY_SET_NAMES and resolves through + GlobalScope without an explicit `with` import; unknown property + names within the set return None / Unresolved; resolution is + case-insensitive per the AADL spec. + fields: + method: automated-test + steps: + - run: >- + cargo test -p spar-hir-def --lib -- + standard_properties::tests::test_standard_properties_in_spar_migration + standard_properties::tests::test_spar_migration_property_set_resolved_via_global_scope + standard_properties::tests::test_spar_migration_unknown_property_returns_none + status: passing + tags: [migration, track-e, v080] + links: + - type: satisfies + target: REQ-MIGRATION-001 + - type: satisfies + target: REQ-MIGRATION-002 + - type: satisfies + target: REQ-MIGRATION-003 + + - id: TEST-SPAR-MIGRATION-HELPERS + type: feature + title: is_frozen / is_mobile helper unit tests + description: > + Unit tests in crates/spar-hir-def/src/migration.rs that exercise + the boolean helpers over the Spar_Migration property set. Covers: + default-false behaviour for unannotated property maps; honouring + typed PropertyExpr::Boolean values; raw-string fallback for + pre-typed-lowering fixtures; defensive Frozen-wins-over-Mobile + resolution when both are declared on the same item (per §6.1 of + the v0.8.0 migration design). + fields: + method: automated-test + steps: + - run: cargo test -p spar-hir-def --lib -- migration::tests + status: passing + tags: [migration, track-e, v080] + links: + - type: satisfies + target: REQ-MIGRATION-001 + - type: satisfies + target: REQ-MIGRATION-002 diff --git a/crates/spar-hir-def/src/lib.rs b/crates/spar-hir-def/src/lib.rs index bd3a59a..606c030 100644 --- a/crates/spar-hir-def/src/lib.rs +++ b/crates/spar-hir-def/src/lib.rs @@ -20,6 +20,7 @@ pub mod category_rules; pub mod feature_group; pub mod instance; pub mod item_tree; +pub mod migration; pub mod name; pub mod properties; pub mod property_check; diff --git a/crates/spar-hir-def/src/migration.rs b/crates/spar-hir-def/src/migration.rs new file mode 100644 index 0000000..61989ec --- /dev/null +++ b/crates/spar-hir-def/src/migration.rs @@ -0,0 +1,231 @@ +//! Spar_Migration property helpers (Track E commit 1/8, v0.8.0). +//! +//! Provides the thin boolean accessors over the `Spar_Migration::Frozen` +//! and `Spar_Migration::Mobile` properties registered in +//! [`standard_properties`](crate::standard_properties). +//! +//! These helpers are intentionally minimal — no salsa query, no +//! per-instance enum cache yet. They read the property at lookup time +//! using the same typed-first / string-fallback pattern as +//! `spar-analysis::property_accessors`. The HIR-level cache lands in +//! Track E commit 2 once the hypothetical-binding overlay needs it. +//! Per the design research §6.2 tradeoff analysis: minimal surface +//! now, expand on demand. + +use crate::item_tree::PropertyExpr; +use crate::properties::PropertyMap; + +/// The `Spar_Migration` property set name. +const SPAR_MIGRATION: &str = "Spar_Migration"; + +/// Return `true` if `Spar_Migration::Frozen` is set on this property map. +/// +/// Returns `false` if the property is unset, set to `false`, or set to a +/// non-boolean value. Defaults to `false` so unannotated components are +/// treated as eligible for hypothetical rebinding (i.e., the overlay +/// only rejects moves that touch components which were *explicitly* +/// declared platform). +/// +/// Reads via [`PropertyMap::get_typed`] first (preferred — exact +/// boolean), falling back to [`PropertyMap::get`] with case-insensitive +/// "true"/"false" parsing for compatibility with raw-string properties +/// (e.g., assertion fixtures that pre-date typed lowering). +pub fn is_frozen(props: &PropertyMap) -> bool { + read_bool_property(props, "Frozen").unwrap_or(false) +} + +/// Return `true` if `Spar_Migration::Mobile` is set on this property map +/// **and** `Frozen` is *not* set. +/// +/// When both `Frozen=true` and `Mobile=true` are declared on the same +/// item the relation is contradictory; this helper resolves it +/// defensively in favour of `Frozen` (refuse to rebind) rather than +/// `Mobile` (allow rebind). Per §6.1 of the design research: "mutually +/// inconsistent with `Frozen=true`". +/// +/// Returns `false` if `Mobile` is unset, set to `false`, set to a +/// non-boolean value, or if `Frozen=true` overrides it. +pub fn is_mobile(props: &PropertyMap) -> bool { + if is_frozen(props) { + return false; + } + read_bool_property(props, "Mobile").unwrap_or(false) +} + +/// Read a `Spar_Migration::` boolean property. +/// +/// Returns `Some(true)` / `Some(false)` if the property is present and +/// parses as a boolean; returns `None` if the property is absent or has +/// a non-boolean value. +fn read_bool_property(props: &PropertyMap, name: &str) -> Option { + // Typed path: prefer the structured PropertyExpr. + if let Some(expr) = props.get_typed(SPAR_MIGRATION, name) + && let PropertyExpr::Boolean(b) = expr + { + return Some(*b); + } + + // String fallback: tolerate raw "true"/"false" (case-insensitive). + let raw = props.get(SPAR_MIGRATION, name)?; + match raw.trim().to_ascii_lowercase().as_str() { + "true" => Some(true), + "false" => Some(false), + _ => None, + } +} + +#[cfg(test)] +mod tests { + use super::*; + use crate::name::{Name, PropertyRef}; + use crate::properties::PropertyValue; + + /// Build a PropertyMap with a typed expression value. + fn make_typed_props(set: &str, name: &str, value: &str, expr: PropertyExpr) -> PropertyMap { + let mut props = PropertyMap::new(); + props.add(PropertyValue { + name: PropertyRef { + property_set: if set.is_empty() { + None + } else { + Some(Name::new(set)) + }, + property_name: Name::new(name), + }, + value: value.to_string(), + typed_expr: Some(expr), + is_append: false, + }); + props + } + + /// Build a PropertyMap with only a raw string value (no typed expr). + fn make_string_props(set: &str, name: &str, value: &str) -> PropertyMap { + let mut props = PropertyMap::new(); + props.add(PropertyValue { + name: PropertyRef { + property_set: if set.is_empty() { + None + } else { + Some(Name::new(set)) + }, + property_name: Name::new(name), + }, + value: value.to_string(), + typed_expr: None, + is_append: false, + }); + props + } + + // ── is_frozen ───────────────────────────────────────────────── + + #[test] + fn test_is_frozen_default_false() { + // Unannotated property map: not frozen. + let props = PropertyMap::new(); + assert!(!is_frozen(&props)); + } + + #[test] + fn test_is_frozen_when_property_set() { + // Spar_Migration::Frozen => true (typed) → frozen. + let props = make_typed_props( + "Spar_Migration", + "Frozen", + "true", + PropertyExpr::Boolean(true), + ); + assert!(is_frozen(&props)); + + // Spar_Migration::Frozen => false (typed) → not frozen. + let props = make_typed_props( + "Spar_Migration", + "Frozen", + "false", + PropertyExpr::Boolean(false), + ); + assert!(!is_frozen(&props)); + + // Raw-string fallback (no typed expr) is also accepted. + let props = make_string_props("Spar_Migration", "Frozen", "true"); + assert!(is_frozen(&props)); + let props = make_string_props("Spar_Migration", "Frozen", "FALSE"); + assert!(!is_frozen(&props)); + } + + #[test] + fn test_is_frozen_non_boolean_value_treated_as_false() { + // Defensive: a malformed value must not be silently treated as + // "frozen" (which is the safe-against-rebinding side); the + // analysis's job is to flag malformed properties via the type + // checker, not for this helper to invent a result. + let props = make_string_props("Spar_Migration", "Frozen", "yes-please"); + assert!(!is_frozen(&props)); + } + + // ── is_mobile ───────────────────────────────────────────────── + + #[test] + fn test_is_mobile_default_false() { + // Unannotated property map: not mobile. + let props = PropertyMap::new(); + assert!(!is_mobile(&props)); + } + + #[test] + fn test_is_mobile_when_property_set() { + // Spar_Migration::Mobile => true (typed) → mobile. + let props = make_typed_props( + "Spar_Migration", + "Mobile", + "true", + PropertyExpr::Boolean(true), + ); + assert!(is_mobile(&props)); + + // Spar_Migration::Mobile => false (typed) → not mobile. + let props = make_typed_props( + "Spar_Migration", + "Mobile", + "false", + PropertyExpr::Boolean(false), + ); + assert!(!is_mobile(&props)); + + // Raw-string fallback also accepted. + let props = make_string_props("Spar_Migration", "Mobile", "True"); + assert!(is_mobile(&props)); + } + + #[test] + fn test_is_mobile_loses_to_frozen_when_both_set() { + // Defensive: if a model declares both Frozen=true and + // Mobile=true, prefer Frozen — refuse to rebind. Per §6.1. + let mut props = PropertyMap::new(); + props.add(PropertyValue { + name: PropertyRef { + property_set: Some(Name::new("Spar_Migration")), + property_name: Name::new("Frozen"), + }, + value: "true".to_string(), + typed_expr: Some(PropertyExpr::Boolean(true)), + is_append: false, + }); + props.add(PropertyValue { + name: PropertyRef { + property_set: Some(Name::new("Spar_Migration")), + property_name: Name::new("Mobile"), + }, + value: "true".to_string(), + typed_expr: Some(PropertyExpr::Boolean(true)), + is_append: false, + }); + + assert!(is_frozen(&props), "Frozen=true must be honoured"); + assert!( + !is_mobile(&props), + "Mobile must lose to Frozen when both are set", + ); + } +} diff --git a/crates/spar-hir-def/src/standard_properties.rs b/crates/spar-hir-def/src/standard_properties.rs index 627ee8b..ab05d4e 100644 --- a/crates/spar-hir-def/src/standard_properties.rs +++ b/crates/spar-hir-def/src/standard_properties.rs @@ -37,6 +37,7 @@ pub const STANDARD_PROPERTY_SET_NAMES: &[&str] = &[ "Spar_Timing", "Spar_Trace", "Spar_Network", + "Spar_Migration", ]; // ── Timing_Properties ─────────────────────────────────────────────── @@ -372,6 +373,42 @@ const SPAR_NETWORK: &[(&str, &str)] = &[ ("Output_Rate", "Data_Rate"), ]; +// ── Spar_Migration ────────────────────────────────────────────────── +// +// Non-standard property set defined by spar itself (not AS5506); used +// for the v0.8.0 Track E "frozen-platform / mobile-application" split +// and the hypothetical-rebinding oracle. Provides the AADL vocabulary +// for declaring which items are platform (immutable for hypothetical +// rebinding) vs. which are application (eligible for movement). Per +// the design research in `docs/designs/track-e-migration-research.md` +// §6.1. + +const SPAR_MIGRATION: &[(&str, &str)] = &[ + // Marks the item as platform — its binding/properties cannot be + // altered by hypothetical-rebinding queries. Default false. Applies + // to every component category (process, processor, memory, bus, + // device, system, thread, …). + ("Frozen", "aadlboolean"), + // Marks the item as application — eligible for hypothetical + // rebinding. Default false. Mutually inconsistent with Frozen=true; + // when both are set Frozen wins (defensive; see is_frozen helper). + ("Mobile", "aadlboolean"), + // Enumerates the set of valid rebinding targets. Empty list = no + // restriction beyond the platform's frozen set. + // + // TODO(v0.9.0): broaden to "list of reference (component)" once the + // AADL type table supports the generic-component reference form. + // Today we register as `list of reference (thread)` — the most + // common case for hypothetical rebinding (threads are what get + // rebound). Per §6.1 of the migration research; the property set + // surface is permissive at the registration level since the + // declarative type only gates parser-level type checking, and + // analyses read the references untyped via PropertyExpr. + ("Allowed_Targets", "list of reference (thread)"), + // Human-readable reason for `Frozen => true`. For audit trails. + ("Pinned_Reason", "aadlstring"), +]; + /// Helper: collect properties from a table into the result vector. fn collect_properties( table: &[(&'static str, &'static str)], @@ -410,6 +447,7 @@ pub fn all_standard_properties() -> Vec { collect_properties(SPAR_TIMING, "Spar_Timing", &mut result); collect_properties(SPAR_TRACE, "Spar_Trace", &mut result); collect_properties(SPAR_NETWORK, "Spar_Network", &mut result); + collect_properties(SPAR_MIGRATION, "Spar_Migration", &mut result); result } @@ -438,6 +476,7 @@ fn lookup_table(set_lower: &str) -> Option<&'static [(&'static str, &'static str "spar_timing" => Some(SPAR_TIMING), "spar_trace" => Some(SPAR_TRACE), "spar_network" => Some(SPAR_NETWORK), + "spar_migration" => Some(SPAR_MIGRATION), _ => None, } } @@ -485,6 +524,7 @@ mod tests { assert!(is_standard_property_set("Spar_Timing")); assert!(is_standard_property_set("Spar_Trace")); assert!(is_standard_property_set("Spar_Network")); + assert!(is_standard_property_set("Spar_Migration")); // Case-insensitive assert!(is_standard_property_set("timing_properties")); @@ -832,6 +872,99 @@ mod tests { ); } + #[test] + fn test_standard_properties_in_spar_migration() { + // Spar_Migration is a known property set. + assert!(is_standard_property_set("Spar_Migration")); + + let props = standard_properties_in_set("Spar_Migration"); + assert_eq!(props.len(), 4); + assert!(props.contains(&"Frozen")); + assert!(props.contains(&"Mobile")); + assert!(props.contains(&"Allowed_Targets")); + assert!(props.contains(&"Pinned_Reason")); + + // Each property resolves to its expected type. + assert_eq!( + standard_property_type("Spar_Migration", "Frozen"), + Some("aadlboolean") + ); + assert_eq!( + standard_property_type("Spar_Migration", "Mobile"), + Some("aadlboolean") + ); + assert_eq!( + standard_property_type("Spar_Migration", "Allowed_Targets"), + Some("list of reference (thread)") + ); + assert_eq!( + standard_property_type("Spar_Migration", "Pinned_Reason"), + Some("aadlstring") + ); + + // Case-insensitive. + assert_eq!( + standard_property_type("spar_migration", "frozen"), + Some("aadlboolean") + ); + assert_eq!( + standard_property_type("SPAR_MIGRATION", "PINNED_REASON"), + Some("aadlstring") + ); + } + + #[test] + fn test_spar_migration_unknown_property_returns_none() { + // Unknown property within a known spar_migration set. + assert_eq!( + standard_property_type("Spar_Migration", "Nonexistent"), + None + ); + assert_eq!( + standard_property_type("Spar_Migration", "Migration_Cost"), + None, + "Migration_Cost is documented in §6.1 but deferred past commit 1; \ + must not resolve in the foundation property set" + ); + } + + #[test] + fn test_spar_migration_property_set_resolved_via_global_scope() { + use crate::name::Name; + use crate::resolver::{GlobalScope, ResolvedProperty}; + + let scope = GlobalScope::from_trees(vec![]); + + // Each Spar_Migration property is resolvable without explicit `with`. + for prop_name in ["Frozen", "Mobile", "Allowed_Targets", "Pinned_Reason"] { + let result = + scope.resolve_property(&Name::new("Spar_Migration"), &Name::new(prop_name)); + assert!( + matches!(result, ResolvedProperty::PropertyDef { .. }), + "expected PropertyDef for Spar_Migration::{}, got {:?}", + prop_name, + result + ); + } + + // Deliberately-wrong name inside a known spar set is Unresolved. + let result = + scope.resolve_property(&Name::new("Spar_Migration"), &Name::new("Nonexistent")); + assert!( + matches!(result, ResolvedProperty::Unresolved), + "expected Unresolved for Spar_Migration::Nonexistent, got {:?}", + result + ); + + // Case-insensitive resolution + let result = scope.resolve_property(&Name::new("spar_migration"), &Name::new("frozen")); + assert!( + matches!(result, ResolvedProperty::PropertyDef { .. }), + "expected case-insensitive match for Spar_Migration::Frozen, got {:?}", + result + ); + } + #[test] fn test_standard_properties_unknown_set() { let props = standard_properties_in_set("Nonexistent_Properties"); @@ -848,8 +981,11 @@ mod tests { #[test] fn test_all_standard_properties_total_count() { let all = all_standard_properties(); - // 12 + 13 + 14 + 14 + 7 + 25 + 4 + 13 + 4 + 4 + 4 = 114 - assert_eq!(all.len(), 114); + // 12 + 13 + 14 + 14 + 7 + 25 + 4 + 13 + 4 + 4 + 4 + 4 = 118 + // (Timing + Communication + Memory + Deployment + Thread + Programming + // + Modeling + AADL_Project + Spar_Timing + Spar_Trace + Spar_Network + // + Spar_Migration) + assert_eq!(all.len(), 118); } #[test]