FoldProc.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
* -------------------------------------------------------------------- *)
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.
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.