• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
    • Apt
    • Zfc
    • Acre
    • Milawa
    • Smtlink
    • Abnf
    • Vwsim
    • Isar
    • Wp-gen
    • Dimacs-reader
    • Pfcs
    • Legacy-defrstobj
    • C
    • Proof-checker-array
    • Soft
    • Farray
    • Rp-rewriter
    • Instant-runoff-voting
    • Imp-language
    • Sidekick
    • Ethereum
    • Leftist-trees
    • Java
    • Riscv
    • Taspi
    • Bitcoin
    • Zcash
    • Des
    • X86isa
    • Sha-2
    • Yul
    • Proof-checker-itp13
    • Regex
    • ACL2-programming-language
    • Json
    • Jfkr
    • Equational
    • Cryptography
    • Axe
    • Poseidon
    • Where-do-i-place-my-book
    • Aleo
      • Aleobft
      • Aleovm
        • Circuits
        • Language
          • Grammar
          • Early-version
            • Abstract-syntax
            • Parser
              • Lex-record
              • Lex-group-escaped-char-body
              • Lex-group-instruction-body
              • Lex-increment
              • Lex-decrement
              • Lex-value-type
              • Lex-unary-op
              • Lex-rest-of-block-comment-fns
              • Lex-not-dq-or-backslash
              • Lex-not-star-or-slash
              • *defparse-aleo-group-table*
              • Lex-hex-digit
              • Lex-transition-output
              • Lex-transition-input
              • Lex-binary-op
              • Lex-transition
              • Lex-mapping-value
              • Lex-group-program-declaration
              • Lex-function-output
              • Lex-function-input
              • Lex-finalize-output
              • Lex-finalize-input
              • Lex-program
              • Lex-not-star
              • Lex-mapping-key
              • Lex-hash-op
              • *defparse-aleo-repetition-table*
              • Lex-cast
              • Lex-call
              • Lex-unsigned-type
              • Lex-signed-type
              • Lex-function
              • Lex-finalize-type
              • Lex-finalize
              • Lex-commit
              • Lex-is
              • Lex-register-type
              • Lex-mapping
              • Lex-group-entry-type-visibility
              • Lex-group-bhp-sizes
              • Lex-arithmetic-literal
              • Lex-tuple
              • Lex-safe-nonascii
              • Lex-literal-type
              • Lex-instruction
              • Lex-entry
              • Lex-arithmetic-type
              • Lex-struct
              • Lex-not-lf-or-cr
              • Lex-commit-op
              • Lex-ternary
              • Lex-plain-ws
              • Lex-operand
              • Lex-literal
              • Lex-hash
              • Lex-group-letter/digit/_
              • Lex-finalize-command
              • Lex-escaped-char
              • Lex-binary
              • Lex-unary
              • Lex-string-element
              • Lex-import
              • Lex-group-psd-sizes
              • Lex-group-escaped-lf/not-lf-or-cr
              • Lex-group-address-public/private
              • Lex-group-1*-plain-ws/escaped-lf
              • Lex-unsigned-literal
              • Lex-repetition-1*6-hex-digit
              • Lex-group-u64-public/private
              • Lex-group-locator/identifier
              • Lex-signed-literal
              • Lex-scalar-literal
              • Lex-group-literal
              • Lex-group-address-char-*-underbar
              • Lex-field-literal
              • Lex-command
              • Lex-assert
              • Lex-string-literal
              • Lex-register-access
              • Lex-program-id
              • Lex-plaintext-type
              • Lex-optional-transition-finalize
              • Lex-integer-literal
              • Lex-group-ped-sizes
              • Lex-group-dot-identifier
              • Lex-group-digit-*-underbar
              • Lex-group-1-ws-register
              • Lex-boolean-literal
              • Lex-locator
              • Lex-line-comment
              • Lex-integer-type
              • Lex-identifier
              • Lex-group-1-ws-operand
              • Lex-group-1-operand
              • Lex-entry-type
              • Lex-address-literal
              • Lex-letter
              • Lex-comment
              • Lex-block-comment
              • Lex-assert-op
              • Lex-uppercase-letter
              • Lex-repetition-1*-program-declaration
              • Lex-repetition-1*-address-char-*-underbar
              • Lex-register
              • Lex-lowercase-letter
              • Lex-is-op
              • Lex-escaped-ws
              • Lex-escaped-lf
              • Lex-visible-ascii
              • Lex-string-type
              • Lex-scalar-type
              • Lex-boolean-type
              • Lex-address-type
              • Lex-ternary-op
              • Lex-repetition-*-program-declaration
              • Lex-repetition-*-plain-ws-or-escaped-lf
              • Lex-repetition-*-escaped-lf/not-lf-or-cr
              • Lex-repetition-*-address-char-*-underbar
              • Lex-repetition-1*-digit-*-underbar
              • Lex-group-type
              • Lex-field-type
              • Lex-repetition-3-operands
              • Lex-repetition-1*-ws-register
              • Lex-repetition-1*-ws-operand
              • Lex-repetition-1*-instruction
              • Lex-optional-hyphen
              • Lex-digit
              • Lex-sp
              • Lex-repetition-*-transition-output
              • Lex-repetition-*-transition-input
              • Lex-repetition-*-string-element
              • Lex-repetition-*-letter/digit/_
              • Lex-repetition-*-function-output
              • Lex-repetition-*-function-input
              • Lex-repetition-*-finalize-output
              • Lex-repetition-*-finalize-input
              • Lex-repetition-*-dot-identifier
              • Lex-repetition-*-digit-*-underbar
              • Lex-repetition-1*-command
              • Lex-lf
              • Lex-ht
              • Lex-dq
              • Lex-cr
              • Lex-ws
              • Lex-repetition-*-ws-register
              • Lex-repetition-*-ws-operand
              • Lex-repetition-*-instruction
              • Lex-repetition-2-operands
              • Lex-repetition-*-plain-ws
              • Lex-repetition-*-import
              • Lex-repetition-*-hex-digit
              • Lex-repetition-*-comment/ws
              • Lex-repetition-*-command
              • Lex-repetition-1*-plain-ws
              • Lex-group-comment/ws
              • Lex-repetition-*-underbar
              • Lex-repetition-*-tuple
              • Lex-repetition-*-entry
              • Lex-repetition-*-digit
              • Lex-repetition-1*-tuple
              • Lex-repetition-1*-digit
              • Lex-address-char
              • Lex-group-address-char
              • Lex-cws
              • Address-char-nat-p
              • *defparse-aleo-option-table*
            • Concrete-syntax
          • Concrete-syntax
      • Leo
    • Bigmems
    • Builtins
    • Execloader
    • Solidity
    • Paco
    • Concurrent-programs
    • Bls12-377-curves
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Parser

