		Search-engine friendly clone of the ACL2 documentation.

Debug.lisp

Svtv-debug-eval-aliases-track

Signature
(svtv-debug-eval-aliases-track n aliases wirevals vcd-vals) → (mv changes vcd-vals1)
Arguments: n — Guard (natp n).; wirevals — Guard (svex-env-p wirevals).
Returns: changes — Type (nat-listp changes).

Definitions and Theorems

Function: svtv-debug-eval-aliases-track

(defun svtv-debug-eval-aliases-track (n aliases wirevals vcd-vals)
 (declare (xargs :stobjs (aliases vcd-vals)))
 (declare (xargs :guard (and (natp n) (svex-env-p wirevals))))
 (declare (xargs :guard (and (<= n (aliass-length aliases))
                             (<= (aliass-length aliases)
                                 (4vecs-length vcd-vals)))))
 (let ((__function__ 'svtv-debug-eval-aliases-track))
   (declare (ignorable __function__))
   (b* (((when (mbe :logic (zp (- (aliass-length aliases) (nfix n)))
                    :exec (eql (aliass-length aliases) n)))
         (mv nil vcd-vals))
        (lhs (get-alias n aliases))
        (val (svtv-debug-lhs-eval lhs n wirevals vcd-vals))
        (prev-val (get-4vec n vcd-vals))
        (vcd-vals (set-4vec n val vcd-vals))
        ((when (equal prev-val val))
         (svtv-debug-eval-aliases-track (1+ (lnfix n))
                                        aliases wirevals vcd-vals))
        ((mv rest-changes vcd-vals)
         (svtv-debug-eval-aliases-track (1+ (lnfix n))
                                        aliases wirevals vcd-vals)))
     (mv (cons (lnfix n) rest-changes)
         vcd-vals))))

Theorem: nat-listp-of-svtv-debug-eval-aliases-track.changes

(defthm nat-listp-of-svtv-debug-eval-aliases-track.changes
 (b* (((mv ?changes ?vcd-vals1)
       (svtv-debug-eval-aliases-track n aliases wirevals vcd-vals)))
   (nat-listp changes))
 :rule-classes :rewrite)

Theorem: len-vcd-vals-of-svtv-debug-eval-aliases-track

(defthm len-vcd-vals-of-svtv-debug-eval-aliases-track
 (<=
  (len vcd-vals)
  (len
   (mv-nth
      1
      (svtv-debug-eval-aliases-track n aliases wirevals vcd-vals))))
 :rule-classes :linear)

Theorem: nat-list-max-of-svtv-debug-eval-aliases-track

(defthm nat-list-max-of-svtv-debug-eval-aliases-track
 (implies
  (consp
   (mv-nth
       0
       (svtv-debug-eval-aliases-track n aliases wirevals vcd-vals)))
  (<
   (nat-list-max
    (mv-nth
       0
       (svtv-debug-eval-aliases-track n aliases wirevals vcd-vals)))
   (len aliases)))
 :rule-classes :linear)

Theorem: svtv-debug-eval-aliases-track-of-nfix-n

(defthm svtv-debug-eval-aliases-track-of-nfix-n
  (equal
       (svtv-debug-eval-aliases-track (nfix n)
                                      aliases wirevals vcd-vals)
       (svtv-debug-eval-aliases-track n aliases wirevals vcd-vals)))

Theorem: svtv-debug-eval-aliases-track-nat-equiv-congruence-on-n

(defthm svtv-debug-eval-aliases-track-nat-equiv-congruence-on-n
 (implies
  (nat-equiv n n-equiv)
  (equal (svtv-debug-eval-aliases-track n aliases wirevals vcd-vals)
         (svtv-debug-eval-aliases-track
              n-equiv aliases wirevals vcd-vals)))
 :rule-classes :congruence)

Theorem: svtv-debug-eval-aliases-track-of-lhslist-fix-aliases

(defthm svtv-debug-eval-aliases-track-of-lhslist-fix-aliases
  (equal
       (svtv-debug-eval-aliases-track n (lhslist-fix aliases)
                                      wirevals vcd-vals)
       (svtv-debug-eval-aliases-track n aliases wirevals vcd-vals)))

Theorem: svtv-debug-eval-aliases-track-lhslist-equiv-congruence-on-aliases

(defthm
  svtv-debug-eval-aliases-track-lhslist-equiv-congruence-on-aliases
 (implies
  (lhslist-equiv aliases aliases-equiv)
  (equal (svtv-debug-eval-aliases-track n aliases wirevals vcd-vals)
         (svtv-debug-eval-aliases-track
              n aliases-equiv wirevals vcd-vals)))
 :rule-classes :congruence)

Theorem: svtv-debug-eval-aliases-track-of-svex-env-fix-wirevals

(defthm svtv-debug-eval-aliases-track-of-svex-env-fix-wirevals
 (equal
    (svtv-debug-eval-aliases-track n aliases (svex-env-fix wirevals)
                                   vcd-vals)
    (svtv-debug-eval-aliases-track n aliases wirevals vcd-vals)))

Theorem: svtv-debug-eval-aliases-track-svex-env-equiv-congruence-on-wirevals

(defthm
 svtv-debug-eval-aliases-track-svex-env-equiv-congruence-on-wirevals
 (implies
  (svex-env-equiv wirevals wirevals-equiv)
  (equal (svtv-debug-eval-aliases-track n aliases wirevals vcd-vals)
         (svtv-debug-eval-aliases-track
              n aliases wirevals-equiv vcd-vals)))
 :rule-classes :congruence)