https://github.com/EasyCrypt/easycrypt
Tip revision: 846710a2a656834065e745d19416ebdc83158f55 authored by Benjamin Gregoire on 14 July 2019, 06:50:07 UTC
Start restructuration of the code to be able to avant mutual dependency between type and mpath
Start restructuration of the code to be able to avant mutual dependency between type and mpath
Tip revision: 846710a
IterProc.eca
(* --------------------------------------------------------------------
* Copyright (c) - 2012--2016 - IMDEA Software Institute
* Copyright (c) - 2012--2018 - Inria
* Copyright (c) - 2012--2018 - Ecole Polytechnique
*
* Distributed under the terms of the CeCILL-B-V1 license
* -------------------------------------------------------------------- *)
pragma -oldip.
require import Core List.
type t.
module type Orcl = {
proc f (x : t) : unit
}.
module Iter (O:Orcl) = {
proc iter(l : t list) = {
while (l <> []) {
O.f(head witness l);
l <- drop 1 l;
}
}
proc iters(l1 l2 : t list) = {
iter(l1);
iter(l2);
}
proc iter_1s(t:t, l:t list) = {
O.f(t);
iter(l);
}
proc iter_12(t1 t2 : t) = {
O.f(t1);
O.f(t2);
}
proc iter_21(t1 t2 : t) = {
O.f(t2);
O.f(t1);
}
}.
lemma iter_ll (O <: Orcl): islossless O.f => islossless Iter(O).iter.
proof.
move=> O_ll; proc; inline Iter(O).iter.
while true (size l); auto=> /=.
+ call O_ll; skip=> /= ? [#] Hl <-.
smt w=(size_eq0 size_ge0 size_drop).
smt w=(size_eq0 size_ge0).
qed.
lemma iters_ll (O <: Orcl): islossless O.f => islossless Iter(O).iters.
proof. by move=> f_ll;proc;do 2!call (iter_ll O f_ll). qed.
lemma iter_1s_ll (O <: Orcl): islossless O.f => islossless Iter(O).iter_1s.
proof. by move=> f_ll;proc;call (iter_ll O f_ll);call f_ll. qed.
equiv iter_cat (O <: Orcl):
Iter(O).iter ~ Iter(O).iters:
={glob O} /\ l{1} = (l1++l2){2} ==> ={glob O}.
proof.
proc=> /=; inline Iter(O).iter.
exists* l2{2}; elim*=> _l2.
splitwhile{1} 1: l <> _l2.
while (={glob O} /\ l{1} = l0{2}).
+ by auto; call (_: true).
wp; while (={glob O} /\ l{1} = l{2}++_l2).
+ auto; call (_: true); auto.
move=> ? &ml [#] 2!->; case: (l{ml})=> //= x l'.
rewrite !drop0=> /= _ Ol Or ->> /= - {Ol Or}; split=> [[] _|].
+ by apply/contraLR=> /= ->.
rewrite -size_eq0=> size_l'.
by split; rewrite -negP=> /(congr1 size); rewrite size_cat [smt(size_ge0)].
auto=> /> &2; split=> [_|].
+ by apply/contraLR=> /= ->.
rewrite -size_eq0=> size_l1.
by split; rewrite -negP=> /(congr1 size); rewrite size_cat [smt(size_ge0)].
qed.
equiv iter_cat_cat (O <: Orcl):
Iter(O).iters ~ Iter(O).iters:
={glob O} /\ (l1++l2){1} = (l1++l2){2} ==> ={glob O}.
proof.
transitivity Iter(O).iter
(={glob O} /\ (l1++l2){1} = l{2} ==> ={glob O})
(={glob O} /\ l{1} = (l1++l2){2} ==> ={glob O})=> [/#|//||].
+ by symmetry; conseq (iter_cat O).
by apply (iter_cat O).
qed.
equiv iter_12_eq (O <: Orcl): Iter(O).iter_12 ~ Iter(O).iter:
={glob O} /\ l{2} = [t1;t2]{1} ==> ={glob O}.
proof.
proc=> /=.
rcondt{2} 1; 1: by auto.
rcondt{2} 3; 1: by auto; call (_: true); auto.
rcondf{2} 5; 1: by do !(auto; call (_: true)); auto.
by do !(auto; call (_: true)); auto.
qed.
lemma iter_21_eq (O <: Orcl):
equiv [Iter(O).iter_21 ~ Iter(O).iter:
={glob O} /\ l{2} = [t2;t1]{1} ==> ={glob O}].
proof.
proc=> /=.
rcondt{2} 1; 1: by auto.
rcondt{2} 3; 1: by auto; call (_: true); auto.
rcondf{2} 5; 1: by do !(auto; call (_: true)); auto.
by do !(auto; call (_: true)); auto.
qed.
section.
declare module O:Orcl.
axiom iter2_eq:
equiv [Iter(O).iter_12 ~ Iter(O).iter_21:
={glob O,t1,t2} ==> ={glob O}].
lemma iter_swap s1 i s2:
equiv [Iter(O).iter ~ Iter(O).iter :
l{1} = i::s1++s2 /\ l{2} = s1++i::s2 /\ ={glob O} ==> ={glob O}].
proof.
elim: s1=> /= [|i' s1 Hrec]; 1:by sim.
transitivity Iter(O).iters
(={glob O} /\ l{1} = i::i'::(s1++s2) /\ l1{2} = [i;i'] /\ l2{2} = s1++s2 ==>
={glob O})
(={glob O} /\ l1{1} = [i;i'] /\ l2{1} = s1 ++ s2 /\ l{2} = i'::(s1++i::s2) ==>
={glob O})=> //.
+ by move=> /> &2; exists ((glob O){2}) ([i;i'],s1++s2).
+ by conseq (iter_cat O)=> ? &ml [#] 4!->.
transitivity Iter(O).iters
(={glob O,l2} /\ l1{1} = [i;i'] /\ l1{2} = [i';i] /\ l2{1} = s1++s2 ==>
={glob O})
(={glob O} /\ l1{1} = [i';i] /\ l2{1} = s1 ++ s2 /\ l{2} = i'::(s1++i::s2) ==>
={glob O})=> //.
+ by move=> /> &1 &2 _ ->; exists ((glob O){2}) ([i'; i],s1++s2).
+ proc; call (_: ={glob O}).
* by while (={glob O,l}); auto; call (_: true).
conseq (_: ={glob O} /\ l1{1} = [i;i'] /\ l1{2} = [i';i] ==> ={glob O})=> //.
transitivity{1} {Iter(O).iter_12(i,i');}
(l1{1} = [i;i'] /\ ={glob O,l1} ==> ={glob O})
(l1{1} = [i;i'] /\ l1{2} = [i';i] /\ ={glob O} ==> ={glob O})=> [/#|//||].
+ by symmetry; call (iter_12_eq O).
transitivity{1} {Iter(O).iter_21(i,i');}
(l1{1} = [i;i'] /\ l1{2} =[i';i] /\ ={glob O} ==> ={glob O})
(l1{1} = [i';i] /\ ={glob O,l1} ==> ={glob O})=> [/#|//||].
+ by wp; call iter2_eq.
by call (iter_21_eq O).
transitivity Iter(O).iters
(={glob O} /\ l1{1} = [i';i] /\ l2{1} = s1++s2 /\ l1{2} = [i'] /\ l2{2} = i::(s1++s2) ==>
={glob O})
(={glob O} /\ l1{1} = [i'] /\ l2{1} = i::s1++s2 /\ l{2} = i'::(s1++i::s2) ==>
={glob O})=> //.
+ by move=> /> &1 &2 _ _; exists ((glob O){2}) ([i'],i::(s1++s2)).
+ by conseq (iter_cat_cat O)=> ? &ml [#] 5!->.
transitivity Iter(O).iters
(={glob O,l1} /\ l1{1} = [i'] /\ l2{1} = i::s1++s2 /\ l2{2} = s1++i::s2 ==>
={glob O})
(={glob O} /\ l1{1} = [i'] /\ l2{1} = s1++i::s2 /\ l{2} = i'::s1++i::s2 ==>
={glob O})=> //.
+ by move=> /> &1 &2 -> _; exists ((glob O){2}) ([i'],s1++i::s2).
+ proc; call Hrec; call (_: ={glob O})=> //.
by while (={glob O, l}); auto; call (_: true).
by symmetry; conseq (iter_cat O)=> // ? &ml [#] 4!->.
qed.
lemma iter_perm :
equiv [Iter(O).iter ~ Iter(O).iter : perm_eq l{1} l{2} /\ ={glob O} ==> ={glob O}].
proof.
exists*l{1}, l{2}; elim*=>l1 l2; case (perm_eq l1 l2)=> Hp; last first.
+ conseq (_: false ==> _)=> // ?? [#] //.
elim: l1 l2 Hp=> [|i s1 ih] s2 eq_s12 /=.
+ have ->: s2 = [] by apply/perm_eq_small/perm_eq_sym.
by proc; rcondf{1} 1=> //; rcondf{2} 1=> //.
have/perm_eq_mem /(_ i):= eq_s12; rewrite mem_head /=.
move/splitPr => [s3 s4] ->>.
transitivity Iter(O).iter
(l{1}=i::s1 /\ l{2}=i::(s3++s4) /\ ={glob O} ==> ={glob O})
(l{1}=i::(s3++s4) /\ l{2}=s3++i::s4 /\ ={glob O} ==> ={glob O})=>//.
+ by move=> ? &mr [#] 2!-> _ ->; exists (glob O){mr} (i :: (s3 ++ s4)).
+ proc; rcondt{1} 1=> //; rcondt{2}1=> //.
seq 2 2: (s1 = l{1} /\ l{2}=s3++s4 /\ ={glob O}).
+ by wp; call (_: true); auto; progress; rewrite drop0.
transitivity{1} {Iter(O).iter(l);}
(={l,glob O} ==> ={glob O})
(s1 = l{1} /\ l{2} = s3 ++ s4 /\ ={glob O} ==> ={glob O})=> //.
+ by move=> &1 &mr [#] 3!->; exists (glob O){mr} l{1}.
+ by inline Iter(O).iter; sim.
transitivity{1} {Iter(O).iter(l);}
(s1 = l{1} /\ l{2} = s3 ++ s4 /\ ={glob O} ==> ={glob O})
(={l,glob O} ==> ={glob O})=> //.
+ by move=> ? &mr [#] 3!->; exists (glob O){mr} (s3++s4).
+ move: eq_s12; rewrite -(cat1s i s4) catA perm_eq_sym.
rewrite perm_catCA /= perm_cons perm_eq_sym=> Hp.
by call (ih (s3++s4) Hp).
by inline Iter(O).iter; sim.
by apply/(iter_swap s3 i s4). (* FIXME: apply iter_swap fail! *)
qed.
lemma iters_perm:
equiv [Iter(O).iters ~ Iter(O).iter :
perm_eq (l1{1}++l2{1}) l{2} /\ ={glob O} ==> ={glob O}].
proof.
transitivity Iter(O).iter
(l{2} = l1{1}++l2{1} /\ ={glob O} ==> ={glob O})
(perm_eq l{1} l{2} /\ ={glob O} ==> ={glob O})=>//.
+ by move=> &ml&mr[??]; exists (glob O){mr} (l1{ml} ++ l2{ml}).
+ by symmetry;conseq (iter_cat O).
by apply iter_perm.
qed.
lemma iter1_perm:
equiv [Iter(O).iter_1s ~ Iter(O).iter :
perm_eq (t{1}::l{1}) l{2} /\ ={glob O} ==> ={glob O}].
proof.
transitivity Iter(O).iter
(l{2} = t{1}::l{1} /\ ={glob O} ==> ={glob O})
(perm_eq l{1} l{2} /\ ={glob O} ==> ={glob O})=>//.
+ by move=> &ml&mr[??]; exists (glob O){mr} (t{ml}::l{ml}).
+ proc;rcondt{2}1;1:by auto.
by inline*;sim;wp;call (_:true);skip;progress;rewrite drop0.
by apply iter_perm.
qed.
end section.
lemma iter_inv (O<:Orcl) (P:t -> bool) (Inv: glob O -> glob O -> bool):
equiv [ O.f ~ O.f:
={x} /\ P x{1} /\ Inv (glob O){1} (glob O){2} ==>
Inv (glob O){1} (glob O){2} ] =>
equiv [ Iter(O).iter ~ Iter(O).iter :
={l} /\ (forall x, mem l{1} x => P x) /\ Inv (glob O){1} (glob O){2} ==>
Inv (glob O){1} (glob O){2} ].
proof.
move=> Hf;proc.
while (={l} /\ (forall x, mem l{1} x => P x) /\ Inv (glob O){1} (glob O){2});auto.
call Hf;auto=> ??[#]-> HP HI Hl _ /=;split.
+ by rewrite HI HP // <@ Hl=>/head_behead /(_ witness) {1}<-.
by move=>_ ??->/= x Hx;apply/HP/(mem_drop 1).
qed.