		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Modscope-push-frame

Push an instantiation onto a modscope, given by the instance index within the current module.

Signature
(modscope-push-frame instidx x moddb) → new-x
Arguments: instidx — Guard (natp instidx).; x — Guard (modscope-p x).; moddb — Guard (moddb-ok moddb).
Returns: new-x — Type (modscope-p new-x).

Definitions and Theorems

Function: modscope-push-frame

(defun modscope-push-frame (instidx x moddb)
 (declare (xargs :stobjs (moddb)))
 (declare (xargs :guard (and (natp instidx)
                             (modscope-p x)
                             (moddb-ok moddb))))
 (declare
  (xargs
       :guard (and (modscope-okp x moddb)
                   (< instidx
                      (b* ((modidx (modscope->modidx x))
                           ((stobj-get ninsts)
                            ((elab-mod (moddb->modsi modidx moddb)))
                            (elab-mod-ninsts elab-mod)))
                        ninsts)))))
 (let ((__function__ 'modscope-push-frame))
   (declare (ignorable __function__))
   (b* (((modscope x))
        ((stobj-get modidx wireoffset instoffset)
         ((elab-mod (moddb->modsi x.modidx moddb)))
         (mv (elab-mod->inst-modidx instidx elab-mod)
             (elab-mod->inst-wireoffset instidx elab-mod)
             (elab-mod->inst-instoffset instidx elab-mod))))
     (make-modscope-nested :modidx modidx
                           :wireoffset (+ wireoffset x.wireoffset)
                           :instoffset (+ instoffset x.instoffset)
                           :upper x))))

Theorem: modscope-p-of-modscope-push-frame

(defthm modscope-p-of-modscope-push-frame
  (b* ((new-x (modscope-push-frame instidx x moddb)))
    (modscope-p new-x))
  :rule-classes :rewrite)

Theorem: modscope-okp-of-modscope-push-frame

(defthm modscope-okp-of-modscope-push-frame
  (b* ((new-x (modscope-push-frame instidx x moddb)))
    (implies (and (modscope-okp x moddb)
                  (moddb-ok moddb)
                  (< (nfix instidx)
                     (b* ((modidx (modscope->modidx x))
                          ((stobj-get ninsts)
                           ((elab-mod (moddb->modsi modidx moddb)))
                           (elab-mod-ninsts elab-mod)))
                       ninsts)))
             (modscope-okp new-x moddb)))
  :rule-classes :rewrite)

Theorem: modidx-bound-of-modscope-push-frame

(defthm modidx-bound-of-modscope-push-frame
  (b* ((new-x (modscope-push-frame instidx x moddb)))
    (implies (and (modscope-okp x moddb)
                  (moddb-ok moddb)
                  (< (nfix instidx)
                     (b* ((modidx (modscope->modidx x))
                          ((stobj-get ninsts)
                           ((elab-mod (moddb->modsi modidx moddb)))
                           (elab-mod-ninsts elab-mod)))
                       ninsts)))
             (< (modscope->modidx new-x)
                (modscope->modidx x))))
  :rule-classes :rewrite)

Theorem: modscope-push-frame-of-nfix-instidx

(defthm modscope-push-frame-of-nfix-instidx
  (equal (modscope-push-frame (nfix instidx)
                              x moddb)
         (modscope-push-frame instidx x moddb)))

Theorem: modscope-push-frame-nat-equiv-congruence-on-instidx

(defthm modscope-push-frame-nat-equiv-congruence-on-instidx
  (implies (nat-equiv instidx instidx-equiv)
           (equal (modscope-push-frame instidx x moddb)
                  (modscope-push-frame instidx-equiv x moddb)))
  :rule-classes :congruence)

Theorem: modscope-push-frame-of-modscope-fix-x

(defthm modscope-push-frame-of-modscope-fix-x
  (equal (modscope-push-frame instidx (modscope-fix x)
                              moddb)
         (modscope-push-frame instidx x moddb)))

Theorem: modscope-push-frame-modscope-equiv-congruence-on-x

(defthm modscope-push-frame-modscope-equiv-congruence-on-x
  (implies (modscope-equiv x x-equiv)
           (equal (modscope-push-frame instidx x moddb)
                  (modscope-push-frame instidx x-equiv moddb)))
  :rule-classes :congruence)

Theorem: modscope-push-frame-of-moddb-fix-moddb

(defthm modscope-push-frame-of-moddb-fix-moddb
  (equal (modscope-push-frame instidx x (moddb-fix moddb))
         (modscope-push-frame instidx x moddb)))

Theorem: modscope-push-frame-moddb-equiv-congruence-on-moddb

(defthm modscope-push-frame-moddb-equiv-congruence-on-moddb
  (implies (moddb-equiv moddb moddb-equiv)
           (equal (modscope-push-frame instidx x moddb)
                  (modscope-push-frame instidx x moddb-equiv)))
  :rule-classes :congruence)