Skip to main content

Browse the archive

Revision 9e85ab18f02ff773df83e7bf925a8d15949e6f6b authored by Benjamin Gregoire on 06 December 2023, 17:00:18 UTC, committed by Pierre-Yves Strub on 07 December 2023, 10:21:48 UTC 
Add tactic `weakmem`
 
This tactic allows to weaken the memory of a phoare hypothesis
by adding new variables to it.

This tactic is needed in the while rule for phoare, when one
wants to apply the induction hypothesis & the memories are
not compatible. Currently, the convertibility check does not
enforce that memories are equal, but a to-come PR is going to
fix that point.
1 parent d248e73
Raw File
default.nix 
{ withProvers ? false, devDeps ? [] }:

with import <nixpkgs> {};

let provers =
  if withProvers then [
    alt-ergo
    cvc4
    cvc5
    z3
  ] else []; in

let why3-pin =
  why3.overrideAttrs (o : rec {
    version = "1.6.0";
    src = fetchurl {
      url = "https://why3.gitlabpages.inria.fr/releases/${o.pname}-${version}.tar.gz";
      sha256 = "sha256-hFvM6kHScaCtcHCc6Vezl9CR7BFbiKPoTEh7kj0ZJxw=";
    };
  });
in

stdenv.mkDerivation {
  pname = "easycrypt";
  version = "git";
  src = ./.;

  buildInputs = [ git ] ++ (with ocamlPackages; [
    ocaml
    findlib
    batteries
    camlp-streams
    dune_3
    dune-build-info
    dune-site
    inifiles
    menhir
    menhirLib
    yojson
    zarith
  ]);

  propagatedBuildInputs = [ why3-pin ]
    ++ devDeps
    ++ provers;

  installPhase = ''
    runHook preInstall
    dune install --prefix $out -p $pname
    runHook postInstall
  '';
}
back to top