Skip to content

Commit 7afba09

Browse files
mkannwischermkannwischer
committed
nix: Add initial setup borrowed from mlkem-native (trimmed down)
This add a nix development setup that includes dependencies required for developing CBMC proofs. I have excluded various things from the mlkem-native setup that we can consider adding later - HOL-Light (including s2n-bignum proof infrastructure) - SLOTHY - Valgrind (including the KyberSlash paches) - Big-endian cross compilers Signed-off-by: Matthias J. Kannwischer <[email protected]>
1 parent 91a2218 commit 7afba09

File tree

6 files changed

+493
-0
lines changed

6 files changed

+493
-0
lines changed

‎flake.lock‎

Lines changed: 82 additions & 0 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

‎flake.nix‎

Lines changed: 158 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,158 @@
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+
{
6+
description = "mlkem-native";
7+
8+
inputs = {
9+
nixpkgs-2405.url = "github:NixOS/nixpkgs/nixos-24.05";
10+
nixpkgs.url = "github:NixOS/nixpkgs/nixos-25.05";
11+
nixpkgs-unstable.url = "github:NixOS/nixpkgs/nixos-unstable";
12+
13+
flake-parts = {
14+
url = "github:hercules-ci/flake-parts";
15+
inputs.nixpkgs-lib.follows = "nixpkgs";
16+
};
17+
};
18+
19+
outputs = inputs@{ flake-parts, ... }:
20+
flake-parts.lib.mkFlake { inherit inputs; } {
21+
imports = [ ];
22+
systems = [ "x86_64-linux" "aarch64-linux" "aarch64-darwin" "x86_64-darwin" ];
23+
perSystem = { config, pkgs, system, ... }:
24+
let
25+
pkgs-unstable = inputs.nixpkgs-unstable.legacyPackages.${system};
26+
pkgs-2405 = inputs.nixpkgs-2405.legacyPackages.${system};
27+
util = pkgs.callPackage ./nix/util.nix {
28+
# Keep those around in case we want to switch to unstable versions
29+
cbmc = pkgs-unstable.cbmc;
30+
bitwuzla = pkgs.bitwuzla;
31+
z3 = pkgs.z3;
32+
};
33+
zigWrapCC = zig: pkgs.symlinkJoin {
34+
name = "zig-wrappers";
35+
paths = [
36+
(pkgs.writeShellScriptBin "cc"
37+
''
38+
exec ${zig}/bin/zig cc "$@"
39+
'')
40+
(pkgs.writeShellScriptBin "ar"
41+
''
42+
exec ${zig}/bin/zig ar "$@"
43+
'')
44+
];
45+
};
46+
in
47+
{
48+
_module.args.pkgs = import inputs.nixpkgs {
49+
inherit system;
50+
overlays = [
51+
(_:_: {
52+
gcc48 = pkgs-2405.gcc48;
53+
gcc49 = pkgs-2405.gcc49;
54+
gcc7 = pkgs-2405.gcc7;
55+
})
56+
];
57+
};
58+
59+
packages.linters = util.linters;
60+
packages.cbmc = util.cbmc_pkgs;
61+
62+
packages.toolchains = util.toolchains;
63+
packages.toolchains_native = util.toolchains_native;
64+
packages.toolchain_x86_64 = util.toolchain_x86_64;
65+
packages.toolchain_aarch64 = util.toolchain_aarch64;
66+
packages.toolchain_riscv64 = util.toolchain_riscv64;
67+
packages.toolchain_riscv32 = util.toolchain_riscv32;
68+
packages.toolchain_ppc64le = util.toolchain_ppc64le;
69+
70+
devShells.default = util.mkShell {
71+
packages = builtins.attrValues
72+
{
73+
inherit (config.packages) linters cbmc toolchains_native;
74+
inherit (pkgs)
75+
direnv
76+
nix-direnv
77+
zig_0_13;
78+
};
79+
};
80+
81+
devShells.ci = util.mkShell {
82+
packages = builtins.attrValues { inherit (config.packages) linters toolchains_native; };
83+
};
84+
devShells.ci-bench = util.mkShell {
85+
packages = builtins.attrValues { inherit (config.packages) toolchains_native; };
86+
};
87+
devShells.ci-cbmc = util.mkShell {
88+
packages = builtins.attrValues { inherit (config.packages) cbmc toolchains_native; };
89+
};
90+
devShells.ci-cross = util.mkShell {
91+
packages = builtins.attrValues { inherit (config.packages) linters toolchains; };
92+
};
93+
devShells.ci-cross-x86_64 = util.mkShell {
94+
packages = builtins.attrValues { inherit (config.packages) linters toolchain_x86_64; };
95+
};
96+
devShells.ci-cross-aarch64 = util.mkShell {
97+
packages = builtins.attrValues { inherit (config.packages) linters toolchain_aarch64; };
98+
};
99+
devShells.ci-cross-riscv64 = util.mkShell {
100+
packages = builtins.attrValues { inherit (config.packages) linters toolchain_riscv64; };
101+
};
102+
devShells.ci-cross-riscv32 = util.mkShell {
103+
packages = builtins.attrValues { inherit (config.packages) linters toolchain_riscv32; };
104+
};
105+
devShells.ci-cross-ppc64le = util.mkShell {
106+
packages = builtins.attrValues { inherit (config.packages) linters toolchain_ppc64le; };
107+
};
108+
devShells.ci-linter = util.mkShellNoCC {
109+
packages = builtins.attrValues { inherit (config.packages) linters; };
110+
};
111+
devShells.ci_clang14 = util.mkShellWithCC' pkgs.clang_14;
112+
devShells.ci_clang15 = util.mkShellWithCC' pkgs.clang_15;
113+
devShells.ci_clang16 = util.mkShellWithCC' pkgs.clang_16;
114+
devShells.ci_clang17 = util.mkShellWithCC' pkgs.clang_17;
115+
devShells.ci_clang18 = util.mkShellWithCC' pkgs.clang_18;
116+
devShells.ci_clang19 = util.mkShellWithCC' pkgs.clang_19;
117+
devShells.ci_clang20 = util.mkShellWithCC' pkgs.clang_20;
118+
119+
devShells.ci_zig0_12 = util.mkShellWithCC' (zigWrapCC pkgs.zig_0_12);
120+
devShells.ci_zig0_13 = util.mkShellWithCC' (zigWrapCC pkgs.zig_0_13);
121+
devShells.ci_zig0_14 = util.mkShellWithCC' (zigWrapCC pkgs.zig);
122+
123+
devShells.ci_gcc48 = util.mkShellWithCC' pkgs.gcc48;
124+
devShells.ci_gcc49 = util.mkShellWithCC' pkgs.gcc49;
125+
devShells.ci_gcc7 = util.mkShellWithCC' pkgs.gcc7;
126+
devShells.ci_gcc11 = util.mkShellWithCC' pkgs.gcc11;
127+
devShells.ci_gcc12 = util.mkShellWithCC' pkgs.gcc12;
128+
devShells.ci_gcc13 = util.mkShellWithCC' pkgs.gcc13;
129+
devShells.ci_gcc14 = util.mkShellWithCC' pkgs.gcc14;
130+
};
131+
flake = {
132+
devShell.x86_64-linux =
133+
let
134+
pkgs = inputs.nixpkgs.legacyPackages.x86_64-linux;
135+
pkgs-unstable = inputs.nixpkgs-unstable.legacyPackages.x86_64-linux;
136+
util = pkgs.callPackage ./nix/util.nix {
137+
inherit pkgs;
138+
cbmc = pkgs-unstable.cbmc;
139+
bitwuzla = pkgs.bitwuzla;
140+
z3 = pkgs.z3;
141+
};
142+
in
143+
util.mkShell {
144+
packages =
145+
[
146+
util.linters
147+
util.cbmc_pkgs
148+
util.toolchains_native
149+
pkgs.zig_0_13
150+
];
151+
};
152+
# The usual flake attributes can be defined here, including system-
153+
# agnostic ones like nixosModule and system-enumerating ones, although
154+
# those are more easily expressed in perSystem.
155+
156+
};
157+
};
158+
}

