Add forward ecall with framed preconditions

This extends ecall to support forward calls on Hoare goals via ->>, while keeping backward behavior for existing uses.

It refactors call postcondition generation into reusable helpers, adds proof-term/program-variable substitution utilities needed to instantiate contracts cleanly, and checks that the supplied contract matches the targeted procedure(s). For forward Hoare calls, the tactic now automatically frames precondition conjuncts that are independent of the call’s writes.

A regression test is added in tests/forward-call.ec.

Author: strub

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

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 =

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
 

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)

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

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

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

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

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

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