creusot_std/logic/ra/
nat.rs

1use crate::{
2    logic::{
3        Nat,
4        ra::{RA, UnitRA},
5    },
6    prelude::*,
7};
8
9impl RA for Nat {
10    #[logic(open, inline)]
11    fn op(self, other: Self) -> Option<Nat> {
12        Some(self + other)
13    }
14
15    #[logic(open, inline)]
16    #[ensures(match result {
17        Some(c) => factor.op(c) == Some(self),
18        None => forall<c: Self> factor.op(c) != Some(self),
19    })]
20    fn factor(self, factor: Self) -> Option<Self> {
21        let _ = Nat::ext_eq;
22        if self.to_int() >= factor.to_int() {
23            Some(Nat::new(self.to_int() - factor.to_int()))
24        } else {
25            None
26        }
27    }
28
29    #[logic(open, inline)]
30    #[ensures(result == (self == other))]
31    fn eq(self, other: Self) -> bool {
32        self.ext_eq(other)
33    }
34
35    #[logic(law)]
36    #[ensures(a.op(b) == b.op(a))]
37    fn commutative(a: Self, b: Self) {
38        let _ = Nat::ext_eq;
39    }
40
41    #[logic]
42    #[ensures(a.op(b).and_then_logic(|ab: Self| ab.op(c)) == b.op(c).and_then_logic(|bc| a.op(bc)))]
43    fn associative(a: Self, b: Self, c: Self) {
44        let _ = Nat::ext_eq;
45    }
46
47    #[logic(open, inline)]
48    fn core(self) -> Option<Self> {
49        Some(Nat::new(0))
50    }
51
52    #[logic]
53    #[ensures({
54        let c = self.core().unwrap_logic();
55        c.op(c) == Some(c)
56    })]
57    #[ensures(self.core().unwrap_logic().op(self) == Some(self))]
58    fn core_idemp(self) {
59        let _ = Nat::ext_eq;
60    }
61
62    #[logic]
63    #[requires(i.op(i) == Some(i))]
64    #[requires(i.op(self) == Some(self))]
65    #[ensures(match self.core() {
66        Some(c) => i.incl(c),
67        None => false,
68    })]
69    fn core_is_maximal_idemp(self, i: Self) {}
70}
71
72impl UnitRA for Nat {
73    #[logic(open, inline)]
74    #[ensures(forall<x: Self> #[trigger(x.op(result))] x.op(result) == Some(x))]
75    fn unit() -> Self {
76        let _ = Nat::ext_eq;
77        Nat::new(0)
78    }
79
80    #[logic(open, inline)]
81    #[ensures(self.core() == Some(result))]
82    fn core_total(self) -> Self {
83        Nat::new(0)
84    }
85
86    #[logic]
87    #[ensures(self.core_total().op(self.core_total()) == Some(self.core_total()))]
88    #[ensures(self.core_total().op(self) == Some(self))]
89    fn core_total_idemp(self) {
90        let _ = Nat::ext_eq;
91    }
92}
creusot_std/logic/ra/nat.rs

creusot_std/logic/ra/
nat.rs
