ci: Use Kani with Nix

.github/workflows/push.yaml

@@ -127,9 +127,16 @@ jobs:
     name: Check Kani proofs
     runs-on: ubuntu-latest
     steps:
+      - uses: cachix/install-nix-action@v26
+        with:
+          nix_path: nixpkgs=channel:nixos-unstable
+      - uses: cachix/cachix-action@v14
+        with:
+          name: coliasgroup
+          authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}'
       - uses: actions/checkout@v4
       - name: Check Kani proofs
-        run: make -C hacking/kani/docker check
+        run: make check-kani-proofs
   deploy-docs:
     name: Deploy docs
     if: github.ref == format('refs/heads/{0}', github.event.repository.default_branch)

Makefile

@@ -122,6 +122,10 @@ witness-fast-tests:
 	$(nix_build) -A witnessFastTests --no-out-link
 	$(try_restore_terminal)
 
+.PHONY: check-kani-proofs
+check-kani-proofs:
+	$(run_in_nix_shell) "cargo kani -p sel4-bitfield-ops"
+
 .PHONY: everything-except-non-incremental
 everything-except-non-incremental:
 	$(nix_build) -A everythingExceptNonIncremental --no-out-link

crates/private/tests/root-task/verus/core/Cargo.toml

@@ -21,13 +21,13 @@ verify = true
 
 [dependencies.builtin]
 git = "https://github.com/coliasgroup/verus.git"
-tag = "keep/fdac1c3c52e639bf3e835802f63b4352"
+tag = "keep/c1d8b986315b1d7fcaa0bf63c2e0497f"
 
 [dependencies.builtin_macros]
 git = "https://github.com/coliasgroup/verus.git"
-tag = "keep/fdac1c3c52e639bf3e835802f63b4352"
+tag = "keep/c1d8b986315b1d7fcaa0bf63c2e0497f"
 
 [dependencies.vstd]
 git = "https://github.com/coliasgroup/verus.git"
-tag = "keep/fdac1c3c52e639bf3e835802f63b4352"
+tag = "keep/c1d8b986315b1d7fcaa0bf63c2e0497f"
 default-features = false

hacking/cargo-manifest-management/manifest-scope.nix

@@ -223,6 +223,6 @@ in rec {
 
   verusSource = {
     git = "https://github.com/coliasgroup/verus.git";
-    tag = mkKeepRef "fdac1c3c52e639bf3e835802f63b43520379b1a1"; # branch dev
+    tag = mkKeepRef "c1d8b986315b1d7fcaa0bf63c2e0497fbebab231"; # branch dev
   };
 }

hacking/nix/rust-utils/vendor-lockfile.nix

@@ -8,26 +8,21 @@
 , buildPackages
 , fetchurl
 , jq
+, toTOMLFile
 , defaultRustToolchain
 }:
 
 { rustToolchain ? defaultRustToolchain
-, lockfileContents ? null
+, lockfileValue ? if lockfileContents == null then null else builtins.fromTOML lockfileContents
+, lockfileContents ? if lockfile == null then null else builtins.readFile lockfile
 , lockfile ? null
 , fetchGitSubmodules ? false
 , extraMkCrateTarballURLFns ? {}
 } @ args:
 
-assert lockfileContents != null || lockfile != null;
+assert lockfileValue != null;
 
 let
-  lockfileContents =
-    if lockfile != null
-    then builtins.readFile lockfile
-    else args.lockfileContents;
-
-  lockfileValue = builtins.fromTOML lockfileContents;
-
   packages =
     # TODO enforce?
     # assert lockfileValue.version == 3;
@@ -213,8 +208,18 @@ let
       printf '{"files": {}, "package": null}' > "$out/.cargo-checksum.json"
     '';
 
-in {
-  lockfile = if lockfile != null then lockfile else builtins.toFile "Cargo.lock" lockfileContents;
-  inherit lockfileValue;
+in lib.fix (self: {
   configFragment = vendoredSources;
-}
+  inherit lockfileValue;
+  lockfile =
+    let
+      fname = "Cargo.lock";
+    in
+      if lockfile != null
+      then lockfile
+      else (
+        if lockfileContents != null
+        then builtins.toFile fname lockfileContents
+        else toTOMLFile fname lockfileValue
+      );
+})

hacking/nix/scope/default.nix

@@ -176,6 +176,8 @@ superCallPackage ../rust-utils {} self //
 
   capdl-tool = callBuildBuildPackage ./capdl-tool {};
 
+  kani = callBuildBuildPackage ./kani {};
+
   verus = callBuildBuildPackage ./verus {};
 
   dafny = callBuildBuildPackage ./dafny {};

hacking/nix/scope/kani/cbmc-viewer.nix

@@ -0,0 +1,33 @@
+#
+# Copyright 2024, Colias Group, LLC
+#
+# SPDX-License-Identifier: BSD-2-Clause
+#
+
+{ lib
+, buildPythonPackage
+, fetchFromGitHub
+, setuptools
+, jinja2
+, voluptuous
+}:
+
+buildPythonPackage rec {
+  pname = "cbmc-viewer";
+  version = "3.8";
+
+  format = "pyproject";
+
+  src = fetchFromGitHub {
+    owner = "model-checking";
+    repo = "cbmc-viewer";
+    rev = "viewer-3.8";
+    hash = "sha256-GIpinwjl/v6Dz5HyOsoPfM9fxG0poZ0HPsKLe9js9vM=";
+  };
+
+  propagatedBuildInputs = [
+    setuptools
+    jinja2
+    voluptuous
+  ];
+}