• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
      • Crypto-hdwallet
      • Apt
      • Error-checking
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Set
      • C
        • Syntax-for-tools
          • Formalized-subset
          • Mapping-to-language-definition
          • Input-files
          • Compilation-database
          • Printer
          • Output-files
          • Abstract-syntax-operations
          • Implementation-environments
          • Abstract-syntax
          • Concrete-syntax
          • Disambiguation
          • Validation
          • Gcc-builtins
          • Preprocessing
          • Parsing
            • Parser
              • Parse-exprs/decls/stmts
              • Parser-states
              • Parse-external-declaration
              • Parse-cast-expression
              • Parse-expression-or-type-name
              • Parse-postfix-expression
              • Lexer
                • Check-full-ppnumber
                • Lex-lexeme
                • Lex-oct-iconst-/-dec-fconst
                • Lex-?-integer-suffix
                • Lex-hex-iconst/fconst
                • Lex-identifier/keyword
                • Lex-dec-iconst/fconst
                • Lex-block-comment
                • Lex-escape-sequence
                • Read-token
                • Lex-*-hexadecimal-digit
                • Lex-?-floating-suffix
                • Lex-*-c-char
                • Lex-*-s-char
                • Lex-prepr-directive
                • Lex-line-comment
                • Lex-*-digit
                • Lex-*-q-char
                • Lex-*-h-char
                • Lex-iconst/fconst
                • Lex-?-exponent-part
                • Lex-character-constant
                • Lexeme
                • Lex-string-literal
                • Lex-dec-fconst
                • Reread-to-token
                • Lex-non-octal-digit
                • Lex-hexadecimal-digit
                • Lex-header-name
                • Lex-binary-exponent-part
                • Lex-exponent-part
                • Lex-?-sign
                • Only-whitespace-backward-through-line
                • Lexeme-option
                • Lex-hex-quad
                • Unread-to-token
                • Read-stringlit
                • Unread-tokens
                • Read-identifier
                • Read-punctuator
                • Read-keyword
                • Unread-token
                • Irr-lexeme
              • Parse-primary-expression
              • Token-unary-expression-start-p
              • Parse-declaration-specifier
              • Parse-declaration-specifiers
              • Parse-unary-expression-or-parenthesized-type-name
              • Parse-asm-name-specifier
              • Parse-specifier/qualifier
              • Parse-expression-rest
              • Token-type-specifier-keyword-p
              • Parse-fileset
              • Parse-*-external-declaration
              • Parse-declarator-or-abstract-declarator
              • Parse-asm-goto-labels
              • Parse-asm-clobbers
              • Parse-translation-unit
              • Parse-*-label-declaration
              • Token-postfix-expression-rest-start-p
              • Parse-?-asm-name-specifier
              • Parse-*-comma-identifier
              • Parse-postfix-expression-rest
              • Parse-expression
              • Make-expr-unary-with-preinc/predec-ops
              • Parse-*-stringlit
              • Parse-statement
              • Token-struct-declaration-start-p
              • Parse-*-attribute-specifier
              • Parse-initializer-list
              • Parse-file
              • Parse-pointer
              • Parse-label-declaration
              • Parse-array/function-declarator
              • Token-type-qualifier-p
              • Parse-*-asm-qualifier
              • Parse-parameter-declaration
              • Parse-attribute-name
              • Parse-argument-expressions
              • Make-expr-cast/add-or-cast/sub-ambig
              • Parse-struct-or-union-specifier
              • Parse-declaration-or-statement
              • Parse-assignment-expression
              • Parse-asm-clobber
              • Token-specifier/qualifier-start-p
              • Token-primary-expression-start-p
              • Token-function-specifier-p
              • Token-expression-start-p
              • Parse-*-increment/decrement
              • Parse-direct-abstract-declarator
              • Parse-compound-statement
              • Token-to-type-specifier-keyword
              • Parse-unary-expression
              • Parse-argument-expressions-rest
              • Parse-generic-associations-rest
              • Parse-conditional-expression
              • Parse-fileset-loop
              • Parse-direct-abstract-declarator-rest
              • Token-designation?-initializer-start-p
              • Token-declaration-specifier-start-p
              • Parse-designator-list
              • Token-abstract-declarator-start-p
              • Parse-?-asm-output-operands
              • Parse-?-asm-input-operands
              • Parse-struct-declaration
              • Parse-specifier-qualifier-list
              • Parse-parameter-declaration-list
              • Parse-constant-expression
              • Token-type-specifier-start-p
              • Token-type-qualifier-or-attribute-specifier-start-p
              • Parse-static-assert-declaration
              • Parse-direct-declarator
              • Parse-declaration
              • Parse-attribute-parameters
              • Token-unary-operator-p
              • Token-to-unary-operator
              • Token-to-type-qualifier
              • Token-storage-class-specifier-p
              • Token-initializer-start-p
              • Token-direct-abstract-declarator-start-p
              • Token-declarator-start-p
              • Parse-initializer
              • Parse-direct-declarator-rest
              • Token-to-storage-class-specifier
              • Token-to-assignment-operator
              • Token-to-asm-qualifier
              • Token-struct-declarator-start-p
              • Token-direct-declarator-start-p
              • Token-assignment-operator-p
              • Parse-type-qualifier-and-attribute-specifier-list
              • Parse-enumerator-list
              • Parse-designation?-initializer
              • Parse-compound-literal
              • Parse-block-item
              • Token-type-name-start-p
              • Token-to-function-specifier
              • Token-preinc/predec-operator-p
              • Token-multiplicative-operator-p
              • Token-designator-start-p
              • Token-designation-start-p
              • Parse-generic-association
              • Parse-declaration-list
              • Parse-attribute-specifier
              • Parse-asm-output-operands
              • Token-to-relational-operator
              • Token-to-preinc/predec-operator
              • Token-to-multiplicative-operator
              • Token-relational-operator-p
              • Token-equality-operator-p
              • Token-asm-qualifier-p
              • Token-additive-operator-p
              • Parse-asm-statement
              • Parse-asm-input-operands
              • Token-to-equality-operator
              • Token-to-additive-operator
              • Token-shift-operator-p
              • Parser-messages
              • Parse-type-name
              • Parse-struct-declarator-list
              • Parse-struct-declaration-list
              • Parse-relational-expression-rest
              • Parse-multiplicative-expression-rest
              • Parse-logical-or-expression-rest
              • Parse-logical-and-expression-rest
              • Parse-inclusive-or-expression-rest
              • Parse-exclusive-or-expression-rest
              • Parse-equality-expression-rest
              • Parse-array/function-abstract-declarator
              • Parse-additive-expression-rest
              • Token-to-shift-operator
              • Parse-struct-declarator
              • Parse-shift-expression-rest
              • Parse-member-designor
              • Parse-init-declarator-list
              • Parse-init-declarator
              • Parse-designator
              • Parse-and-expression-rest
              • Parse-alignment-specifier
              • Reader
              • Parse-shift-expression
              • Parse-relational-expression
              • Parse-multiplicative-expression
              • Parse-logical-or-expression
              • Parse-logical-and-expression
              • Parse-inclusive-or-expression
              • Parse-exclusive-or-expression
              • Parse-equality-expression
              • Parse-enum-specifier
              • Parse-block-item-list
              • Parse-attribute-list
              • Parse-and-expression
              • Parse-additive-expression
              • Parse-abstract-declarator
              • Parse-member-designor-rest
              • Parse-declarator
              • Parse-attribute
              • Parse-type-qualifier-or-attribute-specifier
              • Parse-enumerator
              • Parse-asm-output-operand
              • Parse-asm-input-operand
        • Atc
        • Transformation-tools
        • Language
        • Representation
        • Insertion-sort
        • Pack
      • Soft
      • Bv
      • Imp-language
      • Ethereum
      • Event-macros
      • Java
      • Riscv
      • Bitcoin
      • Zcash
      • Yul
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
      • File-io-light
      • Cryptography
      • Number-theory
      • Axe
      • Lists-light
      • Builtins
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Lexer

