creusot_std/logic/ra/
positive.rs

1use crate::{
2    logic::{int::Positive, ra::RA},
3    prelude::*,
4};
5
6impl RA for Positive {
7    #[logic(open)]
8    fn op(self, other: Self) -> Option<Self> {
9        Some(self + other)
10    }
11
12    #[logic]
13    #[ensures(match result {
14        Some(c) => factor.op(c) == Some(self),
15        None => forall<c: Self> factor.op(c) != Some(self),
16    })]
17    fn factor(self, factor: Self) -> Option<Self> {
18        if self > factor { Some(Self::new(self.view() - factor.view())) } else { None }
19    }
20
21    #[logic(law)]
22    #[ensures(a.op(b) == b.op(a))]
23    fn commutative(a: Self, b: Self) {
24        let _ = Self::ext_eq;
25    }
26
27    #[logic]
28    #[ensures(a.op(b).and_then_logic(|ab: Self| ab.op(c)) == b.op(c).and_then_logic(|bc| a.op(bc)))]
29    fn associative(a: Self, b: Self, c: Self) {
30        let _ = Self::ext_eq;
31    }
32
33    #[logic(open)]
34    fn core(self) -> Option<Self> {
35        None
36    }
37
38    #[logic]
39    #[requires(self.core() != None)]
40    #[ensures({
41        let c = self.core().unwrap_logic();
42        c.op(c) == Some(c)
43    })]
44    #[ensures(self.core().unwrap_logic().op(self) == Some(self))]
45    fn core_idemp(self) {}
46
47    #[logic]
48    #[requires(i.op(i) == Some(i))]
49    #[requires(i.op(self) == Some(self))]
50    #[ensures(match self.core() {
51        Some(c) => i.incl(c),
52        None => false,
53    })]
54    fn core_is_maximal_idemp(self, i: Self) {}
55
56    #[logic(open)]
57    #[ensures(result == (forall<x, y> self.op(x) != None ==>
58        self.op(x) == self.op(y) ==> x == y))]
59    fn cancelable(self) -> bool {
60        let _ = Self::ext_eq;
61        true
62    }
63}
creusot_std/logic/ra/positive.rs

creusot_std/logic/ra/
positive.rs
