• 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
          • 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

• Transformations

Dead-code-eliminator-static-safety

Proof that the DeadCodeEliminator transformation preserves the static safety checks.

Definitions and Theorems

Theorem: check-safe-statement-of-statement-dead

(defthm check-safe-statement-of-statement-dead
 (implies
    (and (statement-nofunp stmt)
         (statement-noloopinitp stmt))
    (b* ((varsmodes (check-safe-statement stmt varset funtab))
         (varsmodes-dead (check-safe-statement (statement-dead stmt)
                                               varset funtab)))
      (implies (not (reserrp varsmodes))
               (and (not (reserrp varsmodes-dead))
                    (equal (vars+modes->vars varsmodes-dead)
                           (vars+modes->vars varsmodes))
                    (subset (vars+modes->modes varsmodes-dead)
                            (vars+modes->modes varsmodes)))))))

Theorem: check-safe-statement-list-of-statement-list-dead

(defthm check-safe-statement-list-of-statement-list-dead
 (implies
    (and (statement-list-nofunp stmts)
         (statement-list-noloopinitp stmts))
    (b* ((varsmodes (check-safe-statement-list stmts varset funtab))
         (varsmodes-dead
              (check-safe-statement-list (statement-list-dead stmts)
                                         varset funtab)))
      (implies (not (reserrp varsmodes))
               (and (not (reserrp varsmodes-dead))
                    (subset (vars+modes->modes varsmodes-dead)
                            (vars+modes->modes varsmodes)))))))

Theorem: check-safe-block-of-block-dead

(defthm check-safe-block-of-block-dead
  (implies (and (block-nofunp block)
                (block-noloopinitp block))
           (b* ((modes (check-safe-block block varset funtab))
                (modes-dead (check-safe-block (block-dead block)
                                              varset funtab)))
             (implies (not (reserrp modes))
                      (and (not (reserrp modes-dead))
                           (subset modes-dead modes))))))

Theorem: check-safe-block-option-of-block-option-dead

(defthm check-safe-block-option-of-block-option-dead
 (implies
   (and (block-option-nofunp block?)
        (block-option-noloopinitp block?))
   (b*
    ((modes (check-safe-block-option block? varset funtab))
     (modes-dead (check-safe-block-option (block-option-dead block?)
                                          varset funtab)))
    (implies (not (reserrp modes))
             (and (not (reserrp modes-dead))
                  (subset modes-dead modes))))))

Theorem: check-safe-swcase-of-swcase-dead

(defthm check-safe-swcase-of-swcase-dead
  (implies (and (swcase-nofunp case)
                (swcase-noloopinitp case))
           (b* ((modes (check-safe-swcase case varset funtab))
                (modes-dead (check-safe-swcase (swcase-dead case)
                                               varset funtab)))
             (implies (not (reserrp modes))
                      (and (not (reserrp modes-dead))
                           (subset modes-dead modes))))))

Theorem: check-safe-swcase-list-of-swcase-list

(defthm check-safe-swcase-list-of-swcase-list
 (implies
   (and (swcase-list-nofunp cases)
        (swcase-list-noloopinitp cases))
   (b* ((modes (check-safe-swcase-list cases varset funtab))
        (modes-dead (check-safe-swcase-list (swcase-list-dead cases)
                                            varset funtab)))
     (implies (not (reserrp modes))
              (and (not (reserrp modes-dead))
                   (subset modes-dead modes))))))

Theorem: check-safe-fundef-of-fundef-dead

(defthm check-safe-fundef-of-fundef-dead
  (implies (and (fundef-nofunp fundef)
                (fundef-noloopinitp fundef)
                (not (reserrp (check-safe-fundef fundef funtab))))
           (not (reserrp (check-safe-fundef (fundef-dead fundef)
                                            funtab)))))