FromToBytes

vest_lib::regular::uints

Trait FromToBytes 

Source 
pub trait FromToBytes
where
    Self: ViewReflex + Sized + Copy,
{

Show 15 methods    // Required methods
    spec fn spec_from_le_bytes(s: Seq<u8>) -> Self;
    spec fn spec_to_le_bytes(&self) -> Seq<u8>;
    spec fn spec_from_be_bytes(s: Seq<u8>) -> Self;
    spec fn spec_to_be_bytes(&self) -> Seq<u8>;
    proof fn lemma_spec_to_from_le_bytes(&self);
    proof fn lemma_spec_from_to_le_bytes(s: Seq<u8>);
    proof fn lemma_spec_from_le_bytes_no_lookahead(s1: Seq<u8>, s2: Seq<u8>);
    proof fn lemma_spec_to_from_be_bytes(&self);
    proof fn lemma_spec_from_to_be_bytes(s: Seq<u8>);
    proof fn lemma_spec_from_be_bytes_no_lookahead(s1: Seq<u8>, s2: Seq<u8>);
    exec fn ex_from_le_bytes(s: &[u8]) -> x : Self;
    exec fn ex_to_le_bytes<I, O>(&self, s: &mut O, pos: usize)
       where I: VestPublicInput,
             O: VestPublicOutput<I>;
    exec fn ex_from_be_bytes(s: &[u8]) -> x : Self;
    exec fn ex_to_be_bytes<I, O>(&self, s: &mut O, pos: usize)
       where I: VestPublicInput,
             O: VestPublicOutput<I>;
    exec fn eq(&self, other: &Self) -> res : bool;

}
Expand description

A trait for converting an integer type to and from a sequence of bytes.

Required Methods§

Source

spec fn spec_from_le_bytes(s: Seq<u8>) -> Self

Spec version of Self::ex_from_le_bytes

Source

spec fn spec_to_le_bytes(&self) -> Seq<u8>

Spec version of Self::ex_to_le_bytes

Source

spec fn spec_from_be_bytes(s: Seq<u8>) -> Self

Spec version of Self::ex_from_be_bytes

Source

spec fn spec_to_be_bytes(&self) -> Seq<u8>

Spec version of Self::ex_to_be_bytes

Source

proof fn lemma_spec_to_from_le_bytes(&self)

ensures
self.spec_to_le_bytes().len() == size_of::<Self>(),
Self::spec_from_le_bytes(self.spec_to_le_bytes()) == *self,

Lemma that asserts that converting an integer in little-endian byte order to bytes and back results in the original integer

Source

proof fn lemma_spec_from_to_le_bytes(s: Seq<u8>)

ensures
s.len() == size_of::<Self>()
    ==> Self::spec_to_le_bytes(&Self::spec_from_le_bytes(s)) == s,

Lemma that asserts that converting a sequence of bytes to an integer in little-endian byte order and back results in the original sequence

Source

proof fn lemma_spec_from_le_bytes_no_lookahead(s1: Seq<u8>, s2: Seq<u8>)

ensures
s1.len() >= size_of::<Self>()
    ==> Self::spec_from_le_bytes(s1) == Self::spec_from_le_bytes(s1.add(s2)),

Helper lemma for proving SecureSpecCombinator::lemma_prefix_secure

Source

proof fn lemma_spec_to_from_be_bytes(&self)

ensures
self.spec_to_be_bytes().len() == size_of::<Self>(),
Self::spec_from_be_bytes(self.spec_to_be_bytes()) == *self,

Lemma that asserts that converting an integer in big-endian byte order to bytes and back results in the original integer

Source

proof fn lemma_spec_from_to_be_bytes(s: Seq<u8>)

ensures
s.len() == size_of::<Self>()
    ==> Self::spec_to_be_bytes(&Self::spec_from_be_bytes(s)) == s,

Lemma that asserts that converting a sequence of bytes to an integer in big-endian byte order and back results in the original sequence

Source

proof fn lemma_spec_from_be_bytes_no_lookahead(s1: Seq<u8>, s2: Seq<u8>)

ensures
s1.len() >= size_of::<Self>()
    ==> Self::spec_from_be_bytes(s1) == Self::spec_from_be_bytes(s1.add(s2)),

Helper lemma for proving SecureSpecCombinator::lemma_prefix_secure

Source

exec fn ex_from_le_bytes(s: &[u8]) -> x : Self

requires
s@.len() == size_of::<Self>(),
ensures
x == Self::spec_from_le_bytes(s@),

Converts a sequence of bytes to an integer in little-endian byte order.

Source

exec fn ex_to_le_bytes<I, O>(&self, s: &mut O, pos: usize)
where I: VestPublicInput, O: VestPublicOutput<I>,

requires
old(s)@.len() - pos >= size_of::<Self>(),
ensures
old(s)@.len() == s@.len(),
self.spec_to_le_bytes().len() == size_of::<Self>(),
s@ == seq_splice(old(s)@, pos, self.spec_to_le_bytes()),

