karpal_verify/
obligation.rs

1#[cfg(not(feature = "std"))]
2use alloc::{format, string::String, vec, vec::Vec};
3#[cfg(feature = "std")]
4use std::{format, string::String, vec, vec::Vec};
5
6use karpal_proof::{
7    AdditivelyCommutative, HasLeftIdentity, HasLeftInverse, HasRightIdentity, HasRightInverse,
8    IsAbsorptive, IsAssociative, IsCommutative, IsDistributive, IsIdempotent, IsMonoid, Property,
9};
10
11use crate::signature::AlgebraicSignature;
12
13/// Verification philosophy tier, following the roadmap's three-tier model.
14#[derive(Debug, Clone, Copy, PartialEq, Eq)]
15pub enum VerificationTier {
16    /// Illegal states are unrepresentable in Rust's type system.
17    Impossible,
18    /// Statistical evidence makes violations rare in practice.
19    Rare,
20    /// Runtime or search-based discovery catches emergent behavior.
21    Emergent,
22    /// External theorem prover or proof assistant evidence.
23    External,
24}
25
26/// Target proof language / export dialect.
27#[derive(Debug, Clone, Copy, PartialEq, Eq)]
28pub enum ProofDialect {
29    SmtLib2,
30    Lean4,
31}
32
33/// Source location for a generated proof obligation.
34#[derive(Debug, Clone, PartialEq, Eq)]
35pub struct Origin {
36    pub crate_name: String,
37    pub item_path: String,
38}
39
40impl Origin {
41    pub fn new(crate_name: impl Into<String>, item_path: impl Into<String>) -> Self {
42        Self {
43            crate_name: crate_name.into(),
44            item_path: item_path.into(),
45        }
46    }
47}
48
49/// A declared variable or constant used by an obligation.
50#[derive(Debug, Clone, PartialEq, Eq)]
51pub struct Declaration {
52    pub name: String,
53    pub sort: Sort,
54}
55
56impl Declaration {
57    pub fn new(name: impl Into<String>, sort: Sort) -> Self {
58        Self {
59            name: name.into(),
60            sort,
61        }
62    }
63}
64
65/// Sorts supported by the backend-agnostic obligation IR.
66#[derive(Debug, Clone, PartialEq, Eq)]
67pub enum Sort {
68    Bool,
69    Int,
70    Real,
71    Named(String),
72}
73
74impl Sort {
75    pub fn named(name: impl Into<String>) -> Self {
76        Self::Named(name.into())
77    }
78}
79
80/// Backend-agnostic term language for proof obligations.
81#[derive(Debug, Clone, PartialEq, Eq)]
82pub enum Term {
83    Var(String),
84    Bool(bool),
85    Int(i64),
86    App { function: String, args: Vec<Term> },
87    Eq(Box<Term>, Box<Term>),
88    And(Vec<Term>),
89    Or(Vec<Term>),
90    Not(Box<Term>),
91    Implies(Box<Term>, Box<Term>),
92}
93
94impl Term {
95    pub fn var(name: impl Into<String>) -> Self {
96        Self::Var(name.into())
97    }
98
99    pub fn bool(value: bool) -> Self {
100        Self::Bool(value)
101    }
102
103    pub fn int(value: i64) -> Self {
104        Self::Int(value)
105    }
106
107    pub fn app(function: impl Into<String>, args: impl IntoIterator<Item = Term>) -> Self {
108        Self::App {
109            function: function.into(),
110            args: args.into_iter().collect(),
111        }
112    }
113
114    pub fn eq(left: Term, right: Term) -> Self {
115        Self::Eq(Box::new(left), Box::new(right))
116    }
117
118    pub fn and(terms: impl IntoIterator<Item = Term>) -> Self {
119        Self::And(terms.into_iter().collect())
120    }
121
122    pub fn or(terms: impl IntoIterator<Item = Term>) -> Self {
123        Self::Or(terms.into_iter().collect())
124    }
125
126    pub fn negate(term: Term) -> Self {
127        Self::Not(Box::new(term))
128    }
129
130    pub fn implies(lhs: Term, rhs: Term) -> Self {
131        Self::Implies(Box::new(lhs), Box::new(rhs))
132    }
133}
134
135/// A backend-agnostic proof obligation.
136#[derive(Debug, Clone, PartialEq, Eq)]
137pub struct Obligation {
138    pub name: String,
139    pub property: &'static str,
140    pub declarations: Vec<Declaration>,
141    pub assumptions: Vec<Term>,
142    pub conclusion: Term,
143    pub origin: Origin,
144    pub tier: VerificationTier,
145}
146
147impl Obligation {
148    /// Create a new obligation for property `P`.
149    pub fn for_property<P: Property>(
150        name: impl Into<String>,
151        origin: Origin,
152        tier: VerificationTier,
153        conclusion: Term,
154    ) -> Self {
155        Self {
156            name: name.into(),
157            property: P::NAME,
158            declarations: Vec::new(),
159            assumptions: Vec::new(),
160            conclusion,
161            origin,
162            tier,
163        }
164    }
165
166    pub fn with_decl(mut self, name: impl Into<String>, sort: Sort) -> Self {
167        self.declarations.push(Declaration::new(name, sort));
168        self
169    }
170
171    pub fn with_assumption(mut self, term: Term) -> Self {
172        self.assumptions.push(term);
173        self
174    }
175
176    /// Build an associativity obligation for a binary operator symbol.
177    pub fn associativity(
178        name: impl Into<String>,
179        origin: Origin,
180        carrier: Sort,
181        op: impl Into<String>,
182    ) -> Self {
183        let op = op.into();
184        let (a, b, c) = (Term::var("a"), Term::var("b"), Term::var("c"));
185        let left = Term::app(
186            op.clone(),
187            vec![Term::app(op.clone(), vec![a.clone(), b.clone()]), c.clone()],
188        );
189        let right = Term::app(
190            op.clone(),
191            vec![a.clone(), Term::app(op, vec![b.clone(), c])],
192        );
193
194        Self::for_property::<IsAssociative>(
195            name,
196            origin,
197            VerificationTier::External,
198            Term::eq(left, right),
199        )
200        .with_decl("a", carrier.clone())
201        .with_decl("b", carrier.clone())
202        .with_decl("c", carrier)
203    }
204
205    pub fn associativity_in(
206        name: impl Into<String>,
207        origin: Origin,
208        signature: &AlgebraicSignature,
209        role: &str,
210    ) -> Self {
211        Self::associativity(
212            name,
213            origin,
214            signature.carrier.clone(),
215            signature.require_binary(role),
216        )
217    }
218
219    /// Build a commutativity obligation for a binary operator symbol.
220    pub fn commutativity(
221        name: impl Into<String>,
222        origin: Origin,
223        carrier: Sort,
224        op: impl Into<String>,
225    ) -> Self {
226        let op = op.into();
227        let (a, b) = (Term::var("a"), Term::var("b"));
228        let left = Term::app(op.clone(), vec![a.clone(), b.clone()]);
229        let right = Term::app(op, vec![b, a]);
230
231        Self::for_property::<IsCommutative>(
232            name,
233            origin,
234            VerificationTier::External,
235            Term::eq(left, right),
236        )
237        .with_decl("a", carrier.clone())
238        .with_decl("b", carrier)
239    }
240
241    pub fn commutativity_in(
242        name: impl Into<String>,
243        origin: Origin,
244        signature: &AlgebraicSignature,
245        role: &str,
246    ) -> Self {
247        Self::commutativity(
248            name,
249            origin,
250            signature.carrier.clone(),
251            signature.require_binary(role),
252        )
253    }
254
255    pub fn additive_commutativity(
256        name: impl Into<String>,
257        origin: Origin,
258        carrier: Sort,
259        add: impl Into<String>,
260    ) -> Self {
261        let add = add.into();
262        let (a, b) = (Term::var("a"), Term::var("b"));
263        let left = Term::app(add.clone(), vec![a.clone(), b.clone()]);
264        let right = Term::app(add, vec![b, a]);
265
266        Self::for_property::<AdditivelyCommutative>(
267            name,
268            origin,
269            VerificationTier::External,
270            Term::eq(left, right),
271        )
272        .with_decl("a", carrier.clone())
273        .with_decl("b", carrier)
274    }
275
276    pub fn additive_commutativity_in(
277        name: impl Into<String>,
278        origin: Origin,
279        signature: &AlgebraicSignature,
280    ) -> Self {
281        Self::additive_commutativity(
282            name,
283            origin,
284            signature.carrier.clone(),
285            signature.require_binary("add"),
286        )
287    }
288
289    /// Build a two-sided identity obligation for a binary operator symbol.
290    pub fn monoid_identity(
291        name: impl Into<String>,
292        origin: Origin,
293        carrier: Sort,
294        op: impl Into<String>,
295        identity: impl Into<String>,
296    ) -> Self {
297        let op = op.into();
298        let e = Term::var(identity);
299        let a = Term::var("a");
300        let left = Term::eq(Term::app(op.clone(), vec![e.clone(), a.clone()]), a.clone());
301        let right = Term::eq(Term::app(op, vec![a.clone(), e]), a);
302
303        Self::for_property::<IsMonoid>(
304            name,
305            origin,
306            VerificationTier::External,
307            Term::and(vec![left, right]),
308        )
309        .with_decl("a", carrier.clone())
310        .with_decl("e", carrier)
311    }
312
313    pub fn monoid_identity_in(
314        name: impl Into<String>,
315        origin: Origin,
316        signature: &AlgebraicSignature,
317    ) -> Self {
318        Self::monoid_identity(
319            name,
320            origin,
321            signature.carrier.clone(),
322            signature.require_binary("combine"),
323            signature.require_constant("identity"),
324        )
325    }
326
327    pub fn left_identity(
328        name: impl Into<String>,
329        origin: Origin,
330        carrier: Sort,
331        op: impl Into<String>,
332        identity: impl Into<String>,
333    ) -> Self {
334        let op = op.into();
335        let e = Term::var(identity);
336        let a = Term::var("a");
337        let conclusion = Term::eq(Term::app(op, vec![e, a.clone()]), a);
338
339        Self::for_property::<HasLeftIdentity>(name, origin, VerificationTier::External, conclusion)
340            .with_decl("a", carrier.clone())
341            .with_decl("e", carrier)
342    }
343
344    pub fn left_identity_in(
345        name: impl Into<String>,
346        origin: Origin,
347        signature: &AlgebraicSignature,
348        op_role: &str,
349        identity_role: &str,
350    ) -> Self {
351        Self::left_identity(
352            name,
353            origin,
354            signature.carrier.clone(),
355            signature.require_binary(op_role),
356            signature.require_constant(identity_role),
357        )
358    }
359
360    pub fn right_identity(
361        name: impl Into<String>,
362        origin: Origin,
363        carrier: Sort,
364        op: impl Into<String>,
365        identity: impl Into<String>,
366    ) -> Self {
367        let op = op.into();
368        let e = Term::var(identity);
369        let a = Term::var("a");
370        let conclusion = Term::eq(Term::app(op, vec![a.clone(), e]), a);
371
372        Self::for_property::<HasRightIdentity>(name, origin, VerificationTier::External, conclusion)
373            .with_decl("a", carrier.clone())
374            .with_decl("e", carrier)
375    }
376
377    pub fn right_identity_in(
378        name: impl Into<String>,
379        origin: Origin,
380        signature: &AlgebraicSignature,
381        op_role: &str,
382        identity_role: &str,
383    ) -> Self {
384        Self::right_identity(
385            name,
386            origin,
387            signature.carrier.clone(),
388            signature.require_binary(op_role),
389            signature.require_constant(identity_role),
390        )
391    }
392
393    pub fn left_inverse(
394        name: impl Into<String>,
395        origin: Origin,
396        carrier: Sort,
397        op: impl Into<String>,
398        inverse: impl Into<String>,
399        identity: impl Into<String>,
400    ) -> Self {
401        let op = op.into();
402        let inv = inverse.into();
403        let e = Term::var(identity);
404        let a = Term::var("a");
405        let conclusion = Term::eq(Term::app(op, vec![Term::app(inv, vec![a.clone()]), a]), e);
406
407        Self::for_property::<HasLeftInverse>(name, origin, VerificationTier::External, conclusion)
408            .with_decl("a", carrier.clone())
409            .with_decl("e", carrier)
410    }
411
412    pub fn left_inverse_in(
413        name: impl Into<String>,
414        origin: Origin,
415        signature: &AlgebraicSignature,
416    ) -> Self {
417        Self::left_inverse(
418            name,
419            origin,
420            signature.carrier.clone(),
421            signature.require_binary("combine"),
422            signature.require_unary("inverse"),
423            signature.require_constant("identity"),
424        )
425    }
426
427    pub fn right_inverse(
428        name: impl Into<String>,
429        origin: Origin,
430        carrier: Sort,
431        op: impl Into<String>,
432        inverse: impl Into<String>,
433        identity: impl Into<String>,
434    ) -> Self {
435        let op = op.into();
436        let inv = inverse.into();
437        let e = Term::var(identity);
438        let a = Term::var("a");
439        let conclusion = Term::eq(Term::app(op, vec![a.clone(), Term::app(inv, vec![a])]), e);
440
441        Self::for_property::<HasRightInverse>(name, origin, VerificationTier::External, conclusion)
442            .with_decl("a", carrier.clone())
443            .with_decl("e", carrier)
444    }
445
446    pub fn right_inverse_in(
447        name: impl Into<String>,
448        origin: Origin,
449        signature: &AlgebraicSignature,
450    ) -> Self {
451        Self::right_inverse(
452            name,
453            origin,
454            signature.carrier.clone(),
455            signature.require_binary("combine"),
456            signature.require_unary("inverse"),
457            signature.require_constant("identity"),
458        )
459    }
460
461    pub fn left_distributivity(
462        name: impl Into<String>,
463        origin: Origin,
464        carrier: Sort,
465        add: impl Into<String>,
466        mul: impl Into<String>,
467    ) -> Self {
468        let add = add.into();
469        let mul = mul.into();
470        let (a, b, c) = (Term::var("a"), Term::var("b"), Term::var("c"));
471        let left = Term::app(
472            mul.clone(),
473            vec![
474                a.clone(),
475                Term::app(add.clone(), vec![b.clone(), c.clone()]),
476            ],
477        );
478        let right = Term::app(
479            add,
480            vec![
481                Term::app(mul.clone(), vec![a.clone(), b]),
482                Term::app(mul, vec![a, c]),
483            ],
484        );
485
486        Self::for_property::<IsDistributive>(
487            name,
488            origin,
489            VerificationTier::External,
490            Term::eq(left, right),
491        )
492        .with_decl("a", carrier.clone())
493        .with_decl("b", carrier.clone())
494        .with_decl("c", carrier)
495    }
496
497    pub fn left_distributivity_in(
498        name: impl Into<String>,
499        origin: Origin,
500        signature: &AlgebraicSignature,
501    ) -> Self {
502        Self::left_distributivity(
503            name,
504            origin,
505            signature.carrier.clone(),
506            signature.require_binary("add"),
507            signature.require_binary("mul"),
508        )
509    }
510
511    pub fn right_distributivity(
512        name: impl Into<String>,
513        origin: Origin,
514        carrier: Sort,
515        add: impl Into<String>,
516        mul: impl Into<String>,
517    ) -> Self {
518        let add = add.into();
519        let mul = mul.into();
520        let (a, b, c) = (Term::var("a"), Term::var("b"), Term::var("c"));
521        let left = Term::app(
522            mul.clone(),
523            vec![
524                Term::app(add.clone(), vec![a.clone(), b.clone()]),
525                c.clone(),
526            ],
527        );
528        let right = Term::app(
529            add,
530            vec![
531                Term::app(mul.clone(), vec![a, c.clone()]),
532                Term::app(mul, vec![b, c]),
533            ],
534        );
535
536        Self::for_property::<IsDistributive>(
537            name,
538            origin,
539            VerificationTier::External,
540            Term::eq(left, right),
541        )
542        .with_decl("a", carrier.clone())
543        .with_decl("b", carrier.clone())
544        .with_decl("c", carrier)
545    }
546
547    pub fn right_distributivity_in(
548        name: impl Into<String>,
549        origin: Origin,
550        signature: &AlgebraicSignature,
551    ) -> Self {
552        Self::right_distributivity(
553            name,
554            origin,
555            signature.carrier.clone(),
556            signature.require_binary("add"),
557            signature.require_binary("mul"),
558        )
559    }
560
561    pub fn idempotency(
562        name: impl Into<String>,
563        origin: Origin,
564        carrier: Sort,
565        op: impl Into<String>,
566    ) -> Self {
567        let op = op.into();
568        let a = Term::var("a");
569        let conclusion = Term::eq(Term::app(op, vec![a.clone(), a.clone()]), a);
570
571        Self::for_property::<IsIdempotent>(name, origin, VerificationTier::External, conclusion)
572            .with_decl("a", carrier)
573    }
574
575    pub fn idempotency_in(
576        name: impl Into<String>,
577        origin: Origin,
578        signature: &AlgebraicSignature,
579        role: &str,
580    ) -> Self {
581        Self::idempotency(
582            name,
583            origin,
584            signature.carrier.clone(),
585            signature.require_binary(role),
586        )
587    }
588
589    pub fn absorption(
590        name: impl Into<String>,
591        origin: Origin,
592        carrier: Sort,
593        meet: impl Into<String>,
594        join: impl Into<String>,
595    ) -> Self {
596        let meet = meet.into();
597        let join = join.into();
598        let (a, b) = (Term::var("a"), Term::var("b"));
599        let left = Term::eq(
600            Term::app(
601                meet.clone(),
602                vec![
603                    a.clone(),
604                    Term::app(join.clone(), vec![a.clone(), b.clone()]),
605                ],
606            ),
607            a.clone(),
608        );
609        let right = Term::eq(
610            Term::app(join, vec![a.clone(), Term::app(meet, vec![a.clone(), b])]),
611            a,
612        );
613
614        Self::for_property::<IsAbsorptive>(
615            name,
616            origin,
617            VerificationTier::External,
618            Term::and(vec![left, right]),
619        )
620        .with_decl("a", carrier.clone())
621        .with_decl("b", carrier)
622    }
623
624    pub fn absorption_in(
625        name: impl Into<String>,
626        origin: Origin,
627        signature: &AlgebraicSignature,
628    ) -> Self {
629        Self::absorption(
630            name,
631            origin,
632            signature.carrier.clone(),
633            signature.require_binary("meet"),
634            signature.require_binary("join"),
635        )
636    }
637
638    /// Human-readable summary used in debugging and certificate generation.
639    pub fn summary(&self) -> String {
640        format!(
641            "{}::{} [{}]",
642            self.origin.crate_name, self.origin.item_path, self.property
643        )
644    }
645}
646
647#[cfg(test)]
648mod tests {
649    use super::*;
650    use crate::signature::AlgebraicSignature;
651
652    #[test]
653    fn associativity_builder_populates_metadata() {
654        let obligation = Obligation::associativity(
655            "option_add_assoc",
656            Origin::new("karpal-algebra", "Semigroup for Sum<i32>"),
657            Sort::Int,
658            "combine",
659        );
660
661        assert_eq!(obligation.property, IsAssociative::NAME);
662        assert_eq!(obligation.declarations.len(), 3);
663        assert!(obligation.summary().contains("associativity"));
664    }
665
666    #[test]
667    fn monoid_identity_builder_creates_conjunction() {
668        let obligation = Obligation::monoid_identity(
669            "sum_identity",
670            Origin::new("karpal-core", "Monoid for Sum<i32>"),
671            Sort::Int,
672            "combine",
673            "e",
674        );
675
676        assert_eq!(obligation.property, IsMonoid::NAME);
677        assert!(matches!(obligation.conclusion, Term::And(_)));
678    }
679
680    #[test]
681    fn signature_driven_group_builders_use_registered_roles() {
682        let sig = AlgebraicSignature::group(Sort::Int, "combine", "e", "inv");
683        let left = Obligation::left_inverse_in("left_inv", Origin::new("k", "G"), &sig);
684        let right = Obligation::right_inverse_in("right_inv", Origin::new("k", "G"), &sig);
685
686        assert_eq!(left.property, HasLeftInverse::NAME);
687        assert_eq!(right.property, HasRightInverse::NAME);
688    }
689
690    #[test]
691    fn lattice_absorption_creates_conjunction() {
692        let sig = AlgebraicSignature::lattice(Sort::Int, "meet", "join");
693        let obligation = Obligation::absorption_in("lattice_absorb", Origin::new("k", "L"), &sig);
694        assert_eq!(obligation.property, IsAbsorptive::NAME);
695        assert!(matches!(obligation.conclusion, Term::And(_)));
696    }
697}
karpal_verify/obligation.rs

karpal_verify/
obligation.rs
