Function usize_from_be_bytes_exec 

pub exec fn usize_from_be_bytes_exec(bytes: &[u8]) -> result : usize

requires

bytes.len() <= size_of_usize(),

ensures

result as nat == nat_from_be_bytes(bytes.deep_view()),

Executable loop-based big-endian base-256 decoding into usize. Verified against the nat_from_be_bytes specification.