• 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
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Soft
      • Bv
      • Imp-language
      • C
      • Event-macros
      • Java
      • Bitcoin
      • Ethereum
      • Yul
        • Transformations
          • Renaming-variables
            • Statements/blocks/cases/fundefs-renamevar
            • Renaming-variables-execution
              • Restrict-vars-when-renamevar
              • Function-environments-when-renaming-variables
              • Exec-when-renamevar
              • Exec-when-renamevar-restrict-vars-lemmas
              • Lstate-match-renamevarp
              • Soutcome-result-renamevarp
              • Lstate-renamevarp
              • Reserr-limitp-theorems
              • Eoutcome-result-renamevarp
              • Eoutcome-renamevarp
              • Soutcome-renamevarp
              • Cstate-renamevarp-with-larger-renaming
              • Cstate-renamevarp
              • Funinfo-renamevarp
              • Funscope-renamevarp
              • Funenv-renamevarp
              • Path/paths-renamevar-theorems
              • Init-local-when-renamevar
              • Write-var/vars-value/values-when-renamevar
              • Add-var/vars-value/values-when-renamevar
              • Read-var/vars-value/values-when-renamevar
              • Vars-of-cstate-after-exec
            • Expressions-renamevar
            • Add-var-to-var-renaming
            • Add-vars-to-var-renaming
            • Renaming-variables-safety
            • 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
      • 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

• Renaming-variables-execution

Eoutcome-renamevarp

Variable renaming relation over expression outcomes.

Signature

(eoutcome-renamevarp old new ren) → yes/no

Arguments

old — Guard (eoutcomep old).

new — Guard (eoutcomep new).

ren — Guard (renamingp ren).

Returns

yes/no — Type (booleanp yes/no).

The underlying computation states must be related, and the two value lists must be the same. The latter condition is because values are not subject to renamings.

Definitions and Theorems

Function: eoutcome-renamevarp

(defun eoutcome-renamevarp (old new ren)
  (declare (xargs :guard (and (eoutcomep old)
                              (eoutcomep new)
                              (renamingp ren))))
  (let ((__function__ 'eoutcome-renamevarp))
    (declare (ignorable __function__))
    (and (cstate-renamevarp (eoutcome->cstate old)
                            (eoutcome->cstate new)
                            ren)
         (equal (eoutcome->values old)
                (eoutcome->values new)))))

Theorem: booleanp-of-eoutcome-renamevarp

(defthm booleanp-of-eoutcome-renamevarp
  (b* ((yes/no (eoutcome-renamevarp old new ren)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: eoutcome-renamevarp-of-eoutcome-fix-old

(defthm eoutcome-renamevarp-of-eoutcome-fix-old
  (equal (eoutcome-renamevarp (eoutcome-fix old)
                              new ren)
         (eoutcome-renamevarp old new ren)))

Theorem: eoutcome-renamevarp-eoutcome-equiv-congruence-on-old

(defthm eoutcome-renamevarp-eoutcome-equiv-congruence-on-old
  (implies (eoutcome-equiv old old-equiv)
           (equal (eoutcome-renamevarp old new ren)
                  (eoutcome-renamevarp old-equiv new ren)))
  :rule-classes :congruence)

Theorem: eoutcome-renamevarp-of-eoutcome-fix-new

(defthm eoutcome-renamevarp-of-eoutcome-fix-new
  (equal (eoutcome-renamevarp old (eoutcome-fix new)
                              ren)
         (eoutcome-renamevarp old new ren)))

Theorem: eoutcome-renamevarp-eoutcome-equiv-congruence-on-new

(defthm eoutcome-renamevarp-eoutcome-equiv-congruence-on-new
  (implies (eoutcome-equiv new new-equiv)
           (equal (eoutcome-renamevarp old new ren)
                  (eoutcome-renamevarp old new-equiv ren)))
  :rule-classes :congruence)

Theorem: eoutcome-renamevarp-of-renaming-fix-ren

(defthm eoutcome-renamevarp-of-renaming-fix-ren
  (equal (eoutcome-renamevarp old new (renaming-fix ren))
         (eoutcome-renamevarp old new ren)))

Theorem: eoutcome-renamevarp-renaming-equiv-congruence-on-ren

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