HOL-Light/x86: Improve clarity of basemul spec

[hanno-becker]

The spec for the AVX2 base multiplication is rather inaccessible:

mlkem-native/proofs/hol_light/x86/proofs/mlkem_poly_basemul_acc_montgomery_cached_k2.ml

Line 862 in d399bd3

==> ensures x86

We should try to write this in a way that abstracts away the specifics of the NTT-domain permutation. Now that that permutation is explicit in the [inv]NTT and mulcache specs, that should not be too hard.

[hanno-becker]

cc @dkostic