Skip to main content

lemma_i8_bytes_roundtrip

vest_lib::combinators::sints::spec

Function lemma_i8_bytes_roundtrip 

Source 
pub broadcast proof fn lemma_i8_bytes_roundtrip(b: u8)
Expand description
ensures
#[trigger] ((b as i8) as u8) == b,