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

crates/temper-platform/src/deploy.rs

@@ -238,6 +238,7 @@ impl DeployPipeline {
                     all_passed: true,
                     levels: vec![],
                     warnings: vec![],
+                    unsupported_invariants: vec![],
                     reachable_paths: None,
                     composite_report: None,
                 }

crates/temper-platform/src/specs/agent.ioa.toml

@@ -185,7 +185,3 @@ hint = "Reset the agent for reuse. Clears all state variables."
 
 # --- Safety Invariants ---
 
-[[invariant]]
-name = "AssignedRequiresGoal"
-when = ["Assigned", "Working", "Blocked", "Completed", "Failed"]
-assert = "goal != ''"

crates/temper-platform/src/specs/agent_credential.ioa.toml

@@ -74,17 +74,3 @@ hint = "Permanently revoke this credential. The key hash can never be used again
 
 # --- Safety Invariants ---
 
-[[invariant]]
-name = "ActiveRequiresKeyHash"
-when = ["Active"]
-assert = "key_hash != ''"
-
-[[invariant]]
-name = "ActiveRequiresAgentType"
-when = ["Active"]
-assert = "agent_type_id != ''"
-
-[[invariant]]
-name = "ActiveRequiresInstanceId"
-when = ["Active"]
-assert = "agent_instance_id != ''"

crates/temper-platform/src/specs/agent_type.ioa.toml

@@ -79,7 +79,3 @@ hint = "Reactivate a deprecated agent type."
 
 # --- Safety Invariants ---
 
-[[invariant]]
-name = "ActiveRequiresName"
-when = ["Active"]
-assert = "name != ''"

crates/temper-platform/src/specs/schedule.ioa.toml

@@ -91,12 +91,3 @@ hint = "Resume a paused schedule."
 
 # --- Safety Invariants ---
 
-[[invariant]]
-name = "ActiveRequiresCron"
-when = ["Active"]
-assert = "cron_expr != ''"
-
-[[invariant]]
-name = "ActiveRequiresGoal"
-when = ["Active"]
-assert = "goal_template != ''"

crates/temper-platform/src/specs/tool_call.ioa.toml

@@ -106,11 +106,6 @@ hint = "Human approved the denied decision. ToolCall returns to Pending for re-a
 
 # --- Safety Invariants ---
 
-[[invariant]]
-name = "RequiresAgentId"
-when = ["Pending", "Authorized", "Denied", "Executing", "Completed", "Failed"]
-assert = "agent_id != ''"
-
 [[invariant]]
 name = "CompletedIsFinal"
 when = ["Completed"]

crates/temper-runtime/src/scheduler/sim_actor_system.rs

@@ -666,6 +666,7 @@ fn evaluate_spec_assert(
             // Holds unless status_before was a terminal state in `when`.
             !when.iter().any(|s| s == status_before)
         }
