(* --------------------------------------------------------------------
 * Copyright (c) - 2012--2016 - IMDEA Software Institute
 * Copyright (c) - 2012--2021 - Inria
 * Copyright (c) - 2012--2021 - Ecole Polytechnique
 *
 * Distributed under the terms of the CeCILL-B-V1 license
 * -------------------------------------------------------------------- *)

require import Core List.
require (*--*) IterProc.

type in_t, state_t.

module type Orcl = {
  proc f (s : state_t, x : in_t) : state_t
}.

module Fold (O:Orcl) = {
  proc fold(s : state_t, l : in_t list) = {
    while (l <> []) {
      s <@ O.f(s,head witness l);
      l <- drop 1 l;
    }
    return s;
  }

  proc fold_12 (s : state_t, t1 : in_t, t2 : in_t) = {
    s <@ O.f(s,t1);
    s <@ O.f(s,t2);
    return s;
  }

  proc fold_21 (s : state_t, t1 : in_t, t2 : in_t) = {
    s <@ O.f(s,t2);
    s <@ O.f(s,t1);
    return s;
  }

}.

lemma fold_ll (O<:Orcl): islossless O.f => islossless Fold(O).fold.
proof.
move=> O_ll; proc; inline Fold(O).fold.
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.

section.
  declare module O <: Orcl.

  declare axiom fold_swap12:
    equiv [Fold(O).fold_12 ~ Fold(O).fold_21 : ={t1,t2,glob O,s} ==> ={glob O,res}].

  local clone import IterProc as IP with
    type t <- in_t.

  local module O' = {
    var s : state_t

    proc f (x : in_t): unit = {
      s <@ O.f(s,x);
    }
  }.

  local equiv Fold_Iter: Fold(O).fold ~ Iter(O').iter:
    ={glob O,l} /\ s{1} = O'.s{2} ==> ={glob O} /\ res{1} = O'.s{2}.
  proof.
  proc; while (={glob O,l} /\ s{1} = O'.s{2}); last by auto.
  by inline O'.f; wp; call (_: true); auto.
  qed.

  local equiv iter_swap1 :
    Iter(O').iter_12 ~ Iter(O').iter_21 :
            ={glob O', t1, t2} ==> ={glob O'}.
  proof.
  transitivity Fold(O).fold_12
    (={glob O,t1,t2} /\ s{2} = O'.s{1} ==> ={glob O} /\ res{2} = O'.s{1})
    (={glob O,t1,t2} /\ s{1} = O'.s{2} ==> ={glob O} /\ res{1} = O'.s{2})=> //.
  + by move=> /> &1 &2 <- <-; exists ((glob O){2}) (O'.s{2},t1{1},t2{1}).
  + by proc;inline *;sim.
  transitivity Fold(O).fold_21
    (={glob O,s,t1,t2} ==> ={glob O, res})
    (={glob O,t1,t2} /\ s{1} = O'.s{2} ==> ={glob O} /\ res{1} = O'.s{2})=> [/#|//||].
  + by conseq fold_swap12.
  by proc;inline *;sim.
  qed.

  equiv fold_perm : Fold(O).fold ~ Fold(O).fold :
    ={glob O,s} /\ perm_eq l{1} l{2} ==> ={glob O,res}.
  proof.
  transitivity Iter(O').iter
    (={glob O,l} /\ s{1} = O'.s{2} ==> ={glob O} /\ res{1} = O'.s{2})
    (={glob O} /\ O'.s{1} = s{2} /\ perm_eq l{1} l{2} ==>
     ={glob O} /\ O'.s{1} = res{2})=> [/#|//||].
  + by conseq Fold_Iter.
  transitivity Iter(O').iter
    (={glob O'} /\ perm_eq l{1} l{2} ==> ={glob O'})
    (={glob O,l} /\ O'.s{1} = s{2} ==> ={glob O} /\ O'.s{1} = res{2})=> [/#|//||].
  + by conseq (iter_perm O' _)=>//=; conseq iter_swap1.
  by symmetry; conseq Fold_Iter.
  qed.

end section.