		Search-engine friendly clone of the ACL2 documentation.

Param

Make-param

Basic constructor macro for param structures.

Syntax

(make-param [:prime <prime>] 
            [:rate <rate>] 
            [:capacity <capacity>] 
            [:alpha <alpha>] 
            [:full-rounds-half <full-rounds-half>] 
            [:partial-rounds <partial-rounds>] 
            [:constants <constants>] 
            [:mds <mds>] 
            [:rate-then-capacity-p <rate-then-capacity-p>] 
            [:ascending-p <ascending-p>] 
            [:partial-first-p <partial-first-p>])

This is the usual way to construct param structures. It simply conses together a structure with the specified fields.

This macro generates a new param structure from scratch. See also change-param, which can "change" an existing structure, instead.

Definition

This is an ordinary make- macro introduced by fty::defprod.

Macro: make-param

(defmacro make-param (&rest args)
  (std::make-aggregate 'param
                       args
                       '((:prime)
                         (:rate)
                         (:capacity)
                         (:alpha)
                         (:full-rounds-half)
                         (:partial-rounds)
                         (:constants)
                         (:mds)
                         (:rate-then-capacity-p)
                         (:ascending-p)
                         (:partial-first-p))
                       'make-param
                       nil))

Function: param

(defun param (prime rate capacity
                    alpha full-rounds-half partial-rounds
                    constants mds rate-then-capacity-p
                    ascending-p partial-first-p)
 (declare (xargs :guard (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))))
 (declare
    (xargs :guard (and (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)))))
 (let ((__function__ 'param))
  (declare (ignorable __function__))
  (b* ((prime (mbe :logic (prime-fix prime)
                   :exec prime))
       (rate (mbe :logic (acl2::pos-fix rate)
                  :exec rate))
       (capacity (mbe :logic (acl2::pos-fix capacity)
                      :exec capacity))
       (alpha (mbe :logic (ifix alpha) :exec alpha))
       (full-rounds-half (mbe :logic (nfix full-rounds-half)
                              :exec full-rounds-half))
       (partial-rounds (mbe :logic (nfix partial-rounds)
                            :exec partial-rounds))
       (rate-then-capacity-p
            (mbe :logic (acl2::bool-fix rate-then-capacity-p)
                 :exec rate-then-capacity-p))
       (ascending-p (mbe :logic (acl2::bool-fix ascending-p)
                         :exec ascending-p))
       (partial-first-p (mbe :logic (acl2::bool-fix partial-first-p)
                             :exec partial-first-p)))
   (let
    ((constants
         (mbe :logic
              (if (and (fe-list-listp constants prime)
                       (all-len-equal-p constants (+ rate capacity))
                       (equal (len constants)
                              (+ (* 2 full-rounds-half)
                                 partial-rounds)))
                  constants
                (repeat (+ (* 2 full-rounds-half)
                           partial-rounds)
                        (repeat (+ rate capacity) 0)))
              :exec constants))
     (mds (mbe :logic
               (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 mds)))
    (list (cons 'prime prime)
          (cons 'rate rate)
          (cons 'capacity capacity)
          (cons 'alpha alpha)
          (cons 'full-rounds-half
                full-rounds-half)
          (cons 'partial-rounds partial-rounds)
          (cons 'constants constants)
          (cons 'mds mds)
          (cons 'rate-then-capacity-p
                rate-then-capacity-p)
          (cons 'ascending-p ascending-p)
          (cons 'partial-first-p
                partial-first-p))))))