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)]
13    #[ensures(result == (exists<factor> self.op(factor) == Some(other)))]
14    fn incl(self, other: Self) -> bool {
15        let _ = Self::ext_eq;
16        let r = self.to_real() < other.to_real();
17        proof_assert!(r ==> self.op(Self::new(other.to_real() - self.to_real())) == Some(other));
18        r
19    }
20
21    #[logic(open, inline)]
22    #[ensures(#[trigger(self == other)] result == (self == other))]
23    fn eq(self, other: Self) -> bool {
24        self.ext_eq(other)
25    }
26
27    #[logic(law)]
28    #[ensures(a.op(b) == b.op(a))]
29    fn commutative(a: Self, b: Self) {
30        let _ = PositiveReal::ext_eq;
31    }
32
33    #[logic]
34    #[ensures(a.op(b).and_then_logic(|ab: Self| ab.op(c)) == b.op(c).and_then_logic(|bc| a.op(bc)))]
35    fn associative(a: Self, b: Self, c: Self) {
36        let _ = PositiveReal::ext_eq;
37
38        let ab = a.op(b).unwrap_logic();
39        let bc = b.op(c).unwrap_logic();
40        let ab_c = ab.op(c).unwrap_logic();
41        let a_bc = a.op(bc).unwrap_logic();
42        proof_assert!(ab_c == a_bc)
43    }
44
45    #[logic(open, inline)]
46    fn core(self) -> Option<Self> {
47        None
48    }
49
50    #[logic]
51    #[requires(self.core() != None)]
52    #[ensures({
53        let c = self.core().unwrap_logic();
54        c.op(c) == Some(c)
55    })]
56    #[ensures(self.core().unwrap_logic().op(self) == Some(self))]
57    fn core_idemp(self) {}
58
59    #[logic]
60    #[requires(i.op(i) == Some(i))]
61    #[requires(i.op(self) == Some(self))]
62    #[ensures(match self.core() {
63        Some(c) => i.incl(c),
64        None => false,
65    })]
66    fn core_is_maximal_idemp(self, i: Self) {}
67
68    #[logic(open)]
69    #[ensures(result == (forall<x, y> self.op(x) != None ==>
70        self.op(x) == self.op(y) ==> x == y))]
71    fn cancelable(self) -> bool {
72        let _ = PositiveReal::ext_eq;
73        true
74    }
75}
creusot_std/logic/ra/positive_real.rs

creusot_std/logic/ra/
positive_real.rs
