		Search-engine friendly clone of the ACL2 documentation.

Param

Paramp

Recognizer for param structures.

Signature
(paramp x) → *

Definitions and Theorems

Function: paramp

(defun paramp (x)
 (declare (xargs :guard t))
 (let ((__function__ 'paramp))
  (declare (ignorable __function__))
  (and
   (mbe
    :logic (and (alistp x)
                (equal (strip-cars x)
                       '(prime rate capacity
                               alpha full-rounds-half partial-rounds
                               constants mds rate-then-capacity-p
                               ascending-p partial-first-p)))
    :exec (fty::alist-with-carsp
               x
               '(prime rate capacity
                       alpha full-rounds-half partial-rounds
                       constants mds rate-then-capacity-p
                       ascending-p partial-first-p)))
   (b* ((prime (cdr (std::da-nth 0 x)))
        (rate (cdr (std::da-nth 1 x)))
        (capacity (cdr (std::da-nth 2 x)))
        (alpha (cdr (std::da-nth 3 x)))
        (full-rounds-half (cdr (std::da-nth 4 x)))
        (partial-rounds (cdr (std::da-nth 5 x)))
        (?constants (cdr (std::da-nth 6 x)))
        (?mds (cdr (std::da-nth 7 x)))
        (rate-then-capacity-p (cdr (std::da-nth 8 x)))
        (ascending-p (cdr (std::da-nth 9 x)))
        (partial-first-p (cdr (std::da-nth 10 x))))
     (and (primep prime)
          (posp rate)
          (posp capacity)
          (integerp alpha)
          (natp full-rounds-half)
          (natp partial-rounds)
          (booleanp rate-then-capacity-p)
          (booleanp ascending-p)
          (booleanp partial-first-p)
          (fe-list-listp constants prime)
          (all-len-equal-p constants (+ rate capacity))
          (equal (len constants)
                 (+ (* 2 full-rounds-half)
                    partial-rounds))
          (fe-list-listp mds prime)
          (all-len-equal-p mds (+ rate capacity))
          (equal (len mds) (+ rate capacity)))))))

Theorem: consp-when-paramp

(defthm consp-when-paramp
  (implies (paramp x) (consp x))
  :rule-classes :compound-recognizer)