| { inputs, self, ... }: | |
| { | |
| imports = [ inputs.devshell.flakeModule ]; | |
| perSystem = | |
| { | |
| pkgs, | |
| config, | |
| system, | |
| ... | |
| }: | |
| let | |
| # cbmc is in nixpkgs; jbmc + kani are built from source by nix/tools.nix. | |
| toolsPkgs = pkgs.extend self.overlays.tools; | |
| in | |
| { | |
| devshells.default = { | |
| name = "AProver devshell"; | |
| packages = builtins.attrValues { | |
| # The project is a uv-managed Python package; uv provisions the | |
| # interpreter and every dependency from pyproject.toml / uv.lock, so we | |
| # deliberately do NOT pin python3 here. | |
| inherit (pkgs) | |
| uv | |
| ; | |
| # Verification oracles + compiler toolchain the pipeline shells out to. | |
| # cbmc — REQUIRED: C bounded model checker (bmc_agent/cbmc.py) | |
| # gcc — dynamic validation, reproducer loop, and the `cc` | |
| # preprocessor (the gcc wrapper also provides `cc`) | |
| inherit (pkgs) | |
| cbmc | |
| gcc | |
| binutils | |
| pkg-config | |
| ; | |
| # jbmc — Java bounded model checker (bmc_agent/jbmc.py) | |
| # kani — Rust bounded model checker (bmc_agent/kani.py) | |
| # Both are built from source by nix/tools.nix (nixpkgs ships neither in | |
| # a usable form). See overlays.tools. | |
| inherit (toolsPkgs) | |
| jbmc | |
| kani | |
| ; | |
| # jdk — `javac`/`java` for the JBMC backend's compile step | |
| # (bmc_agent/config.py:javac_path / java_classpath). | |
| inherit (pkgs) | |
| jdk | |
| ; | |
| # General CLI tooling. | |
| inherit (pkgs) | |
| git | |
| ripgrep | |
| gnumake | |
| coreutils | |
| bash | |
| ; | |
| # Optional deductive-verification path, used only with `--oracle frama-c`. | |
| # frama-c -wp-detect picks up the SMT prover (z3) on PATH. alt-ergo is | |
| # intentionally omitted — it is unfree in nixpkgs (ocamlpro_nc license). | |
| inherit (pkgs) | |
| frama-c | |
| z3 | |
| ; | |
| # Dev tooling. | |
| inherit (inputs.nix-fast-build.packages.${system}) nix-fast-build; | |
| treefmt = config.treefmt.build.wrapper; | |
| }; | |
| commands = [ | |
| { | |
| name = "aprover-verify"; | |
| help = "Run autonomous verification on a source dir"; | |
| command = "exec uv run bmc-agent autonomous \"$@\""; | |
| } | |
| ]; | |
| }; | |
| }; | |
| } | |