		Search-engine friendly clone of the ACL2 documentation.

Rlp-big-endian-representations

Big-endian representation of scalars in RLP.

The library function nat=>bebytes* corresponds to \mathtt{BE} [YP:(181)]. Note that no leading 0 is allowed, even for representing 0, which is thus represented by the empty list of digits.

We introduce two linear rules that relate certain specific upper bounds on numbers and their big-endian representations in base 256. These upper bounds apply to the encoding of lengths in RLP.

Definitions and Theorems

Theorem: len-of-nat=>bebytes*-leq-8

(defthm len-of-nat=>bebytes*-leq-8
  (implies (< nat (expt 2 64))
           (<= (len (nat=>bebytes* nat)) 8))
  :rule-classes :linear)

Theorem: bebytes->nat-lt-2^64

(defthm bebytes->nat-lt-2^64
  (implies (<= (len digits) 8)
           (< (bebytes=>nat digits) (expt 2 64)))
  :rule-classes :linear)