HOL-Light: Unify specification-style for arithmetic arrays

[hanno-becker]

In the mlkem-native and mldsa-native we use a mixture of explicitly quantified pre/post conditions !i. i < 256 ==> word ( ... ) = f i vs. wrapped wordlist_from_memory.

Task:

• Audit how memory pre/post-conditions are specified across mlkem-native and mldsa-native
• Check how to move between the two
• Assuming there is no technical reason for the divergence: Agree and implement a uniform style for array pre/post conditions