|
|
|---|
|
|
|
|---|
Bytes.
In Bitcoin, as in most modern contexts, the unqualified term `byte' denotes an unsigned 8-bit byte.
We use the library type byte to model bytes in our Bitcoin model.
Theorem:
(defthm natp-of-byte-fix (natp (byte-fix x)) :rule-classes :type-prescription)
Theorem:
(defthm byte-fix-upper-bound (< (byte-fix x) 256) :rule-classes :linear)