pub trait MapInvertForwardTrait<Dst>: Sized {
// Required methods
spec fn map_invert_forward_spec(self, bm: &[BitMapping<Self, Dst>]) -> Dst;
exec fn map_invert_forward(self, bm: &[BitMapping<Self, Dst>]) -> Dst;
broadcast proof fn lemma_equal_map_invert_froward(
x: Self,
y: Self,
bm1: &[BitMapping<Self, Dst>],
bm2: &[BitMapping<Self, Dst>],
);
}Required Methods§
Sourcespec fn map_invert_forward_spec(self, bm: &[BitMapping<Self, Dst>]) -> Dst
spec fn map_invert_forward_spec(self, bm: &[BitMapping<Self, Dst>]) -> Dst
Sourceexec fn map_invert_forward(self, bm: &[BitMapping<Self, Dst>]) -> Dst
exec fn map_invert_forward(self, bm: &[BitMapping<Self, Dst>]) -> Dst
Sourcebroadcast proof fn lemma_equal_map_invert_froward(
x: Self,
y: Self,
bm1: &[BitMapping<Self, Dst>],
bm2: &[BitMapping<Self, Dst>],
)
broadcast proof fn lemma_equal_map_invert_froward( x: Self, y: Self, bm1: &[BitMapping<Self, Dst>], bm2: &[BitMapping<Self, Dst>], )
requires
x == y,bm1 == bm2,#[trigger] x.map_invert_forward(bm1) == #[trigger] y.map_invert_forward(bm2),Dyn Compatibility§
This trait is not dyn compatible.
In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.
Implementations on Foreign Types§
Source§impl MapInvertForwardTrait<u8> for u8
impl MapInvertForwardTrait<u8> for u8
Source§open spec fn map_invert_forward_spec(self, bm: &[BitMapping<Self, u8>]) -> u8
open spec fn map_invert_forward_spec(self, bm: &[BitMapping<Self, u8>]) -> u8
{
let inv_src = !self;
bm@
.fold_left(
0 as u8,
|acc: u8, m: BitMapping<Self, u8>| {
if inv_src & m.src == 0 { acc | m.dst } else { acc }
},
)
}Source§exec fn map_invert_forward(self, bm: &[BitMapping<Self, u8>]) -> u8
exec fn map_invert_forward(self, bm: &[BitMapping<Self, u8>]) -> u8
Source§proof fn lemma_equal_map_invert_froward(
x: Self,
y: Self,
bm1: &[BitMapping<Self, u8>],
bm2: &[BitMapping<Self, u8>],
)
proof fn lemma_equal_map_invert_froward( x: Self, y: Self, bm1: &[BitMapping<Self, u8>], bm2: &[BitMapping<Self, u8>], )
Source§impl MapInvertForwardTrait<u16> for u8
impl MapInvertForwardTrait<u16> for u8
Source§open spec fn map_invert_forward_spec(self, bm: &[BitMapping<Self, u16>]) -> u16
open spec fn map_invert_forward_spec(self, bm: &[BitMapping<Self, u16>]) -> u16
{
let inv_src = !self;
bm@
.fold_left(
0 as u16,
|acc: u16, m: BitMapping<Self, u16>| {
if inv_src & m.src == 0 { acc | m.dst } else { acc }
},
)
}Source§exec fn map_invert_forward(self, bm: &[BitMapping<Self, u16>]) -> u16
exec fn map_invert_forward(self, bm: &[BitMapping<Self, u16>]) -> u16
Source§proof fn lemma_equal_map_invert_froward(
x: Self,
y: Self,
bm1: &[BitMapping<Self, u16>],
bm2: &[BitMapping<Self, u16>],
)
proof fn lemma_equal_map_invert_froward( x: Self, y: Self, bm1: &[BitMapping<Self, u16>], bm2: &[BitMapping<Self, u16>], )
Source§impl MapInvertForwardTrait<u32> for u8
impl MapInvertForwardTrait<u32> for u8
Source§open spec fn map_invert_forward_spec(self, bm: &[BitMapping<Self, u32>]) -> u32
open spec fn map_invert_forward_spec(self, bm: &[BitMapping<Self, u32>]) -> u32
{
let inv_src = !self;
bm@
.fold_left(
0 as u32,
|acc: u32, m: BitMapping<Self, u32>| {
if inv_src & m.src == 0 { acc | m.dst } else { acc }
},
)
}Source§exec fn map_invert_forward(self, bm: &[BitMapping<Self, u32>]) -> u32
exec fn map_invert_forward(self, bm: &[BitMapping<Self, u32>]) -> u32
Source§proof fn lemma_equal_map_invert_froward(
x: Self,
y: Self,
bm1: &[BitMapping<Self, u32>],
bm2: &[BitMapping<Self, u32>],
)
proof fn lemma_equal_map_invert_froward( x: Self, y: Self, bm1: &[BitMapping<Self, u32>], bm2: &[BitMapping<Self, u32>], )
Source§impl MapInvertForwardTrait<u32> for u32
impl MapInvertForwardTrait<u32> for u32
Source§open spec fn map_invert_forward_spec(self, bm: &[BitMapping<Self, u32>]) -> u32
open spec fn map_invert_forward_spec(self, bm: &[BitMapping<Self, u32>]) -> u32
{
let inv_src = !self;
bm@
.fold_left(
0 as u32,
|acc: u32, m: BitMapping<Self, u32>| {
if inv_src & m.src == 0 { acc | m.dst } else { acc }
},
)
}Source§exec fn map_invert_forward(self, bm: &[BitMapping<Self, u32>]) -> u32
exec fn map_invert_forward(self, bm: &[BitMapping<Self, u32>]) -> u32
Source§proof fn lemma_equal_map_invert_froward(
x: Self,
y: Self,
bm1: &[BitMapping<Self, u32>],
bm2: &[BitMapping<Self, u32>],
)
proof fn lemma_equal_map_invert_froward( x: Self, y: Self, bm1: &[BitMapping<Self, u32>], bm2: &[BitMapping<Self, u32>], )
Source§impl MapInvertForwardTrait<u64> for u8
impl MapInvertForwardTrait<u64> for u8
Source§open spec fn map_invert_forward_spec(self, bm: &[BitMapping<Self, u64>]) -> u64
open spec fn map_invert_forward_spec(self, bm: &[BitMapping<Self, u64>]) -> u64
{
let inv_src = !self;
bm@
.fold_left(
0 as u64,
|acc: u64, m: BitMapping<Self, u64>| {
if inv_src & m.src == 0 { acc | m.dst } else { acc }
},
)
}Source§exec fn map_invert_forward(self, bm: &[BitMapping<Self, u64>]) -> u64
exec fn map_invert_forward(self, bm: &[BitMapping<Self, u64>]) -> u64
Source§proof fn lemma_equal_map_invert_froward(
x: Self,
y: Self,
bm1: &[BitMapping<Self, u64>],
bm2: &[BitMapping<Self, u64>],
)
proof fn lemma_equal_map_invert_froward( x: Self, y: Self, bm1: &[BitMapping<Self, u64>], bm2: &[BitMapping<Self, u64>], )
Source§impl MapInvertForwardTrait<u64> for u32
impl MapInvertForwardTrait<u64> for u32
Source§open spec fn map_invert_forward_spec(self, bm: &[BitMapping<Self, u64>]) -> u64
open spec fn map_invert_forward_spec(self, bm: &[BitMapping<Self, u64>]) -> u64
{
let inv_src = !self;
bm@
.fold_left(
0 as u64,
|acc: u64, m: BitMapping<Self, u64>| {
if inv_src & m.src == 0 { acc | m.dst } else { acc }
},
)
}Source§exec fn map_invert_forward(self, bm: &[BitMapping<Self, u64>]) -> u64
exec fn map_invert_forward(self, bm: &[BitMapping<Self, u64>]) -> u64
Source§proof fn lemma_equal_map_invert_froward(
x: Self,
y: Self,
bm1: &[BitMapping<Self, u64>],
bm2: &[BitMapping<Self, u64>],
)
proof fn lemma_equal_map_invert_froward( x: Self, y: Self, bm1: &[BitMapping<Self, u64>], bm2: &[BitMapping<Self, u64>], )
Source§impl MapInvertForwardTrait<u64> for u64
impl MapInvertForwardTrait<u64> for u64
Source§open spec fn map_invert_forward_spec(self, bm: &[BitMapping<Self, u64>]) -> u64
open spec fn map_invert_forward_spec(self, bm: &[BitMapping<Self, u64>]) -> u64
{
let inv_src = !self;
bm@
.fold_left(
0 as u64,
|acc: u64, m: BitMapping<Self, u64>| {
if inv_src & m.src == 0 { acc | m.dst } else { acc }
},
)
}Source§exec fn map_invert_forward(self, bm: &[BitMapping<Self, u64>]) -> u64
exec fn map_invert_forward(self, bm: &[BitMapping<Self, u64>]) -> u64
Source§proof fn lemma_equal_map_invert_froward(
x: Self,
y: Self,
bm1: &[BitMapping<Self, u64>],
bm2: &[BitMapping<Self, u64>],
)
proof fn lemma_equal_map_invert_froward( x: Self, y: Self, bm1: &[BitMapping<Self, u64>], bm2: &[BitMapping<Self, u64>], )
Source§impl MapInvertForwardTrait<usize> for u8
impl MapInvertForwardTrait<usize> for u8
Source§open spec fn map_invert_forward_spec(self, bm: &[BitMapping<Self, usize>]) -> usize
open spec fn map_invert_forward_spec(self, bm: &[BitMapping<Self, usize>]) -> usize
{
let inv_src = !self;
bm@
.fold_left(
0 as usize,
|acc: usize, m: BitMapping<Self, usize>| {
if inv_src & m.src == 0 { acc | m.dst } else { acc }
},
)
}Source§exec fn map_invert_forward(self, bm: &[BitMapping<Self, usize>]) -> usize
exec fn map_invert_forward(self, bm: &[BitMapping<Self, usize>]) -> usize
Source§proof fn lemma_equal_map_invert_froward(
x: Self,
y: Self,
bm1: &[BitMapping<Self, usize>],
bm2: &[BitMapping<Self, usize>],
)
proof fn lemma_equal_map_invert_froward( x: Self, y: Self, bm1: &[BitMapping<Self, usize>], bm2: &[BitMapping<Self, usize>], )
Source§impl MapInvertForwardTrait<usize> for u32
impl MapInvertForwardTrait<usize> for u32
Source§open spec fn map_invert_forward_spec(self, bm: &[BitMapping<Self, usize>]) -> usize
open spec fn map_invert_forward_spec(self, bm: &[BitMapping<Self, usize>]) -> usize
{
let inv_src = !self;
bm@
.fold_left(
0 as usize,
|acc: usize, m: BitMapping<Self, usize>| {
if inv_src & m.src == 0 { acc | m.dst } else { acc }
},
)
}Source§exec fn map_invert_forward(self, bm: &[BitMapping<Self, usize>]) -> usize
exec fn map_invert_forward(self, bm: &[BitMapping<Self, usize>]) -> usize
Source§proof fn lemma_equal_map_invert_froward(
x: Self,
y: Self,
bm1: &[BitMapping<Self, usize>],
bm2: &[BitMapping<Self, usize>],
)
proof fn lemma_equal_map_invert_froward( x: Self, y: Self, bm1: &[BitMapping<Self, usize>], bm2: &[BitMapping<Self, usize>], )
Source§impl MapInvertForwardTrait<usize> for u64
impl MapInvertForwardTrait<usize> for u64
Source§open spec fn map_invert_forward_spec(self, bm: &[BitMapping<Self, usize>]) -> usize
open spec fn map_invert_forward_spec(self, bm: &[BitMapping<Self, usize>]) -> usize
{
let inv_src = !self;
bm@
.fold_left(
0 as usize,
|acc: usize, m: BitMapping<Self, usize>| {
if inv_src & m.src == 0 { acc | m.dst } else { acc }
},
)
}