Skip to content

Commit 9bfb08b

Browse files
strubstrub
committed
Merge branch 'main' into inlined-doc
2 parents 11bb6f8 + 3928a0c commit 9bfb08b

262 files changed

Lines changed: 19866 additions & 17109 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎.github/workflows/ci.yml‎

Lines changed: 88 additions & 36 deletions
Original file line numberDiff line numberDiff line change
@@ -1,126 +1,178 @@
11
name: EasyCrypt compilation & check
22

3-
on: [push,pull_request]
3+
on: [push,pull_request,merge_group]
44

55
env:
66
HOME: /home/charlie
77
OPAMYES: true
88
OPAMJOBS: 2
99

1010
jobs:
11+
pre_job:
12+
name: Check for Duplicates Jobs
13+
runs-on: ubuntu-20.04
14+
outputs:
15+
should_skip: ${{ steps.skip_check.outputs.should_skip }}
16+
steps:
17+
- uses: fkirc/skip-duplicate-actions@v5
18+
id: skip_check
19+
with:
20+
concurrent_skipping: 'same_content_newer'
21+
skip_after_successful_duplicate: 'false'
22+
1123
compile-opam:
1224
name: EasyCrypt compilation (opam)
25+
needs: pre_job
26+
if: needs.pre_job.outputs.should_skip != 'true'
1327
runs-on: ubuntu-20.04
1428
container:
1529
image: ghcr.io/easycrypt/ec-build-box
1630
steps:
17-
- uses: actions/checkout@v3
18-
- name: Update OPAM & EasyCrypt dependencies
31+
- uses: actions/checkout@v4
32+
- name: Install EasyCrypt dependencies
1933
run: |
20-
opam update
2134
opam pin add -n easycrypt .
2235
opam install --deps-only easycrypt
2336
- name: Compile EasyCrypt
24-
run: opam config exec -- make
37+
run: opam exec -- make
2538

2639
compile-nix:
2740
name: EasyCrypt compilation (nix)
41+
needs: pre_job
42+
if: needs.pre_job.outputs.should_skip != 'true'
2843
env:
2944
HOME: /home/runner
3045
runs-on: ubuntu-20.04
3146
steps:
32-
- uses: actions/checkout@v3
47+
- uses: actions/checkout@v4
3348
- name: Setup Nix
34-
uses: cachix/install-nix-action@v20
49+
uses: cachix/install-nix-action@v26
3550
with:
3651
nix_path: nixpkgs=channel:nixos-unstable
3752
- name: Setup Cachix
38-
uses: cachix/cachix-action@v12
53+
uses: cachix/cachix-action@v14
3954
with:
4055
name: formosa-crypto
4156
authToken: '${{ secrets.CACHIX_WRITE_TOKEN }}'
4257
- name: Build and cache EasyCrypt and dependencies
4358
run: |
44-
nix-build
59+
make nix-build-with-provers
4560
4661
check:
4762
name: Check EasyCrypt Libraries
48-
needs: compile-opam
63+
needs: [pre_job, compile-opam]
64+
if: needs.pre_job.outputs.should_skip != 'true'
4965
runs-on: ubuntu-20.04
5066
container:
5167
image: ghcr.io/easycrypt/ec-build-box
5268
strategy:
5369
fail-fast: false
5470
matrix:
55-
target: [stdlib, examples]
71+
target: [unit, stdlib, examples]
5672
steps:
57-
- uses: actions/checkout@v3
58-
- name: Update OPAM & EasyCrypt dependencies
73+
- uses: actions/checkout@v4
74+
- name: Install EasyCrypt dependencies
5975
run: |
60-
opam update
6176
opam pin add -n easycrypt .
6277
opam install --deps-only easycrypt
6378
- name: Compile EasyCrypt
64-
run: opam config exec -- make
79+
run: opam exec -- make
6580
- name: Detect SMT provers
6681
run: |
6782
rm -f ~/.why3.conf
68-
opam config exec -- ./ec.native why3config -why3 ~/.why3.conf
83+
opam exec -- ./ec.native why3config -why3 ~/.why3.conf
6984
- name: Compile Library (${{ matrix.target }})
7085
env:
7186
TARGET: ${{ matrix.target }}
72-
run: opam config exec -- make $TARGET
73-
- uses: actions/upload-artifact@v3
87+
run: opam exec -- make $TARGET
88+
- uses: actions/upload-artifact@v4
7489
name: Upload report.log
7590
if: always()
7691
with:
7792
name: report.log (${{ matrix.target }})
7893
path: report.log
7994
if-no-files-found: ignore
8095

