• 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

Soutcome-renamevarp

Variable renaming relation over statement outcomes.

Signature

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

Arguments

old — Guard (soutcomep old).

new — Guard (soutcomep new).

ren — Guard (renamingp ren).

Returns

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

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

Definitions and Theorems

Function: soutcome-renamevarp

(defun soutcome-renamevarp (old new ren)
  (declare (xargs :guard (and (soutcomep old)
                              (soutcomep new)
                              (renamingp ren))))
  (let ((__function__ 'soutcome-renamevarp))
    (declare (ignorable __function__))
    (and (cstate-renamevarp (soutcome->cstate old)
                            (soutcome->cstate new)
                            ren)
         (equal (soutcome->mode old)
                (soutcome->mode new)))))

Theorem: booleanp-of-soutcome-renamevarp

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

Theorem: soutcome-renamevarp-of-soutcome-fix-old

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

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

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

Theorem: soutcome-renamevarp-of-soutcome-fix-new

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

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

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

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

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

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

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