Lex-record

Parse a record.

Signature

(lex-record abnf::input) → (mv abnf::tree abnf::rest-input)

Arguments

abnf::input — Guard (nat-listp abnf::input).

Returns

abnf::tree — Type (abnf::tree-resultp abnf::tree).

abnf::rest-input — Type (nat-listp abnf::rest-input).

Definitions and Theorems

Function: lex-record

(defun lex-record (abnf::input)
 (declare (xargs :guard (nat-listp abnf::input)))
 (let ((__function__ 'lex-record))
  (declare (ignorable __function__))
  (b*
   (((mv abnf::treess abnf::input)
     (b* (((mv abnf::treess1 abnf::input1)
           (b* (((mv abnf::tree abnf::input)
                 (lex-cws abnf::input))
                ((when (reserrp abnf::tree))
                 (mv (reserrf-push abnf::tree)
                     abnf::input))
                (abnf::trees1 (list abnf::tree))
                ((mv abnf::tree abnf::input)
                 (abnf::parse-schars "record" abnf::input))
                ((when (reserrp abnf::tree))
                 (mv (reserrf-push abnf::tree)
                     abnf::input))
                (abnf::trees2 (list abnf::tree))
                ((mv abnf::tree abnf::input)
                 (lex-ws abnf::input))
                ((when (reserrp abnf::tree))
                 (mv (reserrf-push abnf::tree)
                     abnf::input))
                (abnf::trees3 (list abnf::tree))
                ((mv abnf::tree abnf::input)
                 (lex-identifier abnf::input))
                ((when (reserrp abnf::tree))
                 (mv (reserrf-push abnf::tree)
                     abnf::input))
                (abnf::trees4 (list abnf::tree))
                ((mv abnf::tree abnf::input)
                 (lex-ws abnf::input))
                ((when (reserrp abnf::tree))
                 (mv (reserrf-push abnf::tree)
                     abnf::input))
                (abnf::trees5 (list abnf::tree))
                ((mv abnf::tree abnf::input)
                 (abnf::parse-ichars ":" abnf::input))
                ((when (reserrp abnf::tree))
                 (mv (reserrf-push abnf::tree)
                     abnf::input))
                (abnf::trees6 (list abnf::tree))
                ((mv abnf::tree abnf::input)
                 (lex-cws abnf::input))
                ((when (reserrp abnf::tree))
                 (mv (reserrf-push abnf::tree)
                     abnf::input))
                (abnf::trees7 (list abnf::tree))
                ((mv abnf::tree abnf::input)
                 (abnf::parse-schars "owner" abnf::input))
                ((when (reserrp abnf::tree))
                 (mv (reserrf-push abnf::tree)
                     abnf::input))
                (abnf::trees8 (list abnf::tree))
                ((mv abnf::tree abnf::input)
                 (lex-ws abnf::input))
                ((when (reserrp abnf::tree))
                 (mv (reserrf-push abnf::tree)
                     abnf::input))
                (abnf::trees9 (list abnf::tree))
                ((mv abnf::tree abnf::input)
                 (abnf::parse-schars "as" abnf::input))
                ((when (reserrp abnf::tree))
                 (mv (reserrf-push abnf::tree)
                     abnf::input))
                (abnf::trees10 (list abnf::tree))
                ((mv abnf::tree abnf::input)
                 (lex-ws abnf::input))
                ((when (reserrp abnf::tree))
                 (mv (reserrf-push abnf::tree)
                     abnf::input))
                (abnf::trees11 (list abnf::tree))
                ((mv abnf::tree abnf::input)
                 (lex-cws abnf::input))
                ((when (reserrp abnf::tree))
                 (mv (reserrf-push abnf::tree)
                     abnf::input))
                (abnf::trees12 (list abnf::tree))
                ((mv abnf::tree abnf::input)
                 (lex-group-address-public/private abnf::input))
                ((when (reserrp abnf::tree))
                 (mv (reserrf-push abnf::tree)
                     abnf::input))
                (abnf::trees13 (list abnf::tree))
                ((mv abnf::tree abnf::input)
                 (lex-ws abnf::input))
                ((when (reserrp abnf::tree))
                 (mv (reserrf-push abnf::tree)
                     abnf::input))
                (abnf::trees14 (list abnf::tree))
                ((mv abnf::tree abnf::input)
                 (abnf::parse-ichars ";" abnf::input))
                ((when (reserrp abnf::tree))
                 (mv (reserrf-push abnf::tree)
                     abnf::input))
                (abnf::trees15 (list abnf::tree))
                ((mv abnf::tree abnf::input)
                 (lex-cws abnf::input))
                ((when (reserrp abnf::tree))
                 (mv (reserrf-push abnf::tree)
                     abnf::input))
                (abnf::trees16 (list abnf::tree))
                ((mv abnf::tree abnf::input)
                 (abnf::parse-schars "gates" abnf::input))
                ((when (reserrp abnf::tree))
                 (mv (reserrf-push abnf::tree)
                     abnf::input))
                (abnf::trees17 (list abnf::tree))
                ((mv abnf::tree abnf::input)
                 (lex-ws abnf::input))
                ((when (reserrp abnf::tree))
                 (mv (reserrf-push abnf::tree)
                     abnf::input))
                (abnf::trees18 (list abnf::tree))
                ((mv abnf::tree abnf::input)
                 (abnf::parse-schars "as" abnf::input))
                ((when (reserrp abnf::tree))
                 (mv (reserrf-push abnf::tree)
                     abnf::input))
                (abnf::trees19 (list abnf::tree))
                ((mv abnf::tree abnf::input)
                 (lex-ws abnf::input))
                ((when (reserrp abnf::tree))
                 (mv (reserrf-push abnf::tree)
                     abnf::input))
                (abnf::trees20 (list abnf::tree))
                ((mv abnf::tree abnf::input)
                 (lex-cws abnf::input))
                ((when (reserrp abnf::tree))
                 (mv (reserrf-push abnf::tree)
                     abnf::input))
                (abnf::trees21 (list abnf::tree))
                ((mv abnf::tree abnf::input)
                 (lex-group-u64-public/private abnf::input))
                ((when (reserrp abnf::tree))
                 (mv (reserrf-push abnf::tree)
                     abnf::input))
                (abnf::trees22 (list abnf::tree))
                ((mv abnf::tree abnf::input)
                 (lex-ws abnf::input))
                ((when (reserrp abnf::tree))
                 (mv (reserrf-push abnf::tree)
                     abnf::input))
                (abnf::trees23 (list abnf::tree))
                ((mv abnf::tree abnf::input)
                 (abnf::parse-ichars ";" abnf::input))
                ((when (reserrp abnf::tree))
                 (mv (reserrf-push abnf::tree)
                     abnf::input))
                (abnf::trees24 (list abnf::tree))
                ((mv abnf::trees25 abnf::input)
                 (lex-repetition-*-entry abnf::input))
                ((when (reserrp abnf::trees25))
                 (mv (reserrf-push abnf::trees25)
                     abnf::input))
                (abnf::treess
                     (list abnf::trees1 abnf::trees2
                           abnf::trees3 abnf::trees4 abnf::trees5
                           abnf::trees6 abnf::trees7 abnf::trees8
                           abnf::trees9 abnf::trees10 abnf::trees11
                           abnf::trees12 abnf::trees13
                           abnf::trees14 abnf::trees15
                           abnf::trees16 abnf::trees17
                           abnf::trees18 abnf::trees19
                           abnf::trees20 abnf::trees21
                           abnf::trees22 abnf::trees23
                           abnf::trees24 abnf::trees25)))
             (mv abnf::treess abnf::input)))
          ((when (not (reserrp abnf::treess1)))
           (mv abnf::treess1 abnf::input1)))
      (mv
       (reserrf
        (list
         :found (list abnf::treess1)
         :required
         '(((:repetition (:repeat 1 (:finite 1))
                         (:rulename (:rulename "cws")))
            (:repetition (:repeat 1 (:finite 1))
                         (:char-val (:sensitive "record")))
            (:repetition (:repeat 1 (:finite 1))
                         (:rulename (:rulename "ws")))
            (:repetition (:repeat 1 (:finite 1))
                         (:rulename (:rulename "identifier")))
            (:repetition (:repeat 1 (:finite 1))
                         (:rulename (:rulename "ws")))
            (:repetition (:repeat 1 (:finite 1))
                         (:char-val (:insensitive nil ":")))
            (:repetition (:repeat 1 (:finite 1))
                         (:rulename (:rulename "cws")))
            (:repetition (:repeat 1 (:finite 1))
                         (:char-val (:sensitive "owner")))
            (:repetition (:repeat 1 (:finite 1))
                         (:rulename (:rulename "ws")))
            (:repetition (:repeat 1 (:finite 1))
                         (:char-val (:sensitive "as")))
            (:repetition (:repeat 1 (:finite 1))
                         (:rulename (:rulename "ws")))
            (:repetition (:repeat 1 (:finite 1))
                         (:rulename (:rulename "cws")))
            (:repetition
             (:repeat 1 (:finite 1))
             (:group
              (((:repetition
                     (:repeat 1 (:finite 1))
                     (:char-val (:sensitive "address.public"))))
               ((:repetition
                     (:repeat 1 (:finite 1))
                     (:char-val (:sensitive "address.private")))))))
            (:repetition (:repeat 1 (:finite 1))
                         (:rulename (:rulename "ws")))
            (:repetition (:repeat 1 (:finite 1))
                         (:char-val (:insensitive nil ";")))
            (:repetition (:repeat 1 (:finite 1))
                         (:rulename (:rulename "cws")))
            (:repetition (:repeat 1 (:finite 1))
                         (:char-val (:sensitive "gates")))
            (:repetition (:repeat 1 (:finite 1))
                         (:rulename (:rulename "ws")))
            (:repetition (:repeat 1 (:finite 1))
                         (:char-val (:sensitive "as")))
            (:repetition (:repeat 1 (:finite 1))
                         (:rulename (:rulename "ws")))
            (:repetition (:repeat 1 (:finite 1))
                         (:rulename (:rulename "cws")))
            (:repetition
             (:repeat 1 (:finite 1))
             (:group
              (((:repetition (:repeat 1 (:finite 1))
                             (:char-val (:sensitive "u64.public"))))
               ((:repetition
                     (:repeat 1 (:finite 1))
                     (:char-val (:sensitive "u64.private")))))))
            (:repetition (:repeat 1 (:finite 1))
                         (:rulename (:rulename "ws")))
            (:repetition (:repeat 1 (:finite 1))
                         (:char-val (:insensitive nil ";")))
            (:repetition (:repeat 0 (:infinity))
                         (:rulename (:rulename "entry")))))))
       abnf::input)))
    ((when (reserrp abnf::treess))
     (mv (reserrf-push abnf::treess)
         (nat-list-fix abnf::input))))
   (mv (abnf::make-tree-nonleaf :rulename? (abnf::rulename "record")
                                :branches abnf::treess)
       abnf::input))))

