[Easycrypt-club] Help for auto;smt.

Pierre-Yves Strub pierre-yves at strub.nu
Tue Jan 30 14:58:58 CET 2018


Hi,

You can start by replacing "auto; smt" with "auto". This will give you
the goal that you send to SMT and try to understand if this goal is ok
or not. Then, this is not because your goal is valid that SMT can
prove it. You may have to simplify it.

Best. Pierre-Yves.

2018-01-30 14:53 GMT+01:00 sarah chabane <sarah.chabane22 at gmail.com>:
> 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.
>
> _______________________________________________
> Easycrypt-club mailing list
> Easycrypt-club at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/easycrypt-club
>


More information about the Easycrypt-club mailing list