pub exec fn usize_to_be_bytes_exec(v: usize) -> buf : Vec<u8> ⓘExpand description
ensures
buf@ == nat_to_be_bytes(v as nat),Executable big-endian base-256 encoding from usize.
Verified against the nat_to_be_bytes specification.
This allocation-backed compatibility helper builds the result recursively.
Serialization hot paths should prefer usize_to_be_bytes_in_place.