‎nix/cbmc/cbmc-viewer.nix‎

Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
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+
{ python3Packages
6+
, fetchurl
7+
}:
8+
9+
python3Packages.buildPythonApplication rec {
10+
pname = "cbmc-viewer";
11+
version = "3.11";
12+
src = fetchurl {
13+
url = "https://github.com/model-checking/${pname}/releases/download/viewer-${version}/cbmc_viewer-${version}-py3-none-any.whl";
14+
hash = "sha256-Oy51I64KMbtE8lG8xuFXdK4RvXFvWt4zYKBlcXqwILg=";
15+
};
16+
format = "wheel";
17+
dontUseSetuptoolsCheck = true;
18+
19+
propagatedBuildInputs = [
20+
python3Packages.voluptuous
21+
python3Packages.setuptools
22+
python3Packages.jinja2
23+
];
24+
25+
meta = {
26+
description = "CBMC Viewer is a tool that scans the output of CBMC";
27+
homepage = "https://model-checking.github.io/cbmc-viewer/";
28+
};
29+
}

‎nix/cbmc/default.nix‎

Lines changed: 39 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,39 @@
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+
{ buildEnv
6+
, cbmc
7+
, fetchFromGitHub
8+
, callPackage
9+
, bitwuzla
10+
, ninja
11+
, cadical
12+
, z3
13+
, cudd
14+
, replaceVars
15+
}:
16+
17+
buildEnv {
18+
name = "pqcp-cbmc";
19+
paths =
20+
builtins.attrValues {
21+
cbmc = cbmc.overrideAttrs (old: rec {
22+
version = "6.7.1";
23+
src = fetchFromGitHub {
24+
owner = "diffblue";
25+
repo = "cbmc";
26+
hash = "sha256-GUY4Evya0GQksl0R4b01UDSvoxUEOOeq4oOIblmoF5o=";
27+
tag = "cbmc-6.7.1";
28+
};
29+
});
30+
litani = callPackage ./litani.nix { }; # 1.29.0
31+
cbmc-viewer = callPackage ./cbmc-viewer.nix { }; # 3.11
32+
33+
inherit
34+
cadical#2.1.3
35+
bitwuzla# 0.7.0
36+
z3# 4.15.0
37+
ninja; # 1.12.1
38+
};
39+
}