+        SpecAssert::Tautology => true,
         SpecAssert::OrderingConstraint { before, after } => {
             if status_after == after.as_str() {
                 let events = handler.events_json();

crates/temper-runtime/src/scheduler/sim_handler.rs

@@ -32,6 +32,8 @@ pub enum SpecAssert {
     CounterPositive { var: String },
     /// The entity is in a terminal state — no further transitions allowed.
     NoFurtherTransitions,
+    /// Literal `true` — always holds.
+    Tautology,
     /// State A must have been visited before state B in event history.
     /// Expressed as: `ordering(A, B)` — "A precedes B".
     OrderingConstraint { before: String, after: String },

crates/temper-server/src/entity_actor/sim_handler.rs

@@ -124,6 +124,7 @@ fn translate_parsed(
     match parsed {
         ParsedAssert::CounterPositive { var } => Some(SpecAssert::CounterPositive { var }),
         ParsedAssert::NoFurtherTransitions => Some(SpecAssert::NoFurtherTransitions),
+        ParsedAssert::Tautology => Some(SpecAssert::Tautology),
         ParsedAssert::OrderingConstraint { before, after } => {
             Some(SpecAssert::OrderingConstraint { before, after })
         }

crates/temper-spec/src/automaton/assert_parser.rs

@@ -26,6 +26,8 @@ pub enum ParsedAssert {
     CounterPositive { var: String },
     /// The entity is in a terminal state — no further transitions allowed.
     NoFurtherTransitions,
+    /// Literal `true` — always holds (used for trivial / marker invariants).
+    Tautology,
     /// State A must have been visited before state B in event history.
     /// Expressed as: `ordering(A, B)`.
     OrderingConstraint { before: String, after: String },
@@ -311,6 +313,22 @@ fn parse_terminal(tokens: &[Tok], cursor: &mut usize) -> Option<ParsedAssert> {
             return Some(ParsedAssert::NoFurtherTransitions);
         }
 
+        // Literal true — always holds.
+        if name == "true" {
+            *cursor += 1;
+            return Some(ParsedAssert::Tautology);
+        }
+
+        // is_true <bool_var> — same as bare bool (IOA sugar used in os-apps).
+        if name == "is_true" {
+            let var = match tokens.get(*cursor + 1) {
+                Some(Tok::Ident(s)) => s.clone(),
+                _ => return None,
+            };
+            *cursor += 2;
+            return Some(ParsedAssert::BoolRequired { var, expect: true });
+        }
+
         // Bare boolean identifier.
         *cursor += 1;
         return Some(ParsedAssert::BoolRequired {
@@ -352,6 +370,22 @@ mod tests {
         );
     }
 
+    #[test]
+    fn test_tautology_literal_true() {
+        assert_eq!(parse_assert_expr("true"), Some(ParsedAssert::Tautology));
+    }
+
+    #[test]
+    fn test_is_true_sugar() {
+        assert_eq!(
+            parse_assert_expr("is_true has_evidence"),
+            Some(ParsedAssert::BoolRequired {
+                var: "has_evidence".to_string(),
+                expect: true,
+            })
+        );
+    }
+
     #[test]
     fn test_ordering_constraint() {
         assert_eq!(

crates/temper-verify/src/cascade/diagnostics.rs

@@ -0,0 +1,140 @@
+//! Unsupported-safety diagnostics and source-span helpers (ADR-0178).
+
+use crate::model::{InvariantKind, TemperModel};
+
+/// Stable error code for unsupported safety-invariant diagnostics (ADR-0178).
+pub const UNSUPPORTED_SAFETY_INVARIANT_CODE: &str = "VERIFY_UNSUPPORTED_SAFETY_INVARIANT";
+
+/// Byte and 1-based line/column span into the submitted IOA document.
+#[derive(Debug, Clone, PartialEq, Eq, serde::Serialize, serde::Deserialize)]
+pub struct SourceSpan {
+    /// Inclusive start offset in UTF-8 bytes.
+    pub start_byte: usize,
+    /// Exclusive end offset in UTF-8 bytes.
+    pub end_byte: usize,
+    /// 1-based start line.
+    pub start_line: u32,
+    /// 1-based start column (UTF-8 bytes within the line).
+    pub start_column: u32,
+    /// 1-based end line.
+    pub end_line: u32,
+    /// 1-based end column (UTF-8 bytes within the line; exclusive).
+    pub end_column: u32,
+}
+
+/// Structured diagnostic for a safety invariant the verifier cannot encode.
+#[derive(Debug, Clone, PartialEq, Eq, serde::Serialize, serde::Deserialize)]
+pub struct UnsupportedInvariantDiagnostic {
+    /// Stable machine-readable code ([`UNSUPPORTED_SAFETY_INVARIANT_CODE`]).
+    pub code: String,
+    /// `[[invariant]]` name from the submitted document.
+    pub invariant_name: String,
+    /// Original assertion expression that could not be verified.
+    pub expression: String,
+    /// Source range of the `[[invariant]]` table in the submitted IOA, when found.
+    #[serde(default, skip_serializing_if = "Option::is_none")]
+    pub source_span: Option<SourceSpan>,
+}
+
+/// Collect ADR-0178 diagnostics for every `Unverifiable` model invariant.
+pub(crate) fn collect_unsupported_invariant_diagnostics(
+    model: &TemperModel,
+    ioa_source: &str,
+) -> Vec<UnsupportedInvariantDiagnostic> {
+    model
+        .invariants
+        .iter()
+        .filter_map(|inv| {
+            if let InvariantKind::Unverifiable { expression } = &inv.kind {
+                Some(UnsupportedInvariantDiagnostic {
+                    code: UNSUPPORTED_SAFETY_INVARIANT_CODE.to_string(),
+                    invariant_name: inv.name.clone(),
+                    expression: expression.clone(),
+                    source_span: find_invariant_source_span(ioa_source, &inv.name),
+                })
+            } else {
+                None
+            }
+        })
+        .collect()
+}
+
+/// Locate the `[[invariant]]` array-table for `name` in the submitted IOA TOML.
+fn find_invariant_source_span(source: &str, name: &str) -> Option<SourceSpan> {
+    let bytes = source.as_bytes();
+    let mut search_from = 0usize;
+    while let Some(rel) = source[search_from..].find("[[invariant]]") {
+        let table_start = search_from + rel;
+        let after_header = table_start + "[[invariant]]".len();
+        let next_table = source[after_header..]
+            .find("\n[")
+            .map(|i| after_header + i)
+            .unwrap_or(source.len());
+        let table_body = &source[table_start..next_table];
+        if invariant_table_name_matches(table_body, name) {
+            let end = trim_trailing_ws_end(bytes, next_table);
+            return Some(byte_range_to_source_span(source, table_start, end));
+        }
+        search_from = after_header;
+    }
+    None
+}
+
+fn invariant_table_name_matches(table_body: &str, name: &str) -> bool {
+    for line in table_body.lines() {
+        let trimmed = line.trim();
+        if let Some(rest) = trimmed.strip_prefix("name") {
+            let rest = rest.trim_start();
+            if let Some(rest) = rest.strip_prefix('=') {
+                let rest = rest.trim();
+                let value = rest
+                    .strip_prefix('"')
+                    .and_then(|s| s.strip_suffix('"'))
+                    .or_else(|| rest.strip_prefix('\'').and_then(|s| s.strip_suffix('\'')));
+                if value == Some(name) {
+                    return true;
+                }
+            }
+        }
+    }
+    false
+}
+
+fn trim_trailing_ws_end(bytes: &[u8], end: usize) -> usize {
+    let mut e = end;
+    while e > 0 && matches!(bytes[e - 1], b' ' | b'\t' | b'\n' | b'\r') {
+        e -= 1;
+    }
+    e
+}
+
+fn byte_range_to_source_span(source: &str, start_byte: usize, end_byte: usize) -> SourceSpan {
+    let (start_line, start_column) = byte_offset_to_line_col(source, start_byte);
+    let (end_line, end_column) = byte_offset_to_line_col(source, end_byte);
+    SourceSpan {
+        start_byte,
+        end_byte,
+        start_line,
+        start_column,
+        end_line,
+        end_column,
+    }
+}
+
+fn byte_offset_to_line_col(source: &str, offset: usize) -> (u32, u32) {
+    let offset = offset.min(source.len());
+    let mut line = 1u32;
+    let mut col = 1u32;
+    for (i, b) in source.as_bytes().iter().enumerate() {
+        if i >= offset {
+            break;
+        }
+        if *b == b'\n' {
+            line += 1;
+            col = 1;
+        } else {
+            col += 1;
+        }
+    }
+    (line, col)
+}