Trait ExecSpecFixedWidthArith 

pub trait ExecSpecFixedWidthArith: Sized {
    // Required methods
    spec fn spec_fixed_add(self, rhs: Self) -> Self;
    spec fn spec_fixed_sub(self, rhs: Self) -> Self;
    spec fn spec_fixed_mul(self, rhs: Self) -> Self;
    exec fn exec_fixed_add(self, rhs: Self) -> res : Self;
    exec fn exec_fixed_sub(self, rhs: Self) -> res : Self;
    exec fn exec_fixed_mul(self, rhs: Self) -> res : Self;
}

Required Methods

spec fn spec_fixed_add(self, rhs: Self) -> Self

spec fn spec_fixed_sub(self, rhs: Self) -> Self

spec fn spec_fixed_mul(self, rhs: Self) -> Self

exec fn exec_fixed_add(self, rhs: Self) -> res : Self

ensures

res == self.spec_fixed_add(rhs),

exec fn exec_fixed_sub(self, rhs: Self) -> res : Self

ensures

res == self.spec_fixed_sub(rhs),

exec fn exec_fixed_mul(self, rhs: Self) -> res : Self

ensures

res == self.spec_fixed_mul(rhs),

Dyn Compatibility

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety".

Implementations on Foreign Types

impl ExecSpecFixedWidthArith for i8

open spec fn spec_fixed_add(self, rhs: i8) -> i8

{ add(self, rhs) }

open spec fn spec_fixed_sub(self, rhs: i8) -> i8

{ sub(self, rhs) }

open spec fn spec_fixed_mul(self, rhs: i8) -> i8

{ mul(self, rhs) }

exec fn exec_fixed_add(self, rhs: i8) -> res : i8

exec fn exec_fixed_sub(self, rhs: i8) -> res : i8

exec fn exec_fixed_mul(self, rhs: i8) -> res : i8

impl ExecSpecFixedWidthArith for i16

open spec fn spec_fixed_add(self, rhs: i16) -> i16

{ add(self, rhs) }

open spec fn spec_fixed_sub(self, rhs: i16) -> i16

{ sub(self, rhs) }

open spec fn spec_fixed_mul(self, rhs: i16) -> i16

{ mul(self, rhs) }

exec fn exec_fixed_add(self, rhs: i16) -> res : i16

exec fn exec_fixed_sub(self, rhs: i16) -> res : i16

exec fn exec_fixed_mul(self, rhs: i16) -> res : i16

impl ExecSpecFixedWidthArith for i32

open spec fn spec_fixed_add(self, rhs: i32) -> i32

{ add(self, rhs) }

open spec fn spec_fixed_sub(self, rhs: i32) -> i32

{ sub(self, rhs) }

open spec fn spec_fixed_mul(self, rhs: i32) -> i32

{ mul(self, rhs) }

exec fn exec_fixed_add(self, rhs: i32) -> res : i32

exec fn exec_fixed_sub(self, rhs: i32) -> res : i32

exec fn exec_fixed_mul(self, rhs: i32) -> res : i32

impl ExecSpecFixedWidthArith for i64

open spec fn spec_fixed_add(self, rhs: i64) -> i64

{ add(self, rhs) }

open spec fn spec_fixed_sub(self, rhs: i64) -> i64

{ sub(self, rhs) }

open spec fn spec_fixed_mul(self, rhs: i64) -> i64

{ mul(self, rhs) }

exec fn exec_fixed_add(self, rhs: i64) -> res : i64

exec fn exec_fixed_sub(self, rhs: i64) -> res : i64

exec fn exec_fixed_mul(self, rhs: i64) -> res : i64

impl ExecSpecFixedWidthArith for isize

open spec fn spec_fixed_add(self, rhs: isize) -> isize

{ add(self, rhs) }

open spec fn spec_fixed_sub(self, rhs: isize) -> isize

{ sub(self, rhs) }

open spec fn spec_fixed_mul(self, rhs: isize) -> isize

{ mul(self, rhs) }

exec fn exec_fixed_add(self, rhs: isize) -> res : isize

exec fn exec_fixed_sub(self, rhs: isize) -> res : isize

exec fn exec_fixed_mul(self, rhs: isize) -> res : isize

impl ExecSpecFixedWidthArith for u8

open spec fn spec_fixed_add(self, rhs: u8) -> u8

{ add(self, rhs) }

open spec fn spec_fixed_sub(self, rhs: u8) -> u8

{ sub(self, rhs) }

open spec fn spec_fixed_mul(self, rhs: u8) -> u8

{ mul(self, rhs) }

exec fn exec_fixed_add(self, rhs: u8) -> res : u8

exec fn exec_fixed_sub(self, rhs: u8) -> res : u8

exec fn exec_fixed_mul(self, rhs: u8) -> res : u8

impl ExecSpecFixedWidthArith for u16

open spec fn spec_fixed_add(self, rhs: u16) -> u16

{ add(self, rhs) }

open spec fn spec_fixed_sub(self, rhs: u16) -> u16

{ sub(self, rhs) }

open spec fn spec_fixed_mul(self, rhs: u16) -> u16

{ mul(self, rhs) }

exec fn exec_fixed_add(self, rhs: u16) -> res : u16

exec fn exec_fixed_sub(self, rhs: u16) -> res : u16

exec fn exec_fixed_mul(self, rhs: u16) -> res : u16

impl ExecSpecFixedWidthArith for u32

open spec fn spec_fixed_add(self, rhs: u32) -> u32

{ add(self, rhs) }

open spec fn spec_fixed_sub(self, rhs: u32) -> u32

{ sub(self, rhs) }

open spec fn spec_fixed_mul(self, rhs: u32) -> u32

{ mul(self, rhs) }

exec fn exec_fixed_add(self, rhs: u32) -> res : u32

exec fn exec_fixed_sub(self, rhs: u32) -> res : u32

exec fn exec_fixed_mul(self, rhs: u32) -> res : u32

impl ExecSpecFixedWidthArith for u64

open spec fn spec_fixed_add(self, rhs: u64) -> u64

{ add(self, rhs) }

open spec fn spec_fixed_sub(self, rhs: u64) -> u64

{ sub(self, rhs) }

open spec fn spec_fixed_mul(self, rhs: u64) -> u64

{ mul(self, rhs) }

exec fn exec_fixed_add(self, rhs: u64) -> res : u64

exec fn exec_fixed_sub(self, rhs: u64) -> res : u64

exec fn exec_fixed_mul(self, rhs: u64) -> res : u64

impl ExecSpecFixedWidthArith for usize

open spec fn spec_fixed_add(self, rhs: usize) -> usize

{ add(self, rhs) }

open spec fn spec_fixed_sub(self, rhs: usize) -> usize

{ sub(self, rhs) }

open spec fn spec_fixed_mul(self, rhs: usize) -> usize

{ mul(self, rhs) }

exec fn exec_fixed_add(self, rhs: usize) -> res : usize

exec fn exec_fixed_sub(self, rhs: usize) -> res : usize

exec fn exec_fixed_mul(self, rhs: usize) -> res : usize

Implementors