AVX2: Replace intrinsics implementation of `rej_uniform_eta` with assembly

[mkannwischer]

[jakemas]

I’ll do it next. I will attempt to add the HOL Light proof at the same time, it will help that I’ve got the x86 one now.

I’ll first do a round of review on the ASM, so that I don’t have to make significant changes to the proof if there are updates to the ASM. Once the code is stable, I’ll write the proofs.