Merge branch 'main' into add-avx2-vpsllq

jakemas · web-flow · commit e802c1519c80 · 2025-07-24T11:29:35.000-07:00
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -4,9 +4,16 @@ on:
   pull_request:
     branches: [ main ]
 
+env:
+  HOLLIGHT_COMMIT: "157c99b7bb3a485116dc2bfc4ef3ad00912d883b"
+
 jobs:
-  s2n-bignum-arm-tests:
-    runs-on: ubuntu-24.04-arm
+  s2n-bignum-tests:
+    strategy:
+      matrix:
+        arch: [arm, x86]
+
+    runs-on: ${{ matrix.arch == 'arm' && 'ubuntu-24.04-arm' || matrix.arch == 'x86' && 'ubuntu-24.04' }}
 
     steps:
     - name: Checkout code
@@ -19,28 +26,131 @@ jobs:
 
     - name: Run tests
       run: |
-        cd arm
+        cd ${{ matrix.arch }}
         make
+        ${{ matrix.arch == 'x86' && 'cd ../x86_att && make clobber && make && git diff --exit-code .' || true}}
+        echo "Make test"
         cd ../tests
-        make complete
+        CC=gcc make complete
         make ctCheck
+        echo "Make test with valgrind"
+        make clean
+        CC=gcc VALGRIND="valgrind --" make complete || echo "(incomplete test, but proceeding)"
+        echo "Make test (clang, build only)"
+        make clean
+        CC=clang make
+        echo "Make benchmark (build only, for both of those)"
         cd ../benchmarks
-        make
+        CC=gcc make
+        make clean
+        CC=clang make
 
-  s2n-bignum-x86-tests:
-    runs-on: ubuntu-24.04
+  s2n-bignum-aws-lc-integration:
+    strategy:
+      matrix:
+        arch: [arm, x86]
+
+    runs-on: ${{ matrix.arch == 'arm' && 'ubuntu-24.04-arm' || matrix.arch == 'x86' && 'ubuntu-24.04' }}
 
     steps:
     - name: Checkout code
       uses: actions/checkout@v4
 
+    - name: Install dependent packages
+      run: |
+        sudo apt update
+        sudo apt install valgrind cmake golang ninja-build
+        which ninja
+        sudo ln -s /usr/bin/ninja /usr/bin/ninja-build
+        which cmake
+        ln -s /usr/local/bin/cmake /usr/local/bin/cmake3
+
     - name: Run tests
       run: |
-        cd x86
-        make
-        cd ../x86_att && make clobber && make && git diff --exit-code .
-        cd ../tests
-        make complete
-        make ctCheck
-        cd ../benchmarks
-        make
+        echo "Run AWS-LC integration test (GITHUB_REPOSITORY: ${{ github.event.pull_request.head.repo.full_name }}, GITHUB_TARGET: $GITHUB_HEAD_REF)"
+        git clone https://github.com/aws/aws-lc.git --depth=1
+        cd aws-lc/third_party/s2n-bignum
+        rm -rf ./s2n-bignum-imported
+        GITHUB_REPOSITORY=${{ github.event.pull_request.head.repo.full_name }}.git GITHUB_TARGET=$GITHUB_HEAD_REF ./import.sh
+        cd ../../../
+        mkdir aws-lc-build && cd aws-lc-build
+        cmake3 -GNinja -DCMAKE_BUILD_TYPE=RelWithDebInfo -DFIPS=On ../aws-lc
+        ninja-build run_tests
+        cmake3 -GNinja -DCMAKE_BUILD_TYPE=RelWithDebInfo -DFIPS=Off ../aws-lc
+        ninja-build run_tests
+
+  s2n-bignum-sematest:
+    strategy:
+      matrix:
+        arch: [arm, x86]
+
+    runs-on: ${{ matrix.arch == 'arm' && 'ubuntu-24.04-arm' || matrix.arch == 'x86' && 'ubuntu-24.04' }}
+
+    steps:
+    - name: Checkout code
+      uses: actions/checkout@v4
+
+    - name: Install dependent packages
+      run: |
+        sudo apt update
+        sudo apt install libpcre2-dev ocaml libstring-shellquote-perl libgmp-dev xdot
+        wget https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh
+        chmod +x install.sh
+        echo "/usr/local/bin" | sh ./install.sh
+        opam init --disable-sandboxing
+
+    - name: Install HOL Light
+      run: |
+        git clone https://github.com/jrh13/hol-light.git
+        cd hol-light
+        git checkout ${{ env.HOLLIGHT_COMMIT }}
+        make switch-5
+        eval $(opam env)
+        echo $(ocamlc -version)
+        echo $(camlp5 -v)
+        HOLLIGHT_USE_MODULE=1 make
+        cd ..
+
+    - name: Run tests
+      run: |
+        export HOLDIR=`pwd`/hol-light
+        cd ${{ matrix.arch }}
+        make sematest
+
+  s2n-bignum-tutorial:
+    strategy:
+      matrix:
+        arch: [arm, x86]
+
+    runs-on: ${{ matrix.arch == 'arm' && 'ubuntu-24.04-arm' || matrix.arch == 'x86' && 'ubuntu-24.04' }}
+
+    steps:
+    - name: Checkout code
+      uses: actions/checkout@v4
+
+    - name: Install dependent packages
+      run: |
+        sudo apt update
+        sudo apt install libpcre2-dev ocaml libstring-shellquote-perl libgmp-dev xdot
+        wget https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh
+        chmod +x install.sh
+        echo "/usr/local/bin" | sh ./install.sh
+        opam init --disable-sandboxing
+
+    - name: Install HOL Light
+      run: |
+        git clone https://github.com/jrh13/hol-light.git
+        cd hol-light
+        git checkout ${{ env.HOLLIGHT_COMMIT }}
+        make switch-5
+        eval $(opam env)
+        echo $(ocamlc -version)
+        echo $(camlp5 -v)
+        HOLLIGHT_USE_MODULE=1 make
+        cd ..
+
+    - name: Run tutorial
+      run: |
+        export HOLDIR=`pwd`/hol-light
+        cd ${{ matrix.arch }}
+        make tutorial
diff --git a/benchmarks/Makefile b/benchmarks/Makefile
@@ -28,7 +28,7 @@ endif
 
 # Benchmarking progfram
 
