From 6a4af9b0a170e1ac180133e04b5e21d7c7cc8b97 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Fri, 20 Mar 2026 20:03:58 +0100 Subject: [PATCH] Add forward ecall with framed preconditions MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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. --- src/ecAst.mli | 1 + src/ecCoreFol.ml | 5 + src/ecCoreFol.mli | 1 + src/ecEnv.ml | 26 ++- src/ecEnv.mli | 7 +- src/ecFol.ml | 19 ++ src/ecFol.mli | 3 + src/ecHiTacticals.ml | 2 +- src/ecMatching.ml | 4 + src/ecMatching.mli | 1 + src/ecPV.ml | 19 +- src/ecPV.mli | 24 +- src/ecParser.mly | 8 +- src/ecParsetree.ml | 8 +- src/ecProofTerm.ml | 93 ++++++++ src/ecProofTerm.mli | 19 +- src/phl/ecPhlCall.ml | 282 ++++++++++++++-------- src/phl/ecPhlCall.mli | 33 ++- src/phl/ecPhlEager.ml | 26 ++- src/phl/ecPhlExists.ml | 501 +++++++++++++++++++++++++++++++++------- src/phl/ecPhlExists.mli | 2 +- tests/forward-call.ec | 26 +++ 22 files changed, 882 insertions(+), 228 deletions(-) create mode 100644 tests/forward-call.ec diff --git a/src/ecAst.mli b/src/ecAst.mli index 61afbb830a..db7a2a6796 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 54d61478c0..f6cb18e13d 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 1f2afcb856..9c9c603679 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 edd45ca71f..8a449a7797 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 d96a9e192a..04354a391d 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 57322210d9..7a9fbf4942 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 080a4d3dea..6be1d1aafc 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 86338c5af9..6955386156 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 a14e8859b3..efbe257050 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 66c6bc2006..cd1a01301e 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 c1c297d754..10e233d8b5 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 0e9df4354b..3abe99be0d 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 52e9f4b499..f53677474f 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 8e12874e82..debc0937a1 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 9055f24629..cd0e218446 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 8f54208794..c66db30002 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 87a3bc727e..1642392a57 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 1c87ae8f21..2cb7d1cd62 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 800de9b7d4..9bb80a3a59 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 90f017cbb1..0c48ce521d 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 685af80a7d..4e7eea59c8 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 0000000000..4c32690ae1 --- /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.