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
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
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
'';
}
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...