diff --git a/src/ecAst.mli b/src/ecAst.mli
index 61afbb830..db7a2a679 100644
--- a/src/ecAst.mli
+++ b/src/ecAst.mli
@@ -478,6 +478,7 @@ val pv_hash  : prog_var hash
 val pv_fv    : prog_var fv
 
 val pv_kind : prog_var -> pvar_kind
+
 (* -------------------------------------------------------------------- *)
 val idty_equal : (EcIdent.t * ty) equality
 val idty_hash  : (EcIdent.t * ty) hash
diff --git a/src/ecCoreFol.ml b/src/ecCoreFol.ml
index 54d61478c..f6cb18e13 100644
--- a/src/ecCoreFol.ml
+++ b/src/ecCoreFol.ml
@@ -562,6 +562,11 @@ let f_iter g f =
   | FeagerF   eg  -> g (eg_pr eg).inv; g (eg_po eg).inv
   | Fpr       pr  -> g pr.pr_args; g pr.pr_event.inv
 
+(* -------------------------------------------------------------------- *)
+let f_fold (tx : 'a -> form -> 'a) (state : 'a) (f : form) =
+  let state = ref state in
+  f_iter (fun f -> state := tx !state f) f;
+  !state
 
 (* -------------------------------------------------------------------- *)
 let form_exists g f =
diff --git a/src/ecCoreFol.mli b/src/ecCoreFol.mli
index 1f2afcb85..9c9c60367 100644
--- a/src/ecCoreFol.mli
+++ b/src/ecCoreFol.mli
@@ -76,6 +76,7 @@ val f_node  : form -> f_node
 (* not recursive *)
 val f_map  : (EcTypes.ty -> EcTypes.ty) -> (form -> form) -> form -> form
 val f_iter : (form -> unit) -> form -> unit
+val f_fold : ('a -> form -> 'a) -> 'a -> form -> 'a
 val form_exists: (form -> bool) -> form -> bool
 val form_forall: (form -> bool) -> form -> bool
 
diff --git a/src/ecEnv.ml b/src/ecEnv.ml
index edd45ca71..8a449a779 100644
--- a/src/ecEnv.ml
+++ b/src/ecEnv.ml
@@ -3569,30 +3569,40 @@ module LDecl = struct
   let fresh_id  hyps s = fresh_id  (tohyps hyps) s
   let fresh_ids hyps s = snd (fresh_ids (tohyps hyps) s)
 
+  (* ------------------------------------------------------------------ *)
+  let mapenv (f : env -> env) (lenv : hyps) =
+    { lenv with le_env = f lenv.le_env }
+
   (* ------------------------------------------------------------------ *)
   let push_active_ss m lenv =
-    { lenv with le_env = Memory.push_active_ss m lenv.le_env }
+    mapenv (Memory.push_active_ss m) lenv
 
   let push_active_ts ml mr lenv =
-    { lenv with le_env = Memory.push_active_ts ml mr lenv.le_env }
+    mapenv (Memory.push_active_ts ml mr) lenv
 
   let push_all l lenv =
-    { lenv with le_env = Memory.push_all l lenv.le_env }
+    mapenv (Memory.push_all l) lenv
+
+  let push_active_all l lenv =
+    let lenv = mapenv (Memory.push_all l) lenv in
+
+    match l with
+    | [(m, _)] -> mapenv (Memory.set_active_ss m) lenv
+    | _ -> lenv
 
   let hoareF mem xp lenv =
      let env1, env2 = Fun.hoareF mem xp lenv.le_env in
-    { lenv with le_env = env1}, {lenv with le_env = env2 }
+    { lenv with le_env = env1 }, { lenv with le_env = env2 }
 
   let equivF ml mr xp1 xp2 lenv =
     let env1, env2 = Fun.equivF ml mr xp1 xp2 lenv.le_env in
-    { lenv with le_env = env1}, {lenv with le_env = env2 }
+    { lenv with le_env = env1 }, { lenv with le_env = env2 }
 
   let inv_memenv ml mr lenv =
-    { lenv with le_env = Fun.inv_memenv ml mr lenv.le_env }
+    mapenv (Fun.inv_memenv ml mr) lenv
 
   let inv_memenv1 m lenv =
-    { lenv with le_env = Fun.inv_memenv1 m lenv.le_env }
+    mapenv (Fun.inv_memenv1 m) lenv
 end
 
-
 let pp_debug_form = ref (fun _env _f -> assert false)
diff --git a/src/ecEnv.mli b/src/ecEnv.mli
index d96a9e192..04354a391 100644
--- a/src/ecEnv.mli
+++ b/src/ecEnv.mli
@@ -515,9 +515,10 @@ module LDecl : sig
 
   val clear : ?leniant:bool -> EcIdent.Sid.t -> hyps -> hyps
 
-  val push_all       : memenv list -> hyps -> hyps
-  val push_active_ss : memenv -> hyps -> hyps
-  val push_active_ts : memenv -> memenv -> hyps -> hyps
+  val push_all        : memenv list -> hyps -> hyps
+  val push_active_all : memenv list -> hyps -> hyps
+  val push_active_ss  : memenv -> hyps -> hyps
+  val push_active_ts  : memenv -> memenv -> hyps -> hyps
 
   val hoareF : memory -> xpath -> hyps -> hyps * hyps
   val equivF : memory -> memory -> xpath -> xpath -> hyps -> hyps * hyps
diff --git a/src/ecFol.ml b/src/ecFol.ml
index 57322210d..7a9fbf494 100644
--- a/src/ecFol.ml
+++ b/src/ecFol.ml
@@ -1104,6 +1104,25 @@ let rec one_sided_vs mem fp =
   | Fapp (f, args) -> one_sided_vs mem f @ List.concat_map (one_sided_vs mem) args
   | _ -> []
 
+(* -------------------------------------------------------------------- *)
+let filter_topand_form (test : form -> bool) =
+  let rec doit (f : form) =
+    match sform_of_form f with
+    | SFand (mode, (f1, f2)) -> begin
+      match doit f1, doit f2 with
+      | None, None -> None
+      | Some f, None | None, Some f -> Some f
+      | Some f1, Some f2 -> begin
+        match mode with
+        | `Sym -> Some (f_and f1 f2)
+        | `Asym -> Some (f_anda f1 f2)
+      end
+    end
+    | _ ->
+      if test f then Some f else None
+  in fun f -> doit f
+
+(* -------------------------------------------------------------------- *)
 let rec dump_f f =
   let dump_quant q =
     match q with
diff --git a/src/ecFol.mli b/src/ecFol.mli
index 080a4d3de..6be1d1aaf 100644
--- a/src/ecFol.mli
+++ b/src/ecFol.mli
@@ -260,5 +260,8 @@ module DestrReal : sig
   val abs : form -> form
 end
 
+(* -------------------------------------------------------------------- *)
+val filter_topand_form : (form -> bool) -> form -> form option
+
 (* -------------------------------------------------------------------- *)
 val dump_f : form -> string
diff --git a/src/ecHiTacticals.ml b/src/ecHiTacticals.ml
index 86338c5af..695538615 100644
--- a/src/ecHiTacticals.ml
+++ b/src/ecHiTacticals.ml
@@ -206,7 +206,7 @@ and process1_phl (_ : ttenv) (t : phltactic located) (tc : tcenv1) =
     | Pconcave info             -> EcPhlConseq.process_concave info
     | Phrex_elim                -> EcPhlExists.t_hr_exists_elim
     | Phrex_intro (fs, b)       -> EcPhlExists.process_exists_intro ~elim:b fs
-    | Phecall (oside, x)        -> EcPhlExists.process_ecall oside x
+    | Phecall (d, s, data)      -> EcPhlExists.process_ecall d s data
     | Pexfalso                  -> EcPhlAuto.t_exfalso
     | Pbydeno (mode, info)      -> EcPhlDeno.process_deno mode info
     | Pbyupto                   -> EcPhlUpto.process_uptobad
diff --git a/src/ecMatching.ml b/src/ecMatching.ml
index a14e8859b..efbe25705 100644
--- a/src/ecMatching.ml
+++ b/src/ecMatching.ml
@@ -372,6 +372,10 @@ module EV = struct
     | Some (`Set _) -> true
     | _ -> false
 
+  let map (f : 'a -> 'a) (m : 'a evmap) =
+    { ev_map   = Mid.map (omap f) m.ev_map
+    ; ev_unset = m.ev_unset }
+
   let doget (x : ident) (m : 'a evmap) =
     match get x m with
     | Some (`Set a) -> a
diff --git a/src/ecMatching.mli b/src/ecMatching.mli
index 66c6bc200..cd1a01301 100644
--- a/src/ecMatching.mli
+++ b/src/ecMatching.mli
@@ -150,6 +150,7 @@ module EV : sig
   val isset  : ident -> 'a evmap -> bool
   val set    : ident -> 'a -> 'a evmap -> 'a evmap
   val get    : ident -> 'a evmap -> [`Unset | `Set of 'a] option
