feat(migration): Spar_Migration property set + helpers (Track E commit 1/8)

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

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

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;

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::<name>` 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<bool> {
+    // 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",
+        );
+    }
+}