Packaging Kani Rust Verifier

My attempt is here.

It fails with

   Compiling kani-driver v0.50.0 (/build/source/kani-driver)
error: failed to run custom build command for `kani-compiler v0.50.0 (/build/source/kani-compiler)`

Caused by:
  process didn't exit successfully: `/build/source/target/release/build/kani-compiler-6b6e8907781a95f1/build-script-build` (exit status: 101)
  --- stderr
  thread 'main' panicked at kani-compiler/build.rs:25:47:
  called `Result::unwrap()` on an `Err` value: NotPresent

The relevant line in build.rs is

let rustup_home = env::var("RUSTUP_HOME").unwrap();

which aligns with the build instructions’ indication that cargo be installed via rustup.

Not sure how to deal with this in Nix’ sandboxed environment. How should I proceed?

[ There are also pre-compiled binaries for

  • x86_64-unknown-linux-gnu
  • x86_64-apple-darwin
  • aarch64-apple-darwin ]

You would need to set the environment variables so that it can find the dependencies. I attempted packaging it here.

But I do not think I managed to make it work since I eventually used rustup with HOME in /tmp.

1 Like

This gets me a bit further, but I grind to a halt on unresolved imports.

The unusual build procedure combined with my limited Nix packaging experience probably make this lie beyond my reach. On the one hand, I’d like to understand how to deal with this; on the other, I can’t really justify the time required.

How about using the pre-compiled binaries they provide?

Yeah, I think that is because it really requires items from a Nightly compiler, so the bootstrap hack is not sufficient.

You could use fenix to get it but that will not work in Nixpkgs.

Any progress on this?

FWIW, this seems to work to build kani with rust-overlay from oxalica/rust-overlay. But it still wants to be installed in ~/.kani with cbmc and friends, so it’s not usable.

      pkgs = nixpkgs.legacyPackages.${system}.extend (import rust-overlay);
      rustHome = pkgs.rust-bin.nightly."2024-07-01".default.override {
        extensions = ["rustc-dev" "rust-src" "llvm-tools" "rustfmt"];
      };
      rustPlatform = pkgs.makeRustPlatform {
        cargo = rustHome;
        rustc = rustHome;
      };
      kani = rustPlatform.buildRustPackage rec {
        pname = "kani";
        version = "kani-0.53.0";
        src = pkgs.fetchFromGitHub {
          owner = "model-checking";
          repo = pname;
          rev = version;
          hash = "sha256-z64RFTajojxvsFFmlu+HvyxdoeekoyxmR8v8Bih9GVU=";
        };
        cargoHash = "sha256-wQGkyzmpOpVWqPEqSf/RqjIVz7NA+cgY7kPTJE9SefQ=";
        env = {
          RUSTUP_HOME = "${rustHome}";
          RUSTUP_TOOLCHAIN = "..";
        };
      };

I’ve now got a mostly working derivation at nix-tools/kani/default.nix at main · gleachkr/nix-tools · GitHub. It still needs a wrapper script pointing KANI_HOME at the included $out/lib, and the binaries in $out/lib may need a little more patching to be completely pure. If anyone has any pointers on the binary patching, I’d love some advice.