-benchmark: benchmark.c ../include/s2n-bignum.h ../$(ARCH)/libs2nbignum.a; gcc -O3 -o benchmark benchmark.c -L../$(ARCH) -ls2nbignum -lm
+benchmark: benchmark.c ../include/s2n-bignum.h ../$(ARCH)/libs2nbignum.a; $(CC) -O3 -o benchmark benchmark.c -L../$(ARCH) -ls2nbignum -lm
 
 go: benchmark ; ./benchmark
 
diff --git a/tests/Makefile b/tests/Makefile
@@ -11,14 +11,12 @@
 # setting: ARCH=x86 or ARCH=arm as appropriate
 
 ARCH=unknown_architecture
-VALGRIND=valgrind --
+VALGRIND?=
 
 UNAME_RESULT=$(shell uname -m)
 
 ifeq ($(UNAME_RESULT),x86_64)
 ARCH=x86
-# Enabling valgrind makes test unable to detect BMI/ADX
-VALGRIND=
 endif
 
 ifeq ($(UNAME_RESULT),aarch64)
@@ -47,7 +45,7 @@ go: test; ./test +100 | grep -v OK
 
 complete: test ctCheck; $(VALGRIND) ./test +500
 
-test: test.c known_value_tests_p384.h tweetnacl_excerpt.c ../include/s2n-bignum.h ../$(ARCH)/libs2nbignum.a; gcc -Wall -std=gnu99 -o test test.c -L../$(ARCH) -ls2nbignum
+test: test.c known_value_tests_p384.h tweetnacl_excerpt.c ../include/s2n-bignum.h ../$(ARCH)/libs2nbignum.a; $(CC) -Wall -std=gnu99 -o test test.c -L../$(ARCH) -ls2nbignum -lm
 
 clean: ;
 	rm -f test
diff --git a/x86/allowed_asm b/x86/allowed_asm
@@ -120,11 +120,13 @@
 : testq$
 : vpxor$
 : vpaddw$
+: vpaddd$
 : vpand$
 : vpmulhw$
 : vpmullw$
 : vpsllq$
 : vpsrad$
+: vpsubd$
 : vpsubw$
 : vpsraw$
 : vpsrlw$
