		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Elab-mod$c-wires-ok

Signature
(elab-mod$c-wires-ok elab-mod$c) → *

Definitions and Theorems

Function: elab-mod$c-wires-ok

(defun elab-mod$c-wires-ok (elab-mod$c)
  (declare (xargs :stobjs (elab-mod$c)))
  (declare (xargs :guard t))
  (let ((__function__ 'elab-mod$c-wires-ok))
    (declare (ignorable __function__))
    (and (<= (nfix (elab-mod$c->nwires elab-mod$c))
             (elab-mod$c->wiretable-length elab-mod$c))
         (ec-call (elab-mod$c-wire-indices-ok elab-mod$c))
         (ec-call (elab-mod$c-wire-names-ok elab-mod$c)))))

Theorem: elab-mod$c-wires-ok-when-empty

(defthm elab-mod$c-wires-ok-when-empty
  (implies (and (nat-equiv (nth *elab-mod$c->nwires* elab-mod$c)
                           0)
                (not (consp (nth *elab-mod$c->wirename-idxes-get*
                                 elab-mod$c))))
           (elab-mod$c-wires-ok elab-mod$c)))

Theorem: elab-mod$c-wires-ok-implies-lookup-name

(defthm elab-mod$c-wires-ok-implies-lookup-name
 (let
  ((look (hons-assoc-equal k
                           (nth *elab-mod$c->wirename-idxes-get*
                                elab-mod$c)))
   (idx
    (index-of
      k
      (wirelist->names (nth *elab-mod$c->wiretablei* elab-mod$c)))))
  (implies
       (elab-mod$c-wires-ok elab-mod$c)
       (equal look
              (and idx
                   (< idx
                      (nfix (nth *elab-mod$c->nwires* elab-mod$c)))
                   (cons k idx))))))

Theorem: elab-mod$c-indices-ok-in-terms-of-index-of

(defthm elab-mod$c-indices-ok-in-terms-of-index-of
 (implies
     (and (elab-mod$c-wires-ok elab-mod$c)
          (< (nfix idx)
             (nfix (nth *elab-mod$c->nwires* elab-mod$c))))
     (let ((idxes->wires (nth *elab-mod$c->wiretablei* elab-mod$c)))
       (equal (index-of (wire->name (nth idx idxes->wires))
                        (wirelist->names idxes->wires))
              (nfix idx)))))

Theorem: elab-mod$c-wires-ok-linear

(defthm elab-mod$c-wires-ok-linear
 (implies (elab-mod$c-wires-ok elab-mod$c)
          (and (<= (nfix (nth *elab-mod$c->nwires* elab-mod$c))
                   (len (nth *elab-mod$c->wiretablei* elab-mod$c)))
               (implies (natp (nth *elab-mod$c->nwires* elab-mod$c))
                        (<= (nth *elab-mod$c->nwires* elab-mod$c)
                            (len (nth *elab-mod$c->wiretablei*
                                      elab-mod$c))))))
 :rule-classes :linear)

Theorem: elab-mod$c-wires-ok-implies-no-duplicated-names

(defthm elab-mod$c-wires-ok-implies-no-duplicated-names
 (implies
  (and (elab-mod$c-wires-ok elab-mod$c)
       (< (nfix n)
          (nfix (nth *elab-mod$c->nwires* elab-mod$c)))
       (< (nfix m)
          (nfix (nth *elab-mod$c->nwires* elab-mod$c))))
  (equal
   (equal
       (wire->name (nth n
                        (nth *elab-mod$c->wiretablei* elab-mod$c)))
       (wire->name (nth m
                        (nth *elab-mod$c->wiretablei* elab-mod$c))))
   (nat-equiv n m))))