Reproducible builds for Verus with Nix

[JakeGinesin]

This PR adds a flake.nix to provide a fully reproducible development environment and build process for Verus, using nix develop and nix build.

We pin specific versions of rustc, z3 (4.12.5) and cvc5 (1.1.2) to match Verus requirements. vargo dependencies are derived from tools/vargo/Cargo.lock, and verus dependencies are pinned via cargoHash.

We also spoof rustup since vargo invokes rustup to verify toolchain version and execute commands. Since Nix provides the toolchain explicitly (without rustup), a Python shim is added that mocks rustup show (reporting the Nix-provided rustc version) and rustup run (passing commands through to system $PATH).

Pinging @stephen-huan here as he played a large part in authoring this PR :D

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[parno]

Generally looks sane to me, but I don't really speak nix. Maybe we should find someone who does to look it over.

[parno]

Should we remove this old hash?

[parno]

Cut this old comment?

[parno]

Why the custom command to format vstd? Usually we use vargo fmt to format all of the Verus + vstd code.

[stephen-huan]

I don't remember now why I went with this command (which I got from CONTRIBUTING.md; I agree it can safely be changed.

Suggested change

	find vstd -name \*.rs -print0 | xargs -0 -n1 verusfmt
	vargo fmt

[stephen-huan]

In line with #2054 (comment), could add this here.

Suggested change

	statix check
	statix check
	vargo fmt -- --check

[florianjacob]

Thank you for your work! As a Nix user, I can confirm this works.

With this PR, how would the process of updating the flake look like, to keep track of the current developments? Of course, every time the fixed-version dependencies are raised, one needs to manually adjust them here as well, which is probably fine. But how about the main verus cargo hash, does that need a manual update on every weekly release? Or can it be specified / overwritten somehow when using this flake?

This is the minimal flake I came up with to be able to use this branch of verus in a verification project:

# cf. https://github.com/stephen-huan/verus-flake/issues/1
# cf. https://github.com/verus-lang/verus/pull/2054
{
  description = "verus verification environment";

  inputs = {
    nixpkgs.url = "github:NixOS/nixpkgs/nixos-unstable";
    flake-utils.url = "github:numtide/flake-utils";
    # branch of verus including a flake
    # https://github.com/verus-lang/verus/pull/2054
    verus.url = "github:JakeGinesin/verus/flake";
  };

  outputs = { self, nixpkgs, flake-utils, verus, ... }@inputs:
    
    flake-utils.lib.eachDefaultSystem (system:
      let
        pkgs = import nixpkgs {
          inherit system;
        };

      in
      {
        devShells.default = pkgs.mkShell {
          
          packages = [
            # package default is just verus binary itself, without cargo etc
            # verus.packages.${system}.default
            verus.packages.${system}.verus
            verus.packages.${system}.rust-bin
            verus.packages.${system}.vargo
            verus.packages.${system}.verusfmt
            verus.packages.${system}.z3
          ];

        };
      }
    );
}

[JakeGinesin]

This new iteration of the flake makes the following changes:

• by default we now pull in the z3 and CVC5 binaries, as opposed to building z3 and CVC5 manually. To build manually, we may now pass in env variables Z3_SOURCE_BUILD=1 or CVC5_SOURCE_BUILD=1, which requires adding the --impure flag to nix build
• in the verus derivation we switch cargoHash for cargoLock (which only requires pinning one dependency, getopts-0.2.21.) This is primarily to ease maintenance burden, as otherwise cargoHash would need to be updated each time Verus's cargoLock is updated.

@florianjacob with these changes, only the verusfmt hash and the getopts-02.21 hash needs to be maintained. Of course if we update away from 1.1.2 of cvc5, 2.0.0 of cadical (a dependency of cvc5), or 4.12.5 of z3, those hashes will need updating as well. However, it's my understanding that those solver versions should remain fixed for the foreseeable future.

[JakeGinesin]

@florianjacob to answer your question on usage, your flake looks reasonable to me. Until this gets merged, my suggestion to stay up-to-date with the latest Verus changes is to create a fork of my Verus fork, set the upstream to the main Verus repo, and continually sync your fork with the main Verus repo whenever you want the most up-to-date changes. With my flake changes you'll most likely not need to update any of the hashes, but you might need to run nix flake update.

Also pinging @stephen-huan, who might have a better solution here.