diff --git a/x86/proofs/decode.ml b/x86/proofs/decode.ml
@@ -610,10 +610,18 @@ let decode_aux = new_definition `!pfxs rex l. decode_aux pfxs rex l =
           let sz = vexL_size L in
           (read_ModRM rex l >>= \((reg,rm),l).
             SOME (VPSUBW (mmreg reg sz) (mmreg v sz) (simd_of_RM sz rm),l))
+        | [0xfa:8] ->
+          let sz = vexL_size L in
+          (read_ModRM rex l >>= \((reg,rm),l).
+            SOME (VPSUBD (mmreg reg sz) (mmreg v sz) (simd_of_RM sz rm),l))
         | [0xfd:8] ->
           let sz = vexL_size L in
           (read_ModRM rex l >>= \((reg,rm),l).
             SOME (VPADDW (mmreg reg sz) (mmreg v sz) (simd_of_RM sz rm),l))
+        | [0xfe:8] ->
+          let sz = vexL_size L in
+          (read_ModRM rex l >>= \((reg,rm),l).
+            SOME (VPADDD (mmreg reg sz) (mmreg v sz) (simd_of_RM sz rm),l))
         | [0x71:8] ->
           let sz = vexL_size L in
           read_ModRM rex l >>= (\((reg,rm),l).
diff --git a/x86/proofs/instruction.ml b/x86/proofs/instruction.ml
@@ -305,13 +305,15 @@ let instruction_INDUCTION,instruction_RECURSION = define_type
    | TEST operand operand
    | TZCNT operand operand
    | VPADDW operand operand operand
+   | VPADDD operand operand operand
    | VPAND operand operand operand
    | VPMULHW operand operand operand
    | VPMULLW operand operand operand
    | VPSLLQ operand operand operand
    | VPSRAD operand operand operand
    | VPSRAW operand operand operand
    | VPSRLW operand operand operand
+   | VPSUBD operand operand operand
    | VPSUBW operand operand operand
    | VPXOR operand operand operand
    | XCHG operand operand
diff --git a/x86/proofs/simulator.ml b/x86/proofs/simulator.ml
@@ -292,6 +292,34 @@ let iclasses = iclasses @
  [0x66; 0x0f; 0x1f; 0x84; 0x00; 0x00; 0x00; 0x00; 0x00]; (* NOP_N (Memop Word (%%%% (rax,0,rax))) *)
  [0x66; 0x2e; 0x0f; 0x1f; 0x84; 0x00; 0x00; 0x00; 0x00; 0x00]; (* NOP_N (Memop Word (%%%% (rax,0,rax))) *)
  [0x66; 0x66; 0x2e; 0x0f; 0x1f; 0x84; 0x00; 0x00; 0x00; 0x00; 0x00]; (* NOP_N (Memop Word (%%%% (rax,0,rax))) *)
+ [0xc5; 0xfd; 0xfe; 0xc1]; (* VPADDD ymm0, ymm0, ymm1 *)
+ [0xc5; 0xf5; 0xfe; 0xca]; (* VPADDD ymm1, ymm1, ymm2 *)
+ [0xc5; 0xed; 0xfe; 0xd3]; (* VPADDD ymm2, ymm2, ymm3 *)
+ [0xc5; 0xe5; 0xfe; 0xdc]; (* VPADDD ymm3, ymm3, ymm4 *)
+ [0xc5; 0xe9; 0xfe; 0xcb]; (* VPADDD (%_% xmm1) (%_% xmm2) (%_% xmm3) *)
+ [0xc5; 0xf9; 0xfe; 0xff]; (* VPADDD (%_% xmm7) (%_% xmm0) (%_% xmm7) *)
+ [0xc4; 0x41; 0x7d; 0xfe; 0xc1]; (* VPADDD ymm8, ymm8, ymm9 *)
+ [0xc4; 0x41; 0x6d; 0xfe; 0xd3]; (* VPADDD ymm10, ymm10, ymm11 *)
+ [0xc4; 0x41; 0x5d; 0xfe; 0xe5]; (* VPADDD ymm12, ymm12, ymm13 *)
+ [0xc4; 0x41; 0x4d; 0xfe; 0xf7]; (* VPADDD ymm14, ymm14, ymm15 *)
+ [0xc4; 0x41; 0x19; 0xfe; 0xdd]; (* VPADDD (%_% xmm11) (%_% xmm12) (%_% xmm13) *)
+ [0xc4; 0x41; 0x11; 0xfe; 0xfc]; (* VPADDD (%_% xmm15) (%_% xmm13) (%_% xmm12) *)
+ [0xc5; 0xfd; 0xfa; 0xc1]; (* VPSUBD ymm0, ymm0, ymm1 *)
+ [0xc5; 0xf5; 0xfa; 0xca]; (* VPSUBD ymm1, ymm1, ymm2 *)
+ [0xc5; 0xed; 0xfa; 0xd3]; (* VPSUBD ymm2, ymm2, ymm3 *)
+ [0xc5; 0xe5; 0xfa; 0xdc]; (* VPSUBD ymm3, ymm3, ymm4 *)
+ [0xc5; 0xf9; 0xfa; 0xc1]; (* VPSUBD xmm0, xmm0, xmm1 *)
+ [0xc5; 0xf1; 0xfa; 0xca]; (* VPSUBD xmm1, xmm1, xmm2 *)
+ [0xc5; 0xe9; 0xfa; 0xd3]; (* VPSUBD xmm2, xmm2, xmm3 *)
+ [0xc5; 0xe1; 0xfa; 0xdc]; (* VPSUBD xmm3, xmm3, xmm4 *)
+ [0xc4; 0x41; 0x7d; 0xfa; 0xc1]; (* VPSUBD ymm8, ymm8, ymm9 *)
+ [0xc4; 0x41; 0x6d; 0xfa; 0xd3]; (* VPSUBD ymm10, ymm10, ymm11 *)
+ [0xc4; 0x41; 0x5d; 0xfa; 0xe5]; (* VPSUBD ymm12, ymm12, ymm13 *)
+ [0xc4; 0x41; 0x4d; 0xfa; 0xf7]; (* VPSUBD ymm14, ymm14, ymm15 *)
+ [0xc4; 0x41; 0x39; 0xfa; 0xc1]; (* VPSUBD xmm8, xmm8, xmm9 *)
+ [0xc4; 0x41; 0x29; 0xfa; 0xd3]; (* VPSUBD xmm10, xmm10, xmm11 *)
+ [0xc4; 0x41; 0x19; 0xfa; 0xe5]; (* VPSUBD xmm12, xmm12, xmm13 *)
+ [0xc4; 0x41; 0x09; 0xfa; 0xf7]; (* VPSUBD xmm14, xmm14, xmm15 *)
  [0xc5; 0x81; 0xf9; 0xf6]; (* VPSUBW (%_% xmm6) (%_% xmm15) (%_% xmm6) *)
  [0xc5; 0x85; 0xf9; 0xf6]; (* VPSUBW (%_% ymm6) (%_% ymm15) (%_% ymm6) *)
  [0xc5; 0x45; 0xfd; 0xd9]; (* VPADDW (%_% ymm11) (%_% ymm7) (%_% ymm11) *)
diff --git a/x86/proofs/x86.ml b/x86/proofs/x86.ml
@@ -1311,6 +1311,17 @@ let x86_VPADDW = new_definition
         let res:(128)word = simd8 word_add (word_zx x) (word_zx y) in
         (dest := (word_zx res):N word) s`;;
 
