• 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
            • Parser
            • Concrete-syntax
              • Grammar-parsep
              • Parsep
          • Concrete-syntax
      • Leo
    • Bigmems
    • Builtins
    • Execloader
    • Solidity
    • Paco
    • Concurrent-programs
    • Bls12-377-curves
  • Debugging
  • Std
  • Community
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Concrete-syntax

Grammar-parsep

Grammatical parsing.

Signature

(grammar-parsep ucodes tree) → yes/no

Arguments

ucodes — Guard (leo-early::unicode-listp ucodes).

tree — Guard (abnf::treep tree).

Returns

yes/no — Type (booleanp yes/no).

The ABNF grammar of Aleo instructions specifies how a sequence of Unicode characters can be organized into a program, more precisely a program CST. This is the case when the fringe of the CST is the Unicode character sequence.

Given a Unicode character sequence ucodes there may be zero or one or more CSTs that satisfy this predicate. If there is zero, ucodes is not syntactically valid Aleo instructions code. If there is one or more, ucodes may be syntactically valid Aleo instructions code, if additional requirements are satisfied.

Definitions and Theorems

Function: grammar-parsep

(defun grammar-parsep (ucodes tree)
  (declare (xargs :guard (and (leo-early::unicode-listp ucodes)
                              (abnf::treep tree))))
  (let ((__function__ 'grammar-parsep))
    (declare (ignorable __function__))
    (and (cst-matchp tree "program")
         (equal (leo-early::unicode-list->codepoint-list ucodes)
                (abnf::tree->string tree)))))

Theorem: booleanp-of-grammar-parsep

(defthm booleanp-of-grammar-parsep
  (b* ((yes/no (grammar-parsep ucodes tree)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: grammar-parsep-of-unicode-list-fix-ucodes

(defthm grammar-parsep-of-unicode-list-fix-ucodes
  (equal (grammar-parsep (leo-early::unicode-list-fix ucodes)
                         tree)
         (grammar-parsep ucodes tree)))

Theorem: grammar-parsep-unicode-list-equiv-congruence-on-ucodes

(defthm grammar-parsep-unicode-list-equiv-congruence-on-ucodes
  (implies (leo-early::unicode-list-equiv ucodes ucodes-equiv)
           (equal (grammar-parsep ucodes tree)
                  (grammar-parsep ucodes-equiv tree)))
  :rule-classes :congruence)

Theorem: grammar-parsep-of-tree-fix-tree

(defthm grammar-parsep-of-tree-fix-tree
  (equal (grammar-parsep ucodes (abnf::tree-fix tree))
         (grammar-parsep ucodes tree)))

Theorem: grammar-parsep-tree-equiv-congruence-on-tree

(defthm grammar-parsep-tree-equiv-congruence-on-tree
  (implies (abnf::tree-equiv tree tree-equiv)
           (equal (grammar-parsep ucodes tree)
                  (grammar-parsep ucodes tree-equiv)))
  :rule-classes :congruence)