Splitting and rejoining byte strings

ByteArray counterpart of Util.Combine: extract lemmas for concatenations and splits.

def Cryptlib.Util.Bytes.ofVector {n : Nat} (v : Vector UInt8 n) : ByteArray

A fixed-width vector as a byte string.

Equations

• Cryptlib.Util.Bytes.ofVector v = { data := v.toArray }

@[simp]

theorem Cryptlib.Util.Bytes.size_ofVector {n : Nat} (v : Vector UInt8 n) : (ofVector v).size = n

def Cryptlib.Util.Bytes.toVecN (n : Nat) (a : ByteArray) : Vector UInt8 n

A ByteArray as a fixed-width vector; out-of-range bytes are 0.

Equations

• Cryptlib.Util.Bytes.toVecN n a = Vector.ofFn fun (i : Fin n) => a.get! ↑i

@[simp]

theorem Cryptlib.Util.Bytes.toVecN_ofVector {n : Nat} (v : Vector UInt8 n) : toVecN n (ofVector v) = v

toVecN undoes ofVector.

theorem Cryptlib.Util.Bytes.ofVector_toVecN {n : Nat} (X : ByteArray) (h : X.size = n) : ofVector (toVecN n X) = X

ofVector undoes toVecN.

theorem Cryptlib.Util.Bytes.extract_append_left (a b : ByteArray) : (a ++ b).extract 0 a.size = a

The left half of a concatenation.

theorem Cryptlib.Util.Bytes.extract_append_right (a b : ByteArray) : (a ++ b).extract a.size (a.size + b.size) = b

The right half of a concatenation.

theorem Cryptlib.Util.Bytes.extract_append_of_le (a b : ByteArray) {lo hi : Nat} (h : hi ≤ a.size) : (a ++ b).extract lo hi = a.extract lo hi

Extracting a range within the left half of a concatenation.

theorem Cryptlib.Util.Bytes.extract_append_ge (a b : ByteArray) {lo : Nat} (h : lo ≤ a.size) : (a ++ b).extract lo (a.size + b.size) = a.extract lo a.size ++ b

Extracting from an offset in the left half to the end of a concatenation.

theorem Cryptlib.Util.Bytes.extract_append_le (a b : ByteArray) {m : Nat} (h : a.size ≤ m) : (a ++ b).extract 0 m = a ++ b.extract 0 (m - a.size)

Extracting a prefix that extends past the left half of a concatenation.

theorem Cryptlib.Util.Bytes.extract_append_of_ge (a b : ByteArray) {lo hi : Nat} (h : a.size ≤ lo) : (a ++ b).extract lo hi = b.extract (lo - a.size) (hi - a.size)

Extracting a range within the right half of a concatenation, at shifted offsets.

theorem Cryptlib.Util.Bytes.append_extract (b : ByteArray) (n : Nat) (h : n ≤ b.size) : b.extract 0 n ++ b.extract n b.size = b

Splitting at any point and rejoining is the identity.