		Search-engine friendly clone of the ACL2 documentation.

Svstmt-compile.lisp

Svstmt-process-write

Signature
(svstmt-process-write write blockingp nb-delayp xcond st) → (mv new-st lhs)
Arguments: write — Guard (svstmt-write-p write).; st — Guard (svstate-p st).
Returns: new-st — Type (svstate-p new-st).; lhs — Type (lhs-p lhs).

Definitions and Theorems

Function: svstmt-process-write

(defun svstmt-process-write (write blockingp nb-delayp xcond st)
 (declare (xargs :guard (and (svstmt-write-p write)
                             (svstate-p st))))
 (let ((__function__ 'svstmt-process-write))
  (declare (ignorable __function__))
  (b*
   (((svstmt-write write))
    ((svstate st))
    (svstack (if blockingp st.blkst
               (cons st.nonblkst st.blkst)))
    (lhs-indices
     (if xcond
         (4veclist-quote
              (svexlist-xeval (svex-select->indices write.lhs)))
      (svexlist-maskfree-rewrite
          (svexlist-compose-svstack (svex-select->indices write.lhs)
                                    svstack))))
    (rhs (svex-compose-svstack write.rhs svstack))
    (rhs (if (and (eq nb-delayp t) (not blockingp))
             (svex-add-delay rhs 1)
           rhs))
    (rhs (if xcond (svex-x) rhs))
    (lhs-select (svex-select-replace-indices write.lhs lhs-indices))
    (lhs-var (svex-select-inner-var write.lhs))
    (var-value (or (svstack-lookup lhs-var svstack)
                   (svex-var lhs-var)))
    ((mv static-lhs-select static-rhs)
     (svex-select-staticify-assignment lhs-select rhs var-value))
    (lhs (svex-select-to-lhs static-lhs-select))
    (st (svstmt-assign->subst lhs static-rhs 0 blockingp st)))
   (mv st lhs))))

Theorem: svstate-p-of-svstmt-process-write.new-st

(defthm svstate-p-of-svstmt-process-write.new-st
  (b* (((mv ?new-st ?lhs)
        (svstmt-process-write write blockingp nb-delayp xcond st)))
    (svstate-p new-st))
  :rule-classes :rewrite)

Theorem: lhs-p-of-svstmt-process-write.lhs

(defthm lhs-p-of-svstmt-process-write.lhs
  (b* (((mv ?new-st ?lhs)
        (svstmt-process-write write blockingp nb-delayp xcond st)))
    (lhs-p lhs))
  :rule-classes :rewrite)

Theorem: svstates-compatible-of-svstmt-process-write

(defthm svstates-compatible-of-svstmt-process-write
  (b* (((mv ?new-st ?lhs)
        (svstmt-process-write write blockingp nb-delayp xcond st)))
    (implies (consp (svstate->blkst st))
             (svstates-compatible new-st st))))

Theorem: svarlist-addr-p-of-svstmt-process-write

(defthm svarlist-addr-p-of-svstmt-process-write
  (b* (((mv ?new-st ?lhs)
        (svstmt-process-write write blockingp nb-delayp xcond st)))
    (implies (and (svarlist-addr-p (svstmt-write-vars write))
                  (svarlist-addr-p (svstate-vars st)))
             (svarlist-addr-p (svstate-vars new-st)))))

Theorem: svstmt-process-write-of-svstmt-write-fix-write

(defthm svstmt-process-write-of-svstmt-write-fix-write
  (equal (svstmt-process-write (svstmt-write-fix write)
                               blockingp nb-delayp xcond st)
         (svstmt-process-write write blockingp nb-delayp xcond st)))

Theorem: svstmt-process-write-svstmt-write-equiv-congruence-on-write

(defthm svstmt-process-write-svstmt-write-equiv-congruence-on-write
 (implies
    (svstmt-write-equiv write write-equiv)
    (equal (svstmt-process-write write blockingp nb-delayp xcond st)
           (svstmt-process-write write-equiv
                                 blockingp nb-delayp xcond st)))
 :rule-classes :congruence)

Theorem: svstmt-process-write-of-svstate-fix-st

(defthm svstmt-process-write-of-svstate-fix-st
  (equal (svstmt-process-write write blockingp
                               nb-delayp xcond (svstate-fix st))
         (svstmt-process-write write blockingp nb-delayp xcond st)))

Theorem: svstmt-process-write-svstate-equiv-congruence-on-st

(defthm svstmt-process-write-svstate-equiv-congruence-on-st
 (implies
  (svstate-equiv st st-equiv)
  (equal (svstmt-process-write write blockingp nb-delayp xcond st)
         (svstmt-process-write write
                               blockingp nb-delayp xcond st-equiv)))
 :rule-classes :congruence)