• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
      • Crypto-hdwallet
      • Apt
      • Error-checking
      • Abnf
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Soft
      • Bv
      • Imp-language
      • Event-macros
      • C
      • Java
      • Bitcoin
      • Ethereum
      • Yul
        • Transformations
          • Renaming-variables
          • Dead-code-eliminator
          • Renamings
          • Disambiguator
          • Unique-variables
            • Statements/blocks/cases/fundefs-unique-vars
              • Swcase-list-unique-vars
              • Statement-list-unique-vars
              • Fundef-unique-vars
              • Block-option-unique-vars
              • Swcase-unique-vars
              • Statement-unique-vars
              • Block-unique-vars
            • Var-unique-vars
            • Var-list-unique-vars
            • Statements/blocks/cases/fundefs-unique-vars-extend
          • Dead-code-eliminator-static-safety
          • No-function-definitions
          • Unique-functions
          • Renaming-functions
          • Dead-code-eliminator-no-loop-initializers
          • Dead-code-eliminator-no-function-definitions
          • No-loop-initializers
          • For-loop-init-rewriter
        • Language
        • Yul-json
      • Zcash
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
      • File-io-light
      • Number-theory
      • Cryptography
      • Lists-light
      • Builtins
      • Axe
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Unique-variables

Statements/blocks/cases/fundefs-unique-vars

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

Definitions and Theorems

Function: statement-unique-vars

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

Function: statement-list-unique-vars

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

Function: block-unique-vars

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

Function: block-option-unique-vars

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

Function: swcase-unique-vars

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

Function: swcase-list-unique-vars

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

Function: fundef-unique-vars

(defun fundef-unique-vars (fundef allvars)
 (declare (xargs :guard (and (fundefp fundef)
                             (identifier-setp allvars))))
 (let ((__function__ 'fundef-unique-vars))
   (declare (ignorable __function__))
   (b* (((fundef fundef) fundef)
        ((okf allvars)
         (var-list-unique-vars (append fundef.inputs fundef.outputs)
                               allvars)))
     (block-unique-vars fundef.body allvars))))

Theorem: return-type-of-statement-unique-vars.new-allvars

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

Theorem: return-type-of-statement-list-unique-vars.new-allvars

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

Theorem: return-type-of-block-unique-vars.new-allvars

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

Theorem: return-type-of-block-option-unique-vars.new-allvars

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

Theorem: return-type-of-swcase-unique-vars.new-allvars

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

Theorem: return-type-of-swcase-list-unique-vars.new-allvars

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

Theorem: return-type-of-fundef-unique-vars.new-allvars

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

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

(defthm statement-unique-vars-of-statement-fix-stmt
  (equal (statement-unique-vars (statement-fix stmt)
                                allvars)
         (statement-unique-vars stmt allvars)))

Theorem: statement-unique-vars-of-identifier-set-fix-allvars

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

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

(defthm statement-list-unique-vars-of-statement-list-fix-stmts
  (equal (statement-list-unique-vars (statement-list-fix stmts)
                                     allvars)
         (statement-list-unique-vars stmts allvars)))

Theorem: statement-list-unique-vars-of-identifier-set-fix-allvars

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

Theorem: block-unique-vars-of-block-fix-block

(defthm block-unique-vars-of-block-fix-block
  (equal (block-unique-vars (block-fix block)
                            allvars)
         (block-unique-vars block allvars)))

Theorem: block-unique-vars-of-identifier-set-fix-allvars

(defthm block-unique-vars-of-identifier-set-fix-allvars
  (equal (block-unique-vars block (identifier-set-fix allvars))
         (block-unique-vars block allvars)))

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

(defthm block-option-unique-vars-of-block-option-fix-block?
  (equal (block-option-unique-vars (block-option-fix block?)
                                   allvars)
         (block-option-unique-vars block? allvars)))

Theorem: block-option-unique-vars-of-identifier-set-fix-allvars

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

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

(defthm swcase-unique-vars-of-swcase-fix-case
  (equal (swcase-unique-vars (swcase-fix case)
                             allvars)
         (swcase-unique-vars case allvars)))

Theorem: swcase-unique-vars-of-identifier-set-fix-allvars

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

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

(defthm swcase-list-unique-vars-of-swcase-list-fix-cases
  (equal (swcase-list-unique-vars (swcase-list-fix cases)
                                  allvars)
         (swcase-list-unique-vars cases allvars)))

Theorem: swcase-list-unique-vars-of-identifier-set-fix-allvars

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

Theorem: fundef-unique-vars-of-fundef-fix-fundef

(defthm fundef-unique-vars-of-fundef-fix-fundef
  (equal (fundef-unique-vars (fundef-fix fundef)
                             allvars)
         (fundef-unique-vars fundef allvars)))

Theorem: fundef-unique-vars-of-identifier-set-fix-allvars

(defthm fundef-unique-vars-of-identifier-set-fix-allvars
  (equal (fundef-unique-vars fundef (identifier-set-fix allvars))
         (fundef-unique-vars fundef allvars)))

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

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

Theorem: statement-unique-vars-identifier-set-equiv-congruence-on-allvars

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

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

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

Theorem: statement-list-unique-vars-identifier-set-equiv-congruence-on-allvars

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

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

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

Theorem: block-unique-vars-identifier-set-equiv-congruence-on-allvars

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

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

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

Theorem: block-option-unique-vars-identifier-set-equiv-congruence-on-allvars

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

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

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

Theorem: swcase-unique-vars-identifier-set-equiv-congruence-on-allvars

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

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

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

Theorem: swcase-list-unique-vars-identifier-set-equiv-congruence-on-allvars

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

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

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

Theorem: fundef-unique-vars-identifier-set-equiv-congruence-on-allvars

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

Subtopics

Swcase-list-unique-vars

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

Statement-list-unique-vars

Check that a list of statements has unique variable names.

Fundef-unique-vars

Check that a function definition has unique variable names.

Block-option-unique-vars

Check that an optional block has unique variable names.

Swcase-unique-vars

Check that a switch case has unique variable names.

Statement-unique-vars

Check that a statement has unique variable names.

Block-unique-vars

Check that a block has unique variable names.