• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
      • Crypto-hdwallet
      • Apt
      • Error-checking
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Soft
      • Bv
      • Imp-language
      • C
      • Event-macros
      • Java
      • Bitcoin
      • Ethereum
      • Yul
        • Transformations
        • Language
          • Abstract-syntax
          • Dynamic-semantics
          • Concrete-syntax
            • Lexer
            • Parser
            • Grammar-new
              • Cst-literal-conc?
              • Cst-token-conc?
              • Cst-expression-conc?
              • Cst-list-list-conc-matchp$
              • Cst-lexeme-conc?
              • Cst-list-list-alt-matchp$
              • Cst-identifier-rest-conc?
              • Cst-list-rep-matchp$
              • Cst-list-elem-matchp$
              • Cst-comment-conc?
              • Abnf-tree-wrap-fn
              • Abnf-tree-with-root-p
              • Cst-nonzero-decimal-digit-conc-rep-elem
              • Cst-matchp$
              • Abnf-tree-wrap
              • Cst-nonzero-decimal-digit-conc-rep
              • Cst-identifier-rest-conc2-rep-elem
              • Cst-identifier-rest-conc2-rep
              • Cst-identifier-rest-conc1-rep-elem
              • Cst-identifier-rest-conc1-rep
              • Cst-expression-conc3-rep-elem
              • Cst-expression-conc2-rep-elem
              • Cst-uppercase-letter-conc-rep-elem
              • Cst-uppercase-letter-conc-rep
              • Cst-switch-statement-conc
              • Cst-nonzero-decimal-digit-conc
              • Cst-lowercase-letter-conc-rep-elem
              • Cst-lowercase-letter-conc-rep
              • Cst-literal-conc5-rep-elem
              • Cst-literal-conc4-rep-elem
              • Cst-literal-conc3-rep-elem
              • Cst-literal-conc2-rep-elem
              • Cst-literal-conc1-rep-elem
              • Cst-lexeme-conc3-rep-elem
              • Cst-lexeme-conc2-rep-elem
              • Cst-lexeme-conc1-rep-elem
              • Cst-identifier-rest-conc2
              • Cst-identifier-rest-conc1
              • Cst-function-definition-conc
              • Cst-expression-conc3-rep
              • Cst-expression-conc2-rep
              • Cst-expression-conc1-rep-elem
              • Cst-expression-conc1-rep
              • Cst-end-of-line-comment-conc
              • Cst-decimal-digit-conc-rep-elem
              • Cst-comment-conc2-rep-elem
              • Cst-comment-conc1-rep-elem
              • Cst-uppercase-letter-conc
              • Cst-token-conc4-rep-elem
              • Cst-token-conc3-rep-elem
              • Cst-token-conc2-rep-elem
              • Cst-token-conc1-rep-elem
              • Cst-lowercase-letter-conc
              • Cst-literal-conc5-rep
              • Cst-literal-conc5
              • Cst-literal-conc4-rep
              • Cst-literal-conc4
              • Cst-literal-conc3-rep
              • Cst-literal-conc3
              • Cst-literal-conc2-rep
              • Cst-literal-conc2
              • Cst-literal-conc1-rep
              • Cst-literal-conc1
              • Cst-lexeme-conc3-rep
              • Cst-lexeme-conc2-rep
              • Cst-lexeme-conc1-rep
              • Cst-if-statement-conc
              • Cst-function-call-conc
              • Cst-for-statement-conc
              • Cst-expression-conc3
              • Cst-expression-conc2
              • Cst-expression-conc1
              • Cst-escape-sequence-conc
              • Cst-decimal-digit-conc-rep
              • Cst-decimal-digit-conc
              • Cst-comment-conc2-rep
              • Cst-comment-conc2
              • Cst-comment-conc1-rep
              • Cst-comment-conc1
              • Cst-block-comment-conc
              • Cst-whitespace-conc
              • Cst-token-conc4-rep
              • Cst-token-conc4
              • Cst-token-conc3-rep
              • Cst-token-conc3
              • Cst-token-conc2-rep
              • Cst-token-conc2
              • Cst-token-conc1-rep
              • Cst-token-conc1
              • Cst-squote-conc-rep-elem
              • Cst-squote-conc-rep
              • Cst-lexeme-conc3
              • Cst-lexeme-conc2
              • Cst-lexeme-conc1
              • Cst-identifier-conc
              • Cst-hex-string-conc
              • Cst-hex-number-conc
              • Cst-dquote-conc-rep-elem
              • Cst-dquote-conc-rep
              • *grammar-new*
              • Cst-squote-conc
              • Cst-path-conc
              • Cst-lf-conc-rep-elem
              • Cst-lf-conc-rep
              • Cst-dquote-conc
              • Cst-cr-conc-rep-elem
              • Cst-cr-conc-rep
              • Cst-block-conc
              • Abnf-tree-list-with-root-p
              • Cst-lf-conc
              • Cst-cr-conc
              • Cst-%xe-7f-nat
              • Cst-%xb-c-nat
              • Cst-%x61-7a-nat
              • Cst-%x5d-7e-nat
              • Cst-%x41-5a-nat
              • Cst-%x31-39-nat
              • Cst-%x30-7f-nat
              • Cst-%x30-39-nat
              • Cst-%x2b-7f-nat
              • Cst-%x2b-2e-nat
              • Cst-%x28-5b-nat
              • Cst-%x23-5b-nat
              • Cst-%x20-26-nat
              • Cst-%x20-21-nat
              • Cst-%x0-9-nat
              • Cst-%x0-29-nat
            • Tokenizer
            • Grammar-old
          • Static-soundness
          • Static-semantics
          • Errors
        • Yul-json
      • Zcash
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
      • File-io-light
      • Number-theory
      • Cryptography
      • Lists-light
      • Builtins
      • Axe
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Concrete-syntax

