boogie: 2.15.7 -> 3.0.4

// RUN: %parallel-boogie "%s" > "%t"

// RUN: %diff "%s.expect" "%t"

type X;

function {:builtin "MapAdd"} mapadd([X]int, [X]int) : [X]int;

function {:builtin "MapSub"} mapsub([X]int, [X]int) : [X]int;

function {:builtin "MapMul"} mapmul([X]int, [X]int) : [X]int;

function {:builtin "MapDiv"} mapdiv([X]int, [X]int) : [X]int;

function {:builtin "MapMod"} mapmod([X]int, [X]int) : [X]int;

function {:builtin "MapConst"} mapconstint(int) : [X]int;

function {:builtin "MapConst"} mapconstbool(bool) : [X]bool;

function {:builtin "MapAnd"} mapand([X]bool, [X]bool) : [X]bool;

function {:builtin "MapOr"} mapor([X]bool, [X]bool) : [X]bool;

function {:builtin "MapNot"} mapnot([X]bool) : [X]bool;

function {:builtin "MapIte"} mapiteint([X]bool, [X]int, [X]int) : [X]int;

function {:builtin "MapIte"} mapitebool([X]bool, [X]bool, [X]bool) : [X]bool;

function {:builtin "MapLe"} maple([X]int, [X]int) : [X]bool;

function {:builtin "MapLt"} maplt([X]int, [X]int) : [X]bool;

function {:builtin "MapGe"} mapge([X]int, [X]int) : [X]bool;

function {:builtin "MapGt"} mapgt([X]int, [X]int) : [X]bool;

function {:builtin "MapEq"} mapeq([X]int, [X]int) : [X]bool;

function {:builtin "MapIff"} mapiff([X]bool, [X]bool) : [X]bool;

function {:builtin "MapImp"} mapimp([X]bool, [X]bool) : [X]bool;

const FF: [X]bool;

axiom FF == mapconstbool(false);

const TT: [X]bool;

axiom TT == mapconstbool(true);

const MultisetEmpty: [X]int;

axiom MultisetEmpty == mapconstint(0);

function {:inline} MultisetSingleton(x: X) : [X]int

{

  MultisetEmpty[x := 1]

}

function {:inline} MultisetPlus(a: [X]int, b: [X]int) : [X]int

{

  mapadd(a, b)

}

function {:inline} MultisetMinus(a: [X]int, b: [X]int)  : [X]int

{

  mapiteint(mapgt(a, b), mapsub(a, b), mapconstint(0))

}

procedure foo() {

  var x: X;

  assert FF != TT;

  assert mapnot(FF) == TT;

  assert MultisetSingleton(x) != MultisetEmpty;

  assert MultisetPlus(MultisetEmpty, MultisetSingleton(x)) == MultisetSingleton(x);

  assert MultisetMinus(MultisetPlus(MultisetEmpty, MultisetSingleton(x)), MultisetSingleton(x)) == MultisetEmpty;

  assert MultisetMinus(MultisetEmpty, MultisetSingleton(x)) == MultisetEmpty;

}

buildDotnetModule rec {

  pname = "Boogie";

  version = "2.15.7";

  version = "3.0.4";

  src = fetchFromGitHub {

    owner = "boogie-org";

    repo = "boogie";

    rev = "v${version}";

    sha256 = "16kdvkbx2zwj7m43cra12vhczbpj23wyrdnj0ygxf7np7c2aassp";

    sha256 = "sha256-yebThnIOpZ5crYsSZtbDj8Gn6DznTNJ4T/TsFR3gWvs=";

  };

  projectFile = [ "Source/Boogie.sln" ];

  nugetDeps = ./deps.nix;

  postInstall = ''

      mkdir -pv "$out/lib/dotnet/${pname}"

      ln -sv "${z3}/bin/z3" "$out/lib/dotnet/${pname}/z3.exe"

  executables = [ "BoogieDriver" ];

  makeWrapperArgs = [

    "--prefix PATH : ${z3}/bin"

  ];

  postInstall = ''

      # so that this derivation can be used as a vim plugin to install syntax highlighting

      vimdir=$out/share/vim-plugins/boogie

      install -Dt $vimdir/syntax/ Util/vim/syntax/boogie.vim

      rm -f $out/bin/{Microsoft,NUnit3,System}.* "$out/bin"/*Tests

  '';

  doInstallCheck = true;

  installCheckPhase = ''

    $out/bin/boogie ${./install-check-file.bpl}

  '';

  meta = with lib; {

    description = "An intermediate verification language";

    homepage = "https://github.com/boogie-org/boogie";