diff --git a/src/phl/README.md b/src/phl/README.md index 07d7c1e21..f70c495c3 100644 --- a/src/phl/README.md +++ b/src/phl/README.md @@ -143,7 +143,7 @@ src/phl/ transforms/ EcTr: catalogue entries of the program transformations ecPl*.ml computations shared by the rules of every logic: EcPlFrame, EcPlSp, EcPlWp, EcPlRndSem, EcPlRCond, EcPlTransform, - EcPlMatch, EcPlFun + EcPlMatch, EcPlFun, EcPlCall ecPlRecheck.ml checker scaffolding ecPhl.ml legacy: thin dispatchers and adapters, not-yet-migrated tactics @@ -155,6 +155,9 @@ src/phl/ - The `proc` rules (`EcFunDef`, `EcFunAbs`, `EcEquivFunAbsUpto`, `EcFunToCode`, `EcEagerFunToCode`) are logic rules in `rules//`; `proc I` is derived (consequence + rule). +- The `call` rules (`EcCall`) are logic rules on the call alone; + `call` is derived (`seq` + rule), except in bdhoare, whose rule keeps its + composite statement on `c; x <@ f(a)`. - A rule relating two logics (e.g. the `pr` bridges) lives with the logic of its conclusion. - A rule concluding a probability statement from a judgement (`byphoare`, diff --git a/src/phl/REFACTORING.md b/src/phl/REFACTORING.md index 29578af13..8f09c5d28 100644 --- a/src/phl/REFACTORING.md +++ b/src/phl/REFACTORING.md @@ -156,7 +156,8 @@ src/phl/ its obligations), EcPlMatch (branches of a `match` on fresh program variables), EcPlFun (unfolding a procedure, the oracle conditions of the abstract-procedure rules, - the single-call statement of `proc*`) + the single-call statement of `proc*`), EcPlCall (the + result assignment and argument substitution of a call) ecPlRecheck.ml checker scaffolding ecPhl.ml legacy: thin dispatchers and adapters, not-yet-migrated tactics @@ -175,6 +176,13 @@ uniform across logics or relate several judgements: the consequence rule then the rule), `EcEquivFunAbsUpto` (the abstract upto rule) and `EcFunToCode` (`proc*`, also `EcEagerFunToCode` in `rules/eager/`); +- the `call` rules are logic rules in `rules//` (`EcCall`), + stated on the call alone (`lv <@ f(a)`; `lv <@ f(a) ~ skip` for the + one-sided equiv rule), with the specification of the procedure as + premise and the weakest precondition of the call as precondition; + `call` is derived (`seq`, then the rule); the bdhoare rule keeps its + statement on `c; lv <@ f(a)` (implicit seq and framing: the bdhoare + `seq` rule has extra premises); - a rule relating judgements of two logics (the `pr` bridges, `hoare` from `phoare`, …) lives with the logic of its conclusion; - a rule concluding a statement on probabilities from a judgement diff --git a/src/phl/ecPhlCall.ml b/src/phl/ecPhlCall.ml index 5352f522c..e66aeb8c2 100644 --- a/src/phl/ecPhlCall.ml +++ b/src/phl/ecPhlCall.ml @@ -1,13 +1,6 @@ (* -------------------------------------------------------------------- *) -open EcUtils open EcParsetree open EcAst -open EcTypes -open EcModules -open EcFol -open EcEnv -open EcPV -open EcSubst open EcCoreGoal open EcLowGoal @@ -17,435 +10,40 @@ module PT = EcProofTerm module TTC = EcProofTyping (* -------------------------------------------------------------------- *) -let wp_asgn_call ?mc env lv res post = - assert (res.m = post.m); - let m = post.m in - match lv with - | None -> post - | Some lv -> - let lets = lv_subst m lv res.inv in - {m;inv=mk_let_of_lv_substs ?mc env ([lets], post.inv)} +(* The [call] rules live, one module per logic, in [rules//]: + [EcHoareCall], [EcEHoareCall], [EcBdHoareCall] and [EcEquivCall] (two- + and one-sided); their shared computations are in [EcPlCall]. This + module only keeps the legacy entry points (adapters onto those rules, + so external callers and this module's interface are unchanged) and the + logic-agnostic dispatchers. *) (* -------------------------------------------------------------------- *) -let subst_args_call env m e s = - PVM.add env pv_arg m (ss_inv_of_expr m e).inv s +let compute_hoare_call_post = EcHoareCall.hoare_call_wp -(* -------------------------------------------------------------------- *) -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; } = fpost in - let { main = post ; exnmap = epost; } = 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 fepost 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 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 - - 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 = - {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 - - 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 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 call, s = tc1_last_call tc hs.hs_s in - - (* The function satisfies the specification *) - let f_concl = f_hoareF fpre (proj3_2 call) fpost 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 = 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 +let compute_equiv_call_post = EcEquivCall.equiv_call_wp - FApi.xmutate1 tc `HlCall [f_concl; concl] +let compute_equiv1_call_post = EcEquivCall.equiv_call_onesided_wp (* -------------------------------------------------------------------- *) -let ehoare_call_pre_post fpre fpost tc = - let (env, hyps, _) = FApi.tc1_eflat tc in - let hs = tc1_as_ehoareS tc in - let (lp,f,args),s = tc1_last_call tc hs.ehs_s in - let m = EcMemory.memory hs.ehs_m in - let fpre = ss_inv_rebind fpre m in - let fpost = ss_inv_rebind fpost m in - (* Ensure that all asigned variables are locals *) - let all_loc = - match lp with - | None -> true - | Some(LvVar (v,_)) -> EcTypes.is_loc v - | Some(LvTuple vs) -> List.for_all (fun (v,_) -> EcTypes.is_loc v) vs in - if not all_loc then - tc_error !!tc "ehoare call core rule: only local variables are supported on the left side of a call"; - (* The wp *) - let fres = - match lp with - | None -> None - | Some (LvVar (v,ty)) -> Some (f_pvar v ty m) - | Some (LvTuple vs) -> Some (map_ss_inv f_tuple (List.map (fun (v,ty) -> f_pvar v ty m) vs)) in - let pvres = pv_res in - let wppost = - omap_dfl (fun fres -> map_ss_inv2 (PVM.subst1 env pvres m) fres fpost) fpost fres in - let fv = PV.fv env m wppost.inv in - if PV.mem_pv env pv_res fv then - tc_error !!tc - "ehoare call core rule: the post condition of the function depend on res but the result is not assigned"; +let t_hoare_call fpre fpost = + EcHoareCall.(t_hoare_call_last { hcall_pre = fpre; hcall_post = fpost; }) - let spre = subst_args_call env m (e_tuple args) PVM.empty in - let wppre = map_ss_inv1 (PVM.subst env spre) fpre in - hyps, env, hs, s, f, wppre, wppost +let t_ehoare_call fpre fpost = + EcEHoareCall.(t_ehoare_call_last { ehcall_pre = fpre; ehcall_post = fpost; }) +let t_bdhoare_call fpre fpost opt_bd = + EcBdHoareCall.(t_bdhoare_call + { bhcall_pre = fpre; bhcall_post = fpost; bhcall_bd = opt_bd; }) -let t_ehoare_call_core fpre fpost tc = - let hyps, env, hs, s, f, wppre, wppost = ehoare_call_pre_post fpre fpost tc in - if not (List.is_empty s.s_node) then - tc_error !!tc "ehoare call core rule: only single call statements are accepted"; - if not (EcReduction.ss_inv_is_conv hyps (ehs_po hs) wppost) then - (let env = EcEnv.Memory.push_active_ss hs.ehs_m env in - let ppe = EcPrinting.PPEnv.ofenv env in - tc_error !!tc "ehoare call core rule: wrong post-condition %a instead %a" - (EcPrinting.pp_form ppe) (ehs_po hs).inv (EcPrinting.pp_form ppe) wppost.inv); +let t_equiv_call fpre fpost = + EcEquivCall.(t_equiv_call_last { ecall_pre = fpre; ecall_post = fpost; }) - if not (EcReduction.ss_inv_is_conv hyps (ehs_pr hs) wppre) then - (let env = EcEnv.Memory.push_active_ss hs.ehs_m env in - let ppe = EcPrinting.PPEnv.ofenv env in - tc_error !!tc "ehoare call core rule: wrong pre-condition %a instead %a" - (EcPrinting.pp_form ppe) (ehs_pr hs).inv (EcPrinting.pp_form ppe) wppre.inv); - - (* The function satisfies the specification *) - let f_concl = f_eHoareF fpre f fpost in - FApi.xmutate1 tc `HlCall [f_concl] - - -let t_ehoare_call fpre fpost tc = - let _, _, _, _, _, wppre, _ = ehoare_call_pre_post fpre fpost tc in - let tcenv = - EcPhlSeq.t_ehoare_seq (GapBefore (EcMatching.Position.cpos1_last)) wppre tc in - let tcenv = FApi.t_swap_goals 0 1 tcenv in - FApi.t_sub [t_ehoare_call_core fpre fpost; t_id] tcenv - -let t_ehoare_call_concave f fpre fpost tc = - let _, _, _, _, _, wppre, wppost = ehoare_call_pre_post fpre fpost tc in - let tcenv = - EcPhlSeq.t_ehoare_seq (GapBefore (EcMatching.Position.cpos1_last)) - (map_ss_inv2 (fun wppre f -> f_app_simpl f [wppre] txreal) wppre f) tc in - let tcenv = FApi.t_swap_goals 0 1 tcenv in - let t_call = - FApi.t_seqsub (EcPhlConseq.t_ehoareS_concave f wppre wppost) - [ t_id; - t_id; - t_id; - t_ehoare_call_core fpre fpost] - in - - FApi.t_sub [t_call; t_id] tcenv +let t_equiv_call1 side fpre fpost = + EcEquivCall.(t_equiv_call_onesided_last + { ecallos_side = side; ecallos_pre = fpre; ecallos_post = fpost; }) (* -------------------------------------------------------------------- *) -let bdhoare_call_spec pf fpre fpost f cmp bd opt_bd = - let msg = - "optional bound parameter not allowed for upper-bounded judgements" in - - match cmp, opt_bd with - | FHle, Some _ -> tc_error pf "%s" msg - | FHle, None -> f_bdHoareF fpre f fpost FHle bd - | FHeq, Some bd -> f_bdHoareF fpre f fpost FHeq bd - | FHeq, None -> f_bdHoareF fpre f fpost FHeq bd - | FHge, Some bd -> f_bdHoareF fpre f fpost FHge bd - | FHge, None -> f_bdHoareF fpre f fpost FHge bd - -(* -------------------------------------------------------------------- *) -let t_bdhoare_call fpre fpost opt_bd tc = - let env = FApi.tc1_env tc in - let bhs = tc1_as_bdhoareS tc in - let (lp,f,args),s = tc1_last_call tc bhs.bhs_s in - let m = fpre.m in - let fsig = (Fun.by_xpath f env).f_sig in - let bhs_bd = ss_inv_rebind (bhs_bd bhs) m in - let bhs_po = ss_inv_rebind (bhs_po bhs) m in - let bhs_pr = ss_inv_rebind (bhs_pr bhs) m in - - (* The bound of the specification of the called procedure (the bound of - the conclusion, or [opt_bd]) is interpreted in the memory the procedure - starts from: after [s], and with the local variables of the callee. - The bound of the conclusion is interpreted in the initial memory, with - the local variables of the caller. The two coincide only if this bound - depends neither on local variables nor on variables written by [s]. *) - let callee_bd = odfl bhs_bd opt_bd in - let fv_bd = PV.fv env callee_bd.m callee_bd.inv in - - if List.exists (fun (pv, _) -> is_loc pv) (fst (PV.elements fv_bd)) then - tc_error !!tc "The bound cannot depend on local variables"; - - if not (PV.indep env (s_write env s) fv_bd) then - tc_error !!tc - "The bound cannot depend on variables written by the \ - statements preceding the call"; - - (* The function satisfies the specification *) - let f_concl = - bdhoare_call_spec !!tc fpre fpost f bhs.bhs_cmp bhs_bd opt_bd in - - (* The wp *) - 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 bhs_po in - let fpost = map_ss_inv2 (PVM.subst1 env pvres m) fres fpost in - let modi = f_write env f in - let post = - match bhs.bhs_cmp with - | FHle -> map_ss_inv2 f_imp_simpl post fpost - | FHge -> map_ss_inv2 f_imp_simpl fpost post - - | FHeq when f_equal bhs_bd.inv f_r0 -> - map_ss_inv2 f_imp_simpl post fpost - - | FHeq when f_equal bhs_bd.inv f_r1 -> - map_ss_inv2 f_imp_simpl fpost post - - | FHeq -> map_ss_inv2 f_iff_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 - - (* most of the above code is duplicated from t_hoare_call *) - let concl = - let _,mt = bhs.bhs_m in - match bhs.bhs_cmp, opt_bd with - | FHle, None -> - let post =empty_hs post in - f_hoareS mt bhs_pr s post - | FHeq, Some bd -> - f_bdHoareS mt bhs_pr s post bhs.bhs_cmp (map_ss_inv2 f_real_div bhs_bd bd) - | FHeq, None -> - f_bdHoareS mt bhs_pr s post bhs.bhs_cmp {m;inv=f_r1} - | FHge, Some bd -> - f_bdHoareS mt bhs_pr s post bhs.bhs_cmp (map_ss_inv2 f_real_div bhs_bd bd) - | FHge, None -> - f_bdHoareS mt bhs_pr s post FHeq {m;inv=f_r1} - | _, _ -> assert false - in - - FApi.xmutate1 tc `HlCall [f_concl; concl] - -(* -------------------------------------------------------------------- *) -let t_equiv_call fpre fpost tc = - 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 fpost = ts_inv_rebind fpost ml mr 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 - - (* The wp *) - let post = - 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 - - FApi.xmutate1 tc `HlCall [f_concl; concl] - -(* -------------------------------------------------------------------- *) -let t_equiv_call1 side fpre fpost tc = - 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 me = sideif side ml mr 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 fname fpost FHeq { m = fpost.m; inv = f_r1; } in - - (* WP *) - 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 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] - -(* -------------------------------------------------------------------- *) -let call_error env tc f1 f2 = - tc_error_lazy !!tc (fun fmt -> - let ppe = EcPrinting.PPEnv.ofenv env in - Format.fprintf fmt - "call cannot be used with a lemma referring to `%a': \ - the last statement is a call to `%a'" - (EcPrinting.pp_funname ppe) f1 - (EcPrinting.pp_funname ppe) f2) - +(* Dispatch on the specification [ax] and the goal. *) let t_call side ax tc = let env = FApi.tc1_env tc in let hyps, concl = FApi.tc1_flat tc in @@ -454,19 +52,19 @@ let t_call side ax tc = | FhoareF hf, FhoareS hs -> let (_, f, _), _ = tc1_last_call tc hs.hs_s in if not (EcEnv.NormMp.x_equal env hf.hf_f f) then - call_error env tc hf.hf_f f; + EcPlCall.call_error env tc hf.hf_f f; t_hoare_call (hf_pr hf) (hf_po hf) tc | FeHoareF hf, FeHoareS hs -> let (_, f, _), _ = tc1_last_call tc hs.ehs_s in if not (EcEnv.NormMp.x_equal env hf.ehf_f f) then - call_error env tc hf.ehf_f f; + EcPlCall.call_error env tc hf.ehf_f f; t_ehoare_call (ehf_pr hf) (ehf_po hf) tc | FbdHoareF hf, FbdHoareS hs -> let (_, f, _), _ = tc1_last_call tc hs.bhs_s in if not (EcEnv.NormMp.x_equal env hf.bhf_f f) then - call_error env tc hf.bhf_f f; + EcPlCall.call_error env tc hf.bhf_f f; t_bdhoare_call (bhf_pr hf) (bhf_po hf) None tc | FequivF ef, FequivS es -> @@ -496,225 +94,35 @@ let t_call side ax tc = | _, _ -> tc_error !!tc "call: invalid goal shape" (* -------------------------------------------------------------------- *) -let mk_inv_spec (_pf : proofenv) env inv fl fr = - let ml, mr = inv.ml, inv.mr in - match NormMp.is_abstract_fun fl env with - | true -> - let (topl, _, _, sigl), - (topr, _, _ , sigr) = EcLowPhlGoal.abstract_info2 env fl fr in - let eqglob = ts_inv_eqglob topl ml topr mr in - let lpre = [eqglob;inv] in - let eq_params = - ts_inv_eqparams - sigl.fs_arg sigl.fs_anames ml - sigr.fs_arg sigr.fs_anames mr in - let eq_res = ts_inv_eqres sigl.fs_ret ml sigr.fs_ret mr in - let pre = map_ts_inv f_ands (eq_params::lpre) in - let post = map_ts_inv f_ands [eq_res; eqglob; inv] in - f_equivF pre fl fr post - - | false -> - let defl = EcEnv.Fun.by_xpath fl env in - let defr = EcEnv.Fun.by_xpath fr env in - let sigl, sigr = defl.f_sig, defr.f_sig in - - let error s tl tr = - let ppe = EcPrinting.PPEnv.ofenv env in - tc_error _pf "@[The procedures do not have the same %s types:@]@;<2 2>\ - @[Left side: @[%a@]@,\ - Right side: @[%a@]@]@;<2 0>\ - A full contract cannot be inferred; consider providing a full contract using@;<2 2>\ - call (: ...==> ...)@," - s - (EcPrinting.pp_type ppe) tl - (EcPrinting.pp_type ppe) tr - in - - if not (EcReduction.EqTest.for_type env sigl.fs_arg sigr.fs_arg) - then error "argument" sigl.fs_arg sigr.fs_arg; - - if not (EcReduction.EqTest.for_type env sigl.fs_ret sigr.fs_ret) - then error "return" sigl.fs_ret sigr.fs_ret; - - let eq_params = - ts_inv_eqparams - sigl.fs_arg sigl.fs_anames ml - sigr.fs_arg sigr.fs_anames mr in - let eq_res = ts_inv_eqres sigl.fs_ret ml sigr.fs_ret mr in - let pre = map_ts_inv2 f_and eq_params inv in - let post = map_ts_inv2 f_and eq_res inv in - f_equivF pre fl fr post - -let ensure_none_poe tc poe = - if not (is_none poe) then tc_error !!tc "exception are not supported" +(* Dispatch the typing of the cut (the specification of the called + procedure) on the goal. *) +let process_call_cut side tc info = + match (FApi.tc1_goal tc).f_node, info with + | FhoareS _, _ -> EcHoareCall.process_hoare_call_cut side info tc + | FeHoareS _, _ -> EcEHoareCall.process_ehoare_call_cut side info tc + | FbdHoareS _, _ -> EcBdHoareCall.process_bdhoare_call_cut side info tc + | FequivS _, _ -> EcEquivCall.process_equiv_call_cut side info tc + + | _, CI_spec _ -> + tc_error !!tc "the conclusion is not a hoare or an equiv" + + | _, CI_inv _ -> + if not (Option.is_none side) then + tc_error !!tc "cannot specify side for call with invariants"; + tc_error !!tc "the conclusion is not a hoare or an equiv" + + | _, CI_upto _ -> + if not (Option.is_none side) then + tc_error !!tc "cannot specify side for call with invariants"; + tc_error !!tc "the conclusion is not an equiv" +(* -------------------------------------------------------------------- *) let process_call (side, info) tc = - let process_spec_2 tc side pre post = - let (hyps, concl) = FApi.tc1_flat tc in - match concl.f_node, side with - | FbdHoareS bhs, None -> - let (_,f,_) = fst (tc1_last_call tc bhs.bhs_s) in - let m = (EcIdent.create "&hr") in - let penv, qenv = LDecl.hoareF m f hyps in - let pre = TTC.pf_process_form !!tc penv tbool pre in - let post = TTC.pf_process_form !!tc qenv tbool post in - let bd = ss_inv_rebind (bhs_bd bhs) m in - bdhoare_call_spec !!tc {m;inv=pre} {m;inv=post} f bhs.bhs_cmp bd None - - | FeHoareS hs, None -> - let (_,f,_) = fst (tc1_last_call tc hs.ehs_s) in - let m = (EcIdent.create "&hr") in - let penv, qenv = LDecl.hoareF m f hyps in - let pre = TTC.pf_process_form !!tc penv txreal pre in - let post = TTC.pf_process_form !!tc qenv txreal post in - f_eHoareF {m;inv=pre} f {m;inv=post} - - | FbdHoareS _, Some _ - | FhoareS _, Some _ -> - tc_error !!tc "side can only be given for prhl judgements" - - | FequivS es, None -> - let (_,fl,_) = fst (tc1_last_call tc es.es_sl) in - let (_,fr,_) = fst (tc1_last_call tc es.es_sr) in - let (ml, mr) = (EcIdent.create "&1", EcIdent.create "&2") in - let penv, qenv = LDecl.equivF ml mr fl fr hyps in - let pre = TTC.pf_process_form !!tc penv tbool pre in - let post = TTC.pf_process_form !!tc qenv tbool post in - f_equivF {ml;mr;inv=pre} fl fr {ml;mr;inv=post} - - | FequivS es, Some side -> - let fstmt = sideif side es.es_sl es.es_sr in - let m = sideif side (EcIdent.create "&1") (EcIdent.create "&2") in - let (_,f,_) = fst (tc1_last_call tc fstmt) in - let penv, qenv = LDecl.hoareF m f hyps in - let pre = TTC.pf_process_form !!tc penv tbool pre in - let post = TTC.pf_process_form !!tc qenv tbool post in - f_bdHoareF {m;inv=pre} f {m;inv=post} FHeq {m;inv=f_r1} - - | _ -> tc_error !!tc "the conclusion is not a hoare or an equiv" in - - - let process_spec_1 tc side pre post poe = - let (hyps, concl) = FApi.tc1_flat tc in - match concl.f_node, side with - | FhoareS hs, None -> - let (_,f,_) = fst (tc1_last_call tc hs.hs_s) in - let m = (EcIdent.create "&hr") in - let penv, qenv = LDecl.hoareF m f hyps in - let pre = TTC.pf_process_form !!tc penv tbool pre in - let post = TTC.pf_process_form !!tc qenv tbool post in - let env_e = LDecl.inv_memenv1 m hyps in - let poe = TTC.pf_process_poe env_e poe in - f_hoareF {m; inv = pre} f { hsi_m = m; hsi_inv = { main = post; exnmap = poe; } } - - | _ -> tc_error !!tc "the conclusion is not a hoare" in - - let process_inv_1 tc side inv = - if not (is_none side) then - tc_error !!tc "cannot specify side for call with invariants"; - - let hyps, concl = FApi.tc1_flat tc in - match concl.f_node with - | FhoareS hs -> - let m = fst hs.hs_m in - let (_,f,_) = fst (tc1_last_call tc hs.hs_s) in - let me = EcMemory.abstract m in - let hyps = LDecl.push_active_ss me hyps in - let inv = TTC.pf_process_form !!tc hyps tbool inv in - let inv = {m; inv} in - let post = POE.lift inv in - (f_hoareF inv f post , Inv_ss inv) - - | FeHoareS hs -> - let m = fst hs.ehs_m in - let (_,f,_) = fst (tc1_last_call tc hs.ehs_s) in - let me = EcMemory.abstract m in - let hyps = LDecl.push_active_ss me hyps in - let inv = TTC.pf_process_form !!tc hyps txreal inv in - let inv = {m; inv} in - (f_eHoareF inv f inv, Inv_ss inv) - - | FbdHoareS bhs -> - let m = fst bhs.bhs_m in - let (_,f,_) = fst (tc1_last_call tc bhs.bhs_s) in - let me = EcMemory.abstract m in - let hyps = LDecl.push_active_ss me hyps in - let inv = TTC.pf_process_form !!tc hyps tbool inv in - let inv = {m; inv} in - let f = bdhoare_call_spec !!tc inv inv f bhs.bhs_cmp (bhs_bd bhs) None in - (f, Inv_ss inv) - - | FequivS es -> - let ml, mr = fst es.es_ml, fst es.es_mr in - let (_,fl,_) = fst (tc1_last_call tc es.es_sl) in - let (_,fr,_) = fst (tc1_last_call tc es.es_sr) in - let mel, mer = EcMemory.abstract ml, EcMemory.abstract mr in - let hyps = LDecl.push_active_ts mel mer hyps in - let env = LDecl.toenv hyps in - let inv = TTC.pf_process_form !!tc hyps tbool inv in - let inv = {ml;mr; inv} in - (mk_inv_spec !!tc env inv fl fr, Inv_ts inv) - - | _ -> tc_error !!tc "the conclusion is not a hoare or an equiv" in - - let process_upto tc side info = - if not (is_none side) then - tc_error !!tc "cannot specify side for call with invariants"; - let env, _, concl = FApi.tc1_eflat tc in - match concl.f_node with - | FequivS es -> - let ml, mr = fst es.es_ml, fst es.es_mr in - let (_,fl,_) = fst (tc1_last_call tc es.es_sl) in - let (_,fr,_) = fst (tc1_last_call tc es.es_sr) in - let weakened_pre,bad,invP,invQ = EcPhlFun.process_fun_upto_info info tc in - let bad2 = ss_inv_generalize_as_right bad ml mr in - let invP = ts_inv_rebind invP ml mr in - let invQ = ts_inv_rebind invQ ml mr in - let (topl,fl,_,sigl), - (topr,fr,_ ,sigr) = EcLowPhlGoal.abstract_info2 env fl fr in - let eqglob = ts_inv_eqglob topl ml topr mr in - let lpre = [eqglob;invP] in - let eq_params = - ts_inv_eqparams - sigl.fs_arg sigl.fs_anames ml - sigr.fs_arg sigr.fs_anames mr in - let eq_res = ts_inv_eqres sigl.fs_ret ml sigr.fs_ret mr in - let pre = map_ts_inv3 f_if_simpl bad2 invQ (map_ts_inv f_ands (eq_params::lpre)) in - let post = map_ts_inv3 f_if_simpl bad2 invQ (map_ts_inv f_ands [eq_res;eqglob;invP]) in - (weakened_pre,bad,invP,invQ, f_equivF pre fl fr post) - - | _ -> tc_error !!tc "the conclusion is not an equiv" in - let subtactic = ref t_id in let process_cut tc info = - match info with - | CI_spec (pre, epost) -> - begin - let _, concl = FApi.tc1_flat tc in - match concl.f_node with - | FhoareS _ -> - process_spec_1 tc side pre epost.pnormal epost.pexcept - | _ -> - process_spec_2 tc side pre epost.pnormal - end - - | CI_inv inv -> - begin - let f, inv = process_inv_1 tc side inv in - subtactic := (fun tc -> - FApi.t_firsts t_trivial 2 (EcPhlFun.t_fun inv tc)); - f - end - - | CI_upto info -> - let weakened_pre, bad, p, q, form = process_upto tc side info in - let t_tr = FApi.t_or (t_assumption `Conv) t_trivial in - subtactic := (fun tc -> - FApi.t_firsts t_tr 3 (EcPhlFun.t_equivF_abs_upto weakened_pre bad p q tc)); - form - - in + let spec, t_spec = process_call_cut side tc info in + subtactic := t_spec; spec in let pt = PT.tc1_process_full_pterm_cut ~prcut:(process_cut tc) tc info in @@ -741,94 +149,6 @@ let process_call (side, info) tc = (* -------------------------------------------------------------------- *) let process_call_concave (fc, info) tc = - let fc = - let (hyps, concl) = FApi.tc1_flat tc in - match concl.f_node with - | FeHoareS hs -> - let env = LDecl.push_active_ss hs.ehs_m hyps in - {m=fst hs.ehs_m;inv=TTC.pf_process_form !!tc env (tfun txreal txreal) fc} - - | _ -> tc_error !!tc "the conclusion is not a ehoare" in - - (* As for [call] (see [process_call]), the specification is typed in the - memories of the called procedure, and the invariant in an abstract - memory: the local variables of the caller are not in scope (they - would be read as the callee's variables of the same name). *) - let process_spec tc pre post = - let hyps, concl = FApi.tc1_flat tc in - match concl.f_node with - | FeHoareS hs -> - let (_,f,_) = fst (tc1_last_call tc hs.ehs_s) in - let m = EcIdent.create "&hr" in - let penv, qenv = LDecl.hoareF m f hyps in - let pre = TTC.pf_process_form !!tc penv txreal pre in - let post = TTC.pf_process_form !!tc qenv txreal post in - f_eHoareF {m; inv = pre} f {m; inv = post} - - | _ -> tc_error !!tc "the conclusion is not a ehoare" in - - let process_inv tc inv = - let hyps, concl = FApi.tc1_flat tc in - match concl.f_node with - | FeHoareS hs -> - let m = fst hs.ehs_m in - let (_,f,_) = fst (tc1_last_call tc hs.ehs_s) in - let hyps = LDecl.push_active_ss (EcMemory.abstract m) hyps in - let inv = {m; inv = TTC.pf_process_form !!tc hyps txreal inv} in - (f_eHoareF inv f inv, inv) - - | _ -> tc_error !!tc "the conclusion is not a ehoare" in - - let subtactic = ref t_id in - - let process_cut tc info = - match info with - | CI_spec (pre, epost) -> - process_spec tc pre epost.pnormal - - | CI_inv inv -> - let spec, inv = process_inv tc inv in - subtactic := (fun tc -> - FApi.t_firsts t_trivial 2 (EcPhlFun.t_fun (Inv_ss inv) tc)); - spec - - | _ -> - tc_error !!tc "cannot supply additional information for call /" - - in - - let pt = PT.tc1_process_full_pterm_cut ~prcut:(process_cut tc) tc info - in - - let pt = - let rec doit pt = - match TTC.destruct_product ~reduce:true (FApi.tc1_hyps tc) pt.PT.ptev_ax with - | None -> pt - | Some _ -> doit (EcProofTerm.apply_pterm_to_hole pt) - in doit pt in - - let pt, ax = - if not (PT.can_concretize pt.PT.ptev_env) then - tc_error !!tc "cannot infer all placeholders"; - PT.concretize pt in - - let t_call ax tc = - let (env, _, concl) = FApi.tc1_eflat tc in - match ax.f_node, concl.f_node with - | FeHoareF hf, FeHoareS hs -> - let (_, f, _), _ = tc1_last_call tc hs.ehs_s in - if not (EcEnv.NormMp.x_equal env hf.ehf_f f) then - call_error env tc hf.ehf_f f; - t_ehoare_call_concave fc (ehf_pr hf) (ehf_po hf) tc - | _, _ -> tc_error !!tc "call: invalid goal shape" in - - FApi.t_seqsub - (t_call ax) - [ EcPhlConseq.t_concave_incr; - t_trivial; (* pre *) - t_trivial; (* post *) - FApi.t_seqs - [EcLowGoal.Apply.t_apply_bwd_hi ~dpe:true pt; - !subtactic; t_trivial]; - t_id] - tc + match (FApi.tc1_goal tc).f_node with + | FeHoareS _ -> EcEHoareCall.process_ehoare_call_concave (fc, info) tc + | _ -> tc_error !!tc "the conclusion is not a ehoare" diff --git a/src/phl/rules/bdhoare/ecBdHoareCall.ml b/src/phl/rules/bdhoare/ecBdHoareCall.ml new file mode 100644 index 000000000..00e2110a4 --- /dev/null +++ b/src/phl/rules/bdhoare/ecBdHoareCall.ml @@ -0,0 +1,186 @@ +(* -------------------------------------------------------------------- *) +open EcUtils +open EcParsetree +open EcAst +open EcTypes +open EcModules +open EcFol +open EcEnv +open EcPV +open EcSubst + +open EcCoreGoal +open EcLowGoal +open EcLowPhlGoal + +module TTC = EcProofTyping + +(* -------------------------------------------------------------------- *) +(* Parameters of the bdhoare [call] rule: the specification of the called + procedure and the optional bound of that specification. *) +type bdhoare_call = { + bhcall_pre : ss_inv; (* precondition P of the procedure *) + bhcall_post : ss_inv; (* postcondition Q of the procedure *) + bhcall_bd : ss_inv option; (* bound of the procedure, if not d *) +} + +type EcCoreGoal.rule += RBdHoareCall of bdhoare_call + +(* -------------------------------------------------------------------- *) +(* The specification [phoare [f : P ==> Q] cmp bd] of the called + procedure, [bd] being [opt_bd] when given, the bound [d] of the goal + otherwise. Fails when [opt_bd] is given for an upper bound. *) +let bdhoare_call_spec fpre fpost f cmp bd opt_bd = + let msg = + "optional bound parameter not allowed for upper-bounded judgements" in + + match cmp, opt_bd with + | FHle, Some _ -> failwith msg + | FHle, None -> f_bdHoareF fpre f fpost FHle bd + | FHeq, Some bd -> f_bdHoareF fpre f fpost FHeq bd + | FHeq, None -> f_bdHoareF fpre f fpost FHeq bd + | FHge, Some bd -> f_bdHoareF fpre f fpost FHge bd + | FHge, None -> f_bdHoareF fpre f fpost FHge bd + +(* -------------------------------------------------------------------- *) +(* Pure core shared by the rule and its checker. Its side conditions (the + last instruction is a call, the bound given to the procedure depends + neither on local variables nor on variables written before the call, no + optional bound for an upper bound) are part of it, so the checker + re-validates them. Their failures are the user-facing messages. *) +let bdhoare_call_subgoals (hyps : LDecl.hyps) (bhs : bdHoareS) (n : bdhoare_call) = + let env = LDecl.toenv hyps in + let (lp,f,args),s = + match s_last destr_call bhs.bhs_s with + | None -> failwith "invalid last instruction" + | Some x -> x in + let fpre, fpost, opt_bd = n.bhcall_pre, n.bhcall_post, n.bhcall_bd in + let m = fpre.m in + let fsig = (Fun.by_xpath f env).f_sig in + let bhs_bd = ss_inv_rebind (bhs_bd bhs) m in + let bhs_po = ss_inv_rebind (bhs_po bhs) m in + let bhs_pr = ss_inv_rebind (bhs_pr bhs) m in + + (* The bound of the specification of the called procedure (the bound of + the conclusion, or [opt_bd]) is interpreted in the memory the procedure + starts from: after [s], and with the local variables of the callee. + The bound of the conclusion is interpreted in the initial memory, with + the local variables of the caller. The two coincide only if this bound + depends neither on local variables nor on variables written by [s]. *) + let callee_bd = odfl bhs_bd opt_bd in + let fv_bd = PV.fv env callee_bd.m callee_bd.inv in + + if List.exists (fun (pv, _) -> is_loc pv) (fst (PV.elements fv_bd)) then + failwith "The bound cannot depend on local variables"; + + if not (PV.indep env (s_write env s) fv_bd) then + failwith + "The bound cannot depend on variables written by the \ + statements preceding the call"; + + (* The function satisfies the specification *) + let f_concl = + bdhoare_call_spec fpre fpost f bhs.bhs_cmp bhs_bd opt_bd in + + (* The wp *) + let pvres = pv_res in + let vres = EcIdent.create "result" in + let fres = {m;inv=f_local vres fsig.fs_ret} in + let post = EcPlCall.wp_asgn_call env lp fres bhs_po in + let fpost = map_ss_inv2 (PVM.subst1 env pvres m) fres fpost in + let modi = f_write env f in + let post = + match bhs.bhs_cmp with + | FHle -> map_ss_inv2 f_imp_simpl post fpost + | FHge -> map_ss_inv2 f_imp_simpl fpost post + + | FHeq when f_equal bhs_bd.inv f_r0 -> + map_ss_inv2 f_imp_simpl post fpost + + | FHeq when f_equal bhs_bd.inv f_r1 -> + map_ss_inv2 f_imp_simpl fpost post + + | FHeq -> map_ss_inv2 f_iff_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 = EcPlCall.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 concl = + let _,mt = bhs.bhs_m in + match bhs.bhs_cmp, opt_bd with + | FHle, None -> + let post =empty_hs post in + f_hoareS mt bhs_pr s post + | FHeq, Some bd -> + f_bdHoareS mt bhs_pr s post bhs.bhs_cmp (map_ss_inv2 f_real_div bhs_bd bd) + | FHeq, None -> + f_bdHoareS mt bhs_pr s post bhs.bhs_cmp {m;inv=f_r1} + | FHge, Some bd -> + f_bdHoareS mt bhs_pr s post bhs.bhs_cmp (map_ss_inv2 f_real_div bhs_bd bd) + | FHge, None -> + f_bdHoareS mt bhs_pr s post FHeq {m;inv=f_r1} + | _, _ -> assert false + in + + [f_concl; concl] + +(* -------------------------------------------------------------------- *) +(* Rule (TCB). *) +let t_bdhoare_call (n : bdhoare_call) (tc : tcenv1) = + let bhs = tc1_as_bdhoareS tc in + ignore (tc1_last_call tc bhs.bhs_s : _ * _); + let sg = + try bdhoare_call_subgoals (FApi.tc1_hyps tc) bhs n + with Failure msg -> tc_error !!tc "%s" msg in + FApi.xrule1 tc (RBdHoareCall n) sg + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | RBdHoareCall n -> + Some (EcPlRecheck.checker_of "bdhoare-call" pf_as_bdhoareS + (fun hyps bhs -> bdhoare_call_subgoals hyps bhs n)) + | _ -> None) + +(* -------------------------------------------------------------------- *) +(* Elaboration: the goal is known to be a [bdHoareS]. Types the cut of + [call]: the specification of the last call. *) +let process_bdhoare_call_cut (side : oside) (info : call_info) (tc : tcenv1) = + let hyps, concl = FApi.tc1_flat tc in + let bhs = destr_bdHoareS concl in + let last_f () = proj3_2 (fst (tc1_last_call tc bhs.bhs_s)) in + (* No optional bound: the specification is built without failure. *) + let spec fpre fpost f = + bdhoare_call_spec fpre fpost f bhs.bhs_cmp + (ss_inv_rebind (bhs_bd bhs) fpre.m) None in + + match info with + | CI_spec (pre, epost) -> + if not (is_none side) then + tc_error !!tc "side can only be given for prhl judgements"; + let f = last_f () in + let m = EcIdent.create "&hr" in + let penv, qenv = LDecl.hoareF m f hyps in + let pre = TTC.pf_process_form !!tc penv tbool pre in + let post = TTC.pf_process_form !!tc qenv tbool epost.pnormal in + (spec {m;inv=pre} {m;inv=post} f, t_id) + + | CI_inv inv -> + if not (is_none side) then + tc_error !!tc "cannot specify side for call with invariants"; + let m = fst bhs.bhs_m in + let f = last_f () in + let hyps = LDecl.push_active_ss (EcMemory.abstract m) hyps in + let inv = TTC.pf_process_form !!tc hyps tbool inv in + let inv = {m; inv} in + let t_spec tc = + FApi.t_firsts t_trivial 2 (EcPhlFun.t_fun (Inv_ss inv) tc) in + (spec inv inv f, t_spec) + + | CI_upto _ -> + if not (is_none side) then + tc_error !!tc "cannot specify side for call with invariants"; + tc_error !!tc "the conclusion is not an equiv" diff --git a/src/phl/rules/bdhoare/ecBdHoareCall.mli b/src/phl/rules/bdhoare/ecBdHoareCall.mli new file mode 100644 index 000000000..d66280ad9 --- /dev/null +++ b/src/phl/rules/bdhoare/ecBdHoareCall.mli @@ -0,0 +1,75 @@ +(* -------------------------------------------------------------------- *) +open EcParsetree +open EcCoreGoal +open EcCoreGoal.FApi +open EcAst + +(* ==================================================================== *) +(* Rules (trusted) *) + +(* The bdhoare [call] rule is kept with its historical statement, on + [c; lv <@ f(a)]: an implicit [seq] before the call and an implicit + framing of the prefix's postcondition over [mod f], the variables + written by [f]. Its [seq] could not be made explicit with + [EcBdHoareSeq.t_bdhoare_seq] without changing its premises: that rule + also bounds the runs of the prefix ending outside the intermediate + assertion (premises (G1) / (G2), the bound (B)), and asks that the + prefix does not change the bound of the suffix (N), which this rule + does not state (the second is a side condition here). *) + +type bdhoare_call = { + bhcall_pre : ss_inv; (* precondition P of the procedure *) + bhcall_post : ss_inv; (* postcondition Q of the procedure *) + bhcall_bd : ss_inv option; (* bound b of the procedure, if not d *) +} + +(* [t_bdhoare_call { bhcall_pre = P; bhcall_post = Q; bhcall_bd = ob }] — + call, [~] the goal's comparison and [d] its bound: + + phoare [f : P ==> Q] ~ b (b := ob when given, d otherwise) + J [c : P0 ==> P[arg := a] /\ W] + ------------------------------------------------- + phoare [c; lv <@ f(a) : P0 ==> R] ~ d + + W := forall result, forall (mod f), C[res := result, lv := result] + + where [/\] is the asymmetric conjunction [&&], built with the + simplifying constructors, and, by cases on [~ d] and [ob]: + + ~ d ob C J [c : P0 ==> X] + <= d none R => Q hoare [c : P0 ==> X] + = d none Q <=> R [1] phoare [c : P0 ==> X] = 1 + >= d none Q => R phoare [c : P0 ==> X] = 1 + = d / >= d some b as above phoare [c : P0 ==> X] ~ d / b + + [1] [R => Q] when [d] is syntactically [0%r], [Q => R] when it is + [1%r]. Side conditions, in order (each failing with its message): the + last instruction is a call; [b] does not depend on local variables + (it is read in the memory of [f], with the locals of the callee) nor + on the variables written by [c] (#1189); [ob] is not given for [<=]. + + Composite statement (implicit [seq] and framing, see above). Soundness: + with [ob = Some b], the runs of [c] ending outside [P[arg := a] /\ W] + are not accounted for, and [d / b] is [0] for [b = 0]: the conclusion + does not follow for [=], nor for [>=] when [b <= 0]. This form is not + reachable from the surface tactics, which never give [ob]. + + Node: [RBdHoareCall { bhcall_pre = P; bhcall_post = Q; bhcall_bd = ob }]. + Checker: "bdhoare-call". *) +val t_bdhoare_call : bdhoare_call -> backward + +(* ==================================================================== *) +(* Elaboration *) + +(* The cut of [call] on a [bdHoareS] goal, as [(spec, t)]: [spec] is the + specification of the procedure [f] called last, with the comparison and + bound of the goal, [t] the tactic run on it once the cut is applied. + - [call (_ : P ==> Q)] (no side): [P] and [Q] typed in the memory of + [f]; [spec] is [phoare [f : P ==> Q] ~ d], [t] the identity; + - [call (: I)] (no side): [I] typed in an abstract memory (global + variables only); [spec] is [phoare [f : I ==> I] ~ d], [t] is + [proc I] (or [proc] for a concrete [f], see [EcPhlFun.t_fun]) + followed by [trivial] on its first two goals; + - [call (: bad, P, Q)]: fails (an equiv is expected). *) +val process_bdhoare_call_cut : + oside -> call_info -> tcenv1 -> EcFol.form * backward diff --git a/src/phl/rules/ecPlCall.ml b/src/phl/rules/ecPlCall.ml new file mode 100644 index 000000000..608eb7360 --- /dev/null +++ b/src/phl/rules/ecPlCall.ml @@ -0,0 +1,38 @@ +(* -------------------------------------------------------------------- *) +open EcAst +open EcTypes +open EcFol +open EcPV + +open EcCoreGoal +open EcLowPhlGoal + +(* -------------------------------------------------------------------- *) +let wp_asgn_call ?mc env lv (res : ss_inv) (post : ss_inv) = + assert (res.m = post.m); + let m = post.m in + match lv with + | None -> post + | Some lv -> + 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 single_call (name : string) (s : stmt) = + match s.s_node with + | [{ i_node = Scall (lv, f, args) }] -> (lv, f, args) + | _ -> failwith (name ^ ": the statement is not a single call") + +(* -------------------------------------------------------------------- *) +let call_error env tc f1 f2 = + tc_error_lazy !!tc (fun fmt -> + let ppe = EcPrinting.PPEnv.ofenv env in + Format.fprintf fmt + "call cannot be used with a lemma referring to `%a': \ + the last statement is a call to `%a'" + (EcPrinting.pp_funname ppe) f1 + (EcPrinting.pp_funname ppe) f2) diff --git a/src/phl/rules/ecPlCall.mli b/src/phl/rules/ecPlCall.mli new file mode 100644 index 000000000..efb159def --- /dev/null +++ b/src/phl/rules/ecPlCall.mli @@ -0,0 +1,28 @@ +(* -------------------------------------------------------------------- *) +open EcPath +open EcAst +open EcEnv + +(* -------------------------------------------------------------------- *) +(* Computations shared by the [call] rules of every logic + ([EcCall]). *) + +(* [wp_asgn_call ?mc env lv r Q]: [Q] with the result [r] assigned to the + left-value [lv] of the call (let-bound), [Q] itself when the call has no + left-value. [r] and [Q] are in the same memory. [~mc] gives the two + memories of a two-sided [Q]. *) +val wp_asgn_call : + ?mc:(memory * memory) + -> env -> lvalue option -> ss_inv -> ss_inv -> ss_inv + +(* [subst_args_call env m a s] extends [s] with [arg{m} := a{m}]. *) +val subst_args_call : + env -> memory -> expr -> EcPV.PVM.subst -> EcPV.PVM.subst + +(* [call_error env tc f1 f2]: fails with the error of [call] given a + specification of [f1] when the last statement calls [f2]. *) +val call_error : env -> EcCoreGoal.tcenv1 -> xpath -> xpath -> 'a + +(* [single_call name s]: [s] is a single call [lv <@ f(a)], returned as + [(lv, f, a)]; fails with [Failure ": ..."] otherwise. *) +val single_call : string -> stmt -> lvalue option * xpath * expr list diff --git a/src/phl/rules/ehoare/ecEHoareCall.ml b/src/phl/rules/ehoare/ecEHoareCall.ml new file mode 100644 index 000000000..2d2cfe2f7 --- /dev/null +++ b/src/phl/rules/ehoare/ecEHoareCall.ml @@ -0,0 +1,246 @@ +(* -------------------------------------------------------------------- *) +open EcUtils +open EcParsetree +open EcAst +open EcTypes +open EcFol +open EcEnv +open EcPV +open EcSubst + +open EcCoreGoal +open EcLowGoal +open EcLowPhlGoal + +module PT = EcProofTerm +module TTC = EcProofTyping + +(* -------------------------------------------------------------------- *) +(* Parameters of the ehoare [call] rule: the specification of the called + procedure. *) +type ehoare_call = { + ehcall_pre : ss_inv; (* pre-expectation P of the procedure *) + ehcall_post : ss_inv; (* post-expectation Q of the procedure *) +} + +type EcCoreGoal.rule += REHoareCall of ehoare_call + +(* -------------------------------------------------------------------- *) +(* The pre- and post-expectations of [lv <@ f(a)] given the specification + [P ==> Q] of [f] (in memory [m]): [(P[arg := a], Q[res := lv])]. + Fails with [Failure] (user-facing messages) when [lv] assigns a global + variable, or when the call has no left-value and [Q] reads [res]. *) +let ehoare_call_pre_post env (m : memory) (n : ehoare_call) (lp, _, args) = + let fpre = ss_inv_rebind n.ehcall_pre m in + let fpost = ss_inv_rebind n.ehcall_post m in + (* Ensure that all asigned variables are locals *) + let all_loc = + match lp with + | None -> true + | Some(LvVar (v,_)) -> EcTypes.is_loc v + | Some(LvTuple vs) -> List.for_all (fun (v,_) -> EcTypes.is_loc v) vs in + if not all_loc then + failwith "ehoare call core rule: only local variables are supported on the left side of a call"; + (* The wp *) + let fres = + match lp with + | None -> None + | Some (LvVar (v,ty)) -> Some (f_pvar v ty m) + | Some (LvTuple vs) -> Some (map_ss_inv f_tuple (List.map (fun (v,ty) -> f_pvar v ty m) vs)) in + let wppost = + omap_dfl (fun fres -> map_ss_inv2 (PVM.subst1 env pv_res m) fres fpost) fpost fres in + let fv = PV.fv env m wppost.inv in + if PV.mem_pv env pv_res fv then + failwith + "ehoare call core rule: the post condition of the function depend on res but the result is not assigned"; + + let spre = EcPlCall.subst_args_call env m (e_tuple args) PVM.empty in + let wppre = map_ss_inv1 (PVM.subst env spre) fpre in + (wppre, wppost) + +(* -------------------------------------------------------------------- *) +(* Pure core shared by the rule and its checker. Its side conditions (the + statement is a single call, assigning local variables only, and the pre- + and post-expectations are the expected ones) are part of it, so the + checker re-validates them. *) +let ehoare_call_subgoals (hyps : LDecl.hyps) (hs : eHoareS) (n : ehoare_call) = + let env = LDecl.toenv hyps in + let m = fst hs.ehs_m in + let (_, f, _) as call = EcPlCall.single_call "ehoare-call" hs.ehs_s in + let wppre, wppost = ehoare_call_pre_post env m n call in + + let error kind expected actual = + let env = EcEnv.Memory.push_active_ss hs.ehs_m env in + let ppe = EcPrinting.PPEnv.ofenv env in + failwith (Format.asprintf + "ehoare call core rule: wrong %s-condition %a instead %a" kind + (EcPrinting.pp_form ppe) actual (EcPrinting.pp_form ppe) expected) in + + if not (EcReduction.ss_inv_is_conv hyps (ehs_po hs) wppost) then + error "post" wppost.inv (ehs_po hs).inv; + if not (EcReduction.ss_inv_is_conv hyps (ehs_pr hs) wppre) then + error "pre" wppre.inv (ehs_pr hs).inv; + + [f_eHoareF (ss_inv_rebind n.ehcall_pre m) f (ss_inv_rebind n.ehcall_post m)] + +(* -------------------------------------------------------------------- *) +(* Rule (TCB). *) +let t_ehoare_call (n : ehoare_call) (tc : tcenv1) = + let hs = tc1_as_ehoareS tc in + let sg = + try ehoare_call_subgoals (FApi.tc1_hyps tc) hs n + with Failure msg -> tc_error !!tc "%s" msg in + FApi.xrule1 tc (REHoareCall n) sg + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | REHoareCall n -> + Some (EcPlRecheck.checker_of "ehoare-call" pf_as_ehoareS + (fun hyps hs -> ehoare_call_subgoals hyps hs n)) + | _ -> None) + +(* -------------------------------------------------------------------- *) +(* The pre- and post-expectations of the last call of the goal, for the + derived tactics (failures as tactic errors). *) +let tc1_ehoare_call_pre_post (n : ehoare_call) (tc : tcenv1) = + let env = FApi.tc1_env tc in + let hs = tc1_as_ehoareS tc in + let call, _ = tc1_last_call tc hs.ehs_s in + try ehoare_call_pre_post env (fst hs.ehs_m) n call + with Failure msg -> tc_error !!tc "%s" msg + +(* -------------------------------------------------------------------- *) +(* Derived (no proof-node): on [c; lv <@ f(a)], [seq] before the call with + its pre-expectation, then close the call with the rule. The + specification premise comes first. *) +let t_ehoare_call_last (n : ehoare_call) (tc : tcenv1) = + let wppre, _ = tc1_ehoare_call_pre_post n tc in + let at = EcMatching.Position.(GapBefore cpos1_last) in + FApi.t_swap_goals 0 1 + (FApi.t_seqsub + (EcEHoareSeq.t_ehoare_seq { ehsr_at = at; ehsr_mid = wppre }) + [t_id; t_ehoare_call n] + tc) + +(* -------------------------------------------------------------------- *) +(* Derived (no proof-node): as [t_ehoare_call_last], the intermediate + pre-expectation being [fc] applied to that of the call, and the call + being reduced to the rule by the concave consequence. + TEMPORARY: the concave consequence comes from the not-yet-migrated + [EcPhlConseq]. *) +let t_ehoare_call_concave (fc : ss_inv) (n : ehoare_call) (tc : tcenv1) = + let wppre, wppost = tc1_ehoare_call_pre_post n tc in + let at = EcMatching.Position.(GapBefore cpos1_last) in + let mid = map_ss_inv2 (fun wppre f -> f_app_simpl f [wppre] txreal) wppre fc in + let t_call = + FApi.t_seqsub (EcPhlConseq.t_ehoareS_concave fc wppre wppost) + [t_id; t_id; t_id; t_ehoare_call n] in + FApi.t_sub [t_call; t_id] + (FApi.t_swap_goals 0 1 + (EcEHoareSeq.t_ehoare_seq { ehsr_at = at; ehsr_mid = mid } tc)) + +(* -------------------------------------------------------------------- *) +(* Elaboration: the goal is known to be an [eHoareS]. Types the cut of + [call]: the specification of the last call. *) +let process_ehoare_call_cut (side : oside) (info : call_info) (tc : tcenv1) = + let hyps, concl = FApi.tc1_flat tc in + let hs = destr_eHoareS concl in + let last_f () = proj3_2 (fst (tc1_last_call tc hs.ehs_s)) in + + match info with + | CI_spec (pre, epost) -> + if not (is_none side) then + tc_error !!tc "the conclusion is not a hoare or an equiv"; + let f = last_f () in + let m = EcIdent.create "&hr" in + let penv, qenv = LDecl.hoareF m f hyps in + let pre = TTC.pf_process_form !!tc penv txreal pre in + let post = TTC.pf_process_form !!tc qenv txreal epost.pnormal in + (f_eHoareF {m;inv=pre} f {m;inv=post}, t_id) + + | CI_inv inv -> + if not (is_none side) then + tc_error !!tc "cannot specify side for call with invariants"; + let m = fst hs.ehs_m in + let f = last_f () in + let hyps = LDecl.push_active_ss (EcMemory.abstract m) hyps in + let inv = TTC.pf_process_form !!tc hyps txreal inv in + let inv = {m; inv} in + let t_spec tc = + FApi.t_firsts t_trivial 2 (EcPhlFun.t_fun (Inv_ss inv) tc) in + (f_eHoareF inv f inv, t_spec) + + | CI_upto _ -> + if not (is_none side) then + tc_error !!tc "cannot specify side for call with invariants"; + tc_error !!tc "the conclusion is not an equiv" + +(* -------------------------------------------------------------------- *) +(* Elaboration: [call /fc (spec)], the goal being known to be an + [eHoareS]. *) +let process_ehoare_call_concave (fc, info) tc = + let fc = + let hs = tc1_as_ehoareS tc in + let env = LDecl.push_active_ss hs.ehs_m (FApi.tc1_hyps tc) in + {m=fst hs.ehs_m;inv=TTC.pf_process_form !!tc env (tfun txreal txreal) fc} in + + let subtactic = ref t_id in + + (* As for [call] ([process_ehoare_call_cut]), the specification is typed + in the memories of the called procedure and the invariant in an + abstract memory: the local variables of the caller are not in + scope. *) + let process_cut tc info = + match info with + | CI_spec _ -> + fst (process_ehoare_call_cut None info tc) + + | CI_inv _ -> + let spec, t_spec = process_ehoare_call_cut None info tc in + subtactic := t_spec; + spec + + | _ -> + tc_error !!tc "cannot supply additional information for call /" + + in + + let pt = PT.tc1_process_full_pterm_cut ~prcut:(process_cut tc) tc info + in + + let pt = + let rec doit pt = + match TTC.destruct_product ~reduce:true (FApi.tc1_hyps tc) pt.PT.ptev_ax with + | None -> pt + | Some _ -> doit (EcProofTerm.apply_pterm_to_hole pt) + in doit pt in + + let pt, ax = + if not (PT.can_concretize pt.PT.ptev_env) then + tc_error !!tc "cannot infer all placeholders"; + PT.concretize pt in + + let t_call ax tc = + let env = FApi.tc1_env tc in + let hs = tc1_as_ehoareS tc in + match ax.f_node with + | FeHoareF hf -> + let (_, f, _), _ = tc1_last_call tc hs.ehs_s in + if not (EcEnv.NormMp.x_equal env hf.ehf_f f) then + EcPlCall.call_error env tc hf.ehf_f f; + t_ehoare_call_concave fc + { ehcall_pre = ehf_pr hf; ehcall_post = ehf_po hf; } tc + | _ -> tc_error !!tc "call: invalid goal shape" in + + FApi.t_seqsub + (t_call ax) + [ EcPhlConseq.t_concave_incr; + t_trivial; (* pre *) + t_trivial; (* post *) + FApi.t_seqs + [EcLowGoal.Apply.t_apply_bwd_hi ~dpe:true pt; + !subtactic; t_trivial]; + t_id] + tc diff --git a/src/phl/rules/ehoare/ecEHoareCall.mli b/src/phl/rules/ehoare/ecEHoareCall.mli new file mode 100644 index 000000000..33cd1a35d --- /dev/null +++ b/src/phl/rules/ehoare/ecEHoareCall.mli @@ -0,0 +1,100 @@ +(* -------------------------------------------------------------------- *) +open EcParsetree +open EcCoreGoal +open EcCoreGoal.FApi +open EcAst + +(* ==================================================================== *) +(* Rules (trusted) *) + +type ehoare_call = { + ehcall_pre : ss_inv; (* pre-expectation P of the procedure *) + ehcall_post : ss_inv; (* post-expectation Q of the procedure *) +} + +(* [t_ehoare_call { ehcall_pre = P; ehcall_post = Q }] — single call: + + ehoare [f : P ==> Q] + --------------------------------------------- + ehoare [lv <@ f(a) : P[arg := a] ==> Q[res := lv]] + + No framing: the post-expectation of the goal is the one of [f], with + the result read in [lv]. Side conditions, in order: the statement is + the single call [lv <@ f(a)]; [lv] assigns local variables only; when + the call has no left-value, [Q] does not read [res]; the post- and the + pre-expectation of the goal are convertible to the ones displayed + (otherwise fails, with the historical messages of the "ehoare call core + rule"). + + Soundness: [P] and [Q] are read in the memory of [f] in the premise and + in the memory of the goal in the conclusion; the rule is sound when they + read no local variable other than [arg] / [res]. The specifications of + [call (_ : P ==> Q)] and [call (: I)] are typed so; the cut of + [call /fc] is not (see [process_ehoare_call_concave]). + + Node: [REHoareCall { ehcall_pre = P; ehcall_post = Q }]. + Checker: "ehoare-call". *) +val t_ehoare_call : ehoare_call -> backward + +(* ==================================================================== *) +(* Derived tactics *) + +(* [t_ehoare_call_last { ehcall_pre = P; ehcall_post = Q }] — on + [ehoare [c; lv <@ f(a) : P0 ==> R]] (the side conditions on [lv] and + [Q] of [t_ehoare_call] are checked first): + 1. [EcEHoareSeq.t_ehoare_seq] before the call, with intermediate + expectation [P[arg := a]], giving + (a) ehoare [c : P0 ==> P[arg := a]] — left open, + (b) ehoare [lv <@ f(a) : P[arg := a] ==> R]; + 2. [t_ehoare_call] on (b) (failing unless [R] is convertible to + [Q[res := lv]]), giving + (c) ehoare [f : P ==> Q] — left open. + Visible goals: (c), then (a). Emits no node of its own. *) +val t_ehoare_call_last : ehoare_call -> backward + +(* [t_ehoare_call_concave fc { ehcall_pre = P; ehcall_post = Q }] — on + [ehoare [c; lv <@ f(a) : P0 ==> R]], with [fc] a function on + expectations: + 1. [EcEHoareSeq.t_ehoare_seq] before the call, with intermediate + expectation [fc (P[arg := a])], giving + (a) ehoare [c : P0 ==> fc (P[arg := a])] — left open, + (b) ehoare [lv <@ f(a) : fc (P[arg := a]) ==> R]; + 2. on (b), the concave consequence [EcPhlConseq.t_ehoareS_concave fc] + to [ehoare [lv <@ f(a) : P[arg := a] ==> Q[res := lv]]], whose + three side conditions are left open; + 3. [t_ehoare_call] on the latter, giving + (c) ehoare [f : P ==> Q] — left open. + Visible goals: the three side conditions of step 2, (c), then (a). + Emits no node of its own. TEMPORARY: step 2 uses the not-yet-migrated + [EcPhlConseq]. *) +val t_ehoare_call_concave : ss_inv -> ehoare_call -> backward + +(* ==================================================================== *) +(* Elaboration *) + +(* The cut of [call] on an [eHoareS] goal, as [(spec, t)]: [spec] is the + specification of the procedure [f] called last, [t] the tactic run on it + once the cut is applied. + - [call (_ : P ==> Q)] (no side): [P] and [Q] typed as expectations in + the memory of [f]; [spec] is [ehoare [f : P ==> Q]], [t] the + identity; + - [call (: I)] (no side): [I] typed as an expectation in an abstract + memory (global variables only); [spec] is [ehoare [f : I ==> I]], [t] + is [proc I] (or [proc] for a concrete [f], see [EcPhlFun.t_fun]) + followed by [trivial] on its first two goals; + - [call (: bad, P, Q)]: fails (an equiv is expected). *) +val process_ehoare_call_cut : + oside -> call_info -> tcenv1 -> EcFol.form * backward + +(* [call /fc spec], on an [eHoareS] goal: [fc] is typed as a function on + expectations, in the memory of the goal; [spec] is a proof term of an + ehoare specification of the procedure called last (or a cut + [(_ : P ==> Q)] / [(: I)], typed as for [call]: the specification in + the memories of the procedure, the invariant in an abstract memory, so + that the local variables of the caller are not in scope). Applies + [t_ehoare_call_concave], closes the first of its goals with + [EcPhlConseq.t_concave_incr] and the next two with [trivial], applies + [spec] to (c) (running [proc I] then [trivial] for an invariant) and + leaves (a). *) +val process_ehoare_call_concave : + pformula * call_info gppterm -> backward diff --git a/src/phl/rules/equiv/ecEquivCall.ml b/src/phl/rules/equiv/ecEquivCall.ml new file mode 100644 index 000000000..6b999cf58 --- /dev/null +++ b/src/phl/rules/equiv/ecEquivCall.ml @@ -0,0 +1,388 @@ +(* -------------------------------------------------------------------- *) +open EcUtils +open EcParsetree +open EcAst +open EcTypes +open EcModules +open EcFol +open EcEnv +open EcPV +open EcSubst + +open EcCoreGoal +open EcLowGoal +open EcLowPhlGoal + +module TTC = EcProofTyping + +(* -------------------------------------------------------------------- *) +(* Parameters of the two-sided equiv [call] rule: the specification of the + called procedures. *) +type equiv_call = { + ecall_pre : ts_inv; (* precondition P of the procedures *) + ecall_post : ts_inv; (* postcondition Q of the procedures *) +} + +(* Parameters of the one-sided equiv [call] rule: the side of the call and + the specification of the called procedure. *) +type equiv_call_onesided = { + ecallos_side : side; (* side of the call *) + ecallos_pre : ss_inv; (* precondition P of the procedure *) + ecallos_post : ss_inv; (* postcondition Q of the procedure *) +} + +type EcCoreGoal.rule += + | REquivCall of equiv_call + | REquivCallOneSided of equiv_call_onesided + +(* -------------------------------------------------------------------- *) +(* Weakest precondition of [lvL <@ fL(aL) ~ lvR <@ fR(aR)] for the relation + [post], given the specification [P ==> Q] of [fL ~ fR]: + P[arg<1> := aL, arg<2> := aR] /\ + forall resultL resultR, forall (mod fL)<1> (mod fR)<2>, + Q[res<1> := resultL, res<2> := resultR] => + post[lvL<1> := resultL, lvR<2> := resultR] + [mods] are extra variables to generalize over, on each side. *) +let equiv_call_wp + (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 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 + + 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 = + {ml; mr; inv = post} + |> map_ts_inv_left2 (EcPlCall.wp_asgn_call ~mc:(ml, mr) env lpl) fresl + |> map_ts_inv_right2 (EcPlCall.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 = EcPlCall.subst_args_call env ml (e_tuple argsl) PVM.empty in + let spre = EcPlCall.subst_args_call env mr (e_tuple argsr) spre in + + f_anda_simpl (PVM.subst env spre fpre) post + +(* -------------------------------------------------------------------- *) +(* Weakest precondition of [lv <@ f(a) ~ skip] (for [`Left]; symmetrically + for [`Right]) for the relation [post], given the specification + [P ==> Q] of [f] (one-sided, in the memory of [side]): + P[arg<1> := a] /\ + forall result, forall (mod f)<1>, + Q[res<1> := result] => post[lv<1> := result] *) +let equiv_call_onesided_wp + (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 (EcPlCall.wp_asgn_call ~mc:(ml,mr) env lv)) + (map_ts_inv_right2 (EcPlCall.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 = EcPlCall.subst_args_call env me (e_tuple args) PVM.empty in + + f_anda_simpl (PVM.subst env spre fpre) post + +(* -------------------------------------------------------------------- *) +(* Pure cores shared by the rules and their checkers. Their side + conditions (the statements are single calls — resp. a single call and + the empty statement —, and the precondition is the weakest + precondition) are part of them, so the checkers re-validate them. *) +let equiv_call_subgoals (hyps : LDecl.hyps) (es : equivS) (n : equiv_call) = + let ml, mr = fst es.es_ml, fst es.es_mr in + let fpre = ts_inv_rebind n.ecall_pre ml mr in + let fpost = ts_inv_rebind n.ecall_post ml mr in + let (_, fl, _) as call_l = EcPlCall.single_call "equiv-call" es.es_sl in + let (_, fr, _) as call_r = EcPlCall.single_call "equiv-call" es.es_sr in + let wp = + equiv_call_wp hyps (ml, mr) (fpre.inv, fpost.inv) call_l call_r + (es_po es).inv in + if not (EcReduction.is_conv hyps (es_pr es).inv wp) then + failwith "equiv-call: the precondition is not the expected one"; + [f_equivF fpre fl fr fpost] + +let equiv_call_onesided_subgoals + (hyps : LDecl.hyps) (es : equivS) (n : equiv_call_onesided) += + let side = n.ecallos_side in + let ml, mr = fst es.es_ml, fst es.es_mr in + let me = sideif side ml mr in + let fpre = ss_inv_rebind n.ecallos_pre me in + let fpost = ss_inv_rebind n.ecallos_post me in + let s, so = sideif side (es.es_sl, es.es_sr) (es.es_sr, es.es_sl) in + let (_, f, _) as call = EcPlCall.single_call "equiv-call-onesided" s in + if not (List.is_empty so.s_node) then + failwith "equiv-call-onesided: the other statement is not empty"; + let wp = + equiv_call_onesided_wp hyps side (ml, mr) (fpre.inv, fpost.inv) call + (es_po es).inv in + if not (EcReduction.is_conv hyps (es_pr es).inv wp) then + failwith "equiv-call-onesided: the precondition is not the expected one"; + [f_bdHoareF fpre f fpost FHeq { m = fpost.m; inv = f_r1; }] + +(* -------------------------------------------------------------------- *) +(* Rules (TCB). *) +let t_equiv_call (n : equiv_call) (tc : tcenv1) = + let es = tc1_as_equivS tc in + let sg = + try equiv_call_subgoals (FApi.tc1_hyps tc) es n + with Failure msg -> tc_error !!tc "%s" msg in + FApi.xrule1 tc (REquivCall n) sg + +let t_equiv_call_onesided (n : equiv_call_onesided) (tc : tcenv1) = + let es = tc1_as_equivS tc in + let sg = + try equiv_call_onesided_subgoals (FApi.tc1_hyps tc) es n + with Failure msg -> tc_error !!tc "%s" msg in + FApi.xrule1 tc (REquivCallOneSided n) sg + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | REquivCall n -> + Some (EcPlRecheck.checker_of "equiv-call" pf_as_equivS + (fun hyps es -> equiv_call_subgoals hyps es n)) + | REquivCallOneSided n -> + Some (EcPlRecheck.checker_of "equiv-call-onesided" pf_as_equivS + (fun hyps es -> equiv_call_onesided_subgoals hyps es n)) + | _ -> None) + +(* -------------------------------------------------------------------- *) +(* Derived (no proof-node): [seq] before the final calls (resp. before the + final call on one side, at the end of the other one), with their + weakest precondition as intermediate relation, then close the calls + with the rules. The specification premise comes first. *) +let t_equiv_call_last (n : equiv_call) (tc : tcenv1) = + 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 n.ecall_pre ml mr in + let fpost = ts_inv_rebind n.ecall_post ml mr in + let call_l, _ = tc1_last_call tc es.es_sl in + let call_r, _ = tc1_last_call tc es.es_sr in + let mid = + equiv_call_wp hyps (ml, mr) (fpre.inv, fpost.inv) call_l call_r + (es_po es).inv in + let at = EcMatching.Position.gap_before_last_n 1 in + FApi.t_swap_goals 0 1 + (FApi.t_seqsub + (EcEquivSeq.t_equiv_seq + { esr_at = (at, at); esr_mid = { ml; mr; inv = mid; } }) + [t_id; t_equiv_call n] + tc) + +let t_equiv_call_onesided_last (n : equiv_call_onesided) (tc : tcenv1) = + let hyps = FApi.tc1_hyps tc in + let es = tc1_as_equivS tc in + let side = n.ecallos_side in + let ml, mr = fst es.es_ml, fst es.es_mr in + let me = sideif side ml mr in + let fpre = ss_inv_rebind n.ecallos_pre me in + let fpost = ss_inv_rebind n.ecallos_post me in + let call, _ = tc1_last_call tc (sideif side es.es_sl es.es_sr) in + let mid = + equiv_call_onesided_wp hyps side (ml, mr) (fpre.inv, fpost.inv) call + (es_po es).inv in + let at = EcMatching.Position.(sideif side + (gap_before_last_n 1, codegap1_end) + (codegap1_end, gap_before_last_n 1)) in + FApi.t_swap_goals 0 1 + (FApi.t_seqsub + (EcEquivSeq.t_equiv_seq { esr_at = at; esr_mid = { ml; mr; inv = mid; } }) + [t_id; t_equiv_call_onesided n] + tc) + +(* -------------------------------------------------------------------- *) +(* The specification [equiv [fl ~ fr : ={arg} /\ I ==> ={res} /\ I]] of + [call (: I)] (with [={glob A}] for abstract procedures of [A]). *) +let equiv_call_inv_spec (pf : proofenv) env (inv : ts_inv) fl fr = + let ml, mr = inv.ml, inv.mr in + match NormMp.is_abstract_fun fl env with + | true -> + let (topl, _, _, sigl), + (topr, _, _ , sigr) = EcLowPhlGoal.abstract_info2 env fl fr in + let eqglob = ts_inv_eqglob topl ml topr mr in + let lpre = [eqglob;inv] in + let eq_params = + ts_inv_eqparams + sigl.fs_arg sigl.fs_anames ml + sigr.fs_arg sigr.fs_anames mr in + let eq_res = ts_inv_eqres sigl.fs_ret ml sigr.fs_ret mr in + let pre = map_ts_inv f_ands (eq_params::lpre) in + let post = map_ts_inv f_ands [eq_res; eqglob; inv] in + f_equivF pre fl fr post + + | false -> + let defl = EcEnv.Fun.by_xpath fl env in + let defr = EcEnv.Fun.by_xpath fr env in + let sigl, sigr = defl.f_sig, defr.f_sig in + + let error s tl tr = + let ppe = EcPrinting.PPEnv.ofenv env in + tc_error pf "@[The procedures do not have the same %s types:@]@;<2 2>\ + @[Left side: @[%a@]@,\ + Right side: @[%a@]@]@;<2 0>\ + A full contract cannot be inferred; consider providing a full contract using@;<2 2>\ + call (: ...==> ...)@," + s + (EcPrinting.pp_type ppe) tl + (EcPrinting.pp_type ppe) tr + in + + if not (EcReduction.EqTest.for_type env sigl.fs_arg sigr.fs_arg) + then error "argument" sigl.fs_arg sigr.fs_arg; + + if not (EcReduction.EqTest.for_type env sigl.fs_ret sigr.fs_ret) + then error "return" sigl.fs_ret sigr.fs_ret; + + let eq_params = + ts_inv_eqparams + sigl.fs_arg sigl.fs_anames ml + sigr.fs_arg sigr.fs_anames mr in + let eq_res = ts_inv_eqres sigl.fs_ret ml sigr.fs_ret mr in + let pre = map_ts_inv2 f_and eq_params inv in + let post = map_ts_inv2 f_and eq_res inv in + f_equivF pre fl fr post + +(* -------------------------------------------------------------------- *) +(* Elaboration: the goal is known to be an [equivS]. Types the cut of + [call]: the specification of the last call(s). *) +let process_equiv_call_cut (side : oside) (info : call_info) (tc : tcenv1) = + let hyps, concl = FApi.tc1_flat tc in + let es = destr_equivS concl in + let last_fs () = + let (_,fl,_) = fst (tc1_last_call tc es.es_sl) in + let (_,fr,_) = fst (tc1_last_call tc es.es_sr) in + (fl, fr) in + + match info, side with + | CI_spec (pre, epost), None -> + let fl, fr = last_fs () in + let (ml, mr) = (EcIdent.create "&1", EcIdent.create "&2") in + let penv, qenv = LDecl.equivF ml mr fl fr hyps in + let pre = TTC.pf_process_form !!tc penv tbool pre in + let post = TTC.pf_process_form !!tc qenv tbool epost.pnormal in + (f_equivF {ml;mr;inv=pre} fl fr {ml;mr;inv=post}, t_id) + + | CI_spec (pre, epost), Some side -> + let fstmt = sideif side es.es_sl es.es_sr in + let m = sideif side (EcIdent.create "&1") (EcIdent.create "&2") in + let (_,f,_) = fst (tc1_last_call tc fstmt) in + let penv, qenv = LDecl.hoareF m f hyps in + let pre = TTC.pf_process_form !!tc penv tbool pre in + let post = TTC.pf_process_form !!tc qenv tbool epost.pnormal in + (f_bdHoareF {m;inv=pre} f {m;inv=post} FHeq {m;inv=f_r1}, t_id) + + | (CI_inv _ | CI_upto _), Some _ -> + tc_error !!tc "cannot specify side for call with invariants" + + | CI_inv inv, None -> + let ml, mr = fst es.es_ml, fst es.es_mr in + let fl, fr = last_fs () in + let mel, mer = EcMemory.abstract ml, EcMemory.abstract mr in + let hyps = LDecl.push_active_ts mel mer hyps in + let env = LDecl.toenv hyps in + let inv = TTC.pf_process_form !!tc hyps tbool inv in + let inv = {ml;mr; inv} in + let t_spec tc = + FApi.t_firsts t_trivial 2 (EcPhlFun.t_fun (Inv_ts inv) tc) in + (equiv_call_inv_spec !!tc env inv fl fr, t_spec) + + | CI_upto info, None -> + let env = FApi.tc1_env tc in + let ml, mr = fst es.es_ml, fst es.es_mr in + let fl, fr = last_fs () in + let weakened_pre,bad,invP,invQ = EcPhlFun.process_fun_upto_info info tc in + let bad2 = ss_inv_generalize_as_right bad ml mr in + let invP = ts_inv_rebind invP ml mr in + let invQ = ts_inv_rebind invQ ml mr in + let (topl,fl,_,sigl), + (topr,fr,_ ,sigr) = EcLowPhlGoal.abstract_info2 env fl fr in + let eqglob = ts_inv_eqglob topl ml topr mr in + let lpre = [eqglob;invP] in + let eq_params = + ts_inv_eqparams + sigl.fs_arg sigl.fs_anames ml + sigr.fs_arg sigr.fs_anames mr in + let eq_res = ts_inv_eqres sigl.fs_ret ml sigr.fs_ret mr in + let pre = map_ts_inv3 f_if_simpl bad2 invQ (map_ts_inv f_ands (eq_params::lpre)) in + let post = map_ts_inv3 f_if_simpl bad2 invQ (map_ts_inv f_ands [eq_res;eqglob;invP]) in + let t_tr = FApi.t_or (t_assumption `Conv) t_trivial in + let t_spec tc = + FApi.t_firsts t_tr 3 + (EcPhlFun.t_equivF_abs_upto weakened_pre bad invP invQ tc) in + (f_equivF pre fl fr post, t_spec) diff --git a/src/phl/rules/equiv/ecEquivCall.mli b/src/phl/rules/equiv/ecEquivCall.mli new file mode 100644 index 000000000..b7fc09723 --- /dev/null +++ b/src/phl/rules/equiv/ecEquivCall.mli @@ -0,0 +1,145 @@ +(* -------------------------------------------------------------------- *) +open EcParsetree +open EcCoreGoal +open EcCoreGoal.FApi +open EcAst +open EcEnv + +(* ==================================================================== *) +(* Rules (trusted) *) + +type equiv_call = { + ecall_pre : ts_inv; (* precondition P of the procedures *) + ecall_post : ts_inv; (* postcondition Q of the procedures *) +} + +(* [t_equiv_call { ecall_pre = P; ecall_post = Q }] — two-sided call: + + equiv [fL ~ fR : P ==> Q] + ------------------------------------------------------------------ + equiv [lvL <@ fL(aL) ~ lvR <@ fR(aR) : P[arg<1> := aL, arg<2> := aR] /\ W ==> R] + + W := forall resultL resultR, forall (mod fL)<1> (mod fR)<2>, + Q[res<1> := resultL, res<2> := resultR] => + R[lvL<1> := resultL, lvR<2> := resultR] + + where [mod f] are the variables written by [f], and [/\] is the + asymmetric conjunction [&&], built with the simplifying constructors + ([equiv_call_wp]). Side conditions: both statements are single calls, + and the precondition is convertible to the one displayed (otherwise + fails). Soundness: [P] and [Q] read no local variable other than [arg] + / [res], as the typing of the specifications ensures (they are read in + the memories of [fL] / [fR] in the premise, of the goal in the + conclusion). + + Node: [REquivCall { ecall_pre = P; ecall_post = Q }]. + Checker: "equiv-call". *) +val t_equiv_call : equiv_call -> backward + +(* [equiv_call_wp hyps (ml, mr) (P, Q) ?mods callL callR R] is the + precondition of the conclusion of [t_equiv_call] (with [mods] + generalized too, on each side, in [W]). *) +val equiv_call_wp : + LDecl.hyps + -> memory * memory + -> form * form + -> ?mods:(EcPV.PV.t * EcPV.PV.t) + -> lvalue option * EcPath.xpath * expr list + -> lvalue option * EcPath.xpath * expr list + -> form + -> form + +type equiv_call_onesided = { + ecallos_side : side; (* side of the call *) + ecallos_pre : ss_inv; (* precondition P of the procedure *) + ecallos_post : ss_inv; (* postcondition Q of the procedure *) +} + +(* [t_equiv_call_onesided { ecallos_side = `Left; ecallos_pre = P; + ecallos_post = Q }] — one-sided call: + + phoare [f : P ==> Q] = 1%r + ------------------------------------------------------------- + equiv [lv <@ f(a) ~ skip : P<1>[arg<1> := a] /\ W ==> R] + + W := forall result, forall (mod f)<1>, + Q<1>[res<1> := result] => R[lv<1> := result] + + (symmetrically for [`Right]; [/\] is [&&], built with the simplifying + constructors, [equiv_call_onesided_wp]). Side conditions: that side is + a single call, the other one is empty, and the precondition is + convertible to the one displayed (otherwise fails). Soundness: as for + [t_equiv_call], [P] and [Q] read no local variable other than [arg] / + [res]. + + Node: [REquivCallOneSided { ecallos_side; ecallos_pre = P; + ecallos_post = Q }]. + Checker: "equiv-call-onesided". *) +val t_equiv_call_onesided : equiv_call_onesided -> backward + +(* [equiv_call_onesided_wp hyps side (ml, mr) (P, Q) call R] is the + precondition of the conclusion of [t_equiv_call_onesided]. *) +val equiv_call_onesided_wp : + LDecl.hyps + -> side + -> memory * memory + -> form * form + -> lvalue option * EcPath.xpath * expr list + -> form + -> form + +(* ==================================================================== *) +(* Derived tactics *) + +(* [t_equiv_call_last { ecall_pre = P; ecall_post = Q }] — on + [equiv [c; lvL <@ fL(aL) ~ c'; lvR <@ fR(aR) : P0 ==> R]], with [W0] + the precondition of [t_equiv_call] for [R]: + 1. [EcEquivSeq.t_equiv_seq] before both calls, with intermediate + relation [W0], giving + (a) equiv [c ~ c' : P0 ==> W0] — left open, + (b) equiv [lvL <@ fL(aL) ~ lvR <@ fR(aR) : W0 ==> R]; + 2. [t_equiv_call] on (b), giving + (c) equiv [fL ~ fR : P ==> Q] — left open. + Visible goals: (c), then (a). Fails if a last instruction is not a + call. Emits no node of its own. *) +val t_equiv_call_last : equiv_call -> backward + +(* [t_equiv_call_onesided_last { ecallos_side = `Left; ecallos_pre = P; + ecallos_post = Q }] — on + [equiv [c; lv <@ f(a) ~ c' : P0 ==> R]] (symmetrically for [`Right]), + with [W0] the precondition of [t_equiv_call_onesided] for [R]: + 1. [EcEquivSeq.t_equiv_seq] before the call on that side and at the end + of the other one, with intermediate relation [W0], giving + (a) equiv [c ~ c' : P0 ==> W0] — left open, + (b) equiv [lv <@ f(a) ~ skip : W0 ==> R]; + 2. [t_equiv_call_onesided] on (b), giving + (c) phoare [f : P ==> Q] = 1%r — left open. + Visible goals: (c), then (a). Fails if the last instruction on that side + is not a call. Emits no node of its own. *) +val t_equiv_call_onesided_last : equiv_call_onesided -> backward + +(* ==================================================================== *) +(* Elaboration *) + +(* The cut of [call] on an [equivS] goal, as [(spec, t)]: [spec] is the + specification of the procedure(s) called last, [t] the tactic run on it + once the cut is applied. + - [call (_ : P ==> Q)]: [P] and [Q] typed in the memories of [fL] and + [fR]; [spec] is [equiv [fL ~ fR : P ==> Q]], [t] the identity; + - [call{i} (_ : P ==> Q)]: [P] and [Q] typed in the memory of the + procedure called last on side [i]; [spec] is + [phoare [f : P ==> Q] = 1%r], [t] the identity; + - [call (: I)] (no side): [I] typed in abstract memories (global + variables only); [spec] is + [equiv [fL ~ fR : ={arg} /\ I ==> ={res} /\ I]] (with [={glob A}] in + both for procedures of an abstract [A]; for concrete procedures, the + types of their arguments and results must coincide), [t] is [proc I] + (or [proc] for concrete procedures, see [EcPhlFun.t_fun]) followed + by [trivial] on its first two goals; + - [call (: bad, P, Q)] (no side; abstract procedures): [spec] is + [equiv [fL ~ fR : bad<2> ? Q : ={arg, glob A} /\ P ==> + bad<2> ? Q : ={res, glob A} /\ P]], [t] is the + abstract upto rule ([EcPhlFun.t_equivF_abs_upto]) followed by + [assumption] or [trivial] on its first three goals. *) +val process_equiv_call_cut : + oside -> call_info -> tcenv1 -> EcFol.form * backward diff --git a/src/phl/rules/hoare/ecHoareCall.ml b/src/phl/rules/hoare/ecHoareCall.ml new file mode 100644 index 000000000..fe2b9f8e3 --- /dev/null +++ b/src/phl/rules/hoare/ecHoareCall.ml @@ -0,0 +1,169 @@ +(* -------------------------------------------------------------------- *) +open EcUtils +open EcParsetree +open EcAst +open EcTypes +open EcModules +open EcFol +open EcEnv +open EcPV +open EcSubst + +open EcCoreGoal +open EcLowGoal +open EcLowPhlGoal + +module TTC = EcProofTyping + +(* -------------------------------------------------------------------- *) +(* Parameters of the hoare [call] rule: the specification of the called + procedure. *) +type hoare_call = { + hcall_pre : ss_inv; (* precondition P of the procedure *) + hcall_post : hs_inv; (* postcondition Q | E_f of the procedure *) +} + +type EcCoreGoal.rule += RHoareCall of hoare_call + +(* -------------------------------------------------------------------- *) +(* Weakest precondition of [lv <@ f(a)] for the postcondition [post], + given the specification [P ==> Q | E_f] of [f] (in memory [m]): + P[arg := a] /\ forall result, forall (mod f), Q[res := result] => post[lv := result] + conjoined with, for each exception [e], [forall (mod f), E_f(e) => E(e)]. *) +let hoare_call_wp + (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; } = fpost in + let { main = post ; exnmap = epost; } = 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 = + EcPlCall.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 = EcPlCall.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 fepost 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 + +(* -------------------------------------------------------------------- *) +(* Pure core shared by the rule and its checker. Its side conditions (the + statement is a single call, the precondition is its weakest + precondition) are part of it, so the checker re-validates them. *) +let hoare_call_subgoals (hyps : LDecl.hyps) (hs : sHoareS) (n : hoare_call) = + let m = fst hs.hs_m in + let fpre = ss_inv_rebind n.hcall_pre m in + let fpost = hs_inv_rebind n.hcall_post m in + let (_, f, _) as call = EcPlCall.single_call "hoare-call" hs.hs_s in + let wp = + hoare_call_wp hyps m (fpre.inv, fpost.hsi_inv) call (hs_po hs).hsi_inv in + if not (EcReduction.is_conv hyps (hs_pr hs).inv wp) then + failwith "hoare-call: the precondition is not the expected one"; + [f_hoareF fpre f fpost] + +(* -------------------------------------------------------------------- *) +(* Rule (TCB). *) +let t_hoare_call (n : hoare_call) (tc : tcenv1) = + let hs = tc1_as_hoareS tc in + let sg = + try hoare_call_subgoals (FApi.tc1_hyps tc) hs n + with Failure msg -> tc_error !!tc "%s" msg in + FApi.xrule1 tc (RHoareCall n) sg + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | RHoareCall n -> + Some (EcPlRecheck.checker_of "hoare-call" pf_as_hoareS + (fun hyps hs -> hoare_call_subgoals hyps hs n)) + | _ -> None) + +(* -------------------------------------------------------------------- *) +(* Derived (no proof-node): on [c; lv <@ f(a)], [seq] before the call with + its weakest precondition as intermediate assertion, then close the call + with the rule. The specification premise comes first. *) +let t_hoare_call_last (n : hoare_call) (tc : tcenv1) = + let hyps = FApi.tc1_hyps tc in + let hs = tc1_as_hoareS tc in + let m = fst hs.hs_m in + let fpre = ss_inv_rebind n.hcall_pre m in + let fpost = hs_inv_rebind n.hcall_post m in + let call, _ = tc1_last_call tc hs.hs_s in + let mid = + hoare_call_wp hyps m (fpre.inv, fpost.hsi_inv) call (hs_po hs).hsi_inv in + let at = EcMatching.Position.gap_before_last_n 1 in + FApi.t_swap_goals 0 1 + (FApi.t_seqsub + (EcHoareSeq.t_hoare_seq { hsr_at = at; hsr_mid = { m; inv = mid; } }) + [t_id; t_hoare_call n] + tc) + +(* -------------------------------------------------------------------- *) +(* Elaboration: the goal is known to be a [hoareS]. Types the cut of + [call]: the specification of the last call. *) +let process_hoare_call_cut (side : oside) (info : call_info) (tc : tcenv1) = + let hyps, concl = FApi.tc1_flat tc in + let hs = destr_hoareS concl in + let last_f () = proj3_2 (fst (tc1_last_call tc hs.hs_s)) in + + match info with + | CI_spec (pre, epost) -> + if not (is_none side) then + tc_error !!tc "the conclusion is not a hoare"; + let f = last_f () in + let m = EcIdent.create "&hr" in + let penv, qenv = LDecl.hoareF m f hyps in + let pre = TTC.pf_process_form !!tc penv tbool pre in + let post = TTC.pf_process_form !!tc qenv tbool epost.pnormal in + let env_e = LDecl.inv_memenv1 m hyps in + let poe = TTC.pf_process_poe env_e epost.pexcept in + let spec = + f_hoareF {m; inv = pre} f + { hsi_m = m; hsi_inv = { main = post; exnmap = poe; } } in + (spec, t_id) + + | CI_inv inv -> + if not (is_none side) then + tc_error !!tc "cannot specify side for call with invariants"; + let m = fst hs.hs_m in + let f = last_f () in + let hyps = LDecl.push_active_ss (EcMemory.abstract m) hyps in + let inv = TTC.pf_process_form !!tc hyps tbool inv in + let inv = {m; inv} in + let t_spec tc = + FApi.t_firsts t_trivial 2 (EcPhlFun.t_fun (Inv_ss inv) tc) in + (f_hoareF inv f (POE.lift inv), t_spec) + + | CI_upto _ -> + if not (is_none side) then + tc_error !!tc "cannot specify side for call with invariants"; + tc_error !!tc "the conclusion is not an equiv" diff --git a/src/phl/rules/hoare/ecHoareCall.mli b/src/phl/rules/hoare/ecHoareCall.mli new file mode 100644 index 000000000..6ac6a627f --- /dev/null +++ b/src/phl/rules/hoare/ecHoareCall.mli @@ -0,0 +1,81 @@ +(* -------------------------------------------------------------------- *) +open EcParsetree +open EcCoreGoal +open EcCoreGoal.FApi +open EcAst +open EcEnv + +(* ==================================================================== *) +(* Rules (trusted) *) + +type hoare_call = { + hcall_pre : ss_inv; (* precondition P of the procedure *) + hcall_post : hs_inv; (* postcondition Q | E_f of the procedure *) +} + +(* [t_hoare_call { hcall_pre = P; hcall_post = Q | E_f }] — single call: + + hoare [f : P ==> Q | E_f] + ------------------------------------------------------------ + hoare [lv <@ f(a) : P[arg := a] /\ W /\ W_E ==> R | E] + + W := forall result, forall (mod f), + Q[res := result] => R[lv := result] + W_E := forall (mod f), E_f => E (exception per exception) + + where [mod f] are the variables written by [f], [E_f => E] are the + conditions of [EcProofTyping.merge2_poe_list E E_f] (each exceptional + postcondition of [E_f] implies the corresponding one of [E]), and + [/\] is the asymmetric conjunction [&&], built with the simplifying + constructors ([hoare_call_wp]). Side conditions: the statement is the + single call [lv <@ f(a)], and the precondition is convertible to the + one displayed (otherwise fails). Soundness: [P], [Q] and [E_f] are + read in the memory of [f] in the premise and in the memory of the goal + in the conclusion; they read no local variable other than [arg] / + [res], as the typing of the specifications ensures. + + Node: [RHoareCall { hcall_pre = P; hcall_post = Q | E_f }]. + Checker: "hoare-call". *) +val t_hoare_call : hoare_call -> backward + +(* [hoare_call_wp hyps m (P, Q | E_f) (lv, f, a) (R | E)] is the + precondition of the conclusion of [t_hoare_call], in memory [m]. *) +val hoare_call_wp : + LDecl.hyps + -> memory + -> form * exnpost + -> lvalue option * EcPath.xpath * expr list + -> exnpost + -> form + +(* ==================================================================== *) +(* Derived tactics *) + +(* [t_hoare_call_last { hcall_pre = P; hcall_post = Q | E_f }] — on + [hoare [c; lv <@ f(a) : P0 ==> R | E]], with [W0] the precondition of + [t_hoare_call] for [R | E]: + 1. [EcHoareSeq.t_hoare_seq] before the call, with intermediate + assertion [W0], giving + (a) hoare [c : P0 ==> W0 | E] — left open, + (b) hoare [lv <@ f(a) : W0 ==> R | E]; + 2. [t_hoare_call] on (b), giving + (c) hoare [f : P ==> Q | E_f] — left open. + Visible goals: (c), then (a). Fails if the last instruction is not a + call. Emits no node of its own. *) +val t_hoare_call_last : hoare_call -> backward + +(* ==================================================================== *) +(* Elaboration *) + +(* The cut of [call] on a [hoareS] goal, as [(spec, t)]: [spec] is the + specification of the procedure [f] called last, [t] the tactic run on it + once the cut is applied. + - [call (_ : P ==> Q | E)] (no side): [P], [Q] and [E] typed in the + memory of [f]; [spec] is [hoare [f : P ==> Q | E]], [t] the identity; + - [call (: I)] (no side): [I] typed in an abstract memory (global + variables only); [spec] is [hoare [f : I ==> I]], [t] is [proc I] (or + [proc] for a concrete [f], see [EcPhlFun.t_fun]) followed by + [trivial] on its first two goals; + - [call (: bad, P, Q)]: fails (an equiv is expected). *) +val process_hoare_call_cut : + oside -> call_info -> tcenv1 -> EcFol.form * backward diff --git a/tests/call-rules.ec b/tests/call-rules.ec new file mode 100644 index 000000000..0c8fbf7b8 --- /dev/null +++ b/tests/call-rules.ec @@ -0,0 +1,326 @@ +(* The `call` tactic in every logic: a `seq` before the call(s) and the + call rule of the logic on the call alone (the bdhoare rule keeps its + composite statement). Run with EC_RECHECK=1 to recheck the rules. *) +require import AllCore Distr DBool Xreal. + +module G = { var g : int var b : bool }. + +module M = { + proc f(x : int) : int = { G.g <- G.g + x; return G.g; } + + proc h() = { G.g <- G.g + 1; } + + proc main(y : int) : int = { + var r; + G.g <- 0; + r <@ f(y); + return r; + } + + proc single(y : int) : int = { + var r; + r <@ f(y); + return r; + } + + proc proc_h() = { h(); } + + proc bool_f() : bool = { var b; b <$ {0,1}; return b; } + + proc bool_main() : bool = { var r; G.g <- 0; r <@ bool_f(); return r; } +}. + +module type O = { proc o() : unit }. +module type A (O : O) = { proc a() : unit }. + +module O = { proc o() = { G.g <- G.g + 1; } }. + +module Main (A : A) = { + proc main() = { G.g <- 0; A(O).a(); } +}. + +(* -------------------------------------------------------------------- *) +(* hoare *) +lemma f_spec (z w : int) : hoare [M.f : G.g = z /\ x = w ==> res = z + w /\ G.g = res]. +proof. proc; auto. qed. + +lemma h_spec : hoare [M.h : true ==> true]. +proof. by proc; auto. qed. + +lemma bool_f_ll : phoare [M.bool_f : true ==> true] = 1%r. +proof. by proc; auto; rewrite dbool_ll. qed. + +lemma hoare_spec : hoare [M.main : 0 <= y ==> 0 <= res]. +proof. +proc. +call (_ : 0 <= x /\ 0 <= G.g ==> 0 <= res). ++ by proc; auto => /#. +by auto. +qed. + +lemma hoare_lemma (w : int) : hoare [M.main : y = w ==> res = w]. +proof. +proc. +call (f_spec 0 w). +by auto => /#. +qed. + +lemma hoare_single (w : int) : hoare [M.single : y = w /\ G.g = 0 ==> res = w]. +proof. +proc. +call (f_spec 0 w). +by skip => /#. +qed. + +lemma hoare_inv_concrete : hoare [M.proc_h : 0 <= G.g ==> 0 <= G.g]. +proof. +proc. +call (: 0 <= G.g). ++ by auto => /#. +by auto. +qed. + +lemma hoare_inv_abs (A <: A {-G}) : hoare [Main(A).main : true ==> 0 <= G.g]. +proof. +proc. +call (: 0 <= G.g). ++ by proc; auto => /#. +by auto. +qed. + +(* exceptional postconditions *) +exception E. + +module X = { + proc r(x : int) : int = { if (0 <= x) else raise E; return x; } + + proc m(y : int) : int = { var r; G.g <- y; r <@ r(y); return r; } +}. + +lemma hoare_exn : hoare [X.m : true ==> 0 <= res | E => G.g < 0]. +proof. +proc. +call (_ : x = G.g ==> 0 <= res | E => G.g < 0). ++ by proc; auto => /#. +by auto. +qed. + +lemma hoare_errors : hoare [M.main : true ==> true]. +proof. +proc. +fail call{1} (_ : true ==> true). +fail call{1} (: true). +fail call (: G.b, true). +fail call h_spec. +fail call bool_f_ll. +abort. + +lemma hoare_not_call : hoare [M.h : true ==> true]. +proof. +proc. +fail call (_ : true ==> true). +fail call (: true). +abort. + +(* -------------------------------------------------------------------- *) +(* ehoare *) +lemma ehoare_spec : ehoare [M.main : (0 <= y)%xr ==> (0 <= res)%xr]. +proof. +proc. +call (_ : (0 <= G.g + x)%xr ==> (0 <= res)%xr). ++ by proc; auto. +by auto. +qed. + +lemma ehoare_inv (A <: A {-G}) : ehoare [Main(A).main : 1%xr ==> (G.g < 0)%xr]. +proof. +proc. +call (: (G.g < 0)%xr). ++ by proc; auto => &hr /#. +by auto. +qed. + +lemma f_espec : ehoare [M.f : (0 <= G.g + x)%xr ==> (0 <= res)%xr]. +proof. by proc; auto. qed. + +lemma ehoare_concave : ehoare [M.main : (0 <= y)%xr ==> (0 <= res)%xr]. +proof. +proc. +call /(fun x => x) f_espec. +by auto. +qed. + +lemma ehoare_concave_inv (A <: A {-G}) : ehoare [Main(A).main : 1%xr ==> (G.g < 0)%xr]. +proof. +proc. +call /(fun x => x) (: (G.g < 0)%xr). ++ by proc; auto => &hr /#. +by auto. +qed. + +lemma ehoare_errors : ehoare [M.main : 1%xr ==> 1%xr]. +proof. +proc. +fail call{1} (_ : 1%xr ==> 1%xr). +(* the post-expectation of the procedure must be the one of the goal *) +fail call (_ : 1%xr ==> (res = 0)%xr). +abort. + +module N = { + proc k(y : int) = { G.g <@ M.f(y); } + + proc k2(y : int) = { M.f(y); } +}. + +(* only local variables on the left of the call *) +lemma ehoare_glob_lv : ehoare [N.k : 1%xr ==> 1%xr]. +proof. +proc. +fail call (_ : 1%xr ==> 1%xr). +abort. + +(* no left-value: the post-expectation cannot read [res] *) +lemma ehoare_res_nolv : ehoare [N.k2 : 1%xr ==> 1%xr]. +proof. +proc. +fail call (_ : 1%xr ==> (res = 0)%xr). +abort. + +(* -------------------------------------------------------------------- *) +(* bdhoare *) +lemma bool_f_spec : phoare [M.bool_f : true ==> res] = (1%r / 2%r). +proof. by proc; rnd; skip => />; rewrite dboolE. qed. + +lemma bdhoare_eq : phoare [M.bool_main : true ==> res] = (1%r / 2%r). +proof. +proc. +call bool_f_spec. +by auto. +qed. + +lemma bdhoare_le : phoare [M.bool_main : true ==> res] <= (1%r / 2%r). +proof. +proc. +call (_ : true ==> res). ++ proc; rnd; 2: by move=> _ /#. + by skip => />; rewrite dboolE. +by auto. +qed. + +lemma bdhoare_ge : phoare [M.bool_main : true ==> res] >= (1%r / 2%r). +proof. +proc. +call (_ : true ==> res). ++ by proc; rnd; skip => />; rewrite dboolE. +by auto. +qed. + +lemma bdhoare_inv : phoare [M.proc_h : 0 <= G.g ==> 0 <= G.g] = 1%r. +proof. +proc. +call (: 0 <= G.g). ++ by auto => /#. +by auto. +qed. + +lemma bdhoare_errors : phoare [M.bool_main : true ==> res] = (1%r / 2%r). +proof. +proc. +fail call{1} (_ : true ==> res). +fail call{1} (: true). +fail call (: G.b, true). +fail call h_spec. +fail call bool_f_ll. +abort. + +lemma bdhoare_not_call : phoare [M.h : true ==> true] = 1%r. +proof. +proc. +fail call (_ : true ==> true). +abort. + +(* the bound cannot depend on local variables (#1189) *) +lemma bdhoare_local_bound : phoare [M.single : true ==> true] <= (b2r (y = 0)). +proof. +proc. +fail call (_ : true ==> true). +abort. + +(* -------------------------------------------------------------------- *) +(* equiv, two-sided *) +lemma equiv_spec : equiv [M.main ~ M.main : ={y} ==> ={res}]. +proof. +proc. +call (_ : ={x, G.g} ==> ={res}). ++ by proc; auto. +by auto. +qed. + +lemma equiv_inv : equiv [M.main ~ M.main : ={y} ==> ={res, G.g}]. +proof. +proc. +call (: ={G.g}). ++ by auto. +by auto. +qed. + +lemma equiv_inv_abs (A <: A {-G}) : equiv [Main(A).main ~ Main(A).main : ={glob A} ==> ={G.g}]. +proof. +proc. +call (: ={G.g}). ++ by proc; auto. +by auto. +qed. + +lemma equiv_upto (A <: A {-G}) : + (forall (O0 <: O{-A}), islossless O0.o => islossless A(O0).a) => + equiv [Main(A).main ~ Main(A).main : ={glob A} ==> G.b{2} \/ ={G.g}]. +proof. +move=> A_ll; proc. +call (: G.b, ={G.g}). ++ by proc; auto. ++ by move=> &2 _; proc; auto. ++ by move=> _; proc; auto. +by auto => /#. +qed. + +lemma equiv_errors : equiv [M.main ~ M.single : true ==> true]. +proof. +proc. +fail call{1} (: true). +fail call (f_spec 0 0). +fail call equiv_spec. +fail call (: G.b, true). +abort. + +(* -------------------------------------------------------------------- *) +(* equiv, one-sided *) +lemma f_ll : phoare [M.f : true ==> true] = 1%r. +proof. by proc; auto. qed. + +lemma equiv_onesided : equiv [M.main ~ M.single : true ==> true]. +proof. +proc. +call{1} (_ : true ==> true). ++ by proc; auto. +call{2} (_ : true ==> true). ++ by proc; auto. +by auto. +qed. + +lemma equiv_onesided_lemma : equiv [M.main ~ M.single : true ==> true]. +proof. +proc. +call{1} f_ll. +call{2} f_ll. +by auto. +qed. + +lemma equiv_onesided_errors : equiv [M.main ~ M.single : true ==> true]. +proof. +proc. +fail call f_ll. +call{1} f_ll. +fail call{1} f_ll. +fail call{1} (_ : true ==> true). +abort.