• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • 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
        • Address
          • Svarlist-add-delay
          • Svarlist-addr-p
          • Address-fix
          • Svex-alist-add-delay
          • Svarlist-addr-p-badguy
          • Svar-add-delay
          • Make-scoped-svar
          • Address-p
          • Address-equiv
          • Make-address
          • Svar-addr-p
          • Svar-addr-fix
          • Change-address
          • Address->scope
          • Address->path
          • Address->index
          • Svar->address
          • Make-simple-svar
          • Address->svar
          • Svex-add-delay-top
          • Addr-scope
        • Wire
        • Module
        • Lhs
        • Path
        • Svar-add-namespace
        • Design
        • Modinst
        • Lhs-add-namespace
        • Modalist
        • Path-add-namespace
        • Modname->submodnames
        • Name
        • Constraintlist-addr-p
        • Svex-alist-addr-p
        • Svar-map-addr-p
        • Lhspairs-addr-p
        • Modname
        • Assigns-addr-p
        • Lhs-addr-p
        • Lhatom-addr-p
        • Modhier-list-measure
        • Attributes
        • Modhier-measure
        • Modhier-list-measure-aux
        • Modhier-loopfreelist-p
        • Modhier-loopfree-p
      • Svstmt
      • Sv-tutorial
      • Expressions
      • Symbolic-test-vector
      • Vl-to-svex
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Address

Svarlist-add-delay

(svarlist-add-delay x delay) maps svar-add-delay across a list.

Signature

(svarlist-add-delay x delay) → xx

Arguments

x — Guard (svarlist-p x).

delay — Guard (natp delay).

Returns

xx — Type (and (svarlist-p xx) (implies (svarlist-addr-p x) (svarlist-addr-p xx))) .

This is an ordinary defprojection.

Definitions and Theorems

Function: svarlist-add-delay-exec

