The AVX2 backend is directly pulled in from the pqcrystals repository.
We should add documenting comments along the lines of what was done in mlkem-native, in particular regarding coefficient bounds.
This can later help with writing a contract for the native functions and proving them in HOL-Light.