Lex-*-hexadecimal-digit

Lex zero or more hexadecimal digits, as many as available.

Signature

(lex-*-hexadecimal-digit pos-so-far parstate) 
  → 
(mv erp hexdigs last-pos next-pos new-parstate)

Arguments

pos-so-far — Guard (positionp pos-so-far).

parstate — Guard (parstatep parstate).

Returns

hexdigs — Type (hex-digit-char-listp hexdigs).

last-pos — Type (positionp last-pos).

next-pos — Type (positionp next-pos).

new-parstate — Type (parstatep new-parstate), given (parstatep parstate).

That is, we read *hexadecimal-digit, in ABNF notation, i.e. a repetition of zero of more instances of hexadecimal-digit.

The pos-so-far input is the position that has been read so far, just before attempting to read the digits. The last-pos output is the position of the last digit read, or pos-so-far if there are no digits. The next-pos output is the position just after the last digit read, or just after pos-so-far if there are no digits.

We read the next character. If it does not exist, we return. If it exists but is not a hexadecimal digit, we put the character back and return. Otherwise, we recursively read zero or more, and we put the one just read in front. We always return the position of the last hexadecimal character, or the input pos-so-far if there is no hexadecimal character: this input is the position read so far, just before the zero or more hexadecimal digits to be read.