(defun svarlist-add-delay-exec (x delay acc)
 (declare (xargs :guard (and (svarlist-p x) (natp delay))))
 (declare (xargs :guard t))
 (let ((__function__ 'svarlist-add-delay-exec))
   (declare (ignorable __function__))
   (if (consp x)
       (svarlist-add-delay-exec (cdr x)
                                delay
                                (cons (svar-add-delay (car x) delay)
                                      acc))
     acc)))

Function: svarlist-add-delay-nrev

(defun svarlist-add-delay-nrev (x delay acl2::nrev)
 (declare (xargs :stobjs (acl2::nrev)))
 (declare (xargs :guard (and (svarlist-p x) (natp delay))))
 (declare (xargs :guard t))
 (let ((__function__ 'svarlist-add-delay-nrev))
  (declare (ignorable __function__))
  (if (atom x)
      (acl2::nrev-fix acl2::nrev)
   (let ((acl2::nrev (acl2::nrev-push (svar-add-delay (car x) delay)
                                      acl2::nrev)))
     (svarlist-add-delay-nrev (cdr x)
                              delay acl2::nrev)))))

Function: svarlist-add-delay

(defun svarlist-add-delay (x delay)
  (declare (xargs :guard (and (svarlist-p x) (natp delay))))
  (declare (xargs :guard t))
  (let ((__function__ 'svarlist-add-delay))
    (declare (ignorable __function__))
    (mbe :logic
         (if (consp x)
             (cons (svar-add-delay (car x) delay)
                   (svarlist-add-delay (cdr x) delay))
           nil)
         :exec
         (if (atom x)
             nil
           (acl2::with-local-nrev
                (svarlist-add-delay-nrev x delay acl2::nrev))))))

Theorem: return-type-of-svarlist-add-delay

(defthm return-type-of-svarlist-add-delay
  (b* ((xx (svarlist-add-delay x delay)))
    (and (svarlist-p xx)
         (implies (svarlist-addr-p x)
                  (svarlist-addr-p xx))))
  :rule-classes :rewrite)

Theorem: svarlist-add-delay-of-svarlist-fix-x

(defthm svarlist-add-delay-of-svarlist-fix-x
  (equal (svarlist-add-delay (svarlist-fix x)
                             delay)
         (svarlist-add-delay x delay)))

Theorem: svarlist-add-delay-svarlist-equiv-congruence-on-x

(defthm svarlist-add-delay-svarlist-equiv-congruence-on-x
  (implies (svarlist-equiv x x-equiv)
           (equal (svarlist-add-delay x delay)
                  (svarlist-add-delay x-equiv delay)))
  :rule-classes :congruence)

Theorem: svarlist-add-delay-of-nfix-delay

(defthm svarlist-add-delay-of-nfix-delay
  (equal (svarlist-add-delay x (nfix delay))
         (svarlist-add-delay x delay)))

Theorem: svarlist-add-delay-nat-equiv-congruence-on-delay

(defthm svarlist-add-delay-nat-equiv-congruence-on-delay
  (implies (nat-equiv delay delay-equiv)
           (equal (svarlist-add-delay x delay)
                  (svarlist-add-delay x delay-equiv)))
  :rule-classes :congruence)

Theorem: set-equiv-congruence-over-svarlist-add-delay

(defthm set-equiv-congruence-over-svarlist-add-delay
  (implies (set-equiv x y)
           (set-equiv (svarlist-add-delay x delay)
                      (svarlist-add-delay y delay)))
  :rule-classes ((:congruence)))

Theorem: subsetp-of-svarlist-add-delay-when-subsetp

(defthm subsetp-of-svarlist-add-delay-when-subsetp
  (implies (subsetp x y)
           (subsetp (svarlist-add-delay x delay)
                    (svarlist-add-delay y delay)))
  :rule-classes ((:rewrite)))

Theorem: member-of-svar-add-delay-in-svarlist-add-delay

(defthm member-of-svar-add-delay-in-svarlist-add-delay
  (implies (member acl2::k x)
           (member (svar-add-delay acl2::k delay)
                   (svarlist-add-delay x delay)))
  :rule-classes ((:rewrite)))

Theorem: svarlist-add-delay-nrev-removal

(defthm svarlist-add-delay-nrev-removal
  (equal (svarlist-add-delay-nrev x delay acl2::nrev)
         (append acl2::nrev
                 (svarlist-add-delay x delay)))
  :rule-classes ((:rewrite)))

Theorem: svarlist-add-delay-exec-removal

(defthm svarlist-add-delay-exec-removal
  (equal (svarlist-add-delay-exec x delay acl2::acc)
         (revappend (svarlist-add-delay x delay)
                    acl2::acc))
  :rule-classes ((:rewrite)))

Theorem: svarlist-add-delay-of-rev

(defthm svarlist-add-delay-of-rev
  (equal (svarlist-add-delay (rev x) delay)
         (rev (svarlist-add-delay x delay)))
  :rule-classes ((:rewrite)))

Theorem: svarlist-add-delay-of-list-fix

(defthm svarlist-add-delay-of-list-fix
  (equal (svarlist-add-delay (list-fix x) delay)
         (svarlist-add-delay x delay))
  :rule-classes ((:rewrite)))

Theorem: svarlist-add-delay-of-append

(defthm svarlist-add-delay-of-append
  (equal (svarlist-add-delay (append acl2::a acl2::b)
                             delay)
         (append (svarlist-add-delay acl2::a delay)
                 (svarlist-add-delay acl2::b delay)))
  :rule-classes ((:rewrite)))

Theorem: cdr-of-svarlist-add-delay

(defthm cdr-of-svarlist-add-delay
  (equal (cdr (svarlist-add-delay x delay))
         (svarlist-add-delay (cdr x) delay))
  :rule-classes ((:rewrite)))

Theorem: car-of-svarlist-add-delay

(defthm car-of-svarlist-add-delay
  (equal (car (svarlist-add-delay x delay))
         (and (consp x)
              (svar-add-delay (car x) delay)))
  :rule-classes ((:rewrite)))

Theorem: svarlist-add-delay-under-iff

(defthm svarlist-add-delay-under-iff
  (iff (svarlist-add-delay x delay)
       (consp x))
  :rule-classes ((:rewrite)))

Theorem: consp-of-svarlist-add-delay

(defthm consp-of-svarlist-add-delay
  (equal (consp (svarlist-add-delay x delay))
         (consp x))
  :rule-classes ((:rewrite)))

Theorem: len-of-svarlist-add-delay

(defthm len-of-svarlist-add-delay
  (equal (len (svarlist-add-delay x delay))
         (len x))
  :rule-classes ((:rewrite)))

Theorem: true-listp-of-svarlist-add-delay

(defthm true-listp-of-svarlist-add-delay
  (true-listp (svarlist-add-delay x delay))
  :rule-classes :type-prescription)

Theorem: svarlist-add-delay-when-not-consp

(defthm svarlist-add-delay-when-not-consp
  (implies (not (consp x))
           (equal (svarlist-add-delay x delay)
                  nil))
  :rule-classes ((:rewrite)))

Theorem: svarlist-add-delay-of-cons

(defthm svarlist-add-delay-of-cons
  (equal (svarlist-add-delay (cons acl2::a acl2::b)
                             delay)
         (cons (svar-add-delay acl2::a delay)
               (svarlist-add-delay acl2::b delay)))
  :rule-classes ((:rewrite)))

Theorem: svarlist-add-delay-when-0

(defthm svarlist-add-delay-when-0
  (equal (svarlist-add-delay x 0)
         (svarlist-fix x)))