Clean up uses of coerceSize

[mccleeary-galois]

Now that GaloisInc/cryptol#1713 has been merged, some use cases of coerceSize should be able to be removed from cryptol-specs, particularly in ML-KEM, e.g.

cryptol-specs/Primitive/Asymmetric/Cipher/ML-KEM/specification.cry

Line 198 in 049f57d

new_v = coerceSize (lower # upper)

[rod-chapman]

If we make this change now, are we happy that cryptol-specs will depend on a nightly build of Cryptol, rather than a formally tagged release? Put another way - should we create a release 3.2 of Cryptol before updating this repo?

[mccleeary-galois]

cryptol-specs current target is nightly at the moment,

cryptol-specs/.github/workflows/ci.yml

Line 13 in 049f57d

image: ghcr.io/galoisinc/cryptol:nightly

However, the CI overhaul in the roadmap plans to test cryptol-specs against nightly and a predetermined set of releases of cryptol.

I am okay with holding off on this ticket until the new CI is in place (we can start cutting tickets over here for that as well).

[rod-chapman]

OK... sounds good

[marsella]

Oops, I missed the discussion on this issue about waiting to fix. I have a branch that adds all the fixes, I'll just leave it as a draft PR until we're ready to stabilize CI and the version of cryptol with this fix in it. See #107.

[mccleeary-galois]

This will still be useful for testing nightly in the meantime. Thanks Marcella!

[mccleeary-galois]

Discussed this internally and we came to the conclusion of releasing a new Cryptol version and having cryptol-specs CI target nightly and the most recently released version of Cryptol as a starting point.