creusot_std/logic/ra/
positive_real.rs

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

creusot_std/logic/ra/
positive_real.rs
