• 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
            • Dead-code-eliminator-execution
              • Exec-of-dead
              • Soutcome-result-okeq
              • Eoutcome-result-okeq
              • Funscope-dead
              • Funinfo+funenv-result-dead
              • Funinfo+funenv-dead
              • Funinfo-dead
              • Funscope-result-dead
              • Funenv-result-dead
              • Funenv-dead
              • Add-funs-of-dead
              • Funscope-for-fundefs-of-dead
              • Funinfo-for-fundef-of-dead
              • Ensure-funscope-disjoint-of-dead
              • Find-fun-of-dead
            • Statements/blocks/cases/fundefs-dead
            • Fundef-list-dead
          • 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

• Dead-code-eliminator-execution

Funinfo+funenv-result-dead

Eliminate dead code in errors and pairs consisting of function information and a function environment.

Signature

(funinfo+funenv-result-dead funinfoenv?) → new-funinfoenv?

Arguments

funinfoenv? — Guard (funinfo+funenv-resultp funinfoenv?).

Returns

new-funinfoenv? — Type (funinfo+funenv-resultp new-funinfoenv?).

We transform the pairs and leave errors unchanged.

Definitions and Theorems

Function: funinfo+funenv-result-dead

(defun funinfo+funenv-result-dead (funinfoenv?)
  (declare (xargs :guard (funinfo+funenv-resultp funinfoenv?)))
  (let ((__function__ 'funinfo+funenv-result-dead))
    (declare (ignorable __function__))
    (b* ((funinfoenv? (funinfo+funenv-result-fix funinfoenv?)))
      (if (reserrp funinfoenv?)
          funinfoenv?
        (funinfo+funenv-dead funinfoenv?)))))

Theorem: funinfo+funenv-resultp-of-funinfo+funenv-result-dead

(defthm funinfo+funenv-resultp-of-funinfo+funenv-result-dead
  (b* ((new-funinfoenv? (funinfo+funenv-result-dead funinfoenv?)))
    (funinfo+funenv-resultp new-funinfoenv?))
  :rule-classes :rewrite)

Theorem: funinfo+funenv-result-dead-of-funinfo+funenv-result-fix-funinfoenv?

(defthm
 funinfo+funenv-result-dead-of-funinfo+funenv-result-fix-funinfoenv?
 (equal (funinfo+funenv-result-dead
             (funinfo+funenv-result-fix funinfoenv?))
        (funinfo+funenv-result-dead funinfoenv?)))

Theorem: funinfo+funenv-result-dead-funinfo+funenv-result-equiv-congruence-on-funinfoenv?

(defthm
 funinfo+funenv-result-dead-funinfo+funenv-result-equiv-congruence-on-funinfoenv?
 (implies
      (funinfo+funenv-result-equiv funinfoenv? funinfoenv?-equiv)
      (equal (funinfo+funenv-result-dead funinfoenv?)
             (funinfo+funenv-result-dead funinfoenv?-equiv)))
 :rule-classes :congruence)