		Search-engine friendly clone of the ACL2 documentation.

Rlp-encoding

Rlp-scalar-encoding-p

Check if a byte array is an RLP encoding of a scalar.

This is analogous to rlp-tree-encoding-p.

The encoding of a scalar is also the encoding of the byte array that is the big endian representation of the scalar. The encoding of a byte array with no leading zeros is also the encoding of the scalar whose big endian representation is the byte array.

By definition, the witness function is right inverse of the encoding function, over the valid encodings.

Definitions and Theorems

Theorem: rlp-scalar-encoding-p-suff

(defthm rlp-scalar-encoding-p-suff
  (implies (and (natp scalar)
                (b* (((mv error? encoding1)
                      (rlp-encode-scalar scalar)))
                  (and (not error?)
                       (equal encoding1 (byte-list-fix encoding)))))
           (rlp-scalar-encoding-p encoding)))

Theorem: booleanp-of-rlp-scalar-encoding-p

(defthm booleanp-of-rlp-scalar-encoding-p
  (b* ((yes/no (rlp-scalar-encoding-p encoding)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: rlp-scalar-encoding-p-of-byte-list-fix-encoding

(defthm rlp-scalar-encoding-p-of-byte-list-fix-encoding
  (equal (rlp-scalar-encoding-p (byte-list-fix encoding))
         (rlp-scalar-encoding-p encoding)))

Theorem: rlp-scalar-encoding-p-byte-list-equiv-congruence-on-encoding

(defthm rlp-scalar-encoding-p-byte-list-equiv-congruence-on-encoding
  (implies (byte-list-equiv encoding encoding-equiv)
           (equal (rlp-scalar-encoding-p encoding)
                  (rlp-scalar-encoding-p encoding-equiv)))
  :rule-classes :congruence)

Theorem: natp-of-rlp-scalar-encoding-witness

(defthm natp-of-rlp-scalar-encoding-witness
  (implies (rlp-scalar-encoding-p encoding)
           (natp (rlp-scalar-encoding-witness encoding))))

Theorem: rlp-encode-scalar-of-rlp-scalar-encoding-witness

(defthm rlp-encode-scalar-of-rlp-scalar-encoding-witness
 (implies
  (rlp-scalar-encoding-p encoding)
  (b* (((mv error? encoding1)
        (rlp-encode-scalar (rlp-scalar-encoding-witness encoding))))
    (and (not error?)
         (equal encoding1 (byte-list-fix encoding))))))

Theorem: rlp-scalar-encoding-p-of-rlp-scalar-encode-when-no-error

(defthm rlp-scalar-encoding-p-of-rlp-scalar-encode-when-no-error
 (implies
     (not (mv-nth 0 (rlp-encode-scalar scalar)))
     (rlp-scalar-encoding-p (mv-nth 1 (rlp-encode-scalar scalar)))))

Theorem: rlp-bytes-encoding-p-when-rlp-scalar-encoding-p

(defthm rlp-bytes-encoding-p-when-rlp-scalar-encoding-p
  (implies (rlp-scalar-encoding-p encoding)
           (rlp-bytes-encoding-p encoding)))

Theorem: rlp-scalar-encoding-p-when-rlp-bytes-encoding-p-and-no-leading-zeros

(defthm
 rlp-scalar-encoding-p-when-rlp-bytes-encoding-p-and-no-leading-zeros
 (implies
   (and (rlp-bytes-encoding-p encoding)
        (equal (trim-bendian* (rlp-bytes-encoding-witness encoding))
               (rlp-bytes-encoding-witness encoding)))
   (rlp-scalar-encoding-p encoding)))