creusot_contracts/logic/ops/
arithmetic.rs

1//! Arithmetic operators in logic
2
3use crate::*;
4
5/// Trait for addition (`+`) in logic code.
6#[diagnostic::on_unimplemented(
7    message = "Cannot add `{Rhs}` to `{Self}` in logic",
8    label = "no implementation for `{Self} + {Rhs}` in logic"
9)]
10pub trait AddLogic<Rhs = Self> {
11    type Output;
12
13    #[logic]
14    fn add(self, other: Rhs) -> Self::Output;
15}
16
17/// Trait for subtraction (`-`) in logic code.
18#[diagnostic::on_unimplemented(
19    message = "Cannot subtract `{Rhs}` from `{Self}` in logic",
20    label = "no implementation for `{Self} - {Rhs}` in logic"
21)]
22pub trait SubLogic<Rhs = Self> {
23    type Output;
24
25    #[logic]
26    fn sub(self, other: Rhs) -> Self::Output;
27}
28
29/// Trait for multiplication (`*`) in logic code.
30#[diagnostic::on_unimplemented(
31    message = "Cannot multiply `{Self}` by `{Rhs}` in logic",
32    label = "no implementation for `{Self} * {Rhs}` in logic"
33)]
34pub trait MulLogic<Rhs = Self> {
35    type Output;
36
37    #[logic]
38    fn mul(self, other: Rhs) -> Self::Output;
39}
40
41/// Trait for division (`/`) in logic code.
42#[diagnostic::on_unimplemented(
43    message = "Cannot divide `{Self}` by `{Rhs}` in logic",
44    label = "no implementation for `{Self} / {Rhs}` in logic"
45)]
46pub trait DivLogic<Rhs = Self> {
47    type Output;
48
49    #[logic]
50    fn div(self, other: Rhs) -> Self::Output;
51}
52
53/// Trait for remainder (`%`) in logic code.
54#[diagnostic::on_unimplemented(
55    message = "cannot calculate the remainder of `{Self}` divided by `{Rhs}` in logic",
56    label = "no implementation for `{Self} % {Rhs}` in logic"
57)]
58pub trait RemLogic<Rhs = Self> {
59    type Output;
60
61    #[logic]
62    fn rem(self, other: Rhs) -> Self::Output;
63}
64
65/// Trait for negation (unary `-`) in logic code.
66#[diagnostic::on_unimplemented(
67    message = "cannot apply unary operator `-` to type `{Self}`",
68    label = "cannot apply unary operator `-` in logic"
69)]
70pub trait NegLogic {
71    type Output;
72
73    #[logic]
74    fn neg(self) -> Self::Output;
75}
76
77/// Trait for the nth bit of a bitvector in logic code.
78pub trait NthBitLogic {
79    /// The nth bit of a bitvector.
80    /// In [`bitwise_proof`] mode, this is translated to [`nth`](https://www.why3.org/stdlib/bv.html#nth_188) in Why3.
81    /// Otherwise this is an abstract function.
82    #[logic]
83    fn nth_bit(self, n: Int) -> bool;
84}
creusot_contracts/logic/ops/arithmetic.rs

creusot_contracts/logic/ops/
arithmetic.rs