‎nix/cbmc/litani.nix‎

Lines changed: 38 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,38 @@
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+
{ stdenvNoCC
6+
, fetchFromGitHub
7+
, python3Packages
8+
}:
9+
10+
stdenvNoCC.mkDerivation {
11+
pname = "litani";
12+
version = "8002c240ef4f424039ed3cc32e076c0234d01768";
13+
src = fetchFromGitHub {
14+
owner = "awslabs";
15+
repo = "aws-build-accumulator";
16+
rev = "8002c240ef4f424039ed3cc32e076c0234d01768";
17+
sha256 = "sha256-UwF/B6lpsjpQn8SW+tCfOXTp14pNBr2sRGujJH3iPLk=";
18+
};
19+
dontConfigure = true;
20+
installPhase = ''
21+
mkdir -p $out/bin
22+
install -Dm755 litani $out/bin/litani
23+
cp -r lib $out/bin
24+
cp -r templates $out/bin
25+
'';
26+
dontStrip = true;
27+
noAuditTmpdir = true;
28+
propagatedBuildInputs = [
29+
(python3Packages.python.withPackages
30+
(pythonPackages: [ pythonPackages.jinja2 ])
31+
)
32+
];
33+
34+
meta = {
35+
description = "Litani metabuild system";
36+
homepage = "https://awslabs.github.io/aws-build-accumulator/";
37+
};
38+
}

0 commit comments

Comments
 (0)