Converts an integer to a sequence of bytes in little-endian byte order.

Source

exec fn ex_from_be_bytes(s: &[u8]) -> x : Self

requires
s@.len() == size_of::<Self>(),
ensures
x == Self::spec_from_be_bytes(s@),

Converts a sequence of bytes to an integer in big-endian byte order.

Source

exec fn ex_to_be_bytes<I, O>(&self, s: &mut O, pos: usize)
where I: VestPublicInput, O: VestPublicOutput<I>,

requires
old(s)@.len() - pos >= size_of::<Self>(),
ensures
old(s)@.len() == s@.len(),
self.spec_to_be_bytes().len() == size_of::<Self>(),
s@ == seq_splice(old(s)@, pos, self.spec_to_be_bytes()),

Converts an integer to a sequence of bytes in big-endian byte order.

Source

exec fn eq(&self, other: &Self) -> res : bool

ensures
res == (self@ == other@),

Compares two integers for equality.

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 FromToBytes for u8

Source§

open spec fn spec_from_le_bytes(s: Seq<u8>) -> Self

{ s[0] }
Source§

open spec fn spec_to_le_bytes(&self) -> Seq<u8>

{ seq![* self] }
Source§

open spec fn spec_from_be_bytes(s: Seq<u8>) -> Self

{ s[0] }
Source§

open spec fn spec_to_be_bytes(&self) -> Seq<u8>

{ seq![* self] }
Source§

proof fn lemma_spec_to_from_le_bytes(&self)

Source§

proof fn lemma_spec_from_to_le_bytes(s: Seq<u8>)

Source§

proof fn lemma_spec_from_le_bytes_no_lookahead(s1: Seq<u8>, s2: Seq<u8>)

Source§

proof fn lemma_spec_to_from_be_bytes(&self)

Source§

proof fn lemma_spec_from_to_be_bytes(s: Seq<u8>)

Source§

proof fn lemma_spec_from_be_bytes_no_lookahead(s1: Seq<u8>, s2: Seq<u8>)

Source§

exec fn ex_from_le_bytes(s: &[u8]) -> x : u8

Source§

exec fn ex_to_le_bytes<I, O>(&self, s: &mut O, pos: usize)
where I: VestPublicInput, O: VestPublicOutput<I>,

Source§

exec fn ex_from_be_bytes(s: &[u8]) -> x : u8

Source§

exec fn ex_to_be_bytes<I, O>(&self, s: &mut O, pos: usize)
where I: VestPublicInput, O: VestPublicOutput<I>,

Source§

exec fn eq(&self, other: &u8) -> res : bool

Source§

impl FromToBytes for u16

Source§

open spec fn spec_from_le_bytes(s: Seq<u8>) -> Self

{ (s[0] as u16) | (s[1] as u16) << 8 }
Source§

open spec fn spec_to_le_bytes(&self) -> Seq<u8>

{ seq![(self & 0xff) as u8, ((self >> 8) & 0xff) as u8] }
Source§

open spec fn spec_from_be_bytes(s: Seq<u8>) -> Self

{ (s[0] as u16) << 8 | (s[1] as u16) }
Source§

open spec fn spec_to_be_bytes(&self) -> Seq<u8>

{ seq![((self >> 8) & 0xff) as u8, (self & 0xff) as u8] }
Source§

proof fn lemma_spec_to_from_le_bytes(&self)

Source§

proof fn lemma_spec_from_to_le_bytes(s: Seq<u8>)

Source§

proof fn lemma_spec_from_le_bytes_no_lookahead(s1: Seq<u8>, s2: Seq<u8>)

Source§

proof fn lemma_spec_to_from_be_bytes(&self)

Source§

proof fn lemma_spec_from_to_be_bytes(s: Seq<u8>)

Source§

proof fn lemma_spec_from_be_bytes_no_lookahead(s1: Seq<u8>, s2: Seq<u8>)

Source§

exec fn ex_from_le_bytes(s: &[u8]) -> x : u16

Source§

exec fn ex_to_le_bytes<I, O>(&self, s: &mut O, pos: usize)
where I: VestPublicInput, O: VestPublicOutput<I>,

Source§

exec fn ex_from_be_bytes(s: &[u8]) -> x : u16

Source§

exec fn ex_to_be_bytes<I, O>(&self, s: &mut O, pos: usize)
where I: VestPublicInput, O: VestPublicOutput<I>,

Source§

exec fn eq(&self, other: &u16) -> res : bool

Source§

impl FromToBytes for u32

Source§

open spec fn spec_from_le_bytes(s: Seq<u8>) -> Self

{ (s[0] as u32) | (s[1] as u32) << 8 | (s[2] as u32) << 16 | (s[3] as u32) << 24 }
Source§

