[Easycrypt-club] conseq

Alley Stoughton alley.stoughton at icloud.com
Tue Jan 30 19:57:24 CET 2018


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



More information about the Easycrypt-club mailing list