• 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
      • Sv-tutorial
      • Expressions
        • Rewriting
        • Svex
          • Svar
          • Least-fixpoint
          • Svex-p
          • Svex-select
          • Svex-alist
          • Svex-equiv
          • Svexlist
            • Svexlist-p
            • Svex-update-nth
            • Svexlist-equiv
            • Svex-nth
            • Svexlist-fix
            • Patbind-svex-nths
          • Svex-call
          • Fnsym
          • Svex-quote
          • Svex-var
          • Svcall-rw
          • Svcall
          • Svex-kind
          • Svcall*
          • Svex-fix
          • Svex-count
          • Svex-1z
          • Svex-1x
          • Svex-z
          • Svex-x
        • Bit-blasting
        • Functions
        • 4vmask
        • Why-infinite-width
        • Svex-vars
        • Evaluation
        • Values
      • Symbolic-test-vector
      • Vl-to-svex
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Svexlist

Svex-update-nth

update-nth for svexlists, with proper fty-discipline.

Signature

(svex-update-nth n v x) → new-x

Arguments

n — Guard (natp n).

v — Guard (svex-p v).

x — Guard (svexlist-p x).

Returns

new-x — Type (svexlist-p new-x).

Definitions and Theorems

Function: svex-update-nth

(defun svex-update-nth (n v x)
  (declare (xargs :guard (and (natp n)
                              (svex-p v)
                              (svexlist-p x))))
  (let ((__function__ 'svex-update-nth))
    (declare (ignorable __function__))
    (mbe :logic (svexlist-fix (update-nth n v x))
         :exec
         (if (<= n (len x))
             (update-nth n v x)
           (append x
                   (replicate (- n (len x))
                              (svex-quote (4vec-x)))
                   (list v))))))

Theorem: svexlist-p-of-svex-update-nth

(defthm svexlist-p-of-svex-update-nth
  (b* ((new-x (svex-update-nth n v x)))
    (svexlist-p new-x))
  :rule-classes :rewrite)

Theorem: svex-update-nth-of-nfix-n

(defthm svex-update-nth-of-nfix-n
  (equal (svex-update-nth (nfix n) v x)
         (svex-update-nth n v x)))

Theorem: svex-update-nth-nat-equiv-congruence-on-n

(defthm svex-update-nth-nat-equiv-congruence-on-n
  (implies (nat-equiv n n-equiv)
           (equal (svex-update-nth n v x)
                  (svex-update-nth n-equiv v x)))
  :rule-classes :congruence)

Theorem: svex-update-nth-of-svex-fix-v

(defthm svex-update-nth-of-svex-fix-v
  (equal (svex-update-nth n (svex-fix v) x)
         (svex-update-nth n v x)))

Theorem: svex-update-nth-svex-equiv-congruence-on-v

(defthm svex-update-nth-svex-equiv-congruence-on-v
  (implies (svex-equiv v v-equiv)
           (equal (svex-update-nth n v x)
                  (svex-update-nth n v-equiv x)))
  :rule-classes :congruence)

Theorem: svex-update-nth-of-svexlist-fix-x

(defthm svex-update-nth-of-svexlist-fix-x
  (equal (svex-update-nth n v (svexlist-fix x))
         (svex-update-nth n v x)))

Theorem: svex-update-nth-svexlist-equiv-congruence-on-x

(defthm svex-update-nth-svexlist-equiv-congruence-on-x
  (implies (svexlist-equiv x x-equiv)
           (equal (svex-update-nth n v x)
                  (svex-update-nth n v x-equiv)))
  :rule-classes :congruence)