		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Moddb-modinst-ok

Signature
(moddb-modinst-ok instidx modidx moddb) → *
Arguments: instidx — Guard (natp instidx).; modidx — Guard (natp modidx).

Definitions and Theorems

Function: moddb-modinst-ok

(defun moddb-modinst-ok (instidx modidx moddb)
 (declare (xargs :stobjs (moddb)))
 (declare (xargs :guard (and (natp instidx) (natp modidx))))
 (declare
  (xargs
     :guard (and (< modidx (moddb->nmods moddb))
                 (<= (moddb->nmods moddb)
                     (moddb->mods-length moddb))
                 (moddb-mod-order-ok modidx moddb)
                 (stobj-let ((elab-mod (moddb->modsi modidx moddb)))
                            (ok)
                            (< instidx (elab-mod-ninsts elab-mod))
                            ok))))
 (let ((__function__ 'moddb-modinst-ok))
  (declare (ignorable __function__))
  (b*
   (((unless
       (mbt (and (< (lnfix modidx)
                    (lnfix (moddb->nmods moddb)))
                 (stobj-let ((elab-mod (moddb->modsi modidx moddb)))
                            (ok)
                            (< (lnfix instidx)
                               (elab-mod-ninsts elab-mod))
                            ok))))
     t)
    ((stobj-get instname wireoffset instoffset)
     ((elab-mod (moddb->modsi modidx moddb)))
     (mv (elab-mod->instname instidx elab-mod)
         (elab-mod->inst-wireoffset instidx elab-mod)
         (elab-mod->inst-instoffset instidx elab-mod)))
    (wireoffset-spec
         (moddb-mod-inst-wireoffset instidx modidx moddb))
    (instoffset-spec
         (moddb-mod-inst-instoffset instidx modidx moddb))
    ((unless (eql wireoffset wireoffset-spec))
     (cw "Bad wire offset in ~s0: ~x1, should be ~x2~%"
         instname wireoffset wireoffset-spec))
    ((unless (eql instoffset instoffset-spec))
     (cw "Bad inst offset in ~s0: ~x1, should be ~x2~%"
         instname instoffset instoffset-spec)))
   t)))

Theorem: moddb-modinst-ok-of-nfix-instidx

(defthm moddb-modinst-ok-of-nfix-instidx
  (equal (moddb-modinst-ok (nfix instidx)
                           modidx moddb)
         (moddb-modinst-ok instidx modidx moddb)))

Theorem: moddb-modinst-ok-nat-equiv-congruence-on-instidx

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

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

(defthm moddb-modinst-ok-of-nfix-modidx
  (equal (moddb-modinst-ok instidx (nfix modidx)
                           moddb)
         (moddb-modinst-ok instidx modidx moddb)))

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

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

Theorem: moddb-modinst-ok-of-moddb-fix-moddb

(defthm moddb-modinst-ok-of-moddb-fix-moddb
  (equal (moddb-modinst-ok instidx modidx (moddb-fix moddb))
         (moddb-modinst-ok instidx modidx moddb)))

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

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

Theorem: moddb-modinst-ok-implies-instoffset

(defthm moddb-modinst-ok-implies-instoffset
 (implies
  (and
    (moddb-modinst-ok instidx modidx moddb)
    (< (nfix modidx)
       (nfix (nth *moddb->nmods* moddb)))
    (< (nfix instidx)
       (elab-mod$a-ninsts (nth modidx (nth *moddb->modsi* moddb)))))
  (equal (elab-mod$a->inst-instoffset
              instidx
              (nth modidx (nth *moddb->modsi* moddb)))
         (moddb-mod-inst-instoffset instidx modidx moddb))))

Theorem: moddb-modinst-ok-implies-wireoffset

(defthm moddb-modinst-ok-implies-wireoffset
 (implies
  (and
    (moddb-modinst-ok instidx modidx moddb)
    (< (nfix modidx)
       (nfix (nth *moddb->nmods* moddb)))
    (< (nfix instidx)
       (elab-mod$a-ninsts (nth modidx (nth *moddb->modsi* moddb)))))
  (equal (elab-mod$a->inst-wireoffset
              instidx
              (nth modidx (nth *moddb->modsi* moddb)))
         (moddb-mod-inst-wireoffset instidx modidx moddb))))

Theorem: moddb-modinst-ok-of-moddb-norm-moddb

(defthm moddb-modinst-ok-of-moddb-norm-moddb
  (equal (moddb-modinst-ok idx modidx (moddb-norm moddb))
         (moddb-modinst-ok idx modidx moddb)))

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

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