karpal_verify/
bundle.rs

1#[cfg(not(feature = "std"))]
2use alloc::{string::String, vec::Vec};
3#[cfg(feature = "std")]
4use std::{string::String, vec::Vec};
5
6use crate::{AlgebraicSignature, Obligation, Origin};
7
8/// Named collection of related proof obligations.
9#[derive(Debug, Clone, PartialEq, Eq)]
10pub struct ObligationBundle {
11    pub name: String,
12    pub origin: Origin,
13    obligations: Vec<Obligation>,
14}
15
16impl ObligationBundle {
17    pub fn new(name: impl Into<String>, origin: Origin) -> Self {
18        Self {
19            name: name.into(),
20            origin,
21            obligations: Vec::new(),
22        }
23    }
24
25    pub fn with(mut self, obligation: Obligation) -> Self {
26        self.obligations.push(obligation);
27        self
28    }
29
30    pub fn push(&mut self, obligation: Obligation) {
31        self.obligations.push(obligation);
32    }
33
34    pub fn obligations(&self) -> &[Obligation] {
35        &self.obligations
36    }
37
38    pub fn into_obligations(self) -> Vec<Obligation> {
39        self.obligations
40    }
41
42    pub fn semigroup(
43        name: impl Into<String>,
44        origin: Origin,
45        signature: &AlgebraicSignature,
46    ) -> Self {
47        Self::new(name, origin.clone()).with(Obligation::associativity_in(
48            "associativity",
49            origin,
50            signature,
51            "combine",
52        ))
53    }
54
55    pub fn monoid(name: impl Into<String>, origin: Origin, signature: &AlgebraicSignature) -> Self {
56        Self::new(name, origin.clone())
57            .with(Obligation::associativity_in(
58                "associativity",
59                origin.clone(),
60                signature,
61                "combine",
62            ))
63            .with(Obligation::left_identity_in(
64                "left_identity",
65                origin.clone(),
66                signature,
67                "combine",
68                "identity",
69            ))
70            .with(Obligation::right_identity_in(
71                "right_identity",
72                origin,
73                signature,
74                "combine",
75                "identity",
76            ))
77    }
78
79    pub fn group(name: impl Into<String>, origin: Origin, signature: &AlgebraicSignature) -> Self {
80        Self::monoid(name, origin.clone(), signature)
81            .with(Obligation::left_inverse_in(
82                "left_inverse",
83                origin.clone(),
84                signature,
85            ))
86            .with(Obligation::right_inverse_in(
87                "right_inverse",
88                origin,
89                signature,
90            ))
91    }
92
93    pub fn semiring(
94        name: impl Into<String>,
95        origin: Origin,
96        signature: &AlgebraicSignature,
97    ) -> Self {
98        Self::new(name, origin.clone())
99            .with(Obligation::associativity_in(
100                "add_associativity",
101                origin.clone(),
102                signature,
103                "add",
104            ))
105            .with(Obligation::associativity_in(
106                "mul_associativity",
107                origin.clone(),
108                signature,
109                "mul",
110            ))
111            .with(Obligation::additive_commutativity_in(
112                "add_commutativity",
113                origin.clone(),
114                signature,
115            ))
116            .with(Obligation::left_identity_in(
117                "add_left_identity",
118                origin.clone(),
119                signature,
120                "add",
121                "zero",
122            ))
123            .with(Obligation::right_identity_in(
124                "add_right_identity",
125                origin.clone(),
126                signature,
127                "add",
128                "zero",
129            ))
130            .with(Obligation::left_identity_in(
131                "mul_left_identity",
132                origin.clone(),
133                signature,
134                "mul",
135                "one",
136            ))
137            .with(Obligation::right_identity_in(
138                "mul_right_identity",
139                origin.clone(),
140                signature,
141                "mul",
142                "one",
143            ))
144            .with(Obligation::left_distributivity_in(
145                "left_distributivity",
146                origin.clone(),
147                signature,
148            ))
149            .with(Obligation::right_distributivity_in(
150                "right_distributivity",
151                origin,
152                signature,
153            ))
154    }
155
156    pub fn lattice(
157        name: impl Into<String>,
158        origin: Origin,
159        signature: &AlgebraicSignature,
160    ) -> Self {
161        Self::new(name, origin.clone())
162            .with(Obligation::associativity_in(
163                "meet_associativity",
164                origin.clone(),
165                signature,
166                "meet",
167            ))
168            .with(Obligation::associativity_in(
169                "join_associativity",
170                origin.clone(),
171                signature,
172                "join",
173            ))
174            .with(Obligation::commutativity_in(
175                "meet_commutativity",
176                origin.clone(),
177                signature,
178                "meet",
179            ))
180            .with(Obligation::commutativity_in(
181                "join_commutativity",
182                origin.clone(),
183                signature,
184                "join",
185            ))
186            .with(Obligation::idempotency_in(
187                "meet_idempotency",
188                origin.clone(),
189                signature,
190                "meet",
191            ))
192            .with(Obligation::idempotency_in(
193                "join_idempotency",
194                origin.clone(),
195                signature,
196                "join",
197            ))
198            .with(Obligation::absorption_in("absorption", origin, signature))
199    }
200}
201
202#[cfg(test)]
203mod tests {
204    use super::*;
205    use crate::Sort;
206
207    #[test]
208    fn monoid_bundle_contains_expected_laws() {
209        let sig = AlgebraicSignature::monoid(Sort::Int, "combine", "e");
210        let bundle = ObligationBundle::monoid("sum", Origin::new("karpal-core", "Sum<i32>"), &sig);
211        assert_eq!(bundle.obligations().len(), 3);
212    }
213
214    #[test]
215    fn semiring_bundle_contains_expected_laws() {
216        let sig = AlgebraicSignature::semiring(Sort::Int, "add", "mul", "zero", "one");
217        let bundle = ObligationBundle::semiring("ring", Origin::new("karpal-algebra", "i32"), &sig);
218        assert_eq!(bundle.obligations().len(), 9);
219    }
220}
karpal_verify/bundle.rs

karpal_verify/
bundle.rs
