https://github.com/EasyCrypt/easycrypt
Tip revision: 69c9c2e226e29abd4e169d8439b83c6c0aa6aef6 authored by Benjamin Gregoire on 11 November 2022, 08:06:12 UTC
add few lemmas on dfun
add few lemmas on dfun
Tip revision: 69c9c2e
IterProc.eca
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 ->> /= - {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.
declare 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.
lemma iter_inv_HL (O<:Orcl) (P:t -> bool) (Inv: glob O -> bool):
hoare [ O.f :
P x /\ Inv (glob O) ==>
Inv (glob O) ] =>
hoare [ Iter(O).iter :
(forall x, mem l x => P x) /\ Inv (glob O) ==>
Inv (glob O) ].
proof.
move=> Hf;proc.
while ((forall x, mem l x => P x) /\ Inv (glob O));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.