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