• Top

Grammar

ABNF grammar of Aleo instructions.

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

Subtopics

Cst-safe-ascii-conc?

Cst-arithmetic-literal-conc?

Cst-arithmetic-type-conc?

Cst-not-lf-or-cr-conc?

Cst-literal-type-conc?

Cst-plain-ws-conc?

Cst-literal-conc?

Cst-string-element-conc?

Cst-command-conc?

Cst-list-list-conc-matchp$

Cst-plaintext-type-conc?

Cst-list-list-alt-matchp$

Cst-integer-literal-conc?

Cst-integer-type-conc?

Cst-list-rep-matchp$

Cst-list-elem-matchp$

Cst-letter-conc?

Cst-comment-conc?

Cst-character-conc?

Abnf-tree-wrap-fn

Abnf-tree-wrap

Wrap a CST into a nest of CSTs with the given rule names as roots (in the order given) and each with a single subtree, ending with the original tree.

Cst-matchp$

Cst-arithmetic-literal-conc4-rep-elem

Cst-arithmetic-literal-conc4-rep

Cst-arithmetic-literal-conc3-rep-elem

Cst-arithmetic-literal-conc3-rep

Cst-arithmetic-literal-conc2-rep-elem

Cst-arithmetic-literal-conc2-rep

Cst-arithmetic-literal-conc1-rep-elem

Cst-arithmetic-literal-conc1-rep

Cst-string-element-conc3-rep-elem

Cst-string-element-conc3-rep

Cst-string-element-conc2-rep-elem

Cst-string-element-conc2-rep

Cst-string-element-conc1-rep-elem

Cst-string-element-conc1-rep

Cst-safe-ascii-conc5-rep-elem

Cst-plaintext-type-conc2-rep-elem

Cst-plaintext-type-conc2-rep

Cst-plaintext-type-conc1-rep-elem

Cst-plaintext-type-conc1-rep

Cst-not-lf-or-cr-conc4-rep-elem

Cst-not-lf-or-cr-conc3-rep-elem

Cst-not-lf-or-cr-conc2-rep-elem

Cst-not-lf-or-cr-conc1-rep-elem

Cst-literal-type-conc4-rep-elem

Cst-literal-type-conc3-rep-elem

Cst-literal-type-conc2-rep-elem

Cst-literal-type-conc1-rep-elem

Cst-integer-type-conc2-rep-elem

Cst-integer-type-conc1-rep-elem

Cst-integer-literal-conc2-rep-elem

Cst-integer-literal-conc2-rep

Cst-integer-literal-conc1-rep-elem

Cst-integer-literal-conc1-rep

Cst-arithmetic-type-conc4-rep-elem

Cst-arithmetic-type-conc4-rep

Cst-arithmetic-type-conc3-rep-elem

Cst-arithmetic-type-conc3-rep

Cst-arithmetic-type-conc2-rep-elem

Cst-arithmetic-type-conc2-rep

Cst-arithmetic-type-conc1-rep-elem

Cst-arithmetic-type-conc1-rep

Cst-arithmetic-literal-conc4

Cst-arithmetic-literal-conc3

Cst-arithmetic-literal-conc2

Cst-arithmetic-literal-conc1

Cst-visible-ascii-conc-rep-elem

Cst-uppercase-letter-conc-rep-elem

Cst-uppercase-letter-conc-rep

Cst-unsigned-literal-conc

Cst-transition-output-conc

Cst-string-element-conc3

Cst-string-element-conc2

Cst-string-element-conc1

Cst-safe-ascii-conc5-rep

Cst-safe-ascii-conc4-rep-elem

Cst-safe-ascii-conc4-rep

Cst-safe-ascii-conc3-rep-elem

Cst-safe-ascii-conc3-rep

Cst-safe-ascii-conc2-rep-elem

Cst-safe-ascii-conc2-rep

Cst-safe-ascii-conc1-rep-elem

Cst-safe-ascii-conc1-rep

Cst-plaintext-type-conc2

Cst-plaintext-type-conc1

Cst-plain-ws-conc4-rep-elem

Cst-plain-ws-conc3-rep-elem

Cst-plain-ws-conc2-rep-elem

Cst-plain-ws-conc1-rep-elem

Cst-not-lf-or-cr-conc4-rep

Cst-not-lf-or-cr-conc4

Cst-not-lf-or-cr-conc3-rep

Cst-not-lf-or-cr-conc3

Cst-not-lf-or-cr-conc2-rep

Cst-not-lf-or-cr-conc2

Cst-not-lf-or-cr-conc1-rep

Cst-not-lf-or-cr-conc1

Cst-lowercase-letter-conc-rep-elem

Cst-lowercase-letter-conc-rep

Cst-literal-type-conc4-rep

Cst-literal-type-conc4

Cst-literal-type-conc3-rep

Cst-literal-type-conc3

Cst-literal-type-conc2-rep

Cst-literal-type-conc2

Cst-literal-type-conc1-rep

Cst-literal-type-conc1

Cst-literal-conc4-rep-elem

Cst-literal-conc3-rep-elem

Cst-literal-conc2-rep-elem

Cst-literal-conc1-rep-elem

Cst-letter-conc2-rep-elem

Cst-letter-conc1-rep-elem

