From 3329aabcd2c0f75090ac16f80d12af36ebab2f65 Mon Sep 17 00:00:00 2001 From: Larri Date: Thu, 30 Jul 2026 17:04:19 -0600 Subject: [PATCH 1/6] feat: add DD-078 obligation truth model --- src/intent.rs | 422 +++++++++++++++++- src/lib.rs | 1 + src/verification/ids.rs | 212 +++++++++ src/verification/mod.rs | 14 + src/verification/model.rs | 305 +++++++++++++ .../truth/compatibility_derived_ids.intent | 5 + .../truth/documentation_only.intent | 5 + .../truth/duplicate_feature_ids.intent | 5 + .../truth/duplicate_outcome_ids.intent | 8 + .../truth/duplicate_scenario_ids.intent | 12 + .../truth/linked_unexecuted.intent | 7 + .../truth/malformed_feature_id.intent | 2 + .../truth/malformed_outcome_id.intent | 7 + .../truth/malformed_scenario_id.intent | 7 + .../truth/outcome_documentation_only.intent | 7 + .../truth/zero_outcome_behavioral.intent | 3 + tests/verification_truth_tests.rs | 233 ++++++++++ 17 files changed, 1242 insertions(+), 13 deletions(-) create mode 100644 src/verification/ids.rs create mode 100644 src/verification/mod.rs create mode 100644 src/verification/model.rs create mode 100644 tests/fixtures/verification/truth/compatibility_derived_ids.intent create mode 100644 tests/fixtures/verification/truth/documentation_only.intent create mode 100644 tests/fixtures/verification/truth/duplicate_feature_ids.intent create mode 100644 tests/fixtures/verification/truth/duplicate_outcome_ids.intent create mode 100644 tests/fixtures/verification/truth/duplicate_scenario_ids.intent create mode 100644 tests/fixtures/verification/truth/linked_unexecuted.intent create mode 100644 tests/fixtures/verification/truth/malformed_feature_id.intent create mode 100644 tests/fixtures/verification/truth/malformed_outcome_id.intent create mode 100644 tests/fixtures/verification/truth/malformed_scenario_id.intent create mode 100644 tests/fixtures/verification/truth/outcome_documentation_only.intent create mode 100644 tests/fixtures/verification/truth/zero_outcome_behavioral.intent create mode 100644 tests/verification_truth_tests.rs diff --git a/src/intent.rs b/src/intent.rs index 8d48234..03b9d01 100644 --- a/src/intent.rs +++ b/src/intent.rs @@ -45,6 +45,7 @@ use crate::ial::{self, standard_vocabulary, Context as IalContext, Term, Vocabul use crate::interpreter::Interpreter; use crate::lexer::Lexer; use crate::parser::Parser as IntentParser; +use crate::verification::ids::{IdKind, IdMode, IdOrigin, IdWarning, SourceSpan, StableId}; // ============================================================================ // GLOSSARY SYSTEM (IAL Core) @@ -2187,9 +2188,33 @@ pub struct Invariant { // SCENARIO SYSTEM (Natural Language Tests) // ============================================================================ +/// Feature-level verification declaration. Documentation-only is deliberately +/// unavailable on scenarios and outcomes. +#[derive(Debug, Clone, PartialEq, Eq, Serialize)] +pub enum FeatureVerification { + Behavioral, + DocumentationOnly { rationale: String }, +} + +/// Stable identity and location paired with an existing outcome string. +#[derive(Debug, Clone, PartialEq, Eq, Serialize)] +pub struct OutcomeMetadata { + pub id: StableId, + pub source: SourceSpan, +} + /// A natural language scenario that can be executed as a test #[derive(Debug, Clone, Serialize)] pub struct Scenario { + /// Explicit source spelling, absent for compatibility-derived IDs. + #[serde(skip)] + pub id: Option, + #[serde(skip)] + pub verification_id: StableId, + #[serde(skip)] + pub verification_id_source: SourceSpan, + #[serde(skip)] + pub source: SourceSpan, /// Scenario name (e.g., "Successful login") pub name: String, /// Optional description explaining why this scenario exists @@ -2202,6 +2227,9 @@ pub struct Scenario { pub when_clause: String, /// The outcome clauses (each "→" line) pub outcomes: Vec, + /// Stable IDs and locations corresponding one-for-one with `outcomes`. + #[serde(skip)] + pub outcome_metadata: Vec, /// Resolved test case (after glossary term resolution) #[serde(skip_serializing_if = "Option::is_none")] pub resolved_test: Option, @@ -2654,8 +2682,16 @@ pub struct TestCase { #[derive(Debug, Clone, Serialize)] pub struct Feature { pub id: Option, + #[serde(skip)] + pub verification_id: StableId, + #[serde(skip)] + pub verification_id_source: SourceSpan, + #[serde(skip)] + pub source: SourceSpan, pub name: String, pub description: Option, + #[serde(skip)] + pub verification: FeatureVerification, /// Traditional test cases (technical format) pub tests: Vec, /// Natural language scenarios (IAL format) @@ -2683,6 +2719,9 @@ pub struct IntentFile { /// Test data sections (for unit testing) #[serde(skip_serializing_if = "Vec::is_empty")] pub test_data: Vec, + /// Source-located warnings emitted only for compatibility-derived IDs. + #[serde(skip)] + pub verification_warnings: Vec, } /// A section of test data linked to a feature/scenario @@ -2788,13 +2827,18 @@ pub struct FeatureCoverage { } impl IntentFile { - /// Parse an intent file from a path + /// Parse an intent file from a path while preserving legacy behavior. pub fn parse(path: &Path) -> Result { + Self::parse_with_id_mode(path, IdMode::Compatibility) + } + + /// Parse an intent file with explicit stable-ID policy. + pub fn parse_with_id_mode(path: &Path, id_mode: IdMode) -> Result { let content = fs::read_to_string(path).map_err(|e| { IntentError::runtime_error(format!("Failed to read intent file: {}", e)) })?; - Self::parse_content(&content, path.to_string_lossy().to_string()) + Self::parse_content_with_id_mode(&content, path.to_string_lossy().to_string(), id_mode) } /// Look up test data by ID. @@ -2847,8 +2891,17 @@ impl IntentFile { .collect() } - /// Parse intent file content + /// Parse intent file content while preserving legacy behavior. pub fn parse_content(content: &str, source_path: String) -> Result { + Self::parse_content_with_id_mode(content, source_path, IdMode::Compatibility) + } + + /// Parse intent file content with explicit stable-ID policy. + pub fn parse_content_with_id_mode( + content: &str, + source_path: String, + id_mode: IdMode, + ) -> Result { let mut features = Vec::new(); let mut components = Vec::new(); let mut invariants: Vec = Vec::new(); @@ -2874,7 +2927,8 @@ impl IntentFile { let mut current_binding_term: Option<(String, TechnicalBinding)> = None; let mut in_binding_assert_list = false; - for line in content.lines() { + for (line_index, line) in content.lines().enumerate() { + let line_number = line_index + 1; let trimmed = line.trim(); // Skip empty lines @@ -3122,10 +3176,19 @@ impl IntentFile { } let name = trimmed.trim_start_matches("Feature:").trim().to_string(); + let source = Self::line_span(&source_path, line_number, line, "Feature:"); current_feature = Some(Feature { id: None, + verification_id: StableId::compatibility_derived( + IdKind::Feature, + &[&name], + features.len(), + ), + verification_id_source: source.clone(), + source, name, description: None, + verification: FeatureVerification::Behavioral, tests: Vec::new(), scenarios: Vec::new(), }); @@ -3371,7 +3434,7 @@ impl IntentFile { // Inside a component if let Some(ref mut component) = current_component { // Component ID - if trimmed.starts_with("id:") { + if trimmed.starts_with("id:") && current_scenario.is_none() { let id = trimmed.trim_start_matches("id:").trim(); component.id = id.to_string(); continue; @@ -3415,12 +3478,22 @@ impl IntentFile { } let name = trimmed.trim_start_matches("Scenario:").trim().to_string(); + let source = Self::line_span(&source_path, line_number, line, "Scenario:"); current_scenario = Some(Scenario { + id: None, + verification_id: StableId::compatibility_derived( + IdKind::Scenario, + &[&component.name, &name], + component.scenarios.len(), + ), + verification_id_source: source.clone(), + source, name, description: None, given_clause: None, when_clause: String::new(), outcomes: Vec::new(), + outcome_metadata: Vec::new(), resolved_test: None, component_refs: Vec::new(), }); @@ -3429,6 +3502,16 @@ impl IntentFile { // Inside component scenario if let Some(ref mut scenario) = current_scenario { + if trimmed.starts_with("id:") { + let id = trimmed.trim_start_matches("id:").trim(); + let id_source = Self::line_span(&source_path, line_number, line, "id:"); + scenario.id = Some(id.to_string()); + scenario.verification_id = + Self::explicit_id(id, IdKind::Scenario, &id_source)?; + scenario.verification_id_source = id_source; + continue; + } + // Description if trimmed.starts_with("description:") { let desc = trimmed.trim_start_matches("description:").trim(); @@ -3451,12 +3534,20 @@ impl IntentFile { // Outcome clause if trimmed.starts_with("→") || trimmed.starts_with("->") { - let outcome = trimmed + let raw_outcome = trimmed .trim_start_matches("→") .trim_start_matches("->") - .trim() - .to_string(); + .trim(); + let (outcome, metadata) = Self::parse_outcome( + &source_path, + line_number, + line, + raw_outcome, + &scenario.name, + scenario.outcomes.len(), + )?; scenario.outcomes.push(outcome); + scenario.outcome_metadata.push(metadata); continue; } } @@ -3479,10 +3570,61 @@ impl IntentFile { // Inside a feature if let Some(ref mut feature) = current_feature { - // Feature ID + // Scenario ID must be handled before the enclosing feature ID. if trimmed.starts_with("id:") { let id = trimmed.trim_start_matches("id:").trim(); - feature.id = Some(id.to_string()); + let id_source = Self::line_span(&source_path, line_number, line, "id:"); + if let Some(scenario) = current_scenario.as_mut() { + scenario.id = Some(id.to_string()); + scenario.verification_id = + Self::explicit_id(id, IdKind::Scenario, &id_source)?; + scenario.verification_id_source = id_source; + } else { + feature.verification_id = + Self::explicit_id(id, IdKind::Feature, &id_source)?; + feature.verification_id_source = id_source; + feature.id = Some(id.to_string()); + } + continue; + } + + if trimmed.starts_with("verification:") { + if current_scenario.is_some() { + return Err(Self::verification_error( + &Self::line_span(&source_path, line_number, line, "verification:"), + "documentation-only is valid only on a feature", + )); + } + let value = trimmed.trim_start_matches("verification:").trim(); + if value != "documentation-only" { + return Err(Self::verification_error( + &Self::line_span(&source_path, line_number, line, "verification:"), + format!("unknown feature verification declaration '{value}'"), + )); + } + feature.verification = FeatureVerification::DocumentationOnly { + rationale: String::new(), + }; + continue; + } + + if trimmed.starts_with("rationale:") && current_scenario.is_none() { + let rationale = trimmed + .trim_start_matches("rationale:") + .trim() + .trim_matches('"') + .to_string(); + match &mut feature.verification { + FeatureVerification::DocumentationOnly { + rationale: feature_rationale, + } => *feature_rationale = rationale, + FeatureVerification::Behavioral => { + return Err(Self::verification_error( + &Self::line_span(&source_path, line_number, line, "rationale:"), + "rationale requires 'verification: documentation-only'", + )); + } + } continue; } @@ -3507,12 +3649,22 @@ impl IntentFile { } let name = trimmed.trim_start_matches("Scenario:").trim().to_string(); + let source = Self::line_span(&source_path, line_number, line, "Scenario:"); current_scenario = Some(Scenario { + id: None, + verification_id: StableId::compatibility_derived( + IdKind::Scenario, + &[&feature.name, &name], + feature.scenarios.len(), + ), + verification_id_source: source.clone(), + source, name, description: None, given_clause: None, when_clause: String::new(), outcomes: Vec::new(), + outcome_metadata: Vec::new(), resolved_test: None, component_refs: Vec::new(), }); @@ -3544,12 +3696,20 @@ impl IntentFile { // Outcome clause (→ or ->) if trimmed.starts_with("→") || trimmed.starts_with("->") { - let outcome = trimmed + let raw_outcome = trimmed .trim_start_matches("→") .trim_start_matches("->") - .trim() - .to_string(); + .trim(); + let (outcome, metadata) = Self::parse_outcome( + &source_path, + line_number, + line, + raw_outcome, + &scenario.name, + scenario.outcomes.len(), + )?; scenario.outcomes.push(outcome); + scenario.outcome_metadata.push(metadata); continue; } } @@ -3653,6 +3813,14 @@ impl IntentFile { test_data_sections.push(td); } + let mut verification_warnings = Vec::new(); + Self::finalize_verification_ids( + &features, + &components, + id_mode, + &mut verification_warnings, + )?; + Ok(IntentFile { features, source_path, @@ -3661,9 +3829,221 @@ impl IntentFile { components, invariants, test_data: test_data_sections, + verification_warnings, }) } + fn line_span(source_path: &str, line_number: usize, line: &str, marker: &str) -> SourceSpan { + let start_column = line + .find(marker) + .map_or(1, |byte_index| line[..byte_index].chars().count() + 1); + SourceSpan::single_line( + source_path, + line_number, + start_column, + line.chars().count() + 1, + ) + } + + fn verification_error(span: &SourceSpan, message: impl AsRef) -> IntentError { + IntentError::runtime_error(format!("{}: {}", span.location(), message.as_ref())) + } + + fn explicit_id( + value: &str, + kind: IdKind, + source: &SourceSpan, + ) -> Result { + StableId::explicit(value, kind).map_err(|reason| { + Self::verification_error(source, format!("malformed {kind} ID '{value}': {reason}")) + }) + } + + fn parse_outcome( + source_path: &str, + line_number: usize, + line: &str, + raw_outcome: &str, + scenario_name: &str, + ordinal: usize, + ) -> Result<(String, OutcomeMetadata), IntentError> { + let source = Self::line_span(source_path, line_number, line, "id:"); + if raw_outcome.contains("verification: documentation-only") { + return Err(Self::verification_error( + &source, + "documentation-only is valid only on a feature", + )); + } + + let (statement, id) = if let Some(id_declaration) = raw_outcome.strip_prefix("id:") { + let Some((id, statement)) = id_declaration.split_once(';') else { + return Err(Self::verification_error( + &source, + "outcome ID must be followed by ';' and an outcome statement", + )); + }; + let id = id.trim(); + let statement = statement.trim(); + if statement.is_empty() { + return Err(Self::verification_error( + &source, + "outcome statement must not be empty", + )); + } + ( + statement.to_string(), + Self::explicit_id(id, IdKind::Outcome, &source)?, + ) + } else { + ( + raw_outcome.to_string(), + StableId::compatibility_derived( + IdKind::Outcome, + &[scenario_name, raw_outcome], + ordinal, + ), + ) + }; + + Ok(( + statement, + OutcomeMetadata { + id, + source: source.clone(), + }, + )) + } + + fn finalize_verification_ids( + features: &[Feature], + components: &[Component], + id_mode: IdMode, + warnings: &mut Vec, + ) -> Result<(), IntentError> { + let mut feature_ids = HashMap::::new(); + let mut scenario_ids = HashMap::::new(); + let mut outcome_ids = HashMap::::new(); + + for feature in features { + Self::check_id_policy(&feature.verification_id, &feature.source, id_mode, warnings)?; + Self::register_unique_id( + &mut feature_ids, + &feature.verification_id, + &feature.verification_id_source, + )?; + + if let FeatureVerification::DocumentationOnly { rationale } = &feature.verification { + if rationale.trim().is_empty() { + return Err(Self::verification_error( + &feature.source, + "verification: documentation-only requires a non-empty rationale", + )); + } + if !feature.scenarios.is_empty() || !feature.tests.is_empty() { + let span = feature + .scenarios + .first() + .map(|scenario| &scenario.source) + .unwrap_or(&feature.source); + return Err(Self::verification_error( + span, + "documentation-only is valid only for a feature with no behavioral outcomes or tests", + )); + } + } + + for scenario in &feature.scenarios { + Self::check_id_policy( + &scenario.verification_id, + &scenario.source, + id_mode, + warnings, + )?; + Self::register_unique_id( + &mut scenario_ids, + &scenario.verification_id, + &scenario.verification_id_source, + )?; + + for outcome in &scenario.outcome_metadata { + Self::check_id_policy(&outcome.id, &outcome.source, id_mode, warnings)?; + Self::register_unique_id(&mut outcome_ids, &outcome.id, &outcome.source)?; + } + } + } + + for component in components { + for scenario in &component.scenarios { + Self::check_id_policy( + &scenario.verification_id, + &scenario.source, + id_mode, + warnings, + )?; + Self::register_unique_id( + &mut scenario_ids, + &scenario.verification_id, + &scenario.verification_id_source, + )?; + for outcome in &scenario.outcome_metadata { + Self::check_id_policy(&outcome.id, &outcome.source, id_mode, warnings)?; + Self::register_unique_id(&mut outcome_ids, &outcome.id, &outcome.source)?; + } + } + } + Ok(()) + } + + fn check_id_policy( + id: &StableId, + source: &SourceSpan, + id_mode: IdMode, + warnings: &mut Vec, + ) -> Result<(), IntentError> { + if id.origin() == IdOrigin::Explicit { + return Ok(()); + } + if id_mode == IdMode::Strict { + return Err(Self::verification_error( + source, + format!( + "missing {} ID; strict mode requires a stable explicit ID", + id.kind() + ), + )); + } + warnings.push(IdWarning { + message: format!( + "derived {} ID '{}' for compatibility; renaming or reordering changes identity", + id.kind(), + id + ), + id: id.clone(), + span: source.clone(), + }); + Ok(()) + } + + fn register_unique_id( + seen: &mut HashMap, + id: &StableId, + source: &SourceSpan, + ) -> Result<(), IntentError> { + if let Some(first) = seen.get(id.as_str()) { + return Err(Self::verification_error( + source, + format!( + "duplicate {} ID '{}'; first declared at {}", + id.kind(), + id, + first.location() + ), + )); + } + seen.insert(id.to_string(), source.clone()); + Ok(()) + } + /// Parse a single assertion line fn parse_assertion(line: &str) -> Option { let line = line.trim().trim_start_matches('-').trim(); @@ -7080,11 +7460,27 @@ Feature: API }]; let scenario = Scenario { + id: None, + verification_id: StableId::compatibility_derived( + IdKind::Scenario, + &["test-slugify-function"], + 0, + ), + verification_id_source: SourceSpan::single_line("test.intent", 1, 1, 1), + source: SourceSpan::single_line("test.intent", 1, 1, 1), name: "Test slugify function".to_string(), description: None, given_clause: None, when_clause: "testing slugify".to_string(), outcomes: vec!["result is valid".to_string()], + outcome_metadata: vec![OutcomeMetadata { + id: StableId::compatibility_derived( + IdKind::Outcome, + &["test-slugify-function", "result-is-valid"], + 0, + ), + source: SourceSpan::single_line("test.intent", 2, 1, 1), + }], resolved_test: None, component_refs: vec![], }; diff --git a/src/lib.rs b/src/lib.rs index 5f3588b..6270df8 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -20,5 +20,6 @@ mod std_secrets_tests; pub mod stdlib; pub mod typechecker; pub mod types; +pub mod verification; pub use error::{IntentError, Result}; diff --git a/src/verification/ids.rs b/src/verification/ids.rs new file mode 100644 index 0000000..8e82abc --- /dev/null +++ b/src/verification/ids.rs @@ -0,0 +1,212 @@ +use serde::Serialize; +use std::fmt; + +/// Source range for a declaration or diagnostic. +#[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize)] +pub struct SourceSpan { + pub path: String, + pub start_line: usize, + pub start_column: usize, + pub end_line: usize, + pub end_column: usize, +} + +impl SourceSpan { + pub fn single_line( + path: impl Into, + line: usize, + start_column: usize, + end_column: usize, + ) -> Self { + Self { + path: path.into(), + start_line: line, + start_column, + end_line: line, + end_column, + } + } + + pub fn location(&self) -> String { + format!("{}:{}:{}", self.path, self.start_line, self.start_column) + } +} + +impl fmt::Display for SourceSpan { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + write!(f, "{}", self.location()) + } +} + +/// Whether missing IDs are rejected or derived for legacy Intent files. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub enum IdMode { + Strict, + Compatibility, +} + +#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Serialize)] +pub enum IdKind { + Feature, + Scenario, + Outcome, +} + +impl IdKind { + pub const fn prefix(self) -> &'static str { + match self { + Self::Feature => "feature", + Self::Scenario => "scenario", + Self::Outcome => "outcome", + } + } +} + +impl fmt::Display for IdKind { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + f.write_str(self.prefix()) + } +} + +#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Serialize)] +pub enum IdOrigin { + Explicit, + CompatibilityDerived, +} + +/// A validated verification identity. +#[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize)] +pub struct StableId { + value: String, + kind: IdKind, + origin: IdOrigin, +} + +impl StableId { + pub fn explicit(value: impl Into, kind: IdKind) -> Result { + let value = value.into(); + validate_id(&value, kind)?; + Ok(Self { + value, + kind, + origin: IdOrigin::Explicit, + }) + } + + pub(crate) fn compatibility_derived(kind: IdKind, labels: &[&str], ordinal: usize) -> Self { + let label = labels + .iter() + .map(|label| slug(label)) + .filter(|label| !label.is_empty()) + .collect::>() + .join("."); + let label = if label.is_empty() { + "unnamed".to_string() + } else { + label + }; + Self { + value: format!("{}.compat.{}.{}", kind.prefix(), label, ordinal + 1), + kind, + origin: IdOrigin::CompatibilityDerived, + } + } + + pub fn as_str(&self) -> &str { + &self.value + } + + pub const fn kind(&self) -> IdKind { + self.kind + } + + pub const fn origin(&self) -> IdOrigin { + self.origin + } +} + +impl fmt::Display for StableId { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + f.write_str(&self.value) + } +} + +impl AsRef for StableId { + fn as_ref(&self) -> &str { + self.as_str() + } +} + +/// A compatibility diagnostic. Derived identity is deliberately visible because +/// it changes when legacy declarations are renamed or reordered. +#[derive(Debug, Clone, PartialEq, Eq, Serialize)] +pub struct IdWarning { + pub message: String, + pub id: StableId, + pub span: SourceSpan, +} + +pub(crate) fn validate_id(value: &str, kind: IdKind) -> Result<(), String> { + let expected_prefix = format!("{}.", kind.prefix()); + let Some(suffix) = value.strip_prefix(&expected_prefix) else { + return Err(format!("must start with '{expected_prefix}'")); + }; + if suffix.is_empty() { + return Err("must contain at least one name segment".to_string()); + } + + for segment in suffix.split('.') { + if segment.is_empty() { + return Err("must not contain empty name segments".to_string()); + } + let bytes = segment.as_bytes(); + if !bytes.first().is_some_and(u8::is_ascii_alphanumeric) + || !bytes.last().is_some_and(u8::is_ascii_alphanumeric) + || !bytes.iter().all(|byte| { + byte.is_ascii_lowercase() || byte.is_ascii_digit() || *byte == b'-' || *byte == b'_' + }) + { + return Err( + "segments must use lowercase ASCII letters, digits, '-' or '_', and begin/end with a letter or digit" + .to_string(), + ); + } + } + Ok(()) +} + +fn slug(value: &str) -> String { + const MAX_DERIVED_SEGMENT_BYTES: usize = 48; + let mut result = String::new(); + let mut separated = false; + for byte in value.bytes() { + if result.len() >= MAX_DERIVED_SEGMENT_BYTES { + break; + } + if byte.is_ascii_alphanumeric() { + result.push((byte as char).to_ascii_lowercase()); + separated = false; + } else if !separated && !result.is_empty() { + result.push('-'); + separated = true; + } + } + while result.ends_with('-') { + result.pop(); + } + result +} + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn validates_kind_prefix_and_segments() { + assert!(StableId::explicit("outcome.auth.denied-1", IdKind::Outcome).is_ok()); + assert!(StableId::explicit("feature.auth_state", IdKind::Feature).is_ok()); + assert!(StableId::explicit("scenario.auth", IdKind::Outcome).is_err()); + assert!(StableId::explicit("outcome.Auth", IdKind::Outcome).is_err()); + assert!(StableId::explicit("outcome.auth..denied", IdKind::Outcome).is_err()); + } +} diff --git a/src/verification/mod.rs b/src/verification/mod.rs new file mode 100644 index 0000000..fe1dbc5 --- /dev/null +++ b/src/verification/mod.rs @@ -0,0 +1,14 @@ +//! Stable obligation identity and orthogonal verification truth types. +//! +//! Slice 1A deliberately contains no renderer, schema, threshold, policy, +//! planner, executor, or exit-status behavior. + +pub mod ids; +pub mod model; + +pub use ids::{IdKind, IdMode, IdOrigin, IdWarning, SourceSpan, StableId}; +pub use model::{ + AssertionResolution, BindingStatus, DeclarationStatus, Disposition, EvidenceBinding, + ExecutabilityStatus, ExecutableCoverage, FeatureProofStatus, FeatureTruth, Freshness, + ImplementationCoverage, LinkageStatus, Obligation, VerificationTruth, VerifiedCoverage, +}; diff --git a/src/verification/model.rs b/src/verification/model.rs new file mode 100644 index 0000000..5cdf1a7 --- /dev/null +++ b/src/verification/model.rs @@ -0,0 +1,305 @@ +use serde::Serialize; + +use crate::intent::{FeatureVerification, IntentFile}; + +use super::ids::{SourceSpan, StableId}; + +#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize)] +pub enum DeclarationStatus { + Declared, + DocumentationOnly, +} + +#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize)] +pub enum LinkageStatus { + Linked, + Unlinked, +} + +#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize)] +pub enum BindingStatus { + Bound, + Unbound, + Ambiguous, +} + +#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize)] +pub enum ExecutabilityStatus { + Executable, + Unsupported, + Blocked, +} + +#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize)] +pub enum Disposition { + Planned, + Running, + Passed, + Failed, + Flaky, + Skipped, + Cancelled, + NoResult, +} + +#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize)] +pub enum Freshness { + Current, + Stale, +} + +#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize)] +pub enum AssertionResolution { + Resolved, + Unknown, + Unresolved, +} + +/// One candidate source of execution evidence for an obligation. +#[derive(Debug, Clone, PartialEq, Eq, Serialize)] +pub struct EvidenceBinding { + pub id: String, + pub obligation_id: String, + pub source: SourceSpan, + pub declaration: DeclarationStatus, + pub linkage: LinkageStatus, + pub binding: BindingStatus, + pub executability: ExecutabilityStatus, + pub disposition: Disposition, + pub freshness: Freshness, + pub assertion_resolution: AssertionResolution, + pub evidence_atoms: usize, +} + +impl EvidenceBinding { + /// Passing execution is evidence only when its assertion was resolved and + /// produced at least one current evidence atom. + pub fn satisfies_obligation(&self) -> bool { + self.declaration == DeclarationStatus::Declared + && self.linkage == LinkageStatus::Linked + && self.binding == BindingStatus::Bound + && self.executability == ExecutabilityStatus::Executable + && self.disposition == Disposition::Passed + && self.freshness == Freshness::Current + && self.assertion_resolution == AssertionResolution::Resolved + && self.evidence_atoms > 0 + } +} + +/// A source-located behavioral claim produced from one scenario outcome. +#[derive(Debug, Clone, PartialEq, Eq, Serialize)] +pub struct Obligation { + pub id: StableId, + pub feature_id: StableId, + pub scenario_id: StableId, + pub statement: String, + pub source: SourceSpan, + pub declaration: DeclarationStatus, + pub linkage: LinkageStatus, + pub binding: BindingStatus, + pub executability: ExecutabilityStatus, + pub disposition: Disposition, + pub freshness: Freshness, + pub evidence_bindings: Vec, +} + +impl Obligation { + pub fn is_verified(&self) -> bool { + self.declaration == DeclarationStatus::Declared + && self.linkage == LinkageStatus::Linked + && self.binding == BindingStatus::Bound + && self.executability == ExecutabilityStatus::Executable + && self.disposition == Disposition::Passed + && self.freshness == Freshness::Current + && !self.evidence_bindings.is_empty() + && self + .evidence_bindings + .iter() + .all(EvidenceBinding::satisfies_obligation) + } +} + +#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize)] +pub enum FeatureProofStatus { + Unproven, + Pending, + DocumentationOnly, +} + +/// Feature-level truth remains visible even when there are no outcome obligations. +#[derive(Debug, Clone, PartialEq, Eq, Serialize)] +pub struct FeatureTruth { + pub id: StableId, + pub name: String, + pub source: SourceSpan, + pub declaration: DeclarationStatus, + pub rationale: Option, + pub proof_status: FeatureProofStatus, + pub obligation_ids: Vec, +} + +impl FeatureTruth { + pub fn is_unproven(&self) -> bool { + self.proof_status == FeatureProofStatus::Unproven + } +} + +macro_rules! coverage_type { + ($name:ident) => { + #[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize)] + pub struct $name { + pub covered: usize, + pub total: usize, + } + }; +} + +coverage_type!(ImplementationCoverage); +coverage_type!(ExecutableCoverage); +coverage_type!(VerifiedCoverage); + +/// Slice 1A's in-memory truth model. Rendering and exit policy intentionally +/// consume this in later slices rather than living here. +#[derive(Debug, Clone, PartialEq, Eq, Serialize)] +pub struct VerificationTruth { + pub features: Vec, + pub obligations: Vec, +} + +impl VerificationTruth { + pub fn from_intent(intent: &IntentFile) -> Self { + let mut features = Vec::new(); + let mut obligations = Vec::new(); + + for feature in &intent.features { + let feature_id = feature.verification_id.clone(); + let (declaration, rationale) = match &feature.verification { + FeatureVerification::Behavioral => (DeclarationStatus::Declared, None), + FeatureVerification::DocumentationOnly { rationale } => ( + DeclarationStatus::DocumentationOnly, + Some(rationale.clone()), + ), + }; + let mut obligation_ids = Vec::new(); + + if declaration == DeclarationStatus::Declared { + for scenario in &feature.scenarios { + let scenario_id = scenario.verification_id.clone(); + for (statement, metadata) in + scenario.outcomes.iter().zip(&scenario.outcome_metadata) + { + obligation_ids.push(metadata.id.clone()); + obligations.push(Obligation { + id: metadata.id.clone(), + feature_id: feature_id.clone(), + scenario_id: scenario_id.clone(), + statement: statement.clone(), + source: metadata.source.clone(), + declaration, + linkage: LinkageStatus::Unlinked, + binding: BindingStatus::Unbound, + executability: ExecutabilityStatus::Unsupported, + disposition: Disposition::NoResult, + freshness: Freshness::Current, + evidence_bindings: Vec::new(), + }); + } + } + } + + let proof_status = if declaration == DeclarationStatus::DocumentationOnly { + FeatureProofStatus::DocumentationOnly + } else if obligation_ids.is_empty() { + FeatureProofStatus::Unproven + } else { + FeatureProofStatus::Pending + }; + features.push(FeatureTruth { + id: feature_id, + name: feature.name.clone(), + source: feature.source.clone(), + declaration, + rationale, + proof_status, + obligation_ids, + }); + } + + Self { + features, + obligations, + } + } + + pub fn behavioral_feature_count(&self) -> usize { + self.features + .iter() + .filter(|feature| feature.declaration == DeclarationStatus::Declared) + .count() + } + + /// A feature is verified only when it has at least one required obligation + /// and every one of those obligations is verified. + pub fn feature_is_verified(&self, feature_id: &str) -> bool { + let Some(feature) = self + .features + .iter() + .find(|feature| feature.id.as_str() == feature_id) + else { + return false; + }; + feature.declaration == DeclarationStatus::Declared + && !feature.obligation_ids.is_empty() + && feature.obligation_ids.iter().all(|obligation_id| { + self.obligations + .iter() + .any(|obligation| obligation.id == *obligation_id && obligation.is_verified()) + }) + } + + pub fn mark_implementation_linked(&mut self, obligation_id: &str) -> Result<(), String> { + let obligation = self + .obligations + .iter_mut() + .find(|obligation| obligation.id.as_str() == obligation_id) + .ok_or_else(|| format!("unknown obligation ID '{obligation_id}'"))?; + obligation.linkage = LinkageStatus::Linked; + Ok(()) + } + + pub fn implementation_coverage(&self) -> ImplementationCoverage { + ImplementationCoverage { + covered: self + .obligations + .iter() + .filter(|obligation| obligation.linkage == LinkageStatus::Linked) + .count(), + total: self.obligations.len(), + } + } + + pub fn executable_coverage(&self) -> ExecutableCoverage { + ExecutableCoverage { + covered: self + .obligations + .iter() + .filter(|obligation| { + obligation.binding == BindingStatus::Bound + && obligation.executability == ExecutabilityStatus::Executable + }) + .count(), + total: self.obligations.len(), + } + } + + pub fn verified_coverage(&self) -> VerifiedCoverage { + VerifiedCoverage { + covered: self + .obligations + .iter() + .filter(|obligation| obligation.is_verified()) + .count(), + total: self.obligations.len(), + } + } +} diff --git a/tests/fixtures/verification/truth/compatibility_derived_ids.intent b/tests/fixtures/verification/truth/compatibility_derived_ids.intent new file mode 100644 index 0000000..4bd473d --- /dev/null +++ b/tests/fixtures/verification/truth/compatibility_derived_ids.intent @@ -0,0 +1,5 @@ +Feature: Legacy behavior + + Scenario: Legacy scenario + When something happens + → a legacy result is observed diff --git a/tests/fixtures/verification/truth/documentation_only.intent b/tests/fixtures/verification/truth/documentation_only.intent new file mode 100644 index 0000000..5bcb882 --- /dev/null +++ b/tests/fixtures/verification/truth/documentation_only.intent @@ -0,0 +1,5 @@ +Feature: Domain terminology + id: feature.domain-terminology + verification: documentation-only + rationale: "Defines shared vocabulary and makes no behavioral claim" + description: "Terms used by the behavioral specifications" diff --git a/tests/fixtures/verification/truth/duplicate_feature_ids.intent b/tests/fixtures/verification/truth/duplicate_feature_ids.intent new file mode 100644 index 0000000..c12d6a5 --- /dev/null +++ b/tests/fixtures/verification/truth/duplicate_feature_ids.intent @@ -0,0 +1,5 @@ +Feature: First feature + id: feature.duplicate + +Feature: Second feature + id: feature.duplicate diff --git a/tests/fixtures/verification/truth/duplicate_outcome_ids.intent b/tests/fixtures/verification/truth/duplicate_outcome_ids.intent new file mode 100644 index 0000000..644e276 --- /dev/null +++ b/tests/fixtures/verification/truth/duplicate_outcome_ids.intent @@ -0,0 +1,8 @@ +Feature: Duplicate outcomes + id: feature.duplicate-outcomes + + Scenario: Duplicate result declarations + id: scenario.duplicate-outcomes + When something happens + → id: outcome.duplicate; the first result is observed + → id: outcome.duplicate; the second result is observed diff --git a/tests/fixtures/verification/truth/duplicate_scenario_ids.intent b/tests/fixtures/verification/truth/duplicate_scenario_ids.intent new file mode 100644 index 0000000..63732e6 --- /dev/null +++ b/tests/fixtures/verification/truth/duplicate_scenario_ids.intent @@ -0,0 +1,12 @@ +Feature: Duplicate scenarios + id: feature.duplicate-scenarios + + Scenario: First scenario + id: scenario.duplicate + When something happens + → id: outcome.duplicate-scenarios.first; the first result is observed + + Scenario: Second scenario + id: scenario.duplicate + When something else happens + → id: outcome.duplicate-scenarios.second; the second result is observed diff --git a/tests/fixtures/verification/truth/linked_unexecuted.intent b/tests/fixtures/verification/truth/linked_unexecuted.intent new file mode 100644 index 0000000..da1346e --- /dev/null +++ b/tests/fixtures/verification/truth/linked_unexecuted.intent @@ -0,0 +1,7 @@ +Feature: Linked behavior + id: feature.linked + + Scenario: Linked scenario + id: scenario.linked + When something happens + → id: outcome.linked.result; a result is observed diff --git a/tests/fixtures/verification/truth/malformed_feature_id.intent b/tests/fixtures/verification/truth/malformed_feature_id.intent new file mode 100644 index 0000000..9c6d307 --- /dev/null +++ b/tests/fixtures/verification/truth/malformed_feature_id.intent @@ -0,0 +1,2 @@ +Feature: Malformed feature identifier + id: feature.Bad ID diff --git a/tests/fixtures/verification/truth/malformed_outcome_id.intent b/tests/fixtures/verification/truth/malformed_outcome_id.intent new file mode 100644 index 0000000..bc9f08f --- /dev/null +++ b/tests/fixtures/verification/truth/malformed_outcome_id.intent @@ -0,0 +1,7 @@ +Feature: Malformed outcome identifier + id: feature.malformed-outcome + + Scenario: Bad outcome identifier + id: scenario.malformed-outcome + When something happens + → id: outcome.BAD; a result is observed diff --git a/tests/fixtures/verification/truth/malformed_scenario_id.intent b/tests/fixtures/verification/truth/malformed_scenario_id.intent new file mode 100644 index 0000000..1e6b66a --- /dev/null +++ b/tests/fixtures/verification/truth/malformed_scenario_id.intent @@ -0,0 +1,7 @@ +Feature: Malformed scenario identifier + id: feature.malformed-scenario + + Scenario: Bad identifier + id: scenario..bad + When something happens + → id: outcome.malformed-scenario.result; a result is observed diff --git a/tests/fixtures/verification/truth/outcome_documentation_only.intent b/tests/fixtures/verification/truth/outcome_documentation_only.intent new file mode 100644 index 0000000..0fba4a4 --- /dev/null +++ b/tests/fixtures/verification/truth/outcome_documentation_only.intent @@ -0,0 +1,7 @@ +Feature: Invalid suppression + id: feature.invalid-suppression + + Scenario: Promised behavior + id: scenario.invalid-suppression + When something happens + → id: outcome.invalid-suppression.promise; verification: documentation-only diff --git a/tests/fixtures/verification/truth/zero_outcome_behavioral.intent b/tests/fixtures/verification/truth/zero_outcome_behavioral.intent new file mode 100644 index 0000000..0f48880 --- /dev/null +++ b/tests/fixtures/verification/truth/zero_outcome_behavioral.intent @@ -0,0 +1,3 @@ +Feature: Promised behavior without outcomes + id: feature.zero-outcomes + description: "This behavioral promise has no evidence obligations yet" diff --git a/tests/verification_truth_tests.rs b/tests/verification_truth_tests.rs new file mode 100644 index 0000000..c44cf7c --- /dev/null +++ b/tests/verification_truth_tests.rs @@ -0,0 +1,233 @@ +use std::path::{Path, PathBuf}; + +use ntnt::intent::IntentFile; +use ntnt::verification::{ + AssertionResolution, BindingStatus, DeclarationStatus, Disposition, EvidenceBinding, + ExecutabilityStatus, Freshness, IdMode, IdOrigin, LinkageStatus, SourceSpan, VerificationTruth, +}; + +fn fixture(name: &str) -> PathBuf { + Path::new(env!("CARGO_MANIFEST_DIR")) + .join("tests/fixtures/verification/truth") + .join(name) +} + +fn strict_error(name: &str) -> String { + IntentFile::parse_with_id_mode(&fixture(name), IdMode::Strict) + .expect_err("fixture must be rejected") + .to_string() +} + +#[test] +fn duplicate_feature_ids_report_both_source_locations() { + let error = strict_error("duplicate_feature_ids.intent"); + assert!( + error.contains("duplicate feature ID 'feature.duplicate'"), + "{error}" + ); + assert!(error.contains("duplicate_feature_ids.intent:5"), "{error}"); + assert!(error.contains("first declared at"), "{error}"); + assert!(error.contains("duplicate_feature_ids.intent:2"), "{error}"); +} + +#[test] +fn duplicate_scenario_ids_report_both_source_locations() { + let error = strict_error("duplicate_scenario_ids.intent"); + assert!( + error.contains("duplicate scenario ID 'scenario.duplicate'"), + "{error}" + ); + assert!( + error.contains("duplicate_scenario_ids.intent:10"), + "{error}" + ); + assert!(error.contains("duplicate_scenario_ids.intent:5"), "{error}"); +} + +#[test] +fn duplicate_outcome_ids_report_both_source_locations() { + let error = strict_error("duplicate_outcome_ids.intent"); + assert!( + error.contains("duplicate outcome ID 'outcome.duplicate'"), + "{error}" + ); + assert!(error.contains("duplicate_outcome_ids.intent:8"), "{error}"); + assert!(error.contains("duplicate_outcome_ids.intent:7"), "{error}"); +} + +#[test] +fn malformed_ids_report_the_entity_and_source_location() { + for (fixture_name, kind, id, line) in [ + ( + "malformed_feature_id.intent", + "feature", + "feature.Bad ID", + 2, + ), + ( + "malformed_scenario_id.intent", + "scenario", + "scenario..bad", + 5, + ), + ("malformed_outcome_id.intent", "outcome", "outcome.BAD", 7), + ] { + let error = strict_error(fixture_name); + assert!( + error.contains(&format!("malformed {kind} ID '{id}'")), + "{error}" + ); + assert!(error.contains(&format!("{fixture_name}:{line}")), "{error}"); + } +} + +#[test] +fn strict_mode_rejects_missing_stable_ids() { + let error = strict_error("compatibility_derived_ids.intent"); + assert!(error.contains("missing feature ID"), "{error}"); + assert!( + error.contains("compatibility_derived_ids.intent:1"), + "{error}" + ); +} + +#[test] +fn compatibility_mode_derives_ids_and_emits_source_located_warnings() { + let intent = IntentFile::parse_with_id_mode( + &fixture("compatibility_derived_ids.intent"), + IdMode::Compatibility, + ) + .unwrap(); + + assert_eq!(intent.verification_warnings.len(), 3); + assert!(intent + .verification_warnings + .iter() + .all(|warning| warning.id.origin() == IdOrigin::CompatibilityDerived)); + assert!(intent.verification_warnings.iter().any(|warning| { + warning.message.contains("derived feature ID") && warning.span.start_line == 1 + })); + assert!(intent.verification_warnings.iter().any(|warning| { + warning.message.contains("derived scenario ID") && warning.span.start_line == 3 + })); + assert!(intent.verification_warnings.iter().any(|warning| { + warning.message.contains("derived outcome ID") && warning.span.start_line == 5 + })); +} + +#[test] +fn zero_outcome_behavioral_features_are_unproven() { + let intent = + IntentFile::parse_with_id_mode(&fixture("zero_outcome_behavioral.intent"), IdMode::Strict) + .unwrap(); + let truth = VerificationTruth::from_intent(&intent); + + assert_eq!(truth.features.len(), 1); + assert!(truth.features[0].is_unproven()); + assert!(!truth.feature_is_verified("feature.zero-outcomes")); + assert_eq!(truth.features[0].declaration, DeclarationStatus::Declared); + assert!(truth.obligations.is_empty()); + assert_eq!(truth.verified_coverage().covered, 0); + assert_eq!(truth.verified_coverage().total, 0); +} + +#[test] +fn justified_documentation_only_features_are_visible_but_not_behavioral() { + let intent = + IntentFile::parse_with_id_mode(&fixture("documentation_only.intent"), IdMode::Strict) + .unwrap(); + let truth = VerificationTruth::from_intent(&intent); + + assert_eq!(truth.features.len(), 1); + assert_eq!( + truth.features[0].declaration, + DeclarationStatus::DocumentationOnly + ); + assert_eq!( + truth.features[0].rationale.as_deref(), + Some("Defines shared vocabulary and makes no behavioral claim") + ); + assert!(!truth.features[0].is_unproven()); + assert!(!truth.feature_is_verified("feature.domain-terminology")); + assert_eq!(truth.behavioral_feature_count(), 0); +} + +#[test] +fn documentation_only_cannot_suppress_an_outcome() { + let error = strict_error("outcome_documentation_only.intent"); + assert!( + error.contains("documentation-only is valid only on a feature"), + "{error}" + ); + assert!( + error.contains("outcome_documentation_only.intent:7"), + "{error}" + ); +} + +#[test] +fn linked_but_unexecuted_obligations_only_have_implementation_coverage() { + let intent = + IntentFile::parse_with_id_mode(&fixture("linked_unexecuted.intent"), IdMode::Strict) + .unwrap(); + let mut truth = VerificationTruth::from_intent(&intent); + truth + .mark_implementation_linked("outcome.linked.result") + .unwrap(); + + assert_eq!(truth.implementation_coverage().covered, 1); + assert_eq!(truth.implementation_coverage().total, 1); + assert_eq!(truth.executable_coverage().covered, 0); + assert_eq!(truth.executable_coverage().total, 1); + assert_eq!(truth.verified_coverage().covered, 0); + assert_eq!(truth.verified_coverage().total, 1); +} + +#[test] +fn unknown_and_unresolved_assertions_fail_closed() { + let span = SourceSpan::single_line("verification.tnt", 12, 5, 20); + for resolution in [ + AssertionResolution::Unknown, + AssertionResolution::Unresolved, + ] { + let binding = EvidenceBinding { + id: "binding.example".to_string(), + obligation_id: "outcome.example".to_string(), + source: span.clone(), + declaration: DeclarationStatus::Declared, + linkage: LinkageStatus::Linked, + binding: BindingStatus::Bound, + executability: ExecutabilityStatus::Executable, + disposition: Disposition::Passed, + freshness: Freshness::Current, + assertion_resolution: resolution, + evidence_atoms: 1, + }; + + assert!(!binding.satisfies_obligation()); + } +} + +#[test] +fn truth_dimensions_remain_orthogonal() { + let binding = EvidenceBinding { + id: "binding.blocked".to_string(), + obligation_id: "outcome.example".to_string(), + source: SourceSpan::single_line("verification.tnt", 7, 1, 12), + declaration: DeclarationStatus::Declared, + linkage: LinkageStatus::Linked, + binding: BindingStatus::Bound, + executability: ExecutabilityStatus::Blocked, + disposition: Disposition::Planned, + freshness: Freshness::Stale, + assertion_resolution: AssertionResolution::Resolved, + evidence_atoms: 0, + }; + + assert_eq!(binding.linkage, LinkageStatus::Linked); + assert_eq!(binding.binding, BindingStatus::Bound); + assert_eq!(binding.executability, ExecutabilityStatus::Blocked); + assert_eq!(binding.disposition, Disposition::Planned); + assert_eq!(binding.freshness, Freshness::Stale); + assert!(!binding.satisfies_obligation()); +} From b77d27d5d5cddeadd08af5a533a4801f219a3c6f Mon Sep 17 00:00:00 2001 From: Larri Date: Thu, 30 Jul 2026 17:28:46 -0600 Subject: [PATCH 2/6] fix: keep verification truth dimensions independent --- src/intent.rs | 29 +++++++++++++++++- src/verification/model.rs | 2 -- tests/verification_truth_tests.rs | 49 +++++++++++++++++++++++++++++++ 3 files changed, 77 insertions(+), 3 deletions(-) diff --git a/src/intent.rs b/src/intent.rs index 03b9d01..79a664c 100644 --- a/src/intent.rs +++ b/src/intent.rs @@ -2921,6 +2921,11 @@ impl IntentFile { let mut in_component_inherent = false; let mut in_invariant_assertions = false; let mut in_test_data_table = false; + // Constraints are a legacy Intent declaration parsed only indirectly by + // this module. Track their context so their `id:` and `rationale:` + // fields are not reinterpreted as verification metadata for the + // preceding feature. + let mut in_constraint = false; let mut test_data_columns: Vec = Vec::new(); let mut _in_glossary_bindings = false; // Technical bindings parsing state @@ -3149,8 +3154,23 @@ impl IntentFile { continue; } + // Legacy constraint declaration. Preserve the existing behavior + // where constraint scenarios remain visible to the preceding + // feature, but do not treat constraint metadata as feature + // verification metadata. + if trimmed.starts_with("Constraint:") { + if let Some(scenario) = current_scenario.take() { + if let Some(feature) = current_feature.as_mut() { + feature.scenarios.push(scenario); + } + } + in_constraint = true; + continue; + } + // Feature declaration if trimmed.starts_with("Feature:") { + in_constraint = false; // Save previous component if let Some(mut comp) = current_component.take() { if let Some(scenario) = current_scenario.take() { @@ -3205,6 +3225,7 @@ impl IntentFile { // Component declaration if trimmed.starts_with("Component:") { + in_constraint = false; // Save previous component if let Some(mut comp) = current_component.take() { if let Some(scenario) = current_scenario.take() { @@ -3252,6 +3273,7 @@ impl IntentFile { // Invariant declaration if trimmed.starts_with("Invariant:") { + in_constraint = false; // Save previous feature if let Some(mut feat) = current_feature.take() { if let Some(test) = current_test.take() { @@ -3579,6 +3601,10 @@ impl IntentFile { scenario.verification_id = Self::explicit_id(id, IdKind::Scenario, &id_source)?; scenario.verification_id_source = id_source; + } else if in_constraint { + // Keep legacy serialized IDs stable without promoting a + // constraint ID into feature verification identity. + feature.id = Some(id.to_string()); } else { feature.verification_id = Self::explicit_id(id, IdKind::Feature, &id_source)?; @@ -3608,7 +3634,8 @@ impl IntentFile { continue; } - if trimmed.starts_with("rationale:") && current_scenario.is_none() { + if trimmed.starts_with("rationale:") && current_scenario.is_none() && !in_constraint + { let rationale = trimmed .trim_start_matches("rationale:") .trim() diff --git a/src/verification/model.rs b/src/verification/model.rs index 5cdf1a7..ce96831 100644 --- a/src/verification/model.rs +++ b/src/verification/model.rs @@ -76,7 +76,6 @@ impl EvidenceBinding { /// produced at least one current evidence atom. pub fn satisfies_obligation(&self) -> bool { self.declaration == DeclarationStatus::Declared - && self.linkage == LinkageStatus::Linked && self.binding == BindingStatus::Bound && self.executability == ExecutabilityStatus::Executable && self.disposition == Disposition::Passed @@ -106,7 +105,6 @@ pub struct Obligation { impl Obligation { pub fn is_verified(&self) -> bool { self.declaration == DeclarationStatus::Declared - && self.linkage == LinkageStatus::Linked && self.binding == BindingStatus::Bound && self.executability == ExecutabilityStatus::Executable && self.disposition == Disposition::Passed diff --git a/tests/verification_truth_tests.rs b/tests/verification_truth_tests.rs index c44cf7c..9e06667 100644 --- a/tests/verification_truth_tests.rs +++ b/tests/verification_truth_tests.rs @@ -231,3 +231,52 @@ fn truth_dimensions_remain_orthogonal() { assert_eq!(binding.freshness, Freshness::Stale); assert!(!binding.satisfies_obligation()); } + +#[test] +fn behavioral_evidence_does_not_require_implementation_linkage() { + let binding = EvidenceBinding { + id: "binding.behavioral".to_string(), + obligation_id: "outcome.behavioral".to_string(), + source: SourceSpan::single_line("verification.tnt", 9, 1, 20), + declaration: DeclarationStatus::Declared, + linkage: LinkageStatus::Unlinked, + binding: BindingStatus::Bound, + executability: ExecutabilityStatus::Executable, + disposition: Disposition::Passed, + freshness: Freshness::Current, + assertion_resolution: AssertionResolution::Resolved, + evidence_atoms: 1, + }; + + assert!(binding.satisfies_obligation()); + + let intent = + IntentFile::parse_with_id_mode(&fixture("linked_unexecuted.intent"), IdMode::Strict) + .unwrap(); + let mut truth = VerificationTruth::from_intent(&intent); + let obligation = &mut truth.obligations[0]; + obligation.linkage = LinkageStatus::Unlinked; + obligation.binding = BindingStatus::Bound; + obligation.executability = ExecutabilityStatus::Executable; + obligation.disposition = Disposition::Passed; + obligation.freshness = Freshness::Current; + obligation.evidence_bindings.push(binding); + + assert!(obligation.is_verified()); +} + +#[test] +fn compatibility_parser_does_not_reinterpret_constraint_metadata() { + let path = Path::new(env!("CARGO_MANIFEST_DIR")).join("examples/crypto_chart/crypto.intent"); + let intent = IntentFile::parse(&path).expect("legacy Constraint declarations must still lint"); + + assert_eq!(intent.features.len(), 4); + assert_eq!( + intent + .features + .iter() + .map(|feature| feature.scenarios.len()) + .sum::(), + 4 + ); +} From 6eef0ed0153140a9b68447b65f91fb500d7ce123 Mon Sep 17 00:00:00 2001 From: Larri Date: Thu, 30 Jul 2026 17:31:02 -0600 Subject: [PATCH 3/6] fix: keep outcome verification syntax unambiguous --- src/intent.rs | 23 +++++++++----- src/verification/model.rs | 14 +++++++-- tests/verification_truth_tests.rs | 50 +++++++++++++++++++++++++++++++ 3 files changed, 77 insertions(+), 10 deletions(-) diff --git a/src/intent.rs b/src/intent.rs index 79a664c..c993bd9 100644 --- a/src/intent.rs +++ b/src/intent.rs @@ -3894,13 +3894,15 @@ impl IntentFile { scenario_name: &str, ordinal: usize, ) -> Result<(String, OutcomeMetadata), IntentError> { - let source = Self::line_span(source_path, line_number, line, "id:"); - if raw_outcome.contains("verification: documentation-only") { - return Err(Self::verification_error( - &source, - "documentation-only is valid only on a feature", - )); - } + let has_explicit_id = raw_outcome.starts_with("id:"); + let source_marker = if has_explicit_id { + "id:" + } else if line.contains('→') { + "→" + } else { + "->" + }; + let source = Self::line_span(source_path, line_number, line, source_marker); let (statement, id) = if let Some(id_declaration) = raw_outcome.strip_prefix("id:") { let Some((id, statement)) = id_declaration.split_once(';') else { @@ -3932,6 +3934,13 @@ impl IntentFile { ) }; + if statement == "verification: documentation-only" { + return Err(Self::verification_error( + &source, + "documentation-only is valid only on a feature", + )); + } + Ok(( statement, OutcomeMetadata { diff --git a/src/verification/model.rs b/src/verification/model.rs index ce96831..1cc665b 100644 --- a/src/verification/model.rs +++ b/src/verification/model.rs @@ -1,3 +1,5 @@ +use std::collections::HashMap; + use serde::Serialize; use crate::intent::{FeatureVerification, IntentFile}; @@ -246,12 +248,18 @@ impl VerificationTruth { else { return false; }; + let obligations_by_id: HashMap<&str, &Obligation> = self + .obligations + .iter() + .map(|obligation| (obligation.id.as_str(), obligation)) + .collect(); + feature.declaration == DeclarationStatus::Declared && !feature.obligation_ids.is_empty() && feature.obligation_ids.iter().all(|obligation_id| { - self.obligations - .iter() - .any(|obligation| obligation.id == *obligation_id && obligation.is_verified()) + obligations_by_id + .get(obligation_id.as_str()) + .is_some_and(|obligation| obligation.is_verified()) }) } diff --git a/tests/verification_truth_tests.rs b/tests/verification_truth_tests.rs index 9e06667..f63f0db 100644 --- a/tests/verification_truth_tests.rs +++ b/tests/verification_truth_tests.rs @@ -280,3 +280,53 @@ fn compatibility_parser_does_not_reinterpret_constraint_metadata() { 4 ); } + +#[test] +fn outcome_statement_can_quote_documentation_only_syntax() { + let content = r#"Feature: Parser documentation + id: feature.parser-documentation + + Scenario: Explain invalid suppression + id: scenario.parser-documentation.invalid-suppression + When syntax is documented + → id: outcome.parser-documentation.message; parser rejects 'verification: documentation-only' on non-feature nodes +"#; + + let intent = IntentFile::parse_content_with_id_mode( + content, + "parser-documentation.intent".to_string(), + IdMode::Strict, + ) + .expect("quoted syntax is prose, not an outcome-level directive"); + + assert!( + intent.features[0].scenarios[0].outcomes[0].contains("'verification: documentation-only'") + ); +} + +#[test] +fn compatibility_outcome_warning_points_to_the_outcome_marker() { + let content = r#"Feature: Source spans + id: feature.source-spans + + Scenario: Derive an outcome ID + id: scenario.source-spans.derived-outcome + When source locations are recorded + → the widget id: field is set +"#; + + let intent = IntentFile::parse_content_with_id_mode( + content, + "source-spans.intent".to_string(), + IdMode::Compatibility, + ) + .unwrap(); + let warning = intent + .verification_warnings + .iter() + .find(|warning| warning.message.contains("derived outcome ID")) + .expect("outcome warning"); + + assert_eq!(warning.span.start_line, 7); + assert_eq!(warning.span.start_column, 5); +} From c3d179e34659686a6c85c2350b7f6d018ef978ff Mon Sep 17 00:00:00 2001 From: Larri Date: Thu, 30 Jul 2026 17:57:24 -0600 Subject: [PATCH 4/6] fix: preserve component scenarios across constraints --- src/intent.rs | 2 ++ tests/verification_truth_tests.rs | 33 +++++++++++++++++++++++++++++++ 2 files changed, 35 insertions(+) diff --git a/src/intent.rs b/src/intent.rs index c993bd9..c29b8fe 100644 --- a/src/intent.rs +++ b/src/intent.rs @@ -3162,6 +3162,8 @@ impl IntentFile { if let Some(scenario) = current_scenario.take() { if let Some(feature) = current_feature.as_mut() { feature.scenarios.push(scenario); + } else if let Some(component) = current_component.as_mut() { + component.scenarios.push(scenario); } } in_constraint = true; diff --git a/tests/verification_truth_tests.rs b/tests/verification_truth_tests.rs index f63f0db..dc61765 100644 --- a/tests/verification_truth_tests.rs +++ b/tests/verification_truth_tests.rs @@ -330,3 +330,36 @@ fn compatibility_outcome_warning_points_to_the_outcome_marker() { assert_eq!(warning.span.start_line, 7); assert_eq!(warning.span.start_column, 5); } + +#[test] +fn constraint_boundary_preserves_an_active_component_scenario() { + let content = r#"Component: Reusable check + id: component.reusable-check + + Scenario: Existing component behavior + id: scenario.component.existing-behavior + When the component runs + → id: outcome.component.existing-behavior; result is valid + +Constraint: Legacy boundary + id: constraint.legacy-boundary + +Feature: Following feature + id: feature.following +"#; + + let intent = IntentFile::parse_content_with_id_mode( + content, + "component-constraint.intent".to_string(), + IdMode::Strict, + ) + .expect("Constraint must not discard the active component scenario"); + + assert_eq!(intent.components.len(), 1); + assert_eq!(intent.components[0].scenarios.len(), 1); + assert_eq!( + intent.components[0].scenarios[0].verification_id.as_str(), + "scenario.component.existing-behavior" + ); + assert_eq!(intent.components[0].scenarios[0].outcomes.len(), 1); +} From 5a5c1d5069eb645d18a520a737a1943098931476 Mon Sep 17 00:00:00 2001 From: Larri Date: Fri, 31 Jul 2026 15:00:41 -0600 Subject: [PATCH 5/6] fix: isolate constraint metadata during parsing --- src/intent.rs | 4 ++-- tests/verification_truth_tests.rs | 31 ++++++++++++++++++++++++++++++- 2 files changed, 32 insertions(+), 3 deletions(-) diff --git a/src/intent.rs b/src/intent.rs index c29b8fe..3ca7fc5 100644 --- a/src/intent.rs +++ b/src/intent.rs @@ -3458,7 +3458,7 @@ impl IntentFile { // Inside a component if let Some(ref mut component) = current_component { // Component ID - if trimmed.starts_with("id:") && current_scenario.is_none() { + if trimmed.starts_with("id:") && current_scenario.is_none() && !in_constraint { let id = trimmed.trim_start_matches("id:").trim(); component.id = id.to_string(); continue; @@ -3616,7 +3616,7 @@ impl IntentFile { continue; } - if trimmed.starts_with("verification:") { + if trimmed.starts_with("verification:") && !in_constraint { if current_scenario.is_some() { return Err(Self::verification_error( &Self::line_span(&source_path, line_number, line, "verification:"), diff --git a/tests/verification_truth_tests.rs b/tests/verification_truth_tests.rs index dc61765..5e49ead 100644 --- a/tests/verification_truth_tests.rs +++ b/tests/verification_truth_tests.rs @@ -1,6 +1,6 @@ use std::path::{Path, PathBuf}; -use ntnt::intent::IntentFile; +use ntnt::intent::{FeatureVerification, IntentFile}; use ntnt::verification::{ AssertionResolution, BindingStatus, DeclarationStatus, Disposition, EvidenceBinding, ExecutabilityStatus, Freshness, IdMode, IdOrigin, LinkageStatus, SourceSpan, VerificationTruth, @@ -356,6 +356,7 @@ Feature: Following feature .expect("Constraint must not discard the active component scenario"); assert_eq!(intent.components.len(), 1); + assert_eq!(intent.components[0].id, "component.reusable-check"); assert_eq!(intent.components[0].scenarios.len(), 1); assert_eq!( intent.components[0].scenarios[0].verification_id.as_str(), @@ -363,3 +364,31 @@ Feature: Following feature ); assert_eq!(intent.components[0].scenarios[0].outcomes.len(), 1); } + +#[test] +fn constraint_metadata_cannot_change_feature_verification() { + let content = r#"Feature: Behavioral feature + id: feature.behavioral + + Scenario: Existing behavior + id: scenario.behavioral.existing + When the feature runs + → id: outcome.behavioral.existing; result is valid + +Constraint: Legacy boundary + verification: documentation-only + rationale: this belongs to the constraint +"#; + + let intent = IntentFile::parse_content_with_id_mode( + content, + "feature-constraint.intent".to_string(), + IdMode::Strict, + ) + .expect("constraint metadata must not alter feature verification"); + + assert!(matches!( + intent.features[0].verification, + FeatureVerification::Behavioral + )); +} From 0181a100c1135ee6fb0a38cca92597f330551107 Mon Sep 17 00:00:00 2001 From: Larri Date: Tue, 4 Aug 2026 19:39:27 -0600 Subject: [PATCH 6/6] fix: narrow Intent obligation identity semantics --- src/intent.rs | 783 ++++++++++++++++---- src/verification/ids.rs | 42 +- src/verification/mod.rs | 16 +- src/verification/model.rs | 1017 +++++++++++++++++++++++--- tests/verification_truth_tests.rs | 1106 +++++++++++++++++++++++++---- 5 files changed, 2593 insertions(+), 371 deletions(-) diff --git a/src/intent.rs b/src/intent.rs index 3ca7fc5..761dab9 100644 --- a/src/intent.rs +++ b/src/intent.rs @@ -34,6 +34,7 @@ use std::collections::{HashMap, HashSet}; use std::fs; use std::io::{Read, Write}; use std::net::TcpStream; +use std::ops::{Deref, DerefMut}; use std::path::Path; use std::sync::atomic::{AtomicBool, Ordering}; use std::sync::Arc; @@ -2190,31 +2191,33 @@ pub struct Invariant { /// Feature-level verification declaration. Documentation-only is deliberately /// unavailable on scenarios and outcomes. -#[derive(Debug, Clone, PartialEq, Eq, Serialize)] +#[derive(Debug, Clone, PartialEq, Eq)] pub enum FeatureVerification { Behavioral, DocumentationOnly { rationale: String }, } /// Stable identity and location paired with an existing outcome string. -#[derive(Debug, Clone, PartialEq, Eq, Serialize)] -pub struct OutcomeMetadata { - pub id: StableId, - pub source: SourceSpan, +#[derive(Debug, Clone, PartialEq, Eq)] +pub(crate) struct OutcomeMetadata { + pub(crate) id: StableId, + pub(crate) source: SourceSpan, +} + +/// The declaration that owns a parsed scenario. +/// +/// Constraint scenarios remain in the legacy feature/component collections for +/// compatibility, but are not behavioral feature obligations. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub(crate) enum ScenarioOrigin { + Feature, + Component, + Constraint, } /// A natural language scenario that can be executed as a test #[derive(Debug, Clone, Serialize)] pub struct Scenario { - /// Explicit source spelling, absent for compatibility-derived IDs. - #[serde(skip)] - pub id: Option, - #[serde(skip)] - pub verification_id: StableId, - #[serde(skip)] - pub verification_id_source: SourceSpan, - #[serde(skip)] - pub source: SourceSpan, /// Scenario name (e.g., "Successful login") pub name: String, /// Optional description explaining why this scenario exists @@ -2227,9 +2230,6 @@ pub struct Scenario { pub when_clause: String, /// The outcome clauses (each "→" line) pub outcomes: Vec, - /// Stable IDs and locations corresponding one-for-one with `outcomes`. - #[serde(skip)] - pub outcome_metadata: Vec, /// Resolved test case (after glossary term resolution) #[serde(skip_serializing_if = "Option::is_none")] pub resolved_test: Option, @@ -2682,16 +2682,8 @@ pub struct TestCase { #[derive(Debug, Clone, Serialize)] pub struct Feature { pub id: Option, - #[serde(skip)] - pub verification_id: StableId, - #[serde(skip)] - pub verification_id_source: SourceSpan, - #[serde(skip)] - pub source: SourceSpan, pub name: String, pub description: Option, - #[serde(skip)] - pub verification: FeatureVerification, /// Traditional test cases (technical format) pub tests: Vec, /// Natural language scenarios (IAL format) @@ -2719,9 +2711,267 @@ pub struct IntentFile { /// Test data sections (for unit testing) #[serde(skip_serializing_if = "Vec::is_empty")] pub test_data: Vec, - /// Source-located warnings emitted only for compatibility-derived IDs. - #[serde(skip)] - pub verification_warnings: Vec, +} + +/// An intent AST paired with stable verification identity owned by the parser. +/// +/// The wrapped [`IntentFile`] retains its pre-verification public shape. The +/// sidecar is immutable after parsing so edits to public truth-model fields +/// cannot redefine canonical declaration ownership. +#[derive(Debug)] +pub struct IdentifiedIntent { + intent: IntentFile, + metadata: IntentMetadata, +} + +#[derive(Debug)] +pub(crate) struct IntentMetadata { + pub(crate) features: Vec, + pub(crate) components: Vec, + warnings: Vec, +} + +#[derive(Debug)] +pub(crate) struct FeatureMetadata { + pub(crate) id: StableId, + pub(crate) id_source: SourceSpan, + pub(crate) source: SourceSpan, + pub(crate) verification: FeatureVerification, + pub(crate) scenarios: Vec, +} + +#[derive(Debug)] +pub(crate) struct ComponentMetadata { + pub(crate) scenarios: Vec, +} + +#[derive(Debug)] +pub(crate) struct ScenarioMetadata { + pub(crate) id: StableId, + pub(crate) id_source: SourceSpan, + pub(crate) source: SourceSpan, + pub(crate) origin: ScenarioOrigin, + pub(crate) outcomes: Vec, +} + +#[derive(Debug)] +struct ParsedScenario { + ast: Scenario, + id: Option, + verification_id: StableId, + verification_id_source: SourceSpan, + source: SourceSpan, + origin: ScenarioOrigin, + outcome_metadata: Vec, +} + +impl Deref for ParsedScenario { + type Target = Scenario; + + fn deref(&self) -> &Self::Target { + &self.ast + } +} + +impl DerefMut for ParsedScenario { + fn deref_mut(&mut self) -> &mut Self::Target { + &mut self.ast + } +} + +#[derive(Debug)] +struct ParsedFeature { + ast: Feature, + verification_id: StableId, + verification_id_source: SourceSpan, + source: SourceSpan, + verification: FeatureVerification, + scenarios: Vec, +} + +impl Deref for ParsedFeature { + type Target = Feature; + + fn deref(&self) -> &Self::Target { + &self.ast + } +} + +impl DerefMut for ParsedFeature { + fn deref_mut(&mut self) -> &mut Self::Target { + &mut self.ast + } +} + +impl ParsedFeature { + fn into_parts(mut self) -> (Feature, FeatureMetadata) { + let (scenarios, scenario_metadata): (Vec<_>, Vec<_>) = self + .scenarios + .into_iter() + .map(ParsedScenario::into_parts) + .unzip(); + self.ast.scenarios = scenarios; + ( + self.ast, + FeatureMetadata { + id: self.verification_id, + id_source: self.verification_id_source, + source: self.source, + verification: self.verification, + scenarios: scenario_metadata, + }, + ) + } +} + +#[derive(Debug)] +struct ParsedComponent { + ast: Component, + scenarios: Vec, +} + +impl Deref for ParsedComponent { + type Target = Component; + + fn deref(&self) -> &Self::Target { + &self.ast + } +} + +impl DerefMut for ParsedComponent { + fn deref_mut(&mut self) -> &mut Self::Target { + &mut self.ast + } +} + +impl ParsedComponent { + fn into_parts(mut self) -> (Component, ComponentMetadata) { + let (scenarios, scenario_metadata): (Vec<_>, Vec<_>) = self + .scenarios + .into_iter() + .map(ParsedScenario::into_parts) + .unzip(); + self.ast.scenarios = scenarios; + ( + self.ast, + ComponentMetadata { + scenarios: scenario_metadata, + }, + ) + } +} + +impl ParsedScenario { + fn into_parts(self) -> (Scenario, ScenarioMetadata) { + ( + self.ast, + ScenarioMetadata { + id: self.verification_id, + id_source: self.verification_id_source, + source: self.source, + origin: self.origin, + outcomes: self.outcome_metadata, + }, + ) + } +} + +impl IdentifiedIntent { + pub fn as_intent(&self) -> &IntentFile { + &self.intent + } + + pub fn into_intent(self) -> IntentFile { + self.intent + } + + pub fn verification_warnings(&self) -> &[IdWarning] { + &self.metadata.warnings + } + + pub fn feature_stable_id(&self, feature_index: usize) -> Option<&StableId> { + self.metadata + .features + .get(feature_index) + .map(|feature| &feature.id) + } + + pub fn feature_verification(&self, feature_index: usize) -> Option<&FeatureVerification> { + self.metadata + .features + .get(feature_index) + .map(|feature| &feature.verification) + } + + pub fn scenario_stable_id( + &self, + feature_index: usize, + scenario_index: usize, + ) -> Option<&StableId> { + self.metadata + .features + .get(feature_index)? + .scenarios + .get(scenario_index) + .map(|scenario| &scenario.id) + } + + pub fn component_scenario_stable_id( + &self, + component_index: usize, + scenario_index: usize, + ) -> Option<&StableId> { + self.metadata + .components + .get(component_index)? + .scenarios + .get(scenario_index) + .map(|scenario| &scenario.id) + } + + pub fn outcome_stable_id( + &self, + feature_index: usize, + scenario_index: usize, + outcome_index: usize, + ) -> Option<&StableId> { + self.metadata + .features + .get(feature_index)? + .scenarios + .get(scenario_index)? + .outcomes + .get(outcome_index) + .map(|outcome| &outcome.id) + } + + pub fn component_outcome_stable_id( + &self, + component_index: usize, + scenario_index: usize, + outcome_index: usize, + ) -> Option<&StableId> { + self.metadata + .components + .get(component_index)? + .scenarios + .get(scenario_index)? + .outcomes + .get(outcome_index) + .map(|outcome| &outcome.id) + } + + pub(crate) fn metadata(&self) -> &IntentMetadata { + &self.metadata + } +} + +impl Deref for IdentifiedIntent { + type Target = IntentFile; + + fn deref(&self) -> &Self::Target { + self.as_intent() + } } /// A section of test data linked to a feature/scenario @@ -2829,11 +3079,18 @@ pub struct FeatureCoverage { impl IntentFile { /// Parse an intent file from a path while preserving legacy behavior. pub fn parse(path: &Path) -> Result { - Self::parse_with_id_mode(path, IdMode::Compatibility) + let content = fs::read_to_string(path).map_err(|e| { + IntentError::runtime_error(format!("Failed to read intent file: {}", e)) + })?; + + Self::parse_content(&content, path.to_string_lossy().to_string()) } /// Parse an intent file with explicit stable-ID policy. - pub fn parse_with_id_mode(path: &Path, id_mode: IdMode) -> Result { + pub fn parse_with_id_mode( + path: &Path, + id_mode: IdMode, + ) -> Result { let content = fs::read_to_string(path).map_err(|e| { IntentError::runtime_error(format!("Failed to read intent file: {}", e)) })?; @@ -2894,6 +3151,7 @@ impl IntentFile { /// Parse intent file content while preserving legacy behavior. pub fn parse_content(content: &str, source_path: String) -> Result { Self::parse_content_with_id_mode(content, source_path, IdMode::Compatibility) + .map(IdentifiedIntent::into_intent) } /// Parse intent file content with explicit stable-ID policy. @@ -2901,21 +3159,21 @@ impl IntentFile { content: &str, source_path: String, id_mode: IdMode, - ) -> Result { - let mut features = Vec::new(); - let mut components = Vec::new(); + ) -> Result { + let mut features: Vec = Vec::new(); + let mut components: Vec = Vec::new(); let mut invariants: Vec = Vec::new(); let mut test_data_sections: Vec = Vec::new(); let mut glossary = Glossary::new(); let mut has_glossary = false; let mut title: Option = None; let mut expecting_title = false; - let mut current_feature: Option = None; - let mut current_component: Option = None; + let mut current_feature: Option = None; + let mut current_component: Option = None; let mut current_invariant: Option = None; let mut current_test_data: Option = None; let mut current_test: Option = None; - let mut current_scenario: Option = None; + let mut current_scenario: Option = None; let mut in_assertions = false; let mut in_glossary = false; let mut in_component_inherent = false; @@ -2946,6 +3204,42 @@ impl IntentFile { continue; } + // Markdown headings are parser-section boundaries. Finish the previous + // section before the named heading below enables its own state. + if trimmed.starts_with("##") { + Self::finish_current_scenario( + &mut current_scenario, + &mut current_feature, + &mut current_component, + ); + if let Some(test) = current_test.take() { + if let Some(feature) = current_feature.as_mut() { + feature.tests.push(test); + } + } + if let Some((term, binding)) = current_binding_term.take() { + glossary.set_binding(&term, binding); + } + if let Some(test_data) = current_test_data.take() { + test_data_sections.push(test_data); + } + if let Some(invariant) = current_invariant.take() { + invariants.push(invariant); + } + in_constraint = false; + in_glossary = false; + _in_glossary_bindings = false; + in_binding_assert_list = false; + in_test_data_table = false; + test_data_columns.clear(); + in_invariant_assertions = false; + in_component_inherent = false; + in_assertions = false; + if !trimmed.starts_with("## Title") { + expecting_title = false; + } + } + // Section separator (---) if trimmed == "---" { // Save current scenario to feature if any @@ -2966,25 +3260,41 @@ impl IntentFile { } components.push(comp); } - // Save any pending binding term + // Save any pending binding term or parser-owned section. if let Some((term, binding)) = current_binding_term.take() { glossary.set_binding(&term, binding); } - // Reset scenario state since we just saved it + if let Some(test_data) = current_test_data.take() { + test_data_sections.push(test_data); + } + if let Some(invariant) = current_invariant.take() { + invariants.push(invariant); + } + // Reset section state since the separator closed it. current_scenario = None; current_test = None; in_glossary = false; in_component_inherent = false; _in_glossary_bindings = false; in_binding_assert_list = false; + in_test_data_table = false; + test_data_columns.clear(); + in_invariant_assertions = false; + in_assertions = false; + in_constraint = false; + expecting_title = false; continue; } - // Capture title from next line after ## Title header + // Capture title from next non-declaration line after ## Title. if expecting_title && title.is_none() { - title = Some(trimmed.to_string()); - expecting_title = false; - continue; + if Self::is_named_declaration(trimmed) { + expecting_title = false; + } else { + title = Some(trimmed.to_string()); + expecting_title = false; + continue; + } } // Title section header: ## Title @@ -3016,6 +3326,64 @@ impl IntentFile { continue; } + // Named declarations also end any surrounding Markdown parser section. + // Their declaration-specific handling below owns the semantic transition. + let is_legacy_test_declaration = trimmed == "test:"; + let is_test_data_declaration = + trimmed.starts_with("Test Cases:") || trimmed.starts_with("Test Data:"); + let is_named_declaration = Self::is_named_declaration(trimmed); + if is_named_declaration { + if let Some((term, binding)) = current_binding_term.take() { + glossary.set_binding(&term, binding); + } + if let Some(test_data) = current_test_data.take() { + test_data_sections.push(test_data); + } + if let Some(invariant) = current_invariant.take() { + invariants.push(invariant); + } + in_glossary = false; + _in_glossary_bindings = false; + in_binding_assert_list = false; + in_test_data_table = false; + test_data_columns.clear(); + in_invariant_assertions = false; + expecting_title = false; + } + if is_test_data_declaration || is_legacy_test_declaration { + Self::finish_current_scenario( + &mut current_scenario, + &mut current_feature, + &mut current_component, + ); + in_constraint = false; + } + if id_mode == IdMode::Strict && is_legacy_test_declaration && current_feature.is_none() + { + return Err(Self::verification_error( + &Self::line_span(&source_path, line_number, line, "test:"), + "test requires an active Feature owner", + )); + } + + if id_mode == IdMode::Strict + && (trimmed.starts_with('→') || trimmed.starts_with("->")) + && current_scenario.is_none() + && current_invariant.is_none() + && !_in_glossary_bindings + && !in_component_inherent + { + let marker = if trimmed.starts_with('→') { + "→" + } else { + "->" + }; + return Err(Self::verification_error( + &Self::line_span(&source_path, line_number, line, marker), + "outcome requires an active Scenario or Invariant owner", + )); + } + // Parse glossary table rows: | term | meaning | or | term | type | meaning | if in_glossary && trimmed.starts_with('|') && !trimmed.contains("---") { let parts: Vec<&str> = trimmed.split('|').collect(); @@ -3166,6 +3534,13 @@ impl IntentFile { component.scenarios.push(scenario); } } + if let Some(test) = current_test.take() { + if let Some(feature) = current_feature.as_mut() { + feature.tests.push(test); + } + } + in_assertions = false; + in_component_inherent = false; in_constraint = true; continue; } @@ -3199,19 +3574,20 @@ impl IntentFile { let name = trimmed.trim_start_matches("Feature:").trim().to_string(); let source = Self::line_span(&source_path, line_number, line, "Feature:"); - current_feature = Some(Feature { - id: None, - verification_id: StableId::compatibility_derived( - IdKind::Feature, - &[&name], - features.len(), - ), + let verification_id = + StableId::compatibility_derived(IdKind::Feature, &[&name], features.len()); + current_feature = Some(ParsedFeature { + ast: Feature { + id: None, + name, + description: None, + tests: Vec::new(), + scenarios: Vec::new(), + }, + verification_id, verification_id_source: source.clone(), source, - name, - description: None, verification: FeatureVerification::Behavioral, - tests: Vec::new(), scenarios: Vec::new(), }); current_test = None; @@ -3252,12 +3628,15 @@ impl IntentFile { } let name = trimmed.trim_start_matches("Component:").trim().to_string(); - current_component = Some(Component { - id: String::new(), - name, - description: None, - parameters: Vec::new(), - inherent_behavior: Vec::new(), + current_component = Some(ParsedComponent { + ast: Component { + id: String::new(), + name, + description: None, + parameters: Vec::new(), + inherent_behavior: Vec::new(), + scenarios: Vec::new(), + }, scenarios: Vec::new(), }); current_test = None; @@ -3273,6 +3652,17 @@ impl IntentFile { continue; } + if id_mode == IdMode::Strict + && trimmed.starts_with("Scenario:") + && current_feature.is_none() + && current_component.is_none() + { + return Err(Self::verification_error( + &Self::line_span(&source_path, line_number, line, "Scenario:"), + "scenario requires an active Feature or Component owner", + )); + } + // Invariant declaration if trimmed.starts_with("Invariant:") { in_constraint = false; @@ -3464,16 +3854,19 @@ impl IntentFile { continue; } - // Description - only for component if not inside a scenario - if trimmed.starts_with("description:") && current_scenario.is_none() { + // Description - only for component if not inside a scenario or Constraint + if trimmed.starts_with("description:") + && current_scenario.is_none() + && !in_constraint + { let desc = trimmed.trim_start_matches("description:").trim(); let desc = desc.trim_matches('"').to_string(); component.description = Some(desc); continue; } - // Parameters - if trimmed.starts_with("parameters:") { + // Parameters belong to the component, never a following Constraint. + if trimmed.starts_with("parameters:") && !in_constraint { let params_str = trimmed.trim_start_matches("parameters:").trim(); // Parse [param1, param2] or [param1] format let params_str = params_str.trim_matches(|c| c == '[' || c == ']'); @@ -3485,9 +3878,10 @@ impl IntentFile { continue; } - // Inherent Behavior section - if trimmed.starts_with("Inherent Behavior:") - || trimmed.starts_with("inherent_behavior:") + // Inherent Behavior section belongs to the component, not a Constraint. + if !in_constraint + && (trimmed.starts_with("Inherent Behavior:") + || trimmed.starts_with("inherent_behavior:")) { in_component_inherent = true; continue; @@ -3503,23 +3897,37 @@ impl IntentFile { let name = trimmed.trim_start_matches("Scenario:").trim().to_string(); let source = Self::line_span(&source_path, line_number, line, "Scenario:"); - current_scenario = Some(Scenario { + let component_ordinal = (components.len() + 1).to_string(); + current_scenario = Some(ParsedScenario { + ast: Scenario { + name: name.clone(), + description: None, + given_clause: None, + when_clause: String::new(), + outcomes: Vec::new(), + resolved_test: None, + component_refs: Vec::new(), + }, id: None, verification_id: StableId::compatibility_derived( IdKind::Scenario, - &[&component.name, &name], + &[ + "component", + &component_ordinal, + &component.id, + &component.name, + &name, + ], component.scenarios.len(), ), verification_id_source: source.clone(), source, - name, - description: None, - given_clause: None, - when_clause: String::new(), - outcomes: Vec::new(), + origin: if in_constraint { + ScenarioOrigin::Constraint + } else { + ScenarioOrigin::Component + }, outcome_metadata: Vec::new(), - resolved_test: None, - component_refs: Vec::new(), }); continue; } @@ -3527,8 +3935,26 @@ impl IntentFile { // Inside component scenario if let Some(ref mut scenario) = current_scenario { if trimmed.starts_with("id:") { + if in_constraint { + continue; + } let id = trimmed.trim_start_matches("id:").trim(); let id_source = Self::line_span(&source_path, line_number, line, "id:"); + if scenario.id.is_some() { + return Err(Self::verification_error( + &id_source, + format!( + "repeated scenario ID; first declared at {}", + scenario.verification_id_source.location() + ), + )); + } + if !scenario.outcomes.is_empty() { + return Err(Self::verification_error( + &id_source, + "scenario ID must appear before outcomes", + )); + } scenario.id = Some(id.to_string()); scenario.verification_id = Self::explicit_id(id, IdKind::Scenario, &id_source)?; @@ -3567,8 +3993,9 @@ impl IntentFile { line_number, line, raw_outcome, - &scenario.name, + &scenario.verification_id, scenario.outcomes.len(), + scenario.origin != ScenarioOrigin::Constraint, )?; scenario.outcomes.push(outcome); scenario.outcome_metadata.push(metadata); @@ -3576,8 +4003,8 @@ impl IntentFile { } } - // Inherent behavior outcomes - if in_component_inherent { + // Inherent behavior outcomes never consume Constraint lines. + if in_component_inherent && !in_constraint { if trimmed.starts_with("→") || trimmed.starts_with("->") { let outcome = trimmed .trim_start_matches("→") @@ -3596,18 +4023,41 @@ impl IntentFile { if let Some(ref mut feature) = current_feature { // Scenario ID must be handled before the enclosing feature ID. if trimmed.starts_with("id:") { + if in_constraint { + continue; + } let id = trimmed.trim_start_matches("id:").trim(); let id_source = Self::line_span(&source_path, line_number, line, "id:"); if let Some(scenario) = current_scenario.as_mut() { + if scenario.id.is_some() { + return Err(Self::verification_error( + &id_source, + format!( + "repeated scenario ID; first declared at {}", + scenario.verification_id_source.location() + ), + )); + } + if !scenario.outcomes.is_empty() { + return Err(Self::verification_error( + &id_source, + "scenario ID must appear before outcomes", + )); + } scenario.id = Some(id.to_string()); scenario.verification_id = Self::explicit_id(id, IdKind::Scenario, &id_source)?; scenario.verification_id_source = id_source; - } else if in_constraint { - // Keep legacy serialized IDs stable without promoting a - // constraint ID into feature verification identity. - feature.id = Some(id.to_string()); } else { + if feature.id.is_some() { + return Err(Self::verification_error( + &id_source, + format!( + "repeated feature ID; first declared at {}", + feature.verification_id_source.location() + ), + )); + } feature.verification_id = Self::explicit_id(id, IdKind::Feature, &id_source)?; feature.verification_id_source = id_source; @@ -3657,8 +4107,11 @@ impl IntentFile { continue; } - // Description - only for feature if not inside a scenario - if trimmed.starts_with("description:") && current_scenario.is_none() { + // Description - only for feature if not inside a scenario or Constraint + if trimmed.starts_with("description:") + && current_scenario.is_none() + && !in_constraint + { let desc = trimmed.trim_start_matches("description:").trim(); // Remove surrounding quotes if present let desc = desc.trim_matches('"').to_string(); @@ -3679,23 +4132,31 @@ impl IntentFile { let name = trimmed.trim_start_matches("Scenario:").trim().to_string(); let source = Self::line_span(&source_path, line_number, line, "Scenario:"); - current_scenario = Some(Scenario { + current_scenario = Some(ParsedScenario { + ast: Scenario { + name: name.clone(), + description: None, + given_clause: None, + when_clause: String::new(), + outcomes: Vec::new(), + resolved_test: None, + component_refs: Vec::new(), + }, id: None, - verification_id: StableId::compatibility_derived( + verification_id: StableId::compatibility_child( IdKind::Scenario, - &[&feature.name, &name], + &feature.verification_id, + &[&name], feature.scenarios.len(), ), verification_id_source: source.clone(), source, - name, - description: None, - given_clause: None, - when_clause: String::new(), - outcomes: Vec::new(), + origin: if in_constraint { + ScenarioOrigin::Constraint + } else { + ScenarioOrigin::Feature + }, outcome_metadata: Vec::new(), - resolved_test: None, - component_refs: Vec::new(), }); in_assertions = false; continue; @@ -3734,8 +4195,9 @@ impl IntentFile { line_number, line, raw_outcome, - &scenario.name, + &scenario.verification_id, scenario.outcomes.len(), + scenario.origin != ScenarioOrigin::Constraint, )?; scenario.outcomes.push(outcome); scenario.outcome_metadata.push(metadata); @@ -3744,7 +4206,7 @@ impl IntentFile { } // Test section start - if trimmed == "test:" { + if trimmed == "test:" && !in_constraint { // Save any current scenario first if let Some(scenario) = current_scenario.take() { feature.scenarios.push(scenario); @@ -3754,7 +4216,9 @@ impl IntentFile { } // Request line (starts a new test case) - if trimmed.starts_with("- request:") || trimmed.starts_with("request:") { + if !in_constraint + && (trimmed.starts_with("- request:") || trimmed.starts_with("request:")) + { // Save previous test if let Some(test) = current_test.take() { feature.tests.push(test); @@ -3784,13 +4248,13 @@ impl IntentFile { } // Assert section - if trimmed == "assert:" { + if trimmed == "assert:" && !in_constraint { in_assertions = true; continue; } // Assertion lines - if in_assertions { + if in_assertions && !in_constraint { if let Some(ref mut test) = current_test { if let Some(assertion) = Self::parse_assertion(trimmed) { test.assertions.push(assertion); @@ -3800,7 +4264,7 @@ impl IntentFile { } // Body for POST requests - if trimmed.starts_with("body:") { + if trimmed.starts_with("body:") && !in_constraint { if let Some(ref mut test) = current_test { let body = trimmed.trim_start_matches("body:").trim(); let body = body.trim_matches('"').to_string(); @@ -3850,18 +4314,59 @@ impl IntentFile { &mut verification_warnings, )?; - Ok(IntentFile { - features, - source_path, - title, - glossary: if has_glossary { Some(glossary) } else { None }, - components, - invariants, - test_data: test_data_sections, - verification_warnings, + let (features, feature_metadata): (Vec<_>, Vec<_>) = + features.into_iter().map(ParsedFeature::into_parts).unzip(); + let (components, component_metadata): (Vec<_>, Vec<_>) = components + .into_iter() + .map(ParsedComponent::into_parts) + .unzip(); + + Ok(IdentifiedIntent { + intent: IntentFile { + features, + source_path, + title, + glossary: if has_glossary { Some(glossary) } else { None }, + components, + invariants, + test_data: test_data_sections, + }, + metadata: IntentMetadata { + features: feature_metadata, + components: component_metadata, + warnings: verification_warnings, + }, }) } + fn is_named_declaration(trimmed: &str) -> bool { + trimmed.starts_with("Scenario:") + || trimmed == "test:" + || trimmed.starts_with("Test Cases:") + || trimmed.starts_with("Test Data:") + || trimmed.starts_with("Feature:") + || trimmed.starts_with("Component:") + || trimmed.starts_with("Constraint:") + || trimmed.starts_with("Invariant:") + } + + fn finish_current_scenario( + current_scenario: &mut Option, + current_feature: &mut Option, + current_component: &mut Option, + ) { + let Some(scenario) = current_scenario.take() else { + return; + }; + if let Some(feature) = current_feature.as_mut() { + feature.scenarios.push(scenario); + } else if let Some(component) = current_component.as_mut() { + component.scenarios.push(scenario); + } else { + *current_scenario = Some(scenario); + } + } + fn line_span(source_path: &str, line_number: usize, line: &str, marker: &str) -> SourceSpan { let start_column = line .find(marker) @@ -3893,11 +4398,16 @@ impl IntentFile { line_number: usize, line: &str, raw_outcome: &str, - scenario_name: &str, + scenario_id: &StableId, ordinal: usize, + allow_verification_metadata: bool, ) -> Result<(String, OutcomeMetadata), IntentError> { - let has_explicit_id = raw_outcome.starts_with("id:"); - let source_marker = if has_explicit_id { + let explicit_id = allow_verification_metadata + .then_some(raw_outcome) + .and_then(|outcome| outcome.strip_prefix("id:")) + .and_then(|declaration| declaration.split_once(';')) + .filter(|(id, _)| id.trim().starts_with("outcome.")); + let source_marker = if explicit_id.is_some() { "id:" } else if line.contains('→') { "→" @@ -3906,13 +4416,7 @@ impl IntentFile { }; let source = Self::line_span(source_path, line_number, line, source_marker); - let (statement, id) = if let Some(id_declaration) = raw_outcome.strip_prefix("id:") { - let Some((id, statement)) = id_declaration.split_once(';') else { - return Err(Self::verification_error( - &source, - "outcome ID must be followed by ';' and an outcome statement", - )); - }; + let (statement, id) = if let Some((id, statement)) = explicit_id { let id = id.trim(); let statement = statement.trim(); if statement.is_empty() { @@ -3928,15 +4432,16 @@ impl IntentFile { } else { ( raw_outcome.to_string(), - StableId::compatibility_derived( + StableId::compatibility_child( IdKind::Outcome, - &[scenario_name, raw_outcome], + scenario_id, + &[raw_outcome], ordinal, ), ) }; - if statement == "verification: documentation-only" { + if allow_verification_metadata && statement == "verification: documentation-only" { return Err(Self::verification_error( &source, "documentation-only is valid only on a feature", @@ -3953,8 +4458,8 @@ impl IntentFile { } fn finalize_verification_ids( - features: &[Feature], - components: &[Component], + features: &[ParsedFeature], + components: &[ParsedComponent], id_mode: IdMode, warnings: &mut Vec, ) -> Result<(), IntentError> { @@ -3977,10 +4482,16 @@ impl IntentFile { "verification: documentation-only requires a non-empty rationale", )); } - if !feature.scenarios.is_empty() || !feature.tests.is_empty() { + if feature + .scenarios + .iter() + .any(|scenario| scenario.origin == ScenarioOrigin::Feature) + || !feature.tests.is_empty() + { let span = feature .scenarios - .first() + .iter() + .find(|scenario| scenario.origin == ScenarioOrigin::Feature) .map(|scenario| &scenario.source) .unwrap_or(&feature.source); return Err(Self::verification_error( @@ -3991,6 +4502,9 @@ impl IntentFile { } for scenario in &feature.scenarios { + if scenario.origin != ScenarioOrigin::Feature { + continue; + } Self::check_id_policy( &scenario.verification_id, &scenario.source, @@ -4012,6 +4526,9 @@ impl IntentFile { for component in components { for scenario in &component.scenarios { + if scenario.origin != ScenarioOrigin::Component { + continue; + } Self::check_id_policy( &scenario.verification_id, &scenario.source, @@ -7498,27 +8015,11 @@ Feature: API }]; let scenario = Scenario { - id: None, - verification_id: StableId::compatibility_derived( - IdKind::Scenario, - &["test-slugify-function"], - 0, - ), - verification_id_source: SourceSpan::single_line("test.intent", 1, 1, 1), - source: SourceSpan::single_line("test.intent", 1, 1, 1), name: "Test slugify function".to_string(), description: None, given_clause: None, when_clause: "testing slugify".to_string(), outcomes: vec!["result is valid".to_string()], - outcome_metadata: vec![OutcomeMetadata { - id: StableId::compatibility_derived( - IdKind::Outcome, - &["test-slugify-function", "result-is-valid"], - 0, - ), - source: SourceSpan::single_line("test.intent", 2, 1, 1), - }], resolved_test: None, component_refs: vec![], }; diff --git a/src/verification/ids.rs b/src/verification/ids.rs index 8e82abc..8ac0657 100644 --- a/src/verification/ids.rs +++ b/src/verification/ids.rs @@ -1,8 +1,7 @@ -use serde::Serialize; use std::fmt; /// Source range for a declaration or diagnostic. -#[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize)] +#[derive(Debug, Clone, PartialEq, Eq, Hash)] pub struct SourceSpan { pub path: String, pub start_line: usize, @@ -45,7 +44,7 @@ pub enum IdMode { Compatibility, } -#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Serialize)] +#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)] pub enum IdKind { Feature, Scenario, @@ -68,14 +67,14 @@ impl fmt::Display for IdKind { } } -#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Serialize)] +#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)] pub enum IdOrigin { Explicit, CompatibilityDerived, } /// A validated verification identity. -#[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize)] +#[derive(Debug, Clone, PartialEq, Eq, Hash)] pub struct StableId { value: String, kind: IdKind, @@ -112,6 +111,37 @@ impl StableId { } } + /// Derive a compatibility identity beneath an already unique parent. + pub(crate) fn compatibility_child( + kind: IdKind, + parent: &Self, + labels: &[&str], + ordinal: usize, + ) -> Self { + let label = labels + .iter() + .map(|label| slug(label)) + .filter(|label| !label.is_empty()) + .collect::>() + .join("."); + let label = if label.is_empty() { + "unnamed".to_string() + } else { + label + }; + Self { + value: format!( + "{}.compat.{}.{}.{}", + kind.prefix(), + parent.value, + label, + ordinal + 1 + ), + kind, + origin: IdOrigin::CompatibilityDerived, + } + } + pub fn as_str(&self) -> &str { &self.value } @@ -139,7 +169,7 @@ impl AsRef for StableId { /// A compatibility diagnostic. Derived identity is deliberately visible because /// it changes when legacy declarations are renamed or reordered. -#[derive(Debug, Clone, PartialEq, Eq, Serialize)] +#[derive(Debug, Clone, PartialEq, Eq)] pub struct IdWarning { pub message: String, pub id: StableId, diff --git a/src/verification/mod.rs b/src/verification/mod.rs index fe1dbc5..6e8a891 100644 --- a/src/verification/mod.rs +++ b/src/verification/mod.rs @@ -1,7 +1,15 @@ //! Stable obligation identity and orthogonal verification truth types. //! -//! Slice 1A deliberately contains no renderer, schema, threshold, policy, -//! planner, executor, or exit-status behavior. +//! Compatibility-derived identities keep existing Intent files parseable, but +//! remain rename/reorder-sensitive migration markers. Durable cross-run evidence +//! must use strict parsing with explicit IDs. Parser-owned identity metadata lives +//! in `IdentifiedIntent`, preserving the legacy public `IntentFile`/`Feature`/ +//! `Scenario` AST shapes. Legacy Constraint scenarios stay visible in that AST +//! without becoming feature obligations. +//! +//! Slice 1A deliberately exposes read-only truth queries and contains no evidence +//! ingestion authority, renderer, serialization contract, schema, threshold, +//! policy, planner, executor, resource lifecycle, or exit-status behavior. pub mod ids; pub mod model; @@ -9,6 +17,6 @@ pub mod model; pub use ids::{IdKind, IdMode, IdOrigin, IdWarning, SourceSpan, StableId}; pub use model::{ AssertionResolution, BindingStatus, DeclarationStatus, Disposition, EvidenceBinding, - ExecutabilityStatus, ExecutableCoverage, FeatureProofStatus, FeatureTruth, Freshness, - ImplementationCoverage, LinkageStatus, Obligation, VerificationTruth, VerifiedCoverage, + ExecutabilityStatus, ExecutableCoverage, FeatureTruth, Freshness, ImplementationCoverage, + LinkageStatus, Obligation, VerificationTruth, VerifiedCoverage, }; diff --git a/src/verification/model.rs b/src/verification/model.rs index 1cc665b..10cded0 100644 --- a/src/verification/model.rs +++ b/src/verification/model.rs @@ -1,38 +1,36 @@ use std::collections::HashMap; -use serde::Serialize; +use crate::intent::{FeatureVerification, IdentifiedIntent, ScenarioOrigin}; -use crate::intent::{FeatureVerification, IntentFile}; +use super::ids::{IdKind, SourceSpan, StableId}; -use super::ids::{SourceSpan, StableId}; - -#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize)] +#[derive(Debug, Clone, Copy, PartialEq, Eq)] pub enum DeclarationStatus { Declared, DocumentationOnly, } -#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize)] +#[derive(Debug, Clone, Copy, PartialEq, Eq)] pub enum LinkageStatus { Linked, Unlinked, } -#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize)] +#[derive(Debug, Clone, Copy, PartialEq, Eq)] pub enum BindingStatus { Bound, Unbound, Ambiguous, } -#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize)] +#[derive(Debug, Clone, Copy, PartialEq, Eq)] pub enum ExecutabilityStatus { Executable, Unsupported, Blocked, } -#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize)] +#[derive(Debug, Clone, Copy, PartialEq, Eq)] pub enum Disposition { Planned, Running, @@ -44,13 +42,13 @@ pub enum Disposition { NoResult, } -#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize)] +#[derive(Debug, Clone, Copy, PartialEq, Eq)] pub enum Freshness { Current, Stale, } -#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize)] +#[derive(Debug, Clone, Copy, PartialEq, Eq)] pub enum AssertionResolution { Resolved, Unknown, @@ -58,26 +56,73 @@ pub enum AssertionResolution { } /// One candidate source of execution evidence for an obligation. -#[derive(Debug, Clone, PartialEq, Eq, Serialize)] +#[derive(Debug, Clone, PartialEq, Eq)] pub struct EvidenceBinding { - pub id: String, - pub obligation_id: String, - pub source: SourceSpan, - pub declaration: DeclarationStatus, - pub linkage: LinkageStatus, - pub binding: BindingStatus, - pub executability: ExecutabilityStatus, - pub disposition: Disposition, - pub freshness: Freshness, - pub assertion_resolution: AssertionResolution, - pub evidence_atoms: usize, + id: String, + obligation_id: StableId, + source: SourceSpan, + declaration: DeclarationStatus, + linkage: LinkageStatus, + binding: BindingStatus, + executability: ExecutabilityStatus, + disposition: Disposition, + freshness: Freshness, + assertion_resolution: AssertionResolution, + evidence_atoms: usize, } impl EvidenceBinding { + pub fn id(&self) -> &str { + &self.id + } + + pub fn obligation_id(&self) -> &StableId { + &self.obligation_id + } + + pub fn source(&self) -> &SourceSpan { + &self.source + } + + pub fn declaration(&self) -> DeclarationStatus { + self.declaration + } + + pub fn linkage(&self) -> LinkageStatus { + self.linkage + } + + pub fn binding(&self) -> BindingStatus { + self.binding + } + + pub fn executability(&self) -> ExecutabilityStatus { + self.executability + } + + pub fn disposition(&self) -> Disposition { + self.disposition + } + + pub fn freshness(&self) -> Freshness { + self.freshness + } + + pub fn assertion_resolution(&self) -> AssertionResolution { + self.assertion_resolution + } + + pub fn evidence_atoms(&self) -> usize { + self.evidence_atoms + } + /// Passing execution is evidence only when its assertion was resolved and /// produced at least one current evidence atom. - pub fn satisfies_obligation(&self) -> bool { - self.declaration == DeclarationStatus::Declared + pub fn satisfies_obligation(&self, obligation_id: &StableId) -> bool { + self.obligation_id.kind() == IdKind::Outcome + && obligation_id.kind() == IdKind::Outcome + && self.obligation_id == *obligation_id + && self.declaration == DeclarationStatus::Declared && self.binding == BindingStatus::Bound && self.executability == ExecutabilityStatus::Executable && self.disposition == Disposition::Passed @@ -88,25 +133,76 @@ impl EvidenceBinding { } /// A source-located behavioral claim produced from one scenario outcome. -#[derive(Debug, Clone, PartialEq, Eq, Serialize)] +#[derive(Debug, Clone, PartialEq, Eq)] pub struct Obligation { - pub id: StableId, - pub feature_id: StableId, - pub scenario_id: StableId, - pub statement: String, - pub source: SourceSpan, - pub declaration: DeclarationStatus, - pub linkage: LinkageStatus, - pub binding: BindingStatus, - pub executability: ExecutabilityStatus, - pub disposition: Disposition, - pub freshness: Freshness, - pub evidence_bindings: Vec, + id: StableId, + feature_id: StableId, + scenario_id: StableId, + statement: String, + source: SourceSpan, + declaration: DeclarationStatus, + linkage: LinkageStatus, + binding: BindingStatus, + executability: ExecutabilityStatus, + disposition: Disposition, + freshness: Freshness, + evidence_bindings: Vec, } impl Obligation { + pub fn id(&self) -> &StableId { + &self.id + } + + pub fn feature_id(&self) -> &StableId { + &self.feature_id + } + + pub fn scenario_id(&self) -> &StableId { + &self.scenario_id + } + + pub fn statement(&self) -> &str { + &self.statement + } + + pub fn source(&self) -> &SourceSpan { + &self.source + } + + pub fn declaration(&self) -> DeclarationStatus { + self.declaration + } + + pub fn linkage(&self) -> LinkageStatus { + self.linkage + } + + pub fn binding(&self) -> BindingStatus { + self.binding + } + + pub fn executability(&self) -> ExecutabilityStatus { + self.executability + } + + pub fn disposition(&self) -> Disposition { + self.disposition + } + + pub fn freshness(&self) -> Freshness { + self.freshness + } + + pub fn evidence_bindings(&self) -> &[EvidenceBinding] { + &self.evidence_bindings + } + pub fn is_verified(&self) -> bool { - self.declaration == DeclarationStatus::Declared + self.id.kind() == IdKind::Outcome + && self.feature_id.kind() == IdKind::Feature + && self.scenario_id.kind() == IdKind::Scenario + && self.declaration == DeclarationStatus::Declared && self.binding == BindingStatus::Bound && self.executability == ExecutabilityStatus::Executable && self.disposition == Disposition::Passed @@ -115,38 +211,61 @@ impl Obligation { && self .evidence_bindings .iter() - .all(EvidenceBinding::satisfies_obligation) + .all(|binding| binding.satisfies_obligation(&self.id)) } } -#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize)] -pub enum FeatureProofStatus { - Unproven, - Pending, - DocumentationOnly, -} - /// Feature-level truth remains visible even when there are no outcome obligations. -#[derive(Debug, Clone, PartialEq, Eq, Serialize)] +#[derive(Debug, Clone, PartialEq, Eq)] pub struct FeatureTruth { - pub id: StableId, - pub name: String, - pub source: SourceSpan, - pub declaration: DeclarationStatus, - pub rationale: Option, - pub proof_status: FeatureProofStatus, - pub obligation_ids: Vec, + id: StableId, + name: String, + source: SourceSpan, + declaration: DeclarationStatus, + rationale: Option, + obligation_ids: Vec, + /// Legacy `test:` cases that do not yet have stable obligation identities. + unrepresented_legacy_tests: usize, } impl FeatureTruth { + pub fn id(&self) -> &StableId { + &self.id + } + + pub fn name(&self) -> &str { + &self.name + } + + pub fn source(&self) -> &SourceSpan { + &self.source + } + + pub fn declaration(&self) -> DeclarationStatus { + self.declaration + } + + pub fn rationale(&self) -> Option<&str> { + self.rationale.as_deref() + } + + pub fn obligation_ids(&self) -> &[StableId] { + &self.obligation_ids + } + + pub fn unrepresented_legacy_test_count(&self) -> usize { + self.unrepresented_legacy_tests + } + pub fn is_unproven(&self) -> bool { - self.proof_status == FeatureProofStatus::Unproven + self.declaration == DeclarationStatus::Declared + && (self.obligation_ids.is_empty() || self.unrepresented_legacy_tests > 0) } } macro_rules! coverage_type { ($name:ident) => { - #[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize)] + #[derive(Debug, Clone, Copy, PartialEq, Eq)] pub struct $name { pub covered: usize, pub total: usize, @@ -158,22 +277,117 @@ coverage_type!(ImplementationCoverage); coverage_type!(ExecutableCoverage); coverage_type!(VerifiedCoverage); -/// Slice 1A's in-memory truth model. Rendering and exit policy intentionally -/// consume this in later slices rather than living here. -#[derive(Debug, Clone, PartialEq, Eq, Serialize)] +/// Slice 1A's read-only in-memory truth model. Rendering and evidence-ingestion +/// authority intentionally live outside this foundation. +/// +/// Caller code cannot rewrite the parser-owned denominator or truth status: +/// +/// ```compile_fail +/// use ntnt::verification::VerificationTruth; +/// +/// fn suppress_required_truth(truth: &mut VerificationTruth) { +/// truth.obligations.clear(); +/// truth.features[0].unrepresented_legacy_tests = 0; +/// } +/// ``` +#[derive(Debug, Clone, PartialEq, Eq)] pub struct VerificationTruth { - pub features: Vec, - pub obligations: Vec, + features: Vec, + obligations: Vec, + canonical_features: Vec, + canonical_obligations: Vec, +} + +#[derive(Debug, Clone, PartialEq, Eq)] +struct CanonicalFeature { + id: StableId, + name: String, + source: SourceSpan, + declaration: DeclarationStatus, + rationale: Option, + obligation_ids: Vec, + unrepresented_legacy_tests: usize, +} + +impl CanonicalFeature { + fn from_feature(feature: &FeatureTruth) -> Self { + Self { + id: feature.id.clone(), + name: feature.name.clone(), + source: feature.source.clone(), + declaration: feature.declaration, + rationale: feature.rationale.clone(), + obligation_ids: feature.obligation_ids.clone(), + unrepresented_legacy_tests: feature.unrepresented_legacy_tests, + } + } + + fn matches(&self, feature: &FeatureTruth) -> bool { + self.id == feature.id + && self.name == feature.name + && self.source == feature.source + && self.declaration == feature.declaration + && self.rationale == feature.rationale + && self.obligation_ids == feature.obligation_ids + && self.unrepresented_legacy_tests == feature.unrepresented_legacy_tests + } +} + +#[derive(Debug, Clone, PartialEq, Eq)] +struct CanonicalObligation { + id: StableId, + feature_id: StableId, + scenario_id: StableId, + statement: String, + source: SourceSpan, + declaration: DeclarationStatus, +} + +impl CanonicalObligation { + fn from_obligation(obligation: &Obligation) -> Self { + Self { + id: obligation.id.clone(), + feature_id: obligation.feature_id.clone(), + scenario_id: obligation.scenario_id.clone(), + statement: obligation.statement.clone(), + source: obligation.source.clone(), + declaration: obligation.declaration, + } + } + + fn matches(&self, obligation: &Obligation) -> bool { + self.id == obligation.id + && self.feature_id == obligation.feature_id + && self.scenario_id == obligation.scenario_id + && self.statement == obligation.statement + && self.source == obligation.source + && self.declaration == obligation.declaration + } } impl VerificationTruth { - pub fn from_intent(intent: &IntentFile) -> Self { + pub fn from_intent(intent: &IdentifiedIntent) -> Result { let mut features = Vec::new(); let mut obligations = Vec::new(); + let metadata = intent.metadata(); - for feature in &intent.features { - let feature_id = feature.verification_id.clone(); - let (declaration, rationale) = match &feature.verification { + if intent.features.len() != metadata.features.len() { + return Err(format!( + "feature metadata count {} does not match parsed feature count {}", + metadata.features.len(), + intent.features.len() + )); + } + + for (feature, feature_metadata) in intent.features.iter().zip(&metadata.features) { + if feature_metadata.id.kind() != IdKind::Feature { + return Err(format!( + "{}: feature identity '{}' has the wrong stable ID kind", + feature_metadata.id_source, feature_metadata.id + )); + } + let feature_id = feature_metadata.id.clone(); + let (declaration, rationale) = match &feature_metadata.verification { FeatureVerification::Behavioral => (DeclarationStatus::Declared, None), FeatureVerification::DocumentationOnly { rationale } => ( DeclarationStatus::DocumentationOnly, @@ -182,19 +396,55 @@ impl VerificationTruth { }; let mut obligation_ids = Vec::new(); + if feature.scenarios.len() != feature_metadata.scenarios.len() { + return Err(format!( + "{}: scenario metadata count {} does not match parsed scenario count {} for feature '{}'", + feature_metadata.source, + feature_metadata.scenarios.len(), + feature.scenarios.len(), + feature.name + )); + } + if declaration == DeclarationStatus::Declared { - for scenario in &feature.scenarios { - let scenario_id = scenario.verification_id.clone(); - for (statement, metadata) in - scenario.outcomes.iter().zip(&scenario.outcome_metadata) + for (scenario, scenario_metadata) in + feature.scenarios.iter().zip(&feature_metadata.scenarios) + { + if scenario_metadata.origin != ScenarioOrigin::Feature { + continue; + } + if scenario_metadata.id.kind() != IdKind::Scenario { + return Err(format!( + "{}: scenario identity '{}' has the wrong stable ID kind", + scenario_metadata.id_source, scenario_metadata.id + )); + } + if scenario.outcomes.len() != scenario_metadata.outcomes.len() { + return Err(format!( + "{}: outcome metadata count {} does not match declared outcome count {} for scenario '{}'", + scenario_metadata.source, + scenario_metadata.outcomes.len(), + scenario.outcomes.len(), + scenario.name + )); + } + let scenario_id = scenario_metadata.id.clone(); + for (statement, outcome_metadata) in + scenario.outcomes.iter().zip(&scenario_metadata.outcomes) { - obligation_ids.push(metadata.id.clone()); + if outcome_metadata.id.kind() != IdKind::Outcome { + return Err(format!( + "{}: outcome identity '{}' has the wrong stable ID kind", + outcome_metadata.source, outcome_metadata.id + )); + } + obligation_ids.push(outcome_metadata.id.clone()); obligations.push(Obligation { - id: metadata.id.clone(), + id: outcome_metadata.id.clone(), feature_id: feature_id.clone(), scenario_id: scenario_id.clone(), statement: statement.clone(), - source: metadata.source.clone(), + source: outcome_metadata.source.clone(), declaration, linkage: LinkageStatus::Unlinked, binding: BindingStatus::Unbound, @@ -207,40 +457,62 @@ impl VerificationTruth { } } - let proof_status = if declaration == DeclarationStatus::DocumentationOnly { - FeatureProofStatus::DocumentationOnly - } else if obligation_ids.is_empty() { - FeatureProofStatus::Unproven - } else { - FeatureProofStatus::Pending - }; features.push(FeatureTruth { id: feature_id, name: feature.name.clone(), - source: feature.source.clone(), + source: feature_metadata.source.clone(), declaration, rationale, - proof_status, obligation_ids, + unrepresented_legacy_tests: feature.tests.len(), }); } - Self { + let canonical_features = features + .iter() + .map(CanonicalFeature::from_feature) + .collect(); + let canonical_obligations = obligations + .iter() + .map(CanonicalObligation::from_obligation) + .collect(); + + Ok(Self { features, obligations, - } + canonical_features, + canonical_obligations, + }) + } + + pub fn features(&self) -> &[FeatureTruth] { + &self.features + } + + pub fn obligations(&self) -> &[Obligation] { + &self.obligations } pub fn behavioral_feature_count(&self) -> usize { - self.features + self.canonical_features .iter() .filter(|feature| feature.declaration == DeclarationStatus::Declared) .count() } - /// A feature is verified only when it has at least one required obligation - /// and every one of those obligations is verified. + /// A feature is verified only when it has at least one required obligation, + /// every obligation belongs to that feature, and all IDs are globally unique. pub fn feature_is_verified(&self, feature_id: &str) -> bool { + if !self.canonical_topology_is_intact() { + return false; + } + + let obligations_by_id = self + .obligations + .iter() + .map(|obligation| (&obligation.id, obligation)) + .collect::>(); + let Some(feature) = self .features .iter() @@ -248,43 +520,96 @@ impl VerificationTruth { else { return false; }; - let obligations_by_id: HashMap<&str, &Obligation> = self - .obligations - .iter() - .map(|obligation| (obligation.id.as_str(), obligation)) - .collect(); - feature.declaration == DeclarationStatus::Declared + && feature.unrepresented_legacy_tests == 0 && !feature.obligation_ids.is_empty() && feature.obligation_ids.iter().all(|obligation_id| { obligations_by_id - .get(obligation_id.as_str()) - .is_some_and(|obligation| obligation.is_verified()) + .get(obligation_id) + .is_some_and(|obligation| { + obligation.feature_id == feature.id && obligation.is_verified() + }) }) } - pub fn mark_implementation_linked(&mut self, obligation_id: &str) -> Result<(), String> { + fn canonical_topology_is_intact(&self) -> bool { + if self.features.len() != self.canonical_features.len() + || self.obligations.len() != self.canonical_obligations.len() + { + return false; + } + + let mut features_by_id = HashMap::new(); + for feature in &self.features { + if features_by_id.insert(&feature.id, feature).is_some() { + return false; + } + } + if !self.canonical_features.iter().all(|canonical| { + features_by_id + .get(&canonical.id) + .is_some_and(|feature| canonical.matches(feature)) + }) { + return false; + } + + let mut obligations_by_id = HashMap::new(); + for obligation in &self.obligations { + if obligations_by_id + .insert(&obligation.id, obligation) + .is_some() + { + return false; + } + } + self.canonical_obligations.iter().all(|canonical| { + obligations_by_id + .get(&canonical.id) + .is_some_and(|obligation| canonical.matches(obligation)) + }) + } + + #[cfg(test)] + fn mark_implementation_linked(&mut self, obligation_id: &str) -> Result<(), String> { + let match_count = self + .obligations + .iter() + .filter(|obligation| obligation.id.as_str() == obligation_id) + .count(); + match match_count { + 0 => return Err(format!("unknown obligation ID '{obligation_id}'")), + 1 => {} + _ => return Err(format!("duplicate obligation ID '{obligation_id}'")), + } let obligation = self .obligations .iter_mut() .find(|obligation| obligation.id.as_str() == obligation_id) - .ok_or_else(|| format!("unknown obligation ID '{obligation_id}'"))?; + .expect("exactly one obligation matched above"); obligation.linkage = LinkageStatus::Linked; Ok(()) } pub fn implementation_coverage(&self) -> ImplementationCoverage { + let total = self.canonical_obligations.len(); + if !self.canonical_topology_is_intact() { + return ImplementationCoverage { covered: 0, total }; + } ImplementationCoverage { covered: self .obligations .iter() .filter(|obligation| obligation.linkage == LinkageStatus::Linked) .count(), - total: self.obligations.len(), + total, } } pub fn executable_coverage(&self) -> ExecutableCoverage { + let total = self.canonical_obligations.len(); + if !self.canonical_topology_is_intact() { + return ExecutableCoverage { covered: 0, total }; + } ExecutableCoverage { covered: self .obligations @@ -294,18 +619,510 @@ impl VerificationTruth { && obligation.executability == ExecutabilityStatus::Executable }) .count(), - total: self.obligations.len(), + total, } } pub fn verified_coverage(&self) -> VerifiedCoverage { + let total = self.canonical_obligations.len(); + if !self.canonical_topology_is_intact() { + return VerifiedCoverage { covered: 0, total }; + } VerifiedCoverage { covered: self .obligations .iter() .filter(|obligation| obligation.is_verified()) .count(), - total: self.obligations.len(), + total, + } + } +} + +#[cfg(test)] +mod tests { + use super::*; + use crate::intent::IntentFile; + use crate::verification::IdMode; + + fn strict_truth(content: &str) -> VerificationTruth { + let intent = IntentFile::parse_content_with_id_mode( + content, + "verification-model-test.intent".to_string(), + IdMode::Strict, + ) + .expect("test intent must parse"); + VerificationTruth::from_intent(&intent).expect("test truth must build") + } + + fn mark_verified(obligation: &mut Obligation, binding_id: &str) { + obligation.binding = BindingStatus::Bound; + obligation.executability = ExecutabilityStatus::Executable; + obligation.disposition = Disposition::Passed; + obligation.freshness = Freshness::Current; + obligation.evidence_bindings.push(EvidenceBinding { + id: binding_id.to_string(), + obligation_id: obligation.id.clone(), + source: SourceSpan::single_line("verification.tnt", 1, 1, 2), + declaration: DeclarationStatus::Declared, + linkage: LinkageStatus::Unlinked, + binding: BindingStatus::Bound, + executability: ExecutabilityStatus::Executable, + disposition: Disposition::Passed, + freshness: Freshness::Current, + assertion_resolution: AssertionResolution::Resolved, + evidence_atoms: 1, + }); + } + + fn passing_binding(obligation_id: StableId, binding_id: &str) -> EvidenceBinding { + EvidenceBinding { + id: binding_id.to_string(), + obligation_id, + source: SourceSpan::single_line("verification.tnt", 1, 1, 2), + declaration: DeclarationStatus::Declared, + linkage: LinkageStatus::Unlinked, + binding: BindingStatus::Bound, + executability: ExecutabilityStatus::Executable, + disposition: Disposition::Passed, + freshness: Freshness::Current, + assertion_resolution: AssertionResolution::Resolved, + evidence_atoms: 1, + } + } + + #[test] + fn feature_and_obligation_topology_and_statuses_are_readable() { + let truth = strict_truth( + r#"Feature: Required claim + id: feature.required-claim + + Scenario: One claim + id: scenario.required-claim.one + When the behavior runs + → id: outcome.required-claim.one; the claim holds +"#, + ); + let feature = &truth.features()[0]; + assert_eq!(feature.id().as_str(), "feature.required-claim"); + assert_eq!(feature.name(), "Required claim"); + assert_eq!(feature.source().path, "verification-model-test.intent"); + assert_eq!(feature.declaration(), DeclarationStatus::Declared); + assert_eq!(feature.rationale(), None); + assert_eq!(feature.obligation_ids().len(), 1); + assert_eq!(feature.unrepresented_legacy_test_count(), 0); + + let obligation = &truth.obligations()[0]; + assert_eq!(obligation.id().as_str(), "outcome.required-claim.one"); + assert_eq!(obligation.feature_id(), feature.id()); + assert_eq!( + obligation.scenario_id().as_str(), + "scenario.required-claim.one" + ); + assert_eq!(obligation.statement(), "the claim holds"); + assert_eq!(obligation.source().path, "verification-model-test.intent"); + assert_eq!(obligation.declaration(), DeclarationStatus::Declared); + assert_eq!(obligation.linkage(), LinkageStatus::Unlinked); + assert_eq!(obligation.binding(), BindingStatus::Unbound); + assert_eq!(obligation.executability(), ExecutabilityStatus::Unsupported); + assert_eq!(obligation.disposition(), Disposition::NoResult); + assert_eq!(obligation.freshness(), Freshness::Current); + assert!(obligation.evidence_bindings().is_empty()); + assert!(!obligation.is_verified()); + } + + #[test] + fn duplicate_obligations_fail_closed_in_truth_predicates() { + let mut truth = strict_truth( + r#"Feature: Required claim + id: feature.required-claim + + Scenario: One claim + id: scenario.required-claim.one + When the behavior runs + → id: outcome.required-claim.one; the claim holds +"#, + ); + let feature_id = truth.features[0].id.clone(); + mark_verified(&mut truth.obligations[0], "binding.original"); + + let mut conflicting = truth.obligations[0].clone(); + conflicting.binding = BindingStatus::Unbound; + conflicting.executability = ExecutabilityStatus::Unsupported; + conflicting.disposition = Disposition::Failed; + conflicting.evidence_bindings.clear(); + truth.obligations.push(conflicting); + + assert!(!truth.feature_is_verified(feature_id.as_str())); + assert_eq!( + truth.verified_coverage(), + VerifiedCoverage { + covered: 0, + total: 1, + } + ); + } + + #[test] + fn linkage_and_execution_coverage_remain_distinct() { + let mut truth = strict_truth( + r#"Feature: Required claim + id: feature.required-claim + + Scenario: One claim + id: scenario.required-claim.one + When the behavior runs + → id: outcome.required-claim.one; the claim holds +"#, + ); + truth + .mark_implementation_linked("outcome.required-claim.one") + .unwrap(); + + assert_eq!( + truth.implementation_coverage(), + ImplementationCoverage { + covered: 1, + total: 1, + } + ); + assert_eq!( + truth.executable_coverage(), + ExecutableCoverage { + covered: 0, + total: 1, + } + ); + assert_eq!( + truth.verified_coverage(), + VerifiedCoverage { + covered: 0, + total: 1, + } + ); + } + + #[test] + fn zero_atoms_and_unknown_or_unresolved_assertions_fail_closed() { + let obligation_id = StableId::explicit("outcome.example", IdKind::Outcome).unwrap(); + for resolution in [ + AssertionResolution::Unknown, + AssertionResolution::Unresolved, + ] { + let mut binding = passing_binding(obligation_id.clone(), "binding.resolution"); + binding.assertion_resolution = resolution; + assert!(!binding.satisfies_obligation(&obligation_id)); } + + let mut binding = passing_binding(obligation_id.clone(), "binding.zero-atoms"); + binding.evidence_atoms = 0; + assert!(!binding.satisfies_obligation(&obligation_id)); + } + + #[test] + fn truth_dimensions_remain_orthogonal_and_readable() { + let obligation_id = StableId::explicit("outcome.example", IdKind::Outcome).unwrap(); + let binding = EvidenceBinding { + id: "binding.blocked".to_string(), + obligation_id: obligation_id.clone(), + source: SourceSpan::single_line("verification.tnt", 7, 1, 12), + declaration: DeclarationStatus::Declared, + linkage: LinkageStatus::Linked, + binding: BindingStatus::Bound, + executability: ExecutabilityStatus::Blocked, + disposition: Disposition::Planned, + freshness: Freshness::Stale, + assertion_resolution: AssertionResolution::Resolved, + evidence_atoms: 0, + }; + + assert_eq!(binding.id(), "binding.blocked"); + assert_eq!(binding.obligation_id(), &obligation_id); + assert_eq!(binding.source().start_line, 7); + assert_eq!(binding.declaration(), DeclarationStatus::Declared); + assert_eq!(binding.linkage(), LinkageStatus::Linked); + assert_eq!(binding.binding(), BindingStatus::Bound); + assert_eq!(binding.executability(), ExecutabilityStatus::Blocked); + assert_eq!(binding.disposition(), Disposition::Planned); + assert_eq!(binding.freshness(), Freshness::Stale); + assert_eq!( + binding.assertion_resolution(), + AssertionResolution::Resolved + ); + assert_eq!(binding.evidence_atoms(), 0); + assert!(!binding.satisfies_obligation(&obligation_id)); + } + + #[test] + fn unlinked_behavioral_evidence_verifies_only_its_exact_outcome_id_and_kind() { + let mut truth = strict_truth( + r#"Feature: Required claim + id: feature.required-claim + + Scenario: One claim + id: scenario.required-claim.one + When the behavior runs + → id: outcome.required-claim.one; the claim holds +"#, + ); + let obligation = &mut truth.obligations[0]; + let binding = passing_binding(obligation.id.clone(), "binding.behavioral"); + + assert_eq!(binding.linkage(), LinkageStatus::Unlinked); + assert!(binding.satisfies_obligation(&obligation.id)); + let unrelated = StableId::explicit("outcome.unrelated", IdKind::Outcome).unwrap(); + assert!(!binding.satisfies_obligation(&unrelated)); + let wrong_kind = StableId::explicit("scenario.wrong-kind", IdKind::Scenario).unwrap(); + assert!(!binding.satisfies_obligation(&wrong_kind)); + let mut wrong_kind_binding = binding.clone(); + wrong_kind_binding.obligation_id = wrong_kind; + assert!(!wrong_kind_binding.satisfies_obligation(&obligation.id)); + + obligation.linkage = LinkageStatus::Unlinked; + obligation.binding = BindingStatus::Bound; + obligation.executability = ExecutabilityStatus::Executable; + obligation.disposition = Disposition::Passed; + obligation.freshness = Freshness::Current; + obligation.evidence_bindings.push(binding); + + assert!(obligation.is_verified()); + obligation.evidence_bindings[0].obligation_id = unrelated; + assert!( + !obligation.is_verified(), + "evidence for another obligation must fail closed" + ); + } + + #[test] + fn feature_verification_rejects_wrong_feature_ownership_and_id_kind() { + let mut truth = strict_truth( + r#"Feature: Required claim + id: feature.required-claim + + Scenario: One claim + id: scenario.required-claim.one + When the behavior runs + → id: outcome.required-claim.one; the claim holds +"#, + ); + let feature_id = truth.features[0].id.clone(); + mark_verified(&mut truth.obligations[0], "binding.required"); + + truth.obligations[0].feature_id = + StableId::explicit("feature.unrelated", IdKind::Feature).unwrap(); + assert!(!truth.feature_is_verified(feature_id.as_str())); + + truth.obligations[0].feature_id = + StableId::explicit("scenario.wrong-feature-kind", IdKind::Scenario).unwrap(); + assert!(!truth.obligations[0].is_verified()); + assert!(!truth.feature_is_verified(feature_id.as_str())); + } + + #[test] + fn feature_verification_rejects_cross_feature_and_wrong_kind_scenario_ownership() { + let mut truth = strict_truth( + r#"Feature: First feature + id: feature.first + + Scenario: First scenario + id: scenario.first + When the first action runs + → id: outcome.first; the first result holds + +Feature: Second feature + id: feature.second + + Scenario: Second scenario + id: scenario.second + When the second action runs + → id: outcome.second; the second result holds +"#, + ); + let feature_id = truth.features[0].id.clone(); + let other_scenario_id = truth.obligations[1].scenario_id.clone(); + mark_verified(&mut truth.obligations[0], "binding.first"); + assert!(truth.feature_is_verified(feature_id.as_str())); + + truth.obligations[0].scenario_id = other_scenario_id; + assert!( + !truth.feature_is_verified(feature_id.as_str()), + "a valid scenario owned by another feature must fail closed" + ); + + truth.obligations[0].scenario_id = + StableId::explicit("feature.wrong-scenario-kind", IdKind::Feature).unwrap(); + assert!(!truth.obligations[0].is_verified()); + assert!( + !truth.feature_is_verified(feature_id.as_str()), + "an ownership edge with the wrong scenario ID kind must fail closed" + ); + } + + #[test] + fn unrepresented_legacy_tests_prevent_verification() { + let mut truth = strict_truth( + r#"Feature: Mixed authoring + id: feature.mixed-authoring + + Scenario: Native obligation + id: scenario.mixed-authoring.native + When the native path runs + → id: outcome.mixed-authoring.native; the native claim holds + + test: + - request: GET /health + assert: + - status: 200 +"#, + ); + let feature_id = truth.features[0].id.clone(); + mark_verified(&mut truth.obligations[0], "binding.native"); + + assert_eq!(truth.features[0].unrepresented_legacy_test_count(), 1); + assert!( + !truth.feature_is_verified(feature_id.as_str()), + "legacy tests without obligation representation must fail closed" + ); + } + + #[test] + fn same_scenario_outcome_id_and_evidence_swap_fails_closed() { + let mut truth = strict_truth( + r#"Feature: Identity integrity + id: feature.identity-integrity + + Scenario: Two distinct claims + id: scenario.identity-integrity.two-claims + When identity is checked + → id: outcome.identity-integrity.first; the first claim holds + → id: outcome.identity-integrity.second; the second claim holds +"#, + ); + let feature_id = truth.features[0].id.clone(); + for (index, obligation) in truth.obligations.iter_mut().enumerate() { + mark_verified(obligation, &format!("binding.{index}")); + } + assert!(truth.feature_is_verified(feature_id.as_str())); + + let (first, second) = truth.obligations.split_at_mut(1); + std::mem::swap(&mut first[0].id, &mut second[0].id); + std::mem::swap( + &mut first[0].evidence_bindings[0].obligation_id, + &mut second[0].evidence_bindings[0].obligation_id, + ); + + assert!( + !truth.feature_is_verified(feature_id.as_str()), + "an outcome ID and its evidence cannot move to another statement" + ); + assert_eq!(truth.verified_coverage().covered, 0); + } + + #[test] + fn removing_an_obligation_cannot_shrink_the_parser_owned_denominator() { + let mut truth = strict_truth( + r#"Feature: Required claim + id: feature.required-claim + + Scenario: One claim + id: scenario.required-claim.one + When the behavior runs + → id: outcome.required-claim.one; the claim holds +"#, + ); + truth.obligations.clear(); + + assert_eq!( + truth.verified_coverage(), + VerifiedCoverage { + covered: 0, + total: 1, + } + ); + assert!(!truth.feature_is_verified("feature.required-claim")); + } + + #[test] + fn declaration_tampering_invalidates_all_coverage() { + let mut truth = strict_truth( + r#"Feature: Required claim + id: feature.required-claim + + Scenario: One claim + id: scenario.required-claim.one + When the behavior runs + → id: outcome.required-claim.one; the claim holds +"#, + ); + truth + .mark_implementation_linked("outcome.required-claim.one") + .unwrap(); + mark_verified(&mut truth.obligations[0], "binding.required"); + truth.features[0].declaration = DeclarationStatus::DocumentationOnly; + + assert_eq!(truth.behavioral_feature_count(), 1); + assert_eq!(truth.implementation_coverage().covered, 0); + assert_eq!(truth.executable_coverage().covered, 0); + assert_eq!(truth.verified_coverage().covered, 0); + + truth.features[0].declaration = DeclarationStatus::Declared; + truth.obligations[0].declaration = DeclarationStatus::DocumentationOnly; + assert_eq!(truth.implementation_coverage().covered, 0); + assert_eq!(truth.executable_coverage().covered, 0); + assert_eq!(truth.verified_coverage().covered, 0); + } + + #[test] + fn zeroing_the_legacy_denominator_cannot_make_a_feature_verified() { + let mut truth = strict_truth( + r#"Feature: Mixed authoring + id: feature.mixed-authoring + + Scenario: Native obligation + id: scenario.mixed-authoring.native + When the native path runs + → id: outcome.mixed-authoring.native; the native claim holds + + test: + - request: GET /health + assert: + - status: 200 +"#, + ); + let feature_id = truth.features[0].id.clone(); + mark_verified(&mut truth.obligations[0], "binding.native"); + assert!(!truth.feature_is_verified(feature_id.as_str())); + + truth.features[0].unrepresented_legacy_tests = 0; + assert!( + !truth.feature_is_verified(feature_id.as_str()), + "caller-editable state cannot erase the parser-owned legacy denominator" + ); + } + + #[test] + fn removing_a_feature_cannot_change_the_behavioral_feature_count() { + let mut truth = strict_truth( + r#"Feature: Required claim + id: feature.required-claim + + Scenario: One claim + id: scenario.required-claim.one + When the behavior runs + → id: outcome.required-claim.one; the claim holds +"#, + ); + truth + .mark_implementation_linked("outcome.required-claim.one") + .unwrap(); + mark_verified(&mut truth.obligations[0], "binding.required"); + truth.features.clear(); + + assert_eq!(truth.behavioral_feature_count(), 1); + assert!(!truth.feature_is_verified("feature.required-claim")); + assert_eq!(truth.implementation_coverage().covered, 0); + assert_eq!(truth.executable_coverage().covered, 0); + assert_eq!(truth.verified_coverage().covered, 0); + assert_eq!(truth.verified_coverage().total, 1); } } diff --git a/tests/verification_truth_tests.rs b/tests/verification_truth_tests.rs index 5e49ead..4d96af3 100644 --- a/tests/verification_truth_tests.rs +++ b/tests/verification_truth_tests.rs @@ -1,10 +1,7 @@ use std::path::{Path, PathBuf}; use ntnt::intent::{FeatureVerification, IntentFile}; -use ntnt::verification::{ - AssertionResolution, BindingStatus, DeclarationStatus, Disposition, EvidenceBinding, - ExecutabilityStatus, Freshness, IdMode, IdOrigin, LinkageStatus, SourceSpan, VerificationTruth, -}; +use ntnt::verification::{DeclarationStatus, IdMode, IdOrigin, VerificationTruth}; fn fixture(name: &str) -> PathBuf { Path::new(env!("CARGO_MANIFEST_DIR")) @@ -81,6 +78,78 @@ fn malformed_ids_report_the_entity_and_source_location() { } } +#[test] +fn repeated_explicit_ids_on_one_declaration_fail_closed() { + let repeated_feature = r#"Feature: Repeated feature ID + id: feature.first + id: feature.second +"#; + let feature_error = IntentFile::parse_content_with_id_mode( + repeated_feature, + "repeated-feature-id.intent".to_string(), + IdMode::Strict, + ) + .expect_err("a feature cannot replace its stable identity") + .to_string(); + assert!( + feature_error.contains("repeated feature ID"), + "{feature_error}" + ); + assert!( + feature_error.contains("first declared at"), + "{feature_error}" + ); + + let repeated_scenario = r#"Feature: Repeated scenario ID + id: feature.repeated-scenario + + Scenario: Repeated ID + id: scenario.first + id: scenario.second + When one action runs + → id: outcome.repeated-scenario.claim; one claim holds +"#; + let scenario_error = IntentFile::parse_content_with_id_mode( + repeated_scenario, + "repeated-scenario-id.intent".to_string(), + IdMode::Strict, + ) + .expect_err("a scenario cannot replace its stable identity") + .to_string(); + assert!( + scenario_error.contains("repeated scenario ID"), + "{scenario_error}" + ); + assert!( + scenario_error.contains("first declared at"), + "{scenario_error}" + ); + + let repeated_component_scenario = r#"Component: Repeated scenario ID + + Scenario: Repeated ID + id: scenario.component-first + id: scenario.component-second + When one action runs + → id: outcome.component.claim; one claim holds +"#; + let component_error = IntentFile::parse_content_with_id_mode( + repeated_component_scenario, + "repeated-component-scenario-id.intent".to_string(), + IdMode::Strict, + ) + .expect_err("a component scenario cannot replace its stable identity") + .to_string(); + assert!( + component_error.contains("repeated scenario ID"), + "{component_error}" + ); + assert!( + component_error.contains("first declared at"), + "{component_error}" + ); +} + #[test] fn strict_mode_rejects_missing_stable_ids() { let error = strict_error("compatibility_derived_ids.intent"); @@ -91,6 +160,46 @@ fn strict_mode_rejects_missing_stable_ids() { ); } +#[test] +fn legacy_public_ast_struct_literals_remain_constructible() { + let scenario = ntnt::intent::Scenario { + name: "Legacy scenario".to_string(), + description: None, + given_clause: None, + when_clause: "legacy action runs".to_string(), + outcomes: vec!["legacy result".to_string()], + resolved_test: None, + component_refs: Vec::new(), + }; + let feature = ntnt::intent::Feature { + id: Some("legacy.feature".to_string()), + name: "Legacy feature".to_string(), + description: None, + tests: Vec::new(), + scenarios: vec![scenario], + }; + let intent = ntnt::intent::IntentFile { + features: vec![feature], + source_path: "legacy.intent".to_string(), + title: None, + glossary: None, + components: Vec::new(), + invariants: Vec::new(), + test_data: Vec::new(), + }; + + assert_eq!(intent.features[0].scenarios.len(), 1); + + let parsed: IntentFile = IntentFile::parse_content( + "Feature: Legacy compatibility parse", + "legacy-parse.intent".to_string(), + ) + .expect("legacy parse_content remains compatibility-mode IntentFile parsing"); + assert_eq!(parsed.features.len(), 1); + + let _: fn(&Path) -> Result = IntentFile::parse; +} + #[test] fn compatibility_mode_derives_ids_and_emits_source_located_warnings() { let intent = IntentFile::parse_with_id_mode( @@ -99,34 +208,712 @@ fn compatibility_mode_derives_ids_and_emits_source_located_warnings() { ) .unwrap(); - assert_eq!(intent.verification_warnings.len(), 3); + assert_eq!(intent.verification_warnings().len(), 3); assert!(intent - .verification_warnings + .verification_warnings() .iter() .all(|warning| warning.id.origin() == IdOrigin::CompatibilityDerived)); - assert!(intent.verification_warnings.iter().any(|warning| { + assert!(intent.verification_warnings().iter().any(|warning| { warning.message.contains("derived feature ID") && warning.span.start_line == 1 })); - assert!(intent.verification_warnings.iter().any(|warning| { + assert!(intent.verification_warnings().iter().any(|warning| { warning.message.contains("derived scenario ID") && warning.span.start_line == 3 })); - assert!(intent.verification_warnings.iter().any(|warning| { + assert!(intent.verification_warnings().iter().any(|warning| { warning.message.contains("derived outcome ID") && warning.span.start_line == 5 })); } +#[test] +fn compatibility_outcome_ids_are_scoped_by_scenario_identity() { + let content = r#"Feature: Repeated feature name + + Scenario: Shared behavior + When the same action runs + → the same outcome occurs + +Feature: Repeated feature name + + Scenario: Shared behavior + When the same action runs + → the same outcome occurs +"#; + + let intent = IntentFile::parse_content_with_id_mode( + content, + "scoped-derived-outcomes.intent".to_string(), + IdMode::Compatibility, + ) + .expect("separate feature scenarios must not derive colliding outcome IDs"); + + let first = intent.outcome_stable_id(0, 0, 0).unwrap(); + let second = intent.outcome_stable_id(1, 0, 0).unwrap(); + assert_ne!(first, second); + assert_eq!(first.origin(), IdOrigin::CompatibilityDerived); + assert_eq!(second.origin(), IdOrigin::CompatibilityDerived); +} + +#[test] +fn compatibility_child_ids_preserve_exact_parent_identity() { + let content = r#"Feature: First spelling + id: feature.foo_bar + + Scenario: Shared behavior + When the same action runs + → the same outcome occurs + +Feature: Second spelling + id: feature.foo-bar + + Scenario: Shared behavior + When the same action runs + → the same outcome occurs +"#; + + let intent = IntentFile::parse_content_with_id_mode( + content, + "exact-parent-identity.intent".to_string(), + IdMode::Compatibility, + ) + .expect("lossless parent identity must keep child IDs distinct"); + + assert_ne!( + intent.scenario_stable_id(0, 0), + intent.scenario_stable_id(1, 0) + ); +} + +#[test] +fn compatibility_component_scenarios_are_scoped_by_declaration() { + let content = r#"Component: Shared declaration + + Scenario: Shared behavior + When the same action runs + → the same outcome occurs + +Component: Shared declaration + + Scenario: Shared behavior + When the same action runs + → the same outcome occurs +"#; + + let intent = IntentFile::parse_content_with_id_mode( + content, + "component-id-scopes.intent".to_string(), + IdMode::Compatibility, + ) + .expect("separate components must not derive colliding scenario identities"); + + assert_ne!( + intent.component_scenario_stable_id(0, 0), + intent.component_scenario_stable_id(1, 0) + ); + assert_ne!( + intent.component_outcome_stable_id(0, 0, 0), + intent.component_outcome_stable_id(1, 0, 0) + ); +} + +#[test] +fn truth_construction_preserves_outcome_metadata_cardinality() { + let content = r#"Feature: Cardinality + id: feature.cardinality + + Scenario: One claim + id: scenario.cardinality.one-claim + When one action runs + → id: outcome.cardinality.claim; one claim holds +"#; + let intent = IntentFile::parse_content_with_id_mode( + content, + "cardinality.intent".to_string(), + IdMode::Strict, + ) + .unwrap(); + let truth = VerificationTruth::from_intent(&intent).unwrap(); + assert_eq!(intent.features[0].scenarios[0].outcomes.len(), 1); + assert_eq!(truth.obligations().len(), 1); + assert_eq!(truth.obligations()[0].statement(), "one claim holds"); +} + +#[test] +fn constraint_scope_ends_at_section_separator() { + let content = r#"Feature: Sectioned behavior + id: feature.sectioned + +Constraint: Legacy example + Scenario: Constraint scenario + When legacy behavior runs + → legacy result + +--- + + Scenario: Behavioral scenario + id: scenario.sectioned.behavioral + When behavioral work runs + → id: outcome.sectioned.behavioral; behavioral result +"#; + + let intent = IntentFile::parse_content_with_id_mode( + content, + "constraint-separator.intent".to_string(), + IdMode::Strict, + ) + .expect("a section separator ends legacy Constraint containment"); + let truth = VerificationTruth::from_intent(&intent).unwrap(); + assert_eq!(truth.obligations().len(), 1); + assert_eq!( + truth.obligations()[0].id().as_str(), + "outcome.sectioned.behavioral" + ); +} + +#[test] +fn markdown_heading_ends_constraint_scope_for_feature_behavior() { + let content = r#"Feature: Heading behavior + id: feature.heading + +Constraint: Legacy example + Scenario: Constraint scenario + When legacy behavior runs + → legacy result + +## Behavioral Scenarios + + Scenario: Behavioral scenario + id: scenario.heading.behavioral + When behavioral work runs + → id: outcome.heading.behavioral; behavioral result +"#; + + let intent = IntentFile::parse_content_with_id_mode( + content, + "constraint-heading.intent".to_string(), + IdMode::Strict, + ) + .expect("a Markdown heading ends legacy Constraint containment"); + let truth = VerificationTruth::from_intent(&intent).unwrap(); + assert_eq!(truth.obligations().len(), 1); + assert_eq!( + truth.obligations()[0].id().as_str(), + "outcome.heading.behavioral" + ); +} + +#[test] +fn markdown_heading_ends_constraint_scope_for_component_behavior() { + let content = r#"Component: Reusable behavior + id: component.reusable + +Constraint: Legacy example + Scenario: Constraint scenario + When legacy behavior runs + → legacy result + +## Behavioral Scenarios + + Scenario: Behavioral scenario + id: scenario.reusable.behavioral + When reusable work runs + → id: outcome.reusable.behavioral; reusable result +"#; + + let intent = IntentFile::parse_content_with_id_mode( + content, + "component-constraint-heading.intent".to_string(), + IdMode::Strict, + ) + .expect("a Markdown heading ends component Constraint containment"); + assert_eq!(intent.components[0].scenarios.len(), 2); + assert_eq!( + intent.component_scenario_stable_id(0, 1).unwrap().as_str(), + "scenario.reusable.behavioral" + ); + assert_eq!( + intent + .component_outcome_stable_id(0, 1, 0) + .unwrap() + .as_str(), + "outcome.reusable.behavioral" + ); +} + +#[test] +fn strict_component_scenario_after_separator_requires_a_redeclared_owner() { + let content = r#"Component: Reusable behavior + id: component.reusable + +Constraint: Legacy example + Scenario: Constraint scenario + When legacy behavior runs + → legacy result + +--- + +Scenario: Orphaned scenario + id: scenario.orphaned + When orphaned work runs + → id: outcome.orphaned; orphaned result +"#; + + let error = IntentFile::parse_content_with_id_mode( + content, + "component-separator-owner.intent".to_string(), + IdMode::Strict, + ) + .expect_err("strict scenarios after a component section must redeclare their owner") + .to_string(); + assert!( + error.contains("component-separator-owner.intent:11"), + "{error}" + ); + assert!( + error.contains("scenario requires an active Feature or Component owner"), + "{error}" + ); +} + +#[test] +fn test_data_declaration_ends_constraint_scope_for_feature_behavior() { + let content = r#"Feature: Test data boundary + id: feature.test-data-boundary + +Constraint: Legacy example + Scenario: Constraint scenario + When legacy behavior runs + → legacy result + +Test Data: Boundary cases + id: test-data.boundary + +Scenario: Behavioral scenario + id: scenario.test-data-boundary.behavioral + When behavioral work runs + → id: outcome.test-data-boundary.behavioral; behavioral result +"#; + + let intent = IntentFile::parse_content_with_id_mode( + content, + "constraint-test-data.intent".to_string(), + IdMode::Strict, + ) + .expect("Test Data ends feature Constraint containment"); + let truth = VerificationTruth::from_intent(&intent).unwrap(); + assert_eq!(intent.test_data[0].id, "test-data.boundary"); + assert_eq!(truth.obligations().len(), 1); + assert_eq!( + truth.obligations()[0].id().as_str(), + "outcome.test-data-boundary.behavioral" + ); +} + +#[test] +fn test_cases_declaration_ends_constraint_scope_for_component_behavior() { + let content = r#"Component: Test case boundary + id: component.test-case-boundary + +Constraint: Legacy example + Scenario: Constraint scenario + When legacy behavior runs + → legacy result + +Test Cases: Boundary cases + id: test-cases.boundary + +Scenario: Behavioral scenario + id: scenario.test-case-boundary.behavioral + When behavioral work runs + → id: outcome.test-case-boundary.behavioral; behavioral result +"#; + + let intent = IntentFile::parse_content_with_id_mode( + content, + "component-constraint-test-cases.intent".to_string(), + IdMode::Strict, + ) + .expect("Test Cases ends component Constraint containment"); + assert_eq!(intent.test_data[0].id, "test-cases.boundary"); + assert_eq!(intent.components[0].scenarios.len(), 2); + assert_eq!( + intent.component_scenario_stable_id(0, 1).unwrap().as_str(), + "scenario.test-case-boundary.behavioral" + ); + assert_eq!( + intent + .component_outcome_stable_id(0, 1, 0) + .unwrap() + .as_str(), + "outcome.test-case-boundary.behavioral" + ); +} + +#[test] +fn legacy_test_declaration_ends_constraint_scope_without_hiding_later_behavior() { + let content = r#"Feature: Legacy test boundary + id: feature.legacy-test-boundary + +Constraint: Legacy example + Scenario: Constraint scenario + When legacy behavior runs + → legacy result + +test: + - request: GET /health + assert: + - status: 200 + +Scenario: Behavioral scenario + id: scenario.legacy-test-boundary.behavioral + When behavioral work runs + → id: outcome.legacy-test-boundary.behavioral; behavioral result +"#; + + let intent = IntentFile::parse_content_with_id_mode( + content, + "constraint-legacy-test.intent".to_string(), + IdMode::Strict, + ) + .expect("legacy test declaration ends Constraint containment"); + let truth = VerificationTruth::from_intent(&intent).unwrap(); + assert_eq!(intent.features[0].tests.len(), 1); + assert_eq!(truth.features()[0].unrepresented_legacy_test_count(), 1); + assert_eq!(truth.obligations().len(), 1); +} + +#[test] +fn technical_bindings_heading_unwinds_before_feature_behavior() { + let content = r#"Feature: Binding boundary + id: feature.binding-boundary + +Constraint: Legacy example + Scenario: Constraint scenario + When legacy behavior runs + → legacy result + +## Glossary [Technical Bindings] +health check: + action: GET /health + +## Behavioral Scenarios + +Scenario: Behavioral scenario + id: scenario.binding-boundary.behavioral + When behavioral work runs + → id: outcome.binding-boundary.behavioral; behavioral result +"#; + + let intent = IntentFile::parse_content_with_id_mode( + content, + "constraint-technical-bindings.intent".to_string(), + IdMode::Strict, + ) + .expect("a later heading must unwind Technical Bindings state"); + let truth = VerificationTruth::from_intent(&intent).unwrap(); + assert_eq!(truth.obligations().len(), 1); + assert_eq!( + truth.obligations()[0].id().as_str(), + "outcome.binding-boundary.behavioral" + ); +} + +#[test] +fn technical_bindings_heading_unwinds_before_component_behavior() { + let content = r#"Component: Binding boundary + id: component.binding-boundary + +Constraint: Legacy example + Scenario: Constraint scenario + When legacy behavior runs + → legacy result + +## Glossary [Technical Bindings] +health check: + action: GET /health + +## Behavioral Scenarios + +Scenario: Behavioral scenario + id: scenario.component-binding-boundary.behavioral + When behavioral work runs + → id: outcome.component-binding-boundary.behavioral; behavioral result +"#; + + let intent = IntentFile::parse_content_with_id_mode( + content, + "component-constraint-technical-bindings.intent".to_string(), + IdMode::Strict, + ) + .expect("a later heading must unwind component Technical Bindings state"); + assert_eq!(intent.components[0].scenarios.len(), 2); + assert_eq!( + intent.component_scenario_stable_id(0, 1).unwrap().as_str(), + "scenario.component-binding-boundary.behavioral" + ); + assert_eq!( + intent + .component_outcome_stable_id(0, 1, 0) + .unwrap() + .as_str(), + "outcome.component-binding-boundary.behavioral" + ); +} + +#[test] +fn blank_title_does_not_consume_a_following_feature_declaration() { + let content = r#"## Title +Feature: Titled behavior + id: feature.titled + +Scenario: Titled scenario + id: scenario.titled + When titled work runs + → id: outcome.titled; titled result +"#; + + let intent = IntentFile::parse_content_with_id_mode( + content, + "blank-title-boundary.intent".to_string(), + IdMode::Strict, + ) + .expect("a blank Title section must not consume a named declaration"); + let truth = VerificationTruth::from_intent(&intent).unwrap(); + assert_eq!(intent.features.len(), 1); + assert_eq!(truth.obligations().len(), 1); +} + +#[test] +fn separator_finalizes_invariant_and_rejects_an_orphan_outcome() { + let content = r#"Invariant: Stable invariant + id: invariant.stable + Assertions: + → invariant result + +--- + +→ orphaned result +"#; + + let error = IntentFile::parse_content_with_id_mode( + content, + "invariant-separator-boundary.intent".to_string(), + IdMode::Strict, + ) + .expect_err("an outcome after an invariant-closing separator must be rejected") + .to_string(); + assert!( + error.contains("invariant-separator-boundary.intent:8"), + "{error}" + ); + assert!( + error.contains("outcome requires an active Scenario or Invariant owner"), + "{error}" + ); +} + +#[test] +fn constraint_declaration_cannot_mutate_invariant_or_test_data_state() { + let content = r#"Invariant: Stable invariant + id: invariant.stable + Assertions: + → invariant result + +Constraint: Legacy invariant boundary + id: invariant.corrupted + → constraint prose + +Test Data: Stable data + id: test-data.stable + +Constraint: Legacy test-data boundary + id: test-data.corrupted + +Feature: Behavioral owner + id: feature.boundary-owner + +Scenario: Behavioral scenario + id: scenario.boundary-owner + When behavior runs + → id: outcome.boundary-owner; behavioral result +"#; + + let intent = IntentFile::parse_content_with_id_mode( + content, + "constraint-parent-boundaries.intent".to_string(), + IdMode::Compatibility, + ) + .expect("Constraint declarations must close prior parser sections"); + assert_eq!(intent.invariants[0].id, "invariant.stable"); + assert_eq!(intent.invariants[0].assertions, ["invariant result"]); + assert_eq!(intent.test_data[0].id, "test-data.stable"); + assert_eq!( + VerificationTruth::from_intent(&intent) + .unwrap() + .obligations() + .len(), + 1 + ); +} + +#[test] +fn test_data_named_declaration_exits_preserve_sections_and_parent_ids() { + let content = r#"Test Data: Feature data + id: test-data.feature + +Feature: Feature owner + id: feature.after-test-data + +Scenario: Feature scenario + id: scenario.after-test-data + When feature work runs + → id: outcome.after-test-data; feature result + +Test Cases: Component data + id: test-data.component + +Component: Component owner + id: component.after-test-data + +Scenario: Component scenario + id: scenario.component-after-test-data + When component work runs + → id: outcome.component-after-test-data; component result +"#; + + let intent = IntentFile::parse_content_with_id_mode( + content, + "test-data-declaration-exits.intent".to_string(), + IdMode::Strict, + ) + .expect("named declarations must finalize pending test-data sections"); + assert_eq!( + intent + .test_data + .iter() + .map(|data| data.id.as_str()) + .collect::>(), + ["test-data.feature", "test-data.component"] + ); + assert_eq!( + intent.features[0].id.as_deref(), + Some("feature.after-test-data") + ); + assert_eq!(intent.components[0].id, "component.after-test-data"); + assert_eq!( + VerificationTruth::from_intent(&intent) + .unwrap() + .obligations() + .len(), + 1 + ); +} + +#[test] +fn strict_legacy_tests_require_a_feature_owner() { + for (name, content) in [ + ( + "top-level", + r#"test: + - request: GET /health + assert: + - status: 200 +"#, + ), + ( + "component", + r#"Component: Reusable + id: component.reusable + +test: + - request: GET /health + assert: + - status: 200 +"#, + ), + ] { + let error = IntentFile::parse_content_with_id_mode( + content, + format!("{name}-orphan-test.intent"), + IdMode::Strict, + ) + .expect_err("strict legacy tests require a Feature owner") + .to_string(); + assert!( + error.contains("test requires an active Feature owner"), + "{error}" + ); + } +} + +#[test] +fn constraint_outcome_verification_syntax_remains_legacy_prose() { + let content = r#"Feature: Parent feature + id: feature.parent + +Constraint: Legacy containment + Scenario: Constraint example + id: scenario.BAD + When legacy behavior is described + → id: outcome.BAD; legacy constraint prose +"#; + + let intent = IntentFile::parse_content_with_id_mode( + content, + "constraint-outcome-prose.intent".to_string(), + IdMode::Compatibility, + ) + .unwrap(); + let scenario = &intent.features[0].scenarios[0]; + assert_eq!( + scenario.outcomes, + vec!["id: outcome.BAD; legacy constraint prose"] + ); + assert_eq!( + intent.outcome_stable_id(0, 0, 0).unwrap().origin(), + IdOrigin::CompatibilityDerived + ); +} + +#[test] +fn scenario_ids_must_precede_identity_bearing_outcomes() { + let content = r#"Feature: Parent feature + id: feature.parent + + Scenario: Late identity + When behavior runs + → an earlier result + id: scenario.parent.late-identity + → a later result +"#; + + let error = IntentFile::parse_content_with_id_mode( + content, + "late-scenario-id.intent".to_string(), + IdMode::Compatibility, + ) + .expect_err("a scenario ID cannot replace the parent of existing outcome IDs") + .to_string(); + assert!( + error.contains("scenario ID must appear before outcomes"), + "{error}" + ); +} + #[test] fn zero_outcome_behavioral_features_are_unproven() { let intent = IntentFile::parse_with_id_mode(&fixture("zero_outcome_behavioral.intent"), IdMode::Strict) .unwrap(); - let truth = VerificationTruth::from_intent(&intent); + let truth = VerificationTruth::from_intent(&intent).unwrap(); - assert_eq!(truth.features.len(), 1); - assert!(truth.features[0].is_unproven()); + assert_eq!(truth.features().len(), 1); + assert!(truth.features()[0].is_unproven()); assert!(!truth.feature_is_verified("feature.zero-outcomes")); - assert_eq!(truth.features[0].declaration, DeclarationStatus::Declared); - assert!(truth.obligations.is_empty()); + assert_eq!( + truth.features()[0].declaration(), + DeclarationStatus::Declared + ); + assert!(truth.obligations().is_empty()); assert_eq!(truth.verified_coverage().covered, 0); assert_eq!(truth.verified_coverage().total, 0); } @@ -136,18 +923,18 @@ fn justified_documentation_only_features_are_visible_but_not_behavioral() { let intent = IntentFile::parse_with_id_mode(&fixture("documentation_only.intent"), IdMode::Strict) .unwrap(); - let truth = VerificationTruth::from_intent(&intent); + let truth = VerificationTruth::from_intent(&intent).unwrap(); - assert_eq!(truth.features.len(), 1); + assert_eq!(truth.features().len(), 1); assert_eq!( - truth.features[0].declaration, + truth.features()[0].declaration(), DeclarationStatus::DocumentationOnly ); assert_eq!( - truth.features[0].rationale.as_deref(), + truth.features()[0].rationale(), Some("Defines shared vocabulary and makes no behavioral claim") ); - assert!(!truth.features[0].is_unproven()); + assert!(!truth.features()[0].is_unproven()); assert!(!truth.feature_is_verified("feature.domain-terminology")); assert_eq!(truth.behavioral_feature_count(), 0); } @@ -166,118 +953,197 @@ fn documentation_only_cannot_suppress_an_outcome() { } #[test] -fn linked_but_unexecuted_obligations_only_have_implementation_coverage() { - let intent = - IntentFile::parse_with_id_mode(&fixture("linked_unexecuted.intent"), IdMode::Strict) - .unwrap(); - let mut truth = VerificationTruth::from_intent(&intent); - truth - .mark_implementation_linked("outcome.linked.result") - .unwrap(); - - assert_eq!(truth.implementation_coverage().covered, 1); - assert_eq!(truth.implementation_coverage().total, 1); - assert_eq!(truth.executable_coverage().covered, 0); - assert_eq!(truth.executable_coverage().total, 1); - assert_eq!(truth.verified_coverage().covered, 0); - assert_eq!(truth.verified_coverage().total, 1); +fn compatibility_constraints_remain_visible_without_becoming_feature_truth() { + let path = Path::new(env!("CARGO_MANIFEST_DIR")).join("examples/crypto_chart/crypto.intent"); + let intent = IntentFile::parse_with_id_mode(&path, IdMode::Compatibility) + .expect("legacy Constraint declarations must still lint"); + + assert_eq!(intent.features.len(), 4); + assert_eq!( + intent + .features + .iter() + .map(|feature| feature.scenarios.len()) + .sum::(), + 4 + ); + + let error_handling = intent + .features + .iter() + .find(|feature| feature.id.as_deref() == Some("feature.error_handling")) + .expect("Error Handling feature"); + assert_eq!(error_handling.id.as_deref(), Some("feature.error_handling")); + assert_eq!(error_handling.scenarios.len(), 1); + + let truth = VerificationTruth::from_intent(&intent).unwrap(); + let feature_truth = truth + .features() + .iter() + .find(|feature| feature.id().as_str() == "feature.error_handling") + .expect("Error Handling truth"); + assert!(feature_truth.is_unproven()); + assert!(feature_truth.obligation_ids().is_empty()); + assert!(truth + .obligations() + .iter() + .all(|obligation| obligation.feature_id().as_str() != "feature.error_handling")); } #[test] -fn unknown_and_unresolved_assertions_fail_closed() { - let span = SourceSpan::single_line("verification.tnt", 12, 5, 20); - for resolution in [ - AssertionResolution::Unknown, - AssertionResolution::Unresolved, - ] { - let binding = EvidenceBinding { - id: "binding.example".to_string(), - obligation_id: "outcome.example".to_string(), - source: span.clone(), - declaration: DeclarationStatus::Declared, - linkage: LinkageStatus::Linked, - binding: BindingStatus::Bound, - executability: ExecutabilityStatus::Executable, - disposition: Disposition::Passed, - freshness: Freshness::Current, - assertion_resolution: resolution, - evidence_atoms: 1, - }; - - assert!(!binding.satisfies_obligation()); - } +fn constraint_metadata_cannot_mutate_preceding_parent_metadata() { + let feature_content = r#"Feature: Parent feature + id: feature.parent + description: original feature description + test: + - request: GET /original + +Constraint: Constraint metadata + description: constraint description + request: GET /constraint + + Scenario: Constraint scenario + When the constraint is illustrated + → the illustration is visible +"#; + let feature_intent = IntentFile::parse_content_with_id_mode( + feature_content, + "constraint-feature-metadata.intent".to_string(), + IdMode::Strict, + ) + .unwrap(); + assert_eq!( + feature_intent.features[0].description.as_deref(), + Some("original feature description") + ); + assert_eq!(feature_intent.features[0].tests.len(), 1); + assert_eq!(feature_intent.features[0].tests[0].path, "/original"); + + let component_content = r#"Component: Parent component + id: component.parent + description: original component description + parameters: [original] + Inherent Behavior: + → original inherent behavior + +Constraint: Constraint metadata + description: constraint description + parameters: [constraint] + Inherent Behavior: + → constraint inherent behavior + + Scenario: Constraint scenario + When the constraint is illustrated + → the illustration is visible +"#; + let component_intent = IntentFile::parse_content_with_id_mode( + component_content, + "constraint-component-metadata.intent".to_string(), + IdMode::Compatibility, + ) + .unwrap(); + let component = &component_intent.components[0]; + assert_eq!( + component.description.as_deref(), + Some("original component description") + ); + assert_eq!(component.parameters, ["original"]); + assert_eq!(component.inherent_behavior, ["original inherent behavior"]); } #[test] -fn truth_dimensions_remain_orthogonal() { - let binding = EvidenceBinding { - id: "binding.blocked".to_string(), - obligation_id: "outcome.example".to_string(), - source: SourceSpan::single_line("verification.tnt", 7, 1, 12), - declaration: DeclarationStatus::Declared, - linkage: LinkageStatus::Linked, - binding: BindingStatus::Bound, - executability: ExecutabilityStatus::Blocked, - disposition: Disposition::Planned, - freshness: Freshness::Stale, - assertion_resolution: AssertionResolution::Resolved, - evidence_atoms: 0, - }; +fn strict_identity_policy_ignores_legacy_constraint_scenarios() { + let content = r#"Feature: Behavioral feature + id: feature.behavioral - assert_eq!(binding.linkage, LinkageStatus::Linked); - assert_eq!(binding.binding, BindingStatus::Bound); - assert_eq!(binding.executability, ExecutabilityStatus::Blocked); - assert_eq!(binding.disposition, Disposition::Planned); - assert_eq!(binding.freshness, Freshness::Stale); - assert!(!binding.satisfies_obligation()); -} - -#[test] -fn behavioral_evidence_does_not_require_implementation_linkage() { - let binding = EvidenceBinding { - id: "binding.behavioral".to_string(), - obligation_id: "outcome.behavioral".to_string(), - source: SourceSpan::single_line("verification.tnt", 9, 1, 20), - declaration: DeclarationStatus::Declared, - linkage: LinkageStatus::Unlinked, - binding: BindingStatus::Bound, - executability: ExecutabilityStatus::Executable, - disposition: Disposition::Passed, - freshness: Freshness::Current, - assertion_resolution: AssertionResolution::Resolved, - evidence_atoms: 1, - }; +Constraint: Legacy declaration - assert!(binding.satisfies_obligation()); + Scenario: Constraint example + When the constraint is illustrated + → the illustration is visible +"#; - let intent = - IntentFile::parse_with_id_mode(&fixture("linked_unexecuted.intent"), IdMode::Strict) - .unwrap(); - let mut truth = VerificationTruth::from_intent(&intent); - let obligation = &mut truth.obligations[0]; - obligation.linkage = LinkageStatus::Unlinked; - obligation.binding = BindingStatus::Bound; - obligation.executability = ExecutabilityStatus::Executable; - obligation.disposition = Disposition::Passed; - obligation.freshness = Freshness::Current; - obligation.evidence_bindings.push(binding); + let intent = IntentFile::parse_content_with_id_mode( + content, + "strict-constraint.intent".to_string(), + IdMode::Strict, + ) + .expect("non-obligation Constraint scenarios must not require verification IDs"); - assert!(obligation.is_verified()); + let truth = VerificationTruth::from_intent(&intent).unwrap(); + assert!(truth.features()[0].is_unproven()); + assert!(truth.obligations().is_empty()); + assert!(intent.verification_warnings().is_empty()); } #[test] -fn compatibility_parser_does_not_reinterpret_constraint_metadata() { - let path = Path::new(env!("CARGO_MANIFEST_DIR")).join("examples/crypto_chart/crypto.intent"); - let intent = IntentFile::parse(&path).expect("legacy Constraint declarations must still lint"); +fn documentation_only_feature_is_not_made_behavioral_by_following_constraint() { + let content = r#"Feature: Shared terminology + id: feature.shared-terminology + verification: documentation-only + rationale: Defines vocabulary without a behavioral claim - assert_eq!(intent.features.len(), 4); +Constraint: Legacy declaration + + Scenario: Constraint example + When the constraint is illustrated + → the illustration is visible +"#; + + let intent = IntentFile::parse_content_with_id_mode( + content, + "documentation-constraint.intent".to_string(), + IdMode::Strict, + ) + .expect("Constraint scenarios must not invalidate documentation-only features"); + + let truth = VerificationTruth::from_intent(&intent).unwrap(); assert_eq!( - intent - .features - .iter() - .map(|feature| feature.scenarios.len()) - .sum::(), - 4 + truth.features()[0].declaration(), + DeclarationStatus::DocumentationOnly + ); + assert!(!truth.features()[0].is_unproven()); + assert!(truth.obligations().is_empty()); +} + +#[test] +fn compatibility_outcome_starting_with_id_remains_prose_unless_it_declares_an_outcome_id() { + let content = r#"Feature: Compatibility prose + id: feature.compatibility-prose + + Scenario: Describe an id field + id: scenario.compatibility-prose.id-field + When the record is returned + → id: field is returned; alternate key is omitted +"#; + + let intent = IntentFile::parse_content_with_id_mode( + content, + "compatibility-id-prose.intent".to_string(), + IdMode::Compatibility, + ) + .expect("legacy outcome prose beginning with 'id:' must remain valid"); + + let scenario = &intent.features[0].scenarios[0]; + assert_eq!( + scenario.outcomes, + ["id: field is returned; alternate key is omitted"] + ); + assert_eq!( + intent.outcome_stable_id(0, 0, 0).unwrap().origin(), + IdOrigin::CompatibilityDerived + ); + + let strict_error = IntentFile::parse_content_with_id_mode( + content, + "compatibility-id-prose.intent".to_string(), + IdMode::Strict, + ) + .expect_err("strict mode still requires an explicit outcome identity") + .to_string(); + assert!( + strict_error.contains("missing outcome ID"), + "{strict_error}" ); } @@ -322,7 +1188,7 @@ fn compatibility_outcome_warning_points_to_the_outcome_marker() { ) .unwrap(); let warning = intent - .verification_warnings + .verification_warnings() .iter() .find(|warning| warning.message.contains("derived outcome ID")) .expect("outcome warning"); @@ -359,7 +1225,7 @@ Feature: Following feature assert_eq!(intent.components[0].id, "component.reusable-check"); assert_eq!(intent.components[0].scenarios.len(), 1); assert_eq!( - intent.components[0].scenarios[0].verification_id.as_str(), + intent.component_scenario_stable_id(0, 0).unwrap().as_str(), "scenario.component.existing-behavior" ); assert_eq!(intent.components[0].scenarios[0].outcomes.len(), 1); @@ -388,7 +1254,7 @@ Constraint: Legacy boundary .expect("constraint metadata must not alter feature verification"); assert!(matches!( - intent.features[0].verification, - FeatureVerification::Behavioral + intent.feature_verification(0), + Some(&FeatureVerification::Behavioral) )); }