pub trait MapForwardTrait<Dst>: Sized {
// Required methods
spec fn map_forward_spec(self, bm: &[BitMapping<Self, Dst>]) -> Dst;
exec fn map_forward(self, bm: &[BitMapping<Self, Dst>]) -> Dst;
broadcast proof fn lemma_equal_map_froward(
x: Self,
y: Self,
bm1: &[BitMapping<Self, Dst>],
bm2: &[BitMapping<Self, Dst>],
);
}Required Methods§
Sourcespec fn map_forward_spec(self, bm: &[BitMapping<Self, Dst>]) -> Dst
spec fn map_forward_spec(self, bm: &[BitMapping<Self, Dst>]) -> Dst
Sourceexec fn map_forward(self, bm: &[BitMapping<Self, Dst>]) -> Dst
exec fn map_forward(self, bm: &[BitMapping<Self, Dst>]) -> Dst
Sourcebroadcast proof fn lemma_equal_map_froward(
x: Self,
y: Self,
bm1: &[BitMapping<Self, Dst>],
bm2: &[BitMapping<Self, Dst>],
)
broadcast proof fn lemma_equal_map_froward( x: Self, y: Self, bm1: &[BitMapping<Self, Dst>], bm2: &[BitMapping<Self, Dst>], )
requires
x == y,bm1 == bm2,#[trigger] x.map_forward_spec(bm1) == #[trigger] y.map_forward_spec(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 MapForwardTrait<u8> for u8
impl MapForwardTrait<u8> for u8
Source§open spec fn map_forward_spec(self, bm: &[BitMapping<Self, u8>]) -> u8
open spec fn map_forward_spec(self, bm: &[BitMapping<Self, u8>]) -> u8
{
bm@
.fold_left(
0 as u8,
|acc: u8, m: BitMapping<Self, u8>| {
if self & m.src == m.src { acc | m.dst } else { acc }
},
)
}Source§exec fn map_forward(self, bm: &[BitMapping<Self, u8>]) -> u8
exec fn map_forward(self, bm: &[BitMapping<Self, u8>]) -> u8
Source§proof fn lemma_equal_map_froward(
x: Self,
y: Self,
bm1: &[BitMapping<Self, u8>],
bm2: &[BitMapping<Self, u8>],
)
proof fn lemma_equal_map_froward( x: Self, y: Self, bm1: &[BitMapping<Self, u8>], bm2: &[BitMapping<Self, u8>], )
Source§impl MapForwardTrait<u16> for u8
impl MapForwardTrait<u16> for u8
Source§open spec fn map_forward_spec(self, bm: &[BitMapping<Self, u16>]) -> u16
open spec fn map_forward_spec(self, bm: &[BitMapping<Self, u16>]) -> u16
{
bm@
.fold_left(
0 as u16,
|acc: u16, m: BitMapping<Self, u16>| {
if self & m.src == m.src { acc | m.dst } else { acc }
},
)
}Source§exec fn map_forward(self, bm: &[BitMapping<Self, u16>]) -> u16
exec fn map_forward(self, bm: &[BitMapping<Self, u16>]) -> u16
Source§proof fn lemma_equal_map_froward(
x: Self,
y: Self,
bm1: &[BitMapping<Self, u16>],
bm2: &[BitMapping<Self, u16>],
)
proof fn lemma_equal_map_froward( x: Self, y: Self, bm1: &[BitMapping<Self, u16>], bm2: &[BitMapping<Self, u16>], )
Source§impl MapForwardTrait<u32> for u8
impl MapForwardTrait<u32> for u8
Source§open spec fn map_forward_spec(self, bm: &[BitMapping<Self, u32>]) -> u32
open spec fn map_forward_spec(self, bm: &[BitMapping<Self, u32>]) -> u32
{
bm@
.fold_left(
0 as u32,
|acc: u32, m: BitMapping<Self, u32>| {
if self & m.src == m.src { acc | m.dst } else { acc }
},
)
}Source§exec fn map_forward(self, bm: &[BitMapping<Self, u32>]) -> u32
exec fn map_forward(self, bm: &[BitMapping<Self, u32>]) -> u32
Source§proof fn lemma_equal_map_froward(
x: Self,
y: Self,
bm1: &[BitMapping<Self, u32>],
bm2: &[BitMapping<Self, u32>],
)
proof fn lemma_equal_map_froward( x: Self, y: Self, bm1: &[BitMapping<Self, u32>], bm2: &[BitMapping<Self, u32>], )
Source§impl MapForwardTrait<u32> for u32
impl MapForwardTrait<u32> for u32
Source§open spec fn map_forward_spec(self, bm: &[BitMapping<Self, u32>]) -> u32
open spec fn map_forward_spec(self, bm: &[BitMapping<Self, u32>]) -> u32
{
bm@
.fold_left(
0 as u32,
|acc: u32, m: BitMapping<Self, u32>| {
if self & m.src == m.src { acc | m.dst } else { acc }
},
)
}Source§exec fn map_forward(self, bm: &[BitMapping<Self, u32>]) -> u32
exec fn map_forward(self, bm: &[BitMapping<Self, u32>]) -> u32
Source§proof fn lemma_equal_map_froward(
x: Self,
y: Self,
bm1: &[BitMapping<Self, u32>],
bm2: &[BitMapping<Self, u32>],
)
proof fn lemma_equal_map_froward( x: Self, y: Self, bm1: &[BitMapping<Self, u32>], bm2: &[BitMapping<Self, u32>], )
Source§impl MapForwardTrait<u64> for u8
impl MapForwardTrait<u64> for u8
Source§open spec fn map_forward_spec(self, bm: &[BitMapping<Self, u64>]) -> u64
open spec fn map_forward_spec(self, bm: &[BitMapping<Self, u64>]) -> u64
{
bm@
.fold_left(
0 as u64,
|acc: u64, m: BitMapping<Self, u64>| {
if self & m.src == m.src { acc | m.dst } else { acc }
},
)
}Source§exec fn map_forward(self, bm: &[BitMapping<Self, u64>]) -> u64
exec fn map_forward(self, bm: &[BitMapping<Self, u64>]) -> u64
Source§proof fn lemma_equal_map_froward(
x: Self,
y: Self,
bm1: &[BitMapping<Self, u64>],
bm2: &[BitMapping<Self, u64>],
)
proof fn lemma_equal_map_froward( x: Self, y: Self, bm1: &[BitMapping<Self, u64>], bm2: &[BitMapping<Self, u64>], )
Source§impl MapForwardTrait<u64> for u32
impl MapForwardTrait<u64> for u32
Source§open spec fn map_forward_spec(self, bm: &[BitMapping<Self, u64>]) -> u64
open spec fn map_forward_spec(self, bm: &[BitMapping<Self, u64>]) -> u64
{
bm@
.fold_left(
0 as u64,
|acc: u64, m: BitMapping<Self, u64>| {
if self & m.src == m.src { acc | m.dst } else { acc }
},
)
}Source§exec fn map_forward(self, bm: &[BitMapping<Self, u64>]) -> u64
exec fn map_forward(self, bm: &[BitMapping<Self, u64>]) -> u64
Source§proof fn lemma_equal_map_froward(
x: Self,
y: Self,
bm1: &[BitMapping<Self, u64>],
bm2: &[BitMapping<Self, u64>],
)
proof fn lemma_equal_map_froward( x: Self, y: Self, bm1: &[BitMapping<Self, u64>], bm2: &[BitMapping<Self, u64>], )
Source§impl MapForwardTrait<u64> for u64
impl MapForwardTrait<u64> for u64
Source§open spec fn map_forward_spec(self, bm: &[BitMapping<Self, u64>]) -> u64
open spec fn map_forward_spec(self, bm: &[BitMapping<Self, u64>]) -> u64
{
bm@
.fold_left(
0 as u64,
|acc: u64, m: BitMapping<Self, u64>| {
if self & m.src == m.src { acc | m.dst } else { acc }
},
)
}Source§exec fn map_forward(self, bm: &[BitMapping<Self, u64>]) -> u64
exec fn map_forward(self, bm: &[BitMapping<Self, u64>]) -> u64
Source§proof fn lemma_equal_map_froward(
x: Self,
y: Self,
bm1: &[BitMapping<Self, u64>],
bm2: &[BitMapping<Self, u64>],
)
proof fn lemma_equal_map_froward( x: Self, y: Self, bm1: &[BitMapping<Self, u64>], bm2: &[BitMapping<Self, u64>], )
Source§impl MapForwardTrait<usize> for u8
impl MapForwardTrait<usize> for u8
Source§open spec fn map_forward_spec(self, bm: &[BitMapping<Self, usize>]) -> usize
open spec fn map_forward_spec(self, bm: &[BitMapping<Self, usize>]) -> usize
{
bm@
.fold_left(
0 as usize,
|acc: usize, m: BitMapping<Self, usize>| {
if self & m.src == m.src { acc | m.dst } else { acc }
},
)
}Source§exec fn map_forward(self, bm: &[BitMapping<Self, usize>]) -> usize
exec fn map_forward(self, bm: &[BitMapping<Self, usize>]) -> usize
Source§proof fn lemma_equal_map_froward(
x: Self,
y: Self,
bm1: &[BitMapping<Self, usize>],
bm2: &[BitMapping<Self, usize>],
)
proof fn lemma_equal_map_froward( x: Self, y: Self, bm1: &[BitMapping<Self, usize>], bm2: &[BitMapping<Self, usize>], )
Source§impl MapForwardTrait<usize> for u32
impl MapForwardTrait<usize> for u32
Source§open spec fn map_forward_spec(self, bm: &[BitMapping<Self, usize>]) -> usize
open spec fn map_forward_spec(self, bm: &[BitMapping<Self, usize>]) -> usize
{
bm@
.fold_left(
0 as usize,
|acc: usize, m: BitMapping<Self, usize>| {
if self & m.src == m.src { acc | m.dst } else { acc }
},
)
}Source§exec fn map_forward(self, bm: &[BitMapping<Self, usize>]) -> usize
exec fn map_forward(self, bm: &[BitMapping<Self, usize>]) -> usize
Source§proof fn lemma_equal_map_froward(
x: Self,
y: Self,
bm1: &[BitMapping<Self, usize>],
bm2: &[BitMapping<Self, usize>],
)
proof fn lemma_equal_map_froward( x: Self, y: Self, bm1: &[BitMapping<Self, usize>], bm2: &[BitMapping<Self, usize>], )
Source§impl MapForwardTrait<usize> for u64
impl MapForwardTrait<usize> for u64
Source§open spec fn map_forward_spec(self, bm: &[BitMapping<Self, usize>]) -> usize
open spec fn map_forward_spec(self, bm: &[BitMapping<Self, usize>]) -> usize
{
bm@
.fold_left(
0 as usize,
|acc: usize, m: BitMapping<Self, usize>| {
if self & m.src == m.src { acc | m.dst } else { acc }
},
)
}