• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
      • Zfc
      • Acre
      • Milawa
      • Smtlink
      • Abnf
      • Vwsim
      • Isar
      • Pfcs
      • Wp-gen
      • Dimacs-reader
      • Legacy-defrstobj
      • Proof-checker-array
      • Soft
      • C
      • Farray
      • Rp-rewriter
      • Instant-runoff-voting
      • Imp-language
      • Sidekick
      • Leftist-trees
      • Java
      • Taspi
      • Riscv
      • Bitcoin
      • Des
      • Ethereum
      • X86isa
      • Sha-2
      • Yul
      • Zcash
      • Proof-checker-itp13
      • Regex
      • ACL2-programming-language
      • Json
      • Jfkr
      • Equational
      • Cryptography
      • Poseidon
      • Where-do-i-place-my-book
      • Axe
      • Aleo
        • Aleobft
        • Aleovm
          • Circuits
          • Language
            • Grammar
            • Early-version
              • Abstract-syntax
                • Binary-op
                • Literal
                • Instruction
                • Hash-op
                • Literal-type
                • Operand
                • Unary-op
                • Identifier
                • Commit-op
                • Mapping
                • Function
                • Programdef
                • Finalize-type
                • Closure
                • Register-type
                • Finalizer
                • Value-type
                • Record-type
                • Command
                • Plaintext-type
                • Finalization-option
                • Visibility
                • Register
                • Reference
                • Programid
                • Locator
                • Finalization
                • Entry-type
                • Regaccess
                • Program
                • Interface-type
                • Ident+ptype
                • Ident+etype
                • Function-output
                • Finalize-output
                • Finalize-input
                • Closure-output
                • Closure-input
                • Assert-op
                • Function-input
                • Equal-op
                • Finalize-command
                • Ternary-op
                • Import
                • Ident+ptype-list
                • Operand-list
                • Ident+etype-list
                • Programdef-list
                • Instruction-list
                • Import-list
                • Identifier-list
                • Function-output-list
                • Function-input-list
                • Finalize-output-list
                • Finalize-input-list
                • Command-list
                • Closure-output-list
                • Closure-input-list
              • Parser
              • Concrete-syntax
            • Concrete-syntax
        • Leo
      • Bigmems
      • Builtins
      • Execloader
      • Solidity
      • Paco
      • Concurrent-programs
      • Bls12-377-curves
    • Debugging
    • Std
    • Community
    • Proof-automation
    • ACL2
    • Macro-libraries
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Early-version

Abstract-syntax

Abstract syntax.

We define an abstract syntax, based on the ABNF grammar.

Subtopics

Binary-op
Fixtype of binary operators.
Literal
Fixtype of literals.
Instruction
Fixtype of instructions.
Hash-op
Fixtype of hashing operators.
Literal-type
Fixtype of plaintext types.
Operand
Fixtype of operands.
Unary-op
Fixtype of unary operators.
Identifier
Fixtype of identifiers.
Commit-op
Fixtype of commitment operators.
Mapping
Fixtype of mappings.
Function
Fixtype of functions.
Programdef
Fixtype of program definitions.
Finalize-type
Fixtype of finalization types.
Closure
Fixtype of closures.
Register-type
Fixtype of register types.
Finalizer
Fixtype of finalizers.
Value-type
Fixtype of value types.
Record-type
Fixtype of record types.
Command
Fixtype of commands.
Plaintext-type
Fixtype of plaintext types.
Finalization-option
Fixtype of optional finalizations.
Visibility
Fixtype of visibilities.
Register
Fixtype of registers.
Reference
Fixtype of references.
Programid
Fixtype of program IDs.
Locator
Fixtype of locators.
Finalization
Fixtype of finalizations.
Entry-type
Fixtype of entry types.
Regaccess
Fixtype of register accesses.
Program
Fixtype of programs.
Interface-type
Fixtype of interface types.
Ident+ptype
Fixtype of pairs consisting of an identifier and a plaintext type.
Ident+etype
Fixtype of pairs consisting of an identifier and an entry type.
Function-output
Fixtype of function outputs.
Finalize-output
Fixtype of finalizer outputs.
Finalize-input
Fixtype of finalizer inputs.
Closure-output
Fixtype of closure outputs.
Closure-input
Fixtype of closure inputs.
Assert-op
Fixtype of assertion operators.
Function-input
Fixtype of function inputs.
Equal-op
Fixtype of equality operators.
Finalize-command
Fixtype of finalization commands.
Ternary-op
Fixtype of ternary operators.
Import
Fixtype of imports.
Ident+ptype-list
Fixtype of lists of pairs consisting of a identifier and a plaintext type.
Operand-list
Fixtype of lists of operands.
Ident+etype-list
Fixtype of lists of pairs consisting of a identifier and an entry type.
Programdef-list
Fixtype of lists of program definitions.
Instruction-list
Fixtype of lists of instructions.
Import-list
Fixtype of lists of imports.
Identifier-list
Fixtype of lists of identifiers.
Function-output-list
Fixtype of lists of function outputs.
Function-input-list
Fixtype of lists of function inputs.
Finalize-output-list
Fixtype of lists of finalizer outputs.
Finalize-input-list
Fixtype of lists of finalizer inputs.
Command-list
Fixtype of lists of commands.
Closure-output-list
Fixtype of lists of closure outputs.
Closure-input-list
Fixtype of lists of closure inputs.