Little-endian byte encodings of naturals

The one encoder every fixed-width serialization in CompPoly is built from: a natural number becomes exactly w bytes, least significant first, and w bytes become a natural.

• toListLE w n / ofListLE on List UInt8, with the round-trip laws ofListLE_toListLE (as n % 256 ^ w, hence exact below 256 ^ w) and toListLE_ofListLE, and the concatenation law ofListLE_append.
• toVecLE / ofVecLE and toByteArrayLE / ofByteArrayLE, the same maps on Vector UInt8 w and ByteArray.
• bytesFor bound, the number of bytes needed to hold every natural below bound, with le_pow_bytesFor : bound ≤ 256 ^ bytesFor bound. It is Nat.log2-based so that the kernel evaluates it on numerals by decide.

The layout is the one arkworks and plonky3 use for field elements: the canonical integer, little-endian, padded to a fixed width.

Lists

def CompPoly.Bytes.toListLE : ℕ → ℕ → List UInt8

The w little-endian bytes of n; bits above 8 * w are dropped.

def CompPoly.Bytes.ofListLE : List UInt8 → ℕ

The natural with the given little-endian bytes.

@[simp]

theorem CompPoly.Bytes.toListLE_zero (n : ℕ) : toListLE 0 n = []

@[simp]

theorem CompPoly.Bytes.toListLE_succ (w n : ℕ) : toListLE (w + 1) n = UInt8.ofNat (n % 256) :: toListLE w (n / 256)

@[simp]

theorem CompPoly.Bytes.ofListLE_nil : ofListLE [] = 0

@[simp]

theorem CompPoly.Bytes.ofListLE_cons (b : UInt8) (bs : List UInt8) : ofListLE (b :: bs) = b.toNat + 256 * ofListLE bs

@[simp]

theorem CompPoly.Bytes.length_toListLE (w n : ℕ) : (toListLE w n).length = w

theorem CompPoly.Bytes.ofListLE_toListLE (w n : ℕ) : ofListLE (toListLE w n) = n % 256 ^ w

theorem CompPoly.Bytes.ofListLE_toListLE_of_lt {w n : ℕ} (h : n < 256 ^ w) : ofListLE (toListLE w n) = n

theorem CompPoly.Bytes.ofListLE_lt (l : List UInt8) : ofListLE l < 256 ^ l.length

theorem CompPoly.Bytes.toListLE_ofListLE (l : List UInt8) : toListLE l.length (ofListLE l) = l

theorem CompPoly.Bytes.toListLE_inj_of_lt {w n m : ℕ} (hn : n < 256 ^ w) (hm : m < 256 ^ w) (h : toListLE w n = toListLE w m) : n = m

theorem CompPoly.Bytes.ofListLE_append (l₁ l₂ : List UInt8) : ofListLE (l₁ ++ l₂) = ofListLE l₁ + 256 ^ l₁.length * ofListLE l₂

Widths

def CompPoly.Bytes.bytesFor (bound : ℕ) : ℕ

The number of bytes needed to hold every natural below bound: one byte for bound ≤ 256, and in general the least w with bound ≤ 256 ^ w, except that bound ≤ 1 still takes one byte. Defined through Nat.log2 so that the kernel evaluates it on numerals.

theorem CompPoly.Bytes.bytesFor_pos (bound : ℕ) : 0 < bytesFor bound

theorem CompPoly.Bytes.le_pow_bytesFor (bound : ℕ) : bound ≤ 256 ^ bytesFor bound

theorem CompPoly.Bytes.bytesFor_two_pow {k : ℕ} (hk : 0 < k) : bytesFor (2 ^ k) = (k + 7) / 8

The width of a power of two: k bits need ⌈k / 8⌉ bytes. Stated so that a bit-pattern type's width is a small numeral computation rather than a kernel evaluation of 2 ^ k.

Vectors

def CompPoly.Bytes.toVecLE (w n : ℕ) : Vector UInt8 w

The w little-endian bytes of n as a vector.

def CompPoly.Bytes.ofVecLE {w : ℕ} (v : Vector UInt8 w) : ℕ

The natural with the given little-endian bytes.

@[simp]

theorem CompPoly.Bytes.toList_toVecLE (w n : ℕ) : (toVecLE w n).toList = toListLE w n

theorem CompPoly.Bytes.ofVecLE_toVecLE (w n : ℕ) : ofVecLE (toVecLE w n) = n % 256 ^ w

theorem CompPoly.Bytes.ofVecLE_toVecLE_of_lt {w n : ℕ} (h : n < 256 ^ w) : ofVecLE (toVecLE w n) = n

theorem CompPoly.Bytes.ofVecLE_lt {w : ℕ} (v : Vector UInt8 w) : ofVecLE v < 256 ^ w

theorem CompPoly.Bytes.toVecLE_ofVecLE {w : ℕ} (v : Vector UInt8 w) : toVecLE w (ofVecLE v) = v

theorem CompPoly.Bytes.toVecLE_inj_of_lt {w n m : ℕ} (hn : n < 256 ^ w) (hm : m < 256 ^ w) (h : toVecLE w n = toVecLE w m) : n = m

Byte arrays

def CompPoly.Bytes.toByteArrayLE (w n : ℕ) : ByteArray

The w little-endian bytes of n as a ByteArray.

def CompPoly.Bytes.ofByteArrayLE (b : ByteArray) : ℕ

The natural with the given little-endian bytes.

@[simp]

theorem CompPoly.Bytes.size_toByteArrayLE (w n : ℕ) : (toByteArrayLE w n).size = w

@[simp]

theorem CompPoly.Bytes.data_toByteArrayLE (w n : ℕ) : (toByteArrayLE w n).data = (toListLE w n).toArray

theorem CompPoly.Bytes.ofByteArrayLE_toByteArrayLE (w n : ℕ) : ofByteArrayLE (toByteArrayLE w n) = n % 256 ^ w

theorem CompPoly.Bytes.ofByteArrayLE_toByteArrayLE_of_lt {w n : ℕ} (h : n < 256 ^ w) : ofByteArrayLE (toByteArrayLE w n) = n

theorem CompPoly.Bytes.toByteArrayLE_inj_of_lt {w n m : ℕ} (hn : n < 256 ^ w) (hm : m < 256 ^ w) (h : toByteArrayLE w n = toByteArrayLE w m) : n = m