https://github.com/EasyCrypt/easycrypt
Revision 3f4a0bd5596888cd8d28b97687d477942187aa5f authored by Pierre-Yves Strub on 11 June 2022, 06:10:21 UTC, committed by Adrien Koutsos on 13 June 2022, 09:22:31 UTC
Loops' epilogs must now be deterministic and loop/calls-free.

This forbids the following unsoundness:

```
require import AllCore DBool.

module E = {
  var i,j : int
  proc foo () = {
    var c;
    i <- 0;
    j <- 0;
    c <- false;
    while (!c) {
      i <- i + 1;
      j <- j + 1;
      c <$ {0,1};
    }
    return i = j;
  }

  proc bar () = {
    var c;
    i <- 0;
    j <- 0;
    c <- false;
    while (!c) {
      i <- i + 1;
      c <$ {0,1};
    }
    c <- false;
    while (!c) {
      j <- j + 1;
      c <$ {0,1};
    }
    return i = j;
  }
}.

equiv bad : E.foo ~ E.bar : true ==> ={res}.
proof.
proc.
fission{1} 4!1 @1,2. by sim.
qed.
```

Fix #210
1 parent b9af81d
Raw File
Tip revision: 3f4a0bd5596888cd8d28b97687d477942187aa5f authored by Pierre-Yves Strub on 11 June 2022, 06:10:21 UTC
In loop fusion/fission, add more constraints on the epilog
Tip revision: 3f4a0bd
default.nix
with import <nixpkgs> {};

if !lib.versionAtLeast why3.version "1.4" then
  throw "please update your nixpkgs channel: nix-channel --update"
else
let why3_local =
  if !lib.versionAtLeast why3.version "1.5" then
  why3.overrideAttrs (o: rec {
    version = "1.5.0";
    src = fetchurl {
      url = "https://why3.gitlabpages.inria.fr/releases/${o.pname}-${version}.tar.gz";
      sha256 = "sha256:0qjh49pyqmg3xi09fn4lyzz23i6h18y9sgc8ayscvx3bwr3vcqhr";
    };
  })
  else why3
; in
let why3 = why3_local; in
  stdenv.mkDerivation {
    name = "easycrypt-1.0";
    src = ./.;
    buildInputs = [ why3 ] ++ (with ocamlPackages; [
      ocaml
      findlib
      batteries
      dune_2
      dune-build-info
      dune-site
      inifiles
      menhir
      menhirLib
      merlin
      yojson
      zarith
    ]);
    installFlags = [ "PREFIX=$(out)" ];
  }
back to top