/ flake.nix
flake.nix
1 { 2 description = "Aura - Threshold Identity and Storage Platform"; 3 4 inputs = { 5 nixpkgs.url = "github:NixOS/nixpkgs/nixos-unstable"; 6 flake-utils.url = "github:numtide/flake-utils"; 7 rust-overlay = { 8 url = "github:oxalica/rust-overlay"; 9 inputs.nixpkgs.follows = "nixpkgs"; 10 }; 11 crate2nix = { 12 url = "github:timewave-computer/crate2nix"; 13 inputs.nixpkgs.follows = "nixpkgs"; 14 }; 15 # Aeneas: Rust-to-Lean/Coq/F*/HOL4 verification toolchain 16 aeneas = { 17 url = "github:AeneasVerif/aeneas"; 18 # Don't follow nixpkgs - Aeneas has specific OCaml/Coq version requirements 19 }; 20 }; 21 22 outputs = 23 { 24 self, 25 nixpkgs, 26 flake-utils, 27 rust-overlay, 28 crate2nix, 29 aeneas, 30 }: 31 flake-utils.lib.eachDefaultSystem ( 32 system: 33 let 34 overlays = [ (import rust-overlay) ]; 35 pkgs = import nixpkgs { 36 inherit system overlays; 37 }; 38 39 rustToolchain = pkgs.rust-bin.stable.latest.default.override { 40 extensions = [ 41 "rust-src" 42 "rust-analyzer" 43 ]; 44 targets = [ "wasm32-unknown-unknown" ]; 45 }; 46 47 rustToolchainNightly = pkgs.rust-bin.nightly.latest.default.override { 48 extensions = [ 49 "rust-src" 50 "rust-analyzer" 51 ]; 52 targets = [ "wasm32-unknown-unknown" ]; 53 }; 54 55 # Apalache package from pre-built release 56 apalache = pkgs.stdenv.mkDerivation rec { 57 pname = "apalache"; 58 version = "0.45.4"; 59 60 src = pkgs.fetchurl { 61 url = "https://github.com/apalache-mc/apalache/releases/download/v${version}/apalache-${version}.tgz"; 62 sha256 = "sha256-neJbVEIAqOrfuP/4DR2MEhLJdnthxNx4KVoCyoGVdQ4="; 63 }; 64 65 nativeBuildInputs = with pkgs; [ makeWrapper ]; 66 buildInputs = with pkgs; [ jre ]; 67 68 installPhase = '' 69 runHook preInstall 70 mkdir -p $out/bin 71 72 # Copy the entire apalache directory 73 cp -r . $out/lib-apalache 74 75 # Make the apalache-mc script executable 76 chmod +x $out/lib-apalache/bin/apalache-mc 77 78 # Create wrapper script 79 makeWrapper $out/lib-apalache/bin/apalache-mc $out/bin/apalache-mc \ 80 --set JAVA_HOME ${pkgs.jre} \ 81 --prefix PATH : ${pkgs.jre}/bin 82 83 runHook postInstall 84 ''; 85 86 meta = with pkgs.lib; { 87 description = "Symbolic model checker for TLA+ specifications"; 88 homepage = "https://apalache-mc.github.io/apalache/"; 89 license = licenses.asl20; 90 platforms = platforms.unix; 91 }; 92 }; 93 94 # Import generated Cargo.nix with CC crate fix and other overrides 95 cargoNix = import ./Cargo.nix { 96 inherit pkgs; 97 buildRustCrateForPkgs = pkgs: pkgs.buildRustCrate; 98 # Apply CC crate fix for macOS builds and other common overrides 99 defaultCrateOverrides = pkgs.defaultCrateOverrides // { 100 # Override for cc crate - fix Apple target detection on macOS 101 cc = 102 attrs: 103 pkgs.lib.optionalAttrs pkgs.stdenv.isDarwin { 104 # Fix CC crate Apple target detection: it expects "darwin" but Nix reports "macos" 105 preBuild = '' 106 export CARGO_CFG_TARGET_OS="darwin" 107 ''; 108 } 109 // attrs; 110 111 # Override for ring (crypto library) 112 ring = attrs: { 113 nativeBuildInputs = [ pkgs.perl ]; 114 # Ensure consistent deployment target to avoid CC crate issues 115 MACOSX_DEPLOYMENT_TARGET = "11.0"; 116 # Set explicit Rust target for CC crate compatibility 117 TARGET_OS = "darwin"; 118 CARGO_CFG_TARGET_OS = "darwin"; 119 # Override Rust target detection 120 preBuild = '' 121 export TARGET_OS="darwin" 122 export CARGO_CFG_TARGET_OS="darwin" 123 # Ensure cargo sees darwin target 124 export RUST_TARGET_PATH=${pkgs.stdenv.targetPlatform.config} 125 ''; 126 }; 127 }; 128 }; 129 in 130 { 131 packages = { 132 # Main CLI application (terminal interface) 133 default = cargoNix.workspaceMembers.aura-terminal.build; 134 aura-terminal = cargoNix.workspaceMembers.aura-terminal.build; 135 136 # Terminal with development features (demo mode, simulator integration) 137 aura-terminal-dev = cargoNix.workspaceMembers.aura-terminal.build.override { 138 features = [ "development" ]; 139 }; 140 141 # Core applications 142 aura-agent = cargoNix.workspaceMembers.aura-agent.build; 143 aura-simulator = cargoNix.workspaceMembers.aura-simulator.build; 144 145 # Development tools 146 regenerate-cargo-nix = pkgs.writeScriptBin "regenerate-cargo-nix" '' 147 #!${pkgs.bash}/bin/bash 148 echo "Regenerating Cargo.nix with crate2nix..." 149 ${crate2nix.packages.${system}.default}/bin/crate2nix generate 150 echo "Cargo.nix regenerated successfully!" 151 ''; 152 }; 153 154 checks = { 155 # Run tests for key crates 156 # Note: aura-protocol-tests disabled due to circular dev-dependency with aura-testkit 157 # Tests still run via `cargo test` - hermetic checks are optional 158 aura-core-tests = cargoNix.workspaceMembers.aura-core.build.override { 159 runTests = true; 160 }; 161 }; 162 163 devShells.default = pkgs.mkShell { 164 buildInputs = with pkgs; [ 165 # Rust toolchain 166 rustToolchain 167 cargo-watch 168 cargo-edit 169 cargo-audit 170 171 # WASM tools 172 wasm-pack 173 wasm-bindgen-cli 174 trunk 175 176 # Build tools 177 pkg-config 178 openssl 179 180 # Task runner 181 just 182 183 # Documentation 184 mdbook 185 mdbook-mermaid 186 mdbook-katex 187 188 # Development tools 189 git 190 jq 191 ripgrep 192 193 # POSIX tools (for Justfile scripts) 194 coreutils 195 findutils 196 gawk 197 gnused 198 199 # Formal verification and protocol modeling 200 quint 201 apalache 202 tlaplus # TLA+ tools from nixpkgs 203 nodejs_20 204 jre # For ANTLR4TS and Apalache 205 lean4 # Lean 4 for kernel verification 206 aeneas.packages.${system}.aeneas # Rust-to-Lean translator 207 208 # Documentation tools 209 markdown-link-check 210 211 # Nix tools and formatting 212 nixpkgs-fmt 213 crate2nix.packages.${system}.default 214 ]; 215 216 shellHook = '' 217 if [ -z "$AURA_SUPPRESS_NIX_WELCOME" ]; then 218 echo "Aura Development Environment" 219 echo "============================" 220 echo "" 221 echo "Rust version: $(rustc --version)" 222 echo "Cargo version: $(cargo --version)" 223 echo "Quint version: $(quint --version 2>/dev/null || echo 'available')" 224 echo "Apalache version: $(apalache-mc version 2>/dev/null | head -1 || echo 'available')" 225 echo "TLA+ tools: $(tlc2 2>&1 | head -1 | grep -o 'Version.*' || echo 'available')" 226 echo "Node.js version: $(node --version)" 227 echo "Lean version: $(lean --version 2>/dev/null || echo 'available')" 228 echo "Aeneas version: $(aeneas --version 2>/dev/null || echo 'available')" 229 echo "" 230 echo "Available commands:" 231 echo " just --list Show all available tasks" 232 echo " just build Build all crates" 233 echo " just test Run all tests" 234 echo " just check Check workspace (cargo check)" 235 echo " just quint-parse Parse Quint files to JSON" 236 echo " just serve-console Serve console with hot reload (crates/console)" 237 echo " quint --help Formal verification with Quint" 238 echo " apalache-mc --help Model checking with Apalache" 239 echo " lean --help Kernel verification with Lean 4" 240 echo " aeneas --help Rust-to-Lean translation" 241 echo " crate2nix --help Generate hermetic Nix builds" 242 echo "" 243 echo "Hermetic builds:" 244 echo " nix build Build with crate2nix (hermetic)" 245 echo " nix build .#aura-terminal Build specific package" 246 echo " nix run Run aura CLI hermetically" 247 echo " nix flake check Run hermetic tests" 248 echo "" 249 fi 250 251 export RUST_BACKTRACE=1 252 export RUST_LOG=info 253 export MACOSX_DEPLOYMENT_TARGET=11.0 254 255 # Set AURA_PATH to the project directory for development. 256 # This ensures TUI data files (.aura/, .aura-demo/) are created in the 257 # project root rather than ~/.aura, making them visible and easy to 258 # inspect/delete during development. In production, AURA_PATH defaults 259 # to ~ (home directory). 260 export AURA_PATH="$PWD" 261 ''; 262 }; 263 264 devShells.nightly = pkgs.mkShell { 265 buildInputs = with pkgs; [ 266 # Nightly Rust toolchain (required for Kani) 267 rustToolchainNightly 268 cargo-udeps 269 270 # Essential development tools 271 just 272 git 273 ripgrep 274 jq 275 276 # Build tools 277 pkg-config 278 openssl 279 280 # POSIX tools (for Justfile scripts) 281 coreutils 282 findutils 283 gawk 284 gnused 285 286 # Kani dependencies 287 # Note: Kani itself must be installed via `cargo install --locked kani-verifier` 288 # and `cargo kani setup` because it requires specific nightly Rust components 289 # that aren't available in nixpkgs. Kani downloads its own CBMC during setup, 290 # so we only need z3 from nixpkgs. 291 z3 # SMT solver for Kani 292 ]; 293 294 shellHook = '' 295 echo "Aura Nightly Development Environment" 296 echo "=====================================" 297 echo "" 298 echo "Rust version: $(rustc --version)" 299 echo "Cargo version: $(cargo --version)" 300 echo "" 301 echo "Available commands:" 302 echo " cargo udeps Check for unused dependencies" 303 echo " just --list Show all available tasks" 304 echo "" 305 echo "Kani Setup (first time only):" 306 echo " cargo install --locked kani-verifier" 307 echo " cargo kani setup" 308 echo "" 309 echo "Kani Usage:" 310 echo " cargo kani Run Kani on current crate" 311 echo " cargo kani --harness <name> Run specific harness" 312 echo "" 313 export RUST_BACKTRACE=1 314 export RUST_LOG=info 315 export MACOSX_DEPLOYMENT_TARGET=11.0 316 317 # Set AURA_PATH to the project directory for development. 318 # See default devShell for full explanation. 319 export AURA_PATH="$PWD" 320 ''; 321 }; 322 } 323 ); 324 }