• 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
        • Language
          • Abstract-syntax
          • Dynamic-semantics
            • Exec
            • Find-fun
            • Init-local
            • Mode
            • Write-vars-values
            • Add-vars-values
            • Add-funs
            • Eoutcome
            • Soutcome
            • Ensure-funscope-disjoint
            • Write-var-value
            • Restrict-vars
            • Add-var-value
            • Funinfo
            • Exec-top-block
            • Values
            • Cstate
            • Funinfo+funenv
            • Read-vars-values
            • Read-var-value
            • Funenv
            • Funscope-for-fundefs
            • Exec-path
            • Path-to-var
            • Funinfo+funenv-result
            • Exec-literal
            • Soutcome-result
            • Mode-set-result
            • Funscope-result
            • Funinfo-result
            • Funenv-result
            • Eoutcome-result
            • Cstate-result
            • Paths-to-vars
            • Funinfo-for-fundef
            • Literal-evaluation
            • Lstate
            • Funscope
            • Mode-set
          • Concrete-syntax
          • Static-soundness
          • Static-semantics
          • Errors
        • 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

• Dynamic-semantics

Init-local

Initialize the local state of a computation state.

Signature

(init-local in-vars in-vals out-vars cstate) → new-cstate

Arguments

in-vars — Guard (identifier-listp in-vars).

in-vals — Guard (value-listp in-vals).

out-vars — Guard (identifier-listp out-vars).

cstate — Guard (cstatep cstate).

Returns

new-cstate — Type (cstate-resultp new-cstate).

This is used at the beginning of the execution of a function call. The local state is set to consist of the input and output variables of the function, which are passed as the in-vars and out-vars parameters. The input variables are initialized with the input values, passed as the in-vals parameters; note that we implicitly check that the number of input variables matches the number of input values. The output variables are initialized to 0.

Definitions and Theorems

Function: init-local

(defun init-local (in-vars in-vals out-vars cstate)
  (declare (xargs :guard (and (identifier-listp in-vars)
                              (value-listp in-vals)
                              (identifier-listp out-vars)
                              (cstatep cstate))))
  (declare (ignore cstate))
  (let ((__function__ 'init-local))
    (declare (ignorable __function__))
    (b* ((cstate (change-cstate cstate :local nil))
         ((okf cstate)
          (add-vars-values in-vars in-vals cstate))
         ((okf cstate)
          (add-vars-values out-vars
                           (repeat (len out-vars) (value 0))
                           cstate)))
      cstate)))

Theorem: cstate-resultp-of-init-local

(defthm cstate-resultp-of-init-local
  (b* ((new-cstate (init-local in-vars in-vals out-vars cstate)))
    (cstate-resultp new-cstate))
  :rule-classes :rewrite)

Theorem: error-info-wfp-of-init-local

(defthm error-info-wfp-of-init-local
  (b* ((?new-cstate (init-local in-vars in-vals out-vars cstate)))
    (implies (reserrp new-cstate)
             (error-info-wfp new-cstate))))

Theorem: init-local-of-identifier-list-fix-in-vars

(defthm init-local-of-identifier-list-fix-in-vars
  (equal (init-local (identifier-list-fix in-vars)
                     in-vals out-vars cstate)
         (init-local in-vars in-vals out-vars cstate)))

Theorem: init-local-identifier-list-equiv-congruence-on-in-vars

(defthm init-local-identifier-list-equiv-congruence-on-in-vars
  (implies
       (identifier-list-equiv in-vars in-vars-equiv)
       (equal (init-local in-vars in-vals out-vars cstate)
              (init-local in-vars-equiv in-vals out-vars cstate)))
  :rule-classes :congruence)

Theorem: init-local-of-value-list-fix-in-vals

(defthm init-local-of-value-list-fix-in-vals
  (equal (init-local in-vars (value-list-fix in-vals)
                     out-vars cstate)
         (init-local in-vars in-vals out-vars cstate)))

Theorem: init-local-value-list-equiv-congruence-on-in-vals

(defthm init-local-value-list-equiv-congruence-on-in-vals
  (implies
       (value-list-equiv in-vals in-vals-equiv)
       (equal (init-local in-vars in-vals out-vars cstate)
              (init-local in-vars in-vals-equiv out-vars cstate)))
  :rule-classes :congruence)

Theorem: init-local-of-identifier-list-fix-out-vars

(defthm init-local-of-identifier-list-fix-out-vars
  (equal (init-local in-vars
                     in-vals (identifier-list-fix out-vars)
                     cstate)
         (init-local in-vars in-vals out-vars cstate)))

Theorem: init-local-identifier-list-equiv-congruence-on-out-vars

(defthm init-local-identifier-list-equiv-congruence-on-out-vars
  (implies
       (identifier-list-equiv out-vars out-vars-equiv)
       (equal (init-local in-vars in-vals out-vars cstate)
              (init-local in-vars in-vals out-vars-equiv cstate)))
  :rule-classes :congruence)

Theorem: init-local-of-cstate-fix-cstate

(defthm init-local-of-cstate-fix-cstate
  (equal (init-local in-vars
                     in-vals out-vars (cstate-fix cstate))
         (init-local in-vars in-vals out-vars cstate)))

Theorem: init-local-cstate-equiv-congruence-on-cstate

(defthm init-local-cstate-equiv-congruence-on-cstate
  (implies
       (cstate-equiv cstate cstate-equiv)
       (equal (init-local in-vars in-vals out-vars cstate)
              (init-local in-vars in-vals out-vars cstate-equiv)))
  :rule-classes :congruence)