		Search-engine friendly clone of the ACL2 documentation.

Poseidon-main-definition

Param->rounds

Total number of rounds, i.e. 2 R_f + R_P = R_F + R_P.

Signature
(param->rounds param) → rounds
Arguments: param — Guard (paramp param).
Returns: rounds — Type (natp rounds).

Definitions and Theorems

Function: param->rounds

(defun param->rounds (param)
  (declare (xargs :guard (paramp param)))
  (let ((__function__ 'param->rounds))
    (declare (ignorable __function__))
    (+ (param->full-rounds-half param)
       (param->partial-rounds param)
       (param->full-rounds-half param))))

Theorem: natp-of-param->rounds

(defthm natp-of-param->rounds
  (b* ((rounds (param->rounds param)))
    (natp rounds))
  :rule-classes :rewrite)

Theorem: param->rounds-of-param-fix-param

(defthm param->rounds-of-param-fix-param
  (equal (param->rounds (param-fix param))
         (param->rounds param)))

Theorem: param->rounds-param-equiv-congruence-on-param

(defthm param->rounds-param-equiv-congruence-on-param
  (implies (param-equiv param param-equiv)
           (equal (param->rounds param)
                  (param->rounds param-equiv)))
  :rule-classes :congruence)