		Search-engine friendly clone of the ACL2 documentation.

Poseidon-ingonyama-bls-255

Ingonyama-bls-255-hash

Hash no more than c + r inputs to a single field element output.

Signature
(ingonyama-bls-255-hash inputs) → output
Arguments: inputs — Guard (fe-listp inputs (param->prime (ingonyama-bls-255--parameters))).
Returns: output — Type (fep output (param->prime (ingonyama-bls-255--parameters))), given (and (fe-listp inputs (param->prime (ingonyama-bls-255--parameters))) (<= (len inputs) (param->size (ingonyama-bls-255--parameters)))) .

Definitions and Theorems

Function: ingonyama-bls-255-hash

(defun ingonyama-bls-255-hash (inputs)
 (declare
  (xargs :guard
         (fe-listp inputs
                   (param->prime (ingonyama-bls-255--parameters)))))
 (declare
  (xargs :guard (<= (len inputs)
                    (param->size (ingonyama-bls-255--parameters)))))
 (let ((__function__ 'ingonyama-bls-255-hash))
  (declare (ignorable __function__))
  (let
   ((preimage
       (append
            (repeat (- (param->size (ingonyama-bls-255--parameters))
                       (len inputs))
                    0)
            inputs)))
   (nth 1
        (hashp preimage (ingonyama-bls-255--parameters)
               2)))))

Theorem: fep-of-ingonyama-bls-255-hash

(defthm fep-of-ingonyama-bls-255-hash
 (implies
      (and (fe-listp inputs
                     (param->prime (ingonyama-bls-255--parameters)))
           (<= (len inputs)
               (param->size (ingonyama-bls-255--parameters))))
      (b* ((output (ingonyama-bls-255-hash inputs)))
        (fep output
             (param->prime (ingonyama-bls-255--parameters)))))
 :rule-classes :rewrite)