		Search-engine friendly clone of the ACL2 documentation.

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)