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

• Renaming-variables-execution

Exec-when-renamevar-restrict-vars-lemmas

Theorems about restricting variables in parallel executions related by variable renaming.

See restrict-vars-when-renamevar for background and motivation. The following two lemmas are make use of the theorems there to show that, during the execution of certain constructs, the variable renaming relation between computation states is preserved. These lemmas are directly used in the main theorems.

Definitions and Theorems

Theorem: exec-when-renamevar-restrict-vars-lemma-1

(defthm exec-when-renamevar-restrict-vars-lemma-1
 (implies
  (and
   (not
       (reserrp (statement-list-renamevar old-stmts new-stmts ren)))
   (not (reserrp (exec-statement-list
                      old-stmts old-cstate
                      (add-funs (statements-to-fundefs old-stmts)
                                old-funenv)
                      (+ -1 limit))))
   (not (reserrp (exec-statement-list
                      new-stmts new-cstate
                      (add-funs (statements-to-fundefs new-stmts)
                                new-funenv)
                      (+ -1 limit))))
   (cstate-renamevarp old-cstate new-cstate ren)
   (cstate-renamevarp
        (soutcome->cstate
             (exec-statement-list
                  old-stmts old-cstate
                  (add-funs (statements-to-fundefs old-stmts)
                            old-funenv)
                  (+ -1 limit)))
        (soutcome->cstate
             (exec-statement-list
                  new-stmts new-cstate
                  (add-funs (statements-to-fundefs new-stmts)
                            new-funenv)
                  (+ -1 limit)))
        (statement-list-renamevar old-stmts new-stmts ren)))
  (cstate-renamevarp
       (restrict-vars
            (omap::keys (cstate->local old-cstate))
            (soutcome->cstate
                 (exec-statement-list
                      old-stmts old-cstate
                      (add-funs (statements-to-fundefs old-stmts)
                                old-funenv)
                      (+ -1 limit))))
       (restrict-vars
            (omap::keys (cstate->local new-cstate))
            (soutcome->cstate
                 (exec-statement-list
                      new-stmts new-cstate
                      (add-funs (statements-to-fundefs new-stmts)
                                new-funenv)
                      (+ -1 limit))))
       ren)))

Theorem: exec-when-renamevar-restrict-vars-lemma-2

(defthm exec-when-renamevar-restrict-vars-lemma-2
 (implies
  (and
   (not
       (reserrp (statement-list-renamevar old-stmts new-stmts ren)))
   (not (reserrp (exec-statement-list
                      old-stmts old-cstate
                      (add-funs (statements-to-fundefs old-stmts)
                                old-funenv)
                      (+ -1 limit))))
   (not (reserrp (exec-statement-list
                      new-stmts new-cstate
                      (add-funs (statements-to-fundefs new-stmts)
                                new-funenv)
                      (+ -1 limit))))
   (cstate-renamevarp old-cstate new-cstate ren)
   (cstate-renamevarp
        (soutcome->cstate
             (exec-statement-list
                  old-stmts old-cstate
                  (add-funs (statements-to-fundefs old-stmts)
                            old-funenv)
                  (+ -1 limit)))
        (soutcome->cstate
             (exec-statement-list
                  new-stmts new-cstate
                  (add-funs (statements-to-fundefs new-stmts)
                            new-funenv)
                  (+ -1 limit)))
        (statement-list-renamevar old-stmts new-stmts ren))
   (not
     (reserrp
          (exec-for-iterations
               old-test old-update old-body
               (soutcome->cstate
                    (exec-statement-list
                         old-stmts old-cstate
                         (add-funs (statements-to-fundefs old-stmts)
                                   old-funenv)
                         (+ -1 limit)))
               (add-funs (statements-to-fundefs old-stmts)
                         old-funenv)
               (+ -1 limit))))
   (not
     (reserrp
          (exec-for-iterations
               new-test new-update new-body
               (soutcome->cstate
                    (exec-statement-list
                         new-stmts new-cstate
                         (add-funs (statements-to-fundefs new-stmts)
                                   new-funenv)
                         (+ -1 limit)))
               (add-funs (statements-to-fundefs new-stmts)
                         new-funenv)
               (+ -1 limit))))
   (cstate-renamevarp
     (soutcome->cstate
          (exec-for-iterations
               old-test old-update old-body
               (soutcome->cstate
                    (exec-statement-list
                         old-stmts old-cstate
                         (add-funs (statements-to-fundefs old-stmts)
                                   old-funenv)
                         (+ -1 limit)))
               (add-funs (statements-to-fundefs old-stmts)
                         old-funenv)
               (+ -1 limit)))
     (soutcome->cstate
          (exec-for-iterations
               new-test new-update new-body
               (soutcome->cstate
                    (exec-statement-list
                         new-stmts new-cstate
                         (add-funs (statements-to-fundefs new-stmts)
                                   new-funenv)
                         (+ -1 limit)))
               (add-funs (statements-to-fundefs new-stmts)
                         new-funenv)
               (+ -1 limit)))
     (statement-list-renamevar old-stmts new-stmts ren)))
  (cstate-renamevarp
   (restrict-vars
     (omap::keys (cstate->local old-cstate))
     (soutcome->cstate
          (exec-for-iterations
               old-test old-update old-body
               (soutcome->cstate
                    (exec-statement-list
                         old-stmts old-cstate
                         (add-funs (statements-to-fundefs old-stmts)
                                   old-funenv)
                         (+ -1 limit)))
               (add-funs (statements-to-fundefs old-stmts)
                         old-funenv)
               (+ -1 limit))))
   (restrict-vars
     (omap::keys (cstate->local new-cstate))
     (soutcome->cstate
          (exec-for-iterations
               new-test new-update new-body
               (soutcome->cstate
                    (exec-statement-list
                         new-stmts new-cstate
                         (add-funs (statements-to-fundefs new-stmts)
                                   new-funenv)
                         (+ -1 limit)))
               (add-funs (statements-to-fundefs new-stmts)
                         new-funenv)
               (+ -1 limit))))
   ren)))