		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Elab-mod-wire-find-inst-aux

Signature
(elab-mod-wire-find-inst-aux wire mininst minoffset maxinst maxoffset smartp elab-mod) → inst
Arguments: wire — Guard (natp wire).; mininst — Guard (natp mininst).; minoffset — Guard (natp minoffset).; maxinst — Guard (natp maxinst).; maxoffset — Guard (natp maxoffset).; smartp — Try a smart guess for the pivot, versus a dumb binary split.; elab-mod — Guard (elab-mod-of-good-moddb elab-mod).
Returns: inst — Type (natp inst).

Definitions and Theorems

Function: elab-mod-wire-find-inst-aux

(defun elab-mod-wire-find-inst-aux
       (wire mininst minoffset
             maxinst maxoffset smartp elab-mod)
 (declare (xargs :stobjs (elab-mod)))
 (declare (xargs :guard (and (natp wire)
                             (natp mininst)
                             (natp minoffset)
                             (natp maxinst)
                             (natp maxoffset)
                             (elab-mod-of-good-moddb elab-mod))))
 (declare
  (xargs
    :guard (and (< mininst maxinst)
                (<= maxinst (elab-mod-ninsts elab-mod))
                (equal minoffset
                       (elab-mod->inst-wireoffset mininst elab-mod))
                (<= minoffset wire)
                (equal maxoffset
                       (elab-mod-wireoffset maxinst elab-mod))
                (< wire maxoffset))))
 (let ((__function__ 'elab-mod-wire-find-inst-aux))
  (declare (ignorable __function__))
  (b*
   ((maxinst (lnfix maxinst))
    (mininst (lnfix mininst))
    (wire (lnfix wire))
    (maxoffset (mbe :logic (elab-mod-wireoffset maxinst elab-mod)
                    :exec maxoffset))
    (minoffset
         (mbe :logic (elab-mod->inst-wireoffset mininst elab-mod)
              :exec minoffset))
    ((when (<= maxinst (+ 1 mininst)))
     mininst)
    (pivot
     (elab-mod-wiresearch-pivot wire mininst
                                minoffset maxinst maxoffset smartp))
    (pivotoffset (elab-mod->inst-wireoffset pivot elab-mod))
    (smartp-next (elab-mod-wiresearch-next-smartp
                      wire pivotoffset
                      mininst maxinst smartp elab-mod)))
   (if (< wire pivotoffset)
       (elab-mod-wire-find-inst-aux
            wire mininst minoffset
            pivot pivotoffset smartp-next elab-mod)
    (elab-mod-wire-find-inst-aux wire pivot pivotoffset maxinst
                                 maxoffset smartp-next elab-mod)))))

Theorem: natp-of-elab-mod-wire-find-inst-aux

(defthm natp-of-elab-mod-wire-find-inst-aux
  (b* ((inst (elab-mod-wire-find-inst-aux
                  wire mininst minoffset
                  maxinst maxoffset smartp elab-mod)))
    (natp inst))
  :rule-classes :type-prescription)

Theorem: elab-mod-wire-find-inst-aux-norm

(defthm elab-mod-wire-find-inst-aux-norm
 (implies
  (syntaxp (not (and (equal minoffset ''0)
                     (equal maxoffset ''0))))
  (equal
     (elab-mod-wire-find-inst-aux wire mininst minoffset
                                  maxinst maxoffset smartp elab-mod)
     (elab-mod-wire-find-inst-aux
          wire
          mininst 0 maxinst 0 smartp elab-mod))))

Theorem: elab-mod-wire-find-inst-aux-upper-bound

(defthm elab-mod-wire-find-inst-aux-upper-bound
 (implies
  (< (nfix mininst) (nfix maxinst))
  (< (elab-mod-wire-find-inst-aux wire mininst minoffset
                                  maxinst maxoffset smartp elab-mod)
     (nfix maxinst)))
 :rule-classes :linear)

Theorem: elab-mod-wire-find-inst-aux-lower-bound

(defthm elab-mod-wire-find-inst-aux-lower-bound
 (implies
  (< (nfix mininst) (nfix maxinst))
  (<=
   (nfix mininst)
   (elab-mod-wire-find-inst-aux wire mininst minoffset
                                maxinst maxoffset smartp elab-mod)))
 :rule-classes :linear)

Theorem: elab-mod-wire-find-inst-aux-correct1

(defthm elab-mod-wire-find-inst-aux-correct1
 (implies
  (and (< (nfix mininst) (nfix maxinst))
       (<= (elab-mod->inst-wireoffset mininst elab-mod)
           (nfix wire))
       (< (nfix wire)
          (elab-mod-wireoffset maxinst elab-mod))
       (<= (nfix maxinst)
           (elab-mod$a-ninsts elab-mod))
       (elab-mod-of-good-moddb elab-mod))
  (<=
   (elab-mod-wireoffset
     (elab-mod-wire-find-inst-aux wire mininst minoffset
                                  maxinst maxoffset smartp elab-mod)
     elab-mod)
   (nfix wire)))
 :rule-classes :linear)

Theorem: elab-mod-wire-find-inst-aux-correct2

(defthm elab-mod-wire-find-inst-aux-correct2
 (implies
  (and (< (nfix mininst) (nfix maxinst))
       (<= (elab-mod->inst-wireoffset mininst elab-mod)
           (nfix wire))
       (< (nfix wire)
          (elab-mod-wireoffset maxinst elab-mod))
       (<= (nfix maxinst)
           (elab-mod$a-ninsts elab-mod))
       (elab-mod-of-good-moddb elab-mod))
  (<
    (nfix wire)
    (elab-mod-wireoffset (+ 1
                            (elab-mod-wire-find-inst-aux
                                 wire mininst minoffset
                                 maxinst maxoffset smartp elab-mod))
                         elab-mod)))
 :rule-classes :linear)