(* --------------------------------------------------------------------
 * 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 ->> /= - {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.