Properties only working on particular Z3 versions

[mccleeary-galois]

Summary

Currently some properties only work with the latest version of Z3 not what is shipped with what4-solvers

https://github.com/GaloisInc/what4-solvers/releases/tag/snapshot-20240212

This was found during review of https://github.com/GaloisInc/cryptol-specs/pull/161

Acceptance Criteria

Properties that do not :prove on Z3 4.8.14 have been identified and documented and changed to :check in the docstrings

Do

• [x] define acceptance criteria
• [x] add appropriate labels
• [ ] remember to update CHANGES
• [ ] remember to update docs appropriately
• [ ] identified properties that do not :prove on Z3 4.8.14
• [ ] Documented and updated properties to use :check with explanation that it is provable with more recent versions of Z3.

[marsella]

On master (at commit 774ec5b), using z3 4.8.14, I found that

• SHA3 Tests finish
• ML-KEM 512 KAT finishes
• ML-KEM 512 internal docstrings finish

On 144-compress

• Fast: roundingWorks; compressInvertsDecompress`{1, d_v}
• More than 30s : compressInvertsDecompress`{d_u}, decompressMostlyInvertsCompress -- these both work with exhaust instead.

On 144-encode

• All new properties finish within 30s

On 147-ntt

• :check-docstrings finishes. It's not particularly fast but it finishes.