MapInvertBackward

vstd_extra::bit_mapping

Trait MapInvertBackward 

Source 
pub trait MapInvertBackward<Src>: Sized {
    // Required methods
    spec fn map_invert_backward_spec(self, bm: &[BitMapping<Src, Self>]) -> Src;
    exec fn map_invert_backward(self, bm: &[BitMapping<Src, Self>]) -> Src;
    broadcast proof fn lemma_equal_map_invert_backward(
        x: Self,
        y: Self,
        bm1: &[BitMapping<Src, Self>],
        bm2: &[BitMapping<Src, Self>],
    );
}

Required Methods§

Source

spec fn map_invert_backward_spec(self, bm: &[BitMapping<Src, Self>]) -> Src

Source

exec fn map_invert_backward(self, bm: &[BitMapping<Src, Self>]) -> Src

Source

broadcast proof fn lemma_equal_map_invert_backward( x: Self, y: Self, bm1: &[BitMapping<Src, Self>], bm2: &[BitMapping<Src, Self>], )

requires
x == y,
bm1 == bm2,
ensures
#[trigger] x.map_invert_backward(bm1) == #[trigger] y.map_invert_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 MapInvertBackward<u8> for u8

Source§

open spec fn map_invert_backward_spec(self, bm: &[BitMapping<u8, Self>]) -> u8

{
    let inv_src = !self;
    bm@
        .fold_left(
            0 as u8,
            |acc: u8, m: BitMapping<u8, Self>| {
                if inv_src & m.dst == 0 { acc | m.src } else { acc }
            },
        )
}
Source§

exec fn map_invert_backward(self, bm: &[BitMapping<u8, Self>]) -> u8

Source§

proof fn lemma_equal_map_invert_backward( x: Self, y: Self, bm1: &[BitMapping<u8, Self>], bm2: &[BitMapping<u8, Self>], )

Source§

impl MapInvertBackward<u8> for u16

Source§

open spec fn map_invert_backward_spec(self, bm: &[BitMapping<u8, Self>]) -> u8

{
    let inv_src = !self;
    bm@
        .fold_left(
            0 as u8,
            |acc: u8, m: BitMapping<u8, Self>| {
                if inv_src & m.dst == 0 { acc | m.src } else { acc }
            },
        )
}
Source§

exec fn map_invert_backward(self, bm: &[BitMapping<u8, Self>]) -> u8

Source§

proof fn lemma_equal_map_invert_backward( x: Self, y: Self, bm1: &[BitMapping<u8, Self>], bm2: &[BitMapping<u8, Self>], )

Source§

impl MapInvertBackward<u8> for u32

Source§

open spec fn map_invert_backward_spec(self, bm: &[BitMapping<u8, Self>]) -> u8

{
    let inv_src = !self;
    bm@
        .fold_left(
            0 as u8,
            |acc: u8, m: BitMapping<u8, Self>| {
                if inv_src & m.dst == 0 { acc | m.src } else { acc }
            },
        )
}
Source§

exec fn map_invert_backward(self, bm: &[BitMapping<u8, Self>]) -> u8

Source§

proof fn lemma_equal_map_invert_backward( x: Self, y: Self, bm1: &[BitMapping<u8, Self>], bm2: &[BitMapping<u8, Self>], )

Source§

impl MapInvertBackward<u8> for u64

Source§

open spec fn map_invert_backward_spec(self, bm: &[BitMapping<u8, Self>]) -> u8

{
    let inv_src = !self;
    bm@
        .fold_left(
            0 as u8,
            |acc: u8, m: BitMapping<u8, Self>| {
                if inv_src & m.dst == 0 { acc | m.src } else { acc }
            },
        )
}
Source§

exec fn map_invert_backward(self, bm: &[BitMapping<u8, Self>]) -> u8

Source§

proof fn lemma_equal_map_invert_backward( x: Self, y: Self, bm1: &[BitMapping<u8, Self>], bm2: &[BitMapping<u8, Self>], )

Source§

impl MapInvertBackward<u8> for usize

Source§

open spec fn map_invert_backward_spec(self, bm: &[BitMapping<u8, Self>]) -> u8

