Formal verification: resurrect fiat-crypto with formally verified assembly #1979
Workflow file for this run
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: Constantine CI | |
| on: [push, pull_request] | |
| jobs: | |
| build: | |
| strategy: | |
| fail-fast: false | |
| max-parallel: 20 | |
| matrix: | |
| nim_version: [version-1-6, version-2-0] | |
| rust_toolchain: [stable] # [beta, nightly] | |
| go_toolchain: [stable] | |
| target: | |
| - os: linux | |
| cpu: i386 | |
| TEST_LANG: c | |
| BACKEND: NO_ASM | |
| - os: linux | |
| cpu: i386 | |
| TEST_LANG: c | |
| BACKEND: ASM | |
| - os: linux | |
| cpu: amd64 | |
| TEST_LANG: c | |
| BACKEND: NO_ASM | |
| - os: linux | |
| cpu: amd64 | |
| TEST_LANG: c | |
| BACKEND: ASM | |
| - os: windows | |
| cpu: amd64 | |
| TEST_LANG: c | |
| BACKEND: NO_ASM | |
| - os: windows | |
| cpu: amd64 | |
| TEST_LANG: c | |
| BACKEND: ASM | |
| # MacOS Github agents are now using ARM and we need Nim ARM nightlies: https://github.com/mratsim/constantine/issues/372 | |
| # - os: macos | |
| # cpu: amd64 | |
| # TEST_LANG: c | |
| # BACKEND: NO_ASM | |
| # - os: macos | |
| # cpu: amd64 | |
| # TEST_LANG: c | |
| # BACKEND: ASM | |
| include: | |
| - target: | |
| os: linux | |
| builder: ubuntu-latest | |
| # - target: | |
| # os: macos | |
| # builder: macos-latest | |
| - target: | |
| os: windows | |
| builder: windows-latest | |
| name: '${{ matrix.target.os }}-${{ matrix.target.cpu }}-${{ matrix.target.TEST_LANG }}-${{ matrix.target.BACKEND }} (${{ matrix.nim_version }})' | |
| runs-on: ${{ matrix.builder }} | |
| steps: | |
| - name: Get branch name | |
| shell: bash | |
| run: | | |
| if [[ '${{ github.event_name }}' == 'pull_request' ]]; then | |
| echo "##[set-output name=branch_name;]$(echo ${GITHUB_HEAD_REF})" | |
| echo "Branch found (PR): ${GITHUB_HEAD_REF}" | |
| else | |
| echo "##[set-output name=branch_name;]$(echo ${GITHUB_REF#refs/heads/})" | |
| echo "Branch found (not PR): ${GITHUB_REF#refs/heads/}" | |
| fi | |
| id: get_branch | |
| - name: Cancel Previous Runs (except master) | |
| if: > | |
| steps.get_branch.outputs.branch_name != 'master' | |
| uses: styfle/[email protected] | |
| with: | |
| access_token: ${{ github.token }} | |
| - name: Checkout constantine | |
| uses: actions/checkout@v4 | |
| with: | |
| path: constantine | |
| - name: Restore MinGW-W64 (Windows) from cache | |
| if: runner.os == 'Windows' | |
| id: windows-mingw-cache | |
| uses: actions/cache@v3 | |
| with: | |
| path: external/mingw-${{ matrix.target.cpu }} | |
| key: 'mingw-${{ matrix.target.cpu }}' | |
| - name: Restore Nim DLLs dependencies (Windows) from cache | |
| if: runner.os == 'Windows' | |
| id: windows-dlls-cache | |
| uses: actions/cache@v3 | |
| with: | |
| path: external/dlls-${{ matrix.target.cpu }} | |
| key: 'dlls-${{ matrix.target.cpu }}' | |
| - name: Install MinGW64 dependency (Windows) | |
| if: > | |
| steps.windows-mingw-cache.outputs.cache-hit != 'true' && | |
| runner.os == 'Windows' | |
| shell: bash | |
| run: | | |
| mkdir -p external | |
| if [[ '${{ matrix.target.cpu }}' == 'amd64' ]]; then | |
| MINGW_URL="https://github.com/brechtsanders/winlibs_mingw/releases/download/11.1.0-12.0.0-9.0.0-r2/winlibs-x86_64-posix-seh-gcc-11.1.0-mingw-w64-9.0.0-r2.7z" | |
| ARCH=64 | |
| else | |
| MINGW_URL="https://github.com/brechtsanders/winlibs_mingw/releases/download/11.1.0-12.0.0-9.0.0-r2/winlibs-i686-posix-dwarf-gcc-11.1.0-mingw-w64-9.0.0-r2.7z" | |
| ARCH=32 | |
| fi | |
| curl -L "$MINGW_URL" -o "external/mingw-${{ matrix.target.cpu }}.7z" | |
| 7z x -y "external/mingw-${{ matrix.target.cpu }}.7z" -oexternal/ | |
| mv external/mingw$ARCH external/mingw-${{ matrix.target.cpu }} | |
| - name: Install DLLs dependencies (Windows) | |
| if: > | |
| steps.windows-dlls-cache.outputs.cache-hit != 'true' && | |
| runner.os == 'Windows' | |
| shell: bash | |
| run: | | |
| mkdir -p external | |
| curl -L "https://nim-lang.org/download/windeps.zip" -o external/windeps.zip | |
| 7z x -y external/windeps.zip -oexternal/dlls-${{ matrix.target.cpu }} | |
| - name: Path to cached dependencies (Windows) | |
| if: > | |
| runner.os == 'Windows' | |
| shell: bash | |
| run: | | |
| echo '${{ github.workspace }}'"/external/mingw-${{ matrix.target.cpu }}/bin" >> $GITHUB_PATH | |
| echo '${{ github.workspace }}'"/external/dlls-${{ matrix.target.cpu }}" >> $GITHUB_PATH | |
| - name: Restore Nim from cache | |
| if: matrix.nim_version != 'devel' | |
| id: nim-compiler-cache | |
| uses: actions/cache@v2 | |
| with: | |
| path: '${{ github.workspace }}/nim-${{ matrix.nim_version }}-${{ matrix.target.cpu }}' | |
| key: 'nim-${{ matrix.target.cpu }}-${{ matrix.nim_version }}' | |
| - name: Setup Nim | |
| if: steps.nim-compiler-cache.outputs.cache-hit != 'true' | |
| uses: alaviss/[email protected] | |
| with: | |
| path: 'nim-${{ matrix.nim_version }}-${{ matrix.target.cpu }}' | |
| version: ${{ matrix.nim_version }} | |
| architecture: ${{ matrix.target.cpu }} | |
| add-to-path: false | |
| - name: Path to cached Nim | |
| shell: bash | |
| run: | | |
| echo '${{ github.workspace }}'"/nim-${{ matrix.nim_version }}-${{ matrix.target.cpu }}/bin" >> $GITHUB_PATH | |
| echo '${{ github.workspace }}'"/.nimble/bin" >> $GITHUB_PATH | |
| - name: Install test dependencies (Linux amd64) | |
| if: runner.os == 'Linux' && matrix.target.cpu == 'amd64' | |
| run: | | |
| sudo DEBIAN_FRONTEND='noninteractive' apt-fast install \ | |
| --no-install-recommends -yq \ | |
| libgmp-dev \ | |
| llvm | |
| - name: Install test dependencies (Linux i386) | |
| if: runner.os == 'Linux' && matrix.target.cpu == 'i386' | |
| # We don't install LLVM as the Rust libraries that call Constantine are 64-bit only. | |
| run: | | |
| sudo dpkg --add-architecture i386 | |
| sudo apt-fast update -qq | |
| # Try to fix "E: Unable to correct problems, you have held broken packages." | |
| sudo apt-fast clean | |
| sudo DEBIAN_FRONTEND='noninteractive' apt-fast install \ | |
| --no-install-recommends -yq \ | |
| gcc-multilib g++-multilib \ | |
| libssl-dev:i386 libgmp-dev:i386 | |
| mkdir -p external/bin | |
| cat << EOF > external/bin/gcc | |
| #!/bin/bash | |
| exec $(which gcc) -m32 "\$@" | |
| EOF | |
| cat << EOF > external/bin/g++ | |
| #!/bin/bash | |
| exec $(which g++) -m32 "\$@" | |
| EOF | |
| chmod 755 external/bin/{gcc,g++} | |
| echo '${{ github.workspace }}/external/bin' >> $GITHUB_PATH | |
| - name: Install test dependencies (macOS) | |
| if: runner.os == 'macOS' | |
| run: | | |
| brew install gmp | |
| - name: Install Clang with Intel Assembly support (macOS) | |
| if: runner.os == 'macOS' | |
| # Apple Clang does not support Intel syntax due to missing | |
| # commit: https://github.com/llvm/llvm-project/commit/ae98182cf7341181e4aa815c372a072dec82779f | |
| # Revision: https://reviews.llvm.org/D113707 | |
| # Apple upstream: FB12137688 | |
| # Furthermore, Apple Clang can delete symbols when building a static library | |
| # in particular the hasAdxImpl bool for CPU runtime detection. | |
| # run: | | |
| # mkdir -p external/bin | |
| # cat << EOF > external/bin/clang | |
| # #!/bin/bash | |
| # exec $(brew --prefix llvm@15)/bin/clang "\$@" | |
| # EOF | |
| # cat << EOF > external/bin/clang++ | |
| # #!/bin/bash | |
| # exec $(brew --prefix llvm@15)/bin/clang++ "\$@" | |
| # EOF | |
| # chmod 755 external/bin/{clang,clang++} | |
| # echo '${{ github.workspace }}/external/bin' >> $GITHUB_PATH | |
| run: echo "$(brew --prefix llvm@15)/bin" >> $GITHUB_PATH | |
| - name: Setup MSYS2 (Windows) | |
| if: runner.os == 'Windows' | |
| uses: msys2/setup-msys2@v2 | |
| with: | |
| path-type: inherit | |
| update: false | |
| install: base-devel git mingw-w64-x86_64-toolchain | |
| - name: Install Go [${{ matrix.go_toolchain }}] | |
| uses: actions/setup-go@v4 | |
| with: | |
| go-version: ${{ matrix.go_toolchain }} | |
| - name: Install Rust [${{ matrix.rust_toolchain }}] | |
| shell: bash | |
| run: rustup default ${{ matrix.rust_toolchain }} | |
| - name: Print Nim, Go Rust, LLVM versions and CPU specs. | |
| shell: bash | |
| # gcc is an alias to Apple Clang on MacOS | |
| run: | | |
| nim -v | |
| gcc -v | |
| clang -v | |
| go version | |
| rustup --version | |
| if [[ '${{ matrix.target.cpu }}' != 'i386' && '${{ runner.os }}' != 'Windows' ]]; then | |
| llvm-config --version | |
| fi | |
| if [[ '${{ runner.os }}' == 'Linux' ]]; then | |
| cat /proc/cpuinfo | |
| fi | |
| if [[ '${{ runner.os }}' == 'macOS' ]]; then | |
| sysctl -a | grep machdep.cpu | |
| sysctl -a | grep hw | grep cpu | |
| sysctl -a | grep hw.optional | |
| fi | |
| - name: Install test dependencies (Windows) | |
| if: runner.os == 'Windows' | |
| shell: msys2 {0} | |
| run: | | |
| pacman -S --needed --noconfirm mingw-w64-x86_64-gmp mingw-w64-x86_64-llvm | |
| nimble refresh --verbose -y | |
| nimble install --verbose -y gmp@#head jsony asynctools [email protected] cliche | |
| cd constantine | |
| go mod download -modfile=go_test.mod | |
| - name: Install test dependencies | |
| if: runner.os != 'Windows' | |
| shell: bash | |
| run: | | |
| nimble refresh --verbose -y | |
| nimble install --verbose -y gmp@#head jsony asynctools [email protected] cliche | |
| cd constantine | |
| go mod download -modfile=go_test.mod | |
| - name: Run Constantine as C library tests (UNIX with Assembly) | |
| if: runner.os != 'Windows' && matrix.target.BACKEND == 'ASM' | |
| shell: bash | |
| run: | | |
| cd constantine | |
| nimble make_lib --verbose | |
| nimble make_headers --verbose | |
| nimble test_lib --verbose | |
| - name: Run Constantine as C library tests (UNIX no Assembly) | |
| if: runner.os != 'Windows' && matrix.target.BACKEND == 'NO_ASM' | |
| shell: bash | |
| run: | | |
| cd constantine | |
| CTT_ASM=0 nimble make_lib --verbose | |
| nimble make_headers --verbose | |
| nimble test_lib --verbose | |
| - name: Run Constantine as C library tests (Windows with Assembly) | |
| # So "test_bindings" uses C and can find GMP | |
| # but nim-gmp cannot find GMP on Windows CI | |
| if: runner.os == 'Windows' && matrix.target.BACKEND == 'ASM' | |
| shell: msys2 {0} | |
| run: | | |
| cd constantine | |
| nimble make_lib --verbose | |
| nimble make_headers --verbose | |
| nimble test_lib --verbose | |
| - name: Run Constantine as C library tests (Windows no Assembly) | |
| # So "test_bindings" uses C and can find GMP | |
| # but nim-gmp cannot find GMP on Windows CI | |
| if: runner.os == 'Windows' && matrix.target.BACKEND == 'NO_ASM' | |
| shell: msys2 {0} | |
| run: | | |
| cd constantine | |
| CTT_ASM=0 nimble make_lib --verbose | |
| nimble make_headers --verbose | |
| nimble test_lib --verbose | |
| - name: Run Constantine as Go library tests | |
| # This reuses the static library built with `nimble make_lib` | |
| if: matrix.target.cpu != 'i386' | |
| shell: bash | |
| run: | | |
| cd constantine/constantine-go | |
| go test -modfile=../go_test.mod | |
| - name: Run Constantine as Rust library tests (with Assembly) | |
| if: matrix.target.BACKEND == 'ASM' && matrix.target.cpu != 'i386' | |
| shell: bash | |
| # We need to deactivate the assembly (used by default for benches) | |
| run: | | |
| cd constantine | |
| cargo test -- --nocapture | |
| - name: Run Constantine as Rust library tests (NO Assembly) | |
| if: matrix.target.BACKEND == 'NO_ASM' && matrix.target.cpu != 'i386' | |
| shell: bash | |
| # We need to deactivate the assembly (used by default for benches) | |
| run: | | |
| cd constantine | |
| CTT_ASM=0 cargo test -- --nocapture | |
| - name: Compile Constantine Zkalc benchmark (no assembly) | |
| # Skip 32-bit as that would need clang-multilib or -m32 | |
| # Skip Windows as clang throws fatal error LNK1107 | |
| if: matrix.target.BACKEND == 'NO_ASM' && matrix.target.cpu != 'i386' && runner.os != 'Windows' | |
| shell: bash | |
| run: | | |
| cd constantine | |
| CTT_ASM=0 nimble make_zkalc | |
| - name: Compile Constantine Zkalc benchmark (with assembly) | |
| # Skip 32-bit as that would need clang-multilib or -m32 | |
| # Skip Windows as clang throws fatal error LNK1107 | |
| if: matrix.target.BACKEND == 'ASM' && matrix.target.cpu != 'i386' && runner.os != 'Windows' | |
| shell: bash | |
| run: | | |
| cd constantine | |
| nimble make_zkalc | |
| - name: Run Constantine in-depth tests (Unix - with GMP, with Assembly) | |
| if: runner.os != 'Windows' && matrix.target.BACKEND == 'ASM' | |
| shell: bash | |
| run: | | |
| cd constantine | |
| nimble test_parallel --verbose | |
| - name: Run Constantine in-depth tests (Unix - with GMP, no Assembly) | |
| if: runner.os != 'Windows' && matrix.target.BACKEND == 'NO_ASM' | |
| shell: bash | |
| run: | | |
| cd constantine | |
| CTT_ASM=0 nimble test_parallel --verbose | |
| - name: Run Constantine in-depth tests (Windows - no GMP, with Assembly) | |
| # So "test_bindings" uses C and can find GMP | |
| # but nim-gmp cannot find GMP on Windows CI | |
| # Also need to workaround asynctools not being able to create pipes https://github.com/nim-lang/Nim/issues/23118 | |
| if: runner.os == 'Windows' && matrix.target.BACKEND == 'ASM' | |
| shell: msys2 {0} | |
| run: | | |
| cd constantine | |
| if [[ '${{ matrix.nim_version }}' == 'version-2-0' ]]; then | |
| nimble test_no_gmp --verbose | |
| else | |
| nimble test_parallel_no_gmp --verbose | |
| fi | |
| - name: Run Constantine in-depth tests (Windows - no GMP, no Assembly) | |
| # So "test_bindings" uses C and can find GMP | |
| # but nim-gmp cannot find GMP on Windows CI | |
| # Also need to workaround asynctools not being able to create pipes https://github.com/nim-lang/Nim/issues/23118 | |
| if: runner.os == 'Windows' && matrix.target.BACKEND == 'NO_ASM' | |
| shell: msys2 {0} | |
| run: | | |
| cd constantine | |
| if [[ '${{ matrix.nim_version }}' == 'version-2-0' ]]; then | |
| CTT_ASM=0 nimble test_no_gmp --verbose | |
| else | |
| CTT_ASM=0 nimble test_parallel_no_gmp --verbose | |
| fi |