Comments on new ntt

This is great work @rod-chapman!

My main suggestion is to add documentation. Cryptol supports doc-strings - every definition should have one that describes the intent of the function along w/ citations to appropriate reference documents. For example:

https://github.com/awslabs/LibMLKEM/blob/6d192dda3e933632abf8250dbbea5c7e1c3a9ccf/spark_ada/experimental/ntt.cry#L23-L24
What is `BitRev7`? Why `7` when the input and outputs are both `8` bits? On the face it looks like there could be a typo. If the function was documented and a reference provided, understanding could be given rather than inferred/reverse engineered.

Otherwise, some nit-picky things --

Cryptol has a robust (@WeekNightMVP 😄) module system. The first line should be something like

```
module LibMLKEM::spark_ada::experimental::ntt where
```
Or where ever you want it to live - could be as simple as:
```
module ntt where
```
But it should have one!

I suggest being consistent with names and extensions thereof. For example,

https://github.com/awslabs/LibMLKEM/blob/6d192dda3e933632abf8250dbbea5c7e1c3a9ccf/spark_ada/experimental/ntt.cry#L8-L9

I suggest either
```
type Z_q = (Z MLKEM_Q)
type Z_q_256 = [MLKEM_N]Z_q
```

or
```
type Zq = (Z MLKEM_Q)
type Zq_256 = [MLKEM_N]Zq
```

Both camelCase and snake_case are being used. I suggest you pick one. It's ideally best to follow the naming convention in whatever document you are following to create a specification. That way developers will have an easier time using the Cryptol spec along w/ other reference documentation to assist their development work.

Cryptol will soon have the ability to check properties in doc-strings (a la `cargo test`) -- https://github.com/GaloisInc/cryptol/pull/1682
So, properties like the following:
https://github.com/awslabs/LibMLKEM/blob/6d192dda3e933632abf8250dbbea5c7e1c3a9ccf/spark_ada/experimental/ntt.cry#L44-L49
could be better supported like so:

```
/**
* This property demonstrates that `naive_ntt` is the inverse of `naive_invntt`.
* ```
* :prove naive_ntt_inverts
* ```
*/
naive_ntt_inverts : Z_q_256 -> Bool
property naive_ntt_inverts f = f == naive_invntt (naive_ntt f)
```

It's also suggested to write properties (when possible) in the style of a rewrite rule. This assists with any future effort where `saw` would use such a property as a lemma to prove a larger property.

There are unnecessary (and distracting) parens in places. Here is an example:
https://github.com/awslabs/LibMLKEM/blob/6d192dda3e933632abf8250dbbea5c7e1c3a9ccf/spark_ada/experimental/ntt.cry#L92
This could instead be:
```
new_v = [ v@x + zeta * v@(x + len) | x <- [ 0 .. < 2^^q ] ]
```

Suggest removing miscellaneous newlines, for example:
https://github.com/awslabs/LibMLKEM/blob/6d192dda3e933632abf8250dbbea5c7e1c3a9ccf/spark_ada/experimental/ntt.cry#L180-L181

Suggest exploring Cryptol's `generate` syntactic sugar (https://github.com/GaloisInc/cryptol/blob/f5fa503b1898e8bb9dc3358ada036adb4c54b832/docs/RefMan/BasicTypes.rst?plain=1#L161-L163) to simplify some expressions. For example:

https://github.com/awslabs/LibMLKEM/blob/6d192dda3e933632abf8250dbbea5c7e1c3a9ccf/spark_ada/experimental/ntt.cry#L27-L30 Could become:

```
ParametricNTT' : Z_q_256 -> Zq -> Z_q_256
ParametricNTT' f root = join (transpose [map sum f2, map sum f2Plus1])
where
f2, f2Plus1 : [128][128]Zq
f2@i@j = f@(2*j) * root ^^ ((2*(BitRev7 i >> 1)+1)*j)
f2Plus1@i@j = f@(2*j+1) * root ^^ ((2*(BitRev7 i >> 1)+1)*j)
```

```
> :prove \f root -> ParametricNTT' f root == ParametricNTT f root
Q.E.D.
(Total Elapsed Time: 13.740s, using "Z3")
```
How cool is that!

It might be worthwhile to add a comment saying that `coerceSize` is necessary here until the issues related to https://github.com/GaloisInc/cryptol/pull/1392 are addressed. That way, someone may be able to remove this blight at a later date.

Start with spark_ada/experimental/ntt.cry, especially the module declaration, type definitions, properties, generate examples, and the coerceSize use referenced in the issue. Review the linked Cryptol documentation and pull requests before changing anything. Done means the requested documentation, naming, formatting, and property guidance has been addressed consistently in ntt.cry.

Written by the indexing model from the issue text.