Skip to content

feat(ci): test Kyber extraction and proofs #1536

feat(ci): test Kyber extraction and proofs

feat(ci): test Kyber extraction and proofs #1536

name: Install & test
on:
pull_request:
merge_group:
workflow_dispatch:
push:
branches: [main]
jobs:
tests:
name: nix-action
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v3
- uses: DeterminateSystems/nix-installer-action@main
- uses: DeterminateSystems/magic-nix-cache-action@main
- name: Build
run: nix build -L
- name: Install the toolchain
run: |
nix profile install nixpkgs#yq
nix profile install .#rustc
nix profile install .
- name: Ensure readme coherency
run: |
nix build .#check-readme-coherency -L
- name: Test the toolchain
run: |
nix build .#check-toolchain -L
- name: Test the examples
run: |
nix build .#check-examples -L
- name: Checkout specifications
uses: actions/checkout@v3
with:
repository: 'hacspec/specs'
path: specs
- name: Extract specifications
working-directory: specs
run: |
paths=$(tomlq -r '.workspace.members | .[]' Cargo.toml)
for cratePath in $paths; do
crate=$(tomlq -r '.package.name' "$cratePath/Cargo.toml")
for backend in fstar coq; do
for skip in $SKIPLIST; do
if [[ "$skip" == "$crate" || "$skip" == "$crate-$backend" ]]; then
echo "⛔ $crate [$backend] (skipping)"
continue 2
fi
done
echo "::group::$crate [$backend]"
cargo hax -C -p "$crate" \; into "$backend"
echo "::endgroup::"
done
done
env:
SKIPLIST: |
tls_cryptolib
hacspec-merlin
hacspec-halo2-coq
hacspec-halo2-fstar
hacspec-weierstrass-coq
hacspec-weierstrass-fstar
- name: Push to Cachix
if: ${{ github.event_name == 'workflow_dispatch' || github.event_name == 'merge_group' }}
env:
CACHIX_AUTH_TOKEN: ${{ secrets.CACHIX_AUTH_TOKEN }}
run: |
nix profile install nixpkgs#cachix nixpkgs#jq
nix build --json \
| jq -r '.[].outputs | to_entries[].value' \
| cachix push hax