Skip to main content

lemma_to_from_be_bytes_roundtrip

vest_lib::primitives::base256

Function lemma_to_from_be_bytes_roundtrip 

Source 
pub proof fn lemma_to_from_be_bytes_roundtrip(n: nat)
Expand description
ensures
nat_from_be_bytes(nat_to_be_bytes(n)) == n,