[Easycrypt-club] conseq

François Dupressoir fdupress at gmail.com
Tue Jan 30 22:00:30 CET 2018


In other words: the lemmas you are attempting to use in conseq refer to
procedures, but your current goal refers to statements.

Maybe it would be useful to file a feature request that, in this case, the
lemmas be unrolled to statements before application (or the conseq modified
as illustrated by Alley)? Not sure how feasible it is in practice.

In any case a bug report on the horrendous error message will help in the
long run.

François

On Tue, 30 Jan 2018, 18:58 Alley Stoughton, <alley.stoughton at icloud.com>
wrote:

> Hi Bas,
>
> An explanation is below.
>
> Best,
>
> Alley
>
> - - - -
>
> require import AllCore.
>
> module M = {
>   proc f(x : int, y : int) : int * int = {
>     return (x - 1, y + 1);
>   }
> }.
>
> module N = {
>   proc f(x : int, y : int) : int * int = {
>     return (x + 1, y + 1);
>   }
> }.
>
> lemma M_N : equiv[M.f ~ N.f : ={y} ==> res{1}.`2 = res{2}.`2].
> proof. proc; auto. qed.
>
> lemma M : hoare[M.f : 1 < x ==> 0 < res.`1].
> proof. proc; auto; smt(). qed.
>
> lemma N : hoare[N.f : x < 1 ==> res.`1 < 2].
> proof. proc; auto; smt(). qed.
>
> lemma M_N_combined :
>   equiv[M.f ~ N.f :
>         ={y} /\ 1 < x{1} /\ x{2} < 1  ==>
>         res{1}.`2 = res{2}.`2 /\ 0 < res{1} .`1 /\ res{2}.`1 < 2].
> proof.
> proc.
> (* you can't do
>
> conseq M_N M N.
>
>   "do not how to combine equivF and hoareF and hoareF into equivS"
>
>  equivS refers to the statement form of an equiv, after the proc
>  has oppened it up
>
> instead:
> *)
> conseq (_ : ={y} ==> ={y})
>        (_ : 1 < x ==> 0 < x)
>        (_ : x < 1 ==> x < 2).
> smt.
> auto; smt.
> auto; smt.
> auto.
> qed.
>
> (* or: *)
>
> lemma M_N_combined' :
>   equiv[M.f ~ N.f :
>         ={y} /\ 1 < x{1} /\ x{2} < 1  ==>
>         res{1}.`2 = res{2}.`2 /\ 0 < res{1} .`1 /\ res{2}.`1 < 2].
> proof.
> conseq M_N M N.
> qed.
>
> > On Jan 30, 2018, at 12:49 PM, Bas Spitters <b.a.w.spitters at gmail.com>
> wrote:
> >
> > I am trying to use conseq in the form
> >
> > conseq M_N M N.
> >
> > p146 of the refman.
> >
> > I get an error message:
> > do not how to combine equivF and hoareS and hoareS into equivS
> >
> > What does that mean?
> >
> > Thanks,
> >
> > Bas
> > _______________________________________________
> > Easycrypt-club mailing list
> > Easycrypt-club at lists.gforge.inria.fr
> > https://lists.gforge.inria.fr/mailman/listinfo/easycrypt-club
>
> _______________________________________________
> Easycrypt-club mailing list
> Easycrypt-club at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/easycrypt-club
>
-------------- section suivante --------------
Une pièce jointe HTML a été nettoyée...
URL: <http://lists.gforge.inria.fr/pipermail/easycrypt-club/attachments/20180130/c8ab428c/attachment.html>


More information about the Easycrypt-club mailing list