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
History
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
File Mode Size
phl
system
dune -rw-r--r-- 459 bytes
ec.ml -rw-r--r-- 14.0 KB
ecAlgTactic.ml -rw-r--r-- 8.2 KB
ecAlgTactic.mli -rw-r--r-- 1.2 KB
ecAlgebra.ml -rw-r--r-- 13.3 KB
ecAlgebra.mli -rw-r--r-- 4.5 KB
ecBaseLogic.ml -rw-r--r-- 1.2 KB
ecBaseLogic.mli -rw-r--r-- 1.1 KB
ecBigInt.ml -rw-r--r-- 4.8 KB
ecBigInt.mli -rw-r--r-- 34 bytes
ecBigIntCore.ml -rw-r--r-- 1.7 KB
ecCHoare.ml -rw-r--r-- 2.5 KB
ecCHoare.mli -rw-r--r-- 1.5 KB
ecCallbyValue.ml -rw-r--r-- 18.5 KB
ecCallbyValue.mli -rw-r--r-- 270 bytes
ecCommands.ml -rw-r--r-- 32.2 KB
ecCommands.mli -rw-r--r-- 1.6 KB
ecCoreFol.ml -rw-r--r-- 92.6 KB
ecCoreFol.mli -rw-r--r-- 22.8 KB
ecCoreGoal.ml -rw-r--r-- 36.1 KB
ecCoreGoal.mli -rw-r--r-- 16.4 KB
ecCoreHiPhl.ml -rw-r--r-- 2.2 KB
ecCoreHiPhl.mli -rw-r--r-- 629 bytes
ecCoreLib.ml -rw-r--r-- 8.2 KB
ecCoreLib.mli -rw-r--r-- 5.5 KB
ecCoreModules.ml -rw-r--r-- 27.8 KB
ecCoreModules.mli -rw-r--r-- 10.0 KB
ecDecl.ml -rw-r--r-- 10.6 KB
ecDecl.mli -rw-r--r-- 5.4 KB
ecEco.ml -rw-r--r-- 6.0 KB
ecEnv.ml -rw-r--r-- 119.9 KB
ecEnv.mli -rw-r--r-- 16.7 KB
ecField.ml -rw-r--r-- 5.6 KB
ecField.mli -rw-r--r-- 526 bytes
ecFol.ml -rw-r--r-- 42.5 KB
ecFol.mli -rw-r--r-- 7.3 KB
ecGState.ml -rw-r--r-- 4.0 KB
ecGState.mli -rw-r--r-- 1.6 KB
ecGenRegexp.ml -rw-r--r-- 10.1 KB
ecHiGoal.ml -rw-r--r-- 67.1 KB
ecHiGoal.mli -rw-r--r-- 4.1 KB
ecHiInductive.ml -rw-r--r-- 12.6 KB
ecHiInductive.mli -rw-r--r-- 1.8 KB
ecHiNotations.ml -rw-r--r-- 3.5 KB
ecHiNotations.mli -rw-r--r-- 666 bytes
ecHiPredicates.ml -rw-r--r-- 3.0 KB
ecHiPredicates.mli -rw-r--r-- 568 bytes
ecHiTacticals.ml -rw-r--r-- 14.5 KB
ecHiTacticals.mli -rw-r--r-- 327 bytes
ecIdent.ml -rw-r--r-- 1.7 KB
ecIdent.mli -rw-r--r-- 1.2 KB
ecInductive.ml -rw-r--r-- 10.6 KB
ecInductive.mli -rw-r--r-- 2.8 KB
ecIo.ml -rw-r--r-- 6.8 KB
ecIo.mli -rw-r--r-- 1023 bytes
ecLexer.mll -rw-r--r-- 18.5 KB
ecLoader.ml -rw-r--r-- 5.0 KB
ecLoader.mli -rw-r--r-- 836 bytes
ecLocation.ml -rw-r--r-- 2.8 KB
ecLocation.mli -rw-r--r-- 1.3 KB
ecLowGoal.ml -rw-r--r-- 85.0 KB
ecLowGoal.mli -rw-r--r-- 11.1 KB
ecLowPhlGoal.ml -rw-r--r-- 24.7 KB
ecMaps.ml -rw-r--r-- 4.9 KB
ecMatching.ml -rw-r--r-- 42.4 KB
ecMatching.mli -rw-r--r-- 6.1 KB
ecMemory.ml -rw-r--r-- 9.0 KB
ecMemory.mli -rw-r--r-- 2.6 KB
ecModules.ml -rw-r--r-- 3.8 KB
ecModules.mli -rw-r--r-- 2.9 KB
ecOptions.ml -rw-r--r-- 14.6 KB
ecOptions.mli -rw-r--r-- 1.5 KB
ecPException.ml -rw-r--r-- 1.3 KB
ecPException.mli -rw-r--r-- 227 bytes
ecPV.ml -rw-r--r-- 35.3 KB
ecPV.mli -rw-r--r-- 6.0 KB
ecParser.mly -rw-r--r-- 100.5 KB
ecParsetree.ml -rw-r--r-- 37.1 KB
ecPath.ml -rw-r--r-- 10.8 KB
ecPath.mli -rw-r--r-- 4.1 KB
ecPrinting.ml -rw-r--r-- 117.4 KB
ecPrinting.mli -rw-r--r-- 3.9 KB
ecProofTerm.ml -rw-r--r-- 36.2 KB
ecProofTerm.mli -rw-r--r-- 6.2 KB
ecProofTyping.ml -rw-r--r-- 6.0 KB
ecProofTyping.mli -rw-r--r-- 2.7 KB
ecProvers.ml -rw-r--r-- 14.9 KB
ecProvers.mli -rw-r--r-- 1.8 KB
ecReduction.ml -rw-r--r-- 79.4 KB
ecReduction.mli -rw-r--r-- 4.6 KB
ecRegexp.ml -rw-r--r-- 4.0 KB
ecRegexp.mli -rw-r--r-- 1.1 KB
ecRelocate.ml -rw-r--r-- 800 bytes
ecRelocate.mli -rw-r--r-- 84 bytes
ecRing.ml -rw-r--r-- 12.9 KB
ecRing.mli -rw-r--r-- 2.0 KB
ecScope.ml -rw-r--r-- 79.8 KB
ecScope.mli -rw-r--r-- 7.5 KB
ecSearch.ml -rw-r--r-- 3.7 KB
ecSearch.mli -rw-r--r-- 535 bytes
ecSection.ml -rw-r--r-- 52.7 KB
ecSection.mli -rw-r--r-- 1.3 KB
ecSmt.ml -rw-r--r-- 56.3 KB
ecSmt.mli -rw-r--r-- 898 bytes
ecStrongRing.ml -rw-r--r-- 10.4 KB
ecSubst.ml -rw-r--r-- 22.9 KB
ecSubst.mli -rw-r--r-- 2.8 KB
ecSymbols.ml -rw-r--r-- 2.4 KB
ecSymbols.mli -rw-r--r-- 1.2 KB
ecTerminal.ml -rw-r--r-- 8.7 KB
ecTerminal.mli -rw-r--r-- 834 bytes
ecThCloning.ml -rw-r--r-- 19.6 KB
ecThCloning.mli -rw-r--r-- 2.7 KB
ecTheory.ml -rw-r--r-- 3.4 KB
ecTheory.mli -rw-r--r-- 2.4 KB
ecTheoryReplay.ml -rw-r--r-- 38.1 KB
ecTheoryReplay.mli -rw-r--r-- 1.2 KB
ecTransMatching.ml -rw-r--r-- 3.8 KB
ecTransMatching.mli -rw-r--r-- 446 bytes
ecTypeClass.ml -rw-r--r-- 2.2 KB
ecTypeClass.mli -rw-r--r-- 485 bytes
ecTypes.ml -rw-r--r-- 34.6 KB
ecTypes.mli -rw-r--r-- 9.7 KB
ecTyping.ml -rw-r--r-- 135.5 KB
ecTyping.mli -rw-r--r-- 8.6 KB
ecUFind.ml -rw-r--r-- 5.2 KB
ecUFind.mli -rw-r--r-- 1.4 KB
ecUid.ml -rw-r--r-- 1.9 KB
ecUid.mli -rw-r--r-- 923 bytes
ecUnify.ml -rw-r--r-- 13.9 KB
ecUnify.mli -rw-r--r-- 1.6 KB
ecUserMessages.ml -rw-r--r-- 31.5 KB
ecUserMessages.mli -rw-r--r-- 2.3 KB
ecUtils.ml -rw-r--r-- 21.8 KB
ecUtils.mli -rw-r--r-- 11.6 KB
ecVersion.ml -rw-r--r-- 614 bytes
ecVersion.mli -rw-r--r-- 242 bytes
ecWhy3Conv.ml -rw-r--r-- 6.1 KB
ecWhy3Conv.mli -rw-r--r-- 289 bytes

back to top