• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Community
  • 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
        • Bit-blasting
        • Functions
        • 4vmask
        • Why-infinite-width
        • Svex-vars
        • Evaluation
        • Values
          • 4vec
            • 4vec-operations
            • 4vec-p
            • S4vecs
            • 4vec-examples
            • Maybe-4vec
            • 4vec-equiv
            • Make-4vec
            • 4vec->upper
            • 4vec->lower
            • 4veclist
              • 4veclist-fix
              • 4veclist-p
              • 4veclist-<<=
              • 4veclist-nth-safe
              • 4veclist-equiv
            • 4vec-fix
            • Make-honsed-4vec
            • 4vec-index-p
          • 4vec-<<=
          • 3vec
          • 2vec
          • 2vecx
          • 2vecnatx
          • 4vec-x
          • 4vec-1x
          • 4vec-1z
          • 4vec-z
      • Symbolic-test-vector
      • Vl-to-svex
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• 4veclist

4veclist-nth-safe

Like nth but, with proper fty-discipline for 4veclists. ``Safely'' causes a run-time error if n is out of bounds.

Signature

(4veclist-nth-safe n x) → elt

Arguments

n — Guard (natp n).

x — Guard (4veclist-p x).

Returns

elt — Type (4vec-p elt).

Definitions and Theorems

Function: 4veclist-nth-safe

(defun 4veclist-nth-safe (n x)
 (declare (xargs :guard (and (natp n) (4veclist-p x))))
 (let ((__function__ '4veclist-nth-safe))
   (declare (ignorable __function__))
   (mbe :logic (4vec-fix (nth n x))
        :exec
        (or (nth n x)
            (raise "Index ~x0 too large for 4veclist of length ~x1."
                   n (len x))
            (4vec-x)))))

Theorem: 4vec-p-of-4veclist-nth-safe

(defthm 4vec-p-of-4veclist-nth-safe
  (b* ((elt (4veclist-nth-safe n x)))
    (4vec-p elt))
  :rule-classes :rewrite)

Theorem: 4veclist-nth-safe-of-nfix-n

(defthm 4veclist-nth-safe-of-nfix-n
  (equal (4veclist-nth-safe (nfix n) x)
         (4veclist-nth-safe n x)))

Theorem: 4veclist-nth-safe-nat-equiv-congruence-on-n

(defthm 4veclist-nth-safe-nat-equiv-congruence-on-n
  (implies (nat-equiv n n-equiv)
           (equal (4veclist-nth-safe n x)
                  (4veclist-nth-safe n-equiv x)))
  :rule-classes :congruence)

Theorem: 4veclist-nth-safe-of-4veclist-fix-x

(defthm 4veclist-nth-safe-of-4veclist-fix-x
  (equal (4veclist-nth-safe n (4veclist-fix x))
         (4veclist-nth-safe n x)))

Theorem: 4veclist-nth-safe-4veclist-equiv-congruence-on-x

(defthm 4veclist-nth-safe-4veclist-equiv-congruence-on-x
  (implies (4veclist-equiv x x-equiv)
           (equal (4veclist-nth-safe n x)
                  (4veclist-nth-safe n x-equiv)))
  :rule-classes :congruence)

Theorem: 4veclist-nth-safe-of-nil

(defthm 4veclist-nth-safe-of-nil
  (equal (4veclist-nth-safe n nil)
         (4vec-x)))

Theorem: 4veclist-nth-safe-of-cons

(defthm 4veclist-nth-safe-of-cons
  (implies (syntaxp (quotep n))
           (equal (4veclist-nth-safe n (cons a b))
                  (if (zp n)
                      (4vec-fix a)
                    (4veclist-nth-safe (1- n) b)))))

Theorem: 4veclist-nth-safe-out-of-bounds

(defthm 4veclist-nth-safe-out-of-bounds
  (implies (<= (len x) (nfix n))
           (equal (4veclist-nth-safe n x)
                  (4vec-x))))