[Easycrypt-club] Help for auto;smt.

sarah chabane sarah.chabane22 at gmail.com
Tue Jan 30 14:53:28 CET 2018


Hi,

I am a beginner in easycrypt and i want to know why this proof does not
work , it stops in auto;smt.

I want to prove that each element in the set "set2" is not in the set
"set1".  in the next module , when I pick an element from "set1" i process
it and then i erase it from set1 and add it to set2.

the code is the following :

module TEST= {
    var set1 : int fset
    var set2 : int fset
    proc toto(M:int,L:int): int fset ={
    var i,j,k:int;
    set1 = FSet.fset0;
    set2 = FSet.fset0;
    i=0;
    set1 = FSet.fset1 i `|` set1;
    while (set1 <> fset0){
    i = pick set1;
    if (i=M) {i=i+1;  set1 = FSet.fset1 i `|` set1;}
    else i=i-1;
    set1 =  set1 `\` FSet.fset1 i;
    set2 = FSet.fset1 i `|` set2;
   }
  return set2;
}}.

lemma uniqueState :forall (i:int), hoare [TEST.toto:  mem TEST.set2 i ==>
!(mem TEST.set1 i)].

proof.
move =>s.
proc.
sp.
while (TEST.set1 <> fset0).
sp.
auto;smt.
auto.
auto;smt.
qed.



Best regards.
Sarah.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/easycrypt-club/attachments/20180130/3902802c/attachment.html>


More information about the Easycrypt-club mailing list