		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Modscope->top

Given some modscope, pop all the way out to the top level.

Signature
(modscope->top x) → top
Arguments: x — Guard (modscope-p x).
Returns: top — Type (modscope-p top).

Definitions and Theorems

Function: modscope->top

(defun modscope->top (x)
  (declare (xargs :guard (modscope-p x)))
  (let ((__function__ 'modscope->top))
    (declare (ignorable __function__))
    (modscope-case x
                   :top (modscope-fix x)
                   :nested (modscope->top x.upper))))

Theorem: modscope-p-of-modscope->top

(defthm modscope-p-of-modscope->top
  (b* ((top (modscope->top x)))
    (modscope-p top))
  :rule-classes :rewrite)

Theorem: modscope-okp-of-modscope->top

(defthm modscope-okp-of-modscope->top
  (implies (modscope-okp x moddb)
           (modscope-okp (modscope->top x) moddb)))

Theorem: modscope-okp-wireoffset-lower-bound

(defthm modscope-okp-wireoffset-lower-bound
  (implies (modscope-okp x moddb)
           (<= (modscope->wireoffset (modscope->top x))
               (modscope->wireoffset x)))
  :rule-classes (:rewrite :linear))

Theorem: modscope-okp-wireidx-bound

(defthm modscope-okp-wireidx-bound
 (implies
      (and (modscope-okp x moddb)
           (moddb-ok moddb))
      (<= (+ (modscope->wireoffset x)
             (moddb-mod-totalwires (modscope->modidx x)
                                   moddb))
          (moddb-mod-totalwires (modscope->modidx (modscope->top x))
                                moddb)))
 :rule-classes (:rewrite :linear))

Theorem: modscope->offsets-of-modscope->top

(defthm modscope->offsets-of-modscope->top
  (and (equal (modscope->wireoffset (modscope->top x))
              0)
       (equal (modscope->instoffset (modscope->top x))
              0)))

Theorem: modscope->top-of-modscope-push-frame

(defthm modscope->top-of-modscope-push-frame
  (equal (modscope->top (modscope-push-frame idx scope moddb))
         (modscope->top scope)))

Theorem: modscope->top-of-modscope-fix-x

(defthm modscope->top-of-modscope-fix-x
  (equal (modscope->top (modscope-fix x))
         (modscope->top x)))

Theorem: modscope->top-modscope-equiv-congruence-on-x

(defthm modscope->top-modscope-equiv-congruence-on-x
  (implies (modscope-equiv x x-equiv)
           (equal (modscope->top x)
                  (modscope->top x-equiv)))
  :rule-classes :congruence)