logicaffeine_verify/error.rs
1//! Verification error types with Socratic error messages.
2//!
3//! ## Philosophy
4//!
5//! Errors in this module follow the Socratic method: they guide users toward
6//! understanding rather than simply reporting failures. Each error type includes:
7//!
8//! - A clear description of what went wrong
9//! - Context about why it matters
10//! - Guidance on how to address the issue
11//! - When available, a concrete counterexample
12//!
13//! ## Error Categories
14//!
15//! | Category | Error Types | User Action |
16//! |----------|-------------|-------------|
17//! | Logic | `ContradictoryAssertion`, `BoundsViolation`, `RefinementViolation` | Fix the logical issue |
18//! | License | `LicenseRequired`, `LicenseInvalid`, `LicenseInsufficientPlan` | Provide valid license |
19//! | Solver | `SolverUnknown`, `SolverError` | Simplify or restructure |
20//! | Termination | `TerminationViolation` | Add decreasing variant |
21
22use std::fmt;
23
24/// Result type for verification operations.
25pub type VerificationResult<T = ()> = Result<T, VerificationError>;
26
27/// A verification error with Socratic explanation.
28///
29/// Each error includes contextual information to help users understand
30/// and fix the issue.
31///
32/// # Fields
33///
34/// - `kind`: Categorizes the error type
35/// - `span`: Source location (byte offsets) where the error occurred
36/// - `explanation`: Human-readable context explaining why verification failed
37/// - `counterexample`: Concrete variable assignments that demonstrate the failure
38#[derive(Debug)]
39pub struct VerificationError {
40 /// The category of verification error.
41 pub kind: VerificationErrorKind,
42 /// Optional source span as `(start, end)` byte offsets.
43 pub span: Option<(usize, usize)>,
44 /// Human-readable explanation of why verification failed.
45 pub explanation: String,
46 /// Concrete witness showing a failing case, when available.
47 pub counterexample: Option<CounterExample>,
48}
49
50/// The category of verification error.
51///
52/// Each variant represents a distinct failure mode with specific remediation steps.
53#[derive(Debug, Clone, PartialEq)]
54pub enum VerificationErrorKind {
55 /// An assertion that can never be true.
56 ///
57 /// Z3 proved that no interpretation satisfies the assertion.
58 ///
59 /// **Common causes:**
60 /// - Conflicting constraints (e.g., `x > 5` and `x < 3`)
61 /// - Logical contradictions in premises
62 /// - Impossible refinement type predicates
63 ///
64 /// **Action:** Review your assumptions for conflicts.
65 ContradictoryAssertion,
66
67 /// A variable violates its declared bounds.
68 ///
69 /// The verifier found a possible value that falls outside the
70 /// declared constraint.
71 ///
72 /// **Action:** Either tighten the constraint or add assumptions
73 /// that rule out the violating value.
74 BoundsViolation {
75 /// The variable that violated its bounds.
76 var: String,
77 /// The constraint that was expected.
78 expected: String,
79 /// The value that violated the constraint.
80 found: String,
81 },
82
83 /// A refinement type predicate is not satisfied.
84 ///
85 /// The value being assigned does not satisfy the predicate
86 /// in the refinement type definition.
87 ///
88 /// **Action:** Ensure the value meets the refinement predicate,
89 /// or add assumptions that constrain the value appropriately.
90 RefinementViolation {
91 /// The name of the refinement type.
92 type_name: String,
93 },
94
95 /// Verification requires a license key.
96 ///
97 /// **Action:** Provide a license key via `--license <key>` or the
98 /// `LOGOS_LICENSE` environment variable.
99 LicenseRequired,
100
101 /// The license key is invalid or expired.
102 ///
103 /// **Action:** Check that your license key is correct and active.
104 LicenseInvalid {
105 /// The reason the license was rejected.
106 reason: String,
107 },
108
109 /// The license plan doesn't include verification.
110 ///
111 /// Verification requires Pro, Premium, Lifetime, or Enterprise plan.
112 ///
113 /// **Action:** Upgrade your plan at <https://logicaffeine.com/pricing>.
114 LicenseInsufficientPlan {
115 /// The user's current plan.
116 current: String,
117 },
118
119 /// Z3 returned unknown (timeout or undecidable).
120 ///
121 /// The solver could not determine validity within the timeout period,
122 /// or the problem is undecidable.
123 ///
124 /// **Action:** Simplify the assertion or add more constraining assumptions.
125 SolverUnknown,
126
127 /// Z3 initialization or internal error.
128 ///
129 /// An unexpected error occurred in the Z3 solver.
130 ///
131 /// **Action:** Check that Z3 is properly installed and configured.
132 SolverError {
133 /// The error message from Z3.
134 message: String,
135 },
136
137 /// Loop termination cannot be proven.
138 ///
139 /// The verifier could not prove that the loop variant strictly decreases
140 /// on each iteration while remaining non-negative.
141 ///
142 /// **Action:** Ensure your variant expression decreases by at least 1
143 /// on each iteration and has a lower bound.
144 TerminationViolation {
145 /// The variant expression that should decrease.
146 variant: String,
147 /// Why termination could not be proven.
148 reason: String,
149 },
150}
151
152/// A counterexample showing concrete values that falsify an assertion.
153///
154/// When Z3 finds that an assertion is not valid, it produces a model
155/// (set of variable assignments) that makes the negation of the assertion true.
156/// This counterexample helps users understand exactly why verification failed.
157///
158/// # Example Interpretation
159///
160/// If verifying `x > 5` fails with counterexample `x = 3`, this means:
161/// - The solver found that `x = 3` is a possible value
162/// - With `x = 3`, the assertion `x > 5` is false
163/// - Therefore the assertion is not universally valid
164#[derive(Debug, Clone)]
165pub struct CounterExample {
166 /// Variable assignments that make the assertion false.
167 ///
168 /// Each tuple contains `(variable_name, value_as_string)`.
169 pub assignments: Vec<(String, String)>,
170}
171
172impl fmt::Display for CounterExample {
173 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
174 for (var, val) in &self.assignments {
175 write!(f, "{} = {}", var, val)?;
176 if self.assignments.len() > 1 {
177 write!(f, ", ")?;
178 }
179 }
180 Ok(())
181 }
182}
183
184impl fmt::Display for VerificationError {
185 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
186 match &self.kind {
187 VerificationErrorKind::ContradictoryAssertion => {
188 writeln!(f, "This assertion can never be true.")?;
189 writeln!(f)?;
190 writeln!(f, "{}", self.explanation)?;
191 if let Some(ce) = &self.counterexample {
192 writeln!(f)?;
193 writeln!(f, "Counter-example: {}", ce)?;
194 }
195 }
196 VerificationErrorKind::BoundsViolation { var, expected, found } => {
197 writeln!(f, "Value '{}' violates its constraint.", var)?;
198 writeln!(f)?;
199 writeln!(f, "Expected: {}", expected)?;
200 writeln!(f, "But found possible value: {}", found)?;
201 }
202 VerificationErrorKind::RefinementViolation { type_name } => {
203 writeln!(f, "Value does not satisfy refinement type '{}'.", type_name)?;
204 writeln!(f)?;
205 writeln!(f, "{}", self.explanation)?;
206 }
207 VerificationErrorKind::LicenseRequired => {
208 writeln!(f, "Verification requires a license key.")?;
209 writeln!(f)?;
210 writeln!(f, "Use --license <key> or set the LOGOS_LICENSE environment variable.")?;
211 writeln!(f, "Get a license at https://logicaffeine.com/pricing")?;
212 }
213 VerificationErrorKind::LicenseInvalid { reason } => {
214 writeln!(f, "License validation failed: {}", reason)?;
215 }
216 VerificationErrorKind::LicenseInsufficientPlan { current } => {
217 writeln!(f, "Verification requires Pro, Premium, Lifetime, or Enterprise plan.")?;
218 writeln!(f)?;
219 writeln!(f, "Current plan: {}", current)?;
220 writeln!(f, "Upgrade at https://logicaffeine.com/pricing")?;
221 }
222 VerificationErrorKind::SolverUnknown => {
223 writeln!(f, "The solver could not determine if the assertion is valid.")?;
224 writeln!(f)?;
225 writeln!(f, "This may be due to complexity or timeout.")?;
226 }
227 VerificationErrorKind::SolverError { message } => {
228 writeln!(f, "Solver error: {}", message)?;
229 }
230 VerificationErrorKind::TerminationViolation { variant, reason } => {
231 writeln!(f, "Cannot prove loop terminates.")?;
232 writeln!(f)?;
233 writeln!(f, "Variant '{}' does not strictly decrease: {}", variant, reason)?;
234 }
235 }
236 Ok(())
237 }
238}
239
240impl std::error::Error for VerificationError {}
241
242impl VerificationError {
243 // ---- License Errors ----
244
245 /// Create a license required error.
246 ///
247 /// Use when verification is attempted without providing a license key.
248 pub fn license_required() -> Self {
249 Self {
250 kind: VerificationErrorKind::LicenseRequired,
251 span: None,
252 explanation: String::new(),
253 counterexample: None,
254 }
255 }
256
257 /// Create a license invalid error.
258 ///
259 /// Use when the provided license key fails validation.
260 pub fn license_invalid(reason: impl Into<String>) -> Self {
261 Self {
262 kind: VerificationErrorKind::LicenseInvalid {
263 reason: reason.into(),
264 },
265 span: None,
266 explanation: String::new(),
267 counterexample: None,
268 }
269 }
270
271 /// Create an insufficient plan error.
272 ///
273 /// Use when the license is valid but the plan doesn't include verification.
274 pub fn insufficient_plan(current: impl Into<String>) -> Self {
275 Self {
276 kind: VerificationErrorKind::LicenseInsufficientPlan {
277 current: current.into(),
278 },
279 span: None,
280 explanation: String::new(),
281 counterexample: None,
282 }
283 }
284
285 // ---- Logic Errors ----
286
287 /// Create a contradictory assertion error.
288 ///
289 /// Use when Z3 proves the negation of an assertion is satisfiable.
290 pub fn contradiction(explanation: impl Into<String>, counterexample: Option<CounterExample>) -> Self {
291 Self {
292 kind: VerificationErrorKind::ContradictoryAssertion,
293 span: None,
294 explanation: explanation.into(),
295 counterexample,
296 }
297 }
298
299 /// Create a bounds violation error.
300 ///
301 /// Use when a variable's value falls outside its declared constraint.
302 pub fn bounds_violation(
303 var: impl Into<String>,
304 expected: impl Into<String>,
305 found: impl Into<String>,
306 ) -> Self {
307 Self {
308 kind: VerificationErrorKind::BoundsViolation {
309 var: var.into(),
310 expected: expected.into(),
311 found: found.into(),
312 },
313 span: None,
314 explanation: String::new(),
315 counterexample: None,
316 }
317 }
318
319 /// Create a refinement type violation error.
320 ///
321 /// Use when a value does not satisfy its refinement type predicate.
322 pub fn refinement_violation(type_name: impl Into<String>, explanation: impl Into<String>) -> Self {
323 Self {
324 kind: VerificationErrorKind::RefinementViolation {
325 type_name: type_name.into(),
326 },
327 span: None,
328 explanation: explanation.into(),
329 counterexample: None,
330 }
331 }
332
333 // ---- Solver Errors ----
334
335 /// Create a solver unknown error.
336 ///
337 /// Use when Z3 cannot determine satisfiability (timeout or undecidable).
338 pub fn solver_unknown() -> Self {
339 Self {
340 kind: VerificationErrorKind::SolverUnknown,
341 span: None,
342 explanation: String::new(),
343 counterexample: None,
344 }
345 }
346
347 /// Create a solver error.
348 ///
349 /// Use when Z3 encounters an internal error or configuration issue.
350 pub fn solver_error(message: impl Into<String>) -> Self {
351 Self {
352 kind: VerificationErrorKind::SolverError {
353 message: message.into(),
354 },
355 span: None,
356 explanation: String::new(),
357 counterexample: None,
358 }
359 }
360
361 // ---- Termination Errors ----
362
363 /// Create a termination violation error.
364 ///
365 /// Use when loop termination cannot be proven via the variant expression.
366 pub fn termination_violation(variant: impl Into<String>, reason: impl Into<String>) -> Self {
367 Self {
368 kind: VerificationErrorKind::TerminationViolation {
369 variant: variant.into(),
370 reason: reason.into(),
371 },
372 span: None,
373 explanation: String::new(),
374 counterexample: None,
375 }
376 }
377
378 // ---- Builder Methods ----
379
380 /// Set the source span for this error.
381 ///
382 /// Spans are byte offsets `(start, end)` into the source text.
383 pub fn with_span(mut self, start: usize, end: usize) -> Self {
384 self.span = Some((start, end));
385 self
386 }
387}