Grammar-new

New ABNF grammar of Yul.

We use our verified ABNF grammar parser to parse the new ABNF grammar of Yul into a representation in ACL2.

This is the new grammar of Yul; see concrete-syntax.

Subtopics

Cst-literal-conc?

Cst-token-conc?

Cst-expression-conc?

Cst-list-list-conc-matchp$

Cst-lexeme-conc?

Cst-list-list-alt-matchp$

Cst-identifier-rest-conc?

Cst-list-rep-matchp$

Cst-list-elem-matchp$

Cst-comment-conc?

Abnf-tree-wrap-fn

Abnf-tree-with-root-p

Recognize terminated ABNF trees rooted at rulename, for the ABNF grammar of Yul.

Cst-nonzero-decimal-digit-conc-rep-elem

Cst-matchp$

Abnf-tree-wrap

Wrap an ABNF tree into a nest of ABNF trees with the given rule names as roots.

Cst-nonzero-decimal-digit-conc-rep

Cst-identifier-rest-conc2-rep-elem

Cst-identifier-rest-conc2-rep

Cst-identifier-rest-conc1-rep-elem

Cst-identifier-rest-conc1-rep

Cst-expression-conc3-rep-elem

Cst-expression-conc2-rep-elem

Cst-uppercase-letter-conc-rep-elem

Cst-uppercase-letter-conc-rep

Cst-switch-statement-conc

Cst-nonzero-decimal-digit-conc

Cst-lowercase-letter-conc-rep-elem

Cst-lowercase-letter-conc-rep

Cst-literal-conc5-rep-elem

Cst-literal-conc4-rep-elem

Cst-literal-conc3-rep-elem

Cst-literal-conc2-rep-elem

Cst-literal-conc1-rep-elem

Cst-lexeme-conc3-rep-elem

Cst-lexeme-conc2-rep-elem

Cst-lexeme-conc1-rep-elem

Cst-identifier-rest-conc2

Cst-identifier-rest-conc1

Cst-function-definition-conc

Cst-expression-conc3-rep

Cst-expression-conc2-rep

Cst-expression-conc1-rep-elem

Cst-expression-conc1-rep

Cst-end-of-line-comment-conc

Cst-decimal-digit-conc-rep-elem

Cst-comment-conc2-rep-elem

Cst-comment-conc1-rep-elem

Cst-uppercase-letter-conc

Cst-token-conc4-rep-elem

Cst-token-conc3-rep-elem

Cst-token-conc2-rep-elem

Cst-token-conc1-rep-elem

Cst-lowercase-letter-conc

Cst-literal-conc5-rep

Cst-literal-conc5

Cst-literal-conc4-rep

Cst-literal-conc4

Cst-literal-conc3-rep

Cst-literal-conc3

Cst-literal-conc2-rep

Cst-literal-conc2

Cst-literal-conc1-rep

Cst-literal-conc1

Cst-lexeme-conc3-rep

Cst-lexeme-conc2-rep

Cst-lexeme-conc1-rep

Cst-if-statement-conc

Cst-function-call-conc

Cst-for-statement-conc

Cst-expression-conc3

Cst-expression-conc2

Cst-expression-conc1

Cst-escape-sequence-conc

Cst-decimal-digit-conc-rep

Cst-decimal-digit-conc

Cst-comment-conc2-rep

Cst-comment-conc2

Cst-comment-conc1-rep

Cst-comment-conc1

Cst-block-comment-conc

Cst-whitespace-conc

Cst-token-conc4-rep

Cst-token-conc4

Cst-token-conc3-rep

Cst-token-conc3

Cst-token-conc2-rep

Cst-token-conc2

Cst-token-conc1-rep

Cst-token-conc1

Cst-squote-conc-rep-elem

Cst-squote-conc-rep

Cst-lexeme-conc3

Cst-lexeme-conc2

Cst-lexeme-conc1

Cst-identifier-conc

Cst-hex-string-conc

Cst-hex-number-conc

Cst-dquote-conc-rep-elem

Cst-dquote-conc-rep

*grammar-new*

The parsed new ABNF grammar of Yul.

Cst-squote-conc

Cst-path-conc

Cst-lf-conc-rep-elem

Cst-lf-conc-rep

Cst-dquote-conc

Cst-cr-conc-rep-elem

Cst-cr-conc-rep

Cst-block-conc

Abnf-tree-list-with-root-p

Lift abnf-tree-with-root-p to lists

Cst-lf-conc

Cst-cr-conc

Cst-%xe-7f-nat

Cst-%xb-c-nat

Cst-%x61-7a-nat

Cst-%x5d-7e-nat

Cst-%x41-5a-nat

Cst-%x31-39-nat

Cst-%x30-7f-nat

Cst-%x30-39-nat

Cst-%x2b-7f-nat

Cst-%x2b-2e-nat

Cst-%x28-5b-nat

Cst-%x23-5b-nat

Cst-%x20-26-nat

Cst-%x20-21-nat

Cst-%x0-9-nat

Cst-%x0-29-nat