creusot_contracts/logic/
real.rs

1//! Real numbers
2use crate::prelude::*;
3#[cfg(creusot)]
4use num_rational::BigRational;
5use std::{cmp::Ordering, marker::PhantomData};
6
7#[builtin("real.Real.real")]
8pub struct Real(PhantomData<*mut ()>);
9
10#[cfg(creusot)]
11impl DeepModel for BigRational {
12    type DeepModelTy = Real;
13
14    #[logic(opaque)]
15    fn deep_model(self) -> Self::DeepModelTy {
16        dead
17    }
18}
19
20impl Real {
21    #[logic(opaque)]
22    pub fn from_int(_: Int) -> Self {
23        dead
24    }
25}
26
27impl OrdLogic for Real {
28    #[logic(open)]
29    fn cmp_log(self, o: Self) -> Ordering {
30        if self < o {
31            Ordering::Less
32        } else if self == o {
33            Ordering::Equal
34        } else {
35            Ordering::Greater
36        }
37    }
38
39    #[logic]
40    #[builtin("real.Real.(<=)")]
41    fn le_log(self, _: Self) -> bool {
42        true
43    }
44
45    #[logic]
46    #[builtin("real.Real.(<)")]
47    fn lt_log(self, _: Self) -> bool {
48        true
49    }
50
51    #[logic]
52    #[builtin("real.Real.(>=)")]
53    fn ge_log(self, _: Self) -> bool {
54        true
55    }
56
57    #[logic]
58    #[builtin("real.Real.(>)")]
59    fn gt_log(self, _: Self) -> bool {
60        true
61    }
62
63    crate::logic::ord::ord_laws_impl! {}
64}
creusot_contracts/logic/real.rs

creusot_contracts/logic/
real.rs
