vestigia

Detect where execution depends on secrets.
git clone git://git.ppad.tech/vestigia.git
Log | Files | Refs | README | LICENSE

default.nix (2647B)

      1 # Spike 2: ppad-poly1305 under vestigia, on x86_64-linux: the
      2 # release (173e478) and the elenchus vectors' two mutant sets.
      3 #
      4 #   nix build --impure -f etc/spike/poly1305 all
      5 let
      6   system = "x86_64-linux";
      7   vestigia = builtins.getFlake (toString ../../..);
      8   poly = builtins.getFlake ("git+file:///Users/jtobin/src/ppad/poly1305"
      9     + "?rev=173e478290ecf9d639f0c85ae625da474a62a6b2");
     10   pkgs = import vestigia.inputs.nixpkgs { inherit system; };
     11   hlib = pkgs.haskell.lib;
     12   llvm = pkgs.llvmPackages_19.llvm;
     13   clang = pkgs.llvmPackages_19.clang;
     14   withLlvm = p: hlib.addBuildTools (hlib.enableCabalFlag p "llvm")
     15     [ llvm clang ];
     16 
     17   variant = name: patches:
     18     let
     19       hpkgs = pkgs.haskell.packages.ghc910.extend (new: old: {
     20         ppad-base16 =
     21           withLlvm poly.inputs.ppad-base16.packages.${system}.default;
     22         ppad-fixed =
     23           withLlvm poly.inputs.ppad-fixed.packages.${system}.default;
     24         ppad-poly1305 = withLlvm (hlib.dontCheck (hlib.appendPatches
     25           (new.callCabal2nix "ppad-poly1305" poly.outPath { })
     26           patches));
     27       });
     28       ghc = hpkgs.ghcWithPackages (p: [ p.ppad-poly1305 ]);
     29       harness = pkgs.runCommandCC "poly1305-${name}-harness" {
     30         nativeBuildInputs = [ ghc llvm clang ];
     31       } ''
     32         mkdir -p $out/bin build
     33         cp ${./Harness.hs} build/Harness.hs
     34         cp ${vestigia.packages.${system}.include}/include/vestigia.c build/marks.c
     35         cd build
     36         # a small address-space reservation, since memcheck pays for
     37         # the runtime's default terabyte on every run, and no
     38         # interval timer, so runs that differ only in their keys
     39         # schedule alike
     40         ghc -O2 -rtsopts '-with-rtsopts=-xr1G -V0' Harness.hs marks.c \
     41           -I${vestigia.packages.${system}.include}/include \
     42           -I${vestigia.lib.${system}.valgrindDev}/include \
     43           -o $out/bin/harness
     44       '';
     45       bin = "${harness}/bin/harness";
     46       seeds = [ "1" "2" "3" ];
     47     in pkgs.linkFarm "poly1305-${name}" [
     48       { name = "trace";
     49         path = vestigia.lib.${system}.traceOf {
     50           name = "poly1305-${name}";
     51           harness = bin;
     52           runs = [ [ "4" "1" ] ];
     53         }; }
     54       { name = "diff";
     55         path = vestigia.lib.${system}.diffOf {
     56           name = "poly1305-${name}";
     57           harness = bin;
     58           runs = map (s: [ "2" s ]) seeds;
     59         }; }
     60     ];
     61 in
     62 {
     63   all = pkgs.linkFarm "poly1305-spike" [
     64     { name = "release"; path = variant "release" [ ]; }
     65     { name = "mutants-1"; path = variant "mutants-1" [ ./mutants-1.patch ]; }
     66     { name = "mutants-2"; path = variant "mutants-2" [ ./mutants-2.patch ]; }
     67   ];
     68 }