Skip to content

Commit 6079933

Browse files
mkannwischermkannwischer
authored
Merge pull request #16 from pq-code-package/cbmc
Add CBMC scaffolding + CI and initial (trivial) `sha2_256_init` proof
2 parents 91a2218 + c2da259 commit 6079933

File tree

23 files changed

+2966
-1
lines changed

23 files changed

+2966
-1
lines changed

‎.github/actions/cbmc/action.yml‎

Lines changed: 54 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,54 @@
1+
# Copyright (c) The mlkem-native project authors
2+
# Copyright (c) The slhdsa-c project authors
3+
# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
4+
5+
name: CBMC
6+
description: Run CBMC proofs for slhdsa-c
7+
8+
inputs:
9+
nix-shell:
10+
description: Run in the specified Nix environment if exists
11+
default: "ci-cbmc"
12+
nix-cache:
13+
description: Determine whether to enable nix cache
14+
default: 'true'
15+
nix-verbose:
16+
description: Determine wether to suppress nix log or not
17+
default: 'false'
18+
custom_shell:
19+
description: The shell to use. Only relevant if use-nix is 'false'
20+
default: "bash"
21+
gh_token:
22+
description: Github access token to use
23+
required: true
24+
runs:
25+
using: composite
26+
steps:
27+
- uses: ./.github/actions/setup-shell
28+
with:
29+
nix-shell: ${{ inputs.nix-shell }}
30+
nix-cache: ${{ inputs.nix-cache }}
31+
nix-verbose: ${{ inputs.nix-verbose }}
32+
gh_token: ${{ inputs.gh_token }}
33+
custom_shell: ${{ inputs.custom_shell }}
34+
script: |
35+
36+
if [[ ${{ inputs.nix-shell }} != '' ]]; then
37+
nix-collect-garbage
38+
fi
39+
40+
cat >> $GITHUB_STEP_SUMMARY << EOF
41+
## Setup
42+
Architecture: $(uname -m)
43+
- $(nix --version)
44+
- $(cbmc --version)
45+
- litani Version $(litani --version)
46+
- Cadical Version $(cadical --version)
47+
- $(bash --version | grep -m1 "")
48+
EOF
49+
- name: Run CBMC proofs
50+
shell: ${{ env.SHELL }}
51+
run: |
52+
cd proofs/cbmc
53+
python3 run-cbmc-proofs.py --summarize --no-coverage -j$(nproc)
54+

‎.github/actions/setup-nix/action.yml‎