{
    let inv_src = !self;
    bm@
        .fold_left(
            0 as u8,
            |acc: u8, m: BitMapping<u8, Self>| {
                if inv_src & m.dst == 0 { acc | m.src } else { acc }
            },
        )
}
Source§

exec fn map_invert_backward(self, bm: &[BitMapping<u8, Self>]) -> u8

Source§

proof fn lemma_equal_map_invert_backward( x: Self, y: Self, bm1: &[BitMapping<u8, Self>], bm2: &[BitMapping<u8, Self>], )

Source§

impl MapInvertBackward<u32> for u32

Source§

open spec fn map_invert_backward_spec(self, bm: &[BitMapping<u32, Self>]) -> u32

{
    let inv_src = !self;
    bm@
        .fold_left(
            0 as u32,
            |acc: u32, m: BitMapping<u32, Self>| {
                if inv_src & m.dst == 0 { acc | m.src } else { acc }
            },
        )
}
Source§

exec fn map_invert_backward(self, bm: &[BitMapping<u32, Self>]) -> u32

Source§

proof fn lemma_equal_map_invert_backward( x: Self, y: Self, bm1: &[BitMapping<u32, Self>], bm2: &[BitMapping<u32, Self>], )

Source§

impl MapInvertBackward<u32> for u64

Source§

open spec fn map_invert_backward_spec(self, bm: &[BitMapping<u32, Self>]) -> u32

{
    let inv_src = !self;
    bm@
        .fold_left(
            0 as u32,
            |acc: u32, m: BitMapping<u32, Self>| {
                if inv_src & m.dst == 0 { acc | m.src } else { acc }
            },
        )
}
Source§

exec fn map_invert_backward(self, bm: &[BitMapping<u32, Self>]) -> u32

Source§

proof fn lemma_equal_map_invert_backward( x: Self, y: Self, bm1: &[BitMapping<u32, Self>], bm2: &[BitMapping<u32, Self>], )

Source§

impl MapInvertBackward<u32> for usize

Source§

open spec fn map_invert_backward_spec(self, bm: &[BitMapping<u32, Self>]) -> u32

{
    let inv_src = !self;
    bm@
        .fold_left(
            0 as u32,
            |acc: u32, m: BitMapping<u32, Self>| {
                if inv_src & m.dst == 0 { acc | m.src } else { acc }
            },
        )
}
Source§

exec fn map_invert_backward(self, bm: &[BitMapping<u32, Self>]) -> u32

Source§

proof fn lemma_equal_map_invert_backward( x: Self, y: Self, bm1: &[BitMapping<u32, Self>], bm2: &[BitMapping<u32, Self>], )

Source§

impl MapInvertBackward<u64> for u64

Source§

open spec fn map_invert_backward_spec(self, bm: &[BitMapping<u64, Self>]) -> u64

{
    let inv_src = !self;
    bm@
        .fold_left(
            0 as u64,
            |acc: u64, m: BitMapping<u64, Self>| {
                if inv_src & m.dst == 0 { acc | m.src } else { acc }
            },
        )
}
Source§

exec fn map_invert_backward(self, bm: &[BitMapping<u64, Self>]) -> u64

Source§

proof fn lemma_equal_map_invert_backward( x: Self, y: Self, bm1: &[BitMapping<u64, Self>], bm2: &[BitMapping<u64, Self>], )

Source§

impl MapInvertBackward<u64> for usize

Source§

open spec fn map_invert_backward_spec(self, bm: &[BitMapping<u64, Self>]) -> u64

{
    let inv_src = !self;
    bm@
        .fold_left(
            0 as u64,
            |acc: u64, m: BitMapping<u64, Self>| {
                if inv_src & m.dst == 0 { acc | m.src } else { acc }
            },
        )
}
Source§

exec fn map_invert_backward(self, bm: &[BitMapping<u64, Self>]) -> u64

Source§

proof fn lemma_equal_map_invert_backward( x: Self, y: Self, bm1: &[BitMapping<u64, Self>], bm2: &[BitMapping<u64, Self>], )

Implementors§