Theorem: tree-resultp-of-lex-record.tree

(defthm tree-resultp-of-lex-record.tree
  (b* (((mv abnf::?tree abnf::?rest-input)
        (lex-record abnf::input)))
    (abnf::tree-resultp abnf::tree))
  :rule-classes :rewrite)

Theorem: nat-listp-of-lex-record.rest-input

(defthm nat-listp-of-lex-record.rest-input
  (b* (((mv abnf::?tree abnf::?rest-input)
        (lex-record abnf::input)))
    (nat-listp abnf::rest-input))
  :rule-classes :rewrite)

Theorem: len-of-lex-record-<=

(defthm len-of-lex-record-<=
  (b* (((mv abnf::?tree abnf::?rest-input)
        (lex-record abnf::input)))
    (<= (len abnf::rest-input)
        (len abnf::input)))
  :rule-classes :linear)

Theorem: len-of-lex-record-<

(defthm len-of-lex-record-<
  (b* (((mv abnf::?tree abnf::?rest-input)
        (lex-record abnf::input)))
    (implies (not (reserrp abnf::tree))
             (< (len abnf::rest-input)
                (len abnf::input))))
  :rule-classes :linear)

Theorem: lex-record-of-nat-list-fix-input

(defthm lex-record-of-nat-list-fix-input
  (equal (lex-record (nat-list-fix abnf::input))
         (lex-record abnf::input)))

Theorem: lex-record-nat-list-equiv-congruence-on-input

(defthm lex-record-nat-list-equiv-congruence-on-input
  (implies (acl2::nat-list-equiv abnf::input input-equiv)
           (equal (lex-record abnf::input)
                  (lex-record input-equiv)))
  :rule-classes :congruence)