creusot_contracts/logic/
ops.rs

1use crate::prelude::*;
2mod arithmetic;
3
4pub use arithmetic::{AddLogic, DivLogic, MulLogic, NegLogic, NthBitLogic, RemLogic, SubLogic};
5
6/// Used for indexing operations (`container[index]`) in pearlite.
7#[diagnostic::on_unimplemented(
8    message = "the type `{Self}` cannot be indexed by `{I}` in logic",
9    label = "`{Self}` cannot be indexed by `{I}` in logic"
10)]
11pub trait IndexLogic<I: ?Sized> {
12    type Item;
13
14    /// Performs the indexing (`container[index]`) operation.
15    #[logic]
16    #[intrinsic("index_logic")]
17    fn index_logic(self, idx: I) -> Self::Item;
18}
19
20pub trait Fin {
21    type Target: ?Sized;
22
23    /// Allows overloading of the `^` operator.
24    #[logic(prophetic)]
25    fn fin<'a>(self) -> &'a Self::Target;
26}
27
28impl<T: ?Sized> Fin for &mut T {
29    type Target = T;
30
31    #[logic(prophetic)]
32    #[builtin("fin")]
33    fn fin<'a>(self) -> &'a T {
34        dead
35    }
36}
creusot_contracts/logic/ops.rs

creusot_contracts/logic/
ops.rs
