		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Svar->absindexed

Signature
(svar->absindexed x scope moddb) → (mv ok xx)
Arguments: x — Guard (svar-p x).; scope — Guard (modscope-p scope).; moddb — Guard (moddb-ok moddb).
Returns: xx — Type (svar-p xx).

Definitions and Theorems

Function: svar->absindexed

(defun svar->absindexed (x scope moddb)
 (declare (xargs :stobjs (moddb)))
 (declare (xargs :guard (and (svar-p x)
                             (modscope-p scope)
                             (moddb-ok moddb))))
 (declare
  (xargs
     :guard
     (and (modscope-okp scope moddb)
          (svar-idxaddr-okp x (modscope-local-bound scope moddb)))))
 (let ((__function__ 'svar->absindexed))
   (declare (ignorable __function__))
   (b* ((i (svar->address x))
        ((address i))
        (index (if i.index (+ (modscope->wireoffset scope) i.index)
                 (moddb-address->wireidx i scope moddb)))
        ((unless index) (mv nil (svar-fix x))))
     (mv t (svar-set-index x index)))))

Theorem: svar-p-of-svar->absindexed.xx

(defthm svar-p-of-svar->absindexed.xx
  (b* (((mv vl::?ok ?xx)
        (svar->absindexed x scope moddb)))
    (svar-p xx))
  :rule-classes :rewrite)

Theorem: svar->absindexed-of-svar-fix-x

(defthm svar->absindexed-of-svar-fix-x
  (equal (svar->absindexed (svar-fix x)
                           scope moddb)
         (svar->absindexed x scope moddb)))

Theorem: svar->absindexed-svar-equiv-congruence-on-x

(defthm svar->absindexed-svar-equiv-congruence-on-x
  (implies (svar-equiv x x-equiv)
           (equal (svar->absindexed x scope moddb)
                  (svar->absindexed x-equiv scope moddb)))
  :rule-classes :congruence)

Theorem: svar->absindexed-of-modscope-fix-scope

(defthm svar->absindexed-of-modscope-fix-scope
  (equal (svar->absindexed x (modscope-fix scope)
                           moddb)
         (svar->absindexed x scope moddb)))

Theorem: svar->absindexed-modscope-equiv-congruence-on-scope

(defthm svar->absindexed-modscope-equiv-congruence-on-scope
  (implies (modscope-equiv scope scope-equiv)
           (equal (svar->absindexed x scope moddb)
                  (svar->absindexed x scope-equiv moddb)))
  :rule-classes :congruence)

Theorem: svar->absindexed-of-moddb-fix-moddb

(defthm svar->absindexed-of-moddb-fix-moddb
  (equal (svar->absindexed x scope (moddb-fix moddb))
         (svar->absindexed x scope moddb)))

Theorem: svar->absindexed-moddb-equiv-congruence-on-moddb

(defthm svar->absindexed-moddb-equiv-congruence-on-moddb
  (implies (moddb-equiv moddb moddb-equiv)
           (equal (svar->absindexed x scope moddb)
                  (svar->absindexed x scope moddb-equiv)))
  :rule-classes :congruence)

Theorem: svar-boundedp-of-svar->absindexed

(defthm svar-boundedp-of-svar->absindexed
 (b* (((mv ok var)
       (svar->absindexed x scope moddb)))
   (implies
        (and (svar-idxaddr-okp x (modscope-local-bound scope moddb))
             (modscope-okp scope moddb)
             (moddb-ok moddb)
             ok)
        (svar-boundedp var (modscope-top-bound scope moddb)))))