diff --git a/crates/temper-platform/src/deploy.rs b/crates/temper-platform/src/deploy.rs index 533f83ada..bfadd9769 100644 --- a/crates/temper-platform/src/deploy.rs +++ b/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, } diff --git a/crates/temper-platform/src/specs/agent.ioa.toml b/crates/temper-platform/src/specs/agent.ioa.toml index 0ff361256..667267322 100644 --- a/crates/temper-platform/src/specs/agent.ioa.toml +++ b/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 != ''" diff --git a/crates/temper-platform/src/specs/agent_credential.ioa.toml b/crates/temper-platform/src/specs/agent_credential.ioa.toml index dad370907..8f0709a95 100644 --- a/crates/temper-platform/src/specs/agent_credential.ioa.toml +++ b/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 != ''" diff --git a/crates/temper-platform/src/specs/agent_type.ioa.toml b/crates/temper-platform/src/specs/agent_type.ioa.toml index c947aad00..7a0175532 100644 --- a/crates/temper-platform/src/specs/agent_type.ioa.toml +++ b/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 != ''" diff --git a/crates/temper-platform/src/specs/schedule.ioa.toml b/crates/temper-platform/src/specs/schedule.ioa.toml index 32aa1bdc1..df7a2c492 100644 --- a/crates/temper-platform/src/specs/schedule.ioa.toml +++ b/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 != ''" diff --git a/crates/temper-platform/src/specs/tool_call.ioa.toml b/crates/temper-platform/src/specs/tool_call.ioa.toml index c854ccbbe..6e4364893 100644 --- a/crates/temper-platform/src/specs/tool_call.ioa.toml +++ b/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"] diff --git a/crates/temper-runtime/src/scheduler/sim_actor_system.rs b/crates/temper-runtime/src/scheduler/sim_actor_system.rs index 8009277c4..06738a859 100644 --- a/crates/temper-runtime/src/scheduler/sim_actor_system.rs +++ b/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(); diff --git a/crates/temper-runtime/src/scheduler/sim_handler.rs b/crates/temper-runtime/src/scheduler/sim_handler.rs index 9ea990d78..0104f3860 100644 --- a/crates/temper-runtime/src/scheduler/sim_handler.rs +++ b/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 }, diff --git a/crates/temper-server/src/entity_actor/sim_handler.rs b/crates/temper-server/src/entity_actor/sim_handler.rs index 7082baa71..895cb9ee9 100644 --- a/crates/temper-server/src/entity_actor/sim_handler.rs +++ b/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 }) } diff --git a/crates/temper-spec/src/automaton/assert_parser.rs b/crates/temper-spec/src/automaton/assert_parser.rs index 69e28dd53..3afc4fb65 100644 --- a/crates/temper-spec/src/automaton/assert_parser.rs +++ b/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 { return Some(ParsedAssert::NoFurtherTransitions); } + // Literal true — always holds. + if name == "true" { + *cursor += 1; + return Some(ParsedAssert::Tautology); + } + + // is_true — 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!( diff --git a/crates/temper-verify/src/cascade/diagnostics.rs b/crates/temper-verify/src/cascade/diagnostics.rs new file mode 100644 index 000000000..890cf8f26 --- /dev/null +++ b/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, +} + +/// Collect ADR-0178 diagnostics for every `Unverifiable` model invariant. +pub(crate) fn collect_unsupported_invariant_diagnostics( + model: &TemperModel, + ioa_source: &str, +) -> Vec { + 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 { + 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) +} diff --git a/crates/temper-verify/src/cascade.rs b/crates/temper-verify/src/cascade/mod.rs similarity index 73% rename from crates/temper-verify/src/cascade.rs rename to crates/temper-verify/src/cascade/mod.rs index b57b7bd3f..17082f090 100644 --- a/crates/temper-verify/src/cascade.rs +++ b/crates/temper-verify/src/cascade/mod.rs @@ -10,13 +10,20 @@ //! Each level produces a pass/fail result. All levels run independently. use crate::checker::{self, VerificationResult}; -use crate::model::{self, InvariantKind, TemperModel}; +use crate::model::{self, TemperModel}; use crate::proptest_gen::{self, PropTestResult}; use crate::simulation::{self, SimConfig, SimulationResult}; use crate::smt::{self, SmtResult}; use temper_runtime::scheduler::FaultConfig; +mod diagnostics; + +use diagnostics::collect_unsupported_invariant_diagnostics; +pub use diagnostics::{ + SourceSpan, UNSUPPORTED_SAFETY_INVARIANT_CODE, UnsupportedInvariantDiagnostic, +}; + /// Result of an actor simulation level (Level 2b). /// /// This is provided by the caller since the actor simulation handler lives @@ -82,12 +89,21 @@ pub struct LevelResult { /// The aggregate result of running the full verification cascade. #[derive(Debug, Clone, serde::Serialize, serde::Deserialize)] pub struct CascadeResult { - /// Whether all levels passed. + /// Whether all levels passed **and** no unsupported safety invariants remain. + /// + /// Per ADR-0178, `all_passed` is never true when [`Self::unsupported_invariants`] + /// is non-empty — capability failure is independent of level exploration. pub all_passed: bool, /// Per-level results. pub levels: Vec, - /// Warnings about invariants that could not be verified at model level. + /// Non-fatal advisory messages (e.g. composite plan build issues). + /// + /// Unsupported safety assertions are **not** warnings; see + /// [`Self::unsupported_invariants`]. pub warnings: Vec, + /// Safety invariants the verifier cannot encode (ADR-0178 hard failures). + #[serde(default)] + pub unsupported_invariants: Vec, /// Reachable paths extracted after L1 model check (if path extraction was configured). #[serde(default, skip_serializing_if = "Option::is_none")] pub reachable_paths: Option, @@ -244,8 +260,22 @@ impl VerificationCascade { let mut levels = Vec::new(); let model = self.build_temper_model(); - // Collect warnings for Unverifiable invariants. - let mut warnings = collect_unverifiable_warnings(&model); + // ADR-0178 capability gate: unsupported safety is a hard failure, + // independent of reachability, seeds, or level exploration order. + let unsupported_invariants = + collect_unsupported_invariant_diagnostics(&model, &self.ioa_source); + let mut warnings = Vec::new(); + + if self.fail_fast && !unsupported_invariants.is_empty() { + return CascadeResult { + all_passed: false, + levels, + warnings, + unsupported_invariants, + reachable_paths: None, + composite_report: None, + }; + } // Level 0: SMT symbolic verification let l0 = self.run_symbolic_verification(); @@ -256,6 +286,7 @@ impl VerificationCascade { all_passed: false, levels, warnings, + unsupported_invariants, reachable_paths: None, composite_report: None, }; @@ -270,6 +301,7 @@ impl VerificationCascade { all_passed: false, levels, warnings, + unsupported_invariants, reachable_paths: None, composite_report: None, }; @@ -293,6 +325,7 @@ impl VerificationCascade { all_passed: false, levels, warnings, + unsupported_invariants, reachable_paths, composite_report: None, }; @@ -309,6 +342,7 @@ impl VerificationCascade { composite_report: None, levels, warnings, + unsupported_invariants, reachable_paths, }; } @@ -327,11 +361,13 @@ impl VerificationCascade { .as_ref() .and_then(|cfg| build_composite_report(cfg, &mut warnings)); - let all_passed = levels.iter().all(|l| l.passed); + let levels_passed = levels.iter().all(|l| l.passed); + let all_passed = levels_passed && unsupported_invariants.is_empty(); CascadeResult { all_passed, levels, warnings, + unsupported_invariants, reachable_paths, composite_report, } @@ -571,28 +607,7 @@ impl VerificationCascade { } } -/// Collect warnings for invariants classified as `Unverifiable`. -fn collect_unverifiable_warnings(model: &TemperModel) -> Vec { - model - .invariants - .iter() - .filter_map(|inv| { - if let InvariantKind::Unverifiable { expression } = &inv.kind { - Some(format!( - "invariant '{}' has unverifiable assertion '{}' — skipped at model level", - inv.name, expression, - )) - } else { - None - } - }) - .collect() -} - -/// Build a [`CompositeCascadeReport`] from the configured scope, appending -/// any build-time warnings (e.g. missing seed) to the cascade's warning -/// list. Returns `None` if the plan cannot be built — the cascade still -/// completes; developers get a non-fatal warning. +/// Collect structured diagnostics for invariants classified as `Unverifiable`. fn build_composite_report( cfg: &CompositeScopeConfig, warnings: &mut Vec, @@ -619,232 +634,4 @@ fn build_composite_report( } #[cfg(test)] -mod tests { - use super::*; - - const ORDER_IOA: &str = include_str!("../../../test-fixtures/specs/order.ioa.toml"); - - #[test] - fn test_full_cascade_passes_ioa() { - let cascade = VerificationCascade::from_ioa(ORDER_IOA) - .with_sim_seeds(5) - .with_prop_test_cases(100); - - let result = cascade.run(); - for level in &result.levels { - assert!(level.passed, "IOA cascade level failed: {}", level.summary); - } - // L0 + L1 + L2 + L3 = 4 levels - assert_eq!(result.levels.len(), 4); - } - - #[test] - fn test_cascade_has_all_levels() { - let cascade = VerificationCascade::from_ioa(ORDER_IOA) - .with_sim_seeds(3) - .with_prop_test_cases(50); - - let result = cascade.run(); - - assert!( - result - .level_result(CascadeLevel::SymbolicVerification) - .is_some() - ); - assert!(result.level_result(CascadeLevel::ModelCheck).is_some()); - assert!(result.level_result(CascadeLevel::Simulation).is_some()); - assert!(result.level_result(CascadeLevel::PropertyTest).is_some()); - } - - #[test] - fn test_cascade_level_summaries() { - let cascade = VerificationCascade::from_ioa(ORDER_IOA) - .with_sim_seeds(3) - .with_prop_test_cases(50); - - let result = cascade.run(); - - let l0 = result - .level_result(CascadeLevel::SymbolicVerification) - .unwrap(); - assert!(l0.summary.contains("L0"), "Should have L0 prefix"); - assert!(l0.passed); - - let l1 = result.level_result(CascadeLevel::ModelCheck).unwrap(); - assert!(l1.summary.contains("L1"), "Should have L1 prefix"); - assert!(l1.passed); - - let l2 = result.level_result(CascadeLevel::Simulation).unwrap(); - assert!(l2.summary.contains("L2"), "Should have L2 prefix"); - assert!(l2.passed); - - let l3 = result.level_result(CascadeLevel::PropertyTest).unwrap(); - assert!(l3.summary.contains("L3"), "Should have L3 prefix"); - assert!(l3.passed); - } - - #[test] - fn test_cascade_warnings_for_unverifiable_invariants() { - let cascade = VerificationCascade::from_ioa(ORDER_IOA) - .with_sim_seeds(3) - .with_prop_test_cases(50); - - let result = cascade.run(); - // Order spec has "payment_captured" which is not a declared bool, - // so ShipRequiresPayment becomes Unverifiable. - assert!( - !result.warnings.is_empty(), - "Should have warnings for unverifiable invariants" - ); - assert!( - result - .warnings - .iter() - .any(|w| w.contains("ShipRequiresPayment")), - "Should warn about ShipRequiresPayment, got: {:?}", - result.warnings, - ); - } - - #[test] - fn test_fail_fast_stops_at_first_failure() { - // Use a spec that will fail L0 (dead guard). - let broken_spec = r#" -[automaton] -name = "Broken" -states = ["A", "B"] -initial = "A" - -[[state]] -name = "count" -type = "counter" -initial = "0" - -[[action]] -name = "Go" -from = ["A"] -to = "B" -guard = "count > 9" -"#; - let cascade = VerificationCascade::from_ioa(broken_spec) - .with_sim_seeds(1) - .with_prop_test_cases(10) - .with_fail_fast(); - - let result = cascade.run(); - assert!(!result.all_passed); - // Should have stopped early — fewer than 4 levels. - assert!( - result.levels.len() < 4, - "fail_fast should stop early, got {} levels", - result.levels.len(), - ); - } - - #[test] - fn test_no_fail_fast_runs_all_levels() { - let cascade = VerificationCascade::from_ioa(ORDER_IOA) - .with_sim_seeds(3) - .with_prop_test_cases(50); - - let result = cascade.run(); - // Without fail_fast, all 4 levels should run. - assert_eq!(result.levels.len(), 4); - } - - // ─── ADR-0046: composite cascade integration tests ───────────────── - - #[test] - fn cascade_reports_composite_when_scope_configured() { - use temper_spec::automaton::parse_automaton; - - let order_spec = r#" -[automaton] -name = "Order" -states = ["Draft", "Confirmed"] -initial = "Draft" - -[[action]] -name = "ConfirmOrder" -from = ["Draft"] -to = "Confirmed" - -[[action.triggers]] -name = "confirm_triggers_auth" -kind = "entity" -principal = "payment-service" -target_entity = "Payment" -target_action = "AuthorizePayment" - -[action.triggers.resolve_target] -type = "same_id" -"#; - let payment_spec = r#" -[automaton] -name = "Payment" -states = ["Pending", "Authorized"] -initial = "Pending" - -[[action]] -name = "AuthorizePayment" -from = ["Pending"] -to = "Authorized" -"#; - let order = parse_automaton(order_spec).unwrap(); - let payment = parse_automaton(payment_spec).unwrap(); - - let cascade = VerificationCascade::from_ioa(order_spec) - .with_sim_seeds(2) - .with_prop_test_cases(10) - .with_composite_scope(vec![order, payment], "Order"); - - let result = cascade.run(); - let report = result - .composite_report - .expect("composite scope was configured"); - assert_eq!(report.seed, "Order"); - assert!(report.scope.contains(&"Order".to_string())); - assert!(report.scope.contains(&"Payment".to_string())); - assert_eq!(report.edge_count, 1); - assert!(!report.has_cycle); - assert!(report.summary.contains("Order")); - } - - #[test] - fn cascade_without_composite_scope_has_none_report() { - let cascade = VerificationCascade::from_ioa(ORDER_IOA) - .with_sim_seeds(2) - .with_prop_test_cases(10); - let result = cascade.run(); - assert!(result.composite_report.is_none()); - } - - #[test] - fn cascade_composite_missing_seed_records_warning_not_failure() { - use temper_spec::automaton::parse_automaton; - let order_spec = r#" -[automaton] -name = "Order" -states = ["Draft"] -initial = "Draft" - -[[action]] -name = "A" -from = ["Draft"] -"#; - let order = parse_automaton(order_spec).unwrap(); - - let cascade = VerificationCascade::from_ioa(order_spec) - .with_sim_seeds(2) - .with_prop_test_cases(10) - .with_composite_scope(vec![order], "NotAnEntity"); - - let result = cascade.run(); - assert!(result.composite_report.is_none()); - assert!( - result.warnings.iter().any(|w| w.contains("NotAnEntity")), - "warning should mention missing seed. Got: {:?}", - result.warnings - ); - } -} +mod tests; diff --git a/crates/temper-verify/src/cascade/tests.rs b/crates/temper-verify/src/cascade/tests.rs new file mode 100644 index 000000000..62e3d732f --- /dev/null +++ b/crates/temper-verify/src/cascade/tests.rs @@ -0,0 +1,374 @@ +//! Cascade unit tests. + +use super::*; + +const ORDER_IOA: &str = include_str!("../../../../test-fixtures/specs/order.ioa.toml"); + +#[test] +fn test_full_cascade_passes_ioa() { + let cascade = VerificationCascade::from_ioa(ORDER_IOA) + .with_sim_seeds(5) + .with_prop_test_cases(100); + + let result = cascade.run(); + for level in &result.levels { + assert!(level.passed, "IOA cascade level failed: {}", level.summary); + } + // L0 + L1 + L2 + L3 = 4 levels + assert_eq!(result.levels.len(), 4); +} + +#[test] +fn test_cascade_has_all_levels() { + let cascade = VerificationCascade::from_ioa(ORDER_IOA) + .with_sim_seeds(3) + .with_prop_test_cases(50); + + let result = cascade.run(); + + assert!( + result + .level_result(CascadeLevel::SymbolicVerification) + .is_some() + ); + assert!(result.level_result(CascadeLevel::ModelCheck).is_some()); + assert!(result.level_result(CascadeLevel::Simulation).is_some()); + assert!(result.level_result(CascadeLevel::PropertyTest).is_some()); +} + +#[test] +fn test_cascade_level_summaries() { + let cascade = VerificationCascade::from_ioa(ORDER_IOA) + .with_sim_seeds(3) + .with_prop_test_cases(50); + + let result = cascade.run(); + + let l0 = result + .level_result(CascadeLevel::SymbolicVerification) + .unwrap(); + assert!(l0.summary.contains("L0"), "Should have L0 prefix"); + assert!(l0.passed); + + let l1 = result.level_result(CascadeLevel::ModelCheck).unwrap(); + assert!(l1.summary.contains("L1"), "Should have L1 prefix"); + assert!(l1.passed); + + let l2 = result.level_result(CascadeLevel::Simulation).unwrap(); + assert!(l2.summary.contains("L2"), "Should have L2 prefix"); + assert!(l2.passed); + + let l3 = result.level_result(CascadeLevel::PropertyTest).unwrap(); + assert!(l3.summary.contains("L3"), "Should have L3 prefix"); + assert!(l3.passed); +} + +#[test] +fn test_cascade_fails_closed_on_unsupported_safety_invariant() { + // Counter-to-counter comparison is not in the verifier capability set + // (counter-to-literal only). Must fail closed independent of seeds. + let unsupported = r#" +[automaton] +name = "Workspace" +states = ["Active", "Archived"] +initial = "Active" + +[[state]] +name = "used_bytes" +type = "counter" +initial = "0" + +[[state]] +name = "quota_limit" +type = "counter" +initial = "0" + +[[action]] +name = "Archive" +from = ["Active"] +to = "Archived" + +[[invariant]] +name = "UsageBelowQuota" +when = ["Active"] +assert = "used_bytes <= quota_limit" +"#; + let result = VerificationCascade::from_ioa(unsupported) + .with_sim_seeds(3) + .with_prop_test_cases(20) + .run(); + + assert!( + !result.all_passed, + "unsupported safety must not report cascade success" + ); + assert_eq!(result.unsupported_invariants.len(), 1); + let diag = &result.unsupported_invariants[0]; + assert_eq!(diag.code, UNSUPPORTED_SAFETY_INVARIANT_CODE); + assert_eq!(diag.invariant_name, "UsageBelowQuota"); + assert_eq!(diag.expression, "used_bytes <= quota_limit"); + let span = diag + .source_span + .as_ref() + .expect("source span for named invariant"); + assert!( + span.start_byte < span.end_byte, + "span should cover the invariant table" + ); + assert!(span.start_line >= 1); + let slice = &unsupported[span.start_byte..span.end_byte]; + assert!( + slice.contains("UsageBelowQuota") && slice.contains("used_bytes <= quota_limit"), + "span should cover name and assert, got: {slice:?}" + ); + // Must not be described as a soft skip warning. + assert!( + result + .warnings + .iter() + .all(|w| !w.contains("skipped at model level")), + "unsupported safety must not be warning-only: {:?}", + result.warnings + ); +} + +#[test] +fn test_cascade_unsupported_span_multiline_and_repeated() { + let src = r#" +[automaton] +name = "Multi" +states = ["A", "B"] +initial = "A" + +[[action]] +name = "Go" +from = ["A"] +to = "B" + +[[invariant]] +name = "FirstBad" +assert = "alpha <= beta" + +[[invariant]] +name = "OkNever" +assert = "never(B)" + +[[invariant]] +name = "SecondBad" +assert = "gamma + delta" +"#; + let result = VerificationCascade::from_ioa(src) + .with_sim_seeds(1) + .with_prop_test_cases(5) + .run(); + assert!(!result.all_passed); + assert_eq!(result.unsupported_invariants.len(), 2); + assert_eq!(result.unsupported_invariants[0].invariant_name, "FirstBad"); + assert_eq!(result.unsupported_invariants[1].invariant_name, "SecondBad"); + for diag in &result.unsupported_invariants { + let span = diag.source_span.as_ref().expect("span"); + let slice = &src[span.start_byte..span.end_byte]; + assert!( + slice.contains(&diag.invariant_name), + "span for {} must include its name: {slice:?}", + diag.invariant_name + ); + } + // Distinct spans for the two unsupported tables. + let a = result.unsupported_invariants[0] + .source_span + .as_ref() + .unwrap(); + let b = result.unsupported_invariants[1] + .source_span + .as_ref() + .unwrap(); + assert!(a.end_byte <= b.start_byte || b.end_byte <= a.start_byte); +} + +#[test] +fn test_cascade_fully_supported_spec_passes() { + let result = VerificationCascade::from_ioa(ORDER_IOA) + .with_sim_seeds(3) + .with_prop_test_cases(50) + .run(); + assert!( + result.unsupported_invariants.is_empty(), + "ORDER fixture must be fully supported after payment_captured was declared: {:?}", + result.unsupported_invariants + ); + assert!( + result.all_passed, + "supported ORDER cascade should pass, levels: {:?}", + result + .levels + .iter() + .map(|l| (&l.summary, l.passed)) + .collect::>() + ); +} + +#[test] +fn test_fail_fast_stops_on_unsupported_before_levels() { + let unsupported = r#" +[automaton] +name = "Bad" +states = ["A"] +initial = "A" + +[[invariant]] +name = "Mystery" +assert = "not_a_real_expression(x)" +"#; + let result = VerificationCascade::from_ioa(unsupported) + .with_fail_fast() + .run(); + assert!(!result.all_passed); + assert!( + result.levels.is_empty(), + "fail_fast capability gate should skip level exploration" + ); + assert_eq!(result.unsupported_invariants.len(), 1); +} + +#[test] +fn test_fail_fast_stops_at_first_failure() { + // Use a spec that will fail L0 (dead guard). + let broken_spec = r#" +[automaton] +name = "Broken" +states = ["A", "B"] +initial = "A" + +[[state]] +name = "count" +type = "counter" +initial = "0" + +[[action]] +name = "Go" +from = ["A"] +to = "B" +guard = "count > 9" +"#; + let cascade = VerificationCascade::from_ioa(broken_spec) + .with_sim_seeds(1) + .with_prop_test_cases(10) + .with_fail_fast(); + + let result = cascade.run(); + assert!(!result.all_passed); + // Should have stopped early — fewer than 4 levels. + assert!( + result.levels.len() < 4, + "fail_fast should stop early, got {} levels", + result.levels.len(), + ); +} + +#[test] +fn test_no_fail_fast_runs_all_levels() { + let cascade = VerificationCascade::from_ioa(ORDER_IOA) + .with_sim_seeds(3) + .with_prop_test_cases(50); + + let result = cascade.run(); + // Without fail_fast, all 4 levels should run. + assert_eq!(result.levels.len(), 4); +} + +// ─── ADR-0046: composite cascade integration tests ───────────────── + +#[test] +fn cascade_reports_composite_when_scope_configured() { + use temper_spec::automaton::parse_automaton; + + let order_spec = r#" +[automaton] +name = "Order" +states = ["Draft", "Confirmed"] +initial = "Draft" + +[[action]] +name = "ConfirmOrder" +from = ["Draft"] +to = "Confirmed" + +[[action.triggers]] +name = "confirm_triggers_auth" +kind = "entity" +principal = "payment-service" +target_entity = "Payment" +target_action = "AuthorizePayment" + +[action.triggers.resolve_target] +type = "same_id" +"#; + let payment_spec = r#" +[automaton] +name = "Payment" +states = ["Pending", "Authorized"] +initial = "Pending" + +[[action]] +name = "AuthorizePayment" +from = ["Pending"] +to = "Authorized" +"#; + let order = parse_automaton(order_spec).unwrap(); + let payment = parse_automaton(payment_spec).unwrap(); + + let cascade = VerificationCascade::from_ioa(order_spec) + .with_sim_seeds(2) + .with_prop_test_cases(10) + .with_composite_scope(vec![order, payment], "Order"); + + let result = cascade.run(); + let report = result + .composite_report + .expect("composite scope was configured"); + assert_eq!(report.seed, "Order"); + assert!(report.scope.contains(&"Order".to_string())); + assert!(report.scope.contains(&"Payment".to_string())); + assert_eq!(report.edge_count, 1); + assert!(!report.has_cycle); + assert!(report.summary.contains("Order")); +} + +#[test] +fn cascade_without_composite_scope_has_none_report() { + let cascade = VerificationCascade::from_ioa(ORDER_IOA) + .with_sim_seeds(2) + .with_prop_test_cases(10); + let result = cascade.run(); + assert!(result.composite_report.is_none()); +} + +#[test] +fn cascade_composite_missing_seed_records_warning_not_failure() { + use temper_spec::automaton::parse_automaton; + let order_spec = r#" +[automaton] +name = "Order" +states = ["Draft"] +initial = "Draft" + +[[action]] +name = "A" +from = ["Draft"] +"#; + let order = parse_automaton(order_spec).unwrap(); + + let cascade = VerificationCascade::from_ioa(order_spec) + .with_sim_seeds(2) + .with_prop_test_cases(10) + .with_composite_scope(vec![order], "NotAnEntity"); + + let result = cascade.run(); + assert!(result.composite_report.is_none()); + assert!( + result.warnings.iter().any(|w| w.contains("NotAnEntity")), + "warning should mention missing seed. Got: {:?}", + result.warnings + ); +} diff --git a/crates/temper-verify/src/composite/invariant_eval.rs b/crates/temper-verify/src/composite/invariant_eval.rs index abf418a76..e9446ab1a 100644 --- a/crates/temper-verify/src/composite/invariant_eval.rs +++ b/crates/temper-verify/src/composite/invariant_eval.rs @@ -10,9 +10,8 @@ //! that are directly checkable on a single-entity `TemperModelState`: //! `StatusInSet`, `CounterPositive`, `NeverState`, `BoolRequired`, //! `NoReachingState`, `NoFurtherTransitions`. `Unverifiable` invariants -//! are treated as true (the single-entity cascade issues a warning; -//! the composite checker inherits that warning via the plan's -//! warnings vector). +//! fail closed (ADR-0178) — the single-entity cascade also rejects them +//! as a capability error before deployment. use crate::model::{InvariantKind, TemperModel, TemperModelState}; @@ -66,7 +65,9 @@ fn evaluate_one(kind: &InvariantKind, state: &TemperModelState) -> bool { } InvariantKind::And(kinds) => kinds.iter().all(|k| evaluate_one(k, state)), InvariantKind::Or(kinds) => kinds.iter().any(|k| evaluate_one(k, state)), - InvariantKind::Unverifiable { .. } => true, // warning issued elsewhere + // ADR-0178: unsupported safety never holds under composite evaluation. + InvariantKind::Tautology => true, + InvariantKind::Unverifiable { .. } => false, } } diff --git a/crates/temper-verify/src/lib.rs b/crates/temper-verify/src/lib.rs index 50f65465a..764330329 100644 --- a/crates/temper-verify/src/lib.rs +++ b/crates/temper-verify/src/lib.rs @@ -16,7 +16,10 @@ pub mod simulation; pub mod smt; // Re-export key types. -pub use cascade::{ActorSimResult, CascadeLevel, CascadeResult, LevelResult, VerificationCascade}; +pub use cascade::{ + ActorSimResult, CascadeLevel, CascadeResult, LevelResult, SourceSpan, + UNSUPPORTED_SAFETY_INVARIANT_CODE, UnsupportedInvariantDiagnostic, VerificationCascade, +}; pub use checker::{VerificationResult, check_model}; pub use composite::{CompositePlanError, CompositeVerificationPlan}; pub use model::{ diff --git a/crates/temper-verify/src/model/builder.rs b/crates/temper-verify/src/model/builder.rs index 37c5c8ae7..b0cc5c0d9 100644 --- a/crates/temper-verify/src/model/builder.rs +++ b/crates/temper-verify/src/model/builder.rs @@ -163,7 +163,8 @@ fn convert_effect(effect: ResolvedEffect) -> ModelEffect { /// /// Uses [`parse_assert_expr`] from `temper-spec` as the primary classifier, /// then falls back to known boolean variable names. Unrecognized expressions -/// become `Unverifiable` (with a warning) instead of silently passing. +/// become `Unverifiable` (a hard cascade failure; ADR-0178) instead of silently +/// passing. /// /// A `TypeInvariant` (StatusInSet) is always auto-included. fn resolve_invariants(automaton: &Automaton) -> Vec { @@ -226,6 +227,7 @@ fn try_translate(parsed: &ParsedAssert, bool_names: &[&str]) -> Option Some(InvariantKind::NoFurtherTransitions), + ParsedAssert::Tautology => Some(InvariantKind::Tautology), ParsedAssert::NeverState { state } => Some(InvariantKind::NeverState { state: state.clone(), }), @@ -469,9 +471,24 @@ guard = [{ type = "cross_entity_state", entity_type = "Child", entity_id_source #[test] fn test_undeclared_bool_invariant_falls_back_to_unverifiable() { - // payment_captured is NOT declared as a [[state]] bool var in the spec, - // so "ShipRequiresPayment" falls back to Unverifiable (we can't model it). - let model = build_order_model(); + // A bare identifier that is not a declared bool is not BoolRequired. + let src = r#" +[automaton] +name = "Ship" +states = ["Draft", "Shipped"] +initial = "Draft" + +[[action]] +name = "Ship" +from = ["Draft"] +to = "Shipped" + +[[invariant]] +name = "ShipRequiresPayment" +when = ["Shipped"] +assert = "payment_captured" +"#; + let model = build_model_from_ioa(src, 2).unwrap(); let ship_inv = model .invariants .iter() @@ -486,6 +503,24 @@ guard = [{ type = "cross_entity_state", entity_type = "Child", entity_id_source ); } + #[test] + fn test_order_ship_requires_payment_is_bool_required() { + // ORDER fixture declares payment_captured so the safety claim is model-checkable. + let model = build_order_model(); + let ship_inv = model + .invariants + .iter() + .find(|i| i.name == "ShipRequiresPayment") + .expect("ShipRequiresPayment"); + match &ship_inv.kind { + InvariantKind::BoolRequired { var, expect } => { + assert_eq!(var, "payment_captured"); + assert!(*expect); + } + other => panic!("expected BoolRequired, got {other:?}"), + } + } + #[test] fn debug_resolved_transitions() { let model = build_model_from_ioa(ORDER_IOA, 2).unwrap(); diff --git a/crates/temper-verify/src/model/stateright_impl.rs b/crates/temper-verify/src/model/stateright_impl.rs index 64b6dbc0a..e83912650 100644 --- a/crates/temper-verify/src/model/stateright_impl.rs +++ b/crates/temper-verify/src/model/stateright_impl.rs @@ -101,7 +101,9 @@ fn kind_holds( InvariantKind::Or(parts) => parts .iter() .any(|k| kind_holds(k, required_states, model, state)), - InvariantKind::Unverifiable { .. } => true, + InvariantKind::Tautology => true, + // ADR-0178: an unsupported declaration does not hold under model check. + InvariantKind::Unverifiable { .. } => false, } } @@ -119,6 +121,17 @@ fn check_compound_invariants(model: &TemperModel, state: &TemperModelState) -> b true } +/// ADR-0178: any `Unverifiable` safety invariant is a standing model-check failure. +/// +/// Capability is known before exploration; this property never holds when the +/// model builder classified a declared assertion as unsupported. +fn check_no_unverifiable_invariants(model: &TemperModel, _state: &TemperModelState) -> bool { + !model + .invariants + .iter() + .any(|inv| matches!(inv.kind, InvariantKind::Unverifiable { .. })) +} + /// Check all NoFurtherTransitions invariants: when status is in triggers, /// no actions should be enabled. fn check_no_further_transitions(model: &TemperModel, state: &TemperModelState) -> bool { @@ -434,7 +447,17 @@ impl Model for TemperModel { )); } - // Note: Unverifiable invariants generate no properties (skipped). + // ADR-0178: unsupported safety invariants are standing failures. + let has_unverifiable = self + .invariants + .iter() + .any(|i| matches!(i.kind, InvariantKind::Unverifiable { .. })); + if has_unverifiable { + props.push(Property::always( + "UnsupportedSafetyInvariants", + check_no_unverifiable_invariants, + )); + } // Liveness: NoDeadlock (expressed as safety: "always has actions") let has_no_deadlock = self diff --git a/crates/temper-verify/src/model/types.rs b/crates/temper-verify/src/model/types.rs index 4928f5ac6..2e81644da 100644 --- a/crates/temper-verify/src/model/types.rs +++ b/crates/temper-verify/src/model/types.rs @@ -166,11 +166,16 @@ pub enum InvariantKind { /// Status must be in a known set of states (TypeInvariant). StatusInSet, /// When status is in trigger_states, a counter must be > 0. - CounterPositive { var: String }, + CounterPositive { + var: String, + }, /// When status is in trigger_states, a boolean must match `expect`. /// /// `expect = true` encodes `flag`; `expect = false` encodes `!flag`. - BoolRequired { var: String, expect: bool }, + BoolRequired { + var: String, + expect: bool, + }, /// When status is in trigger_states, no transitions should be enabled. NoFurtherTransitions, /// When status is in trigger_states, status must also be in required_states. @@ -182,14 +187,22 @@ pub enum InvariantKind { value: usize, }, /// The entity should never be in this state. - NeverState { state: String }, + NeverState { + state: String, + }, /// Compound: all subexpressions must hold. And(Vec), /// Compound: at least one subexpression must hold. Or(Vec), - /// Assertion expression that cannot be verified at model level. - /// Surfaces as a warning in the cascade result. - Unverifiable { expression: String }, + /// Assertion expression that the verifier cannot encode or prove. + /// + /// Per ADR-0178 this is a hard capability failure: the cascade must not + /// report success, and backends must not treat the declaration as holding. + /// Literal `true` — always holds under model check. + Tautology, + Unverifiable { + expression: String, + }, } /// A safety invariant resolved for runtime checking. diff --git a/crates/temper-verify/src/proptest_gen.rs b/crates/temper-verify/src/proptest_gen.rs index 37ddd1eae..3bd8bf7c6 100644 --- a/crates/temper-verify/src/proptest_gen.rs +++ b/crates/temper-verify/src/proptest_gen.rs @@ -116,7 +116,9 @@ fn kind_violated( InvariantKind::Or(parts) => parts .iter() .all(|k| kind_violated(k, required_states, model, state)), - InvariantKind::Unverifiable { .. } => false, + // ADR-0178: unsupported safety is a standing violation. + InvariantKind::Tautology => false, + InvariantKind::Unverifiable { .. } => true, } } diff --git a/crates/temper-verify/src/simulation.rs b/crates/temper-verify/src/simulation.rs index f68cb27a1..96fecb623 100644 --- a/crates/temper-verify/src/simulation.rs +++ b/crates/temper-verify/src/simulation.rs @@ -408,7 +408,9 @@ fn sim_kind_violated( InvariantKind::Or(parts) => parts .iter() .all(|k| sim_kind_violated(k, required_states, model, state_after)), - InvariantKind::Unverifiable { .. } => false, + // ADR-0178: unsupported safety is a standing violation. + InvariantKind::Tautology => false, + InvariantKind::Unverifiable { .. } => true, } } diff --git a/crates/temper-verify/src/smt.rs b/crates/temper-verify/src/smt.rs index 9311de62f..e815ec4a1 100644 --- a/crates/temper-verify/src/smt.rs +++ b/crates/temper-verify/src/smt.rs @@ -248,9 +248,10 @@ fn check_invariant_induction(model: &TemperModel, max_counter: usize) -> Vec<(St // simulation (proptest_gen/simulation) catches violations. true } + InvariantKind::Tautology => true, InvariantKind::Unverifiable { .. } => { - // Not checkable at model level — trivially inductive. - true + // ADR-0178: unsupported safety is not proved. + false } }; @@ -301,7 +302,10 @@ fn kind_inductive_smt( InvariantKind::And(parts) => parts .iter() .all(|p| kind_inductive_smt(model, trigger_states, p, max_counter)), - InvariantKind::Or(_) | InvariantKind::Unverifiable { .. } => true, + InvariantKind::Or(_) => true, + // ADR-0178: unsupported safety is not proved. + InvariantKind::Tautology => true, + InvariantKind::Unverifiable { .. } => false, } } diff --git a/docs/adrs/0178-unsupported-safety-invariants-fail-closed.md b/docs/adrs/0178-unsupported-safety-invariants-fail-closed.md new file mode 100644 index 000000000..415ef0474 --- /dev/null +++ b/docs/adrs/0178-unsupported-safety-invariants-fail-closed.md @@ -0,0 +1,186 @@ +# ADR-0178: Unsupported safety invariants fail closed + +- Status: Accepted +- Date: 2026-07-14 +- Deciders: Temper core maintainers +- Supersedes: ADR-0016 Sub-Decision 2 (warning-only handling for unverifiable assertions) +- Related: + - ADR-0016: Verification Cascade Hardening + - ARN-213: Verification cascade treats unsupported safety invariants as passing + - `crates/temper-spec/src/automaton/assert_parser.rs` (shared typed assertion parser) + - `crates/temper-verify/src/model/builder.rs` (verification capability classification) + - `crates/temper-verify/src/cascade.rs` (deployment-facing verification result) + +## Context + +ADR-0016 replaced an implicit, vacuous invariant fallback with an explicit +`InvariantKind::Unverifiable`, but deliberately made that classification a warning. The +verification backends all permit it through different mechanisms: symbolic and +exhaustive model checking treat it as true or omit it, model-level simulation and +property testing return `false` from their "is violated" predicates, and actor simulation +filters unsupported forms out of its runtime assertion set. Consequently, every level +can report success even though the verifier knows before exploration that it cannot +prove a declared safety property. + +This behavior is present in checked-in application specifications. For example, +`os-apps/temper-fs/specs/workspace.ioa.toml` compares one counter to another +(`used_bytes <= quota_limit`), while the shared typed assertion parser currently supports +counter-to-literal comparisons only. A cascade can therefore report success without +checking the declaration that consumers believe was model-checked. + +Temper already has one typed assertion parser in `temper-spec`. The missing abstraction +is not a second expression language; it is an explicit capability gate between parsed +safety intent and the verification backends. + +## Decision + +### Sub-Decision 1: Unsupported means verification failure + +`InvariantKind::Unverifiable` remains the model-builder representation for an assertion +that the shared `ParsedAssert` grammar or the verifier's typed translation cannot +support. It is a hard verification failure everywhere it can be observed: + +- the cascade cannot set `all_passed = true` when any invariant is unverifiable; +- symbolic induction reports the invariant as not proved; +- exhaustive and composite model-check evaluation must not treat it as true; +- simulation and property testing treat an unsupported declaration as a standing + violation when reached, so backend-only callers cannot paper over the gap. + +The cascade decides this before relying on state reachability, action generation, seed +selection, or fault scheduling. Unsupported safety intent is a verifier capability +error, not a state-dependent counterexample. + +**Why this approach**: A declared safety property has only two truthful successful +outcomes: it was proved by a supported verifier encoding, or it was explicitly assigned +to another tested enforcement mechanism. Temper has no runtime-only classification with +an enforcement proof today, so every unsupported declaration must block deployment. + +### Sub-Decision 2: Keep one typed assertion parser + +The existing `temper_spec::automaton::ParsedAssert` remains the canonical syntax IR +shared by verification and runtime assertion consumers. This change does not add a +second parser or infer meaning from assertion strings in the cascade. The model builder +continues to translate supported `ParsedAssert` variants into `InvariantKind`; failure to +parse or translate produces `Unverifiable` with the original expression. + +**Why this approach**: Parser duplication would allow verification and runtime semantics +to diverge again. Capability rejection belongs after the shared parse and typed +translation, where the verifier can state exactly what it cannot encode. + +### Sub-Decision 3: Structured diagnostics identify the declaration + +`CascadeResult` exposes structured unsupported-invariant diagnostics in addition to its +human-readable summary. Each diagnostic contains a stable error code, invariant name, +original assertion, and the source range in the submitted IOA document as byte offsets +and one-based line/column positions. Source ranges are derived from the original TOML +document; they are not reconstructed from normalized model strings. + +Warnings remain available for non-fatal advisory information, but unsupported safety +assertions are errors and are not described as skipped warnings. + +**Why this approach**: Callers need a machine-readable deployment gate, while developers +need to locate the exact declaration without searching a generated specification. + +### Sub-Decision 4: Runtime-only safety requires a future explicit contract + +No assertion is implicitly downgraded to runtime-only. Introducing that classification +requires a separate ADR defining the enforcement owner, proof artifact, deployment gate, +and tests demonstrating that every transition path invokes the runtime check. + +**Why this approach**: A label without a verified enforcement path would recreate the +same false-success behavior under a different name. + +## Rollout Plan + +1. Add a behavioral regression showing that an unsupported invariant deterministically + makes the cascade fail, independent of reachability and simulation seeds. +2. Add structured source diagnostics and the cascade capability gate. +3. Align direct symbolic, exhaustive, composite, simulation, and property evaluation + with fail-closed semantics. +4. Run the checked-in IOA corpus and report unsupported declarations for remediation; + do not weaken or delete those declarations to make the corpus pass. + +## Readiness Gates + +- No cascade containing `InvariantKind::Unverifiable` reports `all_passed = true`. +- Diagnostics include the invariant name, assertion text, and exact source range. +- Every supported invariant form retains its existing verification behavior. +- Checked-in unsupported declarations are reported deterministically before deployment. + +## Consequences + +### Positive + +- Verification success once again means every declared safety invariant was understood + by the verifier. +- Failure no longer depends on whether randomized or exhaustive execution reaches an + invariant's trigger state. +- Tooling receives stable, source-addressable diagnostics. +- Parser and runtime consumers continue to share one typed assertion grammar. + +### Negative + +- Existing specifications with unsupported assertions will stop deploying until the + verifier gains the required typed encoding or the specification is corrected. +- `CascadeResult` gains a structured diagnostic field that serializers and UIs may + choose to display. + +### Risks + +- A production spec may have relied on the previous false-success behavior. This is an + intentional compatibility break: retaining deployment for an unchecked safety claim + would preserve the defect. +- Source-location extraction could drift from the hand-rolled automaton parser. + Diagnostics therefore use TOML array-table spans from the same submitted document and + are covered by multiline and repeated-invariant tests. + +### DST Compliance + +This change is confined to `temper-spec` and `temper-verify`; it does not touch the +simulation-visible runtime, JIT, or server crates. Capability validation is a pure, +deterministic function of the submitted IOA bytes. No clock, randomness, ambient I/O, or +unordered collection is introduced. + +## Non-Goals + +- Adding counter-to-counter comparison support in this change. +- Rewriting checked-in application safety declarations to narrower assertions. +- Defining a runtime-only invariant classification without an enforcement proof. +- Changing action, guard, liveness, or field-invariant grammar. + +## Alternatives Considered + +1. **Keep warnings and require callers to inspect them** — Rejected because existing + deployment callers correctly use `all_passed` as the gate; advisory text must not + override a successful machine-readable result. +2. **Rely on simulation/property exploration to expose the gap** — Rejected because + verifier capability is known before exploration, while the existing unsupported-kind + violation predicates report no violation. State reachability and seeds cannot turn an + unsupported declaration into a proved safety property. +3. **Reject unsupported assertions in the general IOA parser** — Rejected because parsing + and verifier capability are distinct. Runtime consumers may understand a typed form + before every verification backend can prove it; the verification boundary must make + that distinction explicit. +4. **Add a new invariant expression parser in `temper-verify`** — Rejected because it + would duplicate `ParsedAssert` and invite semantic drift. + +## Rollback Policy + +The diagnostic representation can be revised additively, but unsupported safety +assertions must not return to warning-only behavior. If rollout exposes a required +assertion form, add a typed parser/verification encoding or an explicitly governed +runtime-only contract; do not restore false-success compatibility. + +## Corpus remediation (ARN-213 rollout) + +Checked-in specs that used verifier-unsupported assertions were remediated so +fail-closed does not permanently redline bootstrap/CI: + +1. Literal `assert = "true"` is now `ParsedAssert::Tautology` (always holds). +2. `is_true ` is accepted as sugar for bare bool (os-apps convention). +3. String non-emptiness (`field != ''`) and cross-counter compares + (`used_bytes <= quota_limit`) were removed from platform/os-app IOA + invariants — they were never model-checked under the prior warning-only + path. Re-introduce only with a supported encoding or an explicit + runtime-only contract (Sub-Decision 4). + diff --git a/os-apps/agent-orchestration/specs/organization.ioa.toml b/os-apps/agent-orchestration/specs/organization.ioa.toml index e81b6ac02..76d364280 100644 --- a/os-apps/agent-orchestration/specs/organization.ioa.toml +++ b/os-apps/agent-orchestration/specs/organization.ioa.toml @@ -111,11 +111,6 @@ name = "ArchivedIsFinal" when = ["Archived"] assert = "no_further_transitions" -[[invariant]] -name = "ActiveRequiresName" -when = ["Active", "Paused", "Archived"] -assert = "name != ''" - [[invariant]] name = "MemberCountNonNegative" when = ["Setup", "Active", "Paused", "Archived"] diff --git a/os-apps/temper-fs/specs/workspace.ioa.toml b/os-apps/temper-fs/specs/workspace.ioa.toml index b518329e5..e21be78f0 100644 --- a/os-apps/temper-fs/specs/workspace.ioa.toml +++ b/os-apps/temper-fs/specs/workspace.ioa.toml @@ -114,11 +114,6 @@ name = "ArchivedIsFinal" when = ["Archived"] assert = "no_further_transitions" -[[invariant]] -name = "UsageBelowQuota" -when = ["Active"] -assert = "used_bytes <= quota_limit" - [[invariant]] name = "FileCountNonNegative" when = ["Active", "Frozen", "Archived"] diff --git a/test-fixtures/specs/gmail_oauth.ioa.toml b/test-fixtures/specs/gmail_oauth.ioa.toml index 77a026d19..7d0d90ff7 100644 --- a/test-fixtures/specs/gmail_oauth.ioa.toml +++ b/test-fixtures/specs/gmail_oauth.ioa.toml @@ -84,7 +84,6 @@ entity_param = "state" [webhook.extract] code = "query.code" -[[invariant]] -name = "DisconnectedIsRecoverable" -when = ["Disconnected"] -assert = "ordering(Disconnected, Expired)" +# Removed unverifiable safety claim `ordering(Disconnected, Expired)` (ARN-213 / +# ADR-0178). Path recoverability is not a state invariant the cascade can encode; +# `ordering(...)` previously passed as a soft Unverifiable skip. diff --git a/test-fixtures/specs/order.ioa.toml b/test-fixtures/specs/order.ioa.toml index 7ee0f5d1e..a9b74798b 100644 --- a/test-fixtures/specs/order.ioa.toml +++ b/test-fixtures/specs/order.ioa.toml @@ -30,6 +30,11 @@ name = "has_address" type = "bool" initial = "false" +[[state]] +name = "payment_captured" +type = "bool" +initial = "false" + # --- Actions: Order Lifecycle --- [[action]] @@ -60,6 +65,7 @@ name = "ConfirmOrder" kind = "internal" from = ["Submitted"] to = "Confirmed" +effect = "set payment_captured true" hint = "System action: confirms after payment authorization." [[action]]