From 8934dae95a1b6bd0a0f50ed3226939baaaac04c7 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Fri, 9 Oct 2026 00:09:49 +0200 Subject: [PATCH] refactor(pl): proc as recheckable per-logic rules PR of the program-logic reorganization stack (see src/phl/REFACTORING.md). It migrates the `proc` tactic class: - `rules//ecFunDef.ml` (hoare, ehoare, bdhoare, equiv): a concrete procedure by its body; parameterless node, the side condition (the procedure is not abstract) re-checked by the builder. - `rules//ecFunAbs.ml` (hoare, ehoare, bdhoare, equiv): an abstract procedure with an invariant, stated on `[f : I ==> I]` exactly (bdhoare: `>= 1%r`); the node records the invariant, the builder re-checks that the procedure is abstract, the invariant independent of its globals, the oracles' memory restrictions (bdhoare) and that the goal is the conclusion of the rule (up to alpha-conversion). `proc I` is derived: the consequence rule to that conclusion, then the rule (bdhoare `= 1%r` through `>= 1%r`, as before). The hoare rule concludes with no exceptional postcondition; its .mli documents that it relies on unlisted exceptions being unconstrained. - rules/equiv/ecEquivFunAbsUpto.ml: the abstract upto rule (`proc B P Q`, `proc @[ll] ...`), likewise stated on its own conclusion and derived through the consequence rule; its elaboration is shared with `call`. - `rules//ecFunToCode.ml` (hoare, ehoare, bdhoare, equiv, and rules/eager/ecEagerFunToCode.ml): `proc*`, the procedure as a single call to fresh locals; parameterless nodes. - rules/ecPlFun.ml: the computations shared by these rules (argument substitution, oracle restrictions, losslessness hypothesis of an abstract procedure, the single-call statement of `proc*`). - EcPhlFun is reduced to the logic-agnostic dispatchers and the legacy adapters (interface unchanged, including FunAbsLow used by eager); the no-op FApi.t_low* wrappers are dropped. The dispatchers keep t_hF_or_bhF_or_eF (match on the goal, reducing it when it is not a judgement), as before. Behaviour is preserved: on the new test, the transcripts of the reference and new builds (all goals printed after each `proc`, and every error message) are identical. A new test, tests/proc.ec, exercises every rule in every logic (also through `call`) and the error paths. The stdlib, the unit tests and the examples pass under EC_RECHECK=1 with no RecheckFailure. Each of the 14 checkers, when deliberately broken, is caught only under EC_RECHECK, on the new test and, where the rule is used there, on the stdlib (files: hoareF-fun-def 13, bdhoareF-fun-def 31, equivF-fun-def 32, hoareF-fun-abs 12, bdhoareF-fun-abs 2, equivF-fun-abs 29, equivF-fun-abs-upto 9, equivF-fun-to-code 12; the ehoare rules and the hoare, bdhoare and eager `proc*` rules are not used by the stdlib). --- src/phl/README.md | 5 +- src/phl/REFACTORING.md | 10 +- src/phl/ecPhlFun.ml | 634 ++----------------- src/phl/rules/bdhoare/ecBdHoareFunAbs.ml | 113 ++++ src/phl/rules/bdhoare/ecBdHoareFunAbs.mli | 65 ++ src/phl/rules/bdhoare/ecBdHoareFunDef.ml | 47 ++ src/phl/rules/bdhoare/ecBdHoareFunDef.mli | 20 + src/phl/rules/bdhoare/ecBdHoareFunToCode.ml | 45 ++ src/phl/rules/bdhoare/ecBdHoareFunToCode.mli | 19 + src/phl/rules/eager/ecEagerFunToCode.ml | 55 ++ src/phl/rules/eager/ecEagerFunToCode.mli | 20 + src/phl/rules/ecPlFun.ml | 106 ++++ src/phl/rules/ecPlFun.mli | 62 ++ src/phl/rules/ehoare/ecEHoareFunAbs.ml | 78 +++ src/phl/rules/ehoare/ecEHoareFunAbs.mli | 52 ++ src/phl/rules/ehoare/ecEHoareFunDef.ml | 45 ++ src/phl/rules/ehoare/ecEHoareFunDef.mli | 19 + src/phl/rules/ehoare/ecEHoareFunToCode.ml | 44 ++ src/phl/rules/ehoare/ecEHoareFunToCode.mli | 17 + src/phl/rules/equiv/ecEquivFunAbs.ml | 125 ++++ src/phl/rules/equiv/ecEquivFunAbs.mli | 61 ++ src/phl/rules/equiv/ecEquivFunAbsUpto.ml | 180 ++++++ src/phl/rules/equiv/ecEquivFunAbsUpto.mli | 71 +++ src/phl/rules/equiv/ecEquivFunDef.ml | 56 ++ src/phl/rules/equiv/ecEquivFunDef.mli | 20 + src/phl/rules/equiv/ecEquivFunToCode.ml | 54 ++ src/phl/rules/equiv/ecEquivFunToCode.mli | 19 + src/phl/rules/hoare/ecHoareFunAbs.ml | 80 +++ src/phl/rules/hoare/ecHoareFunAbs.mli | 54 ++ src/phl/rules/hoare/ecHoareFunDef.ml | 48 ++ src/phl/rules/hoare/ecHoareFunDef.mli | 20 + src/phl/rules/hoare/ecHoareFunToCode.ml | 44 ++ src/phl/rules/hoare/ecHoareFunToCode.mli | 18 + tests/proc.ec | 236 +++++++ 34 files changed, 1962 insertions(+), 580 deletions(-) create mode 100644 src/phl/rules/bdhoare/ecBdHoareFunAbs.ml create mode 100644 src/phl/rules/bdhoare/ecBdHoareFunAbs.mli create mode 100644 src/phl/rules/bdhoare/ecBdHoareFunDef.ml create mode 100644 src/phl/rules/bdhoare/ecBdHoareFunDef.mli create mode 100644 src/phl/rules/bdhoare/ecBdHoareFunToCode.ml create mode 100644 src/phl/rules/bdhoare/ecBdHoareFunToCode.mli create mode 100644 src/phl/rules/eager/ecEagerFunToCode.ml create mode 100644 src/phl/rules/eager/ecEagerFunToCode.mli create mode 100644 src/phl/rules/ecPlFun.ml create mode 100644 src/phl/rules/ecPlFun.mli create mode 100644 src/phl/rules/ehoare/ecEHoareFunAbs.ml create mode 100644 src/phl/rules/ehoare/ecEHoareFunAbs.mli create mode 100644 src/phl/rules/ehoare/ecEHoareFunDef.ml create mode 100644 src/phl/rules/ehoare/ecEHoareFunDef.mli create mode 100644 src/phl/rules/ehoare/ecEHoareFunToCode.ml create mode 100644 src/phl/rules/ehoare/ecEHoareFunToCode.mli create mode 100644 src/phl/rules/equiv/ecEquivFunAbs.ml create mode 100644 src/phl/rules/equiv/ecEquivFunAbs.mli create mode 100644 src/phl/rules/equiv/ecEquivFunAbsUpto.ml create mode 100644 src/phl/rules/equiv/ecEquivFunAbsUpto.mli create mode 100644 src/phl/rules/equiv/ecEquivFunDef.ml create mode 100644 src/phl/rules/equiv/ecEquivFunDef.mli create mode 100644 src/phl/rules/equiv/ecEquivFunToCode.ml create mode 100644 src/phl/rules/equiv/ecEquivFunToCode.mli create mode 100644 src/phl/rules/hoare/ecHoareFunAbs.ml create mode 100644 src/phl/rules/hoare/ecHoareFunAbs.mli create mode 100644 src/phl/rules/hoare/ecHoareFunDef.ml create mode 100644 src/phl/rules/hoare/ecHoareFunDef.mli create mode 100644 src/phl/rules/hoare/ecHoareFunToCode.ml create mode 100644 src/phl/rules/hoare/ecHoareFunToCode.mli create mode 100644 tests/proc.ec diff --git a/src/phl/README.md b/src/phl/README.md index 9e96a991e..19ca60c9e 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 + EcPlMatch, EcPlFun ecPlRecheck.ml checker scaffolding ecPhl.ml legacy: thin dispatchers and adapters, not-yet-migrated tactics @@ -152,6 +152,9 @@ src/phl/ - `wp` and `sp` are logic rules on an explicit suffix / prefix, in `rules//` (the shared computation in `EcPlWp` / `EcPlSp`). - `sym` and `trans` are equiv-only rules, in `rules/equiv/`. +- The `proc` rules (`EcFunDef`, `EcFunAbs`, + `EcEquivFunAbsUpto`, `EcFunToCode`, `EcEagerFunToCode`) are + logic rules in `rules//`; `proc I` is derived (consequence + rule). - A rule relating two logics (e.g. the `pr` bridges) lives with the logic of its conclusion. - Program transformations use the transformation rule of each logic; only diff --git a/src/phl/REFACTORING.md b/src/phl/REFACTORING.md index 306bc7047..fc9c33247 100644 --- a/src/phl/REFACTORING.md +++ b/src/phl/REFACTORING.md @@ -154,7 +154,9 @@ src/phl/ (semantic sampling), EcPlRCond (deciding a conditional or a match), EcPlTransform (the transformation catalogue and its obligations), EcPlMatch (branches of a `match` on - fresh program variables) + fresh program variables), EcPlFun (unfolding a procedure, + the oracle conditions of the abstract-procedure rules, + the single-call statement of `proc*`) ecPlRecheck.ml checker scaffolding ecPhl.ml legacy: thin dispatchers and adapters, not-yet-migrated tactics @@ -167,6 +169,12 @@ uniform across logics or relate several judgements: (`EcHoareWp`, `EcEquivSp`, …), the shared computation being in `EcPlWp` / `EcPlSp`; - `sym` and `trans` are equiv-only rules, in `rules/equiv/`; +- the `proc` rules are logic rules in `rules//`: `EcFunDef` + (a concrete procedure, by its body), `EcFunAbs` (an abstract + procedure with an invariant, stated on `[f : I ==> I]`, `proc I` being + the consequence rule then the rule), `EcEquivFunAbsUpto` (the abstract + upto rule) and `EcFunToCode` (`proc*`, also `EcEagerFunToCode` + in `rules/eager/`); - a rule relating judgements of two logics (the `pr` bridges, `hoare` from `phoare`, …) lives with the logic of its conclusion; - program transformations go through the transformation rule of each logic diff --git a/src/phl/ecPhlFun.ml b/src/phl/ecPhlFun.ml index 67d367f1b..09797517b 100644 --- a/src/phl/ecPhlFun.ml +++ b/src/phl/ecPhlFun.ml @@ -1,568 +1,82 @@ (* -------------------------------------------------------------------- *) -open EcUtils -open EcPath open EcAst -open EcTypes open EcFol -open EcMemory -open EcModules open EcEnv -open EcPV -open EcSubst open EcCoreGoal open EcLowPhlGoal -module TTC = EcProofTyping - -(* FIXME: oracles should ensure they preserve the state of the adversaries - * - * Two solutions: - * - add the equalities in the pre and post. - * - ensure that oracle doesn't write the adversaries states - * - * See [ospec] in [equivF_abs_spec / equivF_abs_upto] *) - (* -------------------------------------------------------------------- *) -let check_oracle_use (_pf : proofenv) env adv o = - let restr = { mr_empty with ur_neg = Sx.empty, Sm.singleton adv } in - - (* This only checks the memory restrictions. *) - EcTyping.check_mem_restr_fun env o restr - -let check_concrete pf env f = - if NormMp.is_abstract_fun f env then - tc_error_lazy pf (fun fmt -> - let ppe = EcPrinting.PPEnv.ofenv env in - Format.fprintf fmt - "The function %a is abstract. Provide an invariant to the [proc] tactic" - (EcPrinting.pp_funname ppe) f) +(* The [proc] rules live, one module per (logic, rule), in + [rules//]: [EcFunDef] (a concrete procedure, by its body), + [EcFunAbs] (an abstract procedure, with an invariant), + [EcEquivFunAbsUpto] (an abstract procedure, up to a bad event) and + [EcFunToCode] ([proc*]); their shared computations are in + [EcPlFun]. 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 lossless_hyps env top sub = - let clear_to_top = { mr_empty with ur_neg = Sx.empty, Sm.singleton top } in - - let sig_ = EcEnv.NormMp.sig_of_mp env top in - let bd = - List.map - (fun (id, mt) -> - (id, GTmodty (mt, clear_to_top)) - ) sig_.mis_params - in - (* WARN: this implies that the oracle do not have access to top *) - let args = List.map (fun (id,_) -> EcPath.mident id) sig_.mis_params in - let concl = f_losslessF (EcPath.xpath (EcPath.m_apply top args) sub) in - let calls = - let name = sub in - (EcSymbols.Msym.find name sig_.mis_oinfos) |> OI.allowed - in - let hyps = List.map f_losslessF calls in - f_forall bd (f_imps hyps concl) +let check_concrete = EcPlFun.check_concrete +let subst_pre = EcPlFun.subst_pre (* -------------------------------------------------------------------- *) -let subst_pre env fs (m : memory) s = - let fresh ov = - match ov.ov_name with - | None -> assert false; - | Some v -> { v_name = v; v_type = ov.ov_type } - in - let v = List.map (fun v -> f_pvloc (fresh v) m) fs.fs_anames in - PVM.add env pv_arg m (map_ss_inv ~m f_tuple v).inv s - -(* ------------------------------------------------------------------ *) -let t_hoareF_fun_def_r tc = - let env = FApi.tc1_env tc in - let hf = tc1_as_hoareF tc in - let f = NormMp.norm_xfun env hf.hf_f in - check_concrete !!tc env f; - let (memenv, (fsig, fdef), env) = Fun.hoareS hf.hf_m f env in - let m = EcMemory.memory memenv in - let fres = odfl {m;inv=f_tt} (omap (ss_inv_of_expr m) fdef.f_ret) in - let post, epost = POE.destruct (hf_po hf).hsi_inv in - let post = {m=(hf_po hf).hsi_m;inv=post} in - let post = map_ss_inv2 (PVM.subst1 env pv_res m) fres post in - let pre = map_ss_inv1 (PVM.subst env (subst_pre env fsig m PVM.empty)) (hf_pr hf) in - let post = { hsi_m = post.m; hsi_inv = POE.mk post.inv epost; } in - let concl' = f_hoareS (snd memenv) pre fdef.f_body post in - FApi.xmutate1 tc `FunDef [concl'] - -(* ------------------------------------------------------------------ *) -let t_ehoareF_fun_def_r tc = - let env = FApi.tc1_env tc in - let hf = tc1_as_ehoareF tc in - let f = NormMp.norm_xfun env hf.ehf_f in - check_concrete !!tc env f; - let (memenv, (fsig, fdef), env) = Fun.hoareS hf.ehf_m f env in - let m = EcMemory.memory memenv in - let fres = odfl {m;inv=f_tt} (omap (ss_inv_of_expr m) fdef.f_ret) in - let post = map_ss_inv2 (PVM.subst1 env pv_res m) fres (ehf_po hf) in - let pre = map_ss_inv1 (PVM.subst env (subst_pre env fsig m PVM.empty)) (ehf_pr hf) in - let concl' = f_eHoareS (snd memenv) pre fdef.f_body post in - FApi.xmutate1 tc `FunDef [concl'] - -(* ------------------------------------------------------------------ *) -let t_bdhoareF_fun_def_r tc = - let env = FApi.tc1_env tc in - let bhf = tc1_as_bdhoareF tc in - let f = NormMp.norm_xfun env bhf.bhf_f in - check_concrete !!tc env f; - let (memenv, (fsig, fdef), env) = Fun.hoareS bhf.bhf_m f env in - let m = EcMemory.memory memenv in - let fres = odfl {m;inv=f_tt} (omap (ss_inv_of_expr m) fdef.f_ret) in - let post = map_ss_inv2 (PVM.subst1 env pv_res m) fres (bhf_po bhf) in - let spre = subst_pre env fsig m PVM.empty in - let pre = map_ss_inv1 (PVM.subst env spre) (bhf_pr bhf) in - let bd = map_ss_inv1 (PVM.subst env spre) (bhf_bd bhf) in - let concl' = f_bdHoareS (snd memenv) pre fdef.f_body post bhf.bhf_cmp bd in - FApi.xmutate1 tc `FunDef [concl'] - -(* ------------------------------------------------------------------ *) -let t_equivF_fun_def_r tc = - let env = FApi.tc1_env tc in - let ef = tc1_as_equivF tc in - let ml, mr = ef.ef_ml, ef.ef_mr in - let fl = NormMp.norm_xfun env ef.ef_fl in - let fr = NormMp.norm_xfun env ef.ef_fr in - check_concrete !!tc env fl; check_concrete !!tc env fr; - let (menvl, eqsl, menvr, eqsr, env) = Fun.equivS ml mr fl fr env in - let (fsigl, fdefl) = eqsl in - let (fsigr, fdefr) = eqsr in - let fresl = odfl {m=ml;inv=f_tt} (omap (ss_inv_of_expr ml) fdefl.f_ret) in - let fresr = odfl {m=mr;inv=f_tt} (omap (ss_inv_of_expr mr) fdefr.f_ret) in - let s = PVM.add env pv_res ml fresl.inv PVM.empty in - let s = PVM.add env pv_res mr fresr.inv s in - let post = map_ts_inv1 (PVM.subst env s) (ef_po ef) in - let s = subst_pre env fsigl ml PVM.empty in - let s = subst_pre env fsigr mr s in - let pre = map_ts_inv1 (PVM.subst env s) (ef_pr ef) in - let concl' = f_equivS (snd menvl) (snd menvr) pre fdefl.f_body fdefr.f_body post in - FApi.xmutate1 tc `FunDef [concl'] +let t_hoareF_fun_def = EcHoareFunDef.t_hoareF_fun_def +let t_bdhoareF_fun_def = EcBdHoareFunDef.t_bdhoareF_fun_def +let t_equivF_fun_def = EcEquivFunDef.t_equivF_fun_def -(* -------------------------------------------------------------------- *) -let t_hoareF_fun_def = FApi.t_low0 "hoare-fun-def" t_hoareF_fun_def_r -let t_ehoareF_fun_def = FApi.t_low0 "ehoare-fun-def" t_ehoareF_fun_def_r -let t_bdhoareF_fun_def = FApi.t_low0 "bdhoare-fun-def" t_bdhoareF_fun_def_r -let t_equivF_fun_def = FApi.t_low0 "equiv-fun-def" t_equivF_fun_def_r - -(* -------------------------------------------------------------------- *) -let t_fun_def_r tc = +let t_fun_def tc = let th = t_hoareF_fun_def - and teh = t_ehoareF_fun_def + and teh = EcEHoareFunDef.t_ehoareF_fun_def and tbh = t_bdhoareF_fun_def and te = t_equivF_fun_def in t_hF_or_bhF_or_eF ~th ~teh ~tbh ~te tc -let t_fun_def = FApi.t_low0 "fun-def" t_fun_def_r - (* -------------------------------------------------------------------- *) module FunAbsLow = struct - (* ------------------------------------------------------------------ *) - let hoareF_abs_spec _pf env f inv = - let (top, _, oi, _) = EcLowPhlGoal.abstract_info env f in - let fv = PV.fv env inv.m inv.inv in - PV.check_depend env fv top; - let ospec o = f_hoareF inv o (POE.lift inv) in - let sg = List.map ospec (OI.allowed oi) in - (inv, inv, sg) - - (* ------------------------------------------------------------------ *) - let ehoareF_abs_spec _pf env f (inv: ss_inv) = - let (top, _, oi, _) = EcLowPhlGoal.abstract_info env f in - let fv = PV.fv env inv.m inv.inv in - PV.check_depend env fv top; - let ospec o = f_eHoareF inv o inv in - let sg = List.map ospec (OI.allowed oi) in - (inv, inv, sg) - - (* ------------------------------------------------------------------ *) - let bdhoareF_abs_spec pf env f inv = - let (top, _, oi, _) = EcLowPhlGoal.abstract_info env f in - let fv = PV.fv env inv.m inv.inv in - - PV.check_depend env fv top; - let ospec o = - check_oracle_use pf env top o; - f_bdHoareF inv o inv FHge {m=inv.m;inv=f_r1} in - - let sg = List.map ospec (OI.allowed oi) in - (inv, inv, lossless_hyps env top f.x_sub :: sg) - - (* ------------------------------------------------------------------ *) - let equivF_abs_spec pf env fl fr (inv: ts_inv) = - let (topl, _fl, oil, sigl), (topr, _fr, oir, sigr) = - EcLowPhlGoal.abstract_info2 env fl fr - in - - let ml, mr = inv.ml, inv.mr in - let fvl = PV.fv env inv.ml inv.inv in - let fvr = PV.fv env inv.mr inv.inv in - PV.check_depend env fvl topl; - PV.check_depend env fvr topr; - let eqglob = ts_inv_eqglob topl ml topr mr in - - let ospec o_l o_r = - let use = - try - check_oracle_use pf env topl o_l; - check_oracle_use pf env topr o_r; - false - with _ -> true - in + let hoareF_abs_spec (_ : proofenv) env f inv = + EcHoareFunAbs.hoareF_abs_spec env f inv - let fo_l = EcEnv.Fun.by_xpath o_l env in - let fo_r = EcEnv.Fun.by_xpath o_r env in + let bdhoareF_abs_spec (_ : proofenv) env f inv = + EcBdHoareFunAbs.bdhoareF_abs_spec env f inv - let eq_params = - f_eqparams - fo_l.f_sig.fs_arg fo_l.f_sig.fs_anames ml - fo_r.f_sig.fs_arg fo_r.f_sig.fs_anames mr in - - let eq_res = - f_eqres fo_l.f_sig.fs_ret ml fo_r.f_sig.fs_ret mr in - - let invs = if use then [eqglob; inv] else [inv] in - let pre = map_ts_inv (fun invs -> EcFol.f_ands (eq_params :: invs)) invs in - let post = map_ts_inv (fun invs -> EcFol.f_ands (eq_res :: invs)) invs in - f_equivF pre o_l o_r post - in - - let sg = List.map2 ospec (OI.allowed oil) (OI.allowed oir) in - - let eq_params = - f_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 lpre = [eqglob;inv] in - let pre = map_ts_inv (fun lpre -> f_ands (eq_params::lpre)) lpre in - let post = map_ts_inv f_ands [eq_res; eqglob; inv] in - - (pre, post, sg) + let equivF_abs_spec (_ : proofenv) env fl fr inv = + EcEquivFunAbs.equivF_abs_spec env fl fr inv end -(* ------------------------------------------------------------------ *) -let t_hoareF_abs_r inv tc = - let env = FApi.tc1_env tc in - let hf = tc1_as_hoareF tc in - let pre, post, sg = FunAbsLow.hoareF_abs_spec !!tc env hf.hf_f inv in - - let tactic tc = FApi.xmutate1 tc `FunAbs sg in - FApi.t_last tactic (EcPhlConseq.t_hoareF_conseq pre (POE.lift post) tc) - -let t_ehoareF_abs_r inv tc = - let env = FApi.tc1_env tc in - let hf = tc1_as_ehoareF tc in - let pre, post, sg = FunAbsLow.ehoareF_abs_spec !!tc env hf.ehf_f inv in - - let tactic tc = FApi.xmutate1 tc `FunAbs sg in - FApi.t_last tactic (EcPhlConseq.t_ehoareF_conseq pre post tc) - -(* ------------------------------------------------------------------ *) -let t_bdhoareF_abs_ge_r inv tc = - let env = FApi.tc1_env tc in - let bhf = tc1_as_bdhoareF tc in - - match bhf.bhf_cmp with - | FHge when f_equal (bhf_bd bhf).inv f_r1 -> - let pre, post, sg = - FunAbsLow.bdhoareF_abs_spec !!tc env bhf.bhf_f inv - in - let tactic tc = FApi.xmutate1 tc `FunAbs sg in - FApi.t_last tactic (EcPhlConseq.t_bdHoareF_conseq pre post tc) - - | _ -> tc_error !!tc "bound must \">= 1%%r\"" - -let t_bdhoareF_abs_r inv tc = - let bhf = tc1_as_bdhoareF tc in - - match bhf.bhf_cmp with - | FHeq when f_equal (bhf_bd bhf).inv f_r1 -> - let tc = FApi.t_seqsub (EcPhlConseq.t_bdHoareF_conseq_bd FHge (bhf_bd bhf)) [EcLowGoal.t_close EcLowGoal.t_trivial; t_bdhoareF_abs_ge_r inv] tc in - let pl_goal_count = FApi.tc_count tc - 3 in - assert (pl_goal_count >= 0); - FApi.t_lasts (EcPhlConseq.t_bdHoareF_conseq_bd FHeq (bhf_bd bhf) |- FApi.t_first (EcLowGoal.t_close EcLowGoal.t_trivial)) pl_goal_count tc - | FHge when f_equal (bhf_bd bhf).inv f_r1 -> - t_bdhoareF_abs_ge_r inv tc - | _ -> tc_error !!tc "bound must \"= 1%%r\" or \">= 1%%r\"" - -(* ------------------------------------------------------------------ *) -let t_equivF_abs_r inv tc = - let env = FApi.tc1_env tc in - let ef = tc1_as_equivF tc in - let pre, post, sg = - FunAbsLow.equivF_abs_spec !!tc env ef.ef_fl ef.ef_fr inv - in - - let tactic tc = FApi.xmutate1 tc `FunAbs sg in - FApi.t_last tactic (EcPhlConseq.t_equivF_conseq pre post tc) - (* -------------------------------------------------------------------- *) -let t_hoareF_abs = FApi.t_low1 "hoare-fun-abs" t_hoareF_abs_r -let t_ehoareF_abs = FApi.t_low1 "ehoare-fun-abs" t_ehoareF_abs_r -let t_bdhoareF_abs = FApi.t_low1 "bdhoare-fun-abs" t_bdhoareF_abs_r -let t_equivF_abs = FApi.t_low1 "equiv-fun-abs" t_equivF_abs_r - -(* -------------------------------------------------------------------- *) -module UpToLow = struct - (* ------------------------------------------------------------------ *) - let equivF_abs_upto pf env weakened_pre fl fr (bad: ss_inv) (invP: ts_inv) (invQ: ts_inv) = - let weakened_pre = Option.value ~default:false weakened_pre in - - let (topl, _fl, oil, sigl), (topr, _fr, oir, sigr) = - EcLowPhlGoal.abstract_info2 env fl fr - in - - let ml, mr = invP.ml, invP.mr in - let bad = ss_inv_rebind bad invP.mr in - let bad2 = ss_inv_generalize_left bad invP.ml in - let allinv = map_ts_inv f_ands [bad2; invP; invQ] in - let fvl = PV.fv env ml allinv.inv in - let fvr = PV.fv env mr allinv.inv in - - PV.check_depend env fvl topl; - PV.check_depend env fvr topr; - - (* FIXME: check there is only global variable *) - let eqglob = ts_inv_eqglob topl ml topr mr in +let t_hoareF_abs inv = + EcHoareFunAbs.(t_hoareF_abs_full { hfa_inv = inv }) - let ospec o_l o_r = - check_oracle_use pf env topl o_l; - check_oracle_use pf env topr o_r; +let t_ehoareF_abs inv = + EcEHoareFunAbs.(t_ehoareF_abs_full { ehfa_inv = inv }) - let fo_l = EcEnv.Fun.by_xpath o_l env in - let fo_r = EcEnv.Fun.by_xpath o_r env in - let eq_params = - ts_inv_eqparams - fo_l.f_sig.fs_arg fo_l.f_sig.fs_anames ml - fo_r.f_sig.fs_arg fo_r.f_sig.fs_anames mr in +let t_bdhoareF_abs inv = + EcBdHoareFunAbs.(t_bdhoareF_abs_full { bhfa_inv = inv }) - let eq_res = - ts_inv_eqres fo_l.f_sig.fs_ret ml fo_r.f_sig.fs_ret mr in - - let pre = map_ts_inv EcFol.f_ands [map_ts_inv1 EcFol.f_not bad2; eq_params; invP] in - let post = map_ts_inv3 EcFol.f_if_simpl bad2 invQ (map_ts_inv2 f_and eq_res invP) in - let cond1 = f_equivF pre o_l o_r post in - if not weakened_pre then - let cond2 = - let f_r1 = {m=invQ.ml; inv=f_r1} in - let concl = ts_inv_lower_left1 (fun bq -> (f_bdHoareF bq o_l bq FHeq f_r1)) invQ in - f_forall_mems_ss_inv (mr, abstract_mt) - (map_ss_inv2 f_imp bad concl) in - let cond3 = - let f_r1 = {m=invQ.mr; inv=f_r1} in - let bq = map_ts_inv2 f_and bad2 invQ in - f_forall_mems_ss_inv (ml, abstract_mt) (ts_inv_lower_right1 (fun bq -> f_bdHoareF bq o_r bq FHeq f_r1) bq) in - - [cond1; cond2; cond3] - else - let cond2 = - let concl = ts_inv_lower_left1 (fun bq -> (f_hoareF bq o_l (POE.lift bq))) invQ in - f_forall_mems_ss_inv (mr, abstract_mt) - (map_ss_inv2 f_imp bad concl) in - let cond3 = - let bq = map_ts_inv2 f_and bad2 invQ in - f_forall_mems_ss_inv (ml, abstract_mt) (ts_inv_lower_right1 (fun bq -> f_hoareF bq o_r (POE.lift bq)) bq) in - - [cond1; cond2; cond3] - in - - let sg = List.map2 ospec (OI.allowed oil) (OI.allowed oir) in - let sg = List.flatten sg in - let lossless_a = if not weakened_pre then - [ lossless_hyps env topl fl.x_sub ] - else - [ f_losslessF fl; f_losslessF fr ] - in - let sg = lossless_a @ sg 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 = [eqglob;invP] in - let pre = map_ts_inv3 f_if_simpl bad2 invQ (map_ts_inv f_ands (eq_params::pre)) in - let post = map_ts_inv3 f_if_simpl bad2 invQ (map_ts_inv f_ands [eq_res;eqglob;invP]) in - - (pre, post, sg) -end +let t_equivF_abs inv = + EcEquivFunAbs.(t_equivF_abs_full { efa_inv = inv }) (* -------------------------------------------------------------------- *) -let t_equivF_abs_upto_r weakened_pre bad invP invQ tc = - let env = FApi.tc1_env tc in - let ef = tc1_as_equivF tc in - let pre, post, sg = - UpToLow.equivF_abs_upto !!tc env weakened_pre ef.ef_fl ef.ef_fr bad invP invQ - in - - let tactic tc = FApi.xmutate1 tc `FunUpto sg in - FApi.t_last tactic (EcPhlConseq.t_equivF_conseq pre post tc) - -let t_equivF_abs_upto = t_equivF_abs_upto_r - -(* -------------------------------------------------------------------- *) -module ToCodeLow = struct - (* ------------------------------------------------------------------ *) - let to_code env f m = - let fd = Fun.by_xpath f env in - let me = EcMemory.empty_local ~witharg:false m in - - let args = - let freshen_arg i ov = - match ov.ov_name with - | None -> { ov with ov_name = Some (Printf.sprintf "arg%d" (i + 1)) } - | Some _ -> ov - in List.mapi freshen_arg fd.f_sig.fs_anames - in - - let (me, args) = EcMemory.bindall_fresh args me in - - let res = { ov_name = Some "r"; ov_type = fd.f_sig.fs_ret; } in - - let me, res = EcMemory.bind_fresh res me in - - let eargs = List.map (fun v -> e_var (pv_loc (oget v.ov_name)) v.ov_type) args in - let args = - let var ov = { v_name = oget ov.ov_name; v_type = ov.ov_type } in - List.map var args - in - - let icall = - i_call (Some (LvVar (pv_loc (oget res.ov_name), res.ov_type)), f, eargs) - in (me, stmt [icall], res, args) - - let add_var env vfrom mfrom v m s = - PVM.add env vfrom mfrom (f_pvar (pv_loc (oget v.ov_name)) v.ov_type m).inv s - - let add_var_tuple env vfrom mfrom vs m s = - let vs = - List.map (fun v -> f_pvar (pv_loc v.v_name) v.v_type m) vs - in PVM.add env vfrom mfrom (map_ss_inv ~m f_tuple vs).inv s -end +let t_equivF_abs_upto weakened_pre bad invP invQ = + EcEquivFunAbsUpto.(t_equivF_abs_upto_full + { efu_ll = Option.value ~default:false weakened_pre; + efu_bad = bad; + efu_inv = invP; + efu_binv = invQ; }) (* -------------------------------------------------------------------- *) -let t_fun_to_code_hoare_r tc = - let env = FApi.tc1_env tc in - let hf = tc1_as_hoareF tc in - let f = hf.hf_f in - let m = hf.hf_m in - let (m0, mt), st, r, a = ToCodeLow.to_code env f m in - assert (EcIdent.id_equal m0 m); - let spr = ToCodeLow.add_var_tuple env pv_arg m a m PVM.empty in - let spo = ToCodeLow.add_var env pv_res m r m PVM.empty in - let pre = PVM.subst env spr (hf_pr hf).inv in - let post = POE.map (PVM.subst env spo) (hf_po hf).hsi_inv in - let concl = f_hoareS mt {m;inv=pre} st {hsi_m=m;hsi_inv=post} in - FApi.xmutate1 tc `FunToCode [concl] - -(* -------------------------------------------------------------------- *) -let t_fun_to_code_ehoare_r tc = - let env = FApi.tc1_env tc in - let hf = tc1_as_ehoareF tc in - let f = hf.ehf_f in - let m = hf.ehf_m in - let (m0, mt), st, r, a = ToCodeLow.to_code env f m in - assert (EcIdent.id_equal m0 m); - let spr = ToCodeLow.add_var_tuple env pv_arg m a m PVM.empty in - let spo = ToCodeLow.add_var env pv_res m r m PVM.empty in - - let pre = PVM.subst env spr (ehf_pr hf).inv in - let post = PVM.subst env spo (ehf_po hf).inv in - let concl = f_eHoareS mt {m;inv=pre} st {m;inv=post} in - - FApi.xmutate1 tc `FunToCode [concl] - -(* -------------------------------------------------------------------- *) -let t_fun_to_code_bdhoare_r tc = - let env = FApi.tc1_env tc in - let hf = tc1_as_bdhoareF tc in - let m = hf.bhf_m in - let f = hf.bhf_f in - let (m0, mt), st, r, a = ToCodeLow.to_code env f m in - assert (EcIdent.id_equal m0 m); - let spr = ToCodeLow.add_var_tuple env pv_arg m0 a m PVM.empty in - let spo = ToCodeLow.add_var env pv_res m0 r m PVM.empty in - let pre = PVM.subst env spr (bhf_pr hf).inv in - let post = PVM.subst env spo (bhf_po hf).inv in - let bd = PVM.subst env spr (bhf_bd hf).inv in - let concl = f_bdHoareS mt {m;inv=pre} st {m;inv=post} hf.bhf_cmp {m;inv=bd} in - FApi.xmutate1 tc `FunToCode [concl] - -(* -------------------------------------------------------------------- *) -let t_fun_to_code_equiv_r tc = - let env = FApi.tc1_env tc in - let ef = tc1_as_equivF tc in - let ml, mr = ef.ef_ml, ef.ef_mr in - let (fl,fr) = ef.ef_fl, ef.ef_fr in - let (ml0, mlt), sl, rl, al = ToCodeLow.to_code env fl ml in - assert (EcIdent.id_equal ml0 ml); - let (mr0, mrt), sr, rr, ar = ToCodeLow.to_code env fr mr in - assert (EcIdent.id_equal mr0 mr); - let spr = - let s = PVM.empty in - let s = ToCodeLow.add_var_tuple env pv_arg ml al ml s in - let s = ToCodeLow.add_var_tuple env pv_arg mr ar mr s in - s in - let spo = - let s = PVM.empty in - let s = ToCodeLow.add_var env pv_res ml rl ml s in - let s = ToCodeLow.add_var env pv_res mr rr mr s in - s in - let pre = PVM.subst env spr (ef_pr ef).inv in - let post = PVM.subst env spo (ef_po ef).inv in - let concl = f_equivS mlt mrt {ml;mr;inv=pre} sl sr {ml;mr;inv=post} in - - FApi.xmutate1 tc `FunToCode [concl] - -let t_fun_to_code_eager_r tc = - let env = FApi.tc1_env tc in - let eg = tc1_as_eagerF tc in - let ml, mr = eg.eg_ml, eg.eg_mr in - let (fl,fr) = eg.eg_fl, eg.eg_fr in - let (ml0, mlt), sl, rl, al = ToCodeLow.to_code env fl ml in - assert (EcIdent.id_equal ml0 ml); - let (mr0, mrt), sr, rr, ar = ToCodeLow.to_code env fr mr in - assert (EcIdent.id_equal mr0 mr); - let spr = - let s = PVM.empty in - let s = ToCodeLow.add_var_tuple env pv_arg ml0 al ml s in - let s = ToCodeLow.add_var_tuple env pv_arg mr0 ar mr s in - s in - let spo = - let s = PVM.empty in - let s = ToCodeLow.add_var env pv_res ml0 rl ml s in - let s = ToCodeLow.add_var env pv_res mr0 rr mr s in - s in - let pre = PVM.subst env spr (eg_pr eg).inv in - let post = PVM.subst env spo (eg_po eg).inv in - let concl = - f_equivS mlt mrt {ml;mr;inv=pre} (s_seq eg.eg_sl sl) (s_seq sr eg.eg_sr) {ml;mr;inv=post} in - FApi.xmutate1 tc `FunToCode [concl] - -(* -------------------------------------------------------------------- *) -let t_fun_to_code_hoare = FApi.t_low0 "hoare-fun-to-code" t_fun_to_code_hoare_r -let t_fun_to_code_ehoare = FApi.t_low0 "ehoare-fun-to-code" t_fun_to_code_ehoare_r -let t_fun_to_code_bdhoare = FApi.t_low0 "bdhoare-fun-to-code" t_fun_to_code_bdhoare_r -let t_fun_to_code_equiv = FApi.t_low0 "equiv-fun-to-code" t_fun_to_code_equiv_r -let t_fun_to_code_eager = FApi.t_low0 "eager-fun-to-code" t_fun_to_code_eager_r - -(* -------------------------------------------------------------------- *) -let t_fun_to_code_r tc = - let th = t_fun_to_code_hoare in - let teh = t_fun_to_code_ehoare in - let tbh = t_fun_to_code_bdhoare in - let te = t_fun_to_code_equiv in - let teg = t_fun_to_code_eager in +let t_fun_to_code tc = + let th = EcHoareFunToCode.t_hoareF_fun_to_code in + let teh = EcEHoareFunToCode.t_ehoareF_fun_to_code in + let tbh = EcBdHoareFunToCode.t_bdhoareF_fun_to_code in + let te = EcEquivFunToCode.t_equivF_fun_to_code in + let teg = EcEagerFunToCode.t_eagerF_fun_to_code in t_hF_or_bhF_or_eF ~th ~teh ~tbh ~te ~teg tc -let t_fun_to_code = FApi.t_low0 "fun-to-code" t_fun_to_code_r - (* -------------------------------------------------------------------- *) -let t_fun_r (inv: inv) tc = +let t_fun (inv: inv) tc = let th tc = let inv = match inv with | Inv_ss inv -> inv @@ -581,7 +95,7 @@ let t_fun_r (inv: inv) tc = let h = destr_eHoareF (FApi.tc1_goal tc) in if NormMp.is_abstract_fun h.ehf_f env then t_ehoareF_abs inv tc - else t_ehoareF_fun_def tc + else EcEHoareFunDef.t_ehoareF_fun_def tc and tbh tc = let inv = match inv with @@ -606,8 +120,6 @@ let t_fun_r (inv: inv) tc = in t_hF_or_bhF_or_eF ~th ~teh ~tbh ~te tc -let t_fun = FApi.t_low1 "fun" t_fun_r - (* -------------------------------------------------------------------- *) let process_fun_def tc = let t_cont tcenv = @@ -618,57 +130,23 @@ let process_fun_def tc = (* -------------------------------------------------------------------- *) let process_fun_to_code tc = - t_fun_to_code_r tc + t_fun_to_code tc (* -------------------------------------------------------------------- *) -let process_fun_upto_info info tc = - let open EcParsetree in - let hyps = FApi.tc1_hyps tc in - let ml, mr = (EcIdent.create "&1", EcIdent.create "&2") in - let env' = LDecl.inv_memenv ml mr hyps in - let p = TTC.pf_process_form !!tc env' tbool info.fui_pre in - let q = info.fui_pos |> omap (TTC.pf_process_form !!tc env' tbool) |> odfl f_true in - let m = EcIdent.create "&hr" in - let bad = - let env' = LDecl.push_active_ss (EcMemory.abstract m) hyps in - TTC.pf_process_form !!tc env' tbool info.fui_bad - in - (info.fui_is_ll_variant, { inv = bad; m }, { inv = p; ml; mr }, { inv = q; ml; mr }) +let process_fun_upto_info (info : EcParsetree.fun_upto_info) tc = + let r = EcEquivFunAbsUpto.process_equivF_abs_upto_info info tc in + EcEquivFunAbsUpto.(info.fui_is_ll_variant, r.efu_bad, r.efu_inv, r.efu_binv) (* -------------------------------------------------------------------- *) -let process_fun_upto info g = - let (weakened_pre, bad, p, q) = process_fun_upto_info info g in - t_equivF_abs_upto weakened_pre bad p q g +let process_fun_upto info tc = + EcEquivFunAbsUpto.process_equivF_abs_upto info tc (* -------------------------------------------------------------------- *) +(* Dispatch on the goal kind only; each logic types the invariant. *) let process_fun_abs inv tc = - let t_hoare tc = - let hyps = FApi.tc1_hyps tc in - let m = EcIdent.create "&hr" in - let env' = LDecl.inv_memenv1 m hyps in - let inv = TTC.pf_process_form !!tc env' tbool inv in - t_hoareF_abs {inv;m} tc - - and t_ehoare tc = - let hyps = FApi.tc1_hyps tc in - let m = EcIdent.create "&hr" in - let env' = LDecl.inv_memenv1 m hyps in - let inv = TTC.pf_process_xreal !!tc env' inv in - t_ehoareF_abs {inv;m} tc - - and t_bdhoare tc = - let hyps = FApi.tc1_hyps tc in - let m = EcIdent.create "&hr" in - let env' = LDecl.inv_memenv1 m hyps in - let inv = TTC.pf_process_form !!tc env' tbool inv in - t_bdhoareF_abs {inv;m} tc - - and t_equiv tc = - let hyps = FApi.tc1_hyps tc in - let ml, mr = EcIdent.create "&1", EcIdent.create "&2" in - let env' = LDecl.inv_memenv ml mr hyps in - let inv = TTC.pf_process_form !!tc env' tbool inv in - t_equivF_abs {inv;ml;mr} tc - - in - t_hF_or_bhF_or_eF ~th:t_hoare ~teh:t_ehoare ~tbh:t_bdhoare ~te:t_equiv tc + t_hF_or_bhF_or_eF + ~th:(EcHoareFunAbs.process_hoareF_abs inv) + ~teh:(EcEHoareFunAbs.process_ehoareF_abs inv) + ~tbh:(EcBdHoareFunAbs.process_bdhoareF_abs inv) + ~te:(EcEquivFunAbs.process_equivF_abs inv) + tc diff --git a/src/phl/rules/bdhoare/ecBdHoareFunAbs.ml b/src/phl/rules/bdhoare/ecBdHoareFunAbs.ml new file mode 100644 index 000000000..21bc4cc3f --- /dev/null +++ b/src/phl/rules/bdhoare/ecBdHoareFunAbs.ml @@ -0,0 +1,113 @@ +(* -------------------------------------------------------------------- *) +open EcUtils +open EcParsetree +open EcTypes +open EcFol +open EcAst +open EcModules +open EcEnv +open EcPV + +open EcCoreGoal +open EcLowPhlGoal + +module TTC = EcProofTyping + +(* -------------------------------------------------------------------- *) +(* Parameter of the bdhoare abstract-procedure rule: the invariant, already + typed. Nothing to resolve: the same record is the rule argument and the + node payload. *) +type bdhoare_fun_abs = { + bhfa_inv : ss_inv; (* invariant I *) +} + +type EcCoreGoal.rule += RBdHoareFunAbs of bdhoare_fun_abs + +(* -------------------------------------------------------------------- *) +let bdhoareF_abs_spec (env : env) (f : EcPath.xpath) (inv : ss_inv) = + let (top, _, oi, _) = EcLowPhlGoal.abstract_info env f in + let fv = PV.fv env inv.m inv.inv in + + PV.check_depend env fv top; + let ospec o = + EcPlFun.check_oracle_use env top o; + f_bdHoareF inv o inv FHge {m=inv.m;inv=f_r1} in + + let sg = List.map ospec (OI.allowed oi) in + (inv, inv, EcPlFun.lossless_hyps env top f.x_sub :: sg) + +(* -------------------------------------------------------------------- *) +(* Pure core shared by the rule and its checker. Its side conditions (the + procedure is abstract, the invariant does not depend on its globals, the + oracles do not access them, the goal is [phoare [f : I ==> I] >= 1%r]) + are part of it, so the checker re-validates them. *) +let bdhoareF_abs_subgoals + (hyps : LDecl.hyps) (bhf : bdHoareF) (n : bdhoare_fun_abs) += + if not (bhf.bhf_cmp = FHge && f_equal (bhf_bd bhf).inv f_r1) then + failwith "bdhoareF-fun-abs: the bound is not [>= 1%r]"; + let pre, post, sg = bdhoareF_abs_spec (LDecl.toenv hyps) bhf.bhf_f n.bhfa_inv in + if not ( EcReduction.ss_inv_alpha_eq hyps (bhf_pr bhf) pre + && EcReduction.ss_inv_alpha_eq hyps (bhf_po bhf) post) then + failwith "bdhoareF-fun-abs: the judgement is not [I ==> I]"; + sg + +(* -------------------------------------------------------------------- *) +let bad_bound_ge tc = tc_error !!tc "bound must \">= 1%%r\"" + +(* Rule (TCB). *) +let t_bdhoareF_abs (r : bdhoare_fun_abs) (tc : tcenv1) = + let bhf = tc1_as_bdhoareF tc in + if not (bhf.bhf_cmp = FHge && f_equal (bhf_bd bhf).inv f_r1) then + bad_bound_ge tc; + FApi.xrule1 tc (RBdHoareFunAbs r) + (bdhoareF_abs_subgoals (FApi.tc1_hyps tc) bhf r) + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | RBdHoareFunAbs n -> + Some (EcPlRecheck.checker_of "bdhoareF-fun-abs" pf_as_bdhoareF + (fun hyps bhf -> bdhoareF_abs_subgoals hyps bhf n)) + | _ -> None) + +(* -------------------------------------------------------------------- *) +(* Derived (no proof-node): the consequence to [I ==> I], then the rule; an + [= 1%r] goal goes through [>= 1%r] with the bound-changing consequence. + + TEMPORARY: the consequence rules still come from the not-yet-migrated + [EcPhlConseq]. *) +let t_bdhoareF_abs_ge (r : bdhoare_fun_abs) (tc : tcenv1) = + let env = FApi.tc1_env tc in + let bhf = tc1_as_bdhoareF tc in + + match bhf.bhf_cmp with + | FHge when f_equal (bhf_bd bhf).inv f_r1 -> + let pre, post, _ = bdhoareF_abs_spec env bhf.bhf_f r.bhfa_inv in + FApi.t_last (t_bdhoareF_abs r) + (EcPhlConseq.t_bdHoareF_conseq pre post tc) + + | _ -> bad_bound_ge tc + +let t_bdhoareF_abs_full (r : bdhoare_fun_abs) (tc : tcenv1) = + let bhf = tc1_as_bdhoareF tc in + + match bhf.bhf_cmp with + | FHeq when f_equal (bhf_bd bhf).inv f_r1 -> + let tc = FApi.t_seqsub (EcPhlConseq.t_bdHoareF_conseq_bd FHge (bhf_bd bhf)) [EcLowGoal.t_close EcLowGoal.t_trivial; t_bdhoareF_abs_ge r] tc in + let pl_goal_count = FApi.tc_count tc - 3 in + assert (pl_goal_count >= 0); + FApi.t_lasts (EcPhlConseq.t_bdHoareF_conseq_bd FHeq (bhf_bd bhf) |- FApi.t_first (EcLowGoal.t_close EcLowGoal.t_trivial)) pl_goal_count tc + | FHge when f_equal (bhf_bd bhf).inv f_r1 -> + t_bdhoareF_abs_ge r tc + | _ -> tc_error !!tc "bound must \"= 1%%r\" or \">= 1%%r\"" + +(* -------------------------------------------------------------------- *) +(* Elaboration: the goal is known to be a [bdhoareF]. *) +let process_bdhoareF_abs (inv : pformula) (tc : tcenv1) = + let hyps = FApi.tc1_hyps tc in + let m = EcIdent.create "&hr" in + let env' = LDecl.inv_memenv1 m hyps in + let inv = TTC.pf_process_form !!tc env' tbool inv in + t_bdhoareF_abs_full { bhfa_inv = { inv; m; } } tc diff --git a/src/phl/rules/bdhoare/ecBdHoareFunAbs.mli b/src/phl/rules/bdhoare/ecBdHoareFunAbs.mli new file mode 100644 index 000000000..53ae7423d --- /dev/null +++ b/src/phl/rules/bdhoare/ecBdHoareFunAbs.mli @@ -0,0 +1,65 @@ +(* -------------------------------------------------------------------- *) +open EcParsetree +open EcCoreGoal.FApi +open EcPath +open EcAst +open EcEnv + +(* ==================================================================== *) +(* Rules (trusted) *) + +type bdhoare_fun_abs = { + bhfa_inv : ss_inv; (* invariant I *) +} + +(* [t_bdhoareF_abs { bhfa_inv = I }] — an abstract procedure that is + lossless when its oracles are, preserves with probability 1 an invariant + its oracles preserve with probability 1: + + forall (O1 <: T1 {-A}) ... (On <: Tn {-A}), + islossless o_1 => ... => islossless o_k => islossless A(O1..On).g + phoare [o_1 : I ==> I] >= 1%r ... phoare [o_k : I ==> I] >= 1%r + ------------------------------------------------------------------ + phoare [f : I ==> I] >= 1%r + + where [f] is [A(...).g], [o_1 ... o_k] the oracles [f] may call ([o_i] + in the first premise being the corresponding procedure of the [Oj]). + Side conditions: [f] (normalized) is a procedure of an abstract module + [A], [I] does not depend on [glob A], no oracle [o_i] accesses [glob A], + and the goal is exactly [phoare [f : I ==> I] >= 1%r] (the bound + syntactically [1%r]) (otherwise fails). + + Node: [RBdHoareFunAbs { bhfa_inv = I }]. Checker: "bdhoareF-fun-abs". *) +val t_bdhoareF_abs : bdhoare_fun_abs -> backward + +(* [bdhoareF_abs_spec env f I] is [(I, I, premises)]: the pre- and + postcondition of the conclusion of [t_bdhoareF_abs], and its premises. + Fails if [f] is not abstract, [I] depends on its globals or an oracle + accesses them. *) +val bdhoareF_abs_spec : env -> xpath -> ss_inv -> ss_inv * ss_inv * form list + +(* ==================================================================== *) +(* Derived tactics *) + +(* [t_bdhoareF_abs_full { bhfa_inv = I }] — on [phoare [f : P ==> Q] ~ 1%r] + ([~] being [>=] or [=], the bound syntactically [1%r]; fails otherwise): + - for [>=]: the consequence rule (currently + [EcPhlConseq.t_bdHoareF_conseq]) to [phoare [f : I ==> I] >= 1%r], + then [t_bdhoareF_abs] on it. Visible goals: the two side conditions of + the consequence ([P => I], [I => Q]), the losslessness premise, then + [phoare [o_i : I ==> I] >= 1%r] for each oracle; + - for [=]: the bound-changing consequence (currently + [EcPhlConseq.t_bdHoareF_conseq_bd]) to [>= 1%r], whose side condition + is closed by [trivial], then the [>=] case; each oracle premise is + turned back into [phoare [o_i : I ==> I] = 1%r] by the bound-changing + consequence, its side condition closed by [trivial]. Visible goals: + as for [>=], with [= 1%r] oracle premises. + Emits no node of its own. *) +val t_bdhoareF_abs_full : bdhoare_fun_abs -> backward + +(* ==================================================================== *) +(* Elaboration *) + +(* [proc I] on a [bdhoareF] goal for an abstract procedure: [I] is typed as + a boolean formula in a memory [&hr]. Applies [t_bdhoareF_abs_full]. *) +val process_bdhoareF_abs : pformula -> backward diff --git a/src/phl/rules/bdhoare/ecBdHoareFunDef.ml b/src/phl/rules/bdhoare/ecBdHoareFunDef.ml new file mode 100644 index 000000000..67cb19b1f --- /dev/null +++ b/src/phl/rules/bdhoare/ecBdHoareFunDef.ml @@ -0,0 +1,47 @@ +(* -------------------------------------------------------------------- *) +open EcUtils +open EcTypes +open EcFol +open EcAst +open EcEnv +open EcPV + +open EcCoreGoal +open EcLowPhlGoal + +(* -------------------------------------------------------------------- *) +(* The bdhoare [fun-def] rule has no parameters. *) +type EcCoreGoal.rule += RBdHoareFunDef + +(* -------------------------------------------------------------------- *) +(* Pure core shared by the rule and its checker. Its side condition (the + procedure is concrete) is part of it, so the checker re-validates it. *) +let bdhoareF_fun_def_subgoals (hyps : LDecl.hyps) (bhf : bdHoareF) : form list = + let env = LDecl.toenv hyps in + let f = NormMp.norm_xfun env bhf.bhf_f in + EcPlFun.ensure_concrete "bdhoareF-fun-def" env f; + let (memenv, (fsig, fdef), env) = Fun.hoareS bhf.bhf_m f env in + let m = EcMemory.memory memenv in + let fres = odfl {m;inv=f_tt} (omap (ss_inv_of_expr m) fdef.f_ret) in + let post = map_ss_inv2 (PVM.subst1 env pv_res m) fres (bhf_po bhf) in + let spre = EcPlFun.subst_pre env fsig m PVM.empty in + let pre = map_ss_inv1 (PVM.subst env spre) (bhf_pr bhf) in + let bd = map_ss_inv1 (PVM.subst env spre) (bhf_bd bhf) in + [f_bdHoareS (snd memenv) pre fdef.f_body post bhf.bhf_cmp bd] + +(* -------------------------------------------------------------------- *) +(* Rule (TCB). *) +let t_bdhoareF_fun_def (tc : tcenv1) = + let env = FApi.tc1_env tc in + let bhf = tc1_as_bdhoareF tc in + EcPlFun.check_concrete !!tc env (NormMp.norm_xfun env bhf.bhf_f); + FApi.xrule1 tc RBdHoareFunDef (bdhoareF_fun_def_subgoals (FApi.tc1_hyps tc) bhf) + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | RBdHoareFunDef -> + Some (EcPlRecheck.checker_of "bdhoareF-fun-def" pf_as_bdhoareF + bdhoareF_fun_def_subgoals) + | _ -> None) diff --git a/src/phl/rules/bdhoare/ecBdHoareFunDef.mli b/src/phl/rules/bdhoare/ecBdHoareFunDef.mli new file mode 100644 index 000000000..dbad6fb5a --- /dev/null +++ b/src/phl/rules/bdhoare/ecBdHoareFunDef.mli @@ -0,0 +1,20 @@ +(* -------------------------------------------------------------------- *) +open EcCoreGoal.FApi + +(* ==================================================================== *) +(* Rules (trusted) *) + +(* [t_bdhoareF_fun_def] — a concrete procedure, by its body, with [~] the + goal's comparison: + + phoare [body : P[arg := xs] ==> Q[res := e]] ~ d[arg := xs] + ----------------------------------------------------------- f concrete + phoare [f : P ==> Q] ~ d + + where [f] (normalized) is [proc f(x1, ..., xn) = { body; return e }], + [xs] is [(x1, ..., xn)] ([e] is [tt] when [f] returns nothing), in the + memory of [f] extended with its parameters and locals. Side condition: + [f] is not abstract (otherwise fails). + + Node: [RBdHoareFunDef]. Checker: "bdhoareF-fun-def". *) +val t_bdhoareF_fun_def : backward diff --git a/src/phl/rules/bdhoare/ecBdHoareFunToCode.ml b/src/phl/rules/bdhoare/ecBdHoareFunToCode.ml new file mode 100644 index 000000000..0cb7cda4a --- /dev/null +++ b/src/phl/rules/bdhoare/ecBdHoareFunToCode.ml @@ -0,0 +1,45 @@ +(* -------------------------------------------------------------------- *) +open EcTypes +open EcFol +open EcAst +open EcEnv +open EcPV + +open EcCoreGoal +open EcLowPhlGoal + +(* -------------------------------------------------------------------- *) +(* The bdhoare [fun-to-code] rule has no parameters. *) +type EcCoreGoal.rule += RBdHoareFunToCode + +(* -------------------------------------------------------------------- *) +(* Pure core shared by the rule and its checker. The fresh variables are + chosen deterministically from the memory of the goal. *) +let bdhoareF_fun_to_code_subgoals (hyps : LDecl.hyps) (hf : bdHoareF) : form list = + let env = LDecl.toenv hyps in + let m = hf.bhf_m in + let f = hf.bhf_f in + let (m0, mt), st, r, a = EcPlFun.to_code env f m in + assert (EcIdent.id_equal m0 m); + let spr = EcPlFun.add_var_tuple env pv_arg m0 a m PVM.empty in + let spo = EcPlFun.add_var env pv_res m0 r m PVM.empty in + let pre = PVM.subst env spr (bhf_pr hf).inv in + let post = PVM.subst env spo (bhf_po hf).inv in + let bd = PVM.subst env spr (bhf_bd hf).inv in + [f_bdHoareS mt {m;inv=pre} st {m;inv=post} hf.bhf_cmp {m;inv=bd}] + +(* -------------------------------------------------------------------- *) +(* Rule (TCB). *) +let t_bdhoareF_fun_to_code (tc : tcenv1) = + let hf = tc1_as_bdhoareF tc in + FApi.xrule1 tc RBdHoareFunToCode + (bdhoareF_fun_to_code_subgoals (FApi.tc1_hyps tc) hf) + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | RBdHoareFunToCode -> + Some (EcPlRecheck.checker_of "bdhoareF-fun-to-code" pf_as_bdhoareF + bdhoareF_fun_to_code_subgoals) + | _ -> None) diff --git a/src/phl/rules/bdhoare/ecBdHoareFunToCode.mli b/src/phl/rules/bdhoare/ecBdHoareFunToCode.mli new file mode 100644 index 000000000..20b16f240 --- /dev/null +++ b/src/phl/rules/bdhoare/ecBdHoareFunToCode.mli @@ -0,0 +1,19 @@ +(* -------------------------------------------------------------------- *) +open EcCoreGoal.FApi + +(* ==================================================================== *) +(* Rules (trusted) *) + +(* [t_bdhoareF_fun_to_code] — a procedure, as a single call ([proc*]), + with [~] the goal's comparison: + + phoare [r <@ f(as) : P[arg := as] ==> Q[res := r]] ~ d[arg := as] + ----------------------------------------------------------------- + phoare [f : P ==> Q] ~ d + + where [as] is [(a1, ..., an)], [a1 ... an] and [r] being fresh local + variables of the memory (the parameters of [f], unnamed ones named + [arg], and its result). + + Node: [RBdHoareFunToCode]. Checker: "bdhoareF-fun-to-code". *) +val t_bdhoareF_fun_to_code : backward diff --git a/src/phl/rules/eager/ecEagerFunToCode.ml b/src/phl/rules/eager/ecEagerFunToCode.ml new file mode 100644 index 000000000..cbf5f4d1d --- /dev/null +++ b/src/phl/rules/eager/ecEagerFunToCode.ml @@ -0,0 +1,55 @@ +(* -------------------------------------------------------------------- *) +open EcTypes +open EcFol +open EcAst +open EcModules +open EcEnv +open EcPV + +open EcCoreGoal +open EcLowPhlGoal + +(* -------------------------------------------------------------------- *) +(* The eager [fun-to-code] rule has no parameters. *) +type EcCoreGoal.rule += REagerFunToCode + +(* -------------------------------------------------------------------- *) +(* Pure core shared by the rule and its checker. The fresh variables are + chosen deterministically from the memories of the goal. *) +let eagerF_fun_to_code_subgoals (hyps : LDecl.hyps) (eg : eagerF) : form list = + let env = LDecl.toenv hyps in + let ml, mr = eg.eg_ml, eg.eg_mr in + let (fl,fr) = eg.eg_fl, eg.eg_fr in + let (ml0, mlt), sl, rl, al = EcPlFun.to_code env fl ml in + assert (EcIdent.id_equal ml0 ml); + let (mr0, mrt), sr, rr, ar = EcPlFun.to_code env fr mr in + assert (EcIdent.id_equal mr0 mr); + let spr = + let s = PVM.empty in + let s = EcPlFun.add_var_tuple env pv_arg ml0 al ml s in + let s = EcPlFun.add_var_tuple env pv_arg mr0 ar mr s in + s in + let spo = + let s = PVM.empty in + let s = EcPlFun.add_var env pv_res ml0 rl ml s in + let s = EcPlFun.add_var env pv_res mr0 rr mr s in + s in + let pre = PVM.subst env spr (eg_pr eg).inv in + let post = PVM.subst env spo (eg_po eg).inv in + [f_equivS mlt mrt {ml;mr;inv=pre} (s_seq eg.eg_sl sl) (s_seq sr eg.eg_sr) {ml;mr;inv=post}] + +(* -------------------------------------------------------------------- *) +(* Rule (TCB). *) +let t_eagerF_fun_to_code (tc : tcenv1) = + let eg = tc1_as_eagerF tc in + FApi.xrule1 tc REagerFunToCode + (eagerF_fun_to_code_subgoals (FApi.tc1_hyps tc) eg) + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | REagerFunToCode -> + Some (EcPlRecheck.checker_of "eagerF-fun-to-code" pf_as_eagerF + eagerF_fun_to_code_subgoals) + | _ -> None) diff --git a/src/phl/rules/eager/ecEagerFunToCode.mli b/src/phl/rules/eager/ecEagerFunToCode.mli new file mode 100644 index 000000000..02af2aebd --- /dev/null +++ b/src/phl/rules/eager/ecEagerFunToCode.mli @@ -0,0 +1,20 @@ +(* -------------------------------------------------------------------- *) +open EcCoreGoal.FApi + +(* ==================================================================== *) +(* Rules (trusted) *) + +(* [t_eagerF_fun_to_code] — an eager judgement, its procedures as single + calls ([proc*]): + + equiv [s; r1 <@ f1(as1) ~ r2 <@ f2(as2); s' : + P[arg<1> := as1, arg<2> := as2] ==> Q[res<1> := r1, res<2> := r2]] + --------------------------------------------------------------------------- + eager [s, f1 ~ f2, s' : P ==> Q] + + where [asi] is [(a1, ..., an)], [a1 ... an] and [ri] being fresh local + variables of the memory of side [i] (the parameters of [fi], unnamed + ones named [arg], and its result). + + Node: [REagerFunToCode]. Checker: "eagerF-fun-to-code". *) +val t_eagerF_fun_to_code : backward diff --git a/src/phl/rules/ecPlFun.ml b/src/phl/rules/ecPlFun.ml new file mode 100644 index 000000000..4df14cdcb --- /dev/null +++ b/src/phl/rules/ecPlFun.ml @@ -0,0 +1,106 @@ +(* -------------------------------------------------------------------- *) +open EcUtils +open EcPath +open EcAst +open EcTypes +open EcFol +open EcModules +open EcEnv +open EcPV + +open EcCoreGoal + +(* -------------------------------------------------------------------- *) +let check_concrete (pf : proofenv) (env : env) (f : xpath) = + if NormMp.is_abstract_fun f env then + tc_error_lazy pf (fun fmt -> + let ppe = EcPrinting.PPEnv.ofenv env in + Format.fprintf fmt + "The function %a is abstract. Provide an invariant to the [proc] tactic" + (EcPrinting.pp_funname ppe) f) + +let ensure_concrete (name : string) (env : env) (f : xpath) = + if NormMp.is_abstract_fun f env then + failwith (name ^ ": the procedure is abstract") + +(* -------------------------------------------------------------------- *) +let subst_pre (env : env) (fs : funsig) (m : memory) (s : PVM.subst) = + let fresh ov = + match ov.ov_name with + | None -> assert false; + | Some v -> { v_name = v; v_type = ov.ov_type } + in + let v = List.map (fun v -> f_pvloc (fresh v) m) fs.fs_anames in + PVM.add env pv_arg m (map_ss_inv ~m f_tuple v).inv s + +(* -------------------------------------------------------------------- *) +(* FIXME: oracles should ensure they preserve the state of the adversaries + * + * Two solutions: + * - add the equalities in the pre and post. + * - ensure that oracle doesn't write the adversaries states + * + * See [ospec] in [EcEquivFunAbs] / [EcEquivFunAbsUpto]. *) +let check_oracle_use (env : env) (adv : mpath) (o : xpath) = + let restr = { mr_empty with ur_neg = Sx.empty, Sm.singleton adv } in + + (* This only checks the memory restrictions. *) + EcTyping.check_mem_restr_fun env o restr + +(* -------------------------------------------------------------------- *) +let lossless_hyps (env : env) (top : mpath) (sub : EcSymbols.symbol) = + let clear_to_top = { mr_empty with ur_neg = Sx.empty, Sm.singleton top } in + + let sig_ = EcEnv.NormMp.sig_of_mp env top in + let bd = + List.map + (fun (id, mt) -> + (id, GTmodty (mt, clear_to_top)) + ) sig_.mis_params + in + (* WARN: this implies that the oracle do not have access to top *) + let args = List.map (fun (id,_) -> EcPath.mident id) sig_.mis_params in + let concl = f_losslessF (EcPath.xpath (EcPath.m_apply top args) sub) in + let calls = + let name = sub in + (EcSymbols.Msym.find name sig_.mis_oinfos) |> OI.allowed + in + let hyps = List.map f_losslessF calls in + f_forall bd (f_imps hyps concl) + +(* -------------------------------------------------------------------- *) +let to_code (env : env) (f : xpath) (m : memory) = + let fd = Fun.by_xpath f env in + let me = EcMemory.empty_local ~witharg:false m in + + let args = + let freshen_arg i ov = + match ov.ov_name with + | None -> { ov with ov_name = Some (Printf.sprintf "arg%d" (i + 1)) } + | Some _ -> ov + in List.mapi freshen_arg fd.f_sig.fs_anames + in + + let (me, args) = EcMemory.bindall_fresh args me in + + let res = { ov_name = Some "r"; ov_type = fd.f_sig.fs_ret; } in + + let me, res = EcMemory.bind_fresh res me in + + let eargs = List.map (fun v -> e_var (pv_loc (oget v.ov_name)) v.ov_type) args in + let args = + let var ov = { v_name = oget ov.ov_name; v_type = ov.ov_type } in + List.map var args + in + + let icall = + i_call (Some (LvVar (pv_loc (oget res.ov_name), res.ov_type)), f, eargs) + in (me, stmt [icall], res, args) + +let add_var env vfrom mfrom v m s = + PVM.add env vfrom mfrom (f_pvar (pv_loc (oget v.ov_name)) v.ov_type m).inv s + +let add_var_tuple env vfrom mfrom vs m s = + let vs = + List.map (fun v -> f_pvar (pv_loc v.v_name) v.v_type m) vs + in PVM.add env vfrom mfrom (map_ss_inv ~m f_tuple vs).inv s diff --git a/src/phl/rules/ecPlFun.mli b/src/phl/rules/ecPlFun.mli new file mode 100644 index 000000000..abbeb3d1a --- /dev/null +++ b/src/phl/rules/ecPlFun.mli @@ -0,0 +1,62 @@ +(* -------------------------------------------------------------------- *) +open EcSymbols +open EcPath +open EcAst +open EcModules +open EcEnv +open EcCoreGoal + +(* -------------------------------------------------------------------- *) +(* Computations shared by the procedure rules ([proc]) of every logic: + unfolding a concrete procedure ([EcFunDef]), the oracle and + losslessness conditions of the abstract-procedure rules + ([EcFunAbs], [EcEquivFunAbsUpto]) and the single-call statement + of [proc*] ([EcFunToCode]). *) + +(* -------------------------------------------------------------------- *) +(* Concrete procedures. *) + +(* Fails with a user-facing error when [f] is abstract. *) +val check_concrete : proofenv -> env -> xpath -> unit + +(* Same, for the subgoal builders: fails with [Failure ": ..."]. *) +val ensure_concrete : string -> env -> xpath -> unit + +(* [subst_pre env fs m s] extends [s] with [arg{m} := (x1, ..., xn){m}], + [x1 ... xn] the parameters of the signature [fs]. *) +val subst_pre : env -> funsig -> memory -> EcPV.PVM.subst -> EcPV.PVM.subst + +(* -------------------------------------------------------------------- *) +(* Abstract procedures. *) + +(* [check_oracle_use env top o]: the oracle [o] does not write the globals + of the abstract module [top] (fails otherwise). *) +val check_oracle_use : env -> mpath -> xpath -> unit + +(* [lossless_hyps env top f]: the procedure [f] of the abstract functor + [top] is lossless when its oracles are: + forall (O1 <: T1 {-top}) ... (On <: Tn {-top}), + islossless o_1 => ... => islossless o_k => islossless top(O1..On).f + [o_1 ... o_k] being the oracles [f] may call. *) +val lossless_hyps : env -> mpath -> symbol -> form + +(* -------------------------------------------------------------------- *) +(* Procedure to code ([proc*]). *) + +(* [to_code env f m]: the statement [r <@ f(a1, ..., an)] in memory [m], + extended with fresh local variables [a1 ... an] (the parameters of + [f], unnamed ones named [arg]) and [r]. Returns the memory, the + statement, [r] and [a1 ... an]. Deterministic. *) +val to_code : + env -> xpath -> memory -> memenv * stmt * ovariable * variable list + +(* [add_var env x m v m' s] extends [s] with [x{m} := v{m'}]. *) +val add_var : + env -> prog_var -> memory -> ovariable -> memory + -> EcPV.PVM.subst -> EcPV.PVM.subst + +(* [add_var_tuple env x m vs m' s] extends [s] with + [x{m} := (v1, ..., vn){m'}]. *) +val add_var_tuple : + env -> prog_var -> memory -> variable list -> memory + -> EcPV.PVM.subst -> EcPV.PVM.subst diff --git a/src/phl/rules/ehoare/ecEHoareFunAbs.ml b/src/phl/rules/ehoare/ecEHoareFunAbs.ml new file mode 100644 index 000000000..58d99af76 --- /dev/null +++ b/src/phl/rules/ehoare/ecEHoareFunAbs.ml @@ -0,0 +1,78 @@ +(* -------------------------------------------------------------------- *) +open EcParsetree +open EcFol +open EcAst +open EcModules +open EcEnv +open EcPV + +open EcCoreGoal +open EcLowPhlGoal + +module TTC = EcProofTyping + +(* -------------------------------------------------------------------- *) +(* Parameter of the ehoare abstract-procedure rule: the invariant, already + typed. Nothing to resolve: the same record is the rule argument and the + node payload. *) +type ehoare_fun_abs = { + ehfa_inv : ss_inv; (* invariant I *) +} + +type EcCoreGoal.rule += REHoareFunAbs of ehoare_fun_abs + +(* -------------------------------------------------------------------- *) +let ehoareF_abs_spec (env : env) (f : EcPath.xpath) (inv : ss_inv) = + let (top, _, oi, _) = EcLowPhlGoal.abstract_info env f in + let fv = PV.fv env inv.m inv.inv in + PV.check_depend env fv top; + let ospec o = f_eHoareF inv o inv in + let sg = List.map ospec (OI.allowed oi) in + (inv, inv, sg) + +(* -------------------------------------------------------------------- *) +(* Pure core shared by the rule and its checker. Its side conditions (the + procedure is abstract, the invariant does not depend on its globals, the + goal is [ehoare [f : I ==> I]]) are part of it, so the checker + re-validates them. *) +let ehoareF_abs_subgoals (hyps : LDecl.hyps) (hf : eHoareF) (n : ehoare_fun_abs) = + let pre, post, sg = ehoareF_abs_spec (LDecl.toenv hyps) hf.ehf_f n.ehfa_inv in + if not ( EcReduction.ss_inv_alpha_eq hyps (ehf_pr hf) pre + && EcReduction.ss_inv_alpha_eq hyps (ehf_po hf) post) then + failwith "ehoareF-fun-abs: the judgement is not [I ==> I]"; + sg + +(* -------------------------------------------------------------------- *) +(* Rule (TCB). *) +let t_ehoareF_abs (r : ehoare_fun_abs) (tc : tcenv1) = + let hf = tc1_as_ehoareF tc in + FApi.xrule1 tc (REHoareFunAbs r) (ehoareF_abs_subgoals (FApi.tc1_hyps tc) hf r) + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | REHoareFunAbs n -> + Some (EcPlRecheck.checker_of "ehoareF-fun-abs" pf_as_ehoareF + (fun hyps hf -> ehoareF_abs_subgoals hyps hf n)) + | _ -> None) + +(* -------------------------------------------------------------------- *) +(* Derived (no proof-node): the consequence to [I ==> I], then the rule. + + TEMPORARY: the consequence rule still comes from the not-yet-migrated + [EcPhlConseq]. *) +let t_ehoareF_abs_full (r : ehoare_fun_abs) (tc : tcenv1) = + let env = FApi.tc1_env tc in + let hf = tc1_as_ehoareF tc in + let pre, post, _ = ehoareF_abs_spec env hf.ehf_f r.ehfa_inv in + FApi.t_last (t_ehoareF_abs r) (EcPhlConseq.t_ehoareF_conseq pre post tc) + +(* -------------------------------------------------------------------- *) +(* Elaboration: the goal is known to be an [ehoareF]. *) +let process_ehoareF_abs (inv : pformula) (tc : tcenv1) = + let hyps = FApi.tc1_hyps tc in + let m = EcIdent.create "&hr" in + let env' = LDecl.inv_memenv1 m hyps in + let inv = TTC.pf_process_xreal !!tc env' inv in + t_ehoareF_abs_full { ehfa_inv = { inv; m; } } tc diff --git a/src/phl/rules/ehoare/ecEHoareFunAbs.mli b/src/phl/rules/ehoare/ecEHoareFunAbs.mli new file mode 100644 index 000000000..e8a81245d --- /dev/null +++ b/src/phl/rules/ehoare/ecEHoareFunAbs.mli @@ -0,0 +1,52 @@ +(* -------------------------------------------------------------------- *) +open EcParsetree +open EcCoreGoal.FApi +open EcPath +open EcAst +open EcEnv + +(* ==================================================================== *) +(* Rules (trusted) *) + +type ehoare_fun_abs = { + ehfa_inv : ss_inv; (* invariant I (an extended real) *) +} + +(* [t_ehoareF_abs { ehfa_inv = I }] — an abstract procedure preserves an + invariant its oracles preserve: + + ehoare [o_1 : I ==> I] ... ehoare [o_k : I ==> I] + ---------------------------------------------------- f = A(...).g abstract + ehoare [f : I ==> I] I independent of glob A + + where [o_1 ... o_k] are the oracles [f] may call. Side conditions: [f] + (normalized) is a procedure of an abstract module [A], [I] does not + depend on [glob A], and the goal is exactly [ehoare [f : I ==> I]] + (otherwise fails). + + Node: [REHoareFunAbs { ehfa_inv = I }]. Checker: "ehoareF-fun-abs". *) +val t_ehoareF_abs : ehoare_fun_abs -> backward + +(* [ehoareF_abs_spec env f I] is [(I, I, premises)]: the pre- and + postcondition of the conclusion of [t_ehoareF_abs], and its premises. + Fails if [f] is not abstract or [I] depends on its globals. *) +val ehoareF_abs_spec : env -> xpath -> ss_inv -> ss_inv * ss_inv * form list + +(* ==================================================================== *) +(* Derived tactics *) + +(* [t_ehoareF_abs_full { ehfa_inv = I }] — on [ehoare [f : P ==> Q]]: + 1. the consequence rule (currently [EcPhlConseq.t_ehoareF_conseq]) to + [ehoare [f : I ==> I]]; + 2. then [t_ehoareF_abs] on it. + Visible goals: the two side conditions of the consequence ([I <= P] and + [Q <= I]), then [ehoare [o_i : I ==> I]] for each oracle. Emits no node + of its own. *) +val t_ehoareF_abs_full : ehoare_fun_abs -> backward + +(* ==================================================================== *) +(* Elaboration *) + +(* [proc I] on an [ehoareF] goal for an abstract procedure: [I] is typed as + an extended real in a memory [&hr]. Applies [t_ehoareF_abs_full]. *) +val process_ehoareF_abs : pformula -> backward diff --git a/src/phl/rules/ehoare/ecEHoareFunDef.ml b/src/phl/rules/ehoare/ecEHoareFunDef.ml new file mode 100644 index 000000000..ab293550c --- /dev/null +++ b/src/phl/rules/ehoare/ecEHoareFunDef.ml @@ -0,0 +1,45 @@ +(* -------------------------------------------------------------------- *) +open EcUtils +open EcTypes +open EcFol +open EcAst +open EcEnv +open EcPV + +open EcCoreGoal +open EcLowPhlGoal + +(* -------------------------------------------------------------------- *) +(* The ehoare [fun-def] rule has no parameters. *) +type EcCoreGoal.rule += REHoareFunDef + +(* -------------------------------------------------------------------- *) +(* Pure core shared by the rule and its checker. Its side condition (the + procedure is concrete) is part of it, so the checker re-validates it. *) +let ehoareF_fun_def_subgoals (hyps : LDecl.hyps) (hf : eHoareF) : form list = + let env = LDecl.toenv hyps in + let f = NormMp.norm_xfun env hf.ehf_f in + EcPlFun.ensure_concrete "ehoareF-fun-def" env f; + let (memenv, (fsig, fdef), env) = Fun.hoareS hf.ehf_m f env in + let m = EcMemory.memory memenv in + let fres = odfl {m;inv=f_tt} (omap (ss_inv_of_expr m) fdef.f_ret) in + let post = map_ss_inv2 (PVM.subst1 env pv_res m) fres (ehf_po hf) in + let pre = map_ss_inv1 (PVM.subst env (EcPlFun.subst_pre env fsig m PVM.empty)) (ehf_pr hf) in + [f_eHoareS (snd memenv) pre fdef.f_body post] + +(* -------------------------------------------------------------------- *) +(* Rule (TCB). *) +let t_ehoareF_fun_def (tc : tcenv1) = + let env = FApi.tc1_env tc in + let hf = tc1_as_ehoareF tc in + EcPlFun.check_concrete !!tc env (NormMp.norm_xfun env hf.ehf_f); + FApi.xrule1 tc REHoareFunDef (ehoareF_fun_def_subgoals (FApi.tc1_hyps tc) hf) + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | REHoareFunDef -> + Some (EcPlRecheck.checker_of "ehoareF-fun-def" pf_as_ehoareF + ehoareF_fun_def_subgoals) + | _ -> None) diff --git a/src/phl/rules/ehoare/ecEHoareFunDef.mli b/src/phl/rules/ehoare/ecEHoareFunDef.mli new file mode 100644 index 000000000..181599fe6 --- /dev/null +++ b/src/phl/rules/ehoare/ecEHoareFunDef.mli @@ -0,0 +1,19 @@ +(* -------------------------------------------------------------------- *) +open EcCoreGoal.FApi + +(* ==================================================================== *) +(* Rules (trusted) *) + +(* [t_ehoareF_fun_def] — a concrete procedure, by its body: + + ehoare [body : P[arg := (x1, ..., xn)] ==> Q[res := e]] + ------------------------------------------------------- f concrete + ehoare [f : P ==> Q] + + where [f] (normalized) is [proc f(x1, ..., xn) = { body; return e }] + ([e] is [tt] when [f] returns nothing), in the memory of [f] extended + with its parameters and locals. Side condition: [f] is not abstract + (otherwise fails). + + Node: [REHoareFunDef]. Checker: "ehoareF-fun-def". *) +val t_ehoareF_fun_def : backward diff --git a/src/phl/rules/ehoare/ecEHoareFunToCode.ml b/src/phl/rules/ehoare/ecEHoareFunToCode.ml new file mode 100644 index 000000000..990488ef1 --- /dev/null +++ b/src/phl/rules/ehoare/ecEHoareFunToCode.ml @@ -0,0 +1,44 @@ +(* -------------------------------------------------------------------- *) +open EcTypes +open EcFol +open EcAst +open EcEnv +open EcPV + +open EcCoreGoal +open EcLowPhlGoal + +(* -------------------------------------------------------------------- *) +(* The ehoare [fun-to-code] rule has no parameters. *) +type EcCoreGoal.rule += REHoareFunToCode + +(* -------------------------------------------------------------------- *) +(* Pure core shared by the rule and its checker. The fresh variables are + chosen deterministically from the memory of the goal. *) +let ehoareF_fun_to_code_subgoals (hyps : LDecl.hyps) (hf : eHoareF) : form list = + let env = LDecl.toenv hyps in + let f = hf.ehf_f in + let m = hf.ehf_m in + let (m0, mt), st, r, a = EcPlFun.to_code env f m in + assert (EcIdent.id_equal m0 m); + let spr = EcPlFun.add_var_tuple env pv_arg m a m PVM.empty in + let spo = EcPlFun.add_var env pv_res m r m PVM.empty in + let pre = PVM.subst env spr (ehf_pr hf).inv in + let post = PVM.subst env spo (ehf_po hf).inv in + [f_eHoareS mt {m;inv=pre} st {m;inv=post}] + +(* -------------------------------------------------------------------- *) +(* Rule (TCB). *) +let t_ehoareF_fun_to_code (tc : tcenv1) = + let hf = tc1_as_ehoareF tc in + FApi.xrule1 tc REHoareFunToCode + (ehoareF_fun_to_code_subgoals (FApi.tc1_hyps tc) hf) + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | REHoareFunToCode -> + Some (EcPlRecheck.checker_of "ehoareF-fun-to-code" pf_as_ehoareF + ehoareF_fun_to_code_subgoals) + | _ -> None) diff --git a/src/phl/rules/ehoare/ecEHoareFunToCode.mli b/src/phl/rules/ehoare/ecEHoareFunToCode.mli new file mode 100644 index 000000000..15392f635 --- /dev/null +++ b/src/phl/rules/ehoare/ecEHoareFunToCode.mli @@ -0,0 +1,17 @@ +(* -------------------------------------------------------------------- *) +open EcCoreGoal.FApi + +(* ==================================================================== *) +(* Rules (trusted) *) + +(* [t_ehoareF_fun_to_code] — a procedure, as a single call ([proc*]): + + ehoare [r <@ f(a1, ..., an) : P[arg := (a1, ..., an)] ==> Q[res := r]] + ----------------------------------------------------------------------- + ehoare [f : P ==> Q] + + where [a1 ... an] and [r] are fresh local variables of the memory (the + parameters of [f], unnamed ones named [arg], and its result). + + Node: [REHoareFunToCode]. Checker: "ehoareF-fun-to-code". *) +val t_ehoareF_fun_to_code : backward diff --git a/src/phl/rules/equiv/ecEquivFunAbs.ml b/src/phl/rules/equiv/ecEquivFunAbs.ml new file mode 100644 index 000000000..f0bcefb74 --- /dev/null +++ b/src/phl/rules/equiv/ecEquivFunAbs.ml @@ -0,0 +1,125 @@ +(* -------------------------------------------------------------------- *) +open EcParsetree +open EcTypes +open EcFol +open EcAst +open EcModules +open EcEnv +open EcPV + +open EcCoreGoal +open EcLowPhlGoal + +module TTC = EcProofTyping + +(* -------------------------------------------------------------------- *) +(* Parameter of the equiv abstract-procedure rule: the invariant, already + typed. Nothing to resolve: the same record is the rule argument and the + node payload. *) +type equiv_fun_abs = { + efa_inv : ts_inv; (* relational invariant I *) +} + +type EcCoreGoal.rule += REquivFunAbs of equiv_fun_abs + +(* -------------------------------------------------------------------- *) +let equivF_abs_spec (env : env) fl fr (inv : ts_inv) = + let (topl, _fl, oil, sigl), (topr, _fr, oir, sigr) = + EcLowPhlGoal.abstract_info2 env fl fr + in + + let ml, mr = inv.ml, inv.mr in + let fvl = PV.fv env inv.ml inv.inv in + let fvr = PV.fv env inv.mr inv.inv in + PV.check_depend env fvl topl; + PV.check_depend env fvr topr; + let eqglob = ts_inv_eqglob topl ml topr mr in + + let ospec o_l o_r = + let use = + try + EcPlFun.check_oracle_use env topl o_l; + EcPlFun.check_oracle_use env topr o_r; + false + with _ -> true + in + + let fo_l = EcEnv.Fun.by_xpath o_l env in + let fo_r = EcEnv.Fun.by_xpath o_r env in + + let eq_params = + f_eqparams + fo_l.f_sig.fs_arg fo_l.f_sig.fs_anames ml + fo_r.f_sig.fs_arg fo_r.f_sig.fs_anames mr in + + let eq_res = + f_eqres fo_l.f_sig.fs_ret ml fo_r.f_sig.fs_ret mr in + + let invs = if use then [eqglob; inv] else [inv] in + let pre = map_ts_inv (fun invs -> EcFol.f_ands (eq_params :: invs)) invs in + let post = map_ts_inv (fun invs -> EcFol.f_ands (eq_res :: invs)) invs in + f_equivF pre o_l o_r post + in + + let sg = List.map2 ospec (OI.allowed oil) (OI.allowed oir) in + + let eq_params = + f_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 lpre = [eqglob;inv] in + let pre = map_ts_inv (fun lpre -> f_ands (eq_params::lpre)) lpre in + let post = map_ts_inv f_ands [eq_res; eqglob; inv] in + + (pre, post, sg) + +(* -------------------------------------------------------------------- *) +(* Pure core shared by the rule and its checker. Its side conditions (the + procedures are instances of the same abstract procedure, the invariant + does not depend on its globals, the goal is the conclusion of the rule) + are part of it, so the checker re-validates them. *) +let equivF_abs_subgoals (hyps : LDecl.hyps) (ef : equivF) (n : equiv_fun_abs) = + let pre, post, sg = + equivF_abs_spec (LDecl.toenv hyps) ef.ef_fl ef.ef_fr n.efa_inv in + if not ( EcReduction.ts_inv_alpha_eq hyps (ef_pr ef) pre + && EcReduction.ts_inv_alpha_eq hyps (ef_po ef) post) then + failwith "equivF-fun-abs: the judgement is not the conclusion of the rule"; + sg + +(* -------------------------------------------------------------------- *) +(* Rule (TCB). *) +let t_equivF_abs (r : equiv_fun_abs) (tc : tcenv1) = + let ef = tc1_as_equivF tc in + FApi.xrule1 tc (REquivFunAbs r) (equivF_abs_subgoals (FApi.tc1_hyps tc) ef r) + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | REquivFunAbs n -> + Some (EcPlRecheck.checker_of "equivF-fun-abs" pf_as_equivF + (fun hyps ef -> equivF_abs_subgoals hyps ef n)) + | _ -> None) + +(* -------------------------------------------------------------------- *) +(* Derived (no proof-node): the consequence to the conclusion of the rule, + then the rule. + + TEMPORARY: the consequence rule still comes from the not-yet-migrated + [EcPhlConseq]. *) +let t_equivF_abs_full (r : equiv_fun_abs) (tc : tcenv1) = + let env = FApi.tc1_env tc in + let ef = tc1_as_equivF tc in + let pre, post, _ = equivF_abs_spec env ef.ef_fl ef.ef_fr r.efa_inv in + FApi.t_last (t_equivF_abs r) (EcPhlConseq.t_equivF_conseq pre post tc) + +(* -------------------------------------------------------------------- *) +(* Elaboration: the goal is known to be an [equivF]. *) +let process_equivF_abs (inv : pformula) (tc : tcenv1) = + let hyps = FApi.tc1_hyps tc in + let ml, mr = EcIdent.create "&1", EcIdent.create "&2" in + let env' = LDecl.inv_memenv ml mr hyps in + let inv = TTC.pf_process_form !!tc env' tbool inv in + t_equivF_abs_full { efa_inv = { inv; ml; mr; } } tc diff --git a/src/phl/rules/equiv/ecEquivFunAbs.mli b/src/phl/rules/equiv/ecEquivFunAbs.mli new file mode 100644 index 000000000..17c56578b --- /dev/null +++ b/src/phl/rules/equiv/ecEquivFunAbs.mli @@ -0,0 +1,61 @@ +(* -------------------------------------------------------------------- *) +open EcParsetree +open EcCoreGoal.FApi +open EcPath +open EcAst +open EcEnv + +(* ==================================================================== *) +(* Rules (trusted) *) + +type equiv_fun_abs = { + efa_inv : ts_inv; (* relational invariant I *) +} + +(* [t_equivF_abs { efa_inv = I }] — two instances of the same abstract + procedure, with oracles related by an invariant: + + equiv [o_1 ~ o'_1 : ={arg} /\ G_1 /\ I ==> ={res} /\ G_1 /\ I] + ... + equiv [o_k ~ o'_k : ={arg} /\ G_k /\ I ==> ={res} /\ G_k /\ I] + ---------------------------------------------------------------- + equiv [f ~ f' : ={arg} /\ ={glob A} /\ I ==> ={res} /\ ={glob A} /\ I] + + where [f] is [A(O..).g] and [f'] is [A(O'..).g] (normalized, the same + procedure [g] of the same abstract module [A]), [o_i] / [o'_i] are the + oracles they may call, pairwise, and [G_i] is [={glob A}] when [o_i] or + [o'_i] may access [glob A], nothing otherwise. Side conditions: [f] and + [f'] are procedures of the same abstract module [A], [I] does not depend + on [glob A] (on either side), and the goal is exactly the conclusion + above (otherwise fails). + + Node: [REquivFunAbs { efa_inv = I }]. Checker: "equivF-fun-abs". *) +val t_equivF_abs : equiv_fun_abs -> backward + +(* [equivF_abs_spec env f f' I] is [(pre, post, premises)]: the pre- and + postcondition of the conclusion of [t_equivF_abs], and its premises. + Fails if the procedures are not instances of the same abstract procedure + or [I] depends on their globals. *) +val equivF_abs_spec : + env -> xpath -> xpath -> ts_inv -> ts_inv * ts_inv * form list + +(* ==================================================================== *) +(* Derived tactics *) + +(* [t_equivF_abs_full { efa_inv = I }] — on [equiv [f ~ f' : P ==> Q]]: + 1. the consequence rule (currently [EcPhlConseq.t_equivF_conseq]) to the + conclusion of [t_equivF_abs]; + 2. then [t_equivF_abs] on it. + Visible goals: the two side conditions of the consequence + ([P => ={arg} /\ ={glob A} /\ I], [={res} /\ ={glob A} /\ I => Q]), then + the premises of the rule, one per pair of oracles. Emits no node of its + own. *) +val t_equivF_abs_full : equiv_fun_abs -> backward + +(* ==================================================================== *) +(* Elaboration *) + +(* [proc I] on an [equivF] goal for an abstract procedure: [I] is typed as + a boolean formula in memories [&1] and [&2]. Applies + [t_equivF_abs_full]. *) +val process_equivF_abs : pformula -> backward diff --git a/src/phl/rules/equiv/ecEquivFunAbsUpto.ml b/src/phl/rules/equiv/ecEquivFunAbsUpto.ml new file mode 100644 index 000000000..faec63375 --- /dev/null +++ b/src/phl/rules/equiv/ecEquivFunAbsUpto.ml @@ -0,0 +1,180 @@ +(* -------------------------------------------------------------------- *) +open EcUtils +open EcParsetree +open EcTypes +open EcFol +open EcAst +open EcMemory +open EcModules +open EcEnv +open EcPV +open EcSubst + +open EcCoreGoal +open EcLowPhlGoal + +module TTC = EcProofTyping + +(* -------------------------------------------------------------------- *) +(* Parameters of the equiv abstract-procedure upto rule, already typed. + Nothing to resolve: the same record is the rule argument and the node + payload. *) +type equiv_fun_abs_upto = { + efu_ll : bool; (* lossless variant *) + efu_bad : ss_inv; (* bad event B, read on the right *) + efu_inv : ts_inv; (* invariant P, while B does not hold *) + efu_binv : ts_inv; (* invariant Q, once B holds *) +} + +type EcCoreGoal.rule += REquivFunAbsUpto of equiv_fun_abs_upto + +(* -------------------------------------------------------------------- *) +(* The pre- and postcondition of the conclusion of the rule, and its + premises. *) +let equivF_abs_upto_spec (env : env) fl fr (r : equiv_fun_abs_upto) = + let { efu_ll = weakened_pre; efu_bad = bad; efu_inv = invP; efu_binv = invQ } = r in + + let (topl, _fl, oil, sigl), (topr, _fr, oir, sigr) = + EcLowPhlGoal.abstract_info2 env fl fr + in + + let ml, mr = invP.ml, invP.mr in + let bad = ss_inv_rebind bad invP.mr in + let bad2 = ss_inv_generalize_left bad invP.ml in + let allinv = map_ts_inv f_ands [bad2; invP; invQ] in + let fvl = PV.fv env ml allinv.inv in + let fvr = PV.fv env mr allinv.inv in + + PV.check_depend env fvl topl; + PV.check_depend env fvr topr; + + (* FIXME: check there is only global variable *) + let eqglob = ts_inv_eqglob topl ml topr mr in + + let ospec o_l o_r = + EcPlFun.check_oracle_use env topl o_l; + EcPlFun.check_oracle_use env topr o_r; + + let fo_l = EcEnv.Fun.by_xpath o_l env in + let fo_r = EcEnv.Fun.by_xpath o_r env in + let eq_params = + ts_inv_eqparams + fo_l.f_sig.fs_arg fo_l.f_sig.fs_anames ml + fo_r.f_sig.fs_arg fo_r.f_sig.fs_anames mr in + + let eq_res = + ts_inv_eqres fo_l.f_sig.fs_ret ml fo_r.f_sig.fs_ret mr in + + let pre = map_ts_inv EcFol.f_ands [map_ts_inv1 EcFol.f_not bad2; eq_params; invP] in + let post = map_ts_inv3 EcFol.f_if_simpl bad2 invQ (map_ts_inv2 f_and eq_res invP) in + let cond1 = f_equivF pre o_l o_r post in + if not weakened_pre then + let cond2 = + let f_r1 = {m=invQ.ml; inv=f_r1} in + let concl = ts_inv_lower_left1 (fun bq -> (f_bdHoareF bq o_l bq FHeq f_r1)) invQ in + f_forall_mems_ss_inv (mr, abstract_mt) + (map_ss_inv2 f_imp bad concl) in + let cond3 = + let f_r1 = {m=invQ.mr; inv=f_r1} in + let bq = map_ts_inv2 f_and bad2 invQ in + f_forall_mems_ss_inv (ml, abstract_mt) (ts_inv_lower_right1 (fun bq -> f_bdHoareF bq o_r bq FHeq f_r1) bq) in + + [cond1; cond2; cond3] + else + let cond2 = + let concl = ts_inv_lower_left1 (fun bq -> (f_hoareF bq o_l (POE.lift bq))) invQ in + f_forall_mems_ss_inv (mr, abstract_mt) + (map_ss_inv2 f_imp bad concl) in + let cond3 = + let bq = map_ts_inv2 f_and bad2 invQ in + f_forall_mems_ss_inv (ml, abstract_mt) (ts_inv_lower_right1 (fun bq -> f_hoareF bq o_r (POE.lift bq)) bq) in + + [cond1; cond2; cond3] + in + + let sg = List.map2 ospec (OI.allowed oil) (OI.allowed oir) in + let sg = List.flatten sg in + let lossless_a = if not weakened_pre then + [ EcPlFun.lossless_hyps env topl fl.x_sub ] + else + [ f_losslessF fl; f_losslessF fr ] + in + let sg = lossless_a @ sg 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 = [eqglob;invP] in + let pre = map_ts_inv3 f_if_simpl bad2 invQ (map_ts_inv f_ands (eq_params::pre)) in + let post = map_ts_inv3 f_if_simpl bad2 invQ (map_ts_inv f_ands [eq_res;eqglob;invP]) in + + (pre, post, sg) + +(* -------------------------------------------------------------------- *) +(* Pure core shared by the rule and its checker. Its side conditions (the + procedures are instances of the same abstract procedure, the formulas + do not depend on its globals, the oracles do not access them, the goal + is the conclusion of the rule) are part of it, so the checker + re-validates them. *) +let equivF_abs_upto_subgoals + (hyps : LDecl.hyps) (ef : equivF) (n : equiv_fun_abs_upto) += + let pre, post, sg = + equivF_abs_upto_spec (LDecl.toenv hyps) ef.ef_fl ef.ef_fr n in + if not ( EcReduction.ts_inv_alpha_eq hyps (ef_pr ef) pre + && EcReduction.ts_inv_alpha_eq hyps (ef_po ef) post) then + failwith "equivF-fun-abs-upto: the judgement is not the conclusion of the rule"; + sg + +(* -------------------------------------------------------------------- *) +(* Rule (TCB). *) +let t_equivF_abs_upto (r : equiv_fun_abs_upto) (tc : tcenv1) = + let ef = tc1_as_equivF tc in + FApi.xrule1 tc (REquivFunAbsUpto r) + (equivF_abs_upto_subgoals (FApi.tc1_hyps tc) ef r) + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | REquivFunAbsUpto n -> + Some (EcPlRecheck.checker_of "equivF-fun-abs-upto" pf_as_equivF + (fun hyps ef -> equivF_abs_upto_subgoals hyps ef n)) + | _ -> None) + +(* -------------------------------------------------------------------- *) +(* Derived (no proof-node): the consequence to the conclusion of the rule, + then the rule. + + TEMPORARY: the consequence rule still comes from the not-yet-migrated + [EcPhlConseq]. *) +let t_equivF_abs_upto_full (r : equiv_fun_abs_upto) (tc : tcenv1) = + let env = FApi.tc1_env tc in + let ef = tc1_as_equivF tc in + let pre, post, _ = equivF_abs_upto_spec env ef.ef_fl ef.ef_fr r in + FApi.t_last (t_equivF_abs_upto r) (EcPhlConseq.t_equivF_conseq pre post tc) + +(* -------------------------------------------------------------------- *) +(* Elaboration. *) +let process_equivF_abs_upto_info (info : fun_upto_info) (tc : tcenv1) = + let hyps = FApi.tc1_hyps tc in + let ml, mr = (EcIdent.create "&1", EcIdent.create "&2") in + let env' = LDecl.inv_memenv ml mr hyps in + let p = TTC.pf_process_form !!tc env' tbool info.fui_pre in + let q = info.fui_pos |> omap (TTC.pf_process_form !!tc env' tbool) |> odfl f_true in + let m = EcIdent.create "&hr" in + let bad = + let env' = LDecl.push_active_ss (EcMemory.abstract m) hyps in + TTC.pf_process_form !!tc env' tbool info.fui_bad + in + { efu_ll = odfl false info.fui_is_ll_variant; + efu_bad = { inv = bad; m }; + efu_inv = { inv = p; ml; mr }; + efu_binv = { inv = q; ml; mr }; } + +let process_equivF_abs_upto (info : fun_upto_info) (tc : tcenv1) = + t_equivF_abs_upto_full (process_equivF_abs_upto_info info tc) tc diff --git a/src/phl/rules/equiv/ecEquivFunAbsUpto.mli b/src/phl/rules/equiv/ecEquivFunAbsUpto.mli new file mode 100644 index 000000000..f1efba0ac --- /dev/null +++ b/src/phl/rules/equiv/ecEquivFunAbsUpto.mli @@ -0,0 +1,71 @@ +(* -------------------------------------------------------------------- *) +open EcParsetree +open EcCoreGoal +open EcCoreGoal.FApi +open EcAst + +(* ==================================================================== *) +(* Rules (trusted) *) + +type equiv_fun_abs_upto = { + efu_ll : bool; (* lossless variant ([proc @[ll]]) *) + efu_bad : ss_inv; (* bad event B, read on the right *) + efu_inv : ts_inv; (* invariant P, while B does not hold *) + efu_binv : ts_inv; (* invariant Q, once B holds *) +} + +(* [t_equivF_abs_upto { efu_ll = false; efu_bad = B; efu_inv = P; + efu_binv = Q }] — two instances of the same abstract + procedure, equivalent up to the bad event [B]: + + forall (O1 <: T1 {-A}) ... (On <: Tn {-A}), + islossless o_1 => ... => islossless o_k => islossless A(O1..On).g + for each pair of oracles (o_i, o'_i): + equiv [o_i ~ o'_i : !B{2} /\ ={arg} /\ P + ==> if B{2} then Q else ={res} /\ P] + forall &2, B{2} => phoare [o_i : Q ==> Q] = 1%r + forall &1, phoare [o'_i : B /\ Q ==> B /\ Q] = 1%r + ----------------------------------------------------------------- + equiv [f ~ f' : if B{2} then Q else ={arg} /\ ={glob A} /\ P + ==> if B{2} then Q else ={res} /\ ={glob A} /\ P] + + where [f] is [A(O..).g] and [f'] is [A(O'..).g] (normalized, the same + procedure [g] of the same abstract module [A]), [o_i] / [o'_i] are the + oracles they may call, pairwise ([o_i] in the first premise being the + corresponding procedure of the [Oj]); in the per-oracle phoare premises, + the other memory is the quantified one ([if B{2} then ...] is + simplified when [B] is [true] or [false]). With [efu_ll = true], the + first premise is [islossless f] and [islossless f'], and the two phoare + premises of each oracle are the corresponding hoare judgements + [hoare [o_i : Q ==> Q]] and [hoare [o'_i : B /\ Q ==> B /\ Q]]. + Side conditions: [f] and [f'] are procedures of the same abstract module + [A], [B], [P] and [Q] do not depend on [glob A] (on either side), no + oracle accesses [glob A], and the goal is exactly the conclusion above + (otherwise fails). + + Node: [REquivFunAbsUpto { efu_ll; efu_bad = B; efu_inv = P; + efu_binv = Q }]. Checker: "equivF-fun-abs-upto". *) +val t_equivF_abs_upto : equiv_fun_abs_upto -> backward + +(* ==================================================================== *) +(* Derived tactics *) + +(* [t_equivF_abs_upto_full r] — on [equiv [f ~ f' : P' ==> Q']]: + 1. the consequence rule (currently [EcPhlConseq.t_equivF_conseq]) to the + conclusion of [t_equivF_abs_upto r]; + 2. then [t_equivF_abs_upto r] on it. + Visible goals: the two side conditions of the consequence, then the + premises of the rule. Emits no node of its own. *) +val t_equivF_abs_upto_full : equiv_fun_abs_upto -> backward + +(* ==================================================================== *) +(* Elaboration *) + +(* Types the arguments of [proc @[ll] B P Q] (also used by [call]): [B] in + a memory [&hr], [P] and [Q] in memories [&1] and [&2], [Q] defaulting to + [true]; the lossless variant is selected by [@[ll]]. *) +val process_equivF_abs_upto_info : fun_upto_info -> tcenv1 -> equiv_fun_abs_upto + +(* [proc @[ll] B P Q] on an [equivF] goal for an abstract procedure. + Applies [t_equivF_abs_upto_full]. *) +val process_equivF_abs_upto : fun_upto_info -> backward diff --git a/src/phl/rules/equiv/ecEquivFunDef.ml b/src/phl/rules/equiv/ecEquivFunDef.ml new file mode 100644 index 000000000..a69877060 --- /dev/null +++ b/src/phl/rules/equiv/ecEquivFunDef.ml @@ -0,0 +1,56 @@ +(* -------------------------------------------------------------------- *) +open EcUtils +open EcTypes +open EcFol +open EcAst +open EcEnv +open EcPV + +open EcCoreGoal +open EcLowPhlGoal + +(* -------------------------------------------------------------------- *) +(* The equiv [fun-def] rule has no parameters. *) +type EcCoreGoal.rule += REquivFunDef + +(* -------------------------------------------------------------------- *) +(* Pure core shared by the rule and its checker. Its side condition (both + procedures are concrete) is part of it, so the checker re-validates + it. *) +let equivF_fun_def_subgoals (hyps : LDecl.hyps) (ef : equivF) : form list = + let env = LDecl.toenv hyps in + let ml, mr = ef.ef_ml, ef.ef_mr in + let fl = NormMp.norm_xfun env ef.ef_fl in + let fr = NormMp.norm_xfun env ef.ef_fr in + EcPlFun.ensure_concrete "equivF-fun-def" env fl; + EcPlFun.ensure_concrete "equivF-fun-def" env fr; + let (menvl, eqsl, menvr, eqsr, env) = Fun.equivS ml mr fl fr env in + let (fsigl, fdefl) = eqsl in + let (fsigr, fdefr) = eqsr in + let fresl = odfl {m=ml;inv=f_tt} (omap (ss_inv_of_expr ml) fdefl.f_ret) in + let fresr = odfl {m=mr;inv=f_tt} (omap (ss_inv_of_expr mr) fdefr.f_ret) in + let s = PVM.add env pv_res ml fresl.inv PVM.empty in + let s = PVM.add env pv_res mr fresr.inv s in + let post = map_ts_inv1 (PVM.subst env s) (ef_po ef) in + let s = EcPlFun.subst_pre env fsigl ml PVM.empty in + let s = EcPlFun.subst_pre env fsigr mr s in + let pre = map_ts_inv1 (PVM.subst env s) (ef_pr ef) in + [f_equivS (snd menvl) (snd menvr) pre fdefl.f_body fdefr.f_body post] + +(* -------------------------------------------------------------------- *) +(* Rule (TCB). *) +let t_equivF_fun_def (tc : tcenv1) = + let env = FApi.tc1_env tc in + let ef = tc1_as_equivF tc in + EcPlFun.check_concrete !!tc env (NormMp.norm_xfun env ef.ef_fl); + EcPlFun.check_concrete !!tc env (NormMp.norm_xfun env ef.ef_fr); + FApi.xrule1 tc REquivFunDef (equivF_fun_def_subgoals (FApi.tc1_hyps tc) ef) + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | REquivFunDef -> + Some (EcPlRecheck.checker_of "equivF-fun-def" pf_as_equivF + equivF_fun_def_subgoals) + | _ -> None) diff --git a/src/phl/rules/equiv/ecEquivFunDef.mli b/src/phl/rules/equiv/ecEquivFunDef.mli new file mode 100644 index 000000000..7b6409530 --- /dev/null +++ b/src/phl/rules/equiv/ecEquivFunDef.mli @@ -0,0 +1,20 @@ +(* -------------------------------------------------------------------- *) +open EcCoreGoal.FApi + +(* ==================================================================== *) +(* Rules (trusted) *) + +(* [t_equivF_fun_def] — two concrete procedures, by their bodies: + + equiv [body1 ~ body2 : P[arg<1> := xs1, arg<2> := xs2] + ==> Q[res<1> := e1, res<2> := e2]] + ------------------------------------------------------ f1, f2 concrete + equiv [f1 ~ f2 : P ==> Q] + + where [fi] (normalized) is [proc fi(xs_i) = { body_i; return e_i }] + ([e_i] is [tt] when [fi] returns nothing), in the memory of [fi] + extended with its parameters and locals. Side condition: neither + procedure is abstract (otherwise fails). + + Node: [REquivFunDef]. Checker: "equivF-fun-def". *) +val t_equivF_fun_def : backward diff --git a/src/phl/rules/equiv/ecEquivFunToCode.ml b/src/phl/rules/equiv/ecEquivFunToCode.ml new file mode 100644 index 000000000..c0fba9f49 --- /dev/null +++ b/src/phl/rules/equiv/ecEquivFunToCode.ml @@ -0,0 +1,54 @@ +(* -------------------------------------------------------------------- *) +open EcTypes +open EcFol +open EcAst +open EcEnv +open EcPV + +open EcCoreGoal +open EcLowPhlGoal + +(* -------------------------------------------------------------------- *) +(* The equiv [fun-to-code] rule has no parameters. *) +type EcCoreGoal.rule += REquivFunToCode + +(* -------------------------------------------------------------------- *) +(* Pure core shared by the rule and its checker. The fresh variables are + chosen deterministically from the memories of the goal. *) +let equivF_fun_to_code_subgoals (hyps : LDecl.hyps) (ef : equivF) : form list = + let env = LDecl.toenv hyps in + let ml, mr = ef.ef_ml, ef.ef_mr in + let (fl,fr) = ef.ef_fl, ef.ef_fr in + let (ml0, mlt), sl, rl, al = EcPlFun.to_code env fl ml in + assert (EcIdent.id_equal ml0 ml); + let (mr0, mrt), sr, rr, ar = EcPlFun.to_code env fr mr in + assert (EcIdent.id_equal mr0 mr); + let spr = + let s = PVM.empty in + let s = EcPlFun.add_var_tuple env pv_arg ml al ml s in + let s = EcPlFun.add_var_tuple env pv_arg mr ar mr s in + s in + let spo = + let s = PVM.empty in + let s = EcPlFun.add_var env pv_res ml rl ml s in + let s = EcPlFun.add_var env pv_res mr rr mr s in + s in + let pre = PVM.subst env spr (ef_pr ef).inv in + let post = PVM.subst env spo (ef_po ef).inv in + [f_equivS mlt mrt {ml;mr;inv=pre} sl sr {ml;mr;inv=post}] + +(* -------------------------------------------------------------------- *) +(* Rule (TCB). *) +let t_equivF_fun_to_code (tc : tcenv1) = + let ef = tc1_as_equivF tc in + FApi.xrule1 tc REquivFunToCode + (equivF_fun_to_code_subgoals (FApi.tc1_hyps tc) ef) + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | REquivFunToCode -> + Some (EcPlRecheck.checker_of "equivF-fun-to-code" pf_as_equivF + equivF_fun_to_code_subgoals) + | _ -> None) diff --git a/src/phl/rules/equiv/ecEquivFunToCode.mli b/src/phl/rules/equiv/ecEquivFunToCode.mli new file mode 100644 index 000000000..d452aad87 --- /dev/null +++ b/src/phl/rules/equiv/ecEquivFunToCode.mli @@ -0,0 +1,19 @@ +(* -------------------------------------------------------------------- *) +open EcCoreGoal.FApi + +(* ==================================================================== *) +(* Rules (trusted) *) + +(* [t_equivF_fun_to_code] — two procedures, as single calls ([proc*]): + + equiv [r1 <@ f1(as1) ~ r2 <@ f2(as2) : + P[arg<1> := as1, arg<2> := as2] ==> Q[res<1> := r1, res<2> := r2]] + --------------------------------------------------------------------------- + equiv [f1 ~ f2 : P ==> Q] + + where [asi] is [(a1, ..., an)], [a1 ... an] and [ri] being fresh local + variables of the memory of side [i] (the parameters of [fi], unnamed + ones named [arg], and its result). + + Node: [REquivFunToCode]. Checker: "equivF-fun-to-code". *) +val t_equivF_fun_to_code : backward diff --git a/src/phl/rules/hoare/ecHoareFunAbs.ml b/src/phl/rules/hoare/ecHoareFunAbs.ml new file mode 100644 index 000000000..caa19e5c8 --- /dev/null +++ b/src/phl/rules/hoare/ecHoareFunAbs.ml @@ -0,0 +1,80 @@ +(* -------------------------------------------------------------------- *) +open EcParsetree +open EcTypes +open EcFol +open EcAst +open EcModules +open EcEnv +open EcPV + +open EcCoreGoal +open EcLowPhlGoal + +module TTC = EcProofTyping + +(* -------------------------------------------------------------------- *) +(* Parameter of the hoare abstract-procedure rule: the invariant, already + typed. Nothing to resolve: the same record is the rule argument and the + node payload. *) +type hoare_fun_abs = { + hfa_inv : ss_inv; (* invariant I *) +} + +type EcCoreGoal.rule += RHoareFunAbs of hoare_fun_abs + +(* -------------------------------------------------------------------- *) +let hoareF_abs_spec (env : env) (f : EcPath.xpath) (inv : ss_inv) = + let (top, _, oi, _) = EcLowPhlGoal.abstract_info env f in + let fv = PV.fv env inv.m inv.inv in + PV.check_depend env fv top; + let ospec o = f_hoareF inv o (POE.lift inv) in + let sg = List.map ospec (OI.allowed oi) in + (inv, inv, sg) + +(* -------------------------------------------------------------------- *) +(* Pure core shared by the rule and its checker. Its side conditions (the + procedure is abstract, the invariant does not depend on its globals, the + goal is [hoare [f : I ==> I]]) are part of it, so the checker + re-validates them. *) +let hoareF_abs_subgoals (hyps : LDecl.hyps) (hf : sHoareF) (n : hoare_fun_abs) = + let pre, post, sg = hoareF_abs_spec (LDecl.toenv hyps) hf.hf_f n.hfa_inv in + if not ( EcReduction.ss_inv_alpha_eq hyps (hf_pr hf) pre + && EcReduction.hs_inv_alpha_eq hyps (hf_po hf) (POE.lift post)) then + failwith "hoareF-fun-abs: the judgement is not [I ==> I]"; + sg + +(* -------------------------------------------------------------------- *) +(* Rule (TCB). *) +let t_hoareF_abs (r : hoare_fun_abs) (tc : tcenv1) = + let hf = tc1_as_hoareF tc in + FApi.xrule1 tc (RHoareFunAbs r) (hoareF_abs_subgoals (FApi.tc1_hyps tc) hf r) + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | RHoareFunAbs n -> + Some (EcPlRecheck.checker_of "hoareF-fun-abs" pf_as_hoareF + (fun hyps hf -> hoareF_abs_subgoals hyps hf n)) + | _ -> None) + +(* -------------------------------------------------------------------- *) +(* Derived (no proof-node): the consequence to [I ==> I], then the rule. + + TEMPORARY: the consequence rule still comes from the not-yet-migrated + [EcPhlConseq]. *) +let t_hoareF_abs_full (r : hoare_fun_abs) (tc : tcenv1) = + let env = FApi.tc1_env tc in + let hf = tc1_as_hoareF tc in + let pre, post, _ = hoareF_abs_spec env hf.hf_f r.hfa_inv in + FApi.t_last (t_hoareF_abs r) + (EcPhlConseq.t_hoareF_conseq pre (POE.lift post) tc) + +(* -------------------------------------------------------------------- *) +(* Elaboration: the goal is known to be a [hoareF]. *) +let process_hoareF_abs (inv : pformula) (tc : tcenv1) = + let hyps = FApi.tc1_hyps tc in + let m = EcIdent.create "&hr" in + let env' = LDecl.inv_memenv1 m hyps in + let inv = TTC.pf_process_form !!tc env' tbool inv in + t_hoareF_abs_full { hfa_inv = { inv; m; } } tc diff --git a/src/phl/rules/hoare/ecHoareFunAbs.mli b/src/phl/rules/hoare/ecHoareFunAbs.mli new file mode 100644 index 000000000..892e2d7d9 --- /dev/null +++ b/src/phl/rules/hoare/ecHoareFunAbs.mli @@ -0,0 +1,54 @@ +(* -------------------------------------------------------------------- *) +open EcParsetree +open EcCoreGoal.FApi +open EcPath +open EcAst +open EcEnv + +(* ==================================================================== *) +(* Rules (trusted) *) + +type hoare_fun_abs = { + hfa_inv : ss_inv; (* invariant I *) +} + +(* [t_hoareF_abs { hfa_inv = I }] — an abstract procedure preserves an + invariant its oracles preserve: + + hoare [o_1 : I ==> I] ... hoare [o_k : I ==> I] + -------------------------------------------------- f = A(...).g abstract + hoare [f : I ==> I] I independent of glob A + + where [o_1 ... o_k] are the oracles [f] may call. The judgements carry + no exceptional postcondition: an exception listed by no branch is + unconstrained (#1188), so the conclusion holds for instances of [A] and + oracles that raise. Side conditions: [f] (normalized) is a procedure of + an abstract module [A], [I] does not depend on [glob A], and the goal is + exactly [hoare [f : I ==> I]] (otherwise fails). + + Node: [RHoareFunAbs { hfa_inv = I }]. Checker: "hoareF-fun-abs". *) +val t_hoareF_abs : hoare_fun_abs -> backward + +(* [hoareF_abs_spec env f I] is [(I, I, premises)]: the pre- and + postcondition of the conclusion of [t_hoareF_abs], and its premises. + Fails if [f] is not abstract or [I] depends on its globals. *) +val hoareF_abs_spec : env -> xpath -> ss_inv -> ss_inv * ss_inv * form list + +(* ==================================================================== *) +(* Derived tactics *) + +(* [t_hoareF_abs_full { hfa_inv = I }] — on [hoare [f : P ==> Q | E]]: + 1. the consequence rule (currently [EcPhlConseq.t_hoareF_conseq]) to + [hoare [f : I ==> I]]; + 2. then [t_hoareF_abs] on it. + Visible goals: the two side conditions of the consequence ([P => I], + and [I => Q] together with the exceptional postconditions [E]), then + [hoare [o_i : I ==> I]] for each oracle. Emits no node of its own. *) +val t_hoareF_abs_full : hoare_fun_abs -> backward + +(* ==================================================================== *) +(* Elaboration *) + +(* [proc I] on a [hoareF] goal for an abstract procedure: [I] is typed as a + boolean formula in a memory [&hr]. Applies [t_hoareF_abs_full]. *) +val process_hoareF_abs : pformula -> backward diff --git a/src/phl/rules/hoare/ecHoareFunDef.ml b/src/phl/rules/hoare/ecHoareFunDef.ml new file mode 100644 index 000000000..dba0ed935 --- /dev/null +++ b/src/phl/rules/hoare/ecHoareFunDef.ml @@ -0,0 +1,48 @@ +(* -------------------------------------------------------------------- *) +open EcUtils +open EcTypes +open EcFol +open EcAst +open EcEnv +open EcPV + +open EcCoreGoal +open EcLowPhlGoal + +(* -------------------------------------------------------------------- *) +(* The hoare [fun-def] rule has no parameters. *) +type EcCoreGoal.rule += RHoareFunDef + +(* -------------------------------------------------------------------- *) +(* Pure core shared by the rule and its checker. Its side condition (the + procedure is concrete) is part of it, so the checker re-validates it. *) +let hoareF_fun_def_subgoals (hyps : LDecl.hyps) (hf : sHoareF) : form list = + let env = LDecl.toenv hyps in + let f = NormMp.norm_xfun env hf.hf_f in + EcPlFun.ensure_concrete "hoareF-fun-def" env f; + let (memenv, (fsig, fdef), env) = Fun.hoareS hf.hf_m f env in + let m = EcMemory.memory memenv in + let fres = odfl {m;inv=f_tt} (omap (ss_inv_of_expr m) fdef.f_ret) in + let post, epost = POE.destruct (hf_po hf).hsi_inv in + let post = {m=(hf_po hf).hsi_m;inv=post} in + let post = map_ss_inv2 (PVM.subst1 env pv_res m) fres post in + let pre = map_ss_inv1 (PVM.subst env (EcPlFun.subst_pre env fsig m PVM.empty)) (hf_pr hf) in + let post = { hsi_m = post.m; hsi_inv = POE.mk post.inv epost; } in + [f_hoareS (snd memenv) pre fdef.f_body post] + +(* -------------------------------------------------------------------- *) +(* Rule (TCB). *) +let t_hoareF_fun_def (tc : tcenv1) = + let env = FApi.tc1_env tc in + let hf = tc1_as_hoareF tc in + EcPlFun.check_concrete !!tc env (NormMp.norm_xfun env hf.hf_f); + FApi.xrule1 tc RHoareFunDef (hoareF_fun_def_subgoals (FApi.tc1_hyps tc) hf) + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | RHoareFunDef -> + Some (EcPlRecheck.checker_of "hoareF-fun-def" pf_as_hoareF + hoareF_fun_def_subgoals) + | _ -> None) diff --git a/src/phl/rules/hoare/ecHoareFunDef.mli b/src/phl/rules/hoare/ecHoareFunDef.mli new file mode 100644 index 000000000..98441c5a7 --- /dev/null +++ b/src/phl/rules/hoare/ecHoareFunDef.mli @@ -0,0 +1,20 @@ +(* -------------------------------------------------------------------- *) +open EcCoreGoal.FApi + +(* ==================================================================== *) +(* Rules (trusted) *) + +(* [t_hoareF_fun_def] — a concrete procedure, by its body: + + hoare [body : P[arg := (x1, ..., xn)] ==> Q[res := e] | E] + ---------------------------------------------------------- f concrete + hoare [f : P ==> Q | E] + + where [f] (normalized) is [proc f(x1, ..., xn) = { body; return e }] + ([e] is [tt] when [f] returns nothing), in the memory of [f] extended + with its parameters and locals, and [E] are the exceptional + postconditions of the goal, kept unchanged. Side condition: [f] is not + abstract (otherwise fails). + + Node: [RHoareFunDef]. Checker: "hoareF-fun-def". *) +val t_hoareF_fun_def : backward diff --git a/src/phl/rules/hoare/ecHoareFunToCode.ml b/src/phl/rules/hoare/ecHoareFunToCode.ml new file mode 100644 index 000000000..05d2d6ef0 --- /dev/null +++ b/src/phl/rules/hoare/ecHoareFunToCode.ml @@ -0,0 +1,44 @@ +(* -------------------------------------------------------------------- *) +open EcTypes +open EcFol +open EcAst +open EcEnv +open EcPV + +open EcCoreGoal +open EcLowPhlGoal + +(* -------------------------------------------------------------------- *) +(* The hoare [fun-to-code] rule has no parameters. *) +type EcCoreGoal.rule += RHoareFunToCode + +(* -------------------------------------------------------------------- *) +(* Pure core shared by the rule and its checker. The fresh variables are + chosen deterministically from the memory of the goal. *) +let hoareF_fun_to_code_subgoals (hyps : LDecl.hyps) (hf : sHoareF) : form list = + let env = LDecl.toenv hyps in + let f = hf.hf_f in + let m = hf.hf_m in + let (m0, mt), st, r, a = EcPlFun.to_code env f m in + assert (EcIdent.id_equal m0 m); + let spr = EcPlFun.add_var_tuple env pv_arg m a m PVM.empty in + let spo = EcPlFun.add_var env pv_res m r m PVM.empty in + let pre = PVM.subst env spr (hf_pr hf).inv in + let post = POE.map (PVM.subst env spo) (hf_po hf).hsi_inv in + [f_hoareS mt {m;inv=pre} st {hsi_m=m;hsi_inv=post}] + +(* -------------------------------------------------------------------- *) +(* Rule (TCB). *) +let t_hoareF_fun_to_code (tc : tcenv1) = + let hf = tc1_as_hoareF tc in + FApi.xrule1 tc RHoareFunToCode + (hoareF_fun_to_code_subgoals (FApi.tc1_hyps tc) hf) + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | RHoareFunToCode -> + Some (EcPlRecheck.checker_of "hoareF-fun-to-code" pf_as_hoareF + hoareF_fun_to_code_subgoals) + | _ -> None) diff --git a/src/phl/rules/hoare/ecHoareFunToCode.mli b/src/phl/rules/hoare/ecHoareFunToCode.mli new file mode 100644 index 000000000..b49074a81 --- /dev/null +++ b/src/phl/rules/hoare/ecHoareFunToCode.mli @@ -0,0 +1,18 @@ +(* -------------------------------------------------------------------- *) +open EcCoreGoal.FApi + +(* ==================================================================== *) +(* Rules (trusted) *) + +(* [t_hoareF_fun_to_code] — a procedure, as a single call ([proc*]): + + hoare [r <@ f(a1, ..., an) : P[arg := (a1, ..., an)] ==> Q[res := r] | E] + ------------------------------------------------------------------------- + hoare [f : P ==> Q | E] + + where [a1 ... an] and [r] are fresh local variables of the memory (the + parameters of [f], unnamed ones named [arg], and its result), and + [E] are the exceptional postconditions of the goal, kept unchanged. + + Node: [RHoareFunToCode]. Checker: "hoareF-fun-to-code". *) +val t_hoareF_fun_to_code : backward diff --git a/tests/proc.ec b/tests/proc.ec new file mode 100644 index 000000000..04af5cef7 --- /dev/null +++ b/tests/proc.ec @@ -0,0 +1,236 @@ +(* The [proc] rules in every logic: a concrete procedure by its body, an + abstract procedure with an invariant (and up to a bad event), and + [proc*]. *) +require import AllCore Xreal. + +module type O = { + proc o(x : int) : int +}. + +module type Adv (O : O) = { + proc run(x : int) : int +}. + +module C = { + var c : int + + proc f(x : int, y : int) : int = { + var z; + z <- x + y; + return z; + } + + proc g() : unit = { + c <- c + 1; + } +}. + +module O1 : O = { + var bad : bool + var s : int + + proc o(x : int) : int = { + if (x = 10) { + bad <- true; + } + s <- s + x; + return x; + } +}. + +module O2 : O = { + import var O1 + + proc o(x : int) : int = { + if (x = 10) { + bad <- true; + x <- 0; + } + s <- s + x; + return x; + } +}. + +(* -------------------------------------------------------------------- *) +(* Concrete procedures, by their bodies. *) + +lemma hoare_def : hoare [C.f : x = 1 /\ y = 2 ==> res = 3]. +proof. proc; wp; skip => /> /#. qed. + +lemma ehoare_def : ehoare [C.f : (x + y = 3)%xr ==> (res = 3)%xr]. +proof. proc; wp; skip => /> &hr /#. qed. + +lemma phoare_def_eq : phoare [C.f : x = 1 /\ y = 2 ==> res = 3] = 1%r. +proof. proc; wp; skip => /> /#. qed. + +(* The bound is read in the initial memory: it may mention the arguments. *) +lemma phoare_def_ge : + phoare [C.f : x = 1 /\ y = 2 ==> res = 3] >= (if y = 2 then 1%r else 1%r/2%r). +proof. proc; wp; skip => //; smt(). qed. + +lemma equiv_def : equiv [C.f ~ C.f : ={x, y} ==> ={res}]. +proof. proc; wp; skip => />. qed. + +lemma equiv_def_unit : equiv [C.g ~ C.g : ={C.c} ==> ={C.c}]. +proof. proc; wp; skip => />. qed. + +(* Through the [call] tactic (with an invariant, concrete callee). *) +module D = { + proc h() : unit = { C.g(); } +}. + +lemma equiv_call_def : equiv [D.h ~ D.h : ={C.c} ==> ={C.c}]. +proof. by proc; call (: ={C.c}); auto. qed. + +section. +declare module A <: Adv {-O1}. + +(* -------------------------------------------------------------------- *) +(* Abstract procedures, with an invariant. *) + +lemma hoare_abs : hoare [A(O1).run : O1.bad ==> O1.bad]. +proof. +proc (O1.bad); expect 3; 1,2: by trivial. +by proc; auto. +qed. + +lemma hoare_abs_true : hoare [A(O1).run : true ==> true]. +proof. by proc (true); expect 3; trivial. qed. + +lemma ehoare_abs : ehoare [A(O1).run : (1%xr) ==> (1%xr)]. +proof. +proc (1%xr); expect 3; 1,2: by trivial. +by proc; auto. +qed. + +lemma phoare_abs_ge : + (forall (O <: O{-A}), islossless O.o => islossless A(O).run) => + phoare [A(O1).run : true ==> true] >= 1%r. +proof. +move=> A_ll; proc (true); expect 4; 1..3: by trivial. +by proc; auto. +qed. + +lemma phoare_abs_eq : + (forall (O <: O{-A}), islossless O.o => islossless A(O).run) => + phoare [A(O1).run : true ==> true] = 1%r. +proof. +move=> A_ll; proc (true); expect 4; 1..3: by trivial. +by proc; auto. +qed. + +lemma equiv_abs : equiv [A(O1).run ~ A(O1).run : + ={x, glob A, O1.s, O1.bad} ==> ={res, glob A, O1.s, O1.bad}]. +proof. +proc (={O1.s, O1.bad}) => //. +by proc; auto. +qed. + +(* Through the [call] tactic (with an invariant, abstract callee). *) +module B (A : Adv) = { + proc main() : int = { + var r; + r <@ A(O1).run(0); + return r; + } +}. + +lemma equiv_call_abs : equiv [B(A).main ~ B(A).main : + ={glob A, O1.s, O1.bad} ==> ={res, O1.s}]. +proof. +proc; call (: ={O1.s, O1.bad}); last by auto. +by proc; auto. +qed. + +(* -------------------------------------------------------------------- *) +(* Abstract procedures, up to a bad event. *) + +lemma equiv_upto : + (forall (O <: O{-A}), islossless O.o => islossless A(O).run) => + equiv [A(O1).run ~ A(O2).run : + ={x, glob A, O1.s, O1.bad} /\ !O1.bad{2} + ==> !O1.bad{2} => ={res, glob A, O1.s}]. +proof. +move=> A_ll. +proc O1.bad (={O1.s}) (true) => //; expect 3. +- by proc; auto => /#. +- by move=> &2 _; proc; auto. +- by move=> &1; proc; auto. +qed. + +lemma equiv_upto_ll : + islossless A(O1).run => islossless A(O2).run => + equiv [A(O1).run ~ A(O2).run : + ={x, glob A, O1.s, O1.bad} /\ !O1.bad{2} + ==> !O1.bad{2} => ={res, glob A, O1.s}]. +proof. +move=> ll1 ll2. +proc @[ll] O1.bad (={O1.s}) (true); expect 7. +- by move=> />. +- by move=> />. +- by apply ll1. +- by apply ll2. +- by proc; auto => /#. +- by move=> &2 _; proc; auto. +- by move=> &1; proc; auto. +qed. + +(* -------------------------------------------------------------------- *) +(* Errors. *) + +lemma abs_no_inv : hoare [A(O1).run : true ==> true]. +proof. fail proc. abort. + +lemma abs_dep_glob : hoare [A(O1).run : true ==> true]. +proof. fail proc (glob A = glob A). abort. + +lemma phoare_abs_le : phoare [A(O1).run : true ==> true] <= 1%r. +proof. fail proc (true). abort. + +lemma phoare_abs_half : phoare [A(O1).run : true ==> true] >= (1%r/2%r). +proof. fail proc (true). abort. + +end section. + +lemma def_with_inv : hoare [C.f : true ==> true]. +proof. fail proc (true). abort. + +lemma def_upto : equiv [C.f ~ C.f : true ==> true]. +proof. fail proc O1.bad (true) (true). abort. + +(* -------------------------------------------------------------------- *) +(* [proc*]: procedures as single calls. *) + +lemma hoare_code : hoare [C.f : x = 1 /\ y = 2 ==> res = 3]. +proof. +proc*; inline *; wp; skip => /> /#. +qed. + +lemma ehoare_code : ehoare [C.f : (x + y = 3)%xr ==> (res = 3)%xr]. +proof. +proc*; inline *; wp; skip => /> &hr /#. +qed. + +lemma phoare_code : phoare [C.f : x = 1 /\ y = 2 ==> res = 3] = 1%r. +proof. +proc*; inline *; wp; skip => /> /#. +qed. + +lemma equiv_code : equiv [C.f ~ C.f : ={x, y} ==> ={res}]. +proof. +proc*; inline *; wp; skip => />. +qed. + +lemma eager_code : + eager [C.g();, C.f ~ C.f, C.g(); : ={arg, C.c} ==> ={res, C.c}]. +proof. +proc*; inline *; wp; skip => />. +qed. + +lemma code_unit : equiv [C.g ~ C.g : ={C.c} ==> ={C.c}]. +proof. +proc*; inline *; wp; skip => />. +qed. + +lemma code_error : forall (x : int), x = x. +proof. fail proc*. abort.