x86: Add missing sematest iclasses for ML-KEM compressions

Add simulator test patterns for VPSRLDQ, VPEXTRW, VPADDQ, VPACKUSWB,
VPBLENDVB, VPMADDUBSW, and VPMADDWD, covering both register and memory
operand variants.

Proposed by @jargh in awslabs#349

Signed-off-by: Matthias J. Kannwischer <matthias@kannwischer.eu>

Author: mkannwischer

x86/proofs/simulator.ml

@@ -833,6 +833,10 @@ let iclasses = iclasses_regreg @
  [0xf8]; (* CLC *)
  [0xfc]; (* CLD *)
  [0xfd]; (* STD *)
+ [0xc4; 0xc1; 0x39; 0x73; 0xd9; 0x7b]; (* VPSRLDQ (%_% xmm8) (%_% xmm9) (Imm8 (word 123)) *)
+ [0xc5; 0xf5; 0x73; 0xda; 0x63]; (* VPSRLDQ (%_% ymm1) (%_% ymm2) (Imm8 (word 99)) *)
+ [0xc4; 0xc1; 0x79; 0xc5; 0xcc; 0x64]; (* VPEXTRW (% ecx) (%_% xmm12) (Imm8 (word 100)) *)
+ [0xc5; 0x79; 0xc5; 0xfe; 0x52]; (* VPEXTRW (% r15d) (%_% xmm6) (Imm8 (word 82)) *)
 ];;
 
 (* ------------------------------------------------------------------------- *)
@@ -1487,6 +1491,19 @@ let simple_memory_iclasses = iclasses_simplemem @
   [0xc4; 0x61; 0x79; 0x17; 0x3c; 0x24];  (* vmovhpd [rsp], xmm15 *)
   [0xc5; 0xe9; 0xc4; 0x4c; 0x24; 0x07; 0x05]; (* vpinsrw xmm1, xmm2, [rsp + 0x7], 0x5 *)
   [0xc5; 0x79; 0xc4; 0x74; 0x24; 0x06; 0x0c]; (* vpinsrw xmm14, xmm0, [rsp + 0x6], 0xc *)
+  [0xc5; 0x99; 0xd4; 0x0c; 0x24]; (* VPADDQ (%_% xmm1) (%_% xmm12) (Memop Word128 (%% (rsp,0))) *)
+  [0xc5; 0x65; 0xd4; 0x44; 0x24; 0x20]; (* VPADDQ (%_% ymm8) (%_% ymm3) (Memop Word256 (%% (rsp,32))) *)
+  [0xc5; 0x0d; 0xd4; 0x74; 0x24; 0x40]; (* VPADDQ (%_% ymm14) (%_% ymm14) (Memop Word256 (%% (rsp,64))) *)
+  [0xc4; 0x63; 0x79; 0x15; 0x1c; 0x24; 0x01]; (* VPEXTRW (Memop Word (%% (rsp,0))) (%_% xmm11) (Imm8 (word 1)) *)
+  [0xc4; 0xe3; 0x79; 0x15; 0x54; 0x24; 0x20; 0xc2]; (* VPEXTRW (Memop Word (%% (rsp,32))) (%_% xmm2) (Imm8 (word 194)) *)
+  [0xc5; 0xb9; 0x67; 0x4c; 0x24; 0x40]; (* VPACKUSWB (%_% xmm1) (%_% xmm8) (Memop Word128 (%% (rsp,64))) *)
+  [0xc5; 0x35; 0x67; 0x0c; 0x24]; (* VPACKUSWB (%_% ymm9) (%_% ymm9) (Memop Word256 (%% (rsp,0))) *)
+  [0xc4; 0xe3; 0x51; 0x4c; 0x4c; 0x24; 0x20; 0x90]; (* VPBLENDVB (%_% xmm1) (%_% xmm5) (Memop Word128 (%% (rsp,32))) (%_% xmm9) *)
+  [0xc4; 0x63; 0x5d; 0x4c; 0x1c; 0x24; 0x90]; (* VPBLENDVB (%_% ymm11) (%_% ymm4) (Memop Word256 (%% (rsp,0))) (%_% ymm9) *)
+  [0xc4; 0xe2; 0x49; 0x04; 0xb4; 0x24; 0x80; 0x00; 0x00; 0x00]; (* VPMADDUBSW (%_% xmm6) (%_% xmm6) (Memop Word128 (%% (rsp,128))) *)
+  [0xc4; 0x62; 0x6d; 0x04; 0x24; 0x24]; (* VPMADDUBSW (%_% ymm12) (%_% ymm2) (Memop Word256 (%% (rsp,0))) *)
+  [0xc5; 0x39; 0xf5; 0x4c; 0x24; 0x20]; (* VPMADDWD (%_% xmm9) (%_% xmm8) (Memop Word128 (%% (rsp,32))) *)
+  [0xc5; 0x75; 0xf5; 0x34; 0x24]; (* VPMADDWD (%_% ymm14) (%_% ymm1) (Memop Word256 (%% (rsp,0))) *)
 ];;
 
 let simplemem_iclasses =