		Search-engine friendly clone of the ACL2 documentation.

Poseidon-ingonyama-bls-255

Ingonyama-bls-255--parameters

Poseidon parameters for Ingonyama BLS-255 rate 4 implementation.

Signature
(ingonyama-bls-255--parameters) → param
Returns: param — Type (paramp param).

Definitions and Theorems

Function: ingonyama-bls-255--parameters

(defun ingonyama-bls-255--parameters nil
  (declare (xargs :guard t))
  (let ((__function__ 'ingonyama-bls-255--parameters))
    (declare (ignorable __function__))
    (make-param :prime primes::*bls12-381-scalar-field-prime*
                :rate 4
                :capacity 1
                :alpha 5
                :full-rounds-half 4
                :partial-rounds 60
                :constants *ingonyama-bls-255-ark*
                :mds *ingonyama-bls-255-mds*
                :rate-then-capacity-p nil
                :ascending-p t
                :partial-first-p t)))

Theorem: paramp-of-ingonyama-bls-255--parameters

(defthm paramp-of-ingonyama-bls-255--parameters
  (b* ((param (ingonyama-bls-255--parameters)))
    (paramp param))
  :rule-classes :rewrite)