Function nat_from_be_bytes 

pub open spec fn nat_from_be_bytes(bytes: Seq<u8>) -> nat

{
    if bytes.len() == 0 {
        0
    } else {
        nat_from_be_bytes(bytes.drop_last()) * 256 + bytes.last() as nat
    }
}

Unsigned big-endian base-256 decoding.