• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
      • Crypto-hdwallet
      • Apt
      • Error-checking
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Set
      • C
        • Syntax-for-tools
          • Formalized-subset
          • Mapping-to-language-definition
          • Input-files
          • Compilation-database
          • Printer
          • Output-files
          • Abstract-syntax-operations
          • Implementation-environments
          • Abstract-syntax
          • Concrete-syntax
          • Disambiguation
            • Disambiguator
            • Unambiguity
              • Abstract-syntax-unambp
              • Abstract-syntax-unambp-additional-theorems
              • Type-spec-list-unambp-of-sublists
              • Expr-unambp-of-operation-on-expr-unambp
          • Validation
          • Gcc-builtins
          • Preprocessing
          • Parsing
        • Atc
        • Transformation-tools
        • Language
        • Representation
        • Insertion-sort
        • Pack
      • Soft
      • Bv
      • Imp-language
      • Ethereum
      • Event-macros
      • Java
      • Riscv
      • Bitcoin
      • Zcash
      • Yul
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
      • File-io-light
      • Cryptography
      • Number-theory
      • Axe
      • Lists-light
      • Builtins
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Unambiguity

Abstract-syntax-unambp-additional-theorems

Additional theorems about the unambiguity predicates.

These are in addition to the ones generated by fty::deffold-reduce. These additional ones seem necessary for actual proofs involving the unambiguity predicates, e.g. the proof that the disambiguator returns unambiguous ASTs. It may be possible to extend fty::deffold-reduce to generate at least some of these, by recognizing certain sufficiently general patterns. However, all in all these are not many compared to the number of theorems already generated by fty::deffold-reduce.

Definitions and Theorems

Theorem: expr-unambp-when-ident

(defthm expr-unambp-when-ident
  (implies (expr-case expr :ident)
           (expr-unambp expr)))

Theorem: expr-unambp-when-const

(defthm expr-unambp-when-const
  (implies (expr-case expr :const)
           (expr-unambp expr)))

Theorem: expr-unambp-when-string

(defthm expr-unambp-when-string
  (implies (expr-case expr :string)
           (expr-unambp expr)))

Theorem: expr-unambp-when-label-addr

(defthm expr-unambp-when-label-addr
  (implies (expr-case expr :label-addr)
           (expr-unambp expr)))

Theorem: member-designor-unambp-when-ident

(defthm member-designor-unambp-when-ident
  (implies (member-designor-case memdes :ident)
           (member-designor-unambp memdes)))

Theorem: type-spec-unambp-when-signed

(defthm type-spec-unambp-when-signed
  (implies (type-spec-case type-spec :signed)
           (type-spec-unambp type-spec)))

Theorem: type-spec-unambp-when-typedef

(defthm type-spec-unambp-when-typedef
  (implies (type-spec-case type-spec :typedef)
           (type-spec-unambp type-spec)))

Theorem: type-spec-unambp-when-int128

(defthm type-spec-unambp-when-int128
  (implies (type-spec-case type-spec :int128)
           (type-spec-unambp type-spec)))

Theorem: type-spec-unambp-when-struct-empty

(defthm type-spec-unambp-when-struct-empty
  (implies (type-spec-case type-spec :struct-empty)
           (type-spec-unambp type-spec)))

Theorem: spec/qual-unambp-when-typequal

(defthm spec/qual-unambp-when-typequal
  (implies (spec/qual-case spec/qual :typequal)
           (spec/qual-unambp spec/qual)))

Theorem: spec/qual-unambp-when-attrib

(defthm spec/qual-unambp-when-attrib
  (implies (spec/qual-case spec/qual :attrib)
           (spec/qual-unambp spec/qual)))

Theorem: designor-unambp-when-dot

(defthm designor-unambp-when-dot
  (implies (designor-case designor :dot)
           (designor-unambp designor)))

Theorem: dirdeclor-unambp-when-ident

(defthm dirdeclor-unambp-when-ident
  (implies (dirdeclor-case dirdeclor :ident)
           (dirdeclor-unambp dirdeclor)))

Theorem: label-unambp-when-name

(defthm label-unambp-when-name
  (implies (label-case label :name)
           (label-unambp label)))

Theorem: stmt-unambp-of-when-goto

(defthm stmt-unambp-of-when-goto
  (implies (stmt-case stmt :goto)
           (stmt-unambp stmt)))

Theorem: stmt-unambp-of-when-asm

(defthm stmt-unambp-of-when-asm
  (implies (stmt-case stmt :asm)
           (stmt-unambp stmt)))

Theorem: decl-spec-unambp-when-not-tyspec/align

(defthm decl-spec-unambp-when-not-tyspec/align
  (implies (and (not (decl-spec-case decl-spec :typespec))
                (not (decl-spec-case decl-spec :align)))
           (decl-spec-unambp decl-spec)))

Theorem: extdecl-unambp-when-not-fundef/decl

