• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
    • Apt
    • Zfc
    • Acre
    • Milawa
    • Smtlink
    • Abnf
    • Vwsim
    • Isar
    • Wp-gen
    • Dimacs-reader
    • Pfcs
    • Legacy-defrstobj
    • Proof-checker-array
    • Soft
    • C
    • Farray
    • Rp-rewriter
    • Instant-runoff-voting
    • Imp-language
    • Sidekick
    • Leftist-trees
    • Java
    • Taspi
    • Bitcoin
    • Riscv
    • Des
    • Ethereum
    • X86isa
    • Sha-2
    • Yul
      • Transformations
      • Language
        • Abstract-syntax
        • Dynamic-semantics
        • Concrete-syntax
          • Lexer
          • Parser
          • Grammar-old
          • Grammar
            • 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*
            • 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
        • Static-soundness
        • Static-semantics
        • Errors
      • Yul-json
    • Zcash
    • Proof-checker-itp13
    • Regex
    • ACL2-programming-language
    • Json
    • Jfkr
    • Equational
    • Cryptography
    • Poseidon
    • Where-do-i-place-my-book
    • Axe
    • Bigmems
    • Builtins
    • Execloader
    • Aleo
    • Solidity
    • Paco
    • Concurrent-programs
    • Bls12-377-curves
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Concrete-syntax

Grammar

ABNF grammar of Yul.

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

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*

The parsed 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