		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Moddb-mod-inst-wireoffset

Signature
(moddb-mod-inst-wireoffset instidx modidx moddb) → offset
Arguments: instidx — Guard (natp instidx).; modidx — Guard (natp modidx).
Returns: offset — Type (natp offset).

Definitions and Theorems

Function: moddb-mod-inst-wireoffset

(defun moddb-mod-inst-wireoffset (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-mod-inst-wireoffset))
  (declare (ignorable __function__))
  (b*
   (((unless (mbt (< (lnfix modidx)
                     (lnfix (moddb->nmods moddb)))))
     0)
    (instidx
       (mbe :logic
            (min (nfix instidx)
                 (stobj-let ((elab-mod (moddb->modsi modidx moddb)))
                            (ninsts)
                            (elab-mod-ninsts elab-mod)
                            ninsts))
            :exec instidx))
    ((when (zp instidx))
     (b* (((stobj-get nwires)
           ((elab-mod (moddb->modsi modidx moddb)))
           (elab-mod-nwires elab-mod)))
       nwires))
    (prev-instidx (1- instidx))
    ((stobj-get prevoffset instmod)
     ((elab-mod (moddb->modsi modidx moddb)))
     (mv (elab-mod->inst-wireoffset prev-instidx elab-mod)
         (elab-mod->inst-modidx prev-instidx elab-mod)))
    ((unless (mbt (< instmod (lnfix modidx))))
     prevoffset)
    ((stobj-get inst-totalwires)
     ((elab-mod (moddb->modsi instmod moddb)))
     (elab-mod->totalwires elab-mod)))
   (+ prevoffset inst-totalwires))))

Theorem: natp-of-moddb-mod-inst-wireoffset

(defthm natp-of-moddb-mod-inst-wireoffset
  (b* ((offset (moddb-mod-inst-wireoffset instidx modidx moddb)))
    (natp offset))
  :rule-classes :type-prescription)

Theorem: moddb-mod-inst-wireoffset-of-nfix-instidx

(defthm moddb-mod-inst-wireoffset-of-nfix-instidx
  (equal (moddb-mod-inst-wireoffset (nfix instidx)
                                    modidx moddb)
         (moddb-mod-inst-wireoffset instidx modidx moddb)))

Theorem: moddb-mod-inst-wireoffset-nat-equiv-congruence-on-instidx

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

Theorem: moddb-mod-inst-wireoffset-of-nfix-modidx

(defthm moddb-mod-inst-wireoffset-of-nfix-modidx
  (equal (moddb-mod-inst-wireoffset instidx (nfix modidx)
                                    moddb)
         (moddb-mod-inst-wireoffset instidx modidx moddb)))

Theorem: moddb-mod-inst-wireoffset-nat-equiv-congruence-on-modidx

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

Theorem: moddb-mod-inst-wireoffset-of-moddb-fix-moddb

(defthm moddb-mod-inst-wireoffset-of-moddb-fix-moddb
 (equal (moddb-mod-inst-wireoffset instidx modidx (moddb-fix moddb))
        (moddb-mod-inst-wireoffset instidx modidx moddb)))

Theorem: moddb-mod-inst-wireoffset-moddb-equiv-congruence-on-moddb

(defthm moddb-mod-inst-wireoffset-moddb-equiv-congruence-on-moddb
 (implies
     (moddb-equiv moddb moddb-equiv)
     (equal (moddb-mod-inst-wireoffset instidx modidx moddb)
            (moddb-mod-inst-wireoffset instidx modidx moddb-equiv)))
 :rule-classes :congruence)

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

(defthm moddb-mod-inst-wireoffset-of-moddb-norm-moddb
  (equal (moddb-mod-inst-wireoffset idx modidx (moddb-norm moddb))
         (moddb-mod-inst-wireoffset idx modidx moddb)))

Theorem: moddb-mod-inst-wireoffset-moddb-norm-equiv-congruence-on-moddb

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