hex

(in-package "STR")

(include-book "ieqv")

(include-book "std/basic/defs" :dir :system)

(include-book "std/util/deflist" :dir :system)

(include-book "ihs/basic-definitions" :dir :system)

(local (include-book "arithmetic"))

(local (include-book "centaur/bitops/ihs-extensions" :dir :system))

(local (defthm unsigned-byte-p-8-of-char-code
    (unsigned-byte-p 8 (char-code x))))

(local (in-theory (disable unsigned-byte-p digit-to-char)))

(local (defthm unsigned-byte-p-8-of-new-nibble-on-the-front
    (implies (and (unsigned-byte-p 4 a)
        (unsigned-byte-p n b))
      (unsigned-byte-p (+ 4 n)
        (+ b (ash a n))))
    :hints (("Goal" :in-theory (enable* ihsext-recursive-redefs ihsext-inductions)))))

(local (defthm unsigned-byte-p-8-of-new-nibble-on-the-front-alt
    (implies (and (unsigned-byte-p 4 a)
        (unsigned-byte-p n b))
      (unsigned-byte-p (+ 4 n)
        (+ (ash a n) b)))
    :hints (("Goal" :in-theory (enable* ihsext-recursive-redefs ihsext-inductions)))))

(local (defthm shift-left-of-sum-of-integers
    (implies (and (natp n) (integerp a) (integerp b))
      (equal (ash (+ a b) n)
        (+ (ash a n) (ash b n))))
    :hints (("Goal" :in-theory (enable* ihsext-recursive-redefs ihsext-inductions)))))

(local (defthm logtail-decreases
    (implies (and (posp n) (posp x))
      (< (logtail n x) x))
    :rule-classes ((:rewrite) (:linear))
    :hints (("Goal" :in-theory (enable* ihsext-recursive-redefs ihsext-inductions logcons)))))

(defsection hex
  :parents (numbers)
  :short "Functions for working with hexadecimal numbers in strings.")

(local (set-default-parents hex))