+let x86_VPADDD = new_definition
+  `x86_VPADDD dest src1 src2 (s:x86state) =
+      let (x:N word) = read src1 s
+      and (y:N word) = read src2 s in
+      if dimindex(:N) = 256 then
+        let res:(256)word = simd8 word_add (word_zx x) (word_zx y) in
+        (dest := (word_zx res):N word) s
+      else
+        let res:(128)word = simd4 word_add (word_zx x) (word_zx y) in
+        (dest := (word_zx res):N word) s`;;
+
 let x86_VPMULHW = new_definition
   `x86_VPMULHW dest src1 src2 (s:x86state) =
       let (x:N word) = read src1 s
@@ -1345,6 +1356,17 @@ let x86_VPSLLQ = new_definition
         let res:(128)word = usimd2 (\z. word_shl z count) (word_zx x) in
         (dest := (word_zx res):N word) s`;;
 
+let x86_VPSUBD = new_definition
+  `x86_VPSUBD dest src1 src2 (s:x86state) =
+      let (x:N word) = read src1 s
+      and (y:N word) = read src2 s in
+      if dimindex(:N) = 256 then
+        let res:(256)word = simd8 word_sub (word_zx x) (word_zx y) in
+        (dest := (word_zx res):N word) s
+      else
+        let res:(128)word = simd4 word_sub (word_zx x) (word_zx y) in
+        (dest := (word_zx res):N word) s`;;
+
 let x86_VPSUBW = new_definition
   `x86_VPSUBW dest src1 src2 (s:x86state) =
       let (x:N word) = read src1 s
@@ -2073,6 +2095,10 @@ let x86_execute = define
         (match operand_size dest with
           256 -> x86_VPADDW (OPERAND256 dest s) (OPERAND256 src1 s) (OPERAND256 src2 s)
         | 128 -> x86_VPADDW (OPERAND128 dest s) (OPERAND128 src1 s) (OPERAND128 src2 s)) s
+    | VPADDD dest src1 src2 ->
+        (match operand_size dest with
+          256 -> x86_VPADDD (OPERAND256 dest s) (OPERAND256 src1 s) (OPERAND256 src2 s)
+        | 128 -> x86_VPADDD (OPERAND128 dest s) (OPERAND128 src1 s) (OPERAND128 src2 s)) s
     | VPMULHW dest src1 src2 ->
         (match operand_size dest with
           256 -> x86_VPMULHW (OPERAND256 dest s) (OPERAND256 src1 s) (OPERAND256 src2 s)
@@ -2085,6 +2111,10 @@ let x86_execute = define
         (match operand_size dest with
           256 -> x86_VPSLLQ (OPERAND256 dest s) (OPERAND256 src s) (OPERAND8 imm8 s)
         | 128 -> x86_VPSLLQ (OPERAND128 dest s) (OPERAND128 src s) (OPERAND8 imm8 s)) s
+    | VPSUBD dest src1 src2 ->
+        (match operand_size dest with
+          256 -> x86_VPSUBD (OPERAND256 dest s) (OPERAND256 src1 s) (OPERAND256 src2 s)
+        | 128 -> x86_VPSUBD (OPERAND128 dest s) (OPERAND128 src1 s) (OPERAND128 src2 s)) s
     | VPSUBW dest src1 src2 ->
         (match operand_size dest with
           256 -> x86_VPSUBW (OPERAND256 dest s) (OPERAND256 src1 s) (OPERAND256 src2 s)
@@ -2827,10 +2857,12 @@ let x86_PADDQ_ALT = EXPAND_SIMD_RULE x86_PADDQ;;
 let x86_PCMPGTD_ALT = EXPAND_SIMD_RULE x86_PCMPGTD;;
 let x86_PSHUFD_ALT = EXPAND_SIMD_RULE x86_PSHUFD;;
 let x86_PSRAD_ALT = EXPAND_SIMD_RULE x86_PSRAD;;
+let x86_VPADDD_ALT = EXPAND_SIMD_RULE x86_VPADDD;;
 let x86_VPADDW_ALT = EXPAND_SIMD_RULE x86_VPADDW;;
 let x86_VPMULHW_ALT = EXPAND_SIMD_RULE x86_VPMULHW;;
 let x86_VPMULLW_ALT = EXPAND_SIMD_RULE x86_VPMULLW;;
 let x86_VPSLLQ_ALT = EXPAND_SIMD_RULE x86_VPSLLQ;;
+let x86_VPSUBD_ALT = EXPAND_SIMD_RULE x86_VPSUBD;;
 let x86_VPSUBW_ALT = EXPAND_SIMD_RULE x86_VPSUBW;;
 let x86_VPSRAD_ALT = EXPAND_SIMD_RULE x86_VPSRAD;;
 let x86_VPSRAW_ALT = EXPAND_SIMD_RULE x86_VPSRAW;;
@@ -2853,8 +2885,8 @@ let X86_OPERATION_CLAUSES =
     x86_SAR; x86_SBB_ALT; x86_SET; x86_SHL; x86_SHLD; x86_SHR; x86_SHRD;
     x86_STC; x86_SUB_ALT; x86_TEST; x86_TZCNT; x86_XCHG; x86_XOR;
     (*** AVX2 instructions ***)
-    x86_VPADDW_ALT; x86_VPMULHW_ALT; x86_VPMULLW_ALT; x86_VPSUBW_ALT;
-    x86_VPXOR; x86_VPAND; x86_VPSRAD_ALT; x86_VPSRAW_ALT; x86_VPSRLW_ALT;
+    x86_VPADDD_ALT; x86_VPADDW_ALT; x86_VPMULHW_ALT; x86_VPMULLW_ALT; x86_VPSUBD_ALT;
+    x86_VPSUBW_ALT; x86_VPXOR; x86_VPAND; x86_VPSRAD_ALT; x86_VPSRAW_ALT; x86_VPSRLW_ALT;
     x86_VPSLLQ_ALT;
     (*** 32-bit backups since the ALT forms are 64-bit only ***)
     INST_TYPE[`:32`,`:N`] x86_ADC;
