creusot_std/logic/ops/
arithmetic.rs

1//! Arithmetic operators in logic
2
3use crate::prelude::*;
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    #[requires(false)]
15    fn add_logic(self, other: Rhs) -> Self::Output;
16}
17
18/// Trait for subtraction (`-`) in logic code.
19#[diagnostic::on_unimplemented(
20    message = "Cannot subtract `{Rhs}` from `{Self}` in logic",
21    label = "no implementation for `{Self} - {Rhs}` in logic"
22)]
23pub trait SubLogic<Rhs = Self> {
24    type Output;
25
26    #[logic]
27    #[requires(false)]
28    fn sub_logic(self, other: Rhs) -> Self::Output;
29}
30
31/// Trait for multiplication (`*`) in logic code.
32#[diagnostic::on_unimplemented(
33    message = "Cannot multiply `{Self}` by `{Rhs}` in logic",
34    label = "no implementation for `{Self} * {Rhs}` in logic"
35)]
36pub trait MulLogic<Rhs = Self> {
37    type Output;
38
39    #[logic]
40    #[requires(false)]
41    fn mul_logic(self, other: Rhs) -> Self::Output;
42}
43
44/// Trait for division (`/`) in logic code.
45#[diagnostic::on_unimplemented(
46    message = "Cannot divide `{Self}` by `{Rhs}` in logic",
47    label = "no implementation for `{Self} / {Rhs}` in logic"
48)]
49pub trait DivLogic<Rhs = Self> {
50    type Output;
51
52    #[logic]
53    #[requires(false)]
54    fn div_logic(self, other: Rhs) -> Self::Output;
55}
56
57/// Trait for remainder (`%`) in logic code.
58#[diagnostic::on_unimplemented(
59    message = "cannot calculate the remainder of `{Self}` divided by `{Rhs}` in logic",
60    label = "no implementation for `{Self} % {Rhs}` in logic"
61)]
62pub trait RemLogic<Rhs = Self> {
63    type Output;
64
65    #[logic]
66    #[requires(false)]
67    fn rem_logic(self, other: Rhs) -> Self::Output;
68}
69
70/// Trait for negation (unary `-`) in logic code.
71#[diagnostic::on_unimplemented(
72    message = "cannot apply unary operator `-` to type `{Self}`",
73    label = "cannot apply unary operator `-` in logic"
74)]
75pub trait NegLogic {
76    type Output;
77
78    #[logic]
79    #[requires(false)]
80    fn neg_logic(self) -> Self::Output;
81}
creusot_std/logic/ops/arithmetic.rs

creusot_std/logic/ops/
arithmetic.rs
