		Search-engine friendly clone of the ACL2 documentation.

Poseidon-rate-4-alpha-17

Rate-4-domain-fe

Domain separation field element for Aleo circuit rate 4 Poseidon hash.

Signature
(rate-4-domain-fe) → *

Definitions and Theorems

Function: rate-4-domain-fe

(defun rate-4-domain-fe nil
  (declare (xargs :guard t))
  (let ((__function__ 'rate-4-domain-fe))
    (declare (ignorable __function__))
    (acl2::lendian=>nat
         256
         (acl2::chars=>nats (acl2::explode "Poseidon4")))))