[Easycrypt-club] conseq

Bas Spitters b.a.w.spitters at gmail.com
Tue Jan 30 22:09:12 CET 2018


Thanks Alley, Francois!

I now have a workaround by cut-and-paste of the pre and post
conditions of the lemma. It's not pretty, but it works. :-S

Here's the ticket:
https://www.easycrypt.info/trac/ticket/17363#ticket

Bas

On Tue, Jan 30, 2018 at 10:00 PM, Fran├žois Dupressoir
<fdupress at gmail.com> wrote:
> 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


More information about the Easycrypt-club mailing list