Skip to content

ML-KEM iNTT proof for x86 AVX2 implementation #493

ML-KEM iNTT proof for x86 AVX2 implementation

ML-KEM iNTT proof for x86 AVX2 implementation #493

Workflow file for this run

name: CI
on:
pull_request:
branches: [ main ]
env:
HOLLIGHT_COMMIT: "08bcac75772d37c2447a90c90d1dff9ab415f217"
jobs:
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
uses: actions/checkout@v4
- name: Install dependent packages
run: |
sudo apt update
sudo apt install valgrind
- name: Run tests
run: |
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
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
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: |
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 -DBUILD_SHARED_LIBS=1 ../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 -j2
s2n-bignum-tutorial-macos-arm:
runs-on: macos-latest
steps:
- name: Checkout code
uses: actions/checkout@v4
- name: Install dependent packages
run: |
brew install opam
opam init -a
- 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 arm
make tutorial -j2