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

Variable renaming relation over expression outcome results.

Signature

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

Arguments

old — Guard (eoutcome-resultp old).

new — Guard (eoutcome-resultp new).

ren — Guard (renamingp ren).

Returns

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

Either they are both (possibly different) errors, or they are related expression outcomes.

Definitions and Theorems

Function: eoutcome-result-renamevarp

(defun eoutcome-result-renamevarp (old new ren)
  (declare (xargs :guard (and (eoutcome-resultp old)
                              (eoutcome-resultp new)
                              (renamingp ren))))
  (let ((__function__ 'eoutcome-result-renamevarp))
    (declare (ignorable __function__))
    (b* ((old (eoutcome-result-fix old))
         (new (eoutcome-result-fix new)))
      (or (and (reserrp old) (reserrp new))
          (and (not (reserrp old))
               (not (reserrp new))
               (eoutcome-renamevarp old new ren))))))

Theorem: booleanp-of-eoutcome-result-renamevarp

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

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

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

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

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

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

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

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

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

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

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

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

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