		Search-engine friendly clone of the ACL2 documentation.

Param

Param->mds

Get the mds field from a param.

Signature
(param->mds x) → fty::x.name
Arguments: x — Guard (paramp x).

This is an ordinary field accessor created by fty::defprod.

Definitions and Theorems

Function: param->mds$inline

(defun param->mds$inline (x)
 (declare (xargs :guard (paramp x)))
 (declare (xargs :guard t))
 (let ((__function__ 'param->mds))
  (declare (ignorable __function__))
  (mbe
   :logic
   (b*
    ((x (and t x))
     (prime (prime-fix (cdr (std::da-nth 0 x))))
     (rate (acl2::pos-fix (cdr (std::da-nth 1 x))))
     (capacity (acl2::pos-fix (cdr (std::da-nth 2 x))))
     (alpha (ifix (cdr (std::da-nth 3 x))))
     (full-rounds-half (nfix (cdr (std::da-nth 4 x))))
     (partial-rounds (nfix (cdr (std::da-nth 5 x))))
     (constants (cdr (std::da-nth 6 x)))
     (mds (cdr (std::da-nth 7 x)))
     (rate-then-capacity-p (acl2::bool-fix (cdr (std::da-nth 8 x))))
     (ascending-p (acl2::bool-fix (cdr (std::da-nth 9 x))))
     (partial-first-p (acl2::bool-fix (cdr (std::da-nth 10 x)))))
    (if (and (fe-list-listp mds prime)
             (all-len-equal-p mds (+ rate capacity))
             (equal (len mds) (+ rate capacity)))
        mds
      (repeat (+ rate capacity)
              (repeat (+ rate capacity) 0))))
   :exec (cdr (std::da-nth 7 x)))))

Theorem: param->mds$inline-of-param-fix-x

(defthm param->mds$inline-of-param-fix-x
  (equal (param->mds$inline (param-fix x))
         (param->mds$inline x)))

Theorem: param->mds$inline-param-equiv-congruence-on-x

(defthm param->mds$inline-param-equiv-congruence-on-x
  (implies (param-equiv x x-equiv)
           (equal (param->mds$inline x)
                  (param->mds$inline x-equiv)))
  :rule-classes :congruence)