-
Notifications
You must be signed in to change notification settings - Fork 14
59 lines (49 loc) · 1.32 KB
/
hax.yml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
name: hax
on:
push:
branches: ["dev"]
paths:
- 'specs/kyber/src/**'
- 'src/kem/kyber768/**'
- 'src/kem/kyber768.rs'
pull_request:
branches: ["dev"]
paths:
- 'specs/kyber/src/**'
- 'src/kem/kyber768/**'
- 'src/kem/kyber768.rs'
workflow_dispatch:
env:
CARGO_TERM_COLOR: always
concurrency:
group: ${{ github.workflow }}-${{ github.ref }}
cancel-in-progress: true
jobs:
hax:
runs-on: "ubuntu-latest"
steps:
- uses: actions/checkout@v4
- name: 🔨 OCaml Setup
uses: ocaml/setup-ocaml@v2
with:
ocaml-compiler: 4.14.1
- name: ⤵ Clone hax repository
uses: actions/checkout@v4
with:
repository: hacspec/hacspec-v2
path: hax
- name: 🔨 Setup hax
working-directory: hax
run: |
sudo apt-get update
sudo apt-get install --yes nodejs
./setup.sh
- name: 🏃🏻♀️ Run hax on Kyber reference implementation
run: |
eval $(opam env)
cargo hax into -i '-** +kem::kyber768::** -kem::kyber768::arithmetic::mutable_operations::**' fstar
- name: 🏃🏻♀️ Run hax on Kyber specification
working-directory: specs/kyber
run: |
eval $(opam env)
cargo hax into fstar