(define hex-digit-char-p
  (x)
  :short "Recognizer for hexadecimal digit characters: 0-9, A-F, a-f."
  :returns bool
  :long "<p>ACL2 provides @(see digit-char-p) which is more flexible and can
recognize numeric characters in other bases.  @(call hex-digit-char-p) only
recognizes base-16 digits, but is much faster, at least on CCL.  Here is an
experiment you can run in raw lisp, with times reported in CCL on an AMD
FX-8350.</p>

@({
  (defconstant *chars*
    (loop for i from 0 to 255 collect (code-char i)))

  ;; 19.216 seconds
  (time (loop for i fixnum from 1 to 10000000 do
              (loop for c in *chars* do (digit-char-p c 16))))

  ;; 4.711 seconds
  (time (loop for i fixnum from 1 to 10000000 do
              (loop for c in *chars* do (str::hex-digit-char-p c))))
})"
  :inline t
  (mbe :logic (let ((code (char-code (char-fix x))))
      (or (and (<= (char-code #\0) code)
          (<= code (char-code #\9)))
        (and (<= (char-code #\a) code)
          (<= code (char-code #\f)))
        (and (<= (char-code #\A) code)
          (<= code (char-code #\F)))))
    :exec (and (characterp x)
      (b* (((the (unsigned-byte 8) code) (char-code (the character x))))
        (if (<= code 70)
          (if (<= code 57)
            (<= 48 code)
            (<= 65 code))
          (and (<= code 102) (<= 97 code))))))
  ///
  (defcong ichareqv
    equal
    (hex-digit-char-p x)
    1
    :hints (("Goal" :in-theory (enable ichareqv downcase-char char-fix))))
  (defthm characterp-when-hex-digit-char-p
    (implies (hex-digit-char-p char)
      (characterp char))
    :rule-classes :compound-recognizer)
  (local (defun test
      (n)
      (let ((x (code-char n)))
        (and (iff (hex-digit-char-p x)
            (member x
              '(#\0 #\1
                #\2
                #\3
                #\4
                #\5
                #\6
                #\7
                #\8
                #\9
                #\a
                #\b
                #\c
                #\d
                #\e
                #\f
                #\A
                #\B
                #\C
                #\D
                #\E
                #\F)))
          (or (zp n) (test (- n 1)))))))
  (local (defthm l0
      (implies (and (test n)
          (natp i)
          (natp n)
          (<= i n))
        (let ((x (code-char i)))
          (iff (hex-digit-char-p x)
            (member x
              '(#\0 #\1
                #\2
                #\3
                #\4
                #\5
                #\6
                #\7
                #\8
                #\9
                #\a
                #\b
                #\c
                #\d
                #\e
                #\f
                #\A
                #\B
                #\C
                #\D
                #\E
                #\F)))))))
  (defthmd hex-digit-char-p-cases
    (iff (hex-digit-char-p x)
      (member x
        '(#\0 #\1
          #\2
          #\3
          #\4
          #\5
          #\6
          #\7
          #\8
          #\9
          #\a
          #\b
          #\c
          #\d
          #\e
          #\f
          #\A
          #\B
          #\C
          #\D
          #\E
          #\F)))
    :hints (("Goal" :in-theory (e/d (member) (l0))
       :use ((:instance l0 (n 255) (i (char-code x))))))))

(define nonzero-hex-digit-char-p
  (x)
  :short "Recognizer for non-zero hexadecimal digit characters: 1-9, A-F, a-f."
  :returns bool
  :inline t
  (mbe :logic (let ((code (char-code (char-fix x))))
      (or (and (<= (char-code #\1) code)
          (<= code (char-code #\9)))
        (and (<= (char-code #\a) code)
          (<= code (char-code #\f)))
        (and (<= (char-code #\A) code)
          (<= code (char-code #\F)))))
    :exec (and (characterp x)
      (b* (((the (unsigned-byte 8) code) (char-code (the character x))))
        (if (<= code 70)
          (if (<= code 57)
            (<= 49 code)
            (<= 65 code))
          (and (<= code 102) (<= 97 code))))))
  ///
  (defcong ichareqv
    equal
    (nonzero-hex-digit-char-p x)
    1
    :hints (("Goal" :in-theory (enable ichareqv downcase-char char-fix))))
  (defthm hex-digit-char-p-when-nonzero-hex-digit-char-p
    (implies (nonzero-hex-digit-char-p x)
      (hex-digit-char-p x))
    :hints (("Goal" :in-theory (enable hex-digit-char-p)))))

(define hex-digit-char-value
  :short "Coerces a @(see hex-digit-char-p) character into a number."
  ((x hex-digit-char-p))
  :split-types t
  :returns (val natp :rule-classes :type-prescription)
  :long "<p>For instance, @('(hex-digit-char-value #\a)') is 10.  For any non-@(see
         hex-digit-char-p), 0 is returned.</p>"
  :inline t
  (mbe :logic (b* (((unless (hex-digit-char-p x)) 0) (code (char-code x))
        ((when (<= (char-code #\a) code)) (- code (- (char-code #\a) 10)))
        ((when (<= (char-code #\A) code)) (- code (- (char-code #\A) 10))))
      (- code (char-code #\0)))
    :exec (b* (((the (unsigned-byte 8) code) (char-code (the character x))) ((when (<= 97 code)) (the (unsigned-byte 8) (- code 87)))
        ((when (<= 65 code)) (the (unsigned-byte 8) (- code 55))))
      (the (unsigned-byte 8) (- code 48))))
  :prepwork ((local (in-theory (enable hex-digit-char-p char-fix))))
  ///
  (defcong ichareqv
    equal
    (hex-digit-char-value x)
    1
    :hints (("Goal" :in-theory (enable ichareqv downcase-char))))
  (defthm hex-digit-char-value-upper-bound
    (< (hex-digit-char-value x) 16)
    :rule-classes ((:rewrite) (:linear)))
  (defthm unsigned-byte-p-of-hex-digit-char-value
    (unsigned-byte-p 4 (hex-digit-char-value x)))
  (defthm equal-of-hex-digit-char-value-and-hex-digit-char-value
    (implies (and (hex-digit-char-p x)
        (hex-digit-char-p y))
      (equal (equal (hex-digit-char-value x)
          (hex-digit-char-value y))
        (ichareqv x y)))
    :hints (("Goal" :in-theory (enable hex-digit-char-p-cases))))
  (defthm hex-digit-char-value-of-digit-to-char
    (implies (and (natp n) (< n 16))
      (equal (hex-digit-char-value (digit-to-char n))
        n))
    :hints (("Goal" :in-theory (enable digit-to-char)))))

(deflist hex-digit-char-list*p
  (x)
  :short "Recognizes lists of @(see hex-digit-char-p) characters."
  (hex-digit-char-p x)
  ///
  (defcong icharlisteqv
    equal
    (hex-digit-char-list*p x)
    1
    :hints (("Goal" :in-theory (enable icharlisteqv))))
  (defthm character-listp-when-hex-digit-char-list*p
    (implies (hex-digit-char-list*p x)
      (equal (character-listp x)
        (true-listp x)))
    :rule-classes ((:rewrite :backchain-limit-lst 1))))

(define hex-digit-chars-value1
  :parents (hex-digit-chars-value)
  ((x hex-digit-char-list*p) (val :type unsigned-byte))
  (if (consp x)
    (hex-digit-chars-value1 (cdr x)
      (the unsigned-byte
        (+ (the (unsigned-byte 4)
            (hex-digit-char-value (car x)))
          (the unsigned-byte
            (ash (mbe :logic (lnfix val) :exec val)
              4)))))
    (lnfix val)))

(define hex-digit-chars-value
  :short "Coerces a @(see hex-digit-char-list*p) into a natural number."
  ((x hex-digit-char-list*p))
  :returns (value natp :rule-classes :type-prescription)
  :long "<p>For instance, @('(hex-digit-chars-value '(#1 #F))') is 31.  See
         also @(see parse-hex-from-charlist) for a more flexible function that
         can tolerate non-hexadecimal characters after the number.</p>"
  :inline t
  :verify-guards nil
  (mbe :logic (if (consp x)
      (+ (ash (hex-digit-char-value (car x))
          (* 4 (1- (len x))))
        (hex-digit-chars-value (cdr x)))
      0)
    :exec (hex-digit-chars-value1 x 0))
  ///
  (defcong icharlisteqv
    equal
    (hex-digit-chars-value x)
    1
    :hints (("Goal" :in-theory (e/d (icharlisteqv)))))
  (defthm unsigned-byte-p-of-hex-digit-chars-value
    (unsigned-byte-p (* 4 (len x))
      (hex-digit-chars-value x)))
  (defthm hex-digit-chars-value-upper-bound
    (< (hex-digit-chars-value x)
      (expt 2 (* 4 (len x))))
    :rule-classes ((:rewrite) (:linear))
    :hints (("Goal" :in-theory (e/d (unsigned-byte-p)
         (unsigned-byte-p-of-hex-digit-chars-value))
       :use ((:instance unsigned-byte-p-of-hex-digit-chars-value)))))
  (defthm hex-digit-chars-value-upper-bound-free
    (implies (equal n (len x))
      (< (hex-digit-chars-value x)
        (expt 2 (* 4 n)))))
  (defthm hex-digit-chars-value1-removal
    (implies (natp val)
      (equal (hex-digit-chars-value1 x val)
        (+ (hex-digit-chars-value x)
          (ash (nfix val) (* 4 (len x))))))
    :hints (("Goal" :in-theory (enable hex-digit-chars-value1)
       :induct (hex-digit-chars-value1 x val))))
  (verify-guards hex-digit-chars-value$inline)
  (defthm hex-digit-chars-value-of-append
    (equal (hex-digit-chars-value (append x (list a)))
      (+ (ash (hex-digit-chars-value x) 4)
        (hex-digit-char-value a)))))

(define skip-leading-hex-digits
  (x)
  :short "Skip over any leading hex digit characters at the start of a character list."
  :returns (tail character-listp
    :hyp (character-listp x))
  (cond ((atom x) nil)
    ((hex-digit-char-p (car x)) (skip-leading-hex-digits (cdr x)))
    (t x))
  ///
  (local (defun ind
      (x y)
      (if (or (atom x) (atom y))
        (list x y)
        (ind (cdr x) (cdr y)))))
  (defcong charlisteqv
    charlisteqv
    (skip-leading-hex-digits x)
    1
    :hints (("Goal" :induct (ind x x-equiv))))
  (defcong icharlisteqv
    icharlisteqv
    (skip-leading-hex-digits x)
    1
    :hints (("Goal" :in-theory (enable icharlisteqv))))
  (defthm len-of-skip-leading-hex-digits
    (implies (hex-digit-char-p (car x))
      (< (len (skip-leading-hex-digits x))
        (len x)))))

(define take-leading-hex-digit-chars
  (x)
  :short "Collect any leading hex digit characters from the start of a character
          list."
  :returns (head character-listp
    :hyp (character-listp x))
  (cond ((atom x) nil)
    ((hex-digit-char-p (car x)) (cons (car x)
        (take-leading-hex-digit-chars (cdr x))))
    (t nil))
  ///
  (local (defun ind
      (x y)
      (if (or (atom x) (atom y))
        (list x y)
        (ind (cdr x) (cdr y)))))
  (defcong charlisteqv
    equal
    (take-leading-hex-digit-chars x)
    1
    :hints (("Goal" :induct (ind x x-equiv)
       :in-theory (enable charlisteqv))))
  (defcong icharlisteqv
    icharlisteqv
    (take-leading-hex-digit-chars x)
    1
    :hints (("Goal" :in-theory (enable icharlisteqv))))
  (defthm hex-digit-char-list*p-of-take-leading-hex-digit-chars
    (hex-digit-char-list*p (take-leading-hex-digit-chars x)))
  (defthm bound-of-len-of-take-leading-hex-digit-chars
    (<= (len (take-leading-hex-digit-chars x))
      (len x))
    :rule-classes :linear)
  (defthm equal-of-take-leading-hex-digit-chars-and-length
    (equal (equal (len (take-leading-hex-digit-chars x))
        (len x))
      (hex-digit-char-list*p x)))
  (defthm take-leading-hex-digit-chars-when-hex-digit-char-list*p
    (implies (hex-digit-char-list*p x)
      (equal (take-leading-hex-digit-chars x)
        (list-fix x))))
  (defthm consp-of-take-leading-hex-digit-chars
    (equal (consp (take-leading-hex-digit-chars x))
      (hex-digit-char-p (car x)))))

(define hex-digit-string-p-aux
  :parents (hex-digit-string-p)
  ((x stringp :type string) (n natp :type unsigned-byte)
    (xl (eql xl (length x)) :type unsigned-byte))
  :guard (<= n xl)
  :split-types t
  :verify-guards nil
  :enabled t
  (mbe :logic (hex-digit-char-list*p (nthcdr n (explode x)))
    :exec (if (eql n xl)
      t
      (and (hex-digit-char-p (char x n))
        (hex-digit-string-p-aux x
          (the unsigned-byte (+ 1 n))
          xl))))
  ///
  (verify-guards hex-digit-string-p-aux
    :hints (("Goal" :in-theory (enable hex-digit-char-list*p)))))

(define hex-digit-string-p
  :short "Recognizer for strings whose characters are hexadecimal digits."
  ((x :type string))
  :returns bool
  :long "<p>Corner case: this accepts the empty string since all of its
characters are hex digits.</p>

<p>Logically this is defined in terms of @(see hex-digit-char-list*p).  But in the
execution, we use a @(see char)-based function that avoids exploding the
string.  This provides much better performance, e.g., on an AMD FX-8350 with
CCL:</p>

@({
    ;; 0.97 seconds, no garbage
    (let ((x "deadbeef"))
      (time$ (loop for i fixnum from 1 to 10000000 do
                   (str::hex-digit-string-p x))))

    ;; 1.74 seconds, 1.28 GB allocated
    (let ((x "deadbeef"))
      (time$ (loop for i fixnum from 1 to 10000000 do
                   (str::hex-digit-char-list*p (explode x)))))
})"
  :inline t
  :enabled t
  (mbe :logic (hex-digit-char-list*p (explode x))
    :exec (hex-digit-string-p-aux x 0 (length x)))
  ///
  (defcong istreqv
    equal
    (hex-digit-string-p x)
    1))

(define hex-digit-to-char
  ((n :type (unsigned-byte 4)))
  :short "Convert a number from 0-15 into a hex character."
  :long "<p>ACL2 has a built-in version of this function, @(see digit-to-char),
but @('hex-digit-to-char') is faster:</p>

@({
  (defconstant *codes*
    (loop for i from 0 to 15 collect i))

  ;; .217 seconds, no garbage
  (time (loop for i fixnum from 1 to 10000000 do
              (loop for c in *codes* do (str::hex-digit-to-char c))))

  ;; .881 seconds, no garbage
  (time (loop for i fixnum from 1 to 10000000 do
              (loop for c in *codes* do (digit-to-char c))))

})"
  :guard-hints (("Goal" :in-theory (enable unsigned-byte-p digit-to-char)))
  :inline t
  :enabled t
  (mbe :logic (digit-to-char n)
    :exec (if (< n 10)
      (code-char (the (unsigned-byte 8) (+ 48 n)))
      (code-char (the (unsigned-byte 8) (+ 55 n))))))

(define basic-nat-to-hex-chars
  :parents (nat-to-hex-chars)
  :short "Logically simple definition that is similar to @(see nat-to-hex-chars)."
  ((n natp))
  :returns (chars hex-digit-char-list*p)
  :long "<p>This <i>almost</i> computes @('(nat-to-hex-chars n)'), but when @('n') is
zero it returns @('nil') instead of @('(#\0)').  You would normally never call
this function directly, but it is convenient for reasoning about @(see
nat-to-hex-chars).</p>"
  (if (zp n)
    nil
    (cons (hex-digit-to-char (logand n 15))
      (basic-nat-to-hex-chars (ash n -4))))
  :prepwork ((local (defthm l0
       (implies (and (< a 16)
           (< b 16)
           (natp a)
           (natp b))
         (equal (equal (digit-to-char a)
             (digit-to-char b))
           (equal a b)))
       :hints (("Goal" :in-theory (enable digit-to-char))))) (local (defthm l1
        (implies (and (< a 16) (natp a))
          (hex-digit-char-p (digit-to-char a)))
        :hints (("Goal" :in-theory (enable digit-to-char)))))
    (local (in-theory (disable digit-to-char))))
  ///
  (defthm basic-nat-to-hex-chars-when-zp
    (implies (zp n)
      (equal (basic-nat-to-hex-chars n) nil)))
  (defthm true-listp-of-basic-nat-to-hex-chars
    (true-listp (basic-nat-to-hex-chars n))
    :rule-classes :type-prescription)
  (defthm character-listp-of-basic-nat-to-hex-chars
    (character-listp (basic-nat-to-hex-chars n)))
  (defthm basic-nat-to-hex-chars-under-iff
    (iff (basic-nat-to-hex-chars n)
      (not (zp n))))
  (defthm consp-of-basic-nat-to-hex-chars
    (equal (consp (basic-nat-to-hex-chars n))
      (if (basic-nat-to-hex-chars n)
        t
        nil)))
  (local (defun my-induction
      (n m)
      (if (or (zp n) (zp m))
        nil
        (my-induction (ash n -4) (ash m -4)))))
  (local (defthm c0
      (implies (and (integerp x) (natp n))
        (equal (logior (ash (logtail n x) n)
            (loghead n x))
          x))
      :hints (("Goal" :in-theory (enable* ihsext-recursive-redefs ihsext-inductions)))))
  (local (defthm c1
      (implies (and (equal (logtail k n) (logtail k m))
          (equal (loghead k n) (loghead k m))
          (integerp n)
          (integerp m)
          (natp k))
        (equal (equal n m) t))
      :hints (("Goal" :in-theory (disable c0)
         :use ((:instance c0 (x n) (n k)) (:instance c0 (x m) (n k)))))))
  (defthm basic-nat-to-hex-chars-one-to-one
    (equal (equal (basic-nat-to-hex-chars n)
        (basic-nat-to-hex-chars m))
      (equal (nfix n) (nfix m)))
    :hints (("Goal" :induct (my-induction n m)))))

(define nat-to-hex-chars-aux
  ((n natp) acc)
  :parents (nat-to-hex-chars)
  :verify-guards nil
  :enabled t
  (mbe :logic (revappend (basic-nat-to-hex-chars n) acc)
    :exec (if (zp n)
      acc
      (nat-to-hex-chars-aux (the unsigned-byte (ash (the unsigned-byte n) -4))
        (cons (hex-digit-to-char (the (unsigned-byte 4)
              (logand (the unsigned-byte n) 15)))
          acc))))
  ///
  (verify-guards nat-to-hex-chars-aux
    :hints (("Goal" :in-theory (enable basic-nat-to-hex-chars)))))

(define nat-to-hex-chars
  :short "Convert a natural number into a list of hexadecimal bits."
  ((n natp))
  :returns (chars hex-digit-char-list*p)
  :long "<p>For instance, @('(nat-to-hex-chars 31)') is @('(#\1 #\F)').</p>

<p>This is like ACL2's built-in function @(see explode-nonnegative-integer),
except that it doesn't deal with accumulators and is limited to base-16 numbers.
These simplifications lead to particularly nice rules, e.g., about @(see
hex-digit-chars-value), and somewhat better performance:</p>

@({
  ;; Times reported by an AMD FX-8350, Linux, 64-bit CCL:

  ;; .732 seconds, 942 MB allocated
  (progn (gc$)
         (time (loop for i fixnum from 1 to 10000000 do
                     (str::nat-to-hex-chars i))))

  ;; 3.71 seconds, 942 MB allocated
  (progn (gc$)
         (time (loop for i fixnum from 1 to 10000000 do
            (explode-nonnegative-integer i 16 nil))))
})"
  :inline t
  (or (nat-to-hex-chars-aux n nil) '(#\0))
  ///
  (defthm true-listp-of-nat-to-hex-chars
    (and (true-listp (nat-to-hex-chars n))
      (consp (nat-to-hex-chars n)))
    :rule-classes :type-prescription)
  (defthm character-listp-of-nat-to-hex-chars
    (character-listp (nat-to-hex-chars n)))
  (local (defthm lemma1
      (equal (equal (rev x) (list y))
        (and (consp x)
          (not (consp (cdr x)))
          (equal (car x) y)))
      :hints (("Goal" :in-theory (enable rev)))))
  (local (defthm crock
      (implies (and (equal (logtail n x) 0)
          (equal (loghead n x) 0)
          (natp n))
        (zip x))
      :rule-classes :forward-chaining :hints (("Goal" :in-theory (enable* ihsext-inductions ihsext-recursive-redefs zip zp)))))
  (local (defthm crock2
      (implies (and (equal (logtail n x) 0)
          (not (zp x))
          (natp n))
        (< 0 (loghead n x)))
      :hints (("Goal" :in-theory (enable* ihsext-inductions ihsext-recursive-redefs)))))
  (local (defthm crock3
      (equal (equal (digit-to-char n) #\0)
        (or (zp n) (< 15 n)))
      :hints (("Goal" :in-theory (enable digit-to-char)))))
  (local (defthmd lemma2
      (not (equal (basic-nat-to-hex-chars n) '(#\0)))
      :hints (("Goal" :in-theory (enable* basic-nat-to-hex-chars
           ihsext-recursive-redefs)))))
  (defthm nat-to-hex-chars-one-to-one
    (equal (equal (nat-to-hex-chars n)
        (nat-to-hex-chars m))
      (equal (nfix n) (nfix m)))
    :hints (("Goal" :in-theory (disable basic-nat-to-hex-chars-one-to-one)
       :use ((:instance basic-nat-to-hex-chars-one-to-one) (:instance lemma2)
         (:instance lemma2 (n m))))))
  (local (defthm c0
      (implies (and (integerp x) (natp n))
        (equal (+ (loghead n x)
            (ash (logtail n x) n))
          x))
      :hints (("Goal" :in-theory (enable* ihsext-recursive-redefs ihsext-inductions)))))
  (local (defthm hex-digit-chars-value-of-rev-of-basic-nat-to-hex-chars
      (equal (hex-digit-chars-value (rev (basic-nat-to-hex-chars n)))
        (nfix n))
      :hints (("Goal" :induct (basic-nat-to-hex-chars n)
         :in-theory (enable* basic-nat-to-hex-chars
           ihsext-recursive-redefs
           logcons)))))
  (defthm hex-digit-chars-value-of-nat-to-hex-chars
    (equal (hex-digit-chars-value (nat-to-hex-chars n))
      (nfix n))))

(define revappend-nat-to-hex-chars-aux
  ((n natp) (acc))
  :parents (revappend-nat-to-hex-chars)
  :enabled t
  :verify-guards nil
  (mbe :logic (append (basic-nat-to-hex-chars n) acc)
    :exec (if (zp n)
      acc
      (cons (hex-digit-to-char (the (unsigned-byte 4)
            (logand (the unsigned-byte n) 15)))
        (revappend-nat-to-hex-chars-aux (the unsigned-byte (ash (the unsigned-byte n) -4))
          acc))))
  ///
  (verify-guards revappend-nat-to-hex-chars-aux
    :hints (("Goal" :in-theory (enable basic-nat-to-hex-chars)))))

(define revappend-nat-to-hex-chars
  :short "More efficient version of @('(revappend (nat-to-hex-chars n) acc).')"
  ((n natp) (acc))
  :returns (new-acc)
  :long "<p>This strange operation can be useful when building strings by consing
         together characters in reverse order.</p>"
  :inline t
  :enabled t
  :prepwork ((local (in-theory (enable nat-to-hex-chars))))
  (mbe :logic (revappend (nat-to-hex-chars n) acc)
    :exec (if (zp n)
      (cons #\0 acc)
      (revappend-nat-to-hex-chars-aux n acc))))

(define nat-to-hex-string
  :short "Convert a natural number into a string with its hex digits."
  ((n natp))
  :returns (str stringp :rule-classes :type-prescription)
  :long "<p>For instance, @('(nat-to-hex-string 31)') is @('"1F"').</p>"
  :inline t
  (implode (nat-to-hex-chars n))
  ///
  (defthm hex-digit-char-list*p-of-nat-to-dec-string
    (hex-digit-char-list*p (explode (nat-to-hex-string n))))
  (defthm nat-to-hex-string-one-to-one
    (equal (equal (nat-to-hex-string n)
        (nat-to-hex-string m))
      (equal (nfix n) (nfix m))))
  (defthm hex-digit-chars-value-of-nat-to-dec-string
    (equal (hex-digit-chars-value (explode (nat-to-hex-string n)))
      (nfix n)))
  (defthm nat-to-hex-string-nonempty
    (not (equal (nat-to-hex-string n) ""))))

(define nat-to-hex-string-list
  :short "Convert a list of natural numbers into a list of hex digit strings."
  ((x nat-listp))
  :returns (strs string-listp)
  (if (atom x)
    nil
    (cons (nat-to-hex-string (car x))
      (nat-to-hex-string-list (cdr x))))
  ///
  (defthm nat-to-hex-string-list-when-atom
    (implies (atom x)
      (equal (nat-to-hex-string-list x) nil)))
  (defthm nat-to-hex-string-list-of-cons
    (equal (nat-to-hex-string-list (cons a x))
      (cons (nat-to-hex-string a)
        (nat-to-hex-string-list x)))))

(define nat-to-hex-string-size-aux
  :parents (nat-to-hex-string-size)
  ((n natp))
  :returns (size natp :rule-classes :type-prescription)
  (if (zp n)
    0
    (+ 1 (nat-to-hex-string-size-aux (ash n -4))))
  :prepwork ((local (in-theory (enable nat-to-hex-chars))))
  ///
  (defthm nat-to-hex-string-size-aux-redef
    (equal (nat-to-hex-string-size-aux n)
      (len (basic-nat-to-hex-chars n)))
    :hints (("Goal" :in-theory (enable basic-nat-to-hex-chars)))))

(define nat-to-hex-string-size
  :short "Number of characters in the hexadecimal representation of a natural."
  ((x natp))
  :returns (size posp :rule-classes :type-prescription)
  :inline t
  (mbe :logic (len (nat-to-hex-chars x))
    :exec (if (zp x)
      1
      (nat-to-hex-string-size-aux x)))
  :prepwork ((local (in-theory (enable nat-to-hex-chars)))))

(define parse-hex-from-charlist
  :short "Parse a hexadecimal number from the beginning of a character list."
  ((x character-listp "Characters to read from.") (val natp
      "Accumulator for the value of the hex digits we have read
                         so far; typically 0 to start with.")
    (len natp
      "Accumulator for the number of hex digits we have read;
                         typically 0 to start with."))
  :returns (mv (val "Value of the initial hex digits as a natural number.")
    (len "Number of initial hex digits we read.")
    (rest "The rest of @('x'), past the leading hex digits."))
  :split-types t
  (declare (type unsigned-byte val len))
  :long "<p>This is like @(call parse-nat-from-charlist), but deals with hex
         digits and returns their hexadecimal value.</p>"
  (cond ((atom x) (mv (lnfix val) (lnfix len) nil))
    ((hex-digit-char-p (car x)) (parse-hex-from-charlist (cdr x)
        (the unsigned-byte
          (+ (the unsigned-byte (hex-digit-char-value (car x)))
            (the unsigned-byte
              (ash (the unsigned-byte (lnfix val)) 4))))
        (the unsigned-byte
          (+ 1 (the unsigned-byte (lnfix len))))))
    (t (mv (lnfix val) (lnfix len) x)))
  ///
  (defthm val-of-parse-hex-from-charlist
    (equal (mv-nth 0
        (parse-hex-from-charlist x val len))
      (+ (hex-digit-chars-value (take-leading-hex-digit-chars x))
        (ash (nfix val)
          (* 4 (len (take-leading-hex-digit-chars x))))))
    :hints (("Goal" :in-theory (enable take-leading-hex-digit-chars
         hex-digit-chars-value))))
  (defthm len-of-parse-hex-from-charlist
    (equal (mv-nth 1
        (parse-hex-from-charlist x val len))
      (+ (nfix len)
        (len (take-leading-hex-digit-chars x))))
    :hints (("Goal" :in-theory (enable take-leading-hex-digit-chars))))
  (defthm rest-of-parse-hex-from-charlist
    (equal (mv-nth 2
        (parse-hex-from-charlist x val len))
      (skip-leading-hex-digits x))
    :hints (("Goal" :in-theory (enable skip-leading-hex-digits)))))

(define parse-hex-from-string
  :short "Parse a hexadecimal number from a string, at some offset."
  ((x stringp "The string to parse.") (val natp
      "Accumulator for the value we have parsed so far; typically 0 to
                 start with.")
    (len natp
      "Accumulator for the number of hex digits we have parsed so far;
                 typically 0 to start with.")
    (n natp
      "Offset into @('x') where we should begin parsing.  Must be a valid
                 index into the string, i.e., @('0 <= n < (length x)').")
    (xl (eql xl (length x))
      "Pre-computed length of @('x')."))
  :guard (<= n xl)
  :returns (mv (val "The value of the hex digits we parsed."
      natp
      :rule-classes :type-prescription)
    (len "The number of hex digits we parsed."
      natp
      :rule-classes :type-prescription))
  :split-types t
  (declare (type string x)
    (type unsigned-byte val len n xl))
  :verify-guards nil
  :enabled t
  :long "<p>This function is flexible but very complicated.  See @(see strval16)
for a very simple alternative that may do what you want.</p>

<p>The final @('val') and @('len') are guaranteed to be natural numbers;
failure is indicated by a return @('len') of zero.</p>

<p>Because of leading zeroes, the @('len') may be much larger than you would
expect based on @('val') alone.  The @('len') argument is generally useful if
you want to continue parsing through the string, i.e., the @('n') you started
with plus the @('len') you got out will be the next position in the string
after the number.</p>

<p>See also @(see parse-hex-from-charlist) for a simpler function that reads a
number from the start of a character list.  This function also serves as part
of our logical definition.</p>"
  (mbe :logic (b* (((mv val len ?rest) (parse-hex-from-charlist (nthcdr n (explode x))
           val
           len)))
      (mv val len))
    :exec (b* (((when (eql n xl)) (mv val len)) ((the character char) (char (the string x) (the unsigned-byte n)))
        ((when (hex-digit-char-p char)) (parse-hex-from-string (the string x)
            (the unsigned-byte
              (+ (the unsigned-byte (hex-digit-char-value char))
                (the unsigned-byte (ash (the unsigned-byte val) 4))))
            (the unsigned-byte (+ 1 (the unsigned-byte len)))
            (the unsigned-byte (+ 1 n))
            (the unsigned-byte xl))))
      (mv val len)))
  ///
  (local (in-theory (disable bound-of-len-of-take-leading-hex-digit-chars
        right-shift-to-logtail
        hex-digit-char-list*p-of-cdr-when-hex-digit-char-list*p)))
  (verify-guards parse-hex-from-string
    :hints (("Goal" :in-theory (enable parse-hex-from-charlist
         take-leading-hex-digit-chars
         hex-digit-chars-value)))))

(define strval16
  :short "Interpret a string as a hexadecimal number."
  ((x stringp))
  :returns (value? (or (natp value?) (not value?))
    :rule-classes :type-prescription)
  :long "<p>For example, @('(strval16 "1F")') is 31.  If the string is empty
or has any non hexadecimal digit characters (0-9, A-F, a-f), we return
@('nil').</p>"
  :split-types t
  (declare (type string x))
  (mbe :logic (let ((chars (explode x)))
      (and (consp chars)
        (hex-digit-char-list*p chars)
        (hex-digit-chars-value chars)))
    :exec (b* (((the unsigned-byte xl) (length x)) ((mv (the unsigned-byte val)
           (the unsigned-byte len)) (parse-hex-from-string x 0 0 0 xl)))
      (and (not (eql 0 len)) (eql len xl) val)))
  ///
  (defcong istreqv equal (strval16 x) 1))