Lines changed: 138 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,138 @@
1+
# Copyright (c) The mlkem-native project authors
2+
# Copyright (c) The slhdsa-c project authors
3+
# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
4+
5+
name: Setup nix
6+
description: Setup nix
7+
8+
inputs:
9+
script:
10+
description: The script to be run in the nix shell
11+
required: false
12+
devShell:
13+
description: The name of the devShell
14+
required: true
15+
cache:
16+
description: Determine whether to enable nix cache
17+
default: 'false'
18+
verbose:
19+
description: Determine wether to suppress nix log or not
20+
default: 'false'
21+
cache_prefix:
22+
description: Fixed prefix of ID of Github cache entries that should be removed.
23+
required: false
24+
save_cache:
25+
description: Determine whether to save cache with primary key or not
26+
required: false
27+
default: 'false'
28+
gh_token:
29+
description: Github access token to use
30+
required: true
31+
install:
32+
required: false
33+
description: Determine how to install nix ('installer' | 'apt')
34+
default: 'installer'
35+
36+
runs:
37+
using: composite
38+
steps:
39+
- name: Pre-check nix
40+
id: nix-pre-check
41+
if: ${{ env.NIX_SHELL == '' }}
42+
shell: bash -lo pipefail {0}
43+
run: |
44+
suppress() {
45+
local exit_code="$?"
46+
local line_no="$1"
47+
echo "Nix check failed at $line_no: $exit_code"
48+
echo "installed=false" >> $GITHUB_OUTPUT
49+
exit 0
50+
}
51+
52+
trap 'suppress $LINENO' ERR
53+
54+
if [[ $USER == 'root' ]]; then
55+
mkdir -p /root
56+
echo "HOME=/root" >> $GITHUB_ENV
57+
fi
58+
59+
nix --version
60+
- name: Install nix via apt
61+
if: ${{ steps.nix-pre-check.outputs.installed == 'false' && inputs.install == 'apt' }}
62+
shell: bash
63+
run: |
64+
if [[ -f /.dockerenv ]]; then
65+
apt install nix -y
66+
else
67+
sudo apt install nix -y
68+
fi
69+
mkdir -p ~/.config/nix
70+
cat >> ~/.config/nix/nix.conf << EOF
71+
experimental-features = nix-command flakes
72+
EOF
73+
74+
if [[ ! -z $GH_TOKEN ]]; then
75+
echo "access-tokens = github.com=$GH_TOKEN" >> ~/.config/nix/nix.conf
76+
fi
77+
- uses: cachix/install-nix-action@08dcb3a5e62fa31e2da3d490afc4176ef55ecd72 # v30
78+
if: ${{ steps.nix-pre-check.outputs.installed == 'false' }}
79+
with:
80+
github_access_token: ${{ inputs.gh_token }}
81+
- name: Post-check nix
82+
id: nix-post-check
83+
continue-on-error: true
84+
shell: bash -lo pipefail {0}
85+
run: |
86+
echo "::group::nix config"
87+
if [[ -z "${{ inputs.cache_prefix }}" ]]; then
88+
cache_prefix="${{ runner.os }}-${{ runner.arch }}"
89+
else
90+
cache_prefix="${{ inputs.cache_prefix }}"
91+
fi
92+
93+
echo "cache_prefix=$cache_prefix" >> $GITHUB_OUTPUT
94+
95+
if [[ "${{ steps.nix-pre-check.outputs.installed }}" == 'false' ]]; then
96+
sudo chown -R $USER:nixbld /nix
97+
fi
98+
99+
nix profile install nixpkgs/nixos-24.11#sqlite
100+
nix config show
101+
echo "::endgroup::"
102+
- uses: nix-community/cache-nix-action@dab0514428ae3988852b7787a6d86a6fc571cc9d #v6.0.0
103+
id: cache
104+
if: ${{ env.NIX_CACHE_ENABLED != 1 && inputs.cache == 'true' }}
105+
continue-on-error: true
106+
with:
107+
primary-key: ${{ steps.nix-post-check.outputs.cache_prefix }}-${{ hashFiles('**/*.nix') }}
108+
restore-prefixes-first-match: ${{ steps.nix-post-check.outputs.cache_prefix }}
109+
gc-max-store-size-linux: 536870912
110+
purge: ${{ inputs.save_cache == 'true' }}
111+
save: ${{ inputs.save_cache == 'true' }}
112+
purge-prefixes: cache-${{ steps.nix-post-check.outputs.cache_prefix }}
113+
purge-created: 0
114+
purge-primary-key: ${{ inputs.save_cache == 'true' && 'always' || 'never' }}
115+
token: ${{ inputs.gh_token }}
116+
- name: Set Shell
117+
shell: bash -lo pipefail {0}
118+
run: |
119+
echo "::group::set nix shell"
120+
if [[ "${{ steps.cache.outputs.hit-primary-key }}" == "true" ]]; then
121+
echo NIX_CACHE_ENABLED=1 >> $GITHUB_ENV
122+
fi
123+
124+
echo NIX_SHELL="${{ inputs.devShell }}" >> $GITHUB_ENV
125+
nix_extra_flags="${{ inputs.verbose == 'false' && '--quiet' || '' }}"
126+
if [[ ${{ inputs.install }} == 'apt' && ! -f /.dockerenv ]]; then
127+
echo SHELL="sudo $(which nix) develop $nix_extra_flags .#${{ inputs.devShell }} -c bash -e {0}" >> $GITHUB_ENV
128+
else
129+
echo SHELL="$(which nix) develop $nix_extra_flags .#${{ inputs.devShell }} -c bash -e {0}" >> $GITHUB_ENV
130+
fi
131+
echo "::endgroup::"
132+
- name: Prepare nix dev shell
133+
shell: ${{ env.SHELL }}
134+
run: |
135+
- name: Dependency check
136+
shell: ${{ env.SHELL }}
137+
if: inputs.script != ''
138+
run: eval ${{ inputs.script }}

