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
ecPhlEager.mli
(* --------------------------------------------------------------------
* 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-C-V1 license
* -------------------------------------------------------------------- *)
(* -------------------------------------------------------------------- *)
open EcUtils
open EcParsetree
open EcFol
open EcCoreGoal.FApi
(* -------------------------------------------------------------------- *)
val t_eager_seq : codepos1 -> codepos1 -> form -> EcIdent.t -> backward
val t_eager_if : backward
val t_eager_while : EcIdent.t -> backward
val t_eager_fun_def : backward
val t_eager_fun_abs : EcFol.form -> EcIdent.t -> backward
val t_eager_call : form -> form -> backward
(* -------------------------------------------------------------------- *)
val process_seq : eager_info -> codepos1 pair -> pformula -> backward
val process_if : backward
val process_while : eager_info -> backward
val process_fun_def : backward
val process_fun_abs : eager_info -> pformula -> backward
val process_call : call_info gppterm -> backward
val process_eager : eager_info -> pformula -> backward
(* -------------------------------------------------------------------- *)
(* [eager-seq]
* (a) c1;S ~ S;c1' : P ==> ={R}
* (b) c2;S ~ S;c2' : ={R} ==> Q
* (c) c2' ~ c2' : ={R.2} ==> ={Q.2}
* (d) ={R} => ={Is}
* (e) compat S S' R Xs
* (h) S ~ S' : ={Is} ==> ={Xs}
* --------------------------------------------------
* c1;c2;S ~ S;c1';c2' : P ==> Q
*
* where compat S S' R Xs =
* forall modS modS', ={Xs{modS,modS'}} => ={R{modS,modS'}}
*
* [eager-if]
* (a) P => e{1} = e'{2}
* (b) S;c1 ~ S';c1' : P /\ e{1} ==> Q
* (c) S;c2 ~ S';c2' : P /\ !e{1} ==> Q
* (d) forall b &2, S : P /\ e = b ==> e = b
* --------------------------------------------------
* S;if e then c1 else c2
* ~ if e' then c1' else c2';S' : P ==> Q
*
* [eager-while]
*
* (a) ={I} => e{1} = e{2}
* (b) S;c ~ c';S' : ={I} /\ e{1} ==> ={I}
* (c) c' ~ c' : ={I.2} ==> ={I.2}
* (d) forall b &2, S : e = b ==> e = b
* (e) ={I} => ={Is}
* (f) compat S S' I Xs
* (h) S ~ S' : ={Is} ==> ={Xs}
* --------------------------------------------------
* S;while e do c ~ while e' do c';S'
* : ={I} ==> ={I,Xs} /\ !e{1}
*
* [eager-fun-def]
*
* (a) S and S' depend only of global
* (this should be an invariant of the typing)
* (b) S;f.body;result = f.res; ~ S';f'.body;result' = f'.res
* : P ==> Q{res{1}<- result, res{2} <- result'}
* --------------------------------------------------
* S, f ~ f', S' : P ==> Q
*
* [eager-fun-abs]
*
* S and S' depend only of global (hould be an invariant of the typing)
*
* (a) ={I} => e{1} = e{2}
* for each oracles o o':
* o and o' do not modify (glob A) (this is implied by (f))
* (b) S,o ~ o',S' : ={I,params} ==> ={I,res}
* (c) o'~ o' : ={I.2, o'.params} ==> ={I.2, res}
* (e) ={I} => ={Is}
* (f) compat S S' I Xs
* (h) S ~ S' : ={Is} ==> ={Xs}
* (i) glob A not in I (checked in EcPhlFun.equivF_abs_spec)
* (j) S, S' do not modify glob A
* --------------------------------------------------
* S, A.f{o} ~ A.f(o'), S'
* : ={I,glob A,A.f.params} ==> ={I,glob A,res}
*
* Remark : ={glob A} is not required in pre condition when A.f is an initializer
*
* [eager-call]
* S,f ~ f',S' : fpre ==> fpost
* S do not write a
* --------------------------------------------------
* S;x = f(a) ~ x' = f'(a');S' : wp_call fpre fpost post ==> post
*)