karpal_proof/
proven.rs

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

karpal_proof/
proven.rs
