• 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
          • Renaming-variables
          • Dead-code-eliminator
          • Renamings
          • Disambiguator
          • Unique-variables
          • Dead-code-eliminator-static-safety
          • No-function-definitions
          • Unique-functions
            • Statements/blocks/cases/fundefs-unique-funs
              • Statement-list-unique-funs
              • Swcase-unique-funs
              • Swcase-list-unique-funs
              • Statement-unique-funs
              • Fundef-unique-funs
              • Block-unique-funs
              • Block-option-unique-funs
          • Renaming-functions
          • Dead-code-eliminator-no-loop-initializers
          • Dead-code-eliminator-no-function-definitions
          • No-loop-initializers
          • For-loop-init-rewriter
        • Language
        • 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

• Unique-functions

Statements/blocks/cases/fundefs-unique-funs

Mutually recursive functions that check the uniqueness of function names in statements, blocks, cases, and function definitions.

Definitions and Theorems

Function: statement-unique-funs

(defun statement-unique-funs (stmt funs)
  (declare (xargs :guard (and (statementp stmt)
                              (identifier-setp funs))))
  (let ((__function__ 'statement-unique-funs))
    (declare (ignorable __function__))
    (statement-case
         stmt
         :block (block-unique-funs stmt.get funs)
         :variable-single
         (identifier-set-fix funs)
         :variable-multi
         (identifier-set-fix funs)
         :assign-single (identifier-set-fix funs)
         :assign-multi (identifier-set-fix funs)
         :funcall (identifier-set-fix funs)
         :if (block-unique-funs stmt.body funs)
         :for
         (b* (((okf funs)
               (block-unique-funs stmt.init funs))
              ((okf funs)
               (block-unique-funs stmt.update funs))
              ((okf funs)
               (block-unique-funs stmt.body funs)))
           funs)
         :switch
         (b* (((okf funs)
               (swcase-list-unique-funs stmt.cases funs))
              ((okf funs)
               (block-option-unique-funs stmt.default funs)))
           funs)
         :leave (identifier-set-fix funs)
         :break (identifier-set-fix funs)
         :continue (identifier-set-fix funs)
         :fundef (fundef-unique-funs stmt.get funs))))

Function: statement-list-unique-funs

(defun statement-list-unique-funs (stmts funs)
  (declare (xargs :guard (and (statement-listp stmts)
                              (identifier-setp funs))))
  (let ((__function__ 'statement-list-unique-funs))
    (declare (ignorable __function__))
    (b* (((when (endp stmts))
          (identifier-set-fix funs))
         ((okf funs)
          (statement-unique-funs (car stmts)
                                 funs))
         ((okf funs)
          (statement-list-unique-funs (cdr stmts)
                                      funs)))
      funs)))

Function: block-unique-funs

(defun block-unique-funs (block funs)
  (declare (xargs :guard (and (blockp block)
                              (identifier-setp funs))))
  (let ((__function__ 'block-unique-funs))
    (declare (ignorable __function__))
    (statement-list-unique-funs (block->statements block)
                                funs)))

Function: block-option-unique-funs

(defun block-option-unique-funs (block? funs)
  (declare (xargs :guard (and (block-optionp block?)
                              (identifier-setp funs))))
  (let ((__function__ 'block-option-unique-funs))
    (declare (ignorable __function__))
    (block-option-case
         block?
         :some (block-unique-funs (block-option-some->val block?)
                                  funs)
         :none (identifier-set-fix funs))))

Function: swcase-unique-funs

(defun swcase-unique-funs (case funs)
  (declare (xargs :guard (and (swcasep case)
                              (identifier-setp funs))))
  (let ((__function__ 'swcase-unique-funs))
    (declare (ignorable __function__))
    (block-unique-funs (swcase->body case)
                       funs)))

Function: swcase-list-unique-funs

(defun swcase-list-unique-funs (cases funs)
  (declare (xargs :guard (and (swcase-listp cases)
                              (identifier-setp funs))))
  (let ((__function__ 'swcase-list-unique-funs))
    (declare (ignorable __function__))
    (b* (((when (endp cases))
          (identifier-set-fix funs))
         ((okf funs)
          (swcase-unique-funs (car cases) funs))
         ((okf funs)
          (swcase-list-unique-funs (cdr cases)
                                   funs)))
      funs)))

Function: fundef-unique-funs

(defun fundef-unique-funs (fundef funs)
  (declare (xargs :guard (and (fundefp fundef)
                              (identifier-setp funs))))
  (let ((__function__ 'fundef-unique-funs))
    (declare (ignorable __function__))
    (b* ((name (fundef->name fundef))
         ((when (in name (identifier-set-fix funs)))
          (reserrf (list :duplicate-funs name)))
         (funs (insert name (identifier-set-fix funs))))
      (block-unique-funs (fundef->body fundef)
                         funs))))

Theorem: return-type-of-statement-unique-funs.new-funs

(defthm return-type-of-statement-unique-funs.new-funs
  (b* ((?new-funs (statement-unique-funs stmt funs)))
    (identifier-set-resultp new-funs))
  :rule-classes :rewrite)

Theorem: return-type-of-statement-list-unique-funs.new-funs

(defthm return-type-of-statement-list-unique-funs.new-funs
  (b* ((?new-funs (statement-list-unique-funs stmts funs)))
    (identifier-set-resultp new-funs))
  :rule-classes :rewrite)

Theorem: return-type-of-block-unique-funs.new-funs

(defthm return-type-of-block-unique-funs.new-funs
  (b* ((?new-funs (block-unique-funs block funs)))
    (identifier-set-resultp new-funs))
  :rule-classes :rewrite)

Theorem: return-type-of-block-option-unique-funs.new-funs

(defthm return-type-of-block-option-unique-funs.new-funs
  (b* ((?new-funs (block-option-unique-funs block? funs)))
    (identifier-set-resultp new-funs))
  :rule-classes :rewrite)

Theorem: return-type-of-swcase-unique-funs.new-funs

(defthm return-type-of-swcase-unique-funs.new-funs
  (b* ((?new-funs (swcase-unique-funs case funs)))
    (identifier-set-resultp new-funs))
  :rule-classes :rewrite)

Theorem: return-type-of-swcase-list-unique-funs.new-funs

(defthm return-type-of-swcase-list-unique-funs.new-funs
  (b* ((?new-funs (swcase-list-unique-funs cases funs)))
    (identifier-set-resultp new-funs))
  :rule-classes :rewrite)

Theorem: return-type-of-fundef-unique-funs.new-funs

(defthm return-type-of-fundef-unique-funs.new-funs
  (b* ((?new-funs (fundef-unique-funs fundef funs)))
    (identifier-set-resultp new-funs))
  :rule-classes :rewrite)

Theorem: statement-unique-funs-of-statement-fix-stmt

(defthm statement-unique-funs-of-statement-fix-stmt
  (equal (statement-unique-funs (statement-fix stmt)
                                funs)
         (statement-unique-funs stmt funs)))

Theorem: statement-unique-funs-of-identifier-set-fix-funs

(defthm statement-unique-funs-of-identifier-set-fix-funs
  (equal (statement-unique-funs stmt (identifier-set-fix funs))
         (statement-unique-funs stmt funs)))

Theorem: statement-list-unique-funs-of-statement-list-fix-stmts

(defthm statement-list-unique-funs-of-statement-list-fix-stmts
  (equal (statement-list-unique-funs (statement-list-fix stmts)
                                     funs)
         (statement-list-unique-funs stmts funs)))

Theorem: statement-list-unique-funs-of-identifier-set-fix-funs

(defthm statement-list-unique-funs-of-identifier-set-fix-funs
 (equal (statement-list-unique-funs stmts (identifier-set-fix funs))
        (statement-list-unique-funs stmts funs)))

Theorem: block-unique-funs-of-block-fix-block

(defthm block-unique-funs-of-block-fix-block
  (equal (block-unique-funs (block-fix block)
                            funs)
         (block-unique-funs block funs)))

Theorem: block-unique-funs-of-identifier-set-fix-funs

(defthm block-unique-funs-of-identifier-set-fix-funs
  (equal (block-unique-funs block (identifier-set-fix funs))
         (block-unique-funs block funs)))

Theorem: block-option-unique-funs-of-block-option-fix-block?

(defthm block-option-unique-funs-of-block-option-fix-block?
  (equal (block-option-unique-funs (block-option-fix block?)
                                   funs)
         (block-option-unique-funs block? funs)))

Theorem: block-option-unique-funs-of-identifier-set-fix-funs

(defthm block-option-unique-funs-of-identifier-set-fix-funs
  (equal (block-option-unique-funs block? (identifier-set-fix funs))
         (block-option-unique-funs block? funs)))

Theorem: swcase-unique-funs-of-swcase-fix-case

(defthm swcase-unique-funs-of-swcase-fix-case
  (equal (swcase-unique-funs (swcase-fix case)
                             funs)
         (swcase-unique-funs case funs)))

Theorem: swcase-unique-funs-of-identifier-set-fix-funs

(defthm swcase-unique-funs-of-identifier-set-fix-funs
  (equal (swcase-unique-funs case (identifier-set-fix funs))
         (swcase-unique-funs case funs)))

Theorem: swcase-list-unique-funs-of-swcase-list-fix-cases

(defthm swcase-list-unique-funs-of-swcase-list-fix-cases
  (equal (swcase-list-unique-funs (swcase-list-fix cases)
                                  funs)
         (swcase-list-unique-funs cases funs)))

Theorem: swcase-list-unique-funs-of-identifier-set-fix-funs

(defthm swcase-list-unique-funs-of-identifier-set-fix-funs
  (equal (swcase-list-unique-funs cases (identifier-set-fix funs))
         (swcase-list-unique-funs cases funs)))

Theorem: fundef-unique-funs-of-fundef-fix-fundef

(defthm fundef-unique-funs-of-fundef-fix-fundef
  (equal (fundef-unique-funs (fundef-fix fundef)
                             funs)
         (fundef-unique-funs fundef funs)))

Theorem: fundef-unique-funs-of-identifier-set-fix-funs

(defthm fundef-unique-funs-of-identifier-set-fix-funs
  (equal (fundef-unique-funs fundef (identifier-set-fix funs))
         (fundef-unique-funs fundef funs)))

Theorem: statement-unique-funs-statement-equiv-congruence-on-stmt

(defthm statement-unique-funs-statement-equiv-congruence-on-stmt
  (implies (statement-equiv stmt stmt-equiv)
           (equal (statement-unique-funs stmt funs)
                  (statement-unique-funs stmt-equiv funs)))
  :rule-classes :congruence)

Theorem: statement-unique-funs-identifier-set-equiv-congruence-on-funs

(defthm
      statement-unique-funs-identifier-set-equiv-congruence-on-funs
  (implies (identifier-set-equiv funs funs-equiv)
           (equal (statement-unique-funs stmt funs)
                  (statement-unique-funs stmt funs-equiv)))
  :rule-classes :congruence)

Theorem: statement-list-unique-funs-statement-list-equiv-congruence-on-stmts

(defthm
 statement-list-unique-funs-statement-list-equiv-congruence-on-stmts
 (implies (statement-list-equiv stmts stmts-equiv)
          (equal (statement-list-unique-funs stmts funs)
                 (statement-list-unique-funs stmts-equiv funs)))
 :rule-classes :congruence)

Theorem: statement-list-unique-funs-identifier-set-equiv-congruence-on-funs

(defthm
 statement-list-unique-funs-identifier-set-equiv-congruence-on-funs
 (implies (identifier-set-equiv funs funs-equiv)
          (equal (statement-list-unique-funs stmts funs)
                 (statement-list-unique-funs stmts funs-equiv)))
 :rule-classes :congruence)

Theorem: block-unique-funs-block-equiv-congruence-on-block

(defthm block-unique-funs-block-equiv-congruence-on-block
  (implies (block-equiv block block-equiv)
           (equal (block-unique-funs block funs)
                  (block-unique-funs block-equiv funs)))
  :rule-classes :congruence)

Theorem: block-unique-funs-identifier-set-equiv-congruence-on-funs

(defthm block-unique-funs-identifier-set-equiv-congruence-on-funs
  (implies (identifier-set-equiv funs funs-equiv)
           (equal (block-unique-funs block funs)
                  (block-unique-funs block funs-equiv)))
  :rule-classes :congruence)

Theorem: block-option-unique-funs-block-option-equiv-congruence-on-block?

(defthm
   block-option-unique-funs-block-option-equiv-congruence-on-block?
  (implies (block-option-equiv block? block?-equiv)
           (equal (block-option-unique-funs block? funs)
                  (block-option-unique-funs block?-equiv funs)))
  :rule-classes :congruence)

Theorem: block-option-unique-funs-identifier-set-equiv-congruence-on-funs

(defthm
   block-option-unique-funs-identifier-set-equiv-congruence-on-funs
  (implies (identifier-set-equiv funs funs-equiv)
           (equal (block-option-unique-funs block? funs)
                  (block-option-unique-funs block? funs-equiv)))
  :rule-classes :congruence)

Theorem: swcase-unique-funs-swcase-equiv-congruence-on-case

(defthm swcase-unique-funs-swcase-equiv-congruence-on-case
  (implies (swcase-equiv case case-equiv)
           (equal (swcase-unique-funs case funs)
                  (swcase-unique-funs case-equiv funs)))
  :rule-classes :congruence)

Theorem: swcase-unique-funs-identifier-set-equiv-congruence-on-funs

(defthm swcase-unique-funs-identifier-set-equiv-congruence-on-funs
  (implies (identifier-set-equiv funs funs-equiv)
           (equal (swcase-unique-funs case funs)
                  (swcase-unique-funs case funs-equiv)))
  :rule-classes :congruence)

Theorem: swcase-list-unique-funs-swcase-list-equiv-congruence-on-cases

(defthm
      swcase-list-unique-funs-swcase-list-equiv-congruence-on-cases
  (implies (swcase-list-equiv cases cases-equiv)
           (equal (swcase-list-unique-funs cases funs)
                  (swcase-list-unique-funs cases-equiv funs)))
  :rule-classes :congruence)

Theorem: swcase-list-unique-funs-identifier-set-equiv-congruence-on-funs

(defthm
    swcase-list-unique-funs-identifier-set-equiv-congruence-on-funs
  (implies (identifier-set-equiv funs funs-equiv)
           (equal (swcase-list-unique-funs cases funs)
                  (swcase-list-unique-funs cases funs-equiv)))
  :rule-classes :congruence)

Theorem: fundef-unique-funs-fundef-equiv-congruence-on-fundef

(defthm fundef-unique-funs-fundef-equiv-congruence-on-fundef
  (implies (fundef-equiv fundef fundef-equiv)
           (equal (fundef-unique-funs fundef funs)
                  (fundef-unique-funs fundef-equiv funs)))
  :rule-classes :congruence)

Theorem: fundef-unique-funs-identifier-set-equiv-congruence-on-funs

(defthm fundef-unique-funs-identifier-set-equiv-congruence-on-funs
  (implies (identifier-set-equiv funs funs-equiv)
           (equal (fundef-unique-funs fundef funs)
                  (fundef-unique-funs fundef funs-equiv)))
  :rule-classes :congruence)

Subtopics

Statement-list-unique-funs

Check that a list of statements has unique function names.

Swcase-unique-funs

Check that a switch case has unique function names.

Swcase-list-unique-funs

Check that a list of switch cases has unique function names.

Statement-unique-funs

Check that a statement has unique function names.

Fundef-unique-funs

Check that a function definition has unique function names.

Block-unique-funs

Check that a block has unique function names.

Block-option-unique-funs

Check that an optional block has unique function names.