Definitions and Theorems

Function: lex-*-hexadecimal-digit

(defun lex-*-hexadecimal-digit (pos-so-far parstate)
  (declare (xargs :stobjs (parstate)))
  (declare (xargs :guard (and (positionp pos-so-far)
                              (parstatep parstate))))
  (let ((__function__ 'lex-*-hexadecimal-digit))
    (declare (ignorable __function__))
    (b* (((reterr)
          nil (irr-position)
          (irr-position)
          parstate)
         ((erp char pos parstate)
          (read-char parstate))
         ((when (not char))
          (retok nil (position-fix pos-so-far)
                 pos parstate))
         ((unless (or (and (utf8-<= (char-code #\0) char)
                           (utf8-<= char (char-code #\9)))
                      (and (utf8-<= (char-code #\A) char)
                           (utf8-<= char (char-code #\F)))
                      (and (utf8-<= (char-code #\a) char)
                           (utf8-<= char (char-code #\f)))))
          (b* ((parstate (unread-char parstate)))
            (retok nil (position-fix pos-so-far)
                   pos parstate)))
         (hexdig (code-char char))
         ((erp hexdigs last-pos next-pos parstate)
          (lex-*-hexadecimal-digit pos parstate)))
      (retok (cons hexdig hexdigs)
             last-pos next-pos parstate))))

Theorem: hex-digit-char-listp-of-lex-*-hexadecimal-digit.hexdigs

(defthm hex-digit-char-listp-of-lex-*-hexadecimal-digit.hexdigs
  (b* (((mv acl2::?erp ?hexdigs
            ?last-pos ?next-pos ?new-parstate)
        (lex-*-hexadecimal-digit pos-so-far parstate)))
    (hex-digit-char-listp hexdigs))
  :rule-classes :rewrite)

Theorem: positionp-of-lex-*-hexadecimal-digit.last-pos

(defthm positionp-of-lex-*-hexadecimal-digit.last-pos
  (b* (((mv acl2::?erp ?hexdigs
            ?last-pos ?next-pos ?new-parstate)
        (lex-*-hexadecimal-digit pos-so-far parstate)))
    (positionp last-pos))
  :rule-classes :rewrite)

Theorem: positionp-of-lex-*-hexadecimal-digit.next-pos

(defthm positionp-of-lex-*-hexadecimal-digit.next-pos
  (b* (((mv acl2::?erp ?hexdigs
            ?last-pos ?next-pos ?new-parstate)
        (lex-*-hexadecimal-digit pos-so-far parstate)))
    (positionp next-pos))
  :rule-classes :rewrite)

Theorem: parstatep-of-lex-*-hexadecimal-digit.new-parstate

(defthm parstatep-of-lex-*-hexadecimal-digit.new-parstate
  (implies (parstatep parstate)
           (b* (((mv acl2::?erp ?hexdigs
                     ?last-pos ?next-pos ?new-parstate)
                 (lex-*-hexadecimal-digit pos-so-far parstate)))
             (parstatep new-parstate)))
  :rule-classes :rewrite)

Theorem: true-listp-of-lex-*-hexadecimal-digit.hexdigs

(defthm true-listp-of-lex-*-hexadecimal-digit.hexdigs
  (b* (((mv acl2::?erp ?hexdigs
            ?last-pos ?next-pos ?new-parstate)
        (lex-*-hexadecimal-digit pos-so-far parstate)))
    (true-listp hexdigs))
  :rule-classes :type-prescription)

Theorem: parsize-of-lex-*-hexadecimal-digit-uncond

(defthm parsize-of-lex-*-hexadecimal-digit-uncond
  (b* (((mv acl2::?erp ?hexdigs
            ?last-pos ?next-pos ?new-parstate)
        (lex-*-hexadecimal-digit pos-so-far parstate)))
    (<= (parsize new-parstate)
        (- (parsize parstate) (len hexdigs))))
  :rule-classes :linear)