		Search-engine friendly clone of the ACL2 documentation.

Bit/byte/integer-conversions

Leos2ip

The function \mathsf{LEOS2IP} in [ZPS:5.1].

Signature
(leos2ip s) → x
Arguments: s — Guard (byte-listp s).
Returns: x — Type (natp x).

The $\ell$ argument can be determined from the S argument: it is the length of S times 8. Thus, in our formalization we just have one argument.

Definitions and Theorems

Function: leos2ip

(defun leos2ip (s)
  (declare (xargs :guard (byte-listp s)))
  (let ((__function__ 'leos2ip))
    (declare (ignorable __function__))
    (acl2::lebytes=>nat s)))

Theorem: natp-of-leos2ip

(defthm natp-of-leos2ip
  (b* ((x (leos2ip s))) (natp x))
  :rule-classes :type-prescription)

Theorem: leos2ip-upper-bound

(defthm leos2ip-upper-bound
  (b* ((?x (leos2ip s)))
    (< x (expt 2 (* 8 (len s)))))
  :rule-classes :linear)

Theorem: leos2ip-injectivity

(defthm leos2ip-injectivity
  (implies (equal (len s1) (len s2))
           (equal (equal (leos2ip s1) (leos2ip s2))
                  (equal (acl2::byte-list-fix s1)
                         (acl2::byte-list-fix s2)))))