		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Elab-mod-initialize-aliases

Signature
(elab-mod-initialize-aliases idx elab-mod offset lhsarr) → lhsarr1
Arguments: idx — Guard (natp idx).; offset — Guard (natp offset).
Returns: lhsarr1 — Type (lhslist-p lhsarr1).

Definitions and Theorems

Function: elab-mod-initialize-aliases

(defun elab-mod-initialize-aliases (idx elab-mod offset lhsarr)
 (declare (xargs :stobjs (elab-mod lhsarr)))
 (declare (xargs :guard (and (natp idx) (natp offset))))
 (declare
      (xargs :guard (and (<= (+ offset (elab-mod-nwires elab-mod))
                             (lhss-length lhsarr))
                         (<= idx (elab-mod-nwires elab-mod)))))
 (let ((__function__ 'elab-mod-initialize-aliases))
  (declare (ignorable __function__))
  (b* (((when (mbe :logic (or (zp (- (elab-mod-nwires elab-mod)
                                     (nfix idx)))
                              (zp (- (lhss-length lhsarr)
                                     (+ (nfix offset) (nfix idx)))))
                   :exec (eql (elab-mod-nwires elab-mod) idx)))
        (lhsarr-fix lhsarr))
       ((wire xf)
        (elab-mod-wiretablei idx elab-mod))
       (widx (+ (lnfix idx) (lnfix offset)))
       (lhs (list (lhrange xf.width
                           (lhatom-var (make-svar :name widx) 0))))
       (lhsarr (set-lhs widx lhs lhsarr)))
    (elab-mod-initialize-aliases (1+ (lnfix idx))
                                 elab-mod offset lhsarr))))

Theorem: lhslist-p-of-elab-mod-initialize-aliases

(defthm lhslist-p-of-elab-mod-initialize-aliases
  (b*
    ((lhsarr1
          (elab-mod-initialize-aliases idx elab-mod offset lhsarr)))
    (lhslist-p lhsarr1))
  :rule-classes :rewrite)

Theorem: elab-mod-initialize-aliases-of-nfix-idx

(defthm elab-mod-initialize-aliases-of-nfix-idx
  (equal (elab-mod-initialize-aliases (nfix idx)
                                      elab-mod offset lhsarr)
         (elab-mod-initialize-aliases idx elab-mod offset lhsarr)))

Theorem: elab-mod-initialize-aliases-nat-equiv-congruence-on-idx

(defthm elab-mod-initialize-aliases-nat-equiv-congruence-on-idx
 (implies
  (nat-equiv idx idx-equiv)
  (equal
    (elab-mod-initialize-aliases idx elab-mod offset lhsarr)
    (elab-mod-initialize-aliases idx-equiv elab-mod offset lhsarr)))
 :rule-classes :congruence)

Theorem: elab-mod-initialize-aliases-of-elab-mod$a-fix-elab-mod

(defthm elab-mod-initialize-aliases-of-elab-mod$a-fix-elab-mod
  (equal (elab-mod-initialize-aliases idx (elab-mod$a-fix elab-mod)
                                      offset lhsarr)
         (elab-mod-initialize-aliases idx elab-mod offset lhsarr)))

Theorem: elab-mod-initialize-aliases-elab-mod$a-equiv-congruence-on-elab-mod

(defthm
 elab-mod-initialize-aliases-elab-mod$a-equiv-congruence-on-elab-mod
 (implies
  (elab-mod$a-equiv elab-mod elab-mod-equiv)
  (equal
    (elab-mod-initialize-aliases idx elab-mod offset lhsarr)
    (elab-mod-initialize-aliases idx elab-mod-equiv offset lhsarr)))
 :rule-classes :congruence)

Theorem: elab-mod-initialize-aliases-of-nfix-offset

(defthm elab-mod-initialize-aliases-of-nfix-offset
  (equal (elab-mod-initialize-aliases idx elab-mod (nfix offset)
                                      lhsarr)
         (elab-mod-initialize-aliases idx elab-mod offset lhsarr)))

Theorem: elab-mod-initialize-aliases-nat-equiv-congruence-on-offset

(defthm elab-mod-initialize-aliases-nat-equiv-congruence-on-offset
 (implies
  (nat-equiv offset offset-equiv)
  (equal
    (elab-mod-initialize-aliases idx elab-mod offset lhsarr)
    (elab-mod-initialize-aliases idx elab-mod offset-equiv lhsarr)))
 :rule-classes :congruence)

Theorem: elab-mod-initialize-aliases-of-lhslist-fix-lhsarr

(defthm elab-mod-initialize-aliases-of-lhslist-fix-lhsarr
 (equal
  (elab-mod-initialize-aliases idx
                               elab-mod offset (lhslist-fix lhsarr))
  (elab-mod-initialize-aliases idx elab-mod offset lhsarr)))

Theorem: elab-mod-initialize-aliases-lhslist-equiv-congruence-on-lhsarr

(defthm
     elab-mod-initialize-aliases-lhslist-equiv-congruence-on-lhsarr
 (implies
  (lhslist-equiv lhsarr lhsarr-equiv)
  (equal
    (elab-mod-initialize-aliases idx elab-mod offset lhsarr)
    (elab-mod-initialize-aliases idx elab-mod offset lhsarr-equiv)))
 :rule-classes :congruence)

Theorem: len-of-elab-mod-initialize-aliases

(defthm len-of-elab-mod-initialize-aliases
 (equal
      (len (elab-mod-initialize-aliases idx elab-mod offset lhsarr))
      (len lhsarr)))

Theorem: lookup-in-elab-mod-initialize-aliases

(defthm lookup-in-elab-mod-initialize-aliases
 (equal
      (nth n
           (elab-mod-initialize-aliases idx elab-mod offset lhsarr))
      (if (and (<= (+ (nfix idx) (nfix offset))
                   (nfix n))
               (< (nfix n)
                  (+ (nfix offset)
                     (elab-mod-nwires elab-mod)))
               (< (nfix n) (len lhsarr)))
          (b* (((wire xf)
                (elab-mod-wiretablei (- (nfix n) (nfix offset))
                                     elab-mod)))
            (list (lhrange xf.width
                           (lhatom-var (make-svar :name (nfix n))
                                       0))))
        (lhs-fix (nth n lhsarr)))))

Theorem: aliases-normorderedp-of-elab-mod-initialize-aliases

(defthm aliases-normorderedp-of-elab-mod-initialize-aliases
 (implies
   (aliases-normorderedp aliases)
   (aliases-normorderedp
        (elab-mod-initialize-aliases idx elab-mod offset aliases))))