Byte-arrays
Byte arrays.
[YP:3] mentions the set \mathbb{B} of byte arrays,
and [YP:(178)] defines it as consisting of all finite sequences of bytes.
We use the library type byte-list to model \mathbb{B}.
[YP:3] also introduces the notation \mathbb{B}_k to denote
the set of byte arrays of length k.
We use the library types
byte-list20, byte-list32, and byte-list64
to model \mathbb{B}_k for k\in\{20,32,64\}.
Arrays of 20 bytes may represent addresses [YP:4.1].
Arrays of 32 bytes may represent Keccak-256 hashes.
Arrays of 64 bytes may represent Keccak-512 hashes.
Definitions and Theorems
Theorem: nat-listp-when-byte-listp
(defthm nat-listp-when-byte-listp
(implies (byte-listp bytes)
(nat-listp bytes)))
Theorem: car-of-byte-list-fix
(defthm car-of-byte-list-fix
(implies (consp x)
(equal (car (byte-list-fix x))
(byte-fix (car x)))))
Theorem: cdr-of-byte-list-fix
(defthm cdr-of-byte-list-fix
(equal (cdr (byte-list-fix x))
(byte-list-fix (cdr x))))
Theorem: byte-list-fix-rewrite-unsigned-byte-list-fix
(defthm byte-list-fix-rewrite-unsigned-byte-list-fix
(equal (byte-list-fix x)
(unsigned-byte-list-fix 8 x)))
