		Search-engine friendly clone of the ACL2 documentation.

Svstmt-compile.lisp

Svex-replace-range

Signature
(svex-replace-range expr &key lsb width val) → res
Arguments: expr — Expression to update.
Guard (svex-p expr).; lsb — Guard (natp lsb).; width — Guard (natp width).; val — Thing to install into expr[lsb+width-1:lsb].
Guard (svex-p val).
Returns: res — Type (svex-p res).

Definitions and Theorems

Function: svex-replace-range-fn

(defun svex-replace-range-fn (expr lsb width val)
  (declare (xargs :guard (and (svex-p expr)
                              (natp lsb)
                              (natp width)
                              (svex-p val))))
  (let ((__function__ 'svex-replace-range))
    (declare (ignorable __function__))
    (b* ((high-part (svex-rsh (+ (lnfix width) (lnfix lsb))
                              expr))
         (new+high (svex-concat width val high-part)))
      (svex-concat lsb expr new+high))))

Theorem: svex-p-of-svex-replace-range

(defthm svex-p-of-svex-replace-range
  (b* ((res (svex-replace-range-fn expr lsb width val)))
    (svex-p res))
  :rule-classes :rewrite)

Theorem: svex-replace-range-correct

(defthm svex-replace-range-correct
  (equal (svex-eval (svex-replace-range x
                                        :lsb lsb
                                        :width width
                                        :val val)
                    env)
         (4vec-replace-range (svex-eval x env)
                             :lsb lsb
                             :width width
                             :val (svex-eval val env))))

Theorem: vars-of-svex-replace-range

(defthm vars-of-svex-replace-range
 (implies (and (not (member v (svex-vars expr)))
               (not (member v (svex-vars val))))
          (not (member v
                       (svex-vars (svex-replace-range expr
                                                      :lsb lsb
                                                      :width width
                                                      :val val))))))

Theorem: svex-replace-range-fn-of-svex-fix-expr

(defthm svex-replace-range-fn-of-svex-fix-expr
  (equal (svex-replace-range-fn (svex-fix expr)
                                lsb width val)
         (svex-replace-range-fn expr lsb width val)))

Theorem: svex-replace-range-fn-svex-equiv-congruence-on-expr

(defthm svex-replace-range-fn-svex-equiv-congruence-on-expr
  (implies (svex-equiv expr expr-equiv)
           (equal (svex-replace-range-fn expr lsb width val)
                  (svex-replace-range-fn expr-equiv lsb width val)))
  :rule-classes :congruence)

Theorem: svex-replace-range-fn-of-nfix-lsb

(defthm svex-replace-range-fn-of-nfix-lsb
  (equal (svex-replace-range-fn expr (nfix lsb)
                                width val)
         (svex-replace-range-fn expr lsb width val)))

Theorem: svex-replace-range-fn-nat-equiv-congruence-on-lsb

(defthm svex-replace-range-fn-nat-equiv-congruence-on-lsb
  (implies (nat-equiv lsb lsb-equiv)
           (equal (svex-replace-range-fn expr lsb width val)
                  (svex-replace-range-fn expr lsb-equiv width val)))
  :rule-classes :congruence)

Theorem: svex-replace-range-fn-of-nfix-width

(defthm svex-replace-range-fn-of-nfix-width
  (equal (svex-replace-range-fn expr lsb (nfix width)
                                val)
         (svex-replace-range-fn expr lsb width val)))

Theorem: svex-replace-range-fn-nat-equiv-congruence-on-width

(defthm svex-replace-range-fn-nat-equiv-congruence-on-width
  (implies (nat-equiv width width-equiv)
           (equal (svex-replace-range-fn expr lsb width val)
                  (svex-replace-range-fn expr lsb width-equiv val)))
  :rule-classes :congruence)

Theorem: svex-replace-range-fn-of-svex-fix-val

(defthm svex-replace-range-fn-of-svex-fix-val
  (equal (svex-replace-range-fn expr lsb width (svex-fix val))
         (svex-replace-range-fn expr lsb width val)))

Theorem: svex-replace-range-fn-svex-equiv-congruence-on-val

(defthm svex-replace-range-fn-svex-equiv-congruence-on-val
  (implies (svex-equiv val val-equiv)
           (equal (svex-replace-range-fn expr lsb width val)
                  (svex-replace-range-fn expr lsb width val-equiv)))
  :rule-classes :congruence)