Skip to main content

lemma_u24_be_from_bytes_range

vest_lib::combinators::uints::spec

Function lemma_u24_be_from_bytes_range 

Source 
pub proof fn lemma_u24_be_from_bytes_range(i: [u8; 3])
Expand description
ensures
u24_be_from_bytes(i) < 0x01000000,