vstd_extra/
spec_operators.rs

1use vstd::prelude::*;
2
3verus! {
4
5pub trait SpecAddTrait<Rhs = Self> {
6    type Output;
7
8    spec fn spec_add(self, rhs: Rhs) -> Self::Output;
9}
10
11pub trait SpecSubTrait<Rhs = Self> {
12    type Output;
13
14    spec fn spec_sub(self, rhs: Rhs) -> Self::Output;
15}
16
17pub trait SpecMulTrait<Rhs = Self> {
18    type Output;
19
20    spec fn spec_mul(self, rhs: Rhs) -> Self::Output;
21}
22
23pub trait SpecShlTrait<Rhs = Self> {
24    type Output;
25
26    spec fn spec_shl(self, rhs: Rhs) -> Self::Output;
27}
28
29pub trait SpecShrTrait<Rhs = Self> {
30    type Output;
31
32    spec fn spec_shr(self, rhs: Rhs) -> Self::Output;
33}
34
35pub trait SpecBitAndTrait<Rhs = Self> {
36    type Output;
37
38    spec fn spec_bitand(self, rhs: Rhs) -> Self::Output;
39}
40
41pub trait SpecBitOrTrait<Rhs = Self> {
42    type Output;
43
44    spec fn spec_bitor(self, rhs: Rhs) -> Self::Output;
45}
46
47pub trait SpecBitXorTrait<Rhs = Self> {
48    type Output;
49
50    spec fn spec_bitxor(self, rhs: Rhs) -> Self::Output;
51}
52
53pub trait SpecNegTrait {
54    type Output;
55
56    spec fn spec_neg(self) -> Self::Output;
57}
58
59} // verus!
vstd_extra/spec_operators.rs

vstd_extra/
spec_operators.rs
