Relax size constraints of VPSxLV instructions

These instructions are available for vector elements of size 16-bit.
jasmin-lang · Jul 17, 2023 · 09de289 · 09de289
1 parent ea2ea7d
commit 09de289
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -27,7 +27,7 @@
 
 ## Bug fixes
 
-- Fix semantics of the `SHLD_16` and `SHRD_16` instructions
+- Fix semantics of the `SHLD_16`, `SHRD_16`, `VPSLLV`, and `VPSRLV` instructions
   ([PR #520](https://github.com/jasmin-lang/jasmin/pull/520)).
 
 - Handle the size parameter in LZCNT semantic

diff --git a/proofs/compiler/x86_instr_decl.v b/proofs/compiler/x86_instr_decl.v
@@ -813,7 +813,7 @@ Definition x86_VPSRA (ve: velem) sz := x86_u128_shift ve sz (@wsar _).
 
 (* ---------------------------------------------------------------- *)
 Definition x86_u128_shift_variable ve sz op v1 v2 : ex_tpl (w_ty sz) :=
-  Let _ := check_size_32_64 ve in
+  Let _ := check_size_16_64 ve in
   Let _ := check_size_128_256 sz in
   ok (lift2_vec ve (λ v1 v2, op v1 (Z.min (wunsigned v2) (wsize_bits ve))) sz v1 v2).