diff --git a/src/intent.rs b/src/intent.rs index 8d48234..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; @@ -45,6 +46,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,6 +2189,32 @@ 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)] +pub enum FeatureVerification { + Behavioral, + DocumentationOnly { rationale: String }, +} + +/// Stable identity and location paired with an existing outcome string. +#[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 { @@ -2685,6 +2713,267 @@ pub struct IntentFile { pub test_data: 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 #[derive(Debug, Clone, Serialize)] pub struct TestDataSection { @@ -2788,7 +3077,7 @@ 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 { let content = fs::read_to_string(path).map_err(|e| { IntentError::runtime_error(format!("Failed to read intent file: {}", e)) @@ -2797,6 +3086,18 @@ impl IntentFile { 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 { + let content = fs::read_to_string(path).map_err(|e| { + IntentError::runtime_error(format!("Failed to read intent file: {}", e)) + })?; + + Self::parse_content_with_id_mode(&content, path.to_string_lossy().to_string(), id_mode) + } + /// Look up test data by ID. /// /// Test data IDs are typically "test_data.name" format. @@ -2847,34 +3148,50 @@ 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 { - let mut features = Vec::new(); - let mut components = Vec::new(); + Self::parse_content_with_id_mode(content, source_path, IdMode::Compatibility) + .map(IdentifiedIntent::into_intent) + } + + /// 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 = 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; 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 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 @@ -2887,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 @@ -2907,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 @@ -2957,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(); @@ -3095,8 +3522,32 @@ 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); + } else if let Some(component) = current_component.as_mut() { + 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; + } + // 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() { @@ -3122,11 +3573,21 @@ impl IntentFile { } let name = trimmed.trim_start_matches("Feature:").trim().to_string(); - current_feature = Some(Feature { - id: None, - name, - description: None, - tests: Vec::new(), + let source = Self::line_span(&source_path, line_number, line, "Feature:"); + 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, + verification: FeatureVerification::Behavioral, scenarios: Vec::new(), }); current_test = None; @@ -3142,6 +3603,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() { @@ -3166,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; @@ -3187,8 +3652,20 @@ 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; // Save previous feature if let Some(mut feat) = current_feature.take() { if let Some(test) = current_test.take() { @@ -3371,22 +3848,25 @@ 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() && !in_constraint { let id = trimmed.trim_start_matches("id:").trim(); component.id = id.to_string(); 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 == ']'); @@ -3398,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; @@ -3415,20 +3896,72 @@ impl IntentFile { } let name = trimmed.trim_start_matches("Scenario:").trim().to_string(); - current_scenario = Some(Scenario { - name, - description: None, - given_clause: None, - when_clause: String::new(), - outcomes: Vec::new(), - resolved_test: None, - component_refs: Vec::new(), + let source = Self::line_span(&source_path, line_number, line, "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", + &component_ordinal, + &component.id, + &component.name, + &name, + ], + component.scenarios.len(), + ), + verification_id_source: source.clone(), + source, + origin: if in_constraint { + ScenarioOrigin::Constraint + } else { + ScenarioOrigin::Component + }, + outcome_metadata: Vec::new(), }); continue; } // 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)?; + scenario.verification_id_source = id_source; + continue; + } + // Description if trimmed.starts_with("description:") { let desc = trimmed.trim_start_matches("description:").trim(); @@ -3451,18 +3984,27 @@ 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.verification_id, + scenario.outcomes.len(), + scenario.origin != ScenarioOrigin::Constraint, + )?; scenario.outcomes.push(outcome); + scenario.outcome_metadata.push(metadata); continue; } } - // 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("→") @@ -3479,15 +4021,97 @@ 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:") { + if in_constraint { + continue; + } 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() { + 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 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; + feature.id = Some(id.to_string()); + } continue; } - // Description - only for feature if not inside a scenario - if trimmed.starts_with("description:") && current_scenario.is_none() { + 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:"), + "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() && !in_constraint + { + 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; + } + + // 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(); @@ -3507,14 +4131,32 @@ impl IntentFile { } let name = trimmed.trim_start_matches("Scenario:").trim().to_string(); - current_scenario = Some(Scenario { - name, - description: None, - given_clause: None, - when_clause: String::new(), - outcomes: Vec::new(), - resolved_test: None, - component_refs: Vec::new(), + let source = Self::line_span(&source_path, line_number, line, "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_child( + IdKind::Scenario, + &feature.verification_id, + &[&name], + feature.scenarios.len(), + ), + verification_id_source: source.clone(), + source, + origin: if in_constraint { + ScenarioOrigin::Constraint + } else { + ScenarioOrigin::Feature + }, + outcome_metadata: Vec::new(), }); in_assertions = false; continue; @@ -3544,18 +4186,27 @@ 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.verification_id, + scenario.outcomes.len(), + scenario.origin != ScenarioOrigin::Constraint, + )?; scenario.outcomes.push(outcome); + scenario.outcome_metadata.push(metadata); continue; } } // 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); @@ -3565,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); @@ -3595,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); @@ -3611,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(); @@ -3653,17 +4306,299 @@ impl IntentFile { test_data_sections.push(td); } - Ok(IntentFile { - features, + let mut verification_warnings = Vec::new(); + Self::finalize_verification_ids( + &features, + &components, + id_mode, + &mut 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) + .map_or(1, |byte_index| line[..byte_index].chars().count() + 1); + SourceSpan::single_line( source_path, - title, - glossary: if has_glossary { Some(glossary) } else { None }, - components, - invariants, - test_data: test_data_sections, + 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_id: &StableId, + ordinal: usize, + allow_verification_metadata: bool, + ) -> Result<(String, OutcomeMetadata), IntentError> { + 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('→') { + "→" + } else { + "->" + }; + let source = Self::line_span(source_path, line_number, line, source_marker); + + let (statement, id) = if let Some((id, statement)) = explicit_id { + 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_child( + IdKind::Outcome, + scenario_id, + &[raw_outcome], + ordinal, + ), + ) + }; + + if allow_verification_metadata && statement == "verification: documentation-only" { + return Err(Self::verification_error( + &source, + "documentation-only is valid only on a feature", + )); + } + + Ok(( + statement, + OutcomeMetadata { + id, + source: source.clone(), + }, + )) + } + + fn finalize_verification_ids( + features: &[ParsedFeature], + components: &[ParsedComponent], + 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 + .iter() + .any(|scenario| scenario.origin == ScenarioOrigin::Feature) + || !feature.tests.is_empty() + { + let span = feature + .scenarios + .iter() + .find(|scenario| scenario.origin == ScenarioOrigin::Feature) + .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 { + if scenario.origin != ScenarioOrigin::Feature { + continue; + } + 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 { + if scenario.origin != ScenarioOrigin::Component { + continue; + } + 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(); 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..8ac0657 --- /dev/null +++ b/src/verification/ids.rs @@ -0,0 +1,242 @@ +use std::fmt; + +/// Source range for a declaration or diagnostic. +#[derive(Debug, Clone, PartialEq, Eq, Hash)] +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)] +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)] +pub enum IdOrigin { + Explicit, + CompatibilityDerived, +} + +/// A validated verification identity. +#[derive(Debug, Clone, PartialEq, Eq, Hash)] +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, + } + } + + /// 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 + } + + 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)] +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..6e8a891 --- /dev/null +++ b/src/verification/mod.rs @@ -0,0 +1,22 @@ +//! Stable obligation identity and orthogonal verification truth types. +//! +//! 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; + +pub use ids::{IdKind, IdMode, IdOrigin, IdWarning, SourceSpan, StableId}; +pub use model::{ + AssertionResolution, BindingStatus, DeclarationStatus, Disposition, EvidenceBinding, + ExecutabilityStatus, ExecutableCoverage, 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..10cded0 --- /dev/null +++ b/src/verification/model.rs @@ -0,0 +1,1128 @@ +use std::collections::HashMap; + +use crate::intent::{FeatureVerification, IdentifiedIntent, ScenarioOrigin}; + +use super::ids::{IdKind, SourceSpan, StableId}; + +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub enum DeclarationStatus { + Declared, + DocumentationOnly, +} + +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub enum LinkageStatus { + Linked, + Unlinked, +} + +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub enum BindingStatus { + Bound, + Unbound, + Ambiguous, +} + +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub enum ExecutabilityStatus { + Executable, + Unsupported, + Blocked, +} + +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub enum Disposition { + Planned, + Running, + Passed, + Failed, + Flaky, + Skipped, + Cancelled, + NoResult, +} + +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub enum Freshness { + Current, + Stale, +} + +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub enum AssertionResolution { + Resolved, + Unknown, + Unresolved, +} + +/// One candidate source of execution evidence for an obligation. +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct EvidenceBinding { + 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, 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 + && 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)] +pub struct Obligation { + 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.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 + && self.freshness == Freshness::Current + && !self.evidence_bindings.is_empty() + && self + .evidence_bindings + .iter() + .all(|binding| binding.satisfies_obligation(&self.id)) + } +} + +/// Feature-level truth remains visible even when there are no outcome obligations. +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct FeatureTruth { + 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.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)] + pub struct $name { + pub covered: usize, + pub total: usize, + } + }; +} + +coverage_type!(ImplementationCoverage); +coverage_type!(ExecutableCoverage); +coverage_type!(VerifiedCoverage); + +/// 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 { + 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: &IdentifiedIntent) -> Result { + let mut features = Vec::new(); + let mut obligations = Vec::new(); + let metadata = intent.metadata(); + + 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, + Some(rationale.clone()), + ), + }; + 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, 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) + { + 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: outcome_metadata.id.clone(), + feature_id: feature_id.clone(), + scenario_id: scenario_id.clone(), + statement: statement.clone(), + source: outcome_metadata.source.clone(), + declaration, + linkage: LinkageStatus::Unlinked, + binding: BindingStatus::Unbound, + executability: ExecutabilityStatus::Unsupported, + disposition: Disposition::NoResult, + freshness: Freshness::Current, + evidence_bindings: Vec::new(), + }); + } + } + } + + features.push(FeatureTruth { + id: feature_id, + name: feature.name.clone(), + source: feature_metadata.source.clone(), + declaration, + rationale, + obligation_ids, + unrepresented_legacy_tests: feature.tests.len(), + }); + } + + 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.canonical_features + .iter() + .filter(|feature| feature.declaration == DeclarationStatus::Declared) + .count() + } + + /// 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() + .find(|feature| feature.id.as_str() == feature_id) + else { + return false; + }; + 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) + .is_some_and(|obligation| { + obligation.feature_id == feature.id && obligation.is_verified() + }) + }) + } + + 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) + .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, + } + } + + 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 + .iter() + .filter(|obligation| { + obligation.binding == BindingStatus::Bound + && obligation.executability == ExecutabilityStatus::Executable + }) + .count(), + 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, + } + } +} + +#[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/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..4d96af3 --- /dev/null +++ b/tests/verification_truth_tests.rs @@ -0,0 +1,1260 @@ +use std::path::{Path, PathBuf}; + +use ntnt::intent::{FeatureVerification, IntentFile}; +use ntnt::verification::{DeclarationStatus, IdMode, IdOrigin, 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 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"); + assert!(error.contains("missing feature ID"), "{error}"); + assert!( + error.contains("compatibility_derived_ids.intent:1"), + "{error}" + ); +} + +#[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( + &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 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).unwrap(); + + 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).unwrap(); + + assert_eq!(truth.features().len(), 1); + assert_eq!( + truth.features()[0].declaration(), + DeclarationStatus::DocumentationOnly + ); + assert_eq!( + truth.features()[0].rationale(), + 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 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 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 strict_identity_policy_ignores_legacy_constraint_scenarios() { + let content = r#"Feature: Behavioral feature + id: feature.behavioral + +Constraint: Legacy declaration + + Scenario: Constraint example + When the constraint is illustrated + → the illustration is visible +"#; + + 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"); + + 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 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 + +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!( + 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}" + ); +} + +#[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); +} + +#[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].id, "component.reusable-check"); + assert_eq!(intent.components[0].scenarios.len(), 1); + assert_eq!( + intent.component_scenario_stable_id(0, 0).unwrap().as_str(), + "scenario.component.existing-behavior" + ); + 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.feature_verification(0), + Some(&FeatureVerification::Behavioral) + )); +}