(defthm extdecl-unambp-when-not-fundef/decl
  (implies (and (not (extdecl-case extdecl :fundef))
                (not (extdecl-case extdecl :decl)))
           (extdecl-unambp extdecl)))

Theorem: expr-not-sizeof-when-unambp

(defthm expr-not-sizeof-when-unambp
  (implies (expr-unambp expr)
           (not (equal (expr-kind expr) :sizeof-ambig)))
  :rule-classes :forward-chaining)

Theorem: expr-not-alignof-when-unambp

(defthm expr-not-alignof-when-unambp
  (implies (expr-unambp expr)
           (not (equal (expr-kind expr)
                       :alignof-ambig)))
  :rule-classes :forward-chaining)

Theorem: expr-not-cast/call-ambig-when-unambp

(defthm expr-not-cast/call-ambig-when-unambp
  (implies (expr-unambp expr)
           (not (equal (expr-kind expr)
                       :cast/call-ambig)))
  :rule-classes :forward-chaining)

Theorem: expr-not-cast/mul-ambig-when-unambp

(defthm expr-not-cast/mul-ambig-when-unambp
  (implies (expr-unambp expr)
           (not (equal (expr-kind expr)
                       :cast/mul-ambig)))
  :rule-classes :forward-chaining)

Theorem: expr-not-cast/add-ambig-when-unambp

(defthm expr-not-cast/add-ambig-when-unambp
  (implies (expr-unambp expr)
           (not (equal (expr-kind expr)
                       :cast/add-ambig)))
  :rule-classes :forward-chaining)

Theorem: expr-not-cast/sub-ambig-when-unambp

(defthm expr-not-cast/sub-ambig-when-unambp
  (implies (expr-unambp expr)
           (not (equal (expr-kind expr)
                       :cast/sub-ambig)))
  :rule-classes :forward-chaining)

Theorem: expr-not-cast/and-ambig-when-unambp

(defthm expr-not-cast/and-ambig-when-unambp
  (implies (expr-unambp expr)
           (not (equal (expr-kind expr)
                       :cast/and-ambig)))
  :rule-classes :forward-chaining)

Theorem: expr-not-cast/logand-ambig-when-unambp

(defthm expr-not-cast/logand-ambig-when-unambp
  (implies (expr-unambp expr)
           (not (equal (expr-kind expr)
                       :cast/logand-ambig)))
  :rule-classes :forward-chaining)

Theorem: type-spec-not-typeof-ambig-when-unambp

(defthm type-spec-not-typeof-ambig-when-unambp
  (implies (type-spec-unambp tyspec)
           (not (equal (type-spec-kind tyspec)
                       :typeof-ambig)))
  :rule-classes :forward-chaining)

Theorem: align-spec-not-alignas-ambig-when-unambp

(defthm align-spec-not-alignas-ambig-when-unambp
  (implies (align-spec-unambp alignspec)
           (not (equal (align-spec-kind alignspec)
                       :alignas-ambig)))
  :rule-classes :forward-chaining)

Theorem: param-declor-not-ambig-when-unambp

(defthm param-declor-not-ambig-when-unambp
  (implies (param-declor-unambp param-declor)
           (not (equal (param-declor-kind param-declor)
                       :ambig)))
  :rule-classes :forward-chaining)

Theorem: dirabsdeclor-not-dummy-base-when-unambp

(defthm dirabsdeclor-not-dummy-base-when-unambp
  (implies (dirabsdeclor-unambp dirabsdeclor)
           (not (equal (dirabsdeclor-kind dirabsdeclor)
                       :dummy-base)))
  :rule-classes :forward-chaining)

Theorem: stmt-not-for-ambig-when-unambp

(defthm stmt-not-for-ambig-when-unambp
  (implies (stmt-unambp stmt)
           (not (equal (stmt-kind stmt) :for-ambig)))
  :rule-classes :forward-chaining)

Theorem: block-item-not-ambig-when-unambp

(defthm block-item-not-ambig-when-unambp
  (implies (block-item-unambp item)
           (not (equal (block-item-kind item) :ambig)))
  :rule-classes :forward-chaining)

Theorem: expr-unambp-of-type-spec-typeof-expr->expr

(defthm expr-unambp-of-type-spec-typeof-expr->expr
  (implies (and (type-spec-unambp tyspec)
                (equal (type-spec-kind tyspec)
                       :typeof-expr))
           (expr-unambp (type-spec-typeof-expr->expr tyspec)))
  :rule-classes :forward-chaining)

Theorem: tyname-unambp-of-type-spec-typeof-type->type

(defthm tyname-unambp-of-type-spec-typeof-type->type
  (implies (and (type-spec-unambp tyspec)
                (equal (type-spec-kind tyspec)
                       :typeof-type))
           (tyname-unambp (type-spec-typeof-type->type tyspec)))
  :rule-classes :forward-chaining)