‎.github/actions/setup-shell/action.yml‎

Lines changed: 52 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,52 @@
1+
# Copyright (c) The mlkem-native project authors
2+
# Copyright (c) The slhdsa-c project authors
3+
# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
4+
5+
name: Set Shell
6+
description: Setup nix or custom shell for workflows
7+
8+
inputs:
9+
nix-shell:
10+
description: Run in the specified Nix environment if exists. If empty, custom shell will be used instead of nix.
11+
default: 'ci'
12+
nix-cache:
13+
description: Determine whether to enable nix cache
14+
default: 'false'
15+
nix-cache-prefix:
16+
description: Fixed prefix of ID of Github cache entries that should be removed.
17+
required: false
18+
nix-verbose:
19+
description: Determine wether to suppress nix log or not
20+
default: 'false'
21+
custom_shell:
22+
description: The shell to use. Only relevant if no nix-shell specified
23+
default: 'bash'
24+
script:
25+
description: The script to be run in the nix shell
26+
required: false
27+
gh_token:
28+
description: Github access token to use
29+
required: true
30+
31+
runs:
32+
using: composite
33+
steps:
34+
- name: Setup nix
35+
uses: ./.github/actions/setup-nix
36+
if: ${{ inputs.nix-shell != '' }}
37+
with:
38+
devShell: ${{ inputs.nix-shell }}
39+
gh_token: ${{ inputs.gh_token }}
40+
verbose: ${{ inputs.nix-verbose }}
41+
cache: ${{ inputs.nix-cache }}
42+
script: ${{ inputs.script }}
43+
cache_prefix: ${{ inputs.nix-cache-prefix }}
44+
- name: Set custom shell
45+
shell: bash
46+
if: ${{ inputs.nix-shell == '' }}
47+
run: |
48+
echo SHELL="${{ inputs.custom_shell }}" >> $GITHUB_ENV
49+
50+
if [[ "${{ inputs.script }}" != '' ]]; then
51+
eval ${{ inputs.script }}
52+
fi

‎.github/workflows/all.yml‎

Lines changed: 32 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,32 @@
1+
# Copyright (c) The mlkem-native project authors
2+
# Copyright (c) The slhdsa-c project authors
3+
# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
4+
5+
name: CI
6+
permissions:
7+
contents: read
8+
on:
9+
workflow_dispatch:
10+
push:
11+
branches: ["main"]
12+
pull_request:
13+
branches: ["main"]
14+
types: [ "opened", "synchronize" ]
15+
jobs:
16+
nix:
17+
name: Nix
18+
permissions:
19+
actions: 'write'
20+
contents: 'read'
21+
id-token: 'write'
22+
uses: ./.github/workflows/nix.yml
23+
secrets: inherit
24+
cbmc:
25+
name: CBMC
26+
permissions:
27+
contents: 'read'
28+
id-token: 'write'
29+
needs: [ nix ]
30+
uses: ./.github/workflows/cbmc.yml
31+
secrets: inherit
32+

‎.github/workflows/cbmc.yml‎

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
# Copyright (c) The mlkem-native project authors
2+
# Copyright (c) The slhdsa-c project authors
3+
# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
4+
5+
name: CBMC
6+
permissions:
7+
contents: read
8+
on:
9+
workflow_call:
10+
workflow_dispatch:
11+
12+
jobs:
13+
cbmc:
14+
name: CBMC
15+
runs-on: ubuntu-latest
16+
steps:
17+
- uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
18+
- uses: ./.github/actions/cbmc
19+
with:
20+
gh_token: ${{ secrets.GITHUB_TOKEN }}

0 commit comments

Comments
 (0)