@[irreducible]

def Cryptlib.Util.newnat.natToBytesAux (n : Nat) (acc : List UInt8) : List UInt8

Equations

• Cryptlib.Util.newnat.natToBytesAux n acc = if (n == 0) = true then acc else Cryptlib.Util.newnat.natToBytesAux (n / 256) (UInt8.ofNat (n % 256) :: acc)

def Cryptlib.Util.newnat.natToBytes (n : Nat) : ByteArray

Equations

• Cryptlib.Util.newnat.natToBytes n = { data := (Cryptlib.Util.newnat.natToBytesAux n []).toArray }

theorem Cryptlib.Util.newnat.natToBytesAux_length_le (k n : Nat) (acc : List UInt8) : n < 256 ^ k → (natToBytesAux n acc).length ≤ acc.length + k

theorem Cryptlib.Util.newnat.natToBytes_length_le_32 (n : Nat) (h : n < 256 ^ 32) : (natToBytes n).data.toList.length ≤ 32