		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Moddb-mod-totalwires

Signature
(moddb-mod-totalwires modidx moddb) → totalwires
Arguments: modidx — Guard (natp modidx).; moddb — Guard (moddb-basics-ok moddb).
Returns: totalwires — Type (natp totalwires).

Definitions and Theorems

Function: moddb-mod-totalwires

(defun moddb-mod-totalwires (modidx moddb)
  (declare (xargs :stobjs (moddb)))
  (declare (xargs :guard (and (natp modidx)
                              (moddb-basics-ok moddb))))
  (declare (xargs :guard (< modidx (moddb->nmods moddb))))
  (let ((__function__ 'moddb-mod-totalwires))
    (declare (ignorable __function__))
    (b* (((unless (mbt (< (lnfix modidx)
                          (moddb->nmods moddb))))
          0)
         ((stobj-get totalwires)
          ((elab-mod (moddb->modsi modidx moddb)))
          (elab-mod->totalwires elab-mod)))
      totalwires)))

Theorem: natp-of-moddb-mod-totalwires

(defthm natp-of-moddb-mod-totalwires
  (b* ((totalwires (moddb-mod-totalwires modidx moddb)))
    (natp totalwires))
  :rule-classes :type-prescription)

Theorem: moddb-mod-totalwires-in-terms-of-wireoffset

(defthm moddb-mod-totalwires-in-terms-of-wireoffset
 (implies
   (moddb-mods-ok moddb)
   (equal (moddb-mod-totalwires modidx moddb)
          (moddb-mod-inst-wireoffset (moddb-mod-ninsts modidx moddb)
                                     modidx moddb)))
 :rule-classes
 ((:definition
       :install-body nil
       :clique (moddb-mod-inst-wireoffset moddb-mod-totalwires)
       :controller-alist ((moddb-mod-inst-wireoffset t t nil)
                          (moddb-mod-totalwires t nil)))))

Theorem: moddb-mod-inst-wireoffset-recursive

(defthm moddb-mod-inst-wireoffset-recursive
 (implies
  (moddb-mods-ok moddb)
  (equal
   (moddb-mod-inst-wireoffset instidx modidx moddb)
   (if (>= (nfix modidx)
           (nfix (moddb->nmods moddb)))
       0
    (if (or (zp instidx)
            (zp (elab-mod$a-ninsts (moddb->modsi modidx moddb))))
        (elab-mod$a-nwires (moddb->modsi modidx moddb))
     (+
      (moddb-mod-inst-wireoffset (1- instidx)
                                 modidx moddb)
      (let*
       ((submod-idx
             (elab-mod$a->inst-modidx (1- instidx)
                                      (moddb->modsi modidx moddb))))
       (if
         (and (< submod-idx (nfix modidx))
              (<= (nfix instidx)
                  (elab-mod$a-ninsts (moddb->modsi modidx moddb))))
         (moddb-mod-totalwires submod-idx moddb)
         0)))))))
 :rule-classes
 ((:definition
       :install-body nil
       :clique (moddb-mod-inst-wireoffset moddb-mod-totalwires)
       :controller-alist ((moddb-mod-inst-wireoffset t t nil)
                          (moddb-mod-totalwires t nil)))))

Theorem: moddb-mod-inst-wireoffset-monotonic

(defthm moddb-mod-inst-wireoffset-monotonic
  (implies (and (<= (nfix n) (nfix m))
                (moddb-mods-ok moddb))
           (<= (moddb-mod-inst-wireoffset n modidx moddb)
               (moddb-mod-inst-wireoffset m modidx moddb)))
  :rule-classes (:rewrite :linear))

Theorem: moddb-totalwires-rewrite

(defthm moddb-totalwires-rewrite
 (implies
  (< (nfix modidx)
     (nfix (moddb->nmods moddb)))
  (nat-equiv (g :totalwires (nth modidx (nth *moddb->modsi* moddb)))
             (moddb-mod-totalwires modidx moddb))))

Theorem: moddb-mod-totalwires-of-nfix-modidx

(defthm moddb-mod-totalwires-of-nfix-modidx
  (equal (moddb-mod-totalwires (nfix modidx)
                               moddb)
         (moddb-mod-totalwires modidx moddb)))

Theorem: moddb-mod-totalwires-nat-equiv-congruence-on-modidx

(defthm moddb-mod-totalwires-nat-equiv-congruence-on-modidx
  (implies (nat-equiv modidx modidx-equiv)
           (equal (moddb-mod-totalwires modidx moddb)
                  (moddb-mod-totalwires modidx-equiv moddb)))
  :rule-classes :congruence)

Theorem: moddb-mod-totalwires-of-moddb-fix-moddb

(defthm moddb-mod-totalwires-of-moddb-fix-moddb
  (equal (moddb-mod-totalwires modidx (moddb-fix moddb))
         (moddb-mod-totalwires modidx moddb)))

Theorem: moddb-mod-totalwires-moddb-equiv-congruence-on-moddb

(defthm moddb-mod-totalwires-moddb-equiv-congruence-on-moddb
  (implies (moddb-equiv moddb moddb-equiv)
           (equal (moddb-mod-totalwires modidx moddb)
                  (moddb-mod-totalwires modidx moddb-equiv)))
  :rule-classes :congruence)