		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Moddb-mod-ok

Signature
(moddb-mod-ok modidx moddb) → *
Arguments: modidx — Guard (natp modidx).

Definitions and Theorems

Function: moddb-mod-ok

(defun moddb-mod-ok (modidx moddb)
 (declare (xargs :stobjs (moddb)))
 (declare (xargs :guard (natp modidx)))
 (declare (xargs :guard (and (< modidx (moddb->nmods moddb))
                             (<= (moddb->nmods moddb)
                                 (moddb->mods-length moddb)))))
 (let ((__function__ 'moddb-mod-ok))
  (declare (ignorable __function__))
  (b*
   (((unless (moddb-mod-order-ok modidx moddb))
     nil)
    ((unless (moddb-mod-insts-ok modidx moddb))
     nil)
    ((unless (mbt (< (lnfix modidx)
                     (lnfix (moddb->nmods moddb)))))
     t)
    ((stobj-get totwires totinsts ninsts)
     ((elab-mod (moddb->modsi modidx moddb)))
     (mv (elab-mod->totalwires elab-mod)
         (elab-mod->totalinsts elab-mod)
         (elab-mod-ninsts elab-mod)))
    (totwires-spec (moddb-mod-inst-wireoffset ninsts modidx moddb))
    (totinsts-spec (moddb-mod-inst-instoffset ninsts modidx moddb)))
   (and (equal totwires-spec totwires)
        (equal totinsts-spec totinsts)))))

Theorem: moddb-mod-ok-implies-order-ok

(defthm moddb-mod-ok-implies-order-ok
  (implies (moddb-mod-ok modidx moddb)
           (moddb-mod-order-ok modidx moddb)))

Theorem: moddb-mod-ok-implies-modinsts-ok

(defthm moddb-mod-ok-implies-modinsts-ok
  (implies (moddb-mod-ok modidx moddb)
           (moddb-mod-insts-ok modidx moddb)))

Theorem: moddb-mod-ok-implies-totalwires

(defthm moddb-mod-ok-implies-totalwires
 (implies
  (and (moddb-mod-ok modidx moddb)
       (< (lnfix modidx)
          (lnfix (moddb->nmods moddb))))
  (nat-equiv
    (g :totalwires (nth modidx (nth *moddb->modsi* moddb)))
    (moddb-mod-inst-wireoffset
         (elab-mod$a-ninsts (nth modidx (nth *moddb->modsi* moddb)))
         modidx moddb))))

Theorem: moddb-mod-ok-implies-totalinsts

(defthm moddb-mod-ok-implies-totalinsts
 (implies
  (and (moddb-mod-ok modidx moddb)
       (< (lnfix modidx)
          (lnfix (moddb->nmods moddb))))
  (nat-equiv
    (g :totalinsts (nth modidx (nth *moddb->modsi* moddb)))
    (moddb-mod-inst-instoffset
         (elab-mod$a-ninsts (nth modidx (nth *moddb->modsi* moddb)))
         modidx moddb))))

Theorem: moddb-mod-inst-wireoffset-greater-norm

(defthm moddb-mod-inst-wireoffset-greater-norm
 (implies
  (and
   (<= (elab-mod$a-ninsts (nth modidx (nth *moddb->modsi* moddb)))
       (nfix instidx))
   (equal
        newidx
        (elab-mod$a-ninsts (nth modidx (nth *moddb->modsi* moddb))))
   (equal oldidx (nfix instidx))
   (syntaxp (not (equal oldidx newidx))))
  (equal (moddb-mod-inst-wireoffset instidx modidx moddb)
         (moddb-mod-inst-wireoffset newidx modidx moddb))))

Theorem: moddb-mod-inst-instoffset-greater-norm

(defthm moddb-mod-inst-instoffset-greater-norm
 (implies
  (and
   (<= (elab-mod$a-ninsts (nth modidx (nth *moddb->modsi* moddb)))
       (nfix instidx))
   (equal
    newidx
    (nfix
       (elab-mod$a-ninsts (nth modidx (nth *moddb->modsi* moddb)))))
   (equal oldidx (nfix instidx))
   (syntaxp (not (equal oldidx newidx))))
  (equal (moddb-mod-inst-instoffset instidx modidx moddb)
         (moddb-mod-inst-instoffset newidx modidx moddb))))

Theorem: moddb-mod-ok-implies-wire-offset

(defthm moddb-mod-ok-implies-wire-offset
 (implies
  (and (moddb-mod-ok modidx moddb)
       (< (lnfix modidx)
          (lnfix (moddb->nmods moddb))))
  (equal
       (elab-mod-wireoffset instidx
                            (nth modidx (nth *moddb->modsi* moddb)))
       (moddb-mod-inst-wireoffset instidx modidx moddb))))

Theorem: moddb-mod-ok-implies-inst-offset

(defthm moddb-mod-ok-implies-inst-offset
 (implies
  (and (moddb-mod-ok modidx moddb)
       (< (lnfix modidx)
          (lnfix (moddb->nmods moddb))))
  (equal
       (elab-mod-instoffset instidx
                            (nth modidx (nth *moddb->modsi* moddb)))
       (moddb-mod-inst-instoffset instidx modidx moddb))))

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

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

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

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

Theorem: moddb-mod-ok-of-moddb-fix-moddb

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

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

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

Theorem: moddb-mod-ok-of-moddb-norm-moddb

(defthm moddb-mod-ok-of-moddb-norm-moddb
  (equal (moddb-mod-ok modidx (moddb-norm moddb))
         (moddb-mod-ok modidx moddb)))

Theorem: moddb-mod-ok-moddb-norm-equiv-congruence-on-moddb

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