Function integer_fmt 

pub open spec fn integer_fmt() -> IntegerInnerFmt

{
    Mapped {
        inner: Refined(Tail, |bytes: Seq<u8>| integer_bytes_wf(bytes)),
        mapper: (|bytes: Seq<u8>| int_from_be_bytes(bytes), |o: int| int_to_be_bytes(o)),
    }
}