creusot_std/logic/
ops.rs

1use crate::prelude::*;
2use core::ops::{Deref, DerefMut};
3mod arithmetic;
4
5pub use arithmetic::{AddLogic, DivLogic, MulLogic, NegLogic, RemLogic, SubLogic};
6
7/// Used for indexing operations (`container[index]`) in pearlite.
8#[diagnostic::on_unimplemented(
9    message = "the type `{Self}` cannot be indexed by `{I}` in logic",
10    label = "`{Self}` cannot be indexed by `{I}` in logic"
11)]
12pub trait IndexLogic<I: ?Sized> {
13    type Item;
14
15    /// Performs the indexing (`container[index]`) operation.
16    #[logic]
17    #[requires(false)]
18    #[intrinsic("index_logic")]
19    fn index_logic(self, idx: I) -> Self::Item;
20}
21
22pub trait Fin {
23    type Target: ?Sized;
24
25    /// Allows overloading of the `^` operator.
26    #[logic(prophetic)]
27    fn fin<'a>(self) -> &'a Self::Target;
28}
29
30impl<T: ?Sized> Fin for &mut T {
31    type Target = T;
32
33    #[logic(prophetic)]
34    #[builtin("fin")]
35    fn fin<'a>(self) -> &'a T {
36        dead
37    }
38}
39
40/// Trait for left shift (`<<`) in logic code.
41#[diagnostic::on_unimplemented(message = "no implementation for `{Self} << {Rhs}` in logic")]
42pub trait ShlLogic<Rhs = Self> {
43    type Output;
44
45    #[logic]
46    #[requires(false)]
47    fn shl_logic(self, other: Rhs) -> Self::Output;
48}
49
50/// Trait for right shift (`>>`) in logic code.
51#[diagnostic::on_unimplemented(message = "no implementation for `{Self} >> {Rhs}` in logic")]
52pub trait ShrLogic<Rhs = Self> {
53    type Output;
54
55    #[logic]
56    #[requires(false)]
57    fn shr_logic(self, other: Rhs) -> Self::Output;
58}
59
60/// Trait for bitwise AND (`&`) in logic code.
61#[diagnostic::on_unimplemented(message = "no implementation for `{Self} & {Rhs}` in logic")]
62pub trait BitAndLogic<Rhs = Self> {
63    type Output;
64
65    #[logic]
66    #[requires(false)]
67    fn bitand_logic(self, other: Rhs) -> Self::Output;
68}
69
70impl BitAndLogic for bool {
71    type Output = bool;
72
73    #[logic(open, inline)]
74    fn bitand_logic(self, other: bool) -> Self::Output {
75        self && other
76    }
77}
78
79/// Trait for bitwise OR (`|`) in logic code.
80#[diagnostic::on_unimplemented(message = "no implementation for `{Self} | {Rhs}` in logic")]
81pub trait BitOrLogic<Rhs = Self> {
82    type Output;
83
84    #[logic]
85    #[requires(false)]
86    fn bitor_logic(self, other: Rhs) -> Self::Output;
87}
88
89impl BitOrLogic for bool {
90    type Output = bool;
91
92    #[logic(open, inline)]
93    fn bitor_logic(self, other: bool) -> Self::Output {
94        self || other
95    }
96}
97
98/// Trait for bitwise XOR (`^`) in logic code.
99#[diagnostic::on_unimplemented(message = "no implementation for `{Self} ^ {Rhs}` in logic")]
100pub trait BitXorLogic<Rhs = Self> {
101    type Output;
102
103    #[logic]
104    #[requires(false)]
105    fn bitxor_logic(self, other: Rhs) -> Self::Output;
106}
107
108impl BitXorLogic for bool {
109    type Output = bool;
110
111    #[logic(open, inline)]
112    fn bitxor_logic(self, other: bool) -> Self::Output {
113        self != other
114    }
115}
116
117/// Trait for negation operator (`!`) in logic code.
118#[diagnostic::on_unimplemented(message = "no implementation for `!{Self}` in logic")]
119pub trait NotLogic {
120    type Output;
121
122    #[logic]
123    #[requires(false)]
124    fn not_logic(self) -> Self::Output;
125}
126
127impl NotLogic for bool {
128    type Output = bool;
129
130    #[logic]
131    #[builtin("bool.Bool.notb")]
132    fn not_logic(self) -> Self::Output {
133        dead
134    }
135}
136
137/// Trait for dereference in logic.
138///
139/// Implementing this trait does _not_ automatically unlock dereference syntax
140/// (`&*x`); you also need to have a _logical alias_:
141/// ```
142/// use creusot_std::{logic::ops::DerefLogic, prelude::*};
143/// use std::ops::Deref;
144///
145/// struct MyInt(Int);
146///
147/// impl DerefLogic for MyInt {
148///     #[logic]
149///     fn deref_logic(&self) -> &Self::Target {
150///         &self.0
151///     }
152/// }
153///
154/// impl Deref for MyInt {
155///     type Target = Int;
156///     #[check(ghost)]
157///     #[logic_alias(self.deref_logic())]
158///     fn deref(&self) -> &Self::Target {
159///         &self.0
160///     }
161/// }
162///
163/// #[requires(*x == 1int)]
164/// fn foo(x: MyInt) {}
165/// ```
166pub trait DerefLogic: Deref {
167    #[logic]
168    fn deref_logic(&self) -> &Self::Target;
169}
170
171/// Same as [`DerefLogic`], but for mutable borrows.
172pub trait DerefMutLogic: DerefMut + DerefLogic {
173    #[logic]
174    fn deref_mut_logic(&mut self) -> &mut Self::Target;
175}
creusot_std/logic/ops.rs

creusot_std/logic/
ops.rs
