mldsa: add ntt-over-vectors overloading #191

Primitive/Asymmetric/Signature/ML_DSA/Specification.cry

@@ -120,6 +120,18 @@ property modPlusMinusWorks m = inRange && congruent where
     inRange = (lower_bound < m') && (m' <= (`α / 2))
     congruent = ((fromZ m) % `α) == (m' % `α)
 
+/**
+ * Apply `NTT` and `NTTInv` entry-wise over a vector of polynomials.
+ * [FIPS-204] Section 2.5.
+ *
+ * The spec overloads the names `NTT` and `NTTInv` for both the single
+ * application to a polynomial in `Rq` and the vector application to every
+ * entry in a vector. Since Cryptol does not support user-defined overloaded
+ * names, we define the following functions.
+ */
+NTT_Vec = map NTT
+NTTInv_Vec = map NTT
+
 /**
  * Wrapper function around SHAKE256, specifying the length `l` in bytes.
  * [FIPS-204] Section 3.7.