• 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
      • Soft
      • Bv
      • Imp-language
      • Ethereum
      • Event-macros
      • Java
      • Riscv
      • Bitcoin
      • Zcash
      • Yul
        • Transformations
        • Language
          • Abstract-syntax
          • Dynamic-semantics
          • Concrete-syntax
          • Static-soundness
          • Static-semantics
            • Static-safety-checking
            • Static-shadowing-checking
            • Mode-set-result
            • Literal-evaluation
            • Static-identifier-checking
              • Check-identifiers-statements/blocks/cases/fundefs
                • Check-identifiers-swcase-list
                • Check-identifiers-statement-list
                • Check-identifiers-swcase
                • Check-identifiers-statement
                • Check-identifiers-fundef
                • Check-identifiers-block-option
                • Check-identifiers-block
              • Check-identifier
              • Check-identifier-list
            • Static-safety-checking-evm
            • Mode-set
            • Modes
          • Errors
        • Yul-json
      • 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

• Static-identifier-checking

Check-identifiers-statements/blocks/cases/fundefs

Check the well-formedness of identifiers declared in statements, blocks, cases, and function definitions.

Definitions and Theorems

Function: check-identifiers-statement

(defun check-identifiers-statement (stmt)
  (declare (xargs :guard (statementp stmt)))
  (let ((__function__ 'check-identifiers-statement))
    (declare (ignorable __function__))
    (statement-case
         stmt :block
         (check-identifiers-block stmt.get)
         :variable-single
         (check-identifier stmt.name)
         :variable-multi
         (check-identifier-list stmt.names)
         :assign-single
         nil :assign-multi nil :funcall nil
         :if (check-identifiers-block stmt.body)
         :for
         (b* (((okf &)
               (check-identifiers-block stmt.init))
              ((okf &)
               (check-identifiers-block stmt.update))
              ((okf &)
               (check-identifiers-block stmt.body)))
           nil)
         :switch
         (b* (((okf &)
               (check-identifiers-swcase-list stmt.cases))
              ((okf &)
               (check-identifiers-block-option stmt.default)))
           nil)
         :leave nil
         :break nil
         :continue nil
         :fundef (check-identifiers-fundef stmt.get))))

Function: check-identifiers-statement-list

(defun check-identifiers-statement-list (stmts)
  (declare (xargs :guard (statement-listp stmts)))
  (let ((__function__ 'check-identifiers-statement-list))
    (declare (ignorable __function__))
    (b* (((when (endp stmts)) nil)
         ((okf &)
          (check-identifiers-statement (car stmts)))
         ((okf &)
          (check-identifiers-statement-list (cdr stmts))))
      nil)))

Function: check-identifiers-block

(defun check-identifiers-block (block)
  (declare (xargs :guard (blockp block)))
  (let ((__function__ 'check-identifiers-block))
    (declare (ignorable __function__))
    (check-identifiers-statement-list (block->statements block))))

Function: check-identifiers-block-option

(defun check-identifiers-block-option (block?)
  (declare (xargs :guard (block-optionp block?)))
  (let ((__function__ 'check-identifiers-block-option))
    (declare (ignorable __function__))
    (block-option-case block?
                       :none nil
                       :some (check-identifiers-block block?.val))))

Function: check-identifiers-swcase

(defun check-identifiers-swcase (case)
  (declare (xargs :guard (swcasep case)))
  (let ((__function__ 'check-identifiers-swcase))
    (declare (ignorable __function__))
    (check-identifiers-block (swcase->body case))))

Function: check-identifiers-swcase-list

(defun check-identifiers-swcase-list (cases)
  (declare (xargs :guard (swcase-listp cases)))
  (let ((__function__ 'check-identifiers-swcase-list))
    (declare (ignorable __function__))
    (b* (((when (endp cases)) nil)
         ((okf &)
          (check-identifiers-swcase (car cases)))
         ((okf &)
          (check-identifiers-swcase-list (cdr cases))))
      nil)))

Function: check-identifiers-fundef

(defun check-identifiers-fundef (fundef)
  (declare (xargs :guard (fundefp fundef)))
  (let ((__function__ 'check-identifiers-fundef))
    (declare (ignorable __function__))
    (b* (((okf &)
          (check-identifier (fundef->name fundef)))
         ((okf &)
          (check-identifiers-block (fundef->body fundef))))
      nil)))

Theorem: return-type-of-check-identifiers-statement._

(defthm return-type-of-check-identifiers-statement._
  (b* ((?_ (check-identifiers-statement stmt)))
    (reserr-optionp _))
  :rule-classes :rewrite)

Theorem: return-type-of-check-identifiers-statement-list._

(defthm return-type-of-check-identifiers-statement-list._
  (b* ((?_ (check-identifiers-statement-list stmts)))
    (reserr-optionp _))
  :rule-classes :rewrite)

Theorem: return-type-of-check-identifiers-block._

(defthm return-type-of-check-identifiers-block._
  (b* ((?_ (check-identifiers-block block)))
    (reserr-optionp _))
  :rule-classes :rewrite)

Theorem: return-type-of-check-identifiers-block-option._

(defthm return-type-of-check-identifiers-block-option._
  (b* ((?_ (check-identifiers-block-option block?)))
    (reserr-optionp _))
  :rule-classes :rewrite)

Theorem: return-type-of-check-identifiers-swcase._

(defthm return-type-of-check-identifiers-swcase._
  (b* ((?_ (check-identifiers-swcase case)))
    (reserr-optionp _))
  :rule-classes :rewrite)

Theorem: return-type-of-check-identifiers-swcase-list._

(defthm return-type-of-check-identifiers-swcase-list._
  (b* ((?_ (check-identifiers-swcase-list cases)))
    (reserr-optionp _))
  :rule-classes :rewrite)

Theorem: return-type-of-check-identifiers-fundef._

(defthm return-type-of-check-identifiers-fundef._
  (b* ((?_ (check-identifiers-fundef fundef)))
    (reserr-optionp _))
  :rule-classes :rewrite)

Theorem: check-identifiers-statement-of-statement-fix-stmt

(defthm check-identifiers-statement-of-statement-fix-stmt
  (equal (check-identifiers-statement (statement-fix stmt))
         (check-identifiers-statement stmt)))

Theorem: check-identifiers-statement-list-of-statement-list-fix-stmts

(defthm check-identifiers-statement-list-of-statement-list-fix-stmts
  (equal
       (check-identifiers-statement-list (statement-list-fix stmts))
       (check-identifiers-statement-list stmts)))

Theorem: check-identifiers-block-of-block-fix-block

(defthm check-identifiers-block-of-block-fix-block
  (equal (check-identifiers-block (block-fix block))
         (check-identifiers-block block)))

Theorem: check-identifiers-block-option-of-block-option-fix-block?

(defthm check-identifiers-block-option-of-block-option-fix-block?
  (equal (check-identifiers-block-option (block-option-fix block?))
         (check-identifiers-block-option block?)))

Theorem: check-identifiers-swcase-of-swcase-fix-case

(defthm check-identifiers-swcase-of-swcase-fix-case
  (equal (check-identifiers-swcase (swcase-fix case))
         (check-identifiers-swcase case)))

Theorem: check-identifiers-swcase-list-of-swcase-list-fix-cases

(defthm check-identifiers-swcase-list-of-swcase-list-fix-cases
  (equal (check-identifiers-swcase-list (swcase-list-fix cases))
         (check-identifiers-swcase-list cases)))

Theorem: check-identifiers-fundef-of-fundef-fix-fundef

(defthm check-identifiers-fundef-of-fundef-fix-fundef
  (equal (check-identifiers-fundef (fundef-fix fundef))
         (check-identifiers-fundef fundef)))

Theorem: check-identifiers-statement-statement-equiv-congruence-on-stmt

(defthm
     check-identifiers-statement-statement-equiv-congruence-on-stmt
  (implies (statement-equiv stmt stmt-equiv)
           (equal (check-identifiers-statement stmt)
                  (check-identifiers-statement stmt-equiv)))
  :rule-classes :congruence)

Theorem: check-identifiers-statement-list-statement-list-equiv-congruence-on-stmts

(defthm
 check-identifiers-statement-list-statement-list-equiv-congruence-on-stmts
 (implies (statement-list-equiv stmts stmts-equiv)
          (equal (check-identifiers-statement-list stmts)
                 (check-identifiers-statement-list stmts-equiv)))
 :rule-classes :congruence)

Theorem: check-identifiers-block-block-equiv-congruence-on-block

(defthm check-identifiers-block-block-equiv-congruence-on-block
  (implies (block-equiv block block-equiv)
           (equal (check-identifiers-block block)
                  (check-identifiers-block block-equiv)))
  :rule-classes :congruence)

Theorem: check-identifiers-block-option-block-option-equiv-congruence-on-block?

(defthm
 check-identifiers-block-option-block-option-equiv-congruence-on-block?
 (implies (block-option-equiv block? block?-equiv)
          (equal (check-identifiers-block-option block?)
                 (check-identifiers-block-option block?-equiv)))
 :rule-classes :congruence)

Theorem: check-identifiers-swcase-swcase-equiv-congruence-on-case

(defthm check-identifiers-swcase-swcase-equiv-congruence-on-case
  (implies (swcase-equiv case case-equiv)
           (equal (check-identifiers-swcase case)
                  (check-identifiers-swcase case-equiv)))
  :rule-classes :congruence)

Theorem: check-identifiers-swcase-list-swcase-list-equiv-congruence-on-cases

(defthm
 check-identifiers-swcase-list-swcase-list-equiv-congruence-on-cases
 (implies (swcase-list-equiv cases cases-equiv)
          (equal (check-identifiers-swcase-list cases)
                 (check-identifiers-swcase-list cases-equiv)))
 :rule-classes :congruence)

Theorem: check-identifiers-fundef-fundef-equiv-congruence-on-fundef

(defthm check-identifiers-fundef-fundef-equiv-congruence-on-fundef
  (implies (fundef-equiv fundef fundef-equiv)
           (equal (check-identifiers-fundef fundef)
                  (check-identifiers-fundef fundef-equiv)))
  :rule-classes :congruence)

Subtopics

Check-identifiers-swcase-list

Check the well-formedness of identifiers declared in lists of cases of switch statements.

Check-identifiers-statement-list

Check the well-formedness of identifiers declared in a list of statements.

Check-identifiers-swcase

Check the well-formedness of identifiers declared in cases of switch statements.

Check-identifiers-statement

Check the well-formedness of identifiers declared in statements.

Check-identifiers-fundef

Check the well-formedness of identifiers declared in function definitions.

Check-identifiers-block-option

Check the well-formedness of identifiers declared in an optional block.

Check-identifiers-block

Check the well-formedness of identifiers declared in a block.