fix(verify): fail closed on unsupported safety invariants (ARN-213)

crates/temper-cli/src/serve/actor_runtime.rs

@@ -252,6 +252,13 @@ fn validate_actor_runtime_compatible(
     entity_type: &str,
     spec: &EntitySpec,
 ) -> Result<()> {
+    let runtime_invariants = temper_spec::automaton::compile_runtime_invariants(&spec.automaton);
+    if !runtime_invariants.is_empty() {
+        bail!(
+            "tenant {tenant} entity {entity_type} declares runtime-enforced invariants, which are not yet supported by --actor-runtime postgres"
+        );
+    }
+
     if !spec.integrations.is_empty() {
         bail!(
             "tenant {tenant} entity {entity_type} declares legacy integrations, which are not yet supported by --actor-runtime postgres"
@@ -403,6 +410,64 @@ mod tests {
         assert!(err.to_string().contains("not yet supported"));
     }
 
+    #[test]
+    fn rejects_runtime_enforced_invariants_on_postgres_actor_runtime() {
+        let ioa = r#"
+[automaton]
+name = "Goal"
+states = ["Active"]
+initial = "Active"
+allow_indefinite_states = ["Active"]
+
+[[state]]
+name = "goal"
+type = "string"
+initial = ""
+
+[[invariant]]
+name = "GoalRequired"
+when = ["Active"]
+assert = "goal != ''"
+"#;
+        let registry = registry_with("alpha", "Goal", ioa);
+        let error = collect_actor_runtime_definitions(&registry, &["Goal".into()]).unwrap_err();
+
+        assert!(error.to_string().contains("runtime-enforced invariants"));
+    }
+
+    #[test]
+    fn accepts_model_only_counter_invariant_on_postgres_actor_runtime() {
+        let ioa = r#"
+[automaton]
+name = "Counter"
+states = ["Active"]
+initial = "Active"
+allow_indefinite_states = ["Active"]
+
+[[state]]
+name = "items"
+type = "counter"
+initial = "1"
+
+[[action]]
+name = "Add"
+kind = "input"
+from = ["Active"]
+to = "Active"
+effect = [{ type = "increment", var = "items" }]
+
+[[invariant]]
+name = "HasItems"
+when = ["Active"]
+assert = "items > 0"
+"#;
+        let registry = registry_with("alpha", "Counter", ioa);
+        let definitions = collect_actor_runtime_definitions(&registry, &["Counter".into()])
+            .expect("model-only counter invariant remains actor-runtime compatible");
+
+        assert!(definitions.actor_backed_keys.contains("Counter"));
+    }
+
     #[test]
     fn rejects_conflicting_same_named_specs_across_tenants() {
         let mut registry = registry_with("alpha", "Order", ORDER_IOA);

crates/temper-cli/src/serve/mod.rs

@@ -755,21 +755,10 @@ async fn spawn_background_verification(state: &PlatformState, specs_dir: &str, t
                         }
                     }
 
-                    // Build verification result
-                    let verification_result = EntityVerificationResult {
-                        all_passed: cascade_result.all_passed,
-                        levels: cascade_result
-                            .levels
-                            .iter()
-                            .map(|l| EntityLevelSummary {
-                                level: format!("{:?}", l.level),
-                                passed: l.passed,
-                                summary: l.summary.clone(),
-                                details: None,
-                            })
-                            .collect(),
-                        verified_at: chrono::Utc::now().to_rfc3339(), // determinism-ok: CLI code
-                    };
+                    let verification_result = EntityVerificationResult::from_cascade(
+                        &cascade_result,
+                        chrono::Utc::now().to_rfc3339(), // determinism-ok: CLI code
+                    );
 
                     let all_passed = cascade_result.all_passed;
 
@@ -850,6 +839,8 @@ async fn spawn_background_verification(state: &PlatformState, specs_dir: &str, t
                             summary: format!("Verification failed: {e}"),
                             details: None,
                         }],
+                        warnings: Vec::new(),
+                        errors: Vec::new(),
                         verified_at: chrono::Utc::now().to_rfc3339(), // determinism-ok: CLI code
                     };
 

crates/temper-jit/src/shadow.rs

@@ -115,6 +115,7 @@ mod tests {
             entity_name: "Order".into(),
             states: vec!["Draft".into(), "Submitted".into(), "Cancelled".into()],
             initial_state: "Draft".into(),
+            state_var_initials: Default::default(),
             keys: vec![],
             vectors: vec![],
             rules: vec![
@@ -141,6 +142,8 @@ mod tests {
             ],
             state_var_metadata: Default::default(),
             composite_actions: Default::default(),
+            runtime_invariants: Default::default(),
+            model_protected_state_vars: Default::default(),
             rule_index: Default::default(),
         };
         table.rebuild_index();

crates/temper-jit/src/swap.rs

@@ -86,6 +86,7 @@ mod tests {
             entity_name: name.to_string(),
             states: vec!["A".into(), "B".into()],
             initial_state: "A".into(),
+            state_var_initials: Default::default(),
             keys: vec![],
             vectors: vec![],
             rules: vec![TransitionRule {
@@ -97,6 +98,8 @@ mod tests {
             }],
             state_var_metadata: Default::default(),
             composite_actions: Default::default(),
+            runtime_invariants: Default::default(),
+            model_protected_state_vars: Default::default(),
             rule_index: Default::default(),
         };
         table.rebuild_index();

crates/temper-jit/src/table/builder.rs

@@ -4,42 +4,71 @@
 //! translation layer in `temper-spec`. The shared layer eliminates duplicated
 //! guard/effect translation logic between JIT and verification paths.
 
-use temper_spec::automaton::{self, Automaton, ResolvedEffect, ResolvedGuard, translate_actions};
+use temper_spec::automaton::{
+    self, Automaton, ResolvedEffect, ResolvedGuard, parse_bool_initial,
+    parse_counter_initial_usize, translate_actions,
+};
 
 use super::guard::Guard;
 use super::types::{
-    CompositeActionMetadata, CompositeCedarGate, Effect, SubWriteSpec, TransitionRule,
-    TransitionTable,
+    CompositeActionMetadata, CompositeCedarGate, Effect, StateVarInitialValue, SubWriteSpec,
+    TransitionRule, TransitionTable,
 };
 
 impl TransitionTable {
     /// Build a TransitionTable from I/O Automaton TOML source.
     ///
-    /// Returns an error if the TOML fails to parse. Prefer this over
-    /// [`from_ioa_source`](Self::from_ioa_source) in production code
-    /// where parse errors should be propagated.
+    /// Returns an error if the TOML fails to parse or declares an unsupported
+    /// safety invariant. Prefer this over [`from_ioa_source`](Self::from_ioa_source)
+    /// in production code where construction errors should be propagated.
     pub fn try_from_ioa_source(ioa_toml: &str) -> Result<Self, String> {
         let automaton = automaton::parse_automaton(ioa_toml)
             .map_err(|e| format!("failed to parse I/O Automaton TOML: {e}"))?;
-        Ok(Self::from_automaton(&automaton))
+        Self::try_from_automaton(&automaton)
     }
 
     /// Build a TransitionTable from I/O Automaton TOML source.
     ///
     /// # Panics
     ///
-    /// Panics if the TOML fails to parse. Use [`try_from_ioa_source`](Self::try_from_ioa_source)
-    /// for fallible construction.
+    /// Panics if the TOML fails to parse or declares an unsupported safety
+    /// invariant. Use [`try_from_ioa_source`](Self::try_from_ioa_source) for
+    /// fallible construction.
     pub fn from_ioa_source(ioa_toml: &str) -> Self {
-        Self::try_from_ioa_source(ioa_toml).expect("failed to parse I/O Automaton TOML")
+        Self::try_from_ioa_source(ioa_toml)
+            .expect("failed to build transition table from I/O Automaton TOML")
     }
 
     /// Build a TransitionTable directly from a parsed [`Automaton`].
     ///
     /// Each action becomes a [`TransitionRule`] with guards and effects
     /// derived from the IOA specification via the shared translation layer.
     /// Output actions are skipped (they don't transition state).
+    ///
+    /// # Panics
+    ///
+    /// Panics if the automaton declares an unsupported safety invariant. Use
+    /// [`try_from_automaton`](Self::try_from_automaton) for fallible construction.
     pub fn from_automaton(automaton: &Automaton) -> Self {
+        Self::try_from_automaton(automaton).expect("failed to build transition table")
+    }
+
+    /// Build a TransitionTable directly from a parsed [`Automaton`].
+    ///
+    /// Returns an error before constructing executable rules if any declared
+    /// safety invariant is outside the shared verification/runtime contract.
+    pub fn try_from_automaton(automaton: &Automaton) -> Result<Self, String> {
+        let unsupported = automaton::unsupported_safety_invariant_names(automaton);
+        if !unsupported.is_empty() {
+            return Err(format!(
+                "unsupported safety invariants: {}",
+                unsupported.join(", ")
+            ));
+        }
+        Ok(Self::build_from_automaton(automaton))
+    }
+
+    fn build_from_automaton(automaton: &Automaton) -> Self {
         let resolved_actions = translate_actions(automaton);
 
         let rules: Vec<TransitionRule> = resolved_actions
@@ -120,6 +149,21 @@ impl TransitionTable {
             entity_name: automaton.automaton.name.clone(),
             states: automaton.automaton.states.clone(),
             initial_state: automaton.automaton.initial.clone(),
+            state_var_initials: automaton
+                .state
+                .iter()
+                .filter_map(|state| {
+                    let initial = match state.var_type.as_str() {
+                        "counter" => StateVarInitialValue::Counter(parse_counter_initial_usize(
+                            &state.initial,
+                        )),
+                        "bool" => StateVarInitialValue::Bool(parse_bool_initial(&state.initial)),
+                        "string" => StateVarInitialValue::String(state.initial.clone()),
+                        _ => return None,
+                    };
+                    Some((state.name.clone(), initial))
+                })
+                .collect(),
             rules,
             keys: automaton
                 .keys
@@ -142,11 +186,17 @@ impl TransitionTable {
                 .collect(),
             state_var_metadata,
             composite_actions,
+            runtime_invariants: automaton::compile_runtime_invariants(automaton),
+            model_protected_state_vars: automaton::model_protected_state_var_names(automaton),
             rule_index,
         }
     }
 }
 
+#[cfg(test)]
+#[path = "builder_safety_tests.rs"]
+mod builder_safety_tests;
+
 /// Convert a shared [`ResolvedGuard`] to the JIT [`Guard`] type.
 fn convert_guard(guard: ResolvedGuard) -> Guard {
     match guard {
@@ -221,82 +271,12 @@ fn convert_effect(effect: ResolvedEffect) -> Effect {
 }
 
 #[cfg(test)]
-mod tests {
-    use super::*;
+#[path = "builder_metadata_tests.rs"]
+mod builder_metadata_tests;
 
-    #[test]
-    fn test_schedule_effect_maps_to_schedule_action() {
-        let spec = r#"
-[automaton]
-name = "OAuthToken"
-states = ["Active", "Refreshing", "Expired"]
-initial = "Active"
-
-[[action]]
-name = "Activate"
-from = ["Refreshing"]
-to = "Active"
-effect = [{ type = "schedule", action = "Refresh", delay_seconds = 2700 }]
-"#;
-
-        let table = TransitionTable::from_ioa_source(spec);
-        let rule = table.rules.iter().find(|r| r.name == "Activate").unwrap();
-
-        let has_schedule = rule.effects.iter().any(|e| {
-            matches!(
-                e,
-                Effect::ScheduleAction { action, delay_seconds }
-                    if action == "Refresh" && *delay_seconds == 2700
-            )
-        });
-        assert!(
-            has_schedule,
-            "expected ScheduleAction effect, got: {:?}",
-            rule.effects
-        );
-    }
-
-    #[test]
-    fn composite_metadata_is_registered_on_transition_table() {
-        let spec = r#"
-[automaton]
-name = "Repository"
-states = ["Active"]
-initial = "Active"
-
-[[action]]
-name = "IngestPack"
-kind = "Composite"
-from = ["Active"]
-to = "Active"
-record_parent_event = false
-
-[[action.cedar_gate]]
-principal = "request.principal"
-resource = "this"
-action = "Repository::IngestPack"
-
-[[action.sub_writes]]
-target_entity = "Blob"
-action = "Create"
-generated_from = "pack_bytes"
-"#;
-
-        let table = TransitionTable::from_ioa_source(spec);
-        let metadata = table.composite_actions.get("IngestPack").unwrap();
-
-        assert_eq!(
-            metadata
-                .cedar_gate
-                .as_ref()
-                .map(|gate| gate.action.as_str()),
-            Some("Repository::IngestPack")
-        );
-        assert!(!metadata.record_parent_event);
-        assert_eq!(metadata.sub_writes.len(), 1);
-        assert_eq!(metadata.sub_writes[0].target_entity, "Blob");
-    }
-}
+#[cfg(test)]
+#[path = "builder_initial_tests.rs"]
+mod builder_initial_tests;
 
 #[cfg(test)]
 mod cross_entity_tests {

crates/temper-jit/src/table/builder_initial_tests.rs

@@ -0,0 +1,32 @@
+use super::{StateVarInitialValue, TransitionTable};
+
+#[test]
+fn state_initials_use_the_shared_model_and_runtime_parsers() {
+    let spec = r#"
+[automaton]
+name = "TypedInitials"
+states = ["Ready"]
+initial = "Ready"
+allow_indefinite_states = ["Ready"]
+
+[[state]]
+name = "enabled"
+type = "bool"
+initial = "YES"
+
+[[state]]
+name = "retries"
+type = "counter"
+initial = " 3 "
+"#;
+
+    let table = TransitionTable::from_ioa_source(spec);
+    assert_eq!(
+        table.state_var_initials.get("enabled"),
+        Some(&StateVarInitialValue::Bool(true))
+    );
+    assert_eq!(
+        table.state_var_initials.get("retries"),
+        Some(&StateVarInitialValue::Counter(3))
+    );
+}