		Search-engine friendly clone of the ACL2 documentation.

Poseidon-main-definition

Param-additional-theorems

Additional theorems about the parameters in param.

Definitions and Theorems

Theorem: posp-of-param->prime

(defthm posp-of-param->prime
  (posp (param->prime param)))

Theorem: all-len-equal-p-of-param->constants

(defthm all-len-equal-p-of-param->constants
  (all-len-equal-p (param->constants param)
                   (param->size param)))

Theorem: all-len-equal-p-of-param->mds

(defthm all-len-equal-p-of-param->mds
  (all-len-equal-p (param->mds param)
                   (param->size param)))

Theorem: len-of-param->constants

(defthm len-of-param->constants
  (equal (len (param->constants param))
         (param->rounds param)))

Theorem: len-of-param->mds

(defthm len-of-param->mds
  (equal (len (param->mds param))
         (param->size param)))

Theorem: param->rate-less-than-size

(defthm param->rate-less-than-size
  (< (param->rate param)
     (param->size param))
  :rule-classes :linear)

Theorem: param->capacity-less-than-size

(defthm param->capacity-less-than-size
  (< (param->capacity param)
     (param->size param))
  :rule-classes :linear)

Theorem: param->size-equal-rate+capacity

(defthm param->size-equal-rate+capacity
  (equal (param->size param)
         (+ (param->rate param)
            (param->capacity param)))
  :rule-classes :linear)