• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
      • Svex-stvs
      • Svex-decomposition-methodology
      • Sv-versus-esim
      • Svex-decomp
      • Svex-compose-dfs
      • Svex-compilation
      • Moddb
      • Svmods
      • Svstmt
        • Svstmt-case
        • Svstmt-while
        • Svstmt-p
        • Svstmt-if
        • Svstmt-equiv
        • Svstmt-xcond
        • Svstmt-scope
        • Svstmt-assign
        • Svstmt-compile
          • Svstmt-compile.lisp
            • Svstate-merge-branches
            • Svex-alist-merge-branches
            • Svstmt-assign->subst
            • Svstack-merge-branches
            • Svstacks-compatible
            • Svjumpstate-merge-svstate-branches
            • Svjumpstate-svstate-compatible
            • Svstmt-lhs-check-masks
            • Svjumpstate
            • Svjumpstates-compatible
            • Svstmtlist-compile-top
            • Svjumpstate-sequence-svstates
            • Constraintlist-merge-branches
            • Svjumpstate-merge-branches
            • Svex-replace-range
            • Svex-svstmt-ite
            • Svstmt-process-write
            • Svjumpstate-sequence
            • Svstmt-process-writelist
            • Svstack-assign
            • Svstmt-writelist-var-sizes
            • Svstates-compatible
            • 4vec-replace-range
            • Svstmt-write-var-sizes
            • Make-empty-svjumpstate
            • Constraintlist-add-pathcond
            • Svjumpstate-pop-scope
            • Constraintlist-compose-svstack
            • Svstack-to-svex-alist
            • Svstack-filter-global-lhs-vars
            • Svjumpstate-vars
            • Svex-svstmt-or
            • Svex-svstmt-andc1
            • Svstate-push-scope
            • Svstate-pop-scope
            • Svstate-vars
            • Svstack-lookup
            • Svar-subtract-delay
            • Svstmt-initialize-locals
            • Svstack-fork
            • Svstack-clean
            • Svstack-nonempty-fix
            • Svstate-fork
            • Svstate-clean
            • Svstack-globalp
            • Svjumpstate-fork
            • Svar-delayed-member
            • Svjumpstate-levels
            • Svjumpstate-free
            • Svstate-free
            • Svstack-free
            • Svstack
            • Svar-size-alist
          • Svstate
        • Svstmt-constraints
        • Svstmt-jump
        • Svstmtlist
        • Svstmt-kind
        • Svstmt.lisp
        • Svstmt-fix
        • Svstmt-count
      • Sv-tutorial
      • Expressions
      • Symbolic-test-vector
      • Vl-to-svex
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Svstmt-compile.lisp

Svstate-merge-branches

Signature

(svstate-merge-branches cond then-st else-st) → merged-st

Arguments

cond — Guard (svex-p cond).

then-st — Guard (svstate-p then-st).

else-st — Guard (svstate-p else-st).

Returns

merged-st — Type (svstate-p merged-st).

Definitions and Theorems

Function: svstate-merge-branches

