nix: Add Kani

Signed-off-by: Nick Spinale <nick@nickspinale.com>

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
+  ];
+}

hacking/nix/scope/kani/default.nix

@@ -0,0 +1,130 @@
+#
+# Copyright 2024, Colias Group, LLC
+#
+# SPDX-License-Identifier: BSD-2-Clause
+#
+
+{ lib, stdenv
+, callPackage
+, fetchFromGitHub
+, makeWrapper
+, python3
+, python3Packages
+, cbmc
+, kissat
+
+, crateUtils
+, vendorLockfile
+, sources
+, fenix
+, elaborateRustEnvironment
+, mkDefaultElaborateRustEnvironmentArgs
+, mkMkCustomTargetPathForEnvironment
+}:
+
+let
+  cbmc-viewer = python3Packages.callPackage ./cbmc-viewer.nix {};
+
+  rustToolchainAttrs = builtins.fromTOML (builtins.readFile (src + "/rust-toolchain.toml"));
+
+  rustToolchain = fenix.fromToolchainFile {
+    file = crateUtils.toTOMLFile "rust-toolchain.toml" (crateUtils.clobber [
+      rustToolchainAttrs
+      {
+        toolchain.components = rustToolchainAttrs.toolchain.components ++ [ "rust-src" ];
+      }
+    ]);
+    sha256 = "sha256-akRjdj8CP0mRL4czKC7GssksdunxdckSNiNU36zduV0=";
+  };
+
+  rustEnvironment = lib.fix (self: elaborateRustEnvironment (mkDefaultElaborateRustEnvironmentArgs {
+    inherit rustToolchain;
+  } // {
+    inherit (rustToolchainAttrs.toolchain) channel;
+    mkCustomTargetPath = mkMkCustomTargetPathForEnvironment {
+      rustEnvironment = self;
+    };
+  }));
+
+  src = fetchFromGitHub {
+    owner = "model-checking";
+    repo = "kani";
+    rev = "kani-0.52.0";
+    sha256 = "sha256-LyMZt6E1U03n4w5L9JMxgklAyvhltSJTvRl7zxYpw6A=";
+  };
+
+  localLockfile = vendorLockfile {
+    inherit rustToolchain;
+    lockfile = src + "/Cargo.lock";
+  };
+
+  sysrootLockfile = rustEnvironment.vendoredSysrootLockfile;
+
+  augmentedLockfileValue = {
+    version =
+      assert localLockfile.lockfileValue.version == sysrootLockfile.lockfileValue.version;
+      localLockfile.lockfileValue.version;
+    package = localLockfile.lockfileValue.package ++ sysrootLockfile.lockfileValue.package;
+  };
+
+  augmentedLockfile = vendorLockfile {
+    inherit rustToolchain;
+    lockfileValue = augmentedLockfileValue;
+  };
+
+  configFragment = crateUtils.toTOMLFile "config" augmentedLockfile.configFragment;
+
+  pythonEnv = python3.buildEnv.override {
+    extraLibs = [ cbmc-viewer ];
+  };
+
+in
+stdenv.mkDerivation {
+  name = "kani";
+
+  inherit src;
+
+  nativeBuildInputs = [
+    rustToolchain
+    makeWrapper
+    cbmc
+    kissat
+  ];
+
+  postPatch = ''
+    # HACK
+    substituteInPlace src/setup.rs \
+      --replace \
+        'Command::new("python3")' \
+        'Command::new("true")'
+  '';
+
+  configurePhase = ''
+    cat ${configFragment} >> .cargo/config.toml
+  '';
+
+  buildPhase = ''
+    RUSTUP_HOME=/var/empty/rustup \
+    RUSTUP_TOOLCHAIN=none \
+      cargo bundle
+  '';
+
+  installPhase = ''
+    install -D -t $out/bin target/kani/bin/{kani,cargo-kani}
+
+    for p in $out/bin/*; do
+      wrapProgram $p \
+        --set KANI_HOME $out/lib/kani \
+        --prefix PATH : ${lib.makeBinPath [ rustToolchain pythonEnv ]}
+    done
+
+    $out/bin/kani setup \
+      --use-local-bundle kani-*.tar.gz \
+      --use-local-toolchain ${rustToolchain}
+  '';
+
+  passthru = {
+    inherit rustEnvironment;
+    inherit cbmc-viewer;
+  };
+}

hacking/nix/scope/shell-for-hacking.nix

@@ -15,14 +15,15 @@
 , python3Packages
 , cmake
 
+, kani
+, verus
+
 , strace
 , cntr
 , cachix
 
 , openssl
 
-, verus
-
 , shellForMakefile
 }:
 
@@ -40,17 +41,22 @@ mkShell (shellForMakefile.apply {
     perl
     cmake
     rustPlatform.bindgenHook
+    kani
+    verus
     strace
     cntr
     cachix
-    verus
   ];
 
   buildInputs = [
     openssl
   ];
 
   shellHook = ''
+    kargo() {
+      cargo +${kani.rustEnvironment.channel} "$@"
+    }
+
     vargo() {
       cargo +${verus.rustEnvironment.channel} "$@"
     }

hacking/nix/scope/shell-for-makefile.nix

@@ -8,6 +8,7 @@
 , python3
 , reuse
 , cargo-audit
+, kani
 }:
 
 let
@@ -21,6 +22,7 @@ let
       python3
       reuse
       cargo-audit
+      kani
     ];
   };
 

hacking/nix/scope/verus/default.nix

@@ -92,6 +92,6 @@ stdenv.mkDerivation {
 
   passthru = {
     inherit rustEnvironment;
-    rustToolchainChannel = rustToolchainAttrs.toolchain.channel;
+    inherit z3;
   };
 }

hacking/nix/top-level/default.nix

@@ -62,6 +62,9 @@ in {
 
     sel4testInstancesList
 
+    pkgs.build.this.kani
+    pkgs.build.this.verus
+
     pkgs.host.aarch32.none.this.worlds.default.seL4
     pkgs.host.ia32.none.this.worlds.default.seL4