karpal_proof/
proven.rs

1// Copyright (C) 2026 Industrial Algebra
2// SPDX-License-Identifier: Apache-2.0
3
4use core::marker::PhantomData;
5
6use karpal_algebra::{
7    AbelianGroup, BoundedLattice, Field, Group, Lattice, Module, Ring, Semiring, VectorSpace,
8};
9use karpal_core::{Monoid, Semigroup};
10
11use crate::property::*;
12
13/// A value of type `T` accompanied by a compile-time witness
14/// that property `P` holds for `T`.
15///
16/// Construction is deliberately restricted: safe constructors
17/// require the relevant trait bound (e.g., `from_semigroup` requires
18/// `T: Semigroup`). The trait implementation *is* the proof.
19///
20/// For properties verified externally (proptest, SMT solver, inspection),
21/// use the unsafe [`Proven::axiom`] constructor.
22pub struct Proven<P, T> {
23    value: T,
24    _property: PhantomData<P>,
25}
26
27// Manual trait impls: P is phantom, so bounds should only apply to T.
28
29impl<P, T: core::fmt::Debug> core::fmt::Debug for Proven<P, T> {
30    fn fmt(&self, f: &mut core::fmt::Formatter<'_>) -> core::fmt::Result {
31        f.debug_struct("Proven")
32            .field("value", &self.value)
33            .finish()
34    }
35}
36
37impl<P, T: Clone> Clone for Proven<P, T> {
38    fn clone(&self) -> Self {
39        Proven {
40            value: self.value.clone(),
41            _property: PhantomData,
42        }
43    }
44}
45
46impl<P, T: Copy> Copy for Proven<P, T> {}
47
48impl<P, T: PartialEq> PartialEq for Proven<P, T> {
49    fn eq(&self, other: &Self) -> bool {
50        self.value == other.value
51    }
52}
53
54impl<P, T: Eq> Eq for Proven<P, T> {}
55
56impl<P, T: PartialOrd> PartialOrd for Proven<P, T> {
57    fn partial_cmp(&self, other: &Self) -> Option<core::cmp::Ordering> {
58        self.value.partial_cmp(&other.value)
59    }
60}
61
62impl<P, T: Ord> Ord for Proven<P, T> {
63    fn cmp(&self, other: &Self) -> core::cmp::Ordering {
64        self.value.cmp(&other.value)
65    }
66}
67
68impl<P, T: core::hash::Hash> core::hash::Hash for Proven<P, T> {
69    fn hash<H: core::hash::Hasher>(&self, state: &mut H) {
70        self.value.hash(state);
71    }
72}
73
74impl<P, T> Proven<P, T> {
75    /// Create a witness without checking.
76    ///
77    /// # Safety
78    ///
79    /// Caller asserts that property `P` genuinely holds for type `T`.
80    pub unsafe fn axiom(value: T) -> Self {
81        Proven {
82            value,
83            _property: PhantomData,
84        }
85    }
86
87    /// Access the inner value by reference.
88    pub fn value(&self) -> &T {
89        &self.value
90    }
91
92    /// Unwrap the witness, discarding the proof.
93    pub fn into_inner(self) -> T {
94        self.value
95    }
96
97    /// If property `P` implies property `Q`, derive a new witness.
98    pub fn derive<Q>(self) -> Proven<Q, T>
99    where
100        P: Implies<Q>,
101    {
102        Proven {
103            value: self.value,
104            _property: PhantomData,
105        }
106    }
107
108    /// Combine two independent proofs into a conjunction.
109    pub fn and<Q>(self, _other: Proven<Q, T>) -> Proven<And<P, Q>, T> {
110        Proven {
111            value: self.value,
112            _property: PhantomData,
113        }
114    }
115}
116
117impl<P, Q, T> Proven<And<P, Q>, T> {
118    /// Extract the second component from a conjunction proof.
119    ///
120    /// (The first component is available via `.derive()` since
121    /// `And<P, Q>: Implies<P>`.)
122    pub fn derive_second(self) -> Proven<Q, T> {
123        Proven {
124            value: self.value,
125            _property: PhantomData,
126        }
127    }
128}
129
130// ---------------------------------------------------------------------------
131// Safe constructors: trait bound IS the proof
132// ---------------------------------------------------------------------------
133
134impl<T: Semigroup> Proven<IsAssociative, T> {
135    /// Witness associativity from a `Semigroup` implementation.
136    pub fn from_semigroup(value: T) -> Self {
137        Proven {
138            value,
139            _property: PhantomData,
140        }
141    }
142}
143
144impl<T: Monoid> Proven<IsMonoid, T> {
145    /// Witness monoid laws from a `Monoid` implementation.
146    pub fn from_monoid(value: T) -> Self {
147        Proven {
148            value,
149            _property: PhantomData,
150        }
151    }
152}
153
154impl<T: Group> Proven<IsGroup, T> {
155    /// Witness group laws from a `Group` implementation.
156    pub fn from_group(value: T) -> Self {
157        Proven {
158            value,
159            _property: PhantomData,
160        }
161    }
162}
163
164impl<T: AbelianGroup> Proven<IsAbelianGroup, T> {
165    /// Witness abelian group from an `AbelianGroup` implementation.
166    pub fn from_abelian(value: T) -> Self {
167        Proven {
168            value,
169            _property: PhantomData,
170        }
171    }
172}
173
174impl<T: Semiring> Proven<IsSemiring, T> {
175    pub fn from_semiring(value: T) -> Self {
176        Proven {
177            value,
178            _property: PhantomData,
179        }
180    }
181}
182
183impl<T: Ring> Proven<IsRing, T> {
184    pub fn from_ring(value: T) -> Self {
185        Proven {
186            value,
187            _property: PhantomData,
188        }
189    }
190}
191
192impl<T: Field> Proven<IsField, T> {
193    pub fn from_field(value: T) -> Self {
194        Proven {
195            value,
196            _property: PhantomData,
197        }
198    }
199}
200
201impl<T: Lattice> Proven<IsLattice, T> {
202    pub fn from_lattice(value: T) -> Self {
203        Proven {
204            value,
205            _property: PhantomData,
206        }
207    }
208}
209
210impl<T: BoundedLattice> Proven<IsBoundedLattice, T> {
211    pub fn from_bounded_lattice(value: T) -> Self {
212        Proven {
213            value,
214            _property: PhantomData,
215        }
216    }
217}
218
219// ---------------------------------------------------------------------------
220// Trait forwarding: Proven<P, T> inherits T's algebraic structure
221// ---------------------------------------------------------------------------
222
223impl<P, T: Semigroup> Semigroup for Proven<P, T> {
224    fn combine(self, other: Self) -> Self {
225        Proven {
226            value: self.value.combine(other.value),
227            _property: PhantomData,
228        }
229    }
230}
231
232impl<P, T: Monoid> Monoid for Proven<P, T> {
233    fn empty() -> Self {
234        Proven {
235            value: T::empty(),
236            _property: PhantomData,
237        }
238    }
239}
240
241impl<P, T: Group> Group for Proven<P, T> {
242    fn invert(self) -> Self {
243        Proven {
244            value: self.value.invert(),
245            _property: PhantomData,
246        }
247    }
248}
249
250impl<P, T: AbelianGroup> AbelianGroup for Proven<P, T> {}
251
252impl<P, T: Lattice> Lattice for Proven<P, T> {
253    fn meet(self, other: Self) -> Self {
254        Proven {
255            value: self.value.meet(other.value),
256            _property: PhantomData,
257        }
258    }
259
260    fn join(self, other: Self) -> Self {
261        Proven {
262            value: self.value.join(other.value),
263            _property: PhantomData,
264        }
265    }
266}
267
268impl<P, T: BoundedLattice> BoundedLattice for Proven<P, T> {
269    fn top() -> Self {
270        Proven {
271            value: T::top(),
272            _property: PhantomData,
273        }
274    }
275
276    fn bottom() -> Self {
277        Proven {
278            value: T::bottom(),
279            _property: PhantomData,
280        }
281    }
282}
283
284impl<P, T: Semiring> Semiring for Proven<P, T> {
285    fn add(self, other: Self) -> Self {
286        Proven {
287            value: self.value.add(other.value),
288            _property: PhantomData,
289        }
290    }
291
292    fn mul(self, other: Self) -> Self {
293        Proven {
294            value: self.value.mul(other.value),
295            _property: PhantomData,
296        }
297    }
298
299    fn zero() -> Self {
300        Proven {
301            value: T::zero(),
302            _property: PhantomData,
303        }
304    }
305
306    fn one() -> Self {
307        Proven {
308            value: T::one(),
309            _property: PhantomData,
310        }
311    }
312}
313
314impl<P, T: Ring> Ring for Proven<P, T> {
315    fn negate(self) -> Self {
316        Proven {
317            value: self.value.negate(),
318            _property: PhantomData,
319        }
320    }
321}
322
323impl<P, T: Field> Field for Proven<P, T> {
324    fn reciprocal(self) -> Self {
325        Proven {
326            value: self.value.reciprocal(),
327            _property: PhantomData,
328        }
329    }
330}
331
332impl<P, R: Ring, T: Module<R>> Module<R> for Proven<P, T> {
333    fn scale(self, scalar: R) -> Self {
334        Proven {
335            value: self.value.scale(scalar),
336            _property: PhantomData,
337        }
338    }
339}
340
341impl<P, F: Field, T: VectorSpace<F>> VectorSpace<F> for Proven<P, T> {}
342
343#[cfg(test)]
344mod tests {
345    use super::*;
346
347    #[test]
348    fn from_semigroup_and_access() {
349        let p = Proven::<IsAssociative, i32>::from_semigroup(42);
350        assert_eq!(*p.value(), 42);
351        assert_eq!(p.into_inner(), 42);
352    }
353
354    #[test]
355    fn from_monoid() {
356        let p = Proven::<IsMonoid, i32>::from_monoid(10);
357        assert_eq!(*p.value(), 10);
358    }
359
360    #[test]
361    fn from_group() {
362        let p = Proven::<IsGroup, i32>::from_group(-5);
363        assert_eq!(*p.value(), -5);
364    }
365
366    #[test]
367    fn from_abelian() {
368        let p = Proven::<IsAbelianGroup, i32>::from_abelian(7);
369        assert_eq!(*p.value(), 7);
370    }
371
372    #[test]
373    fn derive_weaker_property() {
374        let group_proof = Proven::<IsGroup, i32>::from_group(3);
375        let monoid_proof: Proven<IsMonoid, i32> = group_proof.derive();
376        assert_eq!(*monoid_proof.value(), 3);
377
378        let assoc_proof: Proven<IsAssociative, i32> = monoid_proof.derive();
379        assert_eq!(*assoc_proof.value(), 3);
380    }
381
382    #[test]
383    fn derive_abelian_chain() {
384        let abelian = Proven::<IsAbelianGroup, i32>::from_abelian(5);
385        let _commutative: Proven<IsCommutative, i32> = abelian.derive();
386    }
387
388    #[test]
389    fn and_conjunction() {
390        let assoc = Proven::<IsAssociative, i32>::from_semigroup(1);
391        // Safety: i32 addition is commutative (verified by proptest elsewhere)
392        let comm: Proven<IsCommutative, i32> = unsafe { Proven::axiom(1) };
393        let both = assoc.and(comm);
394        let _: Proven<IsAssociative, i32> = both.derive();
395    }
396
397    #[test]
398    fn semigroup_forwarding() {
399        let a = Proven::<IsAssociative, i32>::from_semigroup(3);
400        let b = Proven::<IsAssociative, i32>::from_semigroup(4);
401        let c = a.combine(b);
402        assert_eq!(*c.value(), 7);
403    }
404
405    #[test]
406    fn monoid_forwarding() {
407        let e = Proven::<IsMonoid, i32>::empty();
408        assert_eq!(*e.value(), 0);
409    }
410
411    #[test]
412    fn group_forwarding() {
413        let p = Proven::<IsGroup, i32>::from_group(5);
414        let inv = p.invert();
415        assert_eq!(*inv.value(), -5);
416    }
417
418    #[test]
419    fn lattice_forwarding() {
420        let a = Proven::<IsLattice, bool>::from_lattice(true);
421        let b = Proven::<IsLattice, bool>::from_lattice(false);
422        assert_eq!(*a.meet(b).value(), false);
423    }
424
425    #[test]
426    fn semiring_forwarding() {
427        let a = Proven::<IsSemiring, i32>::from_semiring(3);
428        let b = Proven::<IsSemiring, i32>::from_semiring(4);
429        assert_eq!(*a.add(b).value(), 7);
430    }
431
432    #[test]
433    fn ring_forwarding() {
434        let a = Proven::<IsRing, i32>::from_ring(5);
435        assert_eq!(*a.negate().value(), -5);
436    }
437
438    #[test]
439    fn field_forwarding() {
440        let a = Proven::<IsField, f64>::from_field(4.0);
441        let r = a.reciprocal();
442        assert!((r.value() - 0.25).abs() < 1e-10);
443    }
444
445    #[test]
446    fn unsafe_axiom() {
447        let p: Proven<IsCommutative, i32> = unsafe { Proven::axiom(42) };
448        assert_eq!(*p.value(), 42);
449    }
450
451    #[test]
452    fn from_semiring() {
453        let p = Proven::<IsSemiring, i32>::from_semiring(10);
454        assert_eq!(*p.value(), 10);
455    }
456
457    #[test]
458    fn from_ring() {
459        let p = Proven::<IsRing, i32>::from_ring(10);
460        assert_eq!(*p.value(), 10);
461    }
462
463    #[test]
464    fn from_field() {
465        let p = Proven::<IsField, f64>::from_field(2.5);
466        assert!((p.value() - 2.5).abs() < 1e-10);
467    }
468
469    #[test]
470    fn from_lattice() {
471        let p = Proven::<IsLattice, bool>::from_lattice(true);
472        assert_eq!(*p.value(), true);
473    }
474
475    #[test]
476    fn from_bounded_lattice() {
477        let p = Proven::<IsBoundedLattice, bool>::from_bounded_lattice(false);
478        assert_eq!(*p.value(), false);
479    }
480
481    #[test]
482    fn derive_second_from_and() {
483        let assoc = Proven::<IsAssociative, i32>::from_semigroup(10);
484        let comm: Proven<IsCommutative, i32> = unsafe { Proven::axiom(10) };
485        let both = assoc.and(comm);
486        let extracted: Proven<IsCommutative, i32> = both.derive_second();
487        assert_eq!(*extracted.value(), 10);
488    }
489
490    #[test]
491    fn proven_preserves_equality() {
492        let a = Proven::<IsMonoid, i32>::from_monoid(5);
493        let b = Proven::<IsMonoid, i32>::from_monoid(5);
494        let c = Proven::<IsMonoid, i32>::from_monoid(6);
495        assert_eq!(a, b);
496        assert_ne!(a, c);
497    }
498
499    #[test]
500    fn proven_preserves_ordering() {
501        let a = Proven::<IsMonoid, i32>::from_monoid(3);
502        let b = Proven::<IsMonoid, i32>::from_monoid(5);
503        assert!(a < b);
504    }
505}
506
507#[cfg(test)]
508mod law_tests {
509    use super::*;
510    use crate::law_check;
511    use proptest::prelude::*;
512
513    proptest! {
514        #[test]
515        fn proven_semigroup_associativity(a in -100i16..100i16, b in -100i16..100i16, c in -100i16..100i16) {
516            let pa = Proven::<IsAssociative, i16>::from_semigroup(a);
517            let pb = Proven::<IsAssociative, i16>::from_semigroup(b);
518            let pc = Proven::<IsAssociative, i16>::from_semigroup(c);
519            let left = pa.combine(pb).combine(pc);
520            let pa2 = Proven::<IsAssociative, i16>::from_semigroup(a);
521            let pb2 = Proven::<IsAssociative, i16>::from_semigroup(b);
522            let pc2 = Proven::<IsAssociative, i16>::from_semigroup(c);
523            let right = pa2.combine(pb2.combine(pc2));
524            prop_assert_eq!(left, right);
525        }
526
527        #[test]
528        fn proven_monoid_identity(a in -100i16..100i16) {
529            let pa = Proven::<IsMonoid, i16>::from_monoid(a);
530            let e = Proven::<IsMonoid, i16>::empty();
531            prop_assert_eq!(pa.combine(e), Proven::from_monoid(a));
532            let pa2 = Proven::<IsMonoid, i16>::from_monoid(a);
533            let e2 = Proven::<IsMonoid, i16>::empty();
534            prop_assert_eq!(e2.combine(pa2), Proven::from_monoid(a));
535        }
536
537        #[test]
538        fn proven_group_inverse(a in -100i16..100i16) {
539            let pa = Proven::<IsGroup, i16>::from_group(a);
540            let inv = pa.clone().invert();
541            let result = pa.combine(inv);
542            prop_assert_eq!(result, Proven::from_group(0));
543        }
544
545        #[test]
546        fn law_check_semigroup_via_trait(a in -100i16..100i16, b in -100i16..100i16, c in -100i16..100i16) {
547            law_check::check_associativity(
548                a, b, c,
549                |x, y| x.wrapping_add(y),
550            ).unwrap();
551        }
552
553        #[test]
554        fn law_check_commutativity_i16(a in -100i16..100i16, b in -100i16..100i16) {
555            law_check::check_commutativity(
556                a, b,
557                |x, y| x.wrapping_add(y),
558            ).unwrap();
559        }
560
561        #[test]
562        fn law_check_inverse_i16(a in -100i16..100i16) {
563            law_check::check_left_inverse(a, 0i16, |x, y| x.wrapping_add(y), |x| x.wrapping_neg()).unwrap();
564            law_check::check_right_inverse(a, 0i16, |x, y| x.wrapping_add(y), |x| x.wrapping_neg()).unwrap();
565        }
566
567        #[test]
568        fn law_check_distributivity_i16(a in -50i16..50i16, b in -50i16..50i16, c in -50i16..50i16) {
569            law_check::check_left_distributivity(
570                a, b, c,
571                |x, y| x.wrapping_add(y),
572                |x, y| x.wrapping_mul(y),
573            ).unwrap();
574        }
575    }
576}
karpal_proof/proven.rs

karpal_proof/
proven.rs