(defun svstate-merge-branches (cond then-st else-st)
 (declare (xargs :guard (and (svex-p cond)
                             (svstate-p then-st)
                             (svstate-p else-st))))
 (let ((__function__ 'svstate-merge-branches))
   (declare (ignorable __function__))
   (b*
    (((svstate then-st)
      (svstate-fix then-st))
     ((svstate else-st)
      (svstate-fix else-st))
     ((when (hons-equal then-st else-st))
      then-st)
     (blkst
          (svstack-merge-branches cond then-st.blkst else-st.blkst))
     (nonblkst nil)
     (nonblkst (svex-alist-merge-branches
                    then-st.nonblkst cond then-st.nonblkst
                    else-st.nonblkst nonblkst))
     (nonblkst (svex-alist-merge-branches
                    else-st.nonblkst cond then-st.nonblkst
                    else-st.nonblkst nonblkst)))
    (svstate-free then-st)
    (svstate-free else-st)
    (make-svstate :blkst blkst
                  :nonblkst nonblkst))))

Theorem: svstate-p-of-svstate-merge-branches

(defthm svstate-p-of-svstate-merge-branches
  (b* ((merged-st (svstate-merge-branches cond then-st else-st)))
    (svstate-p merged-st))
  :rule-classes :rewrite)

Theorem: svstate-merge-branches-lookup-blkst-when-false

(defthm svstate-merge-branches-lookup-blkst-when-false
 (implies
  (and (equal (4vec-reduction-or (svex-eval cond env))
              0)
       (svstacks-compatible (svstate->blkst then-st)
                            (svstate->blkst else-st)))
  (equal
   (svex-eval
     (svex-lookup
          k
          (svstack-to-svex-alist
               (svstate->blkst
                    (svstate-merge-branches cond then-st else-st))))
     env)
   (if
    (svex-lookup k
                 (svstack-to-svex-alist (svstate->blkst else-st)))
    (svex-eval
      (svex-lookup k
                   (svstack-to-svex-alist (svstate->blkst else-st)))
      env)
    (if
     (svex-lookup k
                  (svstack-to-svex-alist (svstate->blkst then-st)))
     (svex-env-lookup k env)
     (4vec-x))))))

Theorem: svstate-merge-branches-lookup-nonblkst-when-false

(defthm svstate-merge-branches-lookup-nonblkst-when-false
 (implies
  (equal (4vec-reduction-or (svex-eval cond env))
         0)
  (equal
      (svex-eval
           (svex-lookup
                k
                (svstate->nonblkst
                     (svstate-merge-branches cond then-st else-st)))
           env)
      (if (svex-lookup k (svstate->nonblkst else-st))
          (svex-eval (svex-lookup k (svstate->nonblkst else-st))
                     env)
        (if (svex-lookup k (svstate->nonblkst then-st))
            (svex-env-lookup k env)
          (4vec-x))))))

Theorem: svstate-merge-branches-lookup-blkst-under-iff

(defthm svstate-merge-branches-lookup-blkst-under-iff
 (implies
  (double-rewrite (svstacks-compatible (svstate->blkst then-st)
                                       (svstate->blkst else-st)))
  (iff
   (svex-lookup
        k
        (svstack-to-svex-alist
             (svstate->blkst
                  (svstate-merge-branches cond then-st else-st))))
   (or
      (svex-lookup k
                   (svstack-to-svex-alist (svstate->blkst then-st)))
      (svex-lookup
           k
           (svstack-to-svex-alist (svstate->blkst else-st)))))))

Theorem: svstate-merge-branches-lookup-nonblkst-under-iff

(defthm svstate-merge-branches-lookup-nonblkst-under-iff
 (iff
   (svex-lookup k
                (svstate->nonblkst
                     (svstate-merge-branches cond then-st else-st)))
   (or (svex-lookup k (svstate->nonblkst then-st))
       (svex-lookup k (svstate->nonblkst else-st)))))

Theorem: svstate-merge-branches-lookup-blkst-when-true

(defthm svstate-merge-branches-lookup-blkst-when-true
 (implies
  (and (svstacks-compatible (svstate->blkst then-st)
                            (svstate->blkst else-st))
       (equal (4vec-reduction-or (svex-eval cond env))
              -1))
  (equal
   (svex-eval
     (svex-lookup
          k
          (svstack-to-svex-alist
               (svstate->blkst
                    (svstate-merge-branches cond then-st else-st))))
     env)
   (if
    (svex-lookup k
                 (svstack-to-svex-alist (svstate->blkst then-st)))
    (svex-eval
      (svex-lookup k
                   (svstack-to-svex-alist (svstate->blkst then-st)))
      env)
    (if
     (svex-lookup k
                  (svstack-to-svex-alist (svstate->blkst else-st)))
     (svex-env-lookup k env)
     (4vec-x))))))

Theorem: svstate-merge-branches-lookup-nonblkst-when-true

(defthm svstate-merge-branches-lookup-nonblkst-when-true
 (implies
  (equal (4vec-reduction-or (svex-eval cond env))
         -1)
  (equal
      (svex-eval
           (svex-lookup
                k
                (svstate->nonblkst
                     (svstate-merge-branches cond then-st else-st)))
           env)
      (if (svex-lookup k (svstate->nonblkst then-st))
          (svex-eval (svex-lookup k (svstate->nonblkst then-st))
                     env)
        (if (svex-lookup k (svstate->nonblkst else-st))
            (svex-env-lookup k env)
          (4vec-x))))))

Theorem: svstate-merge-branches-blkst-when-true

(defthm svstate-merge-branches-blkst-when-true
 (implies
  (and (equal (4vec-reduction-or (svex-eval cond env))
              -1)
       (svstacks-compatible (svstate->blkst then-st)
                            (svstate->blkst else-st)))
  (svex-envs-similar
   (append
      (svex-alist-eval
           (svstack-to-svex-alist
                (svstate->blkst
                     (svstate-merge-branches cond then-st else-st)))
           env)
      env)
   (append (svex-alist-eval
                (svstack-to-svex-alist (svstate->blkst then-st))
                env)
           env))))

Theorem: svstate-merge-branches-nonblkst-when-true

(defthm svstate-merge-branches-nonblkst-when-true
 (implies
  (equal (4vec-reduction-or (svex-eval cond env))
         -1)
  (svex-envs-similar
    (append (svex-alist-eval
                 (svstate->nonblkst
                      (svstate-merge-branches cond then-st else-st))
                 env)
            env)
    (append (svex-alist-eval (svstate->nonblkst then-st)
                             env)
            env))))

Theorem: svstate-merge-branches-blkst-when-false

(defthm svstate-merge-branches-blkst-when-false
 (implies
  (and (equal (4vec-reduction-or (svex-eval cond env))
              0)
       (svstacks-compatible (svstate->blkst then-st)
                            (svstate->blkst else-st)))
  (svex-envs-similar
   (append
      (svex-alist-eval
           (svstack-to-svex-alist
                (svstate->blkst
                     (svstate-merge-branches cond then-st else-st)))
           env)
      env)
   (append (svex-alist-eval
                (svstack-to-svex-alist (svstate->blkst else-st))
                env)
           env))))

Theorem: svstate-merge-branches-nonblkst-when-false

(defthm svstate-merge-branches-nonblkst-when-false
 (implies
  (equal (4vec-reduction-or (svex-eval cond env))
         0)
  (svex-envs-similar
    (append (svex-alist-eval
                 (svstate->nonblkst
                      (svstate-merge-branches cond then-st else-st))
                 env)
            env)
    (append (svex-alist-eval (svstate->nonblkst else-st)
                             env)
            env))))

Theorem: vars-of-svstate-merge-branches

(defthm vars-of-svstate-merge-branches
  (b* ((?merged-st (svstate-merge-branches cond then-st else-st)))
    (implies
         (and (double-rewrite (svstates-compatible then-st else-st))
              (not (member v (svex-vars cond)))
              (not (member v (svstate-vars then-st)))
              (not (member v (svstate-vars else-st))))
         (not (member v (svstate-vars merged-st))))))

Theorem: svstate-merge-branches-blkst-compatible

(defthm svstate-merge-branches-blkst-compatible
  (b* ((?merged-st (svstate-merge-branches cond then-st else-st)))
    (implies
         (double-rewrite (svstates-compatible then-st else-st))
         (svstates-compatible merged-st (double-rewrite then-st)))))

Theorem: svstate-merge-branches-preserves-blkst-consp

(defthm svstate-merge-branches-preserves-blkst-consp
  (b* ((?merged-st (svstate-merge-branches cond then-st else-st)))
    (implies (and (consp (svstate->blkst then-st))
                  (consp (svstate->blkst else-st)))
             (consp (svstate->blkst merged-st)))))

Theorem: svstate-merge-branches-blkst-len

(defthm svstate-merge-branches-blkst-len
  (b* ((?merged-st (svstate-merge-branches cond then-st else-st)))
    (equal (len (svstate->blkst merged-st))
           (min (len (svstate->blkst then-st))
                (len (svstate->blkst else-st))))))

Theorem: svstate-merge-branches-of-svex-fix-cond

(defthm svstate-merge-branches-of-svex-fix-cond
  (equal (svstate-merge-branches (svex-fix cond)
                                 then-st else-st)
         (svstate-merge-branches cond then-st else-st)))

Theorem: svstate-merge-branches-svex-equiv-congruence-on-cond

(defthm svstate-merge-branches-svex-equiv-congruence-on-cond
  (implies
       (svex-equiv cond cond-equiv)
       (equal (svstate-merge-branches cond then-st else-st)
              (svstate-merge-branches cond-equiv then-st else-st)))
  :rule-classes :congruence)

Theorem: svstate-merge-branches-of-svstate-fix-then-st

(defthm svstate-merge-branches-of-svstate-fix-then-st
  (equal (svstate-merge-branches cond (svstate-fix then-st)
                                 else-st)
         (svstate-merge-branches cond then-st else-st)))

Theorem: svstate-merge-branches-svstate-equiv-congruence-on-then-st

(defthm svstate-merge-branches-svstate-equiv-congruence-on-then-st
  (implies
       (svstate-equiv then-st then-st-equiv)
       (equal (svstate-merge-branches cond then-st else-st)
              (svstate-merge-branches cond then-st-equiv else-st)))
  :rule-classes :congruence)

Theorem: svstate-merge-branches-of-svstate-fix-else-st

(defthm svstate-merge-branches-of-svstate-fix-else-st
  (equal (svstate-merge-branches cond then-st (svstate-fix else-st))
         (svstate-merge-branches cond then-st else-st)))

Theorem: svstate-merge-branches-svstate-equiv-congruence-on-else-st

(defthm svstate-merge-branches-svstate-equiv-congruence-on-else-st
  (implies
       (svstate-equiv else-st else-st-equiv)
       (equal (svstate-merge-branches cond then-st else-st)
              (svstate-merge-branches cond then-st else-st-equiv)))
  :rule-classes :congruence)