• 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
            • Statements/blocks/cases/fundefs-renamevar
            • Renaming-variables-execution
            • Expressions-renamevar
            • Add-var-to-var-renaming
            • Add-vars-to-var-renaming
            • Renaming-variables-safety
              • Renaming-variables-statements/blocks/cases/fundefs-safety
              • Renaming-variables-expression-safety
              • Theorems-about-function-tables-and-variable-renaming
              • Varset-old
              • Varset-new
              • Varset-old/new-of-add-var/vars-to-var-renaming
              • Check-safe-path/paths-when-path/paths-renamevar
              • Add-var/vars-not-error-when-add-var/vars-to-var-renaming
              • Check-var-when-var-renamevar
            • Fundef-list-renamevar
            • Expression-option-renamevar
            • Funcall-option-renamevar
            • Path-list-renamevar
            • Var-list-renamevar
            • Var-renamevar
            • Path-renamevar
          • Dead-code-eliminator
          • Renamings
          • Disambiguator
          • Unique-variables
          • 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
      • 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-variables-safety

Check-safe-path/paths-when-path/paths-renamevar

If two (lists of) paths are related by variable renaming, the safety of the old one implies the safety of the new one.

Definitions and Theorems

Theorem: check-safe-path-when-path-renamevar

(defthm check-safe-path-when-path-renamevar
  (implies (not (reserrp (path-renamevar old new ren)))
           (b* ((ok-old (check-safe-path old (varset-old ren)))
                (ok-new (check-safe-path new (varset-new ren))))
             (implies (not (reserrp ok-old))
                      (not (reserrp ok-new))))))

Theorem: check-safe-path-list-when-path-list-renamevar

(defthm check-safe-path-list-when-path-list-renamevar
 (implies (not (reserrp (path-list-renamevar old new ren)))
          (b* ((ok-old (check-safe-path-list old (varset-old ren)))
               (ok-new (check-safe-path-list new (varset-new ren))))
            (implies (not (reserrp ok-old))
                     (not (reserrp ok-new))))))