https://github.com/EasyCrypt/easycrypt
Tip revision: 3f4a0bd5596888cd8d28b97687d477942187aa5f authored by Pierre-Yves Strub on 11 June 2022, 06:10:21 UTC
In loop fusion/fission, add more constraints on the epilog
In loop fusion/fission, add more constraints on the epilog
Tip revision: 3f4a0bd
ecCHoare.mli
open EcFol
open EcPath
open EcSymbols
(* -------------------------------------------------------------------- *)
val check_loaded : EcEnv.env -> unit
(* -------------------------------------------------------------------- *)
val cost_orcl : symbol -> xpath -> form -> form
(* -------------------------------------------------------------------- *)
type csub_res = { cond : form; res : form; }
(* Backward reasoning on cost.
Looks for a solution [x] of [c = x + sub]. *)
val cost_sub : c:form -> sub:form -> csub_res
(* Same as [cost_sub], but only for the concrete cost.
[c] of type [tcost], [sub] of type [xint]. *)
val cost_sub_self : c:form -> sub:form -> csub_res
(* -------------------------------------------------------------------- *)
(* [c] of type [tcost], [a] of type [xint] *)
val cost_add_self : c:form -> a:form -> form
(* -------------------------------------------------------------------- *)
(* [choare_xsum cost (m,n)]:
[cost] of type [tcost], [m] of type [tint], [n] of type [txint].
[n] must be finite, i.e. [n = f_N n_fin]. *)
val choare_xsum : form -> (form * form) -> form
(* -------------------------------------------------------------------- *)
val free_expr : EcTypes.expr -> bool
(* The cost of an expression evaluation in any memory of type [menv]
satisfying [pre].
Type [xint]. *)
val cost_of_expr : EcFol.form -> EcMemory.memenv -> EcTypes.expr -> EcFol.form
(* The cost of an expression evaluation in any memory of type [menv].
Type [xint]. *)
val cost_of_expr_any : EcMemory.memenv -> EcTypes.expr -> EcFol.form