Skip to content

Commit 2458351

Browse files
committed
fix bracket issue in bytecode
Signed-off-by: Jake Massimo <jakemas@amazon.com>
1 parent 19b7053 commit 2458351

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

proofs/hol_light/x86_64/proofs/mldsa_nttunpack.ml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@ needs "common/mlkem_mldsa.ml";;
1515

1616
let mldsa_nttunpack_mc = define_assert_from_elf "mldsa_nttunpack_mc" "x86_64/mldsa/mldsa_nttunpack.o"
1717
(*** BYTECODE START ***)
18-
[
18+
[
1919
0xf3; 0x0f; 0x1e; 0xfa; (* ENDBR64 *)
2020
0xc5; 0xfd; 0x6f; 0x27; (* VMOVDQA (%_% ymm4) (Memop Word256 (%% (rdi,0))) *)
2121
0xc5; 0xfd; 0x6f; 0x6f; 0x20;

0 commit comments

Comments
 (0)