Skip to main content

tldr_cli/commands/contracts/
types.rs

1//! Shared types for Contracts & Flow commands
2//!
3//! This module defines all data types used across the contracts and flow analysis
4//! commands. Types are designed for JSON serialization with serde.
5//!
6//! # Schema Version
7//!
8//! All report types include implicit schema versioning through the module's
9//! SCHEMA_VERSION constant. Consumers should check schema compatibility.
10
11use std::collections::HashMap;
12use std::path::PathBuf;
13
14use clap::ValueEnum;
15use serde::{Deserialize, Serialize};
16
17// =============================================================================
18// Confidence Level
19// =============================================================================
20
21/// Confidence level for inferred contracts and invariants.
22///
23/// Confidence is determined by the source of the inference:
24/// - **High**: Direct code evidence (guard clause, assertion, explicit raise)
25/// - **Medium**: Inferred from patterns or consistent behavior
26/// - **Low**: Derived from type hints or annotations only
27///
28/// # Serialization
29///
30/// Serializes to snake_case: `"high"`, `"medium"`, `"low"`
31#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Serialize, Deserialize, Default)]
32#[serde(rename_all = "snake_case")]
33pub enum Confidence {
34    /// Direct code evidence (guard clause, assertion)
35    High,
36    /// Inferred from patterns or types
37    #[default]
38    Medium,
39    /// Derived from type hints only
40    Low,
41}
42
43impl std::fmt::Display for Confidence {
44    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
45        match self {
46            Self::High => write!(f, "high"),
47            Self::Medium => write!(f, "medium"),
48            Self::Low => write!(f, "low"),
49        }
50    }
51}
52
53// =============================================================================
54// Condition (Contract Element)
55// =============================================================================
56
57/// A single contract condition (precondition, postcondition, or invariant).
58///
59/// Represents a constraint on a variable that was detected in the source code.
60///
61/// # Example
62///
63/// ```json
64/// {
65///   "variable": "x",
66///   "constraint": "x >= 0",
67///   "source_line": 10,
68///   "confidence": "high"
69/// }
70/// ```
71#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
72pub struct Condition {
73    /// Variable name this condition applies to
74    pub variable: String,
75
76    /// Human-readable constraint expression (e.g., "x > 0", "isinstance(x, str)")
77    pub constraint: String,
78
79    /// Source line where condition was detected (1-indexed)
80    pub source_line: u32,
81
82    /// Confidence level of this condition
83    pub confidence: Confidence,
84}
85
86impl Condition {
87    /// Create a new condition with High confidence (from guard clause/assert)
88    pub fn high(variable: impl Into<String>, constraint: impl Into<String>, line: u32) -> Self {
89        Self {
90            variable: variable.into(),
91            constraint: constraint.into(),
92            source_line: line,
93            confidence: Confidence::High,
94        }
95    }
96
97    /// Create a new condition with Medium confidence (from patterns)
98    pub fn medium(variable: impl Into<String>, constraint: impl Into<String>, line: u32) -> Self {
99        Self {
100            variable: variable.into(),
101            constraint: constraint.into(),
102            source_line: line,
103            confidence: Confidence::Medium,
104        }
105    }
106
107    /// Create a new condition with Low confidence (from type hints)
108    pub fn low(variable: impl Into<String>, constraint: impl Into<String>, line: u32) -> Self {
109        Self {
110            variable: variable.into(),
111            constraint: constraint.into(),
112            source_line: line,
113            confidence: Confidence::Low,
114        }
115    }
116}
117
118// =============================================================================
119// Invariant Types
120// =============================================================================
121
122/// Types of invariants that can be inferred from test traces.
123///
124/// Based on Daikon-style invariant templates.
125///
126/// # Serialization
127///
128/// Serializes to snake_case: `"type"`, `"non_null"`, `"non_negative"`, etc.
129#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Serialize, Deserialize)]
130#[serde(rename_all = "snake_case")]
131pub enum InvariantKind {
132    /// Type invariant (e.g., "x: int")
133    Type,
134    /// Non-null invariant (no None values observed)
135    NonNull,
136    /// Non-negative numeric (all values >= 0)
137    NonNegative,
138    /// Positive numeric (all values > 0)
139    Positive,
140    /// Range constraint (min <= x <= max)
141    Range,
142    /// Ordering relation between parameters (e.g., start < end)
143    Relation,
144    /// Length constraint (e.g., len(x) > 0)
145    Length,
146}
147
148impl std::fmt::Display for InvariantKind {
149    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
150        match self {
151            Self::Type => write!(f, "type"),
152            Self::NonNull => write!(f, "non_null"),
153            Self::NonNegative => write!(f, "non_negative"),
154            Self::Positive => write!(f, "positive"),
155            Self::Range => write!(f, "range"),
156            Self::Relation => write!(f, "relation"),
157            Self::Length => write!(f, "length"),
158        }
159    }
160}
161
162/// An inferred invariant from test execution traces.
163///
164/// Invariants are derived from observing function behavior across multiple
165/// test executions.
166#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
167pub struct Invariant {
168    /// Variable name this invariant applies to
169    pub variable: String,
170
171    /// Kind of invariant
172    pub kind: InvariantKind,
173
174    /// Human-readable expression (e.g., "x >= 0", "isinstance(x, int)")
175    pub expression: String,
176
177    /// Confidence level based on observation count
178    pub confidence: Confidence,
179
180    /// Number of observations supporting this invariant
181    pub observations: u32,
182
183    /// Number of counterexamples observed (should be 0 for valid invariants)
184    pub counterexample_count: u32,
185}
186
187// =============================================================================
188// Spec Types (from test extraction)
189// =============================================================================
190
191/// Input/Output specification from a test assertion.
192///
193/// Extracted from patterns like `assert func(args) == expected`.
194#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
195pub struct InputOutputSpec {
196    /// Function being tested
197    pub function: String,
198
199    /// Input arguments (as JSON values)
200    pub inputs: Vec<serde_json::Value>,
201
202    /// Expected output (as JSON value)
203    pub output: serde_json::Value,
204
205    /// Name of the test function where this was found
206    pub test_function: String,
207
208    /// Line number in the test file
209    pub line: u32,
210
211    /// Confidence level
212    pub confidence: Confidence,
213}
214
215/// Exception specification from pytest.raises.
216///
217/// Extracted from patterns like `with pytest.raises(ValueError)`.
218#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
219pub struct ExceptionSpec {
220    /// Function being tested
221    pub function: String,
222
223    /// Input arguments that trigger the exception
224    pub inputs: Vec<serde_json::Value>,
225
226    /// Exception type expected (e.g., "ValueError")
227    pub exception_type: String,
228
229    /// Optional match pattern for exception message
230    pub match_pattern: Option<String>,
231
232    /// Name of the test function where this was found
233    pub test_function: String,
234
235    /// Line number in the test file
236    pub line: u32,
237
238    /// Confidence level
239    pub confidence: Confidence,
240}
241
242/// Property specification from test assertions.
243///
244/// Extracted from patterns like `assert isinstance(f(x), T)` or `assert len(f(x)) == n`.
245#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
246pub struct PropertySpec {
247    /// Function being tested
248    pub function: String,
249
250    /// Type of property: "type", "length", "bounds", "boolean", "membership", "not_none"
251    pub property_type: String,
252
253    /// Human-readable constraint
254    pub constraint: String,
255
256    /// Name of the test function where this was found
257    pub test_function: String,
258
259    /// Line number in the test file
260    pub line: u32,
261
262    /// Confidence level
263    pub confidence: Confidence,
264}
265
266// =============================================================================
267// Interval (for bounds analysis)
268// =============================================================================
269
270/// Numeric interval [lo, hi] for bounds analysis.
271///
272/// Represents the range of possible values for a numeric variable.
273/// Uses f64 for flexibility (handles both int and float).
274///
275/// # Special Values
276///
277/// - `top()`: [NEG_INFINITY, INFINITY] - any value possible
278/// - `bottom()`: [INFINITY, NEG_INFINITY] - no valid values (unreachable)
279/// - `const_val(n)`: [n, n] - exactly one value
280#[derive(Debug, Clone, Copy, PartialEq)]
281pub struct Interval {
282    /// Lower bound (f64::NEG_INFINITY for unbounded below)
283    pub lo: f64,
284
285    /// Upper bound (f64::INFINITY for unbounded above)
286    pub hi: f64,
287}
288
289// Custom serialization to handle infinity values as strings
290impl Serialize for Interval {
291    fn serialize<S>(&self, serializer: S) -> Result<S::Ok, S::Error>
292    where
293        S: serde::Serializer,
294    {
295        use serde::ser::SerializeStruct;
296        let mut state = serializer.serialize_struct("Interval", 2)?;
297
298        // Serialize lo
299        if self.lo == f64::NEG_INFINITY {
300            state.serialize_field("lo", "-inf")?;
301        } else if self.lo == f64::INFINITY {
302            state.serialize_field("lo", "+inf")?;
303        } else if self.lo.is_nan() {
304            state.serialize_field("lo", "NaN")?;
305        } else {
306            state.serialize_field("lo", &self.lo)?;
307        }
308
309        // Serialize hi
310        if self.hi == f64::NEG_INFINITY {
311            state.serialize_field("hi", "-inf")?;
312        } else if self.hi == f64::INFINITY {
313            state.serialize_field("hi", "+inf")?;
314        } else if self.hi.is_nan() {
315            state.serialize_field("hi", "NaN")?;
316        } else {
317            state.serialize_field("hi", &self.hi)?;
318        }
319
320        state.end()
321    }
322}
323
324// Custom deserialization to handle infinity values as strings
325impl<'de> Deserialize<'de> for Interval {
326    fn deserialize<D>(deserializer: D) -> Result<Self, D::Error>
327    where
328        D: serde::Deserializer<'de>,
329    {
330        #[derive(Deserialize)]
331        struct IntervalHelper {
332            lo: serde_json::Value,
333            hi: serde_json::Value,
334        }
335
336        let helper = IntervalHelper::deserialize(deserializer)?;
337
338        fn parse_bound(v: serde_json::Value) -> Result<f64, String> {
339            match v {
340                serde_json::Value::Number(n) => {
341                    n.as_f64().ok_or_else(|| "invalid number".to_string())
342                }
343                serde_json::Value::String(s) => match s.as_str() {
344                    "-inf" | "-Infinity" => Ok(f64::NEG_INFINITY),
345                    "+inf" | "inf" | "Infinity" => Ok(f64::INFINITY),
346                    "NaN" => Ok(f64::NAN),
347                    _ => s.parse::<f64>().map_err(|e| e.to_string()),
348                },
349                serde_json::Value::Null => Ok(f64::INFINITY), // null defaults to infinity
350                _ => Err("expected number or string".to_string()),
351            }
352        }
353
354        let lo = parse_bound(helper.lo).map_err(serde::de::Error::custom)?;
355        let hi = parse_bound(helper.hi).map_err(serde::de::Error::custom)?;
356
357        Ok(Interval { lo, hi })
358    }
359}
360
361impl Interval {
362    /// Create an interval containing exactly one value.
363    pub fn const_val(n: f64) -> Self {
364        Self { lo: n, hi: n }
365    }
366
367    /// Create the top element (any value possible).
368    pub fn top() -> Self {
369        Self {
370            lo: f64::NEG_INFINITY,
371            hi: f64::INFINITY,
372        }
373    }
374
375    /// Create the bottom element (no valid values - unreachable).
376    pub fn bottom() -> Self {
377        Self {
378            lo: f64::INFINITY,
379            hi: f64::NEG_INFINITY,
380        }
381    }
382
383    /// Check if this interval is bottom (empty/unreachable).
384    pub fn is_bottom(&self) -> bool {
385        self.lo > self.hi
386    }
387
388    /// Check if this interval is top (any value possible).
389    pub fn is_top(&self) -> bool {
390        self.lo == f64::NEG_INFINITY && self.hi == f64::INFINITY
391    }
392
393    /// Check if this interval contains a specific value.
394    pub fn contains(&self, n: f64) -> bool {
395        !self.is_bottom() && self.lo <= n && n <= self.hi
396    }
397
398    /// Check if this interval contains zero (important for division-by-zero detection).
399    pub fn contains_zero(&self) -> bool {
400        self.contains(0.0)
401    }
402
403    /// Compute the join (least upper bound) of two intervals.
404    ///
405    /// `[a,b] | [c,d] = [min(a,c), max(b,d)]`
406    pub fn join(&self, other: &Self) -> Self {
407        if self.is_bottom() {
408            return *other;
409        }
410        if other.is_bottom() {
411            return *self;
412        }
413        Self {
414            lo: self.lo.min(other.lo),
415            hi: self.hi.max(other.hi),
416        }
417    }
418
419    /// Compute the meet (greatest lower bound) of two intervals.
420    ///
421    /// `[a,b] & [c,d] = [max(a,c), min(b,d)]` or bottom if empty
422    pub fn meet(&self, other: &Self) -> Self {
423        if self.is_bottom() || other.is_bottom() {
424            return Self::bottom();
425        }
426        // Result may be bottom if intervals don't overlap.
427        Self {
428            lo: self.lo.max(other.lo),
429            hi: self.hi.min(other.hi),
430        }
431    }
432
433    /// Widen this interval based on new observations.
434    ///
435    /// Used to ensure convergence in fixpoint iteration.
436    /// `[a,b] W [c,d] = [c<a ? -inf : a, d>b ? +inf : b]`
437    pub fn widen(&self, other: &Self) -> Self {
438        if self.is_bottom() {
439            return *other;
440        }
441        if other.is_bottom() {
442            return *self;
443        }
444        Self {
445            lo: if other.lo < self.lo {
446                f64::NEG_INFINITY
447            } else {
448                self.lo
449            },
450            hi: if other.hi > self.hi {
451                f64::INFINITY
452            } else {
453                self.hi
454            },
455        }
456    }
457
458    /// Add two intervals: [a,b] + [c,d] = [a+c, b+d]
459    pub fn add(&self, other: &Self) -> Self {
460        if self.is_bottom() || other.is_bottom() {
461            return Self::bottom();
462        }
463        Self {
464            lo: self.lo + other.lo,
465            hi: self.hi + other.hi,
466        }
467    }
468
469    /// Subtract two intervals: [a,b] - [c,d] = [a-d, b-c]
470    pub fn sub(&self, other: &Self) -> Self {
471        if self.is_bottom() || other.is_bottom() {
472            return Self::bottom();
473        }
474        Self {
475            lo: self.lo - other.hi,
476            hi: self.hi - other.lo,
477        }
478    }
479
480    /// Multiply two intervals.
481    ///
482    /// Handles sign combinations correctly.
483    pub fn mul(&self, other: &Self) -> Self {
484        if self.is_bottom() || other.is_bottom() {
485            return Self::bottom();
486        }
487        // Compute all four products and take min/max
488        let products = [
489            self.lo * other.lo,
490            self.lo * other.hi,
491            self.hi * other.lo,
492            self.hi * other.hi,
493        ];
494        Self {
495            lo: products.iter().cloned().fold(f64::INFINITY, f64::min),
496            hi: products.iter().cloned().fold(f64::NEG_INFINITY, f64::max),
497        }
498    }
499
500    /// Divide two intervals.
501    ///
502    /// Returns (result, may_divide_by_zero) where may_divide_by_zero is true
503    /// if the divisor interval contains zero.
504    pub fn div(&self, other: &Self) -> (Self, bool) {
505        if self.is_bottom() || other.is_bottom() {
506            return (Self::bottom(), false);
507        }
508
509        let may_div_zero = other.contains_zero();
510
511        // If divisor is exactly [0,0], result is bottom (undefined)
512        if other.lo == 0.0 && other.hi == 0.0 {
513            return (Self::bottom(), true);
514        }
515
516        // Handle cases where divisor contains zero
517        if may_div_zero {
518            // Conservative: return top
519            return (Self::top(), true);
520        }
521
522        // Safe division: divisor doesn't contain zero
523        let products = [
524            self.lo / other.lo,
525            self.lo / other.hi,
526            self.hi / other.lo,
527            self.hi / other.hi,
528        ];
529        (
530            Self {
531                lo: products.iter().cloned().fold(f64::INFINITY, f64::min),
532                hi: products.iter().cloned().fold(f64::NEG_INFINITY, f64::max),
533            },
534            false,
535        )
536    }
537
538    /// Negate an interval: -[a,b] = [-b, -a]
539    pub fn neg(&self) -> Self {
540        if self.is_bottom() {
541            return Self::bottom();
542        }
543        Self {
544            lo: -self.hi,
545            hi: -self.lo,
546        }
547    }
548}
549
550impl Default for Interval {
551    fn default() -> Self {
552        Self::top()
553    }
554}
555
556impl std::fmt::Display for Interval {
557    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
558        if self.is_bottom() {
559            write!(f, "bottom")
560        } else if self.is_top() {
561            write!(f, "(-inf, +inf)")
562        } else if self.lo == self.hi {
563            write!(f, "[{}]", self.lo)
564        } else {
565            let lo_str = if self.lo == f64::NEG_INFINITY {
566                "-inf".to_string()
567            } else {
568                self.lo.to_string()
569            };
570            let hi_str = if self.hi == f64::INFINITY {
571                "+inf".to_string()
572            } else {
573                self.hi.to_string()
574            };
575            write!(f, "[{}, {}]", lo_str, hi_str)
576        }
577    }
578}
579
580// =============================================================================
581// Dead Store Detection
582// =============================================================================
583
584/// A dead store detected in SSA form.
585///
586/// A definition is dead if it has no uses (empty use_sites).
587#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
588pub struct DeadStore {
589    /// Original variable name (without SSA version suffix)
590    pub variable: String,
591
592    /// SSA versioned name (e.g., "x_2")
593    pub ssa_name: String,
594
595    /// Line number of the dead assignment (1-indexed)
596    pub line: u32,
597
598    /// Block ID where assignment occurs
599    pub block_id: u32,
600
601    /// Whether this is a phi function definition
602    pub is_phi: bool,
603}
604
605impl DeadStore {
606    /// Convert to JSON value for compatibility with spec
607    pub fn to_dict(&self) -> serde_json::Value {
608        serde_json::json!({
609            "variable": self.variable,
610            "ssa_name": self.ssa_name,
611            "line": self.line,
612            "block_id": self.block_id,
613            "is_phi": self.is_phi,
614        })
615    }
616}
617
618// =============================================================================
619// Chop Result (Slice Intersection)
620// =============================================================================
621
622/// Result of a chop operation (slice intersection).
623///
624/// Chop computes `forward_slice(source) AND backward_slice(target)` to find
625/// all statements on any path from source to target.
626#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
627pub struct ChopResult {
628    /// File path the chop was computed in.
629    ///
630    /// schema-cleanup-v1 BUG-21: added for parity with `tldr slice`,
631    /// which carries `file` in its JSON output. Empty string when the
632    /// caller-provided path could not be canonicalized (e.g.
633    /// validation failed before chop was attempted).
634    #[serde(default)]
635    pub file: String,
636
637    /// Lines on the dependency path (sorted)
638    pub lines: Vec<u32>,
639
640    /// Number of lines on the path.
641    ///
642    /// schema-cleanup-v1 BUG-21: kept for back-compat. New consumers
643    /// should prefer `line_count` (alias) which matches `tldr slice`.
644    pub count: u32,
645
646    /// Number of lines on the path. Alias of `count` for parity with
647    /// `tldr slice` (whose schema uses `line_count`).
648    ///
649    /// schema-cleanup-v1 BUG-21: ADDITIVE field — populated to the
650    /// same value as `count` so consumers using either field name see
651    /// matching values.
652    #[serde(default)]
653    pub line_count: u32,
654
655    /// Source line (where data flows FROM)
656    pub source_line: u32,
657
658    /// Target line (where data flows TO)
659    pub target_line: u32,
660
661    /// True if source_line is in backward_slice(target_line)
662    pub path_exists: bool,
663
664    /// Function name containing the analysis
665    pub function: String,
666
667    /// Human-readable explanation of the result
668    pub explanation: Option<String>,
669}
670
671impl ChopResult {
672    /// Create a result for when source and target are the same line.
673    pub fn same_line(line: u32, function: impl Into<String>) -> Self {
674        Self {
675            file: String::new(),
676            lines: vec![line],
677            count: 1,
678            line_count: 1,
679            source_line: line,
680            target_line: line,
681            path_exists: true,
682            function: function.into(),
683            explanation: Some(format!("Source and target are the same line ({}).", line)),
684        }
685    }
686
687    /// Create a result for when no path exists.
688    pub fn no_path(source: u32, target: u32, function: impl Into<String>) -> Self {
689        Self {
690            file: String::new(),
691            lines: vec![],
692            count: 0,
693            line_count: 0,
694            source_line: source,
695            target_line: target,
696            path_exists: false,
697            function: function.into(),
698            explanation: Some(format!(
699                "No dependency path from line {} to line {}. \
700                 The source line does not affect the target line.",
701                source, target
702            )),
703        }
704    }
705}
706
707// =============================================================================
708// Interval Warning
709// =============================================================================
710
711/// Warning from interval/bounds analysis.
712///
713/// Generated when analysis detects potential runtime issues like division by zero.
714#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
715pub struct IntervalWarning {
716    /// Line number where the warning applies
717    pub line: u32,
718
719    /// Kind of warning: "division_by_zero", "out_of_bounds", "overflow"
720    pub kind: String,
721
722    /// Variable involved
723    pub variable: String,
724
725    /// Current bounds for the variable
726    pub bounds: Interval,
727
728    /// Human-readable warning message
729    pub message: String,
730}
731
732// =============================================================================
733// Report Types
734// =============================================================================
735
736/// Report from the contracts command.
737#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
738pub struct ContractsReport {
739    /// Function analyzed
740    pub function: String,
741
742    /// File path
743    pub file: PathBuf,
744
745    /// Detected preconditions
746    pub preconditions: Vec<Condition>,
747
748    /// Detected postconditions
749    pub postconditions: Vec<Condition>,
750
751    /// Detected invariants
752    pub invariants: Vec<Condition>,
753}
754
755/// Invariants for a single function.
756#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
757pub struct FunctionInvariants {
758    /// Function name
759    pub function_name: String,
760
761    /// Inferred preconditions
762    pub preconditions: Vec<Invariant>,
763
764    /// Inferred postconditions
765    pub postconditions: Vec<Invariant>,
766
767    /// Total observations used for inference
768    pub observation_count: u32,
769}
770
771/// Summary of invariant inference.
772#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
773pub struct InvariantsSummary {
774    /// Total test observations across all functions
775    pub total_observations: u32,
776
777    /// Total invariants inferred
778    pub total_invariants: u32,
779
780    /// Count by invariant kind
781    pub by_kind: HashMap<String, u32>,
782
783    /// Number of test files the recogniser classified as tests for the
784    /// language under analysis (verification-pipeline-completeness-v1
785    /// P11.BUG-AGG-3 — previously the invariants command was
786    /// Python-only and silently reported 0 for every non-Python tree).
787    #[serde(default)]
788    pub test_files_scanned: u32,
789
790    /// Number of test functions detected across `test_files_scanned`
791    /// (counted via per-language AST recognisers in
792    /// `contracts::test_recognizer`).
793    #[serde(default)]
794    pub test_functions_scanned: u32,
795}
796
797/// Full report from the invariants command.
798#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
799pub struct InvariantsReport {
800    /// Invariants by function
801    pub functions: Vec<FunctionInvariants>,
802
803    /// Summary statistics
804    pub summary: InvariantsSummary,
805}
806
807/// Specs for a single function.
808#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
809pub struct FunctionSpecs {
810    /// Function name
811    pub function_name: String,
812
813    /// Human-readable summary (e.g., "3 input/output, 1 raises")
814    pub summary: String,
815
816    /// Number of test functions that test this function
817    pub test_count: u32,
818
819    /// Input/output specifications
820    pub input_output_specs: Vec<InputOutputSpec>,
821
822    /// Exception specifications
823    pub exception_specs: Vec<ExceptionSpec>,
824
825    /// Property specifications
826    pub property_specs: Vec<PropertySpec>,
827}
828
829/// Counts by spec type.
830#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
831pub struct SpecsByType {
832    /// Input/output spec count
833    pub input_output: u32,
834
835    /// Exception spec count
836    pub exception: u32,
837
838    /// Property spec count
839    pub property: u32,
840}
841
842/// Summary of specs extraction.
843#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
844pub struct SpecsSummary {
845    /// Total specs extracted
846    pub total_specs: u32,
847
848    /// Counts by type
849    pub by_type: SpecsByType,
850
851    /// Number of test functions scanned
852    pub test_functions_scanned: u32,
853
854    /// Number of test files scanned
855    pub test_files_scanned: u32,
856
857    /// Number of unique functions found
858    pub functions_found: u32,
859}
860
861/// Full report from the specs command.
862#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
863pub struct SpecsReport {
864    /// Specs by function
865    pub functions: Vec<FunctionSpecs>,
866
867    /// Summary statistics
868    pub summary: SpecsSummary,
869}
870
871/// Result from the bounds command.
872#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
873pub struct BoundsResult {
874    /// Function analyzed
875    pub function: String,
876
877    /// Interval bounds: line -> variable -> interval
878    pub bounds: HashMap<u32, HashMap<String, Interval>>,
879
880    /// Warnings (e.g., potential division by zero)
881    pub warnings: Vec<IntervalWarning>,
882
883    /// Whether analysis converged
884    pub converged: bool,
885
886    /// Number of fixpoint iterations
887    pub iterations: u32,
888}
889
890/// Report from the dead-stores command.
891#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
892pub struct DeadStoresReport {
893    /// Function analyzed
894    pub function: String,
895
896    /// File path
897    pub file: PathBuf,
898
899    /// Dead stores detected via SSA analysis
900    pub dead_stores_ssa: Vec<DeadStore>,
901
902    /// Count of dead stores
903    pub count: u32,
904
905    /// Optional: dead stores via live-vars analysis (if --compare flag used)
906    pub dead_stores_live_vars: Option<Vec<DeadStore>>,
907
908    /// Optional: count from live-vars analysis
909    pub live_vars_count: Option<u32>,
910}
911
912/// Status of a sub-analysis in verify command.
913#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
914#[serde(rename_all = "snake_case")]
915pub enum SubAnalysisStatus {
916    /// Analysis completed successfully
917    Success,
918    /// Analysis completed with partial results (some files failed)
919    Partial,
920    /// Analysis failed completely
921    Failed,
922    /// Analysis was skipped (e.g., in quick mode)
923    Skipped,
924}
925
926impl SubAnalysisStatus {
927    /// Returns true if the analysis succeeded (fully or partially)
928    pub fn is_success(&self) -> bool {
929        matches!(self, Self::Success | Self::Partial)
930    }
931}
932
933/// Result from a sub-analysis in verify command.
934#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
935pub struct SubAnalysisResult {
936    /// Name of the sub-analysis
937    pub name: String,
938
939    /// Status of the analysis
940    pub status: SubAnalysisStatus,
941
942    /// Number of items found (contracts, specs, warnings, etc.)
943    pub items_found: u32,
944
945    /// Time taken in milliseconds
946    pub elapsed_ms: u64,
947
948    /// Error message if failed or partial
949    pub error: Option<String>,
950
951    /// Analysis data (command-specific)
952    pub data: Option<serde_json::Value>,
953}
954
955impl SubAnalysisResult {
956    /// Returns true if the analysis succeeded (for backward compatibility)
957    pub fn success(&self) -> bool {
958        self.status.is_success()
959    }
960}
961
962/// Coverage information from verify command.
963///
964/// M18 (med-cleanup-bundle-v1): `total_functions` here counts only the
965/// functions surfaced by the contracts sub-analysis (i.e. those whose
966/// pre/postcondition or invariant amenability was actually evaluated),
967/// NOT every function in the project. Without explicit scoping the
968/// `coverage_pct = constrained_functions / total_functions` ratio
969/// looked like a global coverage number even though `structure` /
970/// `health` reported a much larger function count for the same path.
971/// The `scope` field documents this filter so JSON consumers can not
972/// misread a 96% verify-coverage as 96% project-coverage.
973#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
974pub struct CoverageInfo {
975    /// Number of functions with at least one constraint
976    pub constrained_functions: u32,
977
978    /// Number of functions in the constraint-relevant scope
979    /// (i.e. functions evaluated by the contracts analyzer; this is
980    /// typically a subset of the project's total function count).
981    pub total_functions: u32,
982
983    /// Coverage percentage (0.0 - 100.0), computed against
984    /// `total_functions` (constraint-relevant scope, not the full
985    /// project).
986    pub coverage_pct: f64,
987
988    /// M18: human-readable label describing what `total_functions`
989    /// counts. Always emitted so consumers can self-document the
990    /// `coverage_pct` denominator.
991    #[serde(default = "default_coverage_scope")]
992    pub scope: String,
993}
994
995/// Default scope label for `CoverageInfo` (M18).
996fn default_coverage_scope() -> String {
997    "constraint-relevant functions (subset of all project functions; see verify docs)".to_string()
998}
999
1000/// Summary from verify command.
1001#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
1002pub struct VerifySummary {
1003    /// Specs extracted from tests
1004    pub spec_count: u32,
1005
1006    /// Invariants inferred
1007    pub invariant_count: u32,
1008
1009    /// Contracts inferred
1010    pub contract_count: u32,
1011
1012    /// Annotated[T] constraints found
1013    pub annotated_count: u32,
1014
1015    /// Behavioral models extracted
1016    pub behavioral_count: u32,
1017
1018    /// Patterns detected
1019    pub pattern_count: u32,
1020
1021    /// High-confidence patterns
1022    pub pattern_high_confidence: u32,
1023
1024    /// Function coverage information
1025    pub coverage: CoverageInfo,
1026}
1027
1028/// Full report from verify command.
1029#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
1030pub struct VerifyReport {
1031    /// Path analyzed
1032    pub path: PathBuf,
1033
1034    /// Results from each sub-analysis
1035    pub sub_results: HashMap<String, SubAnalysisResult>,
1036
1037    /// Summary statistics
1038    pub summary: VerifySummary,
1039
1040    /// Total time taken in milliseconds
1041    pub total_elapsed_ms: u64,
1042
1043    /// Number of files analyzed
1044    pub files_analyzed: u32,
1045
1046    /// Number of files that failed to analyze
1047    pub files_failed: u32,
1048
1049    /// Whether some results are partial (some files or analyses failed)
1050    pub partial_results: bool,
1051}
1052
1053// =============================================================================
1054// Output Format
1055// =============================================================================
1056
1057/// Output format for command results.
1058#[derive(Debug, Clone, Copy, PartialEq, Eq, Default, ValueEnum)]
1059pub enum OutputFormat {
1060    /// JSON output (default)
1061    #[default]
1062    Json,
1063
1064    /// Human-readable text output
1065    Text,
1066}
1067
1068impl std::fmt::Display for OutputFormat {
1069    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
1070        match self {
1071            Self::Json => write!(f, "json"),
1072            Self::Text => write!(f, "text"),
1073        }
1074    }
1075}
1076
1077// =============================================================================
1078// Tests
1079// =============================================================================
1080
1081#[cfg(test)]
1082mod tests {
1083    use super::*;
1084
1085    // -------------------------------------------------------------------------
1086    // Confidence Tests
1087    // -------------------------------------------------------------------------
1088
1089    #[test]
1090    fn test_confidence_enum_serialization() {
1091        assert_eq!(
1092            serde_json::to_string(&Confidence::High).unwrap(),
1093            "\"high\""
1094        );
1095        assert_eq!(
1096            serde_json::to_string(&Confidence::Medium).unwrap(),
1097            "\"medium\""
1098        );
1099        assert_eq!(serde_json::to_string(&Confidence::Low).unwrap(), "\"low\"");
1100    }
1101
1102    #[test]
1103    fn test_confidence_enum_deserialization() {
1104        assert_eq!(
1105            serde_json::from_str::<Confidence>("\"high\"").unwrap(),
1106            Confidence::High
1107        );
1108        assert_eq!(
1109            serde_json::from_str::<Confidence>("\"medium\"").unwrap(),
1110            Confidence::Medium
1111        );
1112        assert_eq!(
1113            serde_json::from_str::<Confidence>("\"low\"").unwrap(),
1114            Confidence::Low
1115        );
1116    }
1117
1118    #[test]
1119    fn test_confidence_default() {
1120        assert_eq!(Confidence::default(), Confidence::Medium);
1121    }
1122
1123    // -------------------------------------------------------------------------
1124    // Condition Tests
1125    // -------------------------------------------------------------------------
1126
1127    #[test]
1128    fn test_condition_struct_fields() {
1129        let cond = Condition::high("x", "x >= 0", 10);
1130        assert_eq!(cond.variable, "x");
1131        assert_eq!(cond.constraint, "x >= 0");
1132        assert_eq!(cond.source_line, 10);
1133        assert_eq!(cond.confidence, Confidence::High);
1134    }
1135
1136    #[test]
1137    fn test_condition_serialization() {
1138        let cond = Condition::high("x", "x >= 0", 10);
1139        let json = serde_json::to_string(&cond).unwrap();
1140        assert!(json.contains("\"variable\":\"x\""));
1141        assert!(json.contains("\"confidence\":\"high\""));
1142    }
1143
1144    // -------------------------------------------------------------------------
1145    // Interval Tests
1146    // -------------------------------------------------------------------------
1147
1148    #[test]
1149    fn test_interval_const_val() {
1150        let i = Interval::const_val(5.0);
1151        assert_eq!(i.lo, 5.0);
1152        assert_eq!(i.hi, 5.0);
1153        assert!(i.contains(5.0));
1154        assert!(!i.contains(4.0));
1155        assert!(!i.contains(6.0));
1156    }
1157
1158    #[test]
1159    fn test_interval_basic_operations() {
1160        let i = Interval { lo: 0.0, hi: 10.0 };
1161        assert!(i.contains(0.0));
1162        assert!(i.contains(5.0));
1163        assert!(i.contains(10.0));
1164        assert!(!i.contains(-1.0));
1165        assert!(!i.contains(11.0));
1166    }
1167
1168    #[test]
1169    fn test_interval_bottom_top_detection() {
1170        assert!(Interval::bottom().is_bottom());
1171        assert!(!Interval::top().is_bottom());
1172        assert!(Interval::top().is_top());
1173        assert!(!Interval::bottom().is_top());
1174        assert!(!Interval::const_val(5.0).is_bottom());
1175        assert!(!Interval::const_val(5.0).is_top());
1176    }
1177
1178    #[test]
1179    fn test_interval_contains_zero() {
1180        assert!(Interval { lo: -5.0, hi: 5.0 }.contains_zero());
1181        assert!(Interval { lo: 0.0, hi: 10.0 }.contains_zero());
1182        assert!(Interval { lo: -10.0, hi: 0.0 }.contains_zero());
1183        assert!(!Interval { lo: 1.0, hi: 10.0 }.contains_zero());
1184        assert!(!Interval {
1185            lo: -10.0,
1186            hi: -1.0
1187        }
1188        .contains_zero());
1189    }
1190
1191    #[test]
1192    fn test_interval_join() {
1193        let a = Interval { lo: 0.0, hi: 5.0 };
1194        let b = Interval { lo: 3.0, hi: 10.0 };
1195        let joined = a.join(&b);
1196        assert_eq!(joined.lo, 0.0);
1197        assert_eq!(joined.hi, 10.0);
1198    }
1199
1200    #[test]
1201    fn test_interval_meet() {
1202        let a = Interval { lo: 0.0, hi: 5.0 };
1203        let b = Interval { lo: 3.0, hi: 10.0 };
1204        let met = a.meet(&b);
1205        assert_eq!(met.lo, 3.0);
1206        assert_eq!(met.hi, 5.0);
1207    }
1208
1209    #[test]
1210    fn test_interval_add() {
1211        let a = Interval { lo: 1.0, hi: 5.0 };
1212        let b = Interval { lo: 2.0, hi: 3.0 };
1213        let sum = a.add(&b);
1214        assert_eq!(sum.lo, 3.0);
1215        assert_eq!(sum.hi, 8.0);
1216    }
1217
1218    #[test]
1219    fn test_interval_sub() {
1220        let a = Interval { lo: 5.0, hi: 10.0 };
1221        let b = Interval { lo: 1.0, hi: 3.0 };
1222        let diff = a.sub(&b);
1223        assert_eq!(diff.lo, 2.0); // 5 - 3
1224        assert_eq!(diff.hi, 9.0); // 10 - 1
1225    }
1226
1227    #[test]
1228    fn test_interval_mul() {
1229        let a = Interval { lo: 2.0, hi: 3.0 };
1230        let b = Interval { lo: 4.0, hi: 5.0 };
1231        let prod = a.mul(&b);
1232        assert_eq!(prod.lo, 8.0);
1233        assert_eq!(prod.hi, 15.0);
1234    }
1235
1236    #[test]
1237    fn test_interval_mul_negative() {
1238        let a = Interval { lo: -2.0, hi: 3.0 };
1239        let b = Interval { lo: -1.0, hi: 2.0 };
1240        let prod = a.mul(&b);
1241        // Products: 2, -4, -3, 6 -> min=-4, max=6
1242        assert_eq!(prod.lo, -4.0);
1243        assert_eq!(prod.hi, 6.0);
1244    }
1245
1246    #[test]
1247    fn test_interval_div() {
1248        let a = Interval { lo: 10.0, hi: 20.0 };
1249        let b = Interval { lo: 2.0, hi: 5.0 };
1250        let (quot, div_zero) = a.div(&b);
1251        assert!(!div_zero);
1252        assert_eq!(quot.lo, 2.0); // 10 / 5
1253        assert_eq!(quot.hi, 10.0); // 20 / 2
1254    }
1255
1256    #[test]
1257    fn test_interval_div_by_zero() {
1258        let a = Interval { lo: 10.0, hi: 20.0 };
1259        let b = Interval { lo: -1.0, hi: 1.0 }; // Contains zero
1260        let (_, div_zero) = a.div(&b);
1261        assert!(div_zero);
1262    }
1263
1264    #[test]
1265    fn test_interval_widen() {
1266        let a = Interval { lo: 0.0, hi: 10.0 };
1267        let b = Interval { lo: -5.0, hi: 15.0 };
1268        let widened = a.widen(&b);
1269        assert_eq!(widened.lo, f64::NEG_INFINITY);
1270        assert_eq!(widened.hi, f64::INFINITY);
1271    }
1272
1273    // -------------------------------------------------------------------------
1274    // Dead Store Tests
1275    // -------------------------------------------------------------------------
1276
1277    #[test]
1278    fn test_dead_store_struct() {
1279        let ds = DeadStore {
1280            variable: "x".to_string(),
1281            ssa_name: "x_2".to_string(),
1282            line: 10,
1283            block_id: 1,
1284            is_phi: false,
1285        };
1286        assert_eq!(ds.variable, "x");
1287        assert_eq!(ds.ssa_name, "x_2");
1288        assert_eq!(ds.line, 10);
1289        assert!(!ds.is_phi);
1290    }
1291
1292    #[test]
1293    fn test_dead_store_serialization() {
1294        let ds = DeadStore {
1295            variable: "x".to_string(),
1296            ssa_name: "x_2".to_string(),
1297            line: 10,
1298            block_id: 1,
1299            is_phi: false,
1300        };
1301        let json = serde_json::to_string(&ds).unwrap();
1302        assert!(json.contains("\"variable\":\"x\""));
1303        assert!(json.contains("\"ssa_name\":\"x_2\""));
1304    }
1305
1306    // -------------------------------------------------------------------------
1307    // Chop Result Tests
1308    // -------------------------------------------------------------------------
1309
1310    #[test]
1311    fn test_chop_result_struct() {
1312        let result = ChopResult {
1313            file: "test.py".to_string(),
1314            lines: vec![2, 3, 4],
1315            count: 3,
1316            line_count: 3,
1317            source_line: 2,
1318            target_line: 4,
1319            path_exists: true,
1320            function: "example".to_string(),
1321            explanation: Some("Found path".to_string()),
1322        };
1323        assert_eq!(result.count, 3);
1324        assert!(result.path_exists);
1325    }
1326
1327    #[test]
1328    fn test_chop_result_same_line() {
1329        let result = ChopResult::same_line(5, "test_func");
1330        assert_eq!(result.lines, vec![5]);
1331        assert_eq!(result.count, 1);
1332        assert!(result.path_exists);
1333    }
1334
1335    #[test]
1336    fn test_chop_result_no_path() {
1337        let result = ChopResult::no_path(2, 10, "test_func");
1338        assert!(result.lines.is_empty());
1339        assert_eq!(result.count, 0);
1340        assert!(!result.path_exists);
1341    }
1342
1343    // -------------------------------------------------------------------------
1344    // Contracts Report Tests
1345    // -------------------------------------------------------------------------
1346
1347    #[test]
1348    fn test_contracts_report_struct() {
1349        let report = ContractsReport {
1350            function: "process_data".to_string(),
1351            file: PathBuf::from("test.py"),
1352            preconditions: vec![Condition::high("x", "x >= 0", 10)],
1353            postconditions: vec![],
1354            invariants: vec![],
1355        };
1356        assert_eq!(report.function, "process_data");
1357        assert_eq!(report.preconditions.len(), 1);
1358    }
1359
1360    // -------------------------------------------------------------------------
1361    // InvariantKind Tests
1362    // -------------------------------------------------------------------------
1363
1364    #[test]
1365    fn test_invariant_kind_serialization() {
1366        assert_eq!(
1367            serde_json::to_string(&InvariantKind::Type).unwrap(),
1368            "\"type\""
1369        );
1370        assert_eq!(
1371            serde_json::to_string(&InvariantKind::NonNull).unwrap(),
1372            "\"non_null\""
1373        );
1374        assert_eq!(
1375            serde_json::to_string(&InvariantKind::NonNegative).unwrap(),
1376            "\"non_negative\""
1377        );
1378    }
1379
1380    // -------------------------------------------------------------------------
1381    // Output Format Tests
1382    // -------------------------------------------------------------------------
1383
1384    #[test]
1385    fn test_output_format_default() {
1386        assert_eq!(OutputFormat::default(), OutputFormat::Json);
1387    }
1388
1389    #[test]
1390    fn test_output_format_display() {
1391        assert_eq!(OutputFormat::Json.to_string(), "json");
1392        assert_eq!(OutputFormat::Text.to_string(), "text");
1393    }
1394}