x86: Add VMOVMSKPS, VPMOVZXBD, VZEROUPPER instruction models

[jakemas]

Summary

Add semantic models for three x86 AVX instructions needed by mldsa-native's rej_uniform formal verification (pq-code-package/mldsa-native#1014):

• VMOVMSKPS: Extract sign bits (bit 31) from each 32-bit lane of a YMM register into a GPR. Used to build a comparison mask after VPSUBD rejection testing.
• VPMOVZXBD: Zero-extend bytes to dwords (8→32 bit). Used to expand table lookup indices from the VPERMD compaction table.
• VZEROUPPER: Clear upper 128 bits of all YMM registers. Modeled as a no-op (like ENDBR64) since the proof framework tracks YMM registers as full 256-bit values and the instruction only affects performance, not correctness.

Includes decoder entries, instruction type constructors, semantic definitions, simulator test cases, and execution dispatch.

Having some issues with the Sematest CI:

list-x86-insns.sh fix: The sematest script tools/list-x86-insns.sh generates
memory-operand test cases by disassembling all .S files, extracting instructions
with [...] operands, and replacing them with [rsp+32]. This breaks for rep movs
which has two implicit memory operands (es:[rdi], ds:[rsi]) — replacing [rdi] with
[rsp+32] produces an invalid instruction. This is a pre-existing issue (reproduces
on main) but only surfaces in CI due to runner/assembler version differences. Fixed
by filtering out movs from the memory instruction list, matching the existing
filters for rsp/rip/lea/push/pop/ret/call/j*.

[jakemas]

Note: It looks like we're pulling vzeroupper out of the code (CR comments), but we can keep it modeled here if we like, I was able to get the proof working using it.

[jargh]

Looks great to me except for one thing which it might be nice to make cleaner. The decoding of VMOVMSKPS accepts both XMM and YMM forms but the eventual instruction dispatch always treats the operand as OPERAND256. So for example we'd see a simulator failure in
[0xc5; 0xf8; 0x50; 0xc1] (* vmovmskps eax, xmm1 -- VEX.L=0, 128-bit form *)
It would be nice either to make the decoder return NONE in case L is false (an easy fix) or actually handle both cases in the dispatch (maybe a bit more work for no immediate application, since the core instruction semantics x86_VMOVMSKPS only handles the 256-bit case too).

[jargh]

Thanks, this all looks great and all tests are successful. One minor thing I'd be inclined to add is some simple memory tests in the simulator's simple_memory_iclasses list for the vpmovzxbd instruction. I added the following and they all worked fine with a further make sematest run, which was a nice additional sanity check:

  [0xc4; 0xe2; 0x79; 0x31; 0x0c; 0x24];        (* vpmovzxbd xmm1,DWORD PTR [rsp] *)
  [0xc4; 0x62; 0x79; 0x31; 0x0c; 0x24];        (* vpmovzxbd xmm9,DWORD PTR [rsp] *)
  [0xc4; 0xe2; 0x7d; 0x31; 0x54; 0x24; 0x40];  (* vpmovzxbd ymm2,QWORD PTR [rsp+0x40] *)
  [0xc4; 0x62; 0x7d; 0x31; 0x7c; 0x24; 0x40];  (*  vpmovzxbd ymm15,QWORD PTR [rsp+0x40] *)

However I don't see this as a reason not to merge (since those did all work!) so I'll approve :-)