open spec fn spec_to_le_bytes(&self) -> Seq<u8>

{
    seq![
        (self & 0xff) as u8, ((self >> 8) & 0xff) as u8, ((self >> 16) & 0xff) as u8,
        ((self >> 24) & 0xff) as u8,
    ]
}
Source§

open spec fn spec_from_be_bytes(s: Seq<u8>) -> Self

{ (s[0] as u32) << 24 | (s[1] as u32) << 16 | (s[2] as u32) << 8 | (s[3] as u32) }
Source§

open spec fn spec_to_be_bytes(&self) -> Seq<u8>

{
    seq![
        ((self >> 24) & 0xff) as u8, ((self >> 16) & 0xff) as u8, ((self >> 8) & 0xff) as
        u8, (self & 0xff) as u8,
    ]
}
Source§

proof fn lemma_spec_to_from_le_bytes(&self)

Source§

proof fn lemma_spec_from_to_le_bytes(s: Seq<u8>)

Source§

proof fn lemma_spec_from_le_bytes_no_lookahead(s1: Seq<u8>, s2: Seq<u8>)

Source§

proof fn lemma_spec_to_from_be_bytes(&self)

Source§

proof fn lemma_spec_from_to_be_bytes(s: Seq<u8>)

Source§

proof fn lemma_spec_from_be_bytes_no_lookahead(s1: Seq<u8>, s2: Seq<u8>)

Source§

exec fn ex_from_le_bytes(s: &[u8]) -> x : u32

Source§

exec fn ex_to_le_bytes<I, O>(&self, s: &mut O, pos: usize)
where I: VestPublicInput, O: VestPublicOutput<I>,

Source§

exec fn ex_from_be_bytes(s: &[u8]) -> x : u32

Source§

exec fn ex_to_be_bytes<I, O>(&self, s: &mut O, pos: usize)
where I: VestPublicInput, O: VestPublicOutput<I>,

Source§

exec fn eq(&self, other: &u32) -> res : bool

Source§

impl FromToBytes for u64

Source§

open spec fn spec_from_le_bytes(s: Seq<u8>) -> Self

{
    (s[0] as u64) | (s[1] as u64) << 8 | (s[2] as u64) << 16 | (s[3] as u64) << 24
        | (s[4] as u64) << 32 | (s[5] as u64) << 40 | (s[6] as u64) << 48
        | (s[7] as u64) << 56
}
Source§

open spec fn spec_to_le_bytes(&self) -> Seq<u8>

{
    seq![
        (self & 0xff) as u8, ((self >> 8) & 0xff) as u8, ((self >> 16) & 0xff) as u8,
        ((self >> 24) & 0xff) as u8, ((self >> 32) & 0xff) as u8, ((self >> 40) & 0xff)
        as u8, ((self >> 48) & 0xff) as u8, ((self >> 56) & 0xff) as u8,
    ]
}
Source§

open spec fn spec_from_be_bytes(s: Seq<u8>) -> Self

{
    (s[0] as u64) << 56 | (s[1] as u64) << 48 | (s[2] as u64) << 40 | (s[3] as u64) << 32
        | (s[4] as u64) << 24 | (s[5] as u64) << 16 | (s[6] as u64) << 8 | (s[7] as u64)
}
Source§

open spec fn spec_to_be_bytes(&self) -> Seq<u8>

{
    seq![
        ((self >> 56) & 0xff) as u8, ((self >> 48) & 0xff) as u8, ((self >> 40) & 0xff)
        as u8, ((self >> 32) & 0xff) as u8, ((self >> 24) & 0xff) as u8, ((self >> 16) &
        0xff) as u8, ((self >> 8) & 0xff) as u8, (self & 0xff) as u8,
    ]
}
Source§

proof fn lemma_spec_to_from_le_bytes(&self)

Source§

proof fn lemma_spec_from_to_le_bytes(s: Seq<u8>)

Source§

proof fn lemma_spec_from_le_bytes_no_lookahead(s1: Seq<u8>, s2: Seq<u8>)

Source§

proof fn lemma_spec_to_from_be_bytes(&self)

Source§

proof fn lemma_spec_from_to_be_bytes(s: Seq<u8>)

Source§

proof fn lemma_spec_from_be_bytes_no_lookahead(s1: Seq<u8>, s2: Seq<u8>)

Source§

exec fn ex_from_le_bytes(s: &[u8]) -> x : u64

Source§

exec fn ex_to_le_bytes<I, O>(&self, s: &mut O, pos: usize)
where I: VestPublicInput, O: VestPublicOutput<I>,

Source§

exec fn ex_from_be_bytes(s: &[u8]) -> x : u64

Source§

exec fn ex_to_be_bytes<I, O>(&self, s: &mut O, pos: usize)
where I: VestPublicInput, O: VestPublicOutput<I>,

Source§

exec fn eq(&self, other: &u64) -> res : bool

Implementors§