• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
      • Crypto-hdwallet
      • Error-checking
      • Apt
      • Abnf
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Prime-field-constraint-systems
      • Soft
      • Bv
      • Imp-language
      • Event-macros
      • Bitcoin
      • Ethereum
      • Yul
        • Transformations
        • Language
          • Abstract-syntax
          • Dynamic-semantics
          • Concrete-syntax
          • Static-soundness
            • Static-soundess-of-execution
            • Theorems-about-cstate-to-vars-and-execution
            • Static-soundness-theorems-about-add-funs
            • Static-soundness-theorems-about-modes
            • Static-soundness-theorems-about-init-local
            • Check-var-list
            • Funinfo-safep
            • Static-soundness-theorems-about-find-fun
            • Funenv-to-funtable
            • Theorems-about-checking-expression-lists-in-reverse
            • Static-soundness-of-variable-writing
            • Funscope-to-funtable
            • Funenv-safep
            • Funscope-safep
            • Cstate-to-vars
            • Funinfo-to-funtype
            • Static-soundness-of-variable-addition
            • Static-soundness-of-variable-reading
            • Static-soundness-of-literal-execution
            • Exec-top-block-static-soundness
            • Static-soundness-of-path-execution
          • Static-semantics
          • Errors
        • Yul-json
      • Zcash
      • ACL2-programming-language
      • Prime-fields
      • Java
      • C
      • Syntheto
      • Number-theory
      • Cryptography
      • Lists-light
      • File-io-light
      • Json
      • Built-ins
      • Solidity
      • Axe
      • Std-extensions
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Execloader
    • Axe
  • Testing-utilities
  • Math

• Static-soundness

Static-soundness-of-variable-writing

Theorems about the static soundness of variable writing.

If check-safe-path and check-safe-path-list succeeds, also write-var-value and write-vars-values do. These are proved by showing that path checking ensures the success of path-to-var and paths-to-vars, and also the success of check-var and check-var-list. Then we show that check-var and check-var-list ensure that write-var-value and write-vars-values succeed, and finally we put things together.

Definitions and Theorems

Theorem: path-to-var-when-check-safe-path

(defthm path-to-var-when-check-safe-path
        (implies (not (reserrp (check-safe-path path varset)))
                 (not (reserrp (path-to-var path)))))

Theorem: check-var-when-check-safe-path

(defthm check-var-when-check-safe-path
        (implies (not (reserrp (check-safe-path path varset)))
                 (check-var (path-to-var path) varset)))

Theorem: paths-to-vars-when-check-safe-path-list

(defthm paths-to-vars-when-check-safe-path-list
        (implies (not (reserrp (check-safe-path-list paths varset)))
                 (not (reserrp (paths-to-vars paths)))))

Theorem: check-var-list-when-check-safe-path-list

(defthm check-var-list-when-check-safe-path-list
        (implies (not (reserrp (check-safe-path-list paths varset)))
                 (check-var-list (paths-to-vars paths)
                                 varset)))

Theorem: write-var-value-when-check-var

(defthm write-var-value-when-check-var
        (implies (check-var var (cstate-to-vars cstate))
                 (not (reserrp (write-var-value var val cstate)))))

Theorem: write-var-value-when-check-safe-path

(defthm
 write-var-value-when-check-safe-path
 (implies
      (not (reserrp (check-safe-path path (cstate-to-vars cstate))))
      (not (reserrp (write-var-value (path-to-var path)
                                     val cstate)))))

Theorem: write-vars-values-when-check-var-list

(defthm
     write-vars-values-when-check-var-list
     (implies (and (check-var-list vars (cstate-to-vars cstate))
                   (equal (len vals) (len vars)))
              (not (reserrp (write-vars-values vars vals cstate)))))

Theorem: write-vars-values-when-check-safe-path-list

(defthm
 write-vars-values-when-check-safe-path-list
 (implies
  (and
   (not
     (reserrp (check-safe-path-list paths (cstate-to-vars cstate))))
   (equal (len vals) (len paths)))
  (not (reserrp (write-vars-values (paths-to-vars paths)
                                   vals cstate)))))