karpal_verify/
obligation.rs

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

karpal_verify/
obligation.rs
