github ci: add sematest and tutorial (#261)

This also adds
- A new HOLLIGHT_COMMIT variable for easier configuration
- Combine variants of existing test and aws-lc integration tests with matrix

Author: aqjune-aws

.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,8 +26,9 @@ 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
         CC=gcc make complete
@@ -37,8 +45,12 @@ jobs:
         make clean
         CC=clang make
 
-  s2n-bignum-arm-aws-lc-integration:
-    runs-on: ubuntu-24.04-arm
+  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
@@ -67,8 +79,12 @@ jobs:
         cmake3 -GNinja -DCMAKE_BUILD_TYPE=RelWithDebInfo -DFIPS=Off ../aws-lc
         ninja-build run_tests
 
-  s2n-bignum-x86-tests:
-    runs-on: ubuntu-24.04
+  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
@@ -77,31 +93,36 @@ jobs:
     - name: Install dependent packages
       run: |
         sudo apt update
-        sudo apt install valgrind
+        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: |
-        cd x86
-        make
-        cd ../x86_att && make clobber && make && git diff --exit-code .
-        echo "Make test (build only, for clang)"
-        cd ../tests
-        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
-        CC=gcc make
-        make clean
-        CC=clang make
+        export HOLDIR=`pwd`/hol-light
+        cd ${{ matrix.arch }}
+        make sematest
+
+  s2n-bignum-tutorial:
+    strategy:
+      matrix:
+        arch: [arm, x86]
 
-  s2n-bignum-x86-aws-lc-integration:
-    runs-on: ubuntu-24.04
+    runs-on: ${{ matrix.arch == 'arm' && 'ubuntu-24.04-arm' || matrix.arch == 'x86' && 'ubuntu-24.04' }}
 
     steps:
     - name: Checkout code
@@ -110,22 +131,26 @@ jobs:
     - 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
+        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: Run tests
+    - name: Install HOL Light
       run: |
-        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
+        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