+  val map    : ('a -> 'a) -> 'a evmap -> 'a evmap
   val doget  : ident -> 'a evmap -> 'a
   val fold   : (ident -> 'a -> 'b -> 'b) -> 'a evmap -> 'b -> 'b
   val filled : 'a evmap -> bool
diff --git a/src/ecPV.ml b/src/ecPV.ml
index c1c297d75..10e233d8b 100644
--- a/src/ecPV.ml
+++ b/src/ecPV.ml
@@ -155,6 +155,9 @@ module PVM = struct
     try Mid.change (fun o -> Some (Mpv.add env pv f (odfl Mpv.empty o))) m s
     with AliasClash (env,c) -> uerror env c
 
+  let of_list env pvs =
+    List.fold_left (fun s ((pv, m), f) -> add env pv m f s) empty pvs
+
   let find env pv m s =
     try Mpv.find env pv (Mid.find m s)
     with AliasClash (env,c) -> uerror env c
@@ -580,6 +583,11 @@ let rec e_read_r env r e =
   | Evar pv -> PV.add env pv e.e_ty r
   | _ -> e_fold (e_read_r env) r e
 
+let rec form_read_r env r f =
+  match f.f_node with
+  | Fpvar (pv, _) -> PV.add env pv f.f_ty r
+  | _ -> f_fold (form_read_r env) r f
+
 let rec is_read_r env w s =
   List.fold_left (i_read_r env) w s
 
@@ -624,11 +632,12 @@ let is_write ?(except=Sx.empty) env is = is_write_r ~except env PV.empty is
 let s_write  ?(except=Sx.empty) env s  = s_write_r  ~except env PV.empty s
 let f_write  ?(except=Sx.empty) env f  = f_write_r  ~except env PV.empty f
 
-let e_read  env e  = e_read_r  env PV.empty e
-let i_read  env i  = i_read_r  env PV.empty i
-let is_read env is = is_read_r env PV.empty is
-let s_read  env s  = s_read_r  env PV.empty s
-let f_read  env f  = f_read_r  env PV.empty f
+let e_read     env e  = e_read_r  env PV.empty e
+let form_read  env e  = form_read_r  env PV.empty e
+let i_read     env i  = i_read_r  env PV.empty i
+let is_read    env is = is_read_r env PV.empty is
+let s_read     env s  = s_read_r  env PV.empty s
+let f_read     env f  = f_read_r  env PV.empty f
 
 (* -------------------------------------------------------------------- *)
 exception EqObsInError
diff --git a/src/ecPV.mli b/src/ecPV.mli
index 0e9df4354..3abe99be0 100644
--- a/src/ecPV.mli
+++ b/src/ecPV.mli
@@ -71,6 +71,8 @@ module PVM : sig
 
   val add : env -> prog_var -> EcIdent.t -> form -> subst -> subst
 
+  val of_list : env -> ((prog_var * EcIdent.t) * form) list -> subst
+
   val add_glob : env -> mpath -> EcIdent.t -> form -> subst -> subst
 
   val of_mpv : (form,form) Mpv.t -> EcIdent.t -> subst
@@ -127,11 +129,12 @@ val is_write_r : ?except:Sx.t -> instr list pvaccess
 val s_write_r  : ?except:Sx.t -> stmt       pvaccess
 val f_write_r  : ?except:Sx.t -> xpath      pvaccess
 
-val e_read_r   : expr       pvaccess
-val i_read_r   : instr      pvaccess
-val is_read_r  : instr list pvaccess
-val s_read_r   : stmt       pvaccess
-val f_read_r   : xpath      pvaccess
+val e_read_r      : expr       pvaccess
+val form_read_r   : form       pvaccess
+val i_read_r      : instr      pvaccess
+val is_read_r     : instr list pvaccess
+val s_read_r      : stmt       pvaccess
+val f_read_r      : xpath      pvaccess
 
 (* -------------------------------------------------------------------- *)
 type 'a pvaccess0 = env -> 'a -> PV.t
@@ -142,11 +145,12 @@ val is_write : ?except:Sx.t -> instr list pvaccess0
 val s_write  : ?except:Sx.t -> stmt       pvaccess0
 val f_write  : ?except:Sx.t -> xpath      pvaccess0
 
-val e_read  : expr       pvaccess0
-val i_read  : instr      pvaccess0
-val is_read : instr list pvaccess0
-val s_read  : stmt       pvaccess0
-val f_read  : xpath      pvaccess0
+val e_read     : expr       pvaccess0
+val form_read  : form       pvaccess0
+val i_read     : instr      pvaccess0
+val is_read    : instr list pvaccess0
+val s_read     : stmt       pvaccess0
+val f_read     : xpath      pvaccess0
 
 (* -------------------------------------------------------------------- *)
 exception EqObsInError
diff --git a/src/ecParser.mly b/src/ecParser.mly
index 52e9f4b49..f53677474 100644
--- a/src/ecParser.mly
+++ b/src/ecParser.mly
@@ -2930,6 +2930,10 @@ interleave_info:
 | TILD f=loc(fident) { OKproc(f, true) }
 | f=loc(fident) { OKproc(f, false) }
 
+direction:
+| RRARROW { (`Forward  :> pdirection) }
+| LLARROW { (`Backward :> pdirection) }
+
 %public phltactic:
 | PROC
    { Pfun `Def }
@@ -3115,8 +3119,8 @@ interleave_info:
 
     { Phrex_intro (l, b) }
 
-| ECALL s=side? x=paren(p=qident tvi=tvars_app? fs=sform* { (p, tvi, fs) })
-    { Phecall (s, x) }
+| ECALL d=direction? s=side? x=paren(p=qident tvi=tvars_app? fs=loc(gpterm_arg)* { (p, tvi, fs) })
+    { Phecall (odfl `Backward d, s, x) }
 
 | EXFALSO
     { Pexfalso }
diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml
index 8e12874e8..debc0937a 100644
--- a/src/ecParsetree.ml
+++ b/src/ecParsetree.ml
@@ -736,6 +736,12 @@ type matchmode = [
 (* -------------------------------------------------------------------- *)
 type prrewrite = [`Rw of ppterm | `Simpl]
 
+(* -------------------------------------------------------------------- *)
+type pecall = pqsymbol * ptyannot option * ppt_arg located list
+
+(* -------------------------------------------------------------------- *)
+type pdirection = [`Forward | `Backward]
+
 (* -------------------------------------------------------------------- *)
 type phltactic =
   | Pskip
@@ -774,7 +780,7 @@ type phltactic =
   | Pconcave       of (pformula option tuple2 gppterm * pformula)
   | Phrex_elim
   | Phrex_intro    of (pformula list * bool)
-  | Phecall        of (oside * (pqsymbol * ptyannot option * pformula list))
+  | Phecall        of (pdirection * oside * pecall)
   | Pexfalso
   | Pbydeno        of ([`PHoare | `Equiv | `EHoare ] * (deno_ppterm * bool * pformula option))
   | PPr            of (pformula * pformula) option
diff --git a/src/ecProofTerm.ml b/src/ecProofTerm.ml
index 9055f2462..cd0e21844 100644
--- a/src/ecProofTerm.ml
+++ b/src/ecProofTerm.ml
@@ -789,6 +789,12 @@ and apply_pterm_to_hole ?loc pt =
 and apply_pterm_to_holes ?loc n pt =
   EcUtils.iterop (apply_pterm_to_hole ?loc) n pt
 
+(* -------------------------------------------------------------------- *)
+and apply_pterm_to_max_holes (hyps : LDecl.hyps) (pt : pt_ev) =
+  if is_some (PT.destruct_product ~reduce:true hyps pt.ptev_ax) then
+    apply_pterm_to_max_holes hyps (apply_pterm_to_hole pt)
+  else pt
+  
 (* -------------------------------------------------------------------- *)
 and apply_pterm_to_local ?loc pt id =
   match LDecl.by_id id pt.ptev_env.pte_hy with
@@ -964,3 +970,90 @@ module Prept = struct
   let ahyp h    = asub (hyp h)
   let ahdl h    = asub (hdl h)
 end
+
+(* -------------------------------------------------------------------- *)
+let pvcompare (pv1 : prog_var) (pv2 : prog_var) =
+  match pv1, pv2 with
+  | PVglob x1, PVglob x2 ->
+    EcPath.x_compare x1 x2
+  | PVloc s1, PVloc s2 ->
+    EcSymbols.sym_compare s1 s2
+
+  | PVglob _, PVloc  _ ->  1
+  | PVloc  _, PVglob _ -> -1
+
+module Mpv = Map.Make(struct
+  type t = prog_var
+  let compare = pvcompare
+end)
+
+type mpvars = (ty Mpv.t) Mid.t
+
+(* -------------------------------------------------------------------- *)
+let rec collect_pvars_from_pt (pvs : mpvars) (pt : proofterm) =
+  match pt with
+  | PTApply { pt_args = args } -> begin
+    List.fold_left collect_pvars_from_ptarg pvs args
+  end
+  | PTQuant (_, pt) ->
+    collect_pvars_from_pt pvs pt
+
+and collect_pvars_from_ptarg (pvs : mpvars) (ptarg : pt_arg) =
+  match ptarg with
+  | PAFormula f -> collect_pvars_from_form pvs f
+  | PAMemory _ -> pvs
+  | PAModule _ -> pvs
+  | PASub None -> pvs
+  | PASub (Some pt) -> collect_pvars_from_pt pvs pt
+
+and collect_pvars_from_form (pvs : mpvars) (f : form) =
+  let rec doit (pvs : mpvars) (f : form) =
+    match f.f_node with
+    | Fpvar (pv, m) ->
+      Mid.change (fun pvmap ->
+        Some (Mpv.add pv f.f_ty (odfl Mpv.empty pvmap))
+      ) m pvs
+    | _ -> EcFol.f_fold doit pvs f
+  in doit pvs f
+
+(* -------------------------------------------------------------------- *)
+let collect_pvars_from_pt (pt : proofterm) =
+  Mid.map Mpv.bindings (collect_pvars_from_pt Mid.empty pt)
+
+(* -------------------------------------------------------------------- *)
+module PV = struct
+  open EcPV.PVM
+
+  let rec subst_pt (env : env) (subst : subst) (pt : proofterm) =
+    match pt with
+    | PTApply { pt_head; pt_args } ->
+      PTApply
+        { pt_head = subst_pt_head env subst pt_head
+        ; pt_args = List.map (subst_pt_arg env subst) pt_args }
+    | PTQuant (bds, pt) ->
+      PTQuant (bds, subst_pt env subst pt)
+
+  and subst_pt_head (env : env) (subst : subst) (pth : pt_head) =
+    match pth with
+    | PTHandle _
+    | PTLocal _
+    | PTGlobal _ -> pth
+    | PTCut (f, cs) -> PTCut (subst_form env subst f, cs)
+    | PTTerm pt -> PTTerm (subst_pt env subst pt)
+
+  and subst_pt_arg (env : env) (subst : subst) (pta : pt_arg) =
+    match pta with
+    | PAFormula f -> PAFormula (subst_form env subst f)
+    | PAMemory _  -> pta
+    | PAModule _  -> pta
+    | PASub    pt -> PASub (omap (subst_pt env subst) pt)
+
+  and subst_form (env : env) (subst : subst) (f : form) =
+    EcPV.PVM.subst env subst f
+end
+
+let subst_pv_pt (env : env) (subst : EcPV.PVM.subst) (pt : proofterm) =
+  PV.subst_pt env subst pt
+
+let subst_pv_pt_arg (env : env) (subst : EcPV.PVM.subst) (pt_arg : pt_arg) =
+  PV.subst_pt_arg env subst pt_arg
diff --git a/src/ecProofTerm.mli b/src/ecProofTerm.mli
index 8f5420879..c66db3000 100644
--- a/src/ecProofTerm.mli
+++ b/src/ecProofTerm.mli
@@ -64,6 +64,8 @@ val process_pterm_cut
   : prcut:('a -> form) -> pt_env -> 'a ppt_head -> pt_ev
 val process_pterm
   : pt_env -> (pformula option) ppt_head -> pt_ev
+val process_pterm_arg
+  :  ?implicits:bool -> pt_ev  -> ppt_arg located -> pt_ev_arg
 val process_pterm_args_app
   :  ?implicits:bool -> ?ip:(bool list) -> pt_ev  -> ppt_arg located list
   -> pt_ev * bool list
@@ -99,11 +101,12 @@ val check_pterm_arg :
   -> pt_ev_arg_r
  -> form * pt_arg
 
-val apply_pterm_to_arg   : ?loc:EcLocation.t -> pt_ev -> pt_ev_arg -> pt_ev
-val apply_pterm_to_arg_r : ?loc:EcLocation.t -> pt_ev -> pt_ev_arg_r -> pt_ev
-val apply_pterm_to_local : ?loc:EcLocation.t -> pt_ev -> EcIdent.t -> pt_ev
-val apply_pterm_to_hole  : ?loc:EcLocation.t -> pt_ev -> pt_ev
-val apply_pterm_to_holes : ?loc:EcLocation.t -> int -> pt_ev -> pt_ev
+val apply_pterm_to_arg       : ?loc:EcLocation.t -> pt_ev -> pt_ev_arg -> pt_ev
+val apply_pterm_to_arg_r     : ?loc:EcLocation.t -> pt_ev -> pt_ev_arg_r -> pt_ev
+val apply_pterm_to_local     : ?loc:EcLocation.t -> pt_ev -> EcIdent.t -> pt_ev
+val apply_pterm_to_hole      : ?loc:EcLocation.t -> pt_ev -> pt_ev
+val apply_pterm_to_holes     : ?loc:EcLocation.t -> int -> pt_ev -> pt_ev
+val apply_pterm_to_max_holes : LDecl.hyps -> pt_ev -> pt_ev
 
 (* pattern matching - raise [MatchFailure] on failure. *)
 val pf_form_match : pt_env -> ?mode:fmoptions -> ptn:form -> form -> unit
@@ -198,3 +201,9 @@ module Prept : sig
   val ahyp  : EcIdent.t -> prept_arg
   val ahdl  : handle -> prept_arg
 end
+
+(* -------------------------------------------------------------------- *)
+val collect_pvars_from_pt : proofterm -> ((prog_var * ty) list) EcIdent.Mid.t
+
+val subst_pv_pt :  EcEnv.env -> EcPV.PVM.subst -> proofterm -> proofterm
+val subst_pv_pt_arg :  EcEnv.env -> EcPV.PVM.subst -> pt_arg -> pt_arg
\ No newline at end of file
diff --git a/src/phl/ecPhlCall.ml b/src/phl/ecPhlCall.ml
index 87a3bc727..1642392a5 100644
--- a/src/phl/ecPhlCall.ml
+++ b/src/phl/ecPhlCall.ml
@@ -26,79 +26,186 @@ let wp_asgn_call ?mc env lv res post =
       let lets = lv_subst m lv res.inv in
       {m;inv=mk_let_of_lv_substs ?mc env ([lets], post.inv)}
 
+(* -------------------------------------------------------------------- *)
 let subst_args_call env m e s =
   PVM.add env pv_arg m (ss_inv_of_expr m e).inv s
 
 (* -------------------------------------------------------------------- *)
-let wp2_call
-  env fpre fpost (lpl,fl,argsl) modil (lpr,fr,argsr) modir post hyps
+let compute_hoare_call_post
+  (hyps     : LDecl.hyps)
+  (m        : memory)
+  (contract : form * exnpost)
+  (call     : lvalue option * EcPath.xpath * expr list)
+  (post     : exnpost)
+=
+  let env = LDecl.toenv hyps in
+
+  let (fpre, fpost) = contract in
+  let (lvalue, funname, funargs) = call in
+  let funsig = (Fun.by_xpath funname env).f_sig in
+  let modi  = f_write env funname in
+
+  let { main = fpost; exnmap = (fepost, fd); } = fpost in
+  let { main = post ; exnmap = ( epost,  d); } =  post in
+
+  let vres = LDecl.fresh_id hyps "result" in
+  let fres = f_local vres funsig.fs_ret in
+
+  let fpost = PVM.subst1 env pv_res m fres fpost in
+
+  let post = wp_asgn_call env lvalue { m = m; inv = fres; } { m = m; inv = post; } in
+  let post = (ss_inv_rebind post m).inv in
+  let post = f_imp_simpl fpost post in
+  let post = generalize_mod_ss_inv env modi { m = m; inv = post; } in
+  let post = (ss_inv_rebind post m).inv in
+  let post = f_forall_simpl [(vres, GTty funsig.fs_ret)] post in
+  let post =
+    let spre = subst_args_call env m (e_tuple funargs) PVM.empty in
+    f_anda_simpl (PVM.subst env spre fpre) post in
+
+  let poe = TTC.merge2_poe_list (epost, d) (fepost, fd) in
+  let poe = List.map (fun inv -> { m; inv; }) poe in
+  let poe =
+    let penv_e = EcEnv.Fun.inv_memenv1 m env in
+    List.map (fun f ->
+      let genf = generalize_mod_ss_inv penv_e modi f in
+      (ss_inv_rebind genf m).inv
+    ) poe in
+
+  List.fold f_anda_simpl post poe
+
+(* -------------------------------------------------------------------- *)
+let compute_equiv_call_post
+   (hyps     : LDecl.hyps)
+   ((ml, mr) : memory * memory)
+   (contract : form * form)
+  ?(mods     : EcPV.PV.t * EcPV.PV.t = (EcPV.PV.empty, EcPV.PV.empty))
+   (call_l   : lvalue option * EcPath.xpath * expr list)
+   (call_r   : lvalue option * EcPath.xpath * expr list)
+   (post     : form)
 =
-  let ml, mr = post.ml, post.mr in
+  let env = LDecl.toenv hyps in
+
+  let (fpre, fpost) = contract in
+  let (lpl, fl, argsl) = call_l in
+  let (lpr, fr, argsr) = call_r in
+
+  let modil = EcPV.PV.union (fst mods) (f_write env fl) in
+  let modir = EcPV.PV.union (snd mods) (f_write env fr) in
+
   let fsigl = (Fun.by_xpath fl env).f_sig in
   let fsigr = (Fun.by_xpath fr env).f_sig in
-  (* The wp *)
-  let pvresl = pv_res and pvresr = pv_res in
+
   let vresl = LDecl.fresh_id hyps "result_L" in
   let vresr = LDecl.fresh_id hyps "result_R" in
-  let fresl = {ml;mr; inv=f_local vresl fsigl.fs_ret} in
-  let fresr = {ml;mr; inv=f_local vresr fsigr.fs_ret} in
-  let post = map_ts_inv_left2 (wp_asgn_call ~mc:(ml,mr) env lpl) fresl post in
-  let post = map_ts_inv_right2 (wp_asgn_call ~mc:(ml,mr) env lpr) fresr post in
-  let s    = PVM.empty in
-  let s    = PVM.add env pvresr mr fresr.inv s in
-  let s    = PVM.add env pvresl ml fresl.inv s in
-  let fpost = map_ts_inv1 (PVM.subst env s) fpost in
-  let post = generalize_mod_ts_inv env modil modir (map_ts_inv2 f_imp_simpl fpost post) in
-  let post = map_ts_inv1
+  let fresl = {ml; mr; inv = f_local vresl fsigl.fs_ret} in
+  let fresr = {ml; mr; inv = f_local vresr fsigr.fs_ret} in
+
+  let post =
+       {ml; mr; inv = post}
+    |> map_ts_inv_left2  (wp_asgn_call ~mc:(ml, mr) env lpl) fresl
+    |> map_ts_inv_right2 (wp_asgn_call ~mc:(ml, mr) env lpr) fresr in
+
+  let post = (ts_inv_rebind post ml mr).inv in
+
+  let fpost =
+    let s =
+      PVM.of_list env
+        [((pv_res, mr), fresr.inv); ((pv_res, ml), fresl.inv)] in    
+    PVM.subst env s fpost in
+
+  let post =
+       {ml; mr; inv = (f_imp_simpl fpost post)}
+    |> generalize_mod_ts_inv env modil modir
+  in
+
+  let post = (ts_inv_rebind post ml mr).inv in
+
+  let post =
     (f_forall_simpl
       [(vresl, GTty fsigl.fs_ret);
        (vresr, GTty fsigr.fs_ret)])
       post in
+
   let spre = subst_args_call env ml (e_tuple argsl) PVM.empty in
   let spre = subst_args_call env mr (e_tuple argsr) spre in
-  map_ts_inv2 f_anda_simpl (map_ts_inv1 (PVM.subst env spre) fpre) post
+
+  f_anda_simpl (PVM.subst env spre fpre) post
 
 (* -------------------------------------------------------------------- *)
+let compute_equiv1_call_post
+   (hyps     : LDecl.hyps)
+   (side     : side)
+   ((ml, mr) : memory * memory)
+   (contract : form * form)
+   (call     : lvalue option * EcPath.xpath * expr list)
+   (post     : form)
+=
+  let env = LDecl.toenv hyps in
+
+  let (fpre, fpost) = contract in
+  let (lp, fname, args) = call in
+  let me = sideif side ml mr in
+
+  let wp_asgn_call_side env lv = sideif side
+    (map_ts_inv_left2  (wp_asgn_call ~mc:(ml,mr) env lv))
+    (map_ts_inv_right2 (wp_asgn_call ~mc:(ml,mr) env lv))
+  in
+  let generalize_mod_side = sideif side
+    generalize_mod_left generalize_mod_right in
+
+  let ss_inv_generalize_other_side inv = sideif side
+    (ss_inv_generalize_right inv mr) (ss_inv_generalize_left inv ml) in
+
+  let fsig  = (Fun.by_xpath fname env).f_sig in
+  let vres  = LDecl.fresh_id hyps "result" in
+  let fres  = { ml; mr; inv = f_local vres fsig.fs_ret; } in
+
+  let post  = wp_asgn_call_side env lp fres { ml; mr; inv = post; } in
+  let post  = (ts_inv_rebind post ml mr).inv in
+
+  let subst = PVM.add env pv_res me fres.inv PVM.empty in
+
+  let fpost = ss_inv_generalize_other_side { m = me; inv = fpost; } in
+  let fpost = (ts_inv_rebind fpost ml mr).inv in
+  let fpost = PVM.subst env subst fpost in
 
+  let fpre  = ss_inv_generalize_other_side { m = me; inv = fpre ; } in
+  let fpre  = (ts_inv_rebind fpre ml mr).inv in
+
+  let modi  = f_write env fname in
+  let post  = f_imp_simpl fpost post in
+  let post  = generalize_mod_side env modi { ml; mr; inv = post } in
+  let post  = (ts_inv_rebind post ml mr).inv in
+  let post  = f_forall_simpl [(vres, GTty fsig.fs_ret)] post in
+  let spre  = subst_args_call env me (e_tuple args) PVM.empty in
+
+  f_anda_simpl (PVM.subst env spre fpre) post
+
+(* -------------------------------------------------------------------- *)
 let t_hoare_call fpre fpost tc =
-  let env = FApi.tc1_env tc in
-  let hs = tc1_as_hoareS tc in
-  let (lp,f,args),s = tc1_last_call tc hs.hs_s in
-  let m = EcMemory.memory hs.hs_m in
-  let fsig = (Fun.by_xpath f env).f_sig in
-  (* The function satisfies the specification *)
-  let f_concl = f_hoareF fpre f fpost in
-  (* substitute memories *)
-  let fpre = (ss_inv_rebind fpre m) in
-  let fpost = hs_inv_rebind fpost m in
-  let { main = inv; exnmap = (fepost, fd); } = fpost.hsi_inv in
-  let fpost = {m;inv} in
-  (* The wp *)
-  let { main = post; exnmap = (epost, d); } = (hs_po hs).hsi_inv in
-  let pvres = pv_res in
-  let vres = EcIdent.create "result" in
-  let fres = {m;inv=f_local vres fsig.fs_ret} in
-  let post = wp_asgn_call env lp fres {m=(hs_po hs).hsi_m;inv=post} in
-  let fpost = map_ss_inv2 (PVM.subst1 env pvres m) fres fpost in
-  let modi = f_write env f in
+  let hyps  = FApi.tc1_hyps tc in
+  let hs    = tc1_as_hoareS tc in
+  let m     = EcMemory.memory hs.hs_m in
+  let fpre  = (ss_inv_rebind fpre  m) in
+  let fpost = (hs_inv_rebind fpost m) in
 
-  let post = map_ss_inv2 f_imp_simpl fpost post in
-  let post = generalize_mod_ss_inv env modi post in
-  let post = map_ss_inv1 (f_forall_simpl [(vres, GTty fsig.fs_ret)]) post in
-  let spre = subst_args_call env m (e_tuple args) PVM.empty in
-  let post = map_ss_inv2 f_anda_simpl (map_ss_inv1 (PVM.subst env spre) fpre) post in
+  let call, s = tc1_last_call tc hs.hs_s in
 
-  let poe = TTC.merge2_poe_list (epost,d) (fepost,fd) in
-  let poe = List.map (fun inv -> {m;inv}) poe in
-  let penv_e = EcEnv.Fun.inv_memenv1 m env in
-  let poe = List.map (generalize_mod_ss_inv penv_e modi) poe in
+  (* The function satisfies the specification *)
+  let f_concl = f_hoareF fpre (proj3_2 call) fpost in
 
-  let post = List.fold (map_ss_inv2 f_anda_simpl) post poe in
+  (* WP *)
+  let post  =
+    compute_hoare_call_post hyps m
+      (fpre.inv, fpost.hsi_inv) call (hs_po hs).hsi_inv in
   let post = {
-    hsi_m   = post.m;
-    hsi_inv = { main = post.inv; exnmap = (epost, d); };
+    hsi_m   = m;
+    hsi_inv = { main = post; exnmap = (hs_po hs).hsi_inv.exnmap; };
   } in
+
   let concl = f_hoareS (snd hs.hs_m) (hs_pr hs) s post in
+
   FApi.xmutate1 tc `HlCall [f_concl; concl]
 
 (* -------------------------------------------------------------------- *)
@@ -255,24 +362,25 @@ let t_bdhoare_call fpre fpost opt_bd tc =
 
 (* -------------------------------------------------------------------- *)
 let t_equiv_call fpre fpost tc =
-  let env, hyps, _ = FApi.tc1_eflat tc in
+  let hyps = FApi.tc1_hyps tc in
   let es = tc1_as_equivS tc in
   let ml, mr = fst es.es_ml, fst es.es_mr in
-  let fpre = ts_inv_rebind fpre ml mr in
+
+  let fpre  = ts_inv_rebind fpre  ml mr in
   let fpost = ts_inv_rebind fpost ml mr in
 
-  let (lpl,fl,argsl),sl = tc1_last_call tc es.es_sl in
-  let (lpr,fr,argsr),sr = tc1_last_call tc es.es_sr in
+  let ((_, fl, _) as call_l), sl = tc1_last_call tc es.es_sl in
+  let ((_, fr, _) as call_r), sr = tc1_last_call tc es.es_sr in
+
   (* The functions satisfy their specification *)
   let f_concl = f_equivF fpre fl fr fpost in
-  let modil = f_write env fl in
-  let modir = f_write env fr in
+
   (* The wp *)
   let post =
-    wp2_call env fpre fpost
-      (lpl,fl,argsl) modil (lpr,fr,argsr) modir
-      (es_po es) hyps
-  in
+    compute_equiv_call_post
+      hyps (ml, mr) (fpre.inv, fpost.inv) call_l call_r (es_po es).inv in
+  let post = { ml; mr; inv = post; } in
+
   let concl =
     f_equivS (snd es.es_ml) (snd es.es_mr) (es_pr es) sl sr post in
 
@@ -280,52 +388,34 @@ let t_equiv_call fpre fpost tc =
 
 (* -------------------------------------------------------------------- *)
 let t_equiv_call1 side fpre fpost tc =
-  let env = FApi.tc1_env tc in
-  let equiv = tc1_as_equivS tc in
-  let ml, mr = fst equiv.es_ml, fst equiv.es_mr in
-  let mtl, mtr = snd equiv.es_ml, snd equiv.es_mr in
+  let hyps = FApi.tc1_hyps tc in
+  let es = tc1_as_equivS tc in
 
-  let (me, stmt) =
-    match side with
-    | `Left  -> (EcMemory.memory equiv.es_ml, equiv.es_sl)
-    | `Right -> (EcMemory.memory equiv.es_mr, equiv.es_sr)
-  in
-  let wp_asgn_call_side env lv = sideif side
-    (map_ts_inv_left2 (wp_asgn_call ~mc:(ml,mr) env lv))
-    (map_ts_inv_right2 (wp_asgn_call ~mc:(ml,mr) env lv))
-  in
-  let generalize_mod_side = sideif side
-    generalize_mod_left generalize_mod_right in
-  let ss_inv_generalize_other_side inv = sideif side
-    (ss_inv_generalize_right inv mr) (ss_inv_generalize_left inv ml) in
+  let ml, mr = fst es.es_ml, fst es.es_mr in
+  let me = sideif side ml mr in
 
-  let (lp, f, args), fstmt = tc1_last_call tc stmt in
-  let fsig = (Fun.by_xpath f env).f_sig in
+  let fpre  = ss_inv_rebind fpre  me in
+  let fpost = ss_inv_rebind fpost me in
+
+  let stmt = sideif side es.es_sl es.es_sr in
+  let ((_, fname, _) as call), fstmt = tc1_last_call tc stmt in
 
   (* The function satisfies its specification *)
-  let fconcl = f_bdHoareF fpre f fpost FHeq {m=fpost.m; inv=f_r1} in
+  let fconcl =
+    f_bdHoareF fpre fname fpost FHeq { m = fpost.m; inv = f_r1; } in
 
   (* WP *)
-  let pvres  = pv_res in
-  let vres   = LDecl.fresh_id (FApi.tc1_hyps tc) "result" in
-  let fres   = {ml;mr;inv=f_local vres fsig.fs_ret} in
-  let post   = wp_asgn_call_side env lp fres (es_po equiv) in
-  let subst  = PVM.add env pvres me fres.inv PVM.empty in
-  let fpost  = ss_inv_generalize_other_side (ss_inv_rebind fpost me) in
-  let fpre   = ss_inv_generalize_other_side (ss_inv_rebind fpre me) in
-  let fpost  = map_ts_inv1 (PVM.subst env subst) fpost in
-  let modi   = f_write env f in
-  let post   = map_ts_inv2 f_imp_simpl fpost post in
-  let post   = generalize_mod_side env modi post in
-  let post   = map_ts_inv1 (f_forall_simpl [(vres, GTty fsig.fs_ret)]) post in
-  let spre   = PVM.empty in
-  let spre   = subst_args_call env me (e_tuple args) spre in
-  let post   =
-    map_ts_inv2 f_anda_simpl (map_ts_inv1 (PVM.subst env spre) fpre) post in
+  let post =
+    compute_equiv1_call_post
+      hyps side (ml, mr) (fpre.inv, fpost.inv) call (es_po es).inv in
+  let post = { ml; mr; inv = post; } in
+
+  let mtl, mtr = snd es.es_ml, snd es.es_mr in
+
   let concl  =
     match side with
-    | `Left  -> f_equivS mtl mtr (es_pr equiv) fstmt equiv.es_sr post
-    | `Right -> f_equivS mtl mtr (es_pr equiv) equiv.es_sl fstmt post in
+    | `Left  -> f_equivS mtl mtr (es_pr es) fstmt es.es_sr post
+    | `Right -> f_equivS mtl mtr (es_pr es) es.es_sl fstmt post in
 
   FApi.xmutate1 tc `HlCall [fconcl; concl]
 
diff --git a/src/phl/ecPhlCall.mli b/src/phl/ecPhlCall.mli
index 1c87ae8f2..2cb7d1cd6 100644
--- a/src/phl/ecPhlCall.mli
+++ b/src/phl/ecPhlCall.mli
@@ -4,15 +4,36 @@ open EcCoreGoal.FApi
 open EcAst
 
 (* -------------------------------------------------------------------- *)
-val wp2_call :
-     EcEnv.env -> ts_inv -> ts_inv
+val compute_hoare_call_post :
+     EcEnv.LDecl.hyps
+  -> EcMemory.memory
+  -> form * exnpost
+  -> lvalue option * EcPath.xpath * expr list
+  -> exnpost
+  -> form
+
+(* -------------------------------------------------------------------- *)
+val compute_equiv_call_post :
+     EcEnv.LDecl.hyps
+  -> EcMemory.memory * EcMemory.memory
+  -> form * form
+  -> ?mods:(EcPV.PV.t * EcPV.PV.t)
   -> EcModules.lvalue option * EcPath.xpath * EcTypes.expr list
-  -> EcPV.PV.t
   -> EcModules.lvalue option * EcPath.xpath * EcTypes.expr list
-  -> EcPV.PV.t
-  -> ts_inv
-  -> EcEnv.LDecl.hyps -> ts_inv
+  -> form
+  -> form
 
+(* -------------------------------------------------------------------- *)
+val compute_equiv1_call_post :
+     EcEnv.LDecl.hyps
+  -> side
+  -> EcMemory.memory * EcMemory.memory
+  -> form * form
+  -> EcModules.lvalue option * EcPath.xpath * EcTypes.expr list
+  -> form
+  -> form
+   
+(* -------------------------------------------------------------------- *)
 val t_hoare_call   : ss_inv -> hs_inv -> backward
 val t_bdhoare_call : ss_inv -> ss_inv -> ss_inv option -> backward
 val t_equiv_call   : ts_inv -> ts_inv -> backward
diff --git a/src/phl/ecPhlEager.ml b/src/phl/ecPhlEager.ml
index 800de9b7d..9bb80a3a5 100644
--- a/src/phl/ecPhlEager.ml
+++ b/src/phl/ecPhlEager.ml
@@ -361,11 +361,14 @@ let t_eager_fun_abs_r i tc =
 let t_eager_call_r fpre fpost tc =
   let env, hyps, _ = FApi.tc1_eflat tc in
   let es = tc1_as_equivS tc in
-  let fpre = EcSubst.ts_inv_rebind fpre (fst es.es_ml) (fst es.es_mr) in
-  let fpost = EcSubst.ts_inv_rebind fpost (fst es.es_ml) (fst es.es_mr) in
 
-  let (lvl, fl, argsl), sl = pf_last_call !!tc es.es_sl in
-  let (lvr, fr, argsr), sr = pf_first_call !!tc es.es_sr in
+  let ml, mr = (fst es.es_ml, fst es.es_mr) in
+
+  let fpre  = EcSubst.ts_inv_rebind fpre  ml mr in
+  let fpost = EcSubst.ts_inv_rebind fpost ml mr in
+
+  let ((_, fl, argsl) as call_l), sl = pf_last_call !!tc es.es_sl in
+  let ((_, fr, _) as call_r), sr = pf_first_call !!tc es.es_sr in
 
   let swl = s_write env sl in
   let swr = s_write env sr in
@@ -382,15 +385,18 @@ let t_eager_call_r fpre fpost tc =
 
   List.iter check_a argsl;
 
-  let modil = PV.union (f_write env fl) swl in
-  let modir = PV.union (f_write env fr) swr in
   let post =
-    EcPhlCall.wp2_call env fpre fpost (lvl, fl, argsl) modil (lvr, fr, argsr)
-      modir (es_po es) hyps
+    EcPhlCall.compute_equiv_call_post
+      hyps ~mods:(swl, swr) (ml, mr) (fpre.inv, fpost.inv)
+      call_l call_r (es_po es).inv
   in
-  let f_concl = f_eagerF fpre sl fl fr sr fpost in
+  let post = { ml; mr; inv = post } in
+
+  let f_concl =
+    f_eagerF fpre sl fl fr sr fpost in
+
   let concl =
-    f_equivS (snd es.es_ml) (snd es.es_mr) (es_pr es) (stmt []) (stmt []) post
+    f_equivS (snd es.es_ml) (snd es.es_mr) (es_pr es) s_empty s_empty post
   in
 
   FApi.xmutate1 tc `EagerCall [ f_concl; concl ]
diff --git a/src/phl/ecPhlExists.ml b/src/phl/ecPhlExists.ml
index 90f017cbb..0c48ce521 100644
--- a/src/phl/ecPhlExists.ml
+++ b/src/phl/ecPhlExists.ml
@@ -140,102 +140,443 @@ let process_exists_intro ~(elim : bool) fs tc =
   else tc
 
 (* -------------------------------------------------------------------- *)
-let process_ecall oside (l, tvi, fs) tc =
-  let (hyps, concl) = FApi.tc1_flat tc in
+type call = EcModules.lvalue option * EcPath.xpath * EcTypes.expr list
 
-  let hyps, kind, f_tr =
-    match concl.f_node with
-    | FhoareS hs when is_none oside ->
-        LDecl.push_active_ss hs.hs_m hyps, `Hoare (List.length hs.hs_s.s_node),
-        Inv_ss {m = fst hs.hs_m; inv = f_true}
-    | FequivS es ->
-        let n1 = List.length es.es_sl.s_node in
-        let n2 = List.length es.es_sr.s_node in
-        LDecl.push_all [es.es_ml; es.es_mr] hyps, `Equiv (n1, n2),
-        Inv_ts {ml = fst es.es_ml; mr = fst es.es_mr; inv = f_true}
-    | _ -> tc_error_noXhl ~kinds:[`Hoare `Stmt; `Equiv `Stmt] !!tc
-  in
+type calls = [
+  | `Single of call
+  | `Double of call * call
+]
 
-  let t_local_seq p1 tc =
-    match kind, oside, p1 with
-    | `Hoare n, _, Inv_ss p1 ->
-        EcPhlSeq.t_hoare_seq
-          (Zpr.cpos (n-1)) p1 tc
-    | `Hoare n, _, Inv_hs p1 ->
-        EcPhlSeq.t_hoare_seq
-          (Zpr.cpos (n-1)) (POE.lower p1) tc
-    | `Equiv (n1, n2), None, Inv_ts p1 ->
-        EcPhlSeq.t_equiv_seq
-          (Zpr.cpos (n1-1), Zpr.cpos (n2-1)) p1 tc
-    | `Equiv (n1, n2), Some `Left, Inv_ts p1 ->
-        EcPhlSeq.t_equiv_seq
-          (Zpr.cpos (n1-1), Zpr.cpos n2) p1 tc
-    | `Equiv(n1, n2), Some `Right, Inv_ts p1 ->
-        EcPhlSeq.t_equiv_seq
-          (Zpr.cpos n1, Zpr.cpos (n2-1)) p1 tc
-    | _ -> tc_error !!tc "mismatched sidedness or kind of conclusion"
-  in
+(* -------------------------------------------------------------------- *)
+let check_contract_type
+  ?(loc      : L.t option)
+  ?(phoare   : bool = false)
+  ?(noexn    : bool = true)
+  ~(name     : EcSymbols.qsymbol)
+   (pe       : proofenv)
+   (hyps     : LDecl.hyps)
+   (calls    : calls)
+   (contract : form)
+=
+  let env = LDecl.toenv hyps in
+
+  let contract =
+    EcReduction.h_red_opt EcReduction.full_red hyps contract
+    |> odfl contract in
+
+  match calls with
+  | `Single (_, funname, _) -> begin
+    let cttfname =
+      match contract.f_node with
+      | FhoareF hf ->
+        if noexn then begin
+          if not (POE.is_empty (hf_po hf).hsi_inv) then
+            tc_error ?loc pe
+              "contract must have an empty exception post-condition";
+          end;      
+        hf.hf_f
+      | FbdHoareF hf when phoare -> hf.bhf_f
+      | _ ->
+        tc_error_lazy ?loc pe (fun fmt ->
+          Format.fprintf fmt
+            "contract %a should be a Hoare statement"
+            EcSymbols.pp_qsymbol name
+        )
+    in
+    if not (EcReduction.EqTest.for_xp env funname cttfname) then begin
+      tc_error_lazy ?loc pe (fun fmt ->
+        let ppe = EcPrinting.PPEnv.ofenv env in
+        Format.fprintf fmt
+          "contract %a should be for the procedure %a, not %a"
+          EcSymbols.pp_qsymbol name
+          (EcPrinting.pp_funname ppe) funname
+          (EcPrinting.pp_funname ppe) cttfname
+      )
+    end;
+  end
+
+  | `Double ((_, fl, _), (_, fr, _)) ->
+    let contract =
+      try
+        destr_equivF contract
+      with DestrError _ ->
+        tc_error_lazy ?loc pe (fun fmt ->
+          Format.fprintf fmt
+            "contract %a should be an Equiv statement"
+            EcSymbols.pp_qsymbol name
+        )
+    in
+    List.iter (fun (f, ef_f, side) ->
+      if not (EcReduction.EqTest.for_xp env f ef_f) then begin
+        tc_error_lazy ?loc pe (fun fmt ->
+          let ppe = EcPrinting.PPEnv.ofenv env in
+          Format.fprintf fmt
+            "%s-side of contract %a should be for the procedure %a, not %a"
+            side
+            EcSymbols.pp_qsymbol name
+            (EcPrinting.pp_funname ppe) f
+            (EcPrinting.pp_funname ppe) ef_f
+        )
+      end
+    ) [(fl, contract.ef_fl, "left"); (fr, contract.ef_fr, "right")]
 
-  let fs =
-    List.map
-      (fun f -> map_inv1 (fun _ -> TTC.pf_process_form_opt !!tc hyps None f) f_tr)
-      fs
+(* -------------------------------------------------------------------- *)
+let abstract_pvs
+  (hyps : LDecl.hyps)
+  (ms   : memory list)
+  (pvs  : ((prog_var * ty) list) EcIdent.Mid.t)
+=
+  let env = LDecl.toenv hyps in
+
+  let mkinv =
+    match ms with
+    | [m]      -> fun inv -> Inv_ss { m; inv; }
+    | [ml; mr] -> fun inv -> Inv_ts { ml; mr; inv; }
+    | _        -> assert false in
+
+  let for_memory (subst : EcPV.PVM.subst) (m : memory) =
+    let pvs = EcIdent.Mid.find_def [] m pvs in
+
+    let ids = List.map (fun (pv, ty) ->
+      (Format.sprintf "%s_" (EcTypes.symbol_of_pv pv)), ty) pvs in
+    let ids =
+      List.combine
+        (LDecl.fresh_ids hyps (List.fst ids))
+        (List.snd ids) in
+
+    let pvs_as_inv = List.map (fun (pv, ty) ->
+      mkinv (f_pvar pv ty m).inv
+    ) pvs in
+    let subst = List.fold_left (fun subst ((pv, ty), x) ->
+      EcPV.PVM.add env pv m (f_local x ty) subst
+    ) subst (List.combine pvs (List.fst ids)) in
+
+    (subst, (ids, pvs, pvs_as_inv))
   in
 
-  let ids, p1 =
-    let sub = t_local_seq f_tr tc in
+  let subst, ids =
+    List.fold_left_map for_memory EcPV.PVM.empty ms in
 
-    let sub = FApi.t_rotate `Left 1 sub in
-    let sub = FApi.t_focus (t_hr_exists_intro_r fs) sub in
-    let sub = FApi.t_focus (t_hr_exists_elim_r ~bound:(List.length fs)) sub in
+  let ids = List.map proj3_1 ids 
+  and pvs = List.map proj3_2 ids
+  and pvs_as_inv = List.map proj3_3 ids in
+  let ids = List.flatten ids in
+  let pvs = List.flatten pvs in
+  let pvs_as_inv = List.flatten pvs_as_inv in
 
-    let ids =
-      try  fst (EcFol.destr_forall (FApi.tc_goal sub))
-      with DestrError _ -> [] in
-    let ids = List.map (snd_map gty_as_ty) ids in
+  ids, pvs, pvs_as_inv, subst
+
+(* -------------------------------------------------------------------- *)
+let t_ecall_hoare_fwd ((cttpt, ctt) : (proofterm * form)) (tc : tcenv1) =
+  let hyps = FApi.tc1_hyps tc in
+  let env = EcEnv.LDecl.toenv hyps in
+  let concl = destr_hoareS (FApi.tc1_goal tc) in
+  let m = (fst concl.hs_m) in
+  let (lvalue, funname, _), _ = pf_first_call !!tc concl.hs_s in
+
+  let pvs = PT.collect_pvars_from_pt cttpt in
+  let ids, _, pvs_as_inv, subst = abstract_pvs hyps [m] pvs in
+
+  let tc = t_hr_exists_intro_r pvs_as_inv tc in
+  let tc = FApi.t_focus (t_hr_exists_elim_r ~bound:(List.length ids)) tc in
+  let tc = FApi.t_focus (t_intros_i (List.fst ids)) tc in
+
+  let cttpt = PT.subst_pv_pt env subst cttpt in
+  let ctt = EcPV.PVM.subst env subst ctt in
+
+  let ctt =
+    EcReduction.h_red_opt EcReduction.full_red hyps ctt
+    |> odfl ctt in
+
+  let seqf =
+    let inv = destr_hoareF ctt in
+    let _   = assert (POE.is_empty (hf_po inv).hsi_inv) in
+    let inv = POE.lower (hf_po inv) in
+    let inv = ss_inv_rebind inv (fst concl.hs_m) in
+
+    match lvalue with
+    | None ->
+      let not_contains_res (f : form) =
+        not (EcPV.PV.mem_pv env EcTypes.pv_res (EcPV.form_read env f)) in
+      map_ss_inv1
+        (fun f -> filter_topand_form not_contains_res f |> odfl f_true)
+        inv
+
+    | Some lvalue ->
+      let lv =
+        List.map
+          (fun (pv, ty) -> (f_pvar pv ty inv.m).inv)
+          (EcModules.lv_to_ty_list lvalue) in
+      let sres =
+        EcPV.PVM.add
+          env EcTypes.pv_res inv.m
+          (f_tuple lv) EcPV.PVM.empty in
+
+      { inv = EcPV.PVM.subst env sres inv.inv; m = inv.m; } in
+
+  let seqf_frame =
+    let wr = lvalue |> omap (EcPV.lp_write env) |> odfl EcPV.PV.empty in
+    let wr = EcPV.f_write_r env wr funname in
+    let inv =
+      filter_topand_form
+        (fun f -> EcPV.PV.indep env wr (EcPV.form_read env f))
+        (hs_pr concl).inv in
+    { inv = odfl f_true inv; m = (hs_pr concl).m; } in
+
+  let tc =
+    FApi.t_first
+      (EcPhlSeq.t_hoare_seq (Zpr.cpos 1) (map_ss_inv2 f_and seqf seqf_frame))
+      tc in
+
+  let tc = FApi.t_first EcPhlHoare.t_hoaresplit tc in
+  let tc = FApi.t_first (EcPhlConseq.t_conseqauto ~delta:false ?tsolve:None) tc in
+  let tc = FApi.t_first EcPhlTAuto.t_hoare_true tc in
+
+  let tc = FApi.t_first (EcPhlCall.t_call None ctt) tc in
+  let tc = FApi.t_sub [
+      EcLowGoal.Apply.t_apply_bwd_hi ~dpe:true cttpt;
+      EcPhlSkip.t_skip;
+      t_id
+    ] tc in
+
+  let tc =
+    FApi.t_firsts
+      (t_generalize_hyps ~clear:`Yes (List.fst ids)) 2 tc in
+
+  tc
+
+(* -------------------------------------------------------------------- *)
+let t_ecall_hoare_bwd ((cttpt, _) : proofterm * form) (tc : tcenv1) =
+  let hyps = FApi.tc1_hyps tc in
+  let env = EcEnv.LDecl.toenv hyps in
+  let concl = destr_hoareS (FApi.tc1_goal tc) in
+  let m = fst (concl.hs_m) in
+  let call, _ = pf_last_call !!tc concl.hs_s in
+
+  let pvs = PT.collect_pvars_from_pt cttpt in
+  let ids, _, pvs_as_inv, subst = abstract_pvs hyps [m] pvs in
+
+  let cttpt =
+    let pt_head, pt_args =
+      match cttpt with
+      | PTApply { pt_head; pt_args } -> (pt_head, pt_args)
+      | _ -> assert false in
+    let pt_args = List.map (PT.subst_pv_pt_arg env subst) pt_args in
+    PTApply { pt_head; pt_args } in
+
+  let cttpt, ctt =  EcLowGoal.LowApply.check `Elim cttpt (`Hyps (hyps, !!tc)) in
+
+  let ctt =
+    EcReduction.h_red_opt EcReduction.full_red hyps ctt
+    |> odfl ctt in
+
+  let ids_subst =
+    List.fold_left2
+      (fun s (id, _) pv -> EcSubst.add_flocal s id (inv_of_inv pv))
+      EcSubst.empty ids pvs_as_inv in
+
+  let fpre, fpost =
+    let hf = destr_hoareF ctt in
+    (ss_inv_rebind (hf_pr hf) m).inv, (hs_inv_rebind (hf_po hf) m).hsi_inv
+  in
 
-    let nms = List.map (fun (_, x) -> (EcIdent.create "_", x)) ids in
-    let sub = FApi.t_focus (EcLowGoal.t_intros_i (List.fst nms)) sub in
-    let pte = PT.ptenv_of_penv (FApi.tc_hyps sub) !!tc in
-    let pt  = PT.process_pterm pte (APT.FPNamed (l, tvi)) in
+  let post =
+    EcPhlCall.compute_hoare_call_post
+      hyps m (fpre, fpost) call (hs_po concl).hsi_inv in
+  let post = EcSubst.subst_form ids_subst post in
 
-    let pt =
-      List.fold_left (fun pt (id, ty) ->
-          PT.apply_pterm_to_arg_r pt (PT.PVAFormula (f_local id ty)))
-        pt ids in
+  let tc = EcPhlSeq.t_hoare_seq (Zpr.cpos (-1)) { m = m; inv = post; } tc in
+  let tc = FApi.t_last (t_hr_exists_intro_r pvs_as_inv) tc in
+  let tc = FApi.t_last (t_hr_exists_elim_r ~bound:(List.length ids)) tc in
+  let tc = FApi.t_last (t_intros_i (List.fst ids)) tc in
+  let tc = FApi.t_last (EcPhlCall.t_call None ctt) tc in
 
-    assert (PT.can_concretize pt.PT.ptev_env);
-    let _pt, ax = PT.concretize pt in
+  FApi.t_sub [
+    EcLowGoal.t_id; (* initial hoare statement without the call *)
+    EcLowGoal.Apply.t_apply_bwd_hi ~dpe:true cttpt; (* Prove the Hoare contract *)
+    EcPhlAuto.t_auto ?conv:None; (* Kill the conseq from the call rule *)
+  ] tc
 
-    let sub = FApi.t_focus (EcPhlCall.t_call oside ax) sub in
-    let sub = FApi.t_rotate `Left 1 sub in
-    let sub = oget (get_post (FApi.tc_goal sub)) in
+(* -------------------------------------------------------------------- *)
+let process_ecall_hoare
+  (dir   : APT.pdirection)
+  (pterm : APT.pecall)
+  (tc    : tcenv1)
+=
+  let (ctt_path, ctt_tvi, ctt_args) = pterm in
+  let hyps = FApi.tc1_hyps tc in
+  let concl = destr_hoareS (FApi.tc1_goal tc) in
+
+  (* Type-check contract (lemma) - apply it fully to find the Hoare contract *)
+  let ptenv = PT.ptenv_of_penv (LDecl.push_active_ss concl.hs_m hyps) !!tc in
+  let contract = PT.process_pterm ptenv (APT.FPNamed (ctt_path, ctt_tvi)) in
+  let contract, _ = PT.process_pterm_args_app contract ctt_args in
+  let contract = PT.apply_pterm_to_max_holes hyps contract in
+  
+  assert (PT.can_concretize contract.PT.ptev_env);
+  let contract = PT.concretize contract in
+
+  let call, _ =
+    match dir with
+    | `Forward  -> pf_first_call !!tc concl.hs_s
+    | `Backward -> pf_last_call !!tc concl.hs_s in
+
+  check_contract_type
+    ~noexn:(dir <> `Backward) ~loc:(L.loc ctt_path) ~name:(L.unloc ctt_path)
+    !!tc hyps (`Single call) (snd contract);
+
+  match dir with
+  | `Forward  -> t_ecall_hoare_fwd contract tc
+  | `Backward -> t_ecall_hoare_bwd contract tc
 
-    let subst =
-      List.fold_left2
-        (fun s id f -> add_flocal s id (inv_of_inv f))
-        empty (List.fst ids) fs in
-    (nms, subst_inv subst sub) in
+(* -------------------------------------------------------------------- *)
+let process_ecall_equiv
+  (dir   : APT.pdirection)
+  (oside : side option)
+  (pterm : APT.pecall)
+  (tc    : tcenv1)
+=
+  if dir <> `Backward then
+    tc_error !!tc "unsupported direction for ecall on an equiv. goal";
+
+  let (ctt_path, ctt_tvi, ctt_args) = pterm in
+  let hyps = FApi.tc1_hyps tc in
+  let env = EcEnv.LDecl.toenv hyps in
+  let concl = destr_equivS (FApi.tc1_goal tc) in
+  let (ml, _), (mr, _) = concl.es_ml, concl.es_mr in
+
+  (* Type-check contract (lemma) - apply it fully to find the Hoare/Equiv contract *)
+  let cttpt, _ =
+    let ptenv = PT.ptenv_of_penv (LDecl.push_active_ts concl.es_ml concl.es_mr hyps) !!tc in
+    let contract = PT.process_pterm ptenv (APT.FPNamed (ctt_path, ctt_tvi)) in
+    let contract, _ = PT.process_pterm_args_app contract ctt_args in
+    let contract = PT.apply_pterm_to_max_holes hyps contract in
+    assert (PT.can_concretize contract.PT.ptev_env);
+    PT.concretize contract in
+
+  let pvs = PT.collect_pvars_from_pt cttpt in
+  let ids, _, pvs_as_inv, subst = abstract_pvs hyps [ml; mr] pvs in
+
+  let cttpt =
+    let pt_head, pt_args =
+      match cttpt with
+      | PTApply { pt_head; pt_args } -> (pt_head, pt_args)
+      | _ -> assert false in
+    let pt_args = List.map (PT.subst_pv_pt_arg env subst) pt_args in
+    PTApply { pt_head; pt_args } in
+
+  let cttpt, ctt =  EcLowGoal.LowApply.check `Elim cttpt (`Hyps (hyps, !!tc)) in
+
+  let ctt =
+    EcReduction.h_red_opt EcReduction.full_red hyps ctt
+    |> odfl ctt in
+
+  let ids_subst =
+    List.fold_left2
+      (fun s (id, _) pv -> EcSubst.add_flocal s id (inv_of_inv pv))
+      EcSubst.empty ids pvs_as_inv in
+
+  let calls =
+    match oside with
+    | None ->
+      let call_l, _ = pf_last_call !!tc concl.es_sl in
+      let call_r, _ = pf_last_call !!tc concl.es_sr in
+      `Double (call_l, call_r)
+    | Some side ->
+      let call, _ =
+        pf_last_call !!tc (APT.sideif side concl.es_sl concl.es_sr)
+      in `Single call
+  in
 
-  let tc = t_local_seq p1 tc in
-  let tc = FApi.t_rotate `Left 1 tc in
-  let tc = FApi.t_focus (t_hr_exists_intro_r fs) tc in
-  let tc = FApi.t_focus (t_hr_exists_elim_r ~bound:(List.length fs)) tc in
-  let tc = FApi.t_focus (EcLowGoal.t_intros_i (List.fst ids)) tc in
+  check_contract_type
+    ~phoare:true ~loc:(L.loc ctt_path) ~name:(L.unloc ctt_path)
+    !!tc hyps calls ctt;
+
+  match calls with
+  | `Single call -> begin
+    let side = oget oside in
+    let m = APT.sideif side ml mr in
+
+    let fpre, fpost =
+    match ctt.f_node with
+    | FhoareF hf ->
+      assert (POE.is_empty (hf_po hf).hsi_inv);
+      (ss_inv_rebind (hf_pr hf) m).inv,
+      (hs_inv_rebind (hf_po hf) m).hsi_inv.main
+    | FbdHoareF hf ->
+      (ss_inv_rebind (bhf_pr hf) m).inv,
+      (ss_inv_rebind (bhf_po hf) m).inv
+    | _ -> assert false
+    in
 
-  let pte = PT.ptenv_of_penv (FApi.tc_hyps tc) (FApi.tc_penv tc) in
-  let pt  = PT.process_pterm pte (APT.FPNamed (l, tvi)) in
+    let post =
+      EcPhlCall.compute_equiv1_call_post
+        hyps side (ml, mr) (fpre, fpost) call (es_po concl).inv in
+    let post = EcSubst.subst_form ids_subst post in
+
+    let pos =
+      let nl = List.length concl.es_sl.s_node in
+      let nr = List.length concl.es_sr.s_node in
+      APT.sideif side
+        (Zpr.cpos (-1), Zpr.cpos (nr))
+        (Zpr.cpos (nl), Zpr.cpos (-1)) in
+
+    let tc = EcPhlSeq.t_equiv_seq pos { ml; mr; inv = post; } tc in
+    let tc = FApi.t_last (t_hr_exists_intro_r pvs_as_inv) tc in
+    let tc = FApi.t_last (t_hr_exists_elim_r ~bound:(List.length ids)) tc in
+    let tc = FApi.t_last (t_intros_i (List.fst ids)) tc in
+    let tc = FApi.t_last (EcPhlCall.t_call (Some side) ctt) tc in
+
+    FApi.t_sub [
+      EcLowGoal.t_id; (* initial equiv statement without the call *)
+      EcLowGoal.Apply.t_apply_bwd_hi ~dpe:true cttpt; (* Prove the Hoare contract *)
+      EcPhlAuto.t_auto ?conv:None; (* Kill the conseq from the call rule *)
+    ] tc
+  end
+
+  | `Double (call_l, call_r) -> begin
+    let fpre, fpost =
+      let hf = destr_equivF ctt in
+      (ts_inv_rebind (ef_pr hf) ml mr).inv,
+      (ts_inv_rebind (ef_po hf) ml mr).inv
+    in
 
-  let pt =
-    List.fold_left (fun pt (id, ty) ->
-        PT.apply_pterm_to_arg_r pt (PT.PVAFormula (f_local id ty)))
-      pt ids in
+    let post =
+      EcPhlCall.compute_equiv_call_post
+        hyps (ml, mr) (fpre, fpost) call_l call_r (es_po concl).inv in
+    let post = EcSubst.subst_form ids_subst post in
 
-  assert (PT.can_concretize pt.PT.ptev_env);
+    let tc =
+      EcPhlSeq.t_equiv_seq
+        (Zpr.cpos (-1), Zpr.cpos (-1))
+        { ml; mr; inv = post; } tc in
 
-  let pt, ax = PT.concretize pt in
+    let tc = FApi.t_last (t_hr_exists_intro_r pvs_as_inv) tc in
+    let tc = FApi.t_last (t_hr_exists_elim_r ~bound:(List.length ids)) tc in
+    let tc = FApi.t_last (t_intros_i (List.fst ids)) tc in
+    let tc = FApi.t_last (EcPhlCall.t_call None ctt) tc in
 
-  let tc = FApi.t_focus (EcPhlCall.t_call oside ax) tc in
-  let tc = FApi.t_focus (EcLowGoal.Apply.t_apply_bwd_hi ~dpe:true pt) tc in
+    FApi.t_sub [
+      EcLowGoal.t_id; (* initial equiv statement without the call *)
+      EcLowGoal.Apply.t_apply_bwd_hi ~dpe:true cttpt; (* Prove the Hoare contract *)
+      EcPhlAuto.t_auto ?conv:None; (* Kill the conseq from the call rule *)
+    ] tc
+  end
 
-  FApi.t_last EcPhlAuto.t_auto (FApi.t_rotate `Right 1 tc)
+(* -------------------------------------------------------------------- *)
+let process_ecall
+  (dir   : APT.pdirection)
+  (oside : side option)
+  (pterm : APT.pecall) 
+  (tc    : tcenv1)
+=
+  match (FApi.tc1_goal tc).f_node with
+  | FhoareS _  ->
+      if Option.is_some oside then
+        tc_error !!tc "cannot provide a side for Hoare goals";
+      process_ecall_hoare dir pterm tc
+
+  | FequivS _ ->
+      process_ecall_equiv dir oside pterm tc
+
+  | _ -> tc_error_noXhl ~kinds:[`Hoare `Stmt; `Equiv `Stmt] !!tc
diff --git a/src/phl/ecPhlExists.mli b/src/phl/ecPhlExists.mli
index 685af80a7..4e7eea59c 100644
--- a/src/phl/ecPhlExists.mli
+++ b/src/phl/ecPhlExists.mli
@@ -10,4 +10,4 @@ val t_hr_exists_intro  : inv list -> backward
 
 (* -------------------------------------------------------------------- *)
 val process_exists_intro : elim:bool -> pformula list -> backward
-val process_ecall : oside -> pqsymbol * ptyannot option * pformula list -> backward
+val process_ecall : pdirection -> oside -> pecall -> backward
diff --git a/tests/forward-call.ec b/tests/forward-call.ec
new file mode 100644
index 000000000..4c32690ae
--- /dev/null
+++ b/tests/forward-call.ec
@@ -0,0 +1,26 @@
+require import AllCore.
+
+module M = {
+  proc f(x : int) : int = {
+    return x + 1;
+  }
+
+  proc g(x : int, y : int) : int = {
+    x <@ f(x);
+    x <- x + 1;
+    return 2*x;
+  }
+}.
+
+lemma fP : hoare[M.f : 0 <= x ==> 1 <= res].
+proof. by proc; auto=> /#. qed.
+
+pred p : int.
+
+lemma gP (y_ : int) :
+  hoare[M.g : 0 < x /\ y = y_ /\ p y ==> 0 < res /\ p y_].
+proof.
+proc=> /=.
+ecall ->> (fP); first by move=> &hr |> /#.
+by auto=> &hr |> /#.
+qed.