Cst-integer-type-conc2-rep

Cst-integer-type-conc2

Cst-integer-type-conc1-rep

Cst-integer-type-conc1

Cst-integer-literal-conc2

Cst-integer-literal-conc1

Cst-finalize-command-conc

Cst-comment-conc2-rep-elem

Cst-comment-conc1-rep-elem

Cst-command-conc3-rep-elem

Cst-command-conc2-rep-elem

Cst-command-conc1-rep-elem

Cst-character-conc2-rep-elem

Cst-character-conc2-rep

Cst-character-conc1-rep-elem

Cst-character-conc1-rep

Cst-boolean-type-conc-rep-elem

Cst-arithmetic-type-conc4

Cst-arithmetic-type-conc3

Cst-arithmetic-type-conc2

Cst-arithmetic-type-conc1

Cst-address-type-conc-rep-elem

Cst-visible-ascii-conc-rep

Cst-visible-ascii-conc

Cst-uppercase-letter-conc

Cst-transition-input-conc

Cst-ternary-op-conc-rep-elem

Cst-string-type-conc-rep-elem

Cst-string-type-conc-rep

Cst-string-literal-conc

Cst-signed-literal-conc

Cst-scalar-type-conc-rep-elem

Cst-scalar-type-conc-rep

Cst-scalar-literal-conc

Cst-safe-ascii-conc5

Cst-safe-ascii-conc4

Cst-safe-ascii-conc3

Cst-safe-ascii-conc2

Cst-safe-ascii-conc1

Cst-register-access-conc

Cst-plain-ws-conc4-rep

Cst-plain-ws-conc4

Cst-plain-ws-conc3-rep

Cst-plain-ws-conc3

Cst-plain-ws-conc2-rep

Cst-plain-ws-conc2

Cst-plain-ws-conc1-rep

Cst-plain-ws-conc1

Cst-mapping-value-conc

Cst-lowercase-letter-conc

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-line-comment-conc

Cst-letter-conc2-rep

Cst-letter-conc1-rep

Cst-instruction-conc

Cst-group-type-conc-rep-elem

Cst-group-literal-conc

Cst-function-output-conc

Cst-function-input-conc

Cst-finalize-output-conc

Cst-finalize-input-conc

Cst-field-type-conc-rep-elem

Cst-field-literal-conc

Cst-escaped-char-conc

Cst-comment-conc2-rep

Cst-comment-conc2

Cst-comment-conc1-rep

Cst-comment-conc1

Cst-command-conc3-rep

Cst-command-conc3

Cst-command-conc2-rep

Cst-command-conc2

Cst-command-conc1-rep

Cst-command-conc1

Cst-character-conc2

Cst-character-conc1

Cst-boolean-type-conc-rep

Cst-block-comment-conc

Cst-address-type-conc-rep

Cst-address-literal-conc

Cst-transition-conc

Cst-ternary-op-conc-rep

Cst-ternary-op-conc

Cst-ternary-conc

Cst-struct-conc

Cst-string-type-conc

Cst-scalar-type-conc

Cst-register-conc

Cst-record-conc

Cst-program-id-conc

Cst-program-conc

Cst-mapping-key-conc

Cst-mapping-conc

Cst-locator-conc

Cst-letter-conc2

Cst-letter-conc1

Cst-increment-conc

Cst-identifier-conc

Cst-group-type-conc-rep

Cst-group-type-conc

Cst-function-conc

Cst-finalize-conc

Cst-field-type-conc-rep

Cst-field-type-conc

Cst-escaped-ws-conc

Cst-escaped-lf-conc

Cst-entry-type-conc

Cst-digit-conc-rep-elem

Cst-decrement-conc

Cst-boolean-type-conc

Cst-binary-conc

Cst-address-type-conc

*grammar*

The parsed ABNF grammar of Aleo instructions.

Cst-ws-conc

Cst-unary-conc

Cst-tuple-conc

Cst-sp-conc-rep-elem

Cst-sp-conc-rep

Cst-lf-conc-rep-elem

Cst-lf-conc-rep

Cst-is-conc

Cst-import-conc

Cst-ht-conc-rep-elem

Cst-ht-conc-rep

Cst-hash-conc

Cst-entry-conc

Cst-dq-conc-rep-elem

Cst-dq-conc-rep

Cst-digit-conc-rep

Cst-digit-conc

Cst-cws-conc

Cst-cr-conc-rep-elem

Cst-cr-conc-rep

Cst-commit-conc

Cst-cast-conc

Cst-call-conc

Cst-assert-conc

Cst-sp-conc

Cst-lf-conc

Cst-ht-conc

Cst-dq-conc

Cst-cr-conc

Cst-%xe000-10ffff-nat

Cst-%x206a-d7ff-nat

Cst-%x202f-2065-nat

Cst-%x80-2029-nat

Cst-%x61-7a-nat

Cst-%x5d-7e-nat

Cst-%x41-5a-nat

Cst-%x30-7e-nat

Cst-%x30-39-nat

Cst-%x2b-7e-nat

Cst-%x2b-2e-nat

Cst-%x23-5b-nat

Cst-%x21-7e-nat

Cst-%x20-29-nat

Cst-%x20-21-nat