• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
    • Apt
    • Zfc
    • Acre
    • Milawa
    • Smtlink
    • Abnf
    • Vwsim
    • Isar
    • Wp-gen
    • Dimacs-reader
    • Pfcs
    • Legacy-defrstobj
    • C
    • Proof-checker-array
    • Soft
    • Farray
    • Rp-rewriter
    • Instant-runoff-voting
    • Imp-language
    • Sidekick
    • Ethereum
    • Leftist-trees
    • Java
    • Riscv
    • Taspi
    • Bitcoin
    • Zcash
    • Des
    • X86isa
    • Sha-2
    • 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
    • Proof-checker-itp13
    • Regex
    • ACL2-programming-language
    • Json
    • Jfkr
    • Equational
    • Cryptography
    • Axe
    • Poseidon
    • Where-do-i-place-my-book
    • Aleo
    • Bigmems
    • Builtins
    • Execloader
    • Solidity
    • Paco
    • Concurrent-programs
    • Bls12-377-curves
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • 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)))))