96+
fetch-external-matrix:
97+
name: Fetch EasyCrypt External Projects Matrix
98+
needs: [pre_job]
99+
runs-on: ubuntu-20.04
100+
outputs:
101+
matrix: ${{ steps.set-matrix.outputs.matrix }}
102+
steps:
103+
- uses: actions/checkout@v4
104+
with:
105+
path: 'easycrypt'
106+
- id: set-matrix
107+
run: |
108+
JSON=$(jq -c . < easycrypt/.github/workflows/external.json)
109+
echo "matrix=${JSON}" >> $GITHUB_OUTPUT
110+
81111
external:
82112
name: Check EasyCrypt External Projects
83-
needs: compile-opam
113+
needs: [pre_job, compile-opam, fetch-external-matrix]
114+
if: needs.pre_job.outputs.should_skip != 'true'
84115
runs-on: ubuntu-20.04
85116
container:
86117
image: ghcr.io/easycrypt/ec-build-box
87118
strategy:
88119
fail-fast: false
89120
matrix:
90-
target: [ [ 'jasmin-eclib', 'jasmin-lang/jasmin', 'eclib', 'tests.config', 'jasmin' ] ]
121+
target: ${{fromJson(needs.fetch-external-matrix.outputs.matrix)}}
91122
steps:
92-
- uses: actions/checkout@v3
123+
- uses: actions/checkout@v4
93124
with:
94-
path: 'easycrypt'
95-
- uses: actions/checkout@v3
96-
with:
97-
path: 'project'
98-
repository: ${{ matrix.target[1] }}
99-
- name: Update OPAM & EasyCrypt dependencies
125+
path: easycrypt
126+
- name: Checkout External Project
127+
run: |
128+
git clone --recurse-submodules \
129+
-b ${{ matrix.target.branch }} \
130+
${{ matrix.target.repository }} \
131+
project/${{ matrix.target.name }}
132+
- name: Install EasyCrypt dependencies
100133
run: |
101-
opam update
102134
opam pin add -n easycrypt easycrypt
103135
opam install --deps-only easycrypt
104136
- name: Compile & Install EasyCrypt
105-
run: opam config exec -- make -C easycrypt build install
137+
run: opam exec -- make -C easycrypt build install
106138
- name: Detect SMT provers
107139
run: |
108140
rm -f ~/.why3.conf ~/.config/easycrypt/why3.conf
109-
opam config exec -- easycrypt why3config
141+
opam exec -- easycrypt why3config
110142
- name: Compile project
111-
working-directory: project/${{ matrix.target[2] }}
112-
run: opam config exec -- ec-runtest ${{ matrix.target[3] }} ${{ matrix.target[4] }}
113-
- uses: actions/upload-artifact@v3
143+
working-directory: project/${{ matrix.target.name }}/${{ matrix.target.subdir }}
144+
run: |
145+
opam exec -- easycrypt runtest \
146+
-report report.log \
147+
${{ matrix.target.options }} \
148+
${{ matrix.target.config }} \
149+
${{ matrix.target.scenario }}
150+
- name: Compute real-path to report.log
151+
if: always()
152+
run: |
153+
echo "report=$(realpath project/${{ matrix.target.name }}/${{ matrix.target.subdir }})/report.log" >> $GITHUB_ENV
154+
- uses: actions/upload-artifact@v4
114155
name: Upload report.log
115156
if: always()
116157
with:
117-
name: report.log (${{ matrix.target[0] }})
118-
path: report.log
158+
name: report.log (${{ matrix.target.name }})
159+
path: ${{ env.report }}
119160
if-no-files-found: ignore
120161

162+
external-status:
163+
name: Check EasyCrypt External Projects (set-status)
164+
if: always()
165+
needs: [external]
166+
runs-on: ubuntu-20.04
167+
steps:
168+
- uses: re-actors/alls-green@release/v1
169+
with:
170+
jobs: ${{ toJSON(needs) }}
171+
allowed-skips: external
172+
121173
notification:
122174
name: Notification
123-
needs: [compile-opam, compile-nix, check, external]
175+
needs: [compile-opam, compile-nix, check, external, external-status]
124176
if: |
125177
(github.event_name == 'push') ||
126178
(github.event_name == 'pull_request' && github.event.pull_request.head.repo.full_name == github.repository)

‎.github/workflows/external.json‎

Lines changed: 43 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,43 @@
1+
[
2+
{ "name" : "jasmin-eclib"
3+
, "repository" : "https://github.com/jasmin-lang/jasmin"
4+
, "branch" : "main"
5+
, "subdir" : "eclib"
6+
, "config" : "tests.config"
7+
, "scenario" : "jasmin"
8+
, "options" : ""
9+
}
10+
11+
,
12+
13+
{ "name" : "sha3"
14+
, "repository" : "https://gitlab.com/easycrypt/sha3"
15+
, "branch" : "next"
16+
, "subdir" : "."
17+
, "config" : "config/tests.config"
18+
, "scenario" : "sponge"
19+
, "options" : "-jobs 1"
20+
}
21+
22+
,
23+
24+
{ "name" : "cryptobox"
25+
, "repository" : "https://gitlab.com/fdupress/ec-cryptobox"
26+
, "branch" : "next"
27+
, "subdir" : "."
28+
, "config" : "config/tests.config"
29+
, "scenario" : "cryptobox"
30+
, "options" : ""
31+
}
32+
33+
,
34+
35+
{ "name" : "xsalsa20"
36+
, "repository" : "https://gitlab.com/fdupress/ec-xsalsa"
37+
, "branch" : "master"
38+
, "subdir" : "."
39+
, "config" : "config/tests.config"
40+
, "scenario" : "xsalsa"
41+
, "options" : ""
42+
}
43+
]

‎.gitignore‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@
44
*.pyo
55

66
/_build
7+
/result
78
/etc
89
/theories/attic
910

@@ -19,3 +20,4 @@
1920

2021
.merlin
2122
*.install
23+
*.log

‎Makefile‎

Lines changed: 19 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -6,27 +6,30 @@ ECARGS ?=
66
ECTOUT ?= 10
77
ECJOBS ?= 0
88
ECEXTRA ?= --report=report.log
9-
ECPROVERS ?= Alt-Ergo Z3 CVC4
109
CHECKPY ?=
1110
CHECK := $(CHECKPY) scripts/testing/runtest
12-
CHECK += --bin-args="$(ECARGS)" --bin-args="$(ECPROVERS:%=-p %)"
13-
CHECK += --timeout="$(ECTOUT)" --jobs="$(ECJOBS)"
11+
CHECK += --bin=./ec.native
12+
CHECK += --jobs="$(ECJOBS)"
13+
CHECK += --bin-args=-timeout --bin-args="$(ECTOUT)"
14+
CHECK += $(foreach arg,$(ECARGS),--bin-args="$(arg)")
1415
CHECK += $(ECEXTRA) config/tests.config
16+
NIX ?= nix --extra-experimental-features "nix-command flakes"
1517

1618
# --------------------------------------------------------------------
1719
UNAME_P = $(shell uname -p)
1820
UNAME_S = $(shell uname -s)
1921

2022
# --------------------------------------------------------------------
2123
.PHONY: default build byte native tests check examples
24+
.PHONY: nix-build nix-build-with-provers nix-develop
2225
.PHONY: clean install uninstall
2326

2427
default: build
2528
@true
2629

2730
build:
2831
rm -f src/ec.exe ec.native
29-
dune build -p easycrypt
32+
dune build
3033
ln -sf src/ec.exe ec.native
3134
ifeq ($(UNAME_P)-$(UNAME_S),arm-Darwin)
3235
-codesign -f -s - src/ec.exe
@@ -38,17 +41,27 @@ install: build
3841
uninstall:
3942
$(DUNE) uninstall
4043

41-
check: stdlib examples
44+
unit: build
45+
$(CHECK) unit
4246

4347
stdlib: build
4448
$(CHECK) prelude stdlib
4549

4650
examples: build
4751
$(CHECK) examples mee-cbc
4852

49-
check: stdlib examples
53+
check: unit stdlib examples
5054
@true
5155

56+
nix-build:
57+
$(NIX) build
58+
59+
nix-build-with-provers:
60+
$(NIX) build .#with_provers
61+
62+
nix-develop:
63+
$(NIX) develop
64+
5265
clean:
5366
rm -f ec.native && $(DUNE) clean
5467
find theories examples -name '*.eco' -exec rm '{}' ';'

0 commit comments

Comments
 (0)