• 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
          • Renaming-functions
            • Statements/blocks/cases/fundefs-renamefun
              • Statement-renamefun
              • Fundef-renamefun
              • Swcase-renamefun
              • Swcase-list-renamefun
              • Statement-list-renamefun
              • Block-renamefun
              • Block-option-renamefun
            • Expressions-renamefun
            • Fundef-list-renamefun
            • Expression-option-renamefun
            • Funcall-option-renamefun
            • Add-funs-to-fun-renaming
            • Add-fun-to-fun-renaming
            • Fun-renamefun
          • 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

• Renaming-functions

Statements/blocks/cases/fundefs-renamefun

Mutually recursive ACL2 functions to check if statements, blocks, cases, and function definitions are related by function renaming.

Definitions and Theorems

Function: statement-renamefun

(defun statement-renamefun (old new ren)
 (declare (xargs :guard (and (statementp old)
                             (statementp new)
                             (renamingp ren))))
 (let ((__function__ 'statement-renamefun))
  (declare (ignorable __function__))
  (statement-case
   old :block
   (b* (((unless (statement-case new :block))
         (reserrf (list :mismatch (statement-fix old)
                        (statement-fix new))))
        ((statement-block new) new)
        ((okf &)
         (block-renamefun old.get new.get ren)))
     nil)
   :variable-single
   (b* (((unless (statement-case new :variable-single))
         (reserrf (list :mismatch (statement-fix old)
                        (statement-fix new))))
        ((statement-variable-single new) new)
        ((unless (equal old.name new.name))
         (reserrf (list :mismatch (statement-fix old)
                        (statement-fix new))))
        ((okf &)
         (expression-option-renamefun old.init new.init ren)))
     nil)
   :variable-multi
   (b* (((unless (statement-case new :variable-multi))
         (reserrf (list :mismatch (statement-fix old)
                        (statement-fix new))))
        ((statement-variable-multi new) new)
        ((unless (equal old.names new.names))
         (reserrf (list :mismatch (statement-fix old)
                        (statement-fix new))))
        ((okf &)
         (funcall-option-renamefun old.init new.init ren)))
     nil)
   :assign-single
   (b* (((unless (statement-case new :assign-single))
         (reserrf (list :mismatch (statement-fix old)
                        (statement-fix new))))
        ((statement-assign-single new) new)
        ((unless (equal old.target new.target))
         (reserrf (list :mismatch (statement-fix old)
                        (statement-fix new))))
        ((okf &)
         (expression-renamefun old.value new.value ren)))
     nil)
   :assign-multi
   (b* (((unless (statement-case new :assign-multi))
         (reserrf (list :mismatch (statement-fix old)
                        (statement-fix new))))
        ((statement-assign-multi new) new)
        ((unless (equal old.targets new.targets))
         (reserrf (list :mismatch (statement-fix old)
                        (statement-fix new))))
        ((okf &)
         (funcall-renamefun old.value new.value ren)))
     nil)
   :funcall
   (b* (((unless (statement-case new :funcall))
         (reserrf (list :mismatch (statement-fix old)
                        (statement-fix new))))
        ((statement-funcall new) new)
        ((okf &)
         (funcall-renamefun old.get new.get ren)))
     nil)
   :if
   (b* (((unless (statement-case new :if))
         (reserrf (list :mismatch (statement-fix old)
                        (statement-fix new))))
        ((statement-if new) new)
        ((okf &)
         (expression-renamefun old.test new.test ren))
        ((okf &)
         (block-renamefun old.body new.body ren)))
     nil)
   :for
   (b*
    (((unless (statement-case new :for))
      (reserrf (list :mismatch (statement-fix old)
                     (statement-fix new))))
     ((statement-for new) new)
     (old-stmts (block->statements old.init))
     (new-stmts (block->statements new.init))
     (old-funs
         (fundef-list->name-list (statements-to-fundefs old-stmts)))
     (new-funs
         (fundef-list->name-list (statements-to-fundefs new-stmts)))
     ((okf ren)
      (add-funs-to-fun-renaming old-funs new-funs ren))
     ((okf &)
      (statement-list-renamefun old-stmts new-stmts ren))
     ((okf &)
      (expression-renamefun old.test new.test ren))
     ((okf &)
      (block-renamefun old.update new.update ren))
     ((okf &)
      (block-renamefun old.body new.body ren)))
    nil)
   :switch
   (b* (((unless (statement-case new :switch))
         (reserrf (list :mismatch (statement-fix old)
                        (statement-fix new))))
        ((statement-switch new) new)
        ((okf &)
         (expression-renamefun old.target new.target ren))
        ((okf &)
         (swcase-list-renamefun old.cases new.cases ren))
        ((okf &)
         (block-option-renamefun old.default new.default ren)))
     nil)
   :leave
   (b* (((unless (statement-case new :leave))
         (reserrf (list :mismatch (statement-fix old)
                        (statement-fix new)))))
     nil)
   :break
   (b* (((unless (statement-case new :break))
         (reserrf (list :mismatch (statement-fix old)
                        (statement-fix new)))))
     nil)
   :continue
   (b* (((unless (statement-case new :continue))
         (reserrf (list :mismatch (statement-fix old)
                        (statement-fix new)))))
     nil)
   :fundef
   (b* (((unless (statement-case new :fundef))
         (reserrf (list :mismatch (statement-fix old)
                        (statement-fix new))))
        ((statement-fundef new) new)
        ((okf &)
         (fundef-renamefun old.get new.get ren)))
     nil))))

Function: statement-list-renamefun

(defun statement-list-renamefun (old new ren)
 (declare (xargs :guard (and (statement-listp old)
                             (statement-listp new)
                             (renamingp ren))))
 (let ((__function__ 'statement-list-renamefun))
   (declare (ignorable __function__))
   (b*
    (((when (endp old))
      (if (endp new)
          nil
        (reserrf
             (list :mismatch-extra-new (statement-list-fix new)))))
     ((when (endp new))
      (reserrf (list :mismatch-extra-old (statement-list-fix old))))
     ((okf &)
      (statement-renamefun (car old)
                           (car new)
                           ren)))
    (statement-list-renamefun (cdr old)
                              (cdr new)
                              ren))))

Function: block-renamefun

(defun block-renamefun (old new ren)
 (declare (xargs :guard (and (blockp old)
                             (blockp new)
                             (renamingp ren))))
 (let ((__function__ 'block-renamefun))
  (declare (ignorable __function__))
  (b*
   ((old-stmts (block->statements old))
    (new-stmts (block->statements new))
    (old-fns
         (fundef-list->name-list (statements-to-fundefs old-stmts)))
    (new-fns
         (fundef-list->name-list (statements-to-fundefs new-stmts)))
    ((okf ren)
     (add-funs-to-fun-renaming old-fns new-fns ren))
    ((okf &)
     (statement-list-renamefun old-stmts new-stmts ren)))
   nil)))

Function: block-option-renamefun

(defun block-option-renamefun (old new ren)
 (declare (xargs :guard (and (block-optionp old)
                             (block-optionp new)
                             (renamingp ren))))
 (let ((__function__ 'block-option-renamefun))
  (declare (ignorable __function__))
  (block-option-case
    old :none
    (if (block-option-case new :none)
        nil
      (reserrf (list :mismatch (block-option-fix old)
                     (block-option-fix new))))
    :some (block-option-case
               new
               :none (reserrf (list :mismatch (block-option-fix old)
                                    (block-option-fix new)))
               :some (block-renamefun (block-option-some->val old)
                                      (block-option-some->val new)
                                      ren)))))

Function: swcase-renamefun

(defun swcase-renamefun (old new ren)
  (declare (xargs :guard (and (swcasep old)
                              (swcasep new)
                              (renamingp ren))))
  (let ((__function__ 'swcase-renamefun))
    (declare (ignorable __function__))
    (b* (((unless (equal (swcase->value old)
                         (swcase->value new)))
          (reserrf (list :mismatch-case-value (swcase->value old)
                         (swcase->value new)))))
      (block-renamefun (swcase->body old)
                       (swcase->body new)
                       ren))))

Function: swcase-list-renamefun

(defun swcase-list-renamefun (old new ren)
 (declare (xargs :guard (and (swcase-listp old)
                             (swcase-listp new)
                             (renamingp ren))))
 (let ((__function__ 'swcase-list-renamefun))
   (declare (ignorable __function__))
   (b*
    (((when (endp old))
      (if (endp new)
          nil
        (reserrf (list :mismatch-extra-new (swcase-list-fix new)))))
     ((when (endp new))
      (reserrf (list :mismatch-extra-old (swcase-list-fix old))))
     ((okf &)
      (swcase-renamefun (car old)
                        (car new)
                        ren)))
    (swcase-list-renamefun (cdr old)
                           (cdr new)
                           ren))))

Function: fundef-renamefun

(defun fundef-renamefun (old new ren)
  (declare (xargs :guard (and (fundefp old)
                              (fundefp new)
                              (renamingp ren))))
  (let ((__function__ 'fundef-renamefun))
    (declare (ignorable __function__))
    (b* (((okf &)
          (fun-renamefun (fundef->name old)
                         (fundef->name new)
                         ren))
         ((unless (equal (fundef->inputs old)
                         (fundef->inputs new)))
          (reserrf (list :mismatch (fundef-fix old)
                         (fundef-fix new))))
         ((unless (equal (fundef->outputs old)
                         (fundef->outputs new)))
          (reserrf (list :mismatch (fundef-fix old)
                         (fundef-fix new)))))
      (block-renamefun (fundef->body old)
                       (fundef->body new)
                       ren))))

Theorem: return-type-of-statement-renamefun._

(defthm return-type-of-statement-renamefun._
  (b* ((?_ (statement-renamefun old new ren)))
    (reserr-optionp _))
  :rule-classes :rewrite)

Theorem: return-type-of-statement-list-renamefun._

(defthm return-type-of-statement-list-renamefun._
  (b* ((?_ (statement-list-renamefun old new ren)))
    (reserr-optionp _))
  :rule-classes :rewrite)

Theorem: return-type-of-block-renamefun._

(defthm return-type-of-block-renamefun._
  (b* ((?_ (block-renamefun old new ren)))
    (reserr-optionp _))
  :rule-classes :rewrite)

Theorem: return-type-of-block-option-renamefun._

(defthm return-type-of-block-option-renamefun._
  (b* ((?_ (block-option-renamefun old new ren)))
    (reserr-optionp _))
  :rule-classes :rewrite)

Theorem: return-type-of-swcase-renamefun._

(defthm return-type-of-swcase-renamefun._
  (b* ((?_ (swcase-renamefun old new ren)))
    (reserr-optionp _))
  :rule-classes :rewrite)

Theorem: return-type-of-swcase-list-renamefun._

(defthm return-type-of-swcase-list-renamefun._
  (b* ((?_ (swcase-list-renamefun old new ren)))
    (reserr-optionp _))
  :rule-classes :rewrite)

Theorem: return-type-of-fundef-renamefun._

(defthm return-type-of-fundef-renamefun._
  (b* ((?_ (fundef-renamefun old new ren)))
    (reserr-optionp _))
  :rule-classes :rewrite)

Theorem: statement-renamefun-of-statement-fix-old

(defthm statement-renamefun-of-statement-fix-old
  (equal (statement-renamefun (statement-fix old)
                              new ren)
         (statement-renamefun old new ren)))

Theorem: statement-renamefun-of-statement-fix-new

(defthm statement-renamefun-of-statement-fix-new
  (equal (statement-renamefun old (statement-fix new)
                              ren)
         (statement-renamefun old new ren)))

Theorem: statement-renamefun-of-renaming-fix-ren

(defthm statement-renamefun-of-renaming-fix-ren
  (equal (statement-renamefun old new (renaming-fix ren))
         (statement-renamefun old new ren)))

Theorem: statement-list-renamefun-of-statement-list-fix-old

(defthm statement-list-renamefun-of-statement-list-fix-old
  (equal (statement-list-renamefun (statement-list-fix old)
                                   new ren)
         (statement-list-renamefun old new ren)))

Theorem: statement-list-renamefun-of-statement-list-fix-new

(defthm statement-list-renamefun-of-statement-list-fix-new
  (equal (statement-list-renamefun old (statement-list-fix new)
                                   ren)
         (statement-list-renamefun old new ren)))

Theorem: statement-list-renamefun-of-renaming-fix-ren

(defthm statement-list-renamefun-of-renaming-fix-ren
  (equal (statement-list-renamefun old new (renaming-fix ren))
         (statement-list-renamefun old new ren)))

Theorem: block-renamefun-of-block-fix-old

(defthm block-renamefun-of-block-fix-old
  (equal (block-renamefun (block-fix old)
                          new ren)
         (block-renamefun old new ren)))

Theorem: block-renamefun-of-block-fix-new

(defthm block-renamefun-of-block-fix-new
  (equal (block-renamefun old (block-fix new)
                          ren)
         (block-renamefun old new ren)))

Theorem: block-renamefun-of-renaming-fix-ren

(defthm block-renamefun-of-renaming-fix-ren
  (equal (block-renamefun old new (renaming-fix ren))
         (block-renamefun old new ren)))

Theorem: block-option-renamefun-of-block-option-fix-old

(defthm block-option-renamefun-of-block-option-fix-old
  (equal (block-option-renamefun (block-option-fix old)
                                 new ren)
         (block-option-renamefun old new ren)))

Theorem: block-option-renamefun-of-block-option-fix-new

(defthm block-option-renamefun-of-block-option-fix-new
  (equal (block-option-renamefun old (block-option-fix new)
                                 ren)
         (block-option-renamefun old new ren)))

Theorem: block-option-renamefun-of-renaming-fix-ren

(defthm block-option-renamefun-of-renaming-fix-ren
  (equal (block-option-renamefun old new (renaming-fix ren))
         (block-option-renamefun old new ren)))

Theorem: swcase-renamefun-of-swcase-fix-old

(defthm swcase-renamefun-of-swcase-fix-old
  (equal (swcase-renamefun (swcase-fix old)
                           new ren)
         (swcase-renamefun old new ren)))

Theorem: swcase-renamefun-of-swcase-fix-new

(defthm swcase-renamefun-of-swcase-fix-new
  (equal (swcase-renamefun old (swcase-fix new)
                           ren)
         (swcase-renamefun old new ren)))

Theorem: swcase-renamefun-of-renaming-fix-ren

(defthm swcase-renamefun-of-renaming-fix-ren
  (equal (swcase-renamefun old new (renaming-fix ren))
         (swcase-renamefun old new ren)))

Theorem: swcase-list-renamefun-of-swcase-list-fix-old

(defthm swcase-list-renamefun-of-swcase-list-fix-old
  (equal (swcase-list-renamefun (swcase-list-fix old)
                                new ren)
         (swcase-list-renamefun old new ren)))

Theorem: swcase-list-renamefun-of-swcase-list-fix-new

(defthm swcase-list-renamefun-of-swcase-list-fix-new
  (equal (swcase-list-renamefun old (swcase-list-fix new)
                                ren)
         (swcase-list-renamefun old new ren)))

Theorem: swcase-list-renamefun-of-renaming-fix-ren

(defthm swcase-list-renamefun-of-renaming-fix-ren
  (equal (swcase-list-renamefun old new (renaming-fix ren))
         (swcase-list-renamefun old new ren)))

Theorem: fundef-renamefun-of-fundef-fix-old

(defthm fundef-renamefun-of-fundef-fix-old
  (equal (fundef-renamefun (fundef-fix old)
                           new ren)
         (fundef-renamefun old new ren)))

Theorem: fundef-renamefun-of-fundef-fix-new

(defthm fundef-renamefun-of-fundef-fix-new
  (equal (fundef-renamefun old (fundef-fix new)
                           ren)
         (fundef-renamefun old new ren)))

Theorem: fundef-renamefun-of-renaming-fix-ren

(defthm fundef-renamefun-of-renaming-fix-ren
  (equal (fundef-renamefun old new (renaming-fix ren))
         (fundef-renamefun old new ren)))

Theorem: statement-renamefun-statement-equiv-congruence-on-old

(defthm statement-renamefun-statement-equiv-congruence-on-old
  (implies (statement-equiv old old-equiv)
           (equal (statement-renamefun old new ren)
                  (statement-renamefun old-equiv new ren)))
  :rule-classes :congruence)

Theorem: statement-renamefun-statement-equiv-congruence-on-new

(defthm statement-renamefun-statement-equiv-congruence-on-new
  (implies (statement-equiv new new-equiv)
           (equal (statement-renamefun old new ren)
                  (statement-renamefun old new-equiv ren)))
  :rule-classes :congruence)

Theorem: statement-renamefun-renaming-equiv-congruence-on-ren

(defthm statement-renamefun-renaming-equiv-congruence-on-ren
  (implies (renaming-equiv ren ren-equiv)
           (equal (statement-renamefun old new ren)
                  (statement-renamefun old new ren-equiv)))
  :rule-classes :congruence)

Theorem: statement-list-renamefun-statement-list-equiv-congruence-on-old

(defthm
    statement-list-renamefun-statement-list-equiv-congruence-on-old
  (implies (statement-list-equiv old old-equiv)
           (equal (statement-list-renamefun old new ren)
                  (statement-list-renamefun old-equiv new ren)))
  :rule-classes :congruence)

Theorem: statement-list-renamefun-statement-list-equiv-congruence-on-new

(defthm
    statement-list-renamefun-statement-list-equiv-congruence-on-new
  (implies (statement-list-equiv new new-equiv)
           (equal (statement-list-renamefun old new ren)
                  (statement-list-renamefun old new-equiv ren)))
  :rule-classes :congruence)

Theorem: statement-list-renamefun-renaming-equiv-congruence-on-ren

(defthm statement-list-renamefun-renaming-equiv-congruence-on-ren
  (implies (renaming-equiv ren ren-equiv)
           (equal (statement-list-renamefun old new ren)
                  (statement-list-renamefun old new ren-equiv)))
  :rule-classes :congruence)

Theorem: block-renamefun-block-equiv-congruence-on-old

(defthm block-renamefun-block-equiv-congruence-on-old
  (implies (block-equiv old old-equiv)
           (equal (block-renamefun old new ren)
                  (block-renamefun old-equiv new ren)))
  :rule-classes :congruence)

Theorem: block-renamefun-block-equiv-congruence-on-new

(defthm block-renamefun-block-equiv-congruence-on-new
  (implies (block-equiv new new-equiv)
           (equal (block-renamefun old new ren)
                  (block-renamefun old new-equiv ren)))
  :rule-classes :congruence)

Theorem: block-renamefun-renaming-equiv-congruence-on-ren

(defthm block-renamefun-renaming-equiv-congruence-on-ren
  (implies (renaming-equiv ren ren-equiv)
           (equal (block-renamefun old new ren)
                  (block-renamefun old new ren-equiv)))
  :rule-classes :congruence)

Theorem: block-option-renamefun-block-option-equiv-congruence-on-old

(defthm block-option-renamefun-block-option-equiv-congruence-on-old
  (implies (block-option-equiv old old-equiv)
           (equal (block-option-renamefun old new ren)
                  (block-option-renamefun old-equiv new ren)))
  :rule-classes :congruence)

Theorem: block-option-renamefun-block-option-equiv-congruence-on-new

(defthm block-option-renamefun-block-option-equiv-congruence-on-new
  (implies (block-option-equiv new new-equiv)
           (equal (block-option-renamefun old new ren)
                  (block-option-renamefun old new-equiv ren)))
  :rule-classes :congruence)

Theorem: block-option-renamefun-renaming-equiv-congruence-on-ren

(defthm block-option-renamefun-renaming-equiv-congruence-on-ren
  (implies (renaming-equiv ren ren-equiv)
           (equal (block-option-renamefun old new ren)
                  (block-option-renamefun old new ren-equiv)))
  :rule-classes :congruence)

Theorem: swcase-renamefun-swcase-equiv-congruence-on-old

(defthm swcase-renamefun-swcase-equiv-congruence-on-old
  (implies (swcase-equiv old old-equiv)
           (equal (swcase-renamefun old new ren)
                  (swcase-renamefun old-equiv new ren)))
  :rule-classes :congruence)

Theorem: swcase-renamefun-swcase-equiv-congruence-on-new

(defthm swcase-renamefun-swcase-equiv-congruence-on-new
  (implies (swcase-equiv new new-equiv)
           (equal (swcase-renamefun old new ren)
                  (swcase-renamefun old new-equiv ren)))
  :rule-classes :congruence)

Theorem: swcase-renamefun-renaming-equiv-congruence-on-ren

(defthm swcase-renamefun-renaming-equiv-congruence-on-ren
  (implies (renaming-equiv ren ren-equiv)
           (equal (swcase-renamefun old new ren)
                  (swcase-renamefun old new ren-equiv)))
  :rule-classes :congruence)

Theorem: swcase-list-renamefun-swcase-list-equiv-congruence-on-old

(defthm swcase-list-renamefun-swcase-list-equiv-congruence-on-old
  (implies (swcase-list-equiv old old-equiv)
           (equal (swcase-list-renamefun old new ren)
                  (swcase-list-renamefun old-equiv new ren)))
  :rule-classes :congruence)

Theorem: swcase-list-renamefun-swcase-list-equiv-congruence-on-new

(defthm swcase-list-renamefun-swcase-list-equiv-congruence-on-new
  (implies (swcase-list-equiv new new-equiv)
           (equal (swcase-list-renamefun old new ren)
                  (swcase-list-renamefun old new-equiv ren)))
  :rule-classes :congruence)

Theorem: swcase-list-renamefun-renaming-equiv-congruence-on-ren

(defthm swcase-list-renamefun-renaming-equiv-congruence-on-ren
  (implies (renaming-equiv ren ren-equiv)
           (equal (swcase-list-renamefun old new ren)
                  (swcase-list-renamefun old new ren-equiv)))
  :rule-classes :congruence)

Theorem: fundef-renamefun-fundef-equiv-congruence-on-old

(defthm fundef-renamefun-fundef-equiv-congruence-on-old
  (implies (fundef-equiv old old-equiv)
           (equal (fundef-renamefun old new ren)
                  (fundef-renamefun old-equiv new ren)))
  :rule-classes :congruence)

Theorem: fundef-renamefun-fundef-equiv-congruence-on-new

(defthm fundef-renamefun-fundef-equiv-congruence-on-new
  (implies (fundef-equiv new new-equiv)
           (equal (fundef-renamefun old new ren)
                  (fundef-renamefun old new-equiv ren)))
  :rule-classes :congruence)

Theorem: fundef-renamefun-renaming-equiv-congruence-on-ren

(defthm fundef-renamefun-renaming-equiv-congruence-on-ren
  (implies (renaming-equiv ren ren-equiv)
           (equal (fundef-renamefun old new ren)
                  (fundef-renamefun old new ren-equiv)))
  :rule-classes :congruence)

Theorem: same-statement-kind-when-statement-renamefun

(defthm same-statement-kind-when-statement-renamefun
  (implies (not (reserrp (statement-renamefun old new ren)))
           (equal (statement-kind new)
                  (statement-kind old))))

Subtopics

Statement-renamefun

Check if two statements are related by function renaming.

Fundef-renamefun

Check if two function definitions are related by function renaming.

Swcase-renamefun

Check if two switch cases are related by function renaming.

Swcase-list-renamefun

Check if two lists of switch cases are related by function renaming.

Statement-list-renamefun

Check if two lists of statements are related by function renaming.

Block-renamefun

Check if two blocks are related by function renaming.

Block-option-renamefun

Check if two optional blocks are related by function renaming.