From 629ea0c03c490d1b99e79d27a094b514ee2a2331 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Fri, 9 Oct 2026 00:02:42 +0200 Subject: [PATCH] refactor(pl): deno as recheckable per-logic rules PR of the program-logic reorganization stack (see src/phl/REFACTORING.md). It migrates the `deno` tactic class: `byphoare`, `byehoare` and `byequiv` (including its upto-bad forms `Pr[..] <= Pr[..] + Pr[..]` and `byequiv : B`): - rules/bdhoare/ecBdHoareDeno.ml: `Pr[f(args) @ &n : E] ~ d` (`<=`, `=`, `>=`) from `phoare [f : P ==> Q] ~ d`, `P` on the arguments and memory of the goal and `forall &m, E [=>] Q`. The `d = Pr[..]` form is derived (symmetry, then the rule). - rules/ehoare/ecEHoareDeno.ml: `Pr[f(args) @ &n : E] <= d` from `ehoare [f : P ==> Q]`, `P <= d%xr`, `forall &m, E%xr <= Q` and `0%r <= d` (side conditions unchanged). - rules/equiv/ecEquivDeno.ml: `Pr[f1 ..] = Pr[f2 ..]` (resp. `<=`) from `equiv [f1 ~ f2 : P ==> Q]`, `P` on the arguments and memories of the goal and `forall &1 &2, Q => (E1 <=> E2)` (resp. `=>`). The upto-bad forms stay derived from it and the lemmas of `Real`. - Each rule is documented as an inference rule in its .mli and emits a node recording `P` and `Q`, with a registered checker; the shape of the goal is re-validated by the shared subgoal builder, as is a new side condition: the memories of `P` and `Q` do not occur free in the goal (they are bound around the bound `d` or the events in the premises; the surface tactics always use fresh memories). - EcPhlDeno is reduced to the dispatcher and the legacy adapters; its interface is unchanged. Behaviour is preserved: on the new test, the goals after every `byphoare` / `byehoare` / `byequiv` invocation and the error messages of every failing one are identical to those of the unmodified build. A new test, tests/deno.ec, exercises every rule and derived form (cut, proof term, every comparison and orientation, `eq` flag, upto-bad forms directly and through the consequence rule) and the error paths. The stdlib, the unit tests and the examples pass under EC_RECHECK=1 with no RecheckFailure. Each of the 3 checkers, when deliberately broken, is caught only under EC_RECHECK (on the new test; on the stdlib where the rule is used there: bdhoare-deno 19 files, equiv-deno 31; byehoare is not used by the stdlib). --- src/phl/README.md | 3 + src/phl/REFACTORING.md | 3 + src/phl/ecPhlDeno.ml | 628 +----------------------- src/phl/rules/bdhoare/ecBdHoareDeno.ml | 167 +++++++ src/phl/rules/bdhoare/ecBdHoareDeno.mli | 53 ++ src/phl/rules/ehoare/ecEHoareDeno.ml | 140 ++++++ src/phl/rules/ehoare/ecEHoareDeno.mli | 43 ++ src/phl/rules/equiv/ecEquivDeno.ml | 495 +++++++++++++++++++ src/phl/rules/equiv/ecEquivDeno.mli | 101 ++++ tests/deno.ec | 232 +++++++++ 10 files changed, 1248 insertions(+), 617 deletions(-) create mode 100644 src/phl/rules/bdhoare/ecBdHoareDeno.ml create mode 100644 src/phl/rules/bdhoare/ecBdHoareDeno.mli create mode 100644 src/phl/rules/ehoare/ecEHoareDeno.ml create mode 100644 src/phl/rules/ehoare/ecEHoareDeno.mli create mode 100644 src/phl/rules/equiv/ecEquivDeno.ml create mode 100644 src/phl/rules/equiv/ecEquivDeno.mli create mode 100644 tests/deno.ec diff --git a/src/phl/README.md b/src/phl/README.md index 19ca60c9e..134374ca2 100644 --- a/src/phl/README.md +++ b/src/phl/README.md @@ -157,5 +157,8 @@ src/phl/ 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. +- A rule concluding a probability statement from a judgement (`byphoare`, + `byehoare`, `byequiv`: `EcDeno`) lives with the logic of that + judgement. - Program transformations use the transformation rule of each logic; only their catalogue entries live in `rules/transforms/`. diff --git a/src/phl/REFACTORING.md b/src/phl/REFACTORING.md index fc9c33247..313cff7ba 100644 --- a/src/phl/REFACTORING.md +++ b/src/phl/REFACTORING.md @@ -177,6 +177,9 @@ uniform across logics or relate several judgements: in `rules/eager/`); - a rule relating judgements of two logics (the `pr` bridges, `hoare` from `phoare`, …) lives with the logic of its conclusion; +- a rule concluding a statement on probabilities from a judgement + (`byphoare`, `byehoare`, `byequiv`) lives with the logic of that + judgement (`EcBdHoareDeno`, `EcEHoareDeno`, `EcEquivDeno`); - program transformations go through the transformation rule of each logic (`EcTransform`); only their catalogue entries live in `rules/transforms/`. diff --git a/src/phl/ecPhlDeno.ml b/src/phl/ecPhlDeno.ml index 368f9e011..92ee41c59 100644 --- a/src/phl/ecPhlDeno.ml +++ b/src/phl/ecPhlDeno.ml @@ -1,627 +1,21 @@ (* -------------------------------------------------------------------- *) -open EcUtils open EcParsetree -open EcAst -open EcTypes -open EcFol -open EcEnv -open EcPV -open EcPhlPrRw -open EcHiGoal -open EcSubst - -open EcCoreGoal -open EcLowGoal -open EcLowPhlGoal -open EcCoreGoal.FApi - -module PT = EcProofTerm -module TTC = EcProofTyping - -(* -------------------------------------------------------------------- *) -let real_le_trans = EcCoreLib.CI_Real.real_order_lemma "ler_trans" -let real_ler_add = EcCoreLib.CI_Real.real_order_lemma "ler_add" -let real_eq_le = EcCoreLib.CI_Real.real_order_lemma "lerr_eq" -let real_upto = EcCoreLib.CI_Real.real_lemma "upto2_abs" -let real_upto_notbad = EcCoreLib.CI_Real.real_lemma "upto2_notbad" -let real_upto_imp_bad = EcCoreLib.CI_Real.real_lemma "upto2_imp_bad" -let real_upto_false = EcCoreLib.CI_Real.real_lemma "upto_bad_false" -let real_upto_or = EcCoreLib.CI_Real.real_lemma "upto_bad_or" -let real_upto_sub = EcCoreLib.CI_Real.real_lemma "upto_bad_sub" - -(* -------------------------------------------------------------------- *) -let t_real_le_trans f2 tc = - t_apply_prept (`App (`UG real_le_trans, [`F f2]))tc - -(* -------------------------------------------------------------------- *) -let t_core_phoare_deno pre post tc = - let m = pre.m in - let env, _, concl = FApi.tc1_eflat tc in - - let cmp, f, bd, concl_post = - match concl.f_node with - | Fapp ({f_node = Fop (op, _)}, [f; bd]) - when is_pr f && EcPath.p_equal op EcCoreLib.CI_Real.p_real_le -> - (FHle, f, bd, fun ev po -> map_ss_inv2 f_imp_simpl ev po) - - | Fapp ({f_node = Fop (op, _)}, [bd; f]) - when is_pr f && EcPath.p_equal op EcCoreLib.CI_Real.p_real_le -> - (FHge, f, bd, fun ev po -> map_ss_inv2 f_imp_simpl po ev) - - | Fapp ({f_node = Fop (op, _)}, [f; bd]) - when is_pr f && EcPath.p_equal op EcCoreLib.CI_Bool.p_eq -> - (FHeq, f, bd, map_ss_inv2 f_iff_simpl) - - | _ -> tc_error !!tc "invalid goal shape" - in - - let pr = destr_pr f in - let concl_e = f_bdHoareF pre pr.pr_fun post cmp {m;inv=bd} in - let fun_ = EcEnv.Fun.by_xpath pr.pr_fun env in - - (* building the substitution for the pre *) - let sargs = PVM.add env pv_arg m pr.pr_args PVM.empty in - let smem = Fsubst.f_bind_mem Fsubst.f_subst_id m pr.pr_mem in - let concl_pr = Fsubst.f_subst smem ((PVM.subst env sargs) pre.inv) in - - (* building the substitution for the post *) - let ev = pr.pr_event in - let me = EcEnv.Fun.actmem_post ev.m fun_ in - let post = ss_inv_rebind post ev.m in - let concl_po = EcSubst.f_forall_mems_ss_inv me (concl_post ev post) in - - FApi.xmutate1 tc `HlDeno [concl_e; concl_pr; concl_po] - -(* -------------------------------------------------------------------- *) -let t_phoare_deno_r pre post tc = - let concl = FApi.tc1_goal tc in - - match concl.f_node with - | Fapp ({f_node = Fop (op, _)}, [f; _bd]) - when EcPath.p_equal op EcCoreLib.CI_Bool.p_eq && not (is_pr f) -> - (t_symmetry @! t_core_phoare_deno pre post) tc - - | _ -> t_core_phoare_deno pre post tc - - -(* -------------------------------------------------------------------- *) -let t_ehoare_deno_r pre post tc = - let m = pre.m in - assert (m = post.m); - let env, _, concl = FApi.tc1_eflat tc in - - let f, bd = - match concl.f_node with - | Fapp ({f_node = Fop (op, _)}, [f; bd]) - when is_pr f && EcPath.p_equal op EcCoreLib.CI_Real.p_real_le -> - (f, bd) - - | _ -> tc_error !!tc "invalid goal shape" - in - - let pr = destr_pr f in - let concl_e = f_eHoareF pre pr.pr_fun post in - let _, mpo = EcEnv.Fun.hoareF_memenv m pr.pr_fun env in - (* pre <= bd *) - (* building the substitution for the pre *) - let sargs = PVM.add env pv_arg m pr.pr_args PVM.empty in - let smem = Fsubst.f_bind_mem Fsubst.f_subst_id m pr.pr_mem in - let pre = Fsubst.f_subst smem (PVM.subst env sargs pre.inv) in - let concl_pr = f_xreal_le pre (f_r2xr bd) in - - (* forall m, ev%r%xr <= post *) - let ev = pr.pr_event in - let ev = ss_inv_rebind ev m in - let concl_po = map_ss_inv2 f_xreal_le (map_ss_inv1 f_b2xr ev) post in - let concl_po = f_forall_mems_ss_inv mpo concl_po in - - (* 0%r <= bd *) - let concl_nn = f_real_le f_r0 bd in - - FApi.xmutate1 tc `HlDeno [concl_e; concl_pr; concl_po; concl_nn] - -(* -------------------------------------------------------------------- *) -let cond_pre env prl prr pre = - (* building the substitution for the pre *) - (* we substitute param by args and left by ml and right by mr *) - let ml, mr = pre.ml, pre.mr in - let sargs = PVM.add env pv_arg ml prl.pr_args PVM.empty in - let sargs = PVM.add env pv_arg mr prr.pr_args sargs in - let smem = Fsubst.f_subst_id in - let smem = Fsubst.f_bind_mem smem ml prl.pr_mem in - let smem = Fsubst.f_bind_mem smem mr prr.pr_mem in - Fsubst.f_subst smem (PVM.subst env sargs pre.inv) - -let t_equiv_deno_r pre post tc = - let env, _, concl = FApi.tc1_eflat tc in - let ml, mr = pre.ml, pre.mr in - - let cmp, f1, f2 = - match concl.f_node with - | Fapp({f_node = Fop(op,_)}, [f1;f2]) when is_pr f1 && is_pr f2 && - (EcPath.p_equal op EcCoreLib.CI_Bool.p_eq || - EcPath.p_equal op EcCoreLib.CI_Real.p_real_le) -> - let cmp = - match op with - | _ when EcPath.p_equal op EcCoreLib.CI_Bool.p_eq -> `Eq - | _ when EcPath.p_equal op EcCoreLib.CI_Real.p_real_le -> `Le - | _ -> assert false - in cmp, f1, f2 - - | _ -> tc_error !!tc "invalid goal shape" - - in - - let (prl, prr) = (destr_pr f1, destr_pr f2) in - let concl_e = f_equivF pre prl.pr_fun prr.pr_fun post in - let funl = EcEnv.Fun.by_xpath prl.pr_fun env in - let funr = EcEnv.Fun.by_xpath prr.pr_fun env in - - (* building the substitution for the pre *) - (* we substitute param by args and left by ml and right by mr *) - let concl_pr = cond_pre env prl prr pre in - - (* building the substitution for the post *) - let evl = ss_inv_generalize_as_left prl.pr_event ml mr in - let evr = ss_inv_generalize_as_right prr.pr_event ml mr in - let cmp = - match cmp with - | `Eq -> map_ts_inv2 f_iff evl evr - | `Le -> map_ts_inv2 f_imp evl evr - | `Ge -> map_ts_inv2 f_imp evr evl in - - let mel = EcEnv.Fun.actmem_post ml funl in - let mer = EcEnv.Fun.actmem_post mr funr in - let concl_po = f_forall_mems_ts_inv mel mer (map_ts_inv2 f_imp post cmp) in - - FApi.xmutate1 tc `HlDeno [concl_e; concl_pr; concl_po] - -(* -------------------------------------------------------------------- *) -let t_phoare_deno = FApi.t_low2 "phoare-deno" t_phoare_deno_r -let t_ehoare_deno = FApi.t_low2 "ehoare-deno" t_ehoare_deno_r -let t_equiv_deno = FApi.t_low2 "equiv-deno" t_equiv_deno_r - -(* -------------------------------------------------------------------- *) -let process_phoare_deno info tc = - let error () = - tc_error !!tc "the conclusion is not a suitable Pr expression" in - - let process_cut (pre, post) = - let hyps, concl = FApi.tc1_flat tc in - let cmp, f, bd = - match concl.f_node with - | Fapp ({f_node = Fop (op, _)}, [f1; f2]) - when EcPath.p_equal op EcCoreLib.CI_Bool.p_eq - -> - if is_pr f1 then (FHeq, f1, f2) - else if is_pr f2 then (FHeq, f2, f1) - else error () - - | Fapp({f_node = Fop (op, _)}, [f1; f2]) - when EcPath.p_equal op EcCoreLib.CI_Real.p_real_le - -> - if is_pr f1 then (FHle, f1, f2) (* f1 <= f2 *) - else if is_pr f2 then (FHge, f2, f1) (* f2 >= f1 *) - else error () - - | _ -> error () - in - - let { pr_fun = f } as pr = destr_pr f in - let event = pr.pr_event in - let m = event.m in - let penv, qenv = LDecl.hoareF m f hyps in - let pre = pre |> omap_dfl (fun p -> TTC.pf_process_formula !!tc penv p) f_true in - let post = post |> omap_dfl (fun p -> TTC.pf_process_formula !!tc qenv p) event.inv in - - f_bdHoareF {m;inv=pre} f {m;inv=post} cmp {m;inv=bd} - in - - let pt, ax = - PT.tc1_process_full_closed_pterm_cut - ~prcut:process_cut tc info in - - let pre, post = - let bhf = pf_as_bdhoareF !!tc ax in - (bhf_pr bhf, bhf_po bhf) - in - - FApi.t_first (EcLowGoal.Apply.t_apply_bwd_hi ~dpe:true pt) (t_phoare_deno pre post tc) (* -------------------------------------------------------------------- *) -let process_ehoare_deno info tc = - let error () = - tc_error !!tc "the conclusion is not a suitable Pr expression" in - - let process_cut (pre, post) = - let hyps, concl = FApi.tc1_flat tc in - let f, bd = - match concl.f_node with - | Fapp({f_node = Fop (op, _)}, [f1; f2]) - when EcPath.p_equal op EcCoreLib.CI_Real.p_real_le && is_pr f1 -> - (f1, f2) (* f1 <= f2 *) - | _ -> error () - in - - let { pr_fun = f } as pr = destr_pr f in - let event = pr.pr_event in - let m = event.m in - let penv, qenv = LDecl.hoareF m f hyps in - let smem = Fsubst.f_bind_mem Fsubst.f_subst_id pr.pr_mem m in - let dpre = {m;inv=f_r2xr (Fsubst.f_subst smem bd)} in - - let pre = pre |> omap_dfl (fun p -> {m;inv=TTC.pf_process_xreal !!tc penv p}) dpre in - let post = post |> omap_dfl (fun p -> {m;inv=TTC.pf_process_xreal !!tc qenv p}) (map_ss_inv1 f_b2xr event) in - - f_eHoareF pre f post - in - - let pt, ax = - PT.tc1_process_full_closed_pterm_cut - ~prcut:process_cut tc info in - - let pre, post = - let hf = pf_as_ehoareF !!tc ax in - (ehf_pr hf, ehf_po hf) - in - - (* [t_ehoare_deno] always emits the [0%r <= bd] non-negativity goal last; try - to close it automatically so trivially non-negative bounds stay effort-free - (a genuinely negative bound is left as an unprovable goal). *) - FApi.t_last (FApi.t_try t_trivial) - (FApi.t_first (EcLowGoal.Apply.t_apply_bwd_hi ~dpe:true pt) (t_ehoare_deno pre post tc)) - - -(* -------------------------------------------------------------------- *) -let destr_deno_bad env f = - try - let fpr1, (fpr2, fpr3) = snd_map DestrReal.add (DestrReal.le f) in - let _, pr2, pr3 = t3_map destr_pr (fpr1, fpr2, fpr3) in - - if not (NormMp.x_equal env pr2.pr_fun pr3.pr_fun) then - raise (DestrError ""); - (fpr1, fpr2, fpr3) - - with DestrError _ -> raise (DestrError "destr_deno_bad") - -(* -------------------------------------------------------------------- *) -let tc_destr_deno_bad tc env f = - try destr_deno_bad env f - with DestrError _ -> tc_error !!tc "invalid goal shape" - -(* -------------------------------------------------------------------- *) -let t_pr_pos tc = - let pr = - try - let _, fpr = DestrReal.le (tc1_goal tc) in - destr_pr fpr - with DestrError _ -> tc_error !!tc "invalid goal shape" in - let prf = f_pr_r {pr with pr_event = {m=pr.pr_event.m; inv=f_false}} in - (t_real_le_trans prf @+ - [ t_pr_rewrite ("mu_false", None) @! t_true; - t_pr_rewrite ("mu_sub", None) @! t_true]) tc - -(* -------------------------------------------------------------------- *) -let t_equiv_deno_bad pre tc = - let env, _hyps, concl = FApi.tc1_eflat tc in - let fpr1, fpr2, fprb = tc_destr_deno_bad tc env concl in - let pr1 = destr_pr fpr1 and pr2 = destr_pr fpr2 and prb = destr_pr fprb in - if not (pr2.pr_mem = prb.pr_mem) then - tc_error !!tc "invalid goal shape"; - let m = prb.pr_event.m in - let ev2 = ss_inv_rebind pr2.pr_event m in - let fand = map_ss_inv2 f_and ev2 (map_ss_inv1 f_not prb.pr_event) in - let pro = f_pr pr2.pr_mem pr2.pr_fun pr2.pr_args (map_ss_inv2 f_or fand prb.pr_event) in - let pra = f_pr pr2.pr_mem pr2.pr_fun pr2.pr_args fand in - let t_false tc = t_apply_prept (`UG real_upto_false) tc in - let ml, mr = pre.ml, pre.mr in - let post = - let ev1 = ss_inv_generalize_as_left pr1.pr_event ml mr in - let ev2 = ss_inv_generalize_as_right ev2 ml mr in - let bad2 = ss_inv_generalize_as_right prb.pr_event ml mr in - map_ts_inv2 f_imp (map_ts_inv1 f_not bad2) (map_ts_inv2 f_imp ev1 ev2) in - - (t_real_le_trans pro @+ - [t_equiv_deno pre post @+ [ - t_id; - t_id; - t_intros_s (`Symbol ["_";"_"]) @! t_apply_prept (`UG real_upto_or) ]; - t_pr_rewrite_i ("mu_disjoint", None) @+ - [ t_intro_s (`Symbol "_") @! t_false; - t_apply_prept - (`App (`UG real_ler_add, [`F pra;`F fpr2;`F fprb;`F fprb; `H_; `H_])) - @+ [ - t_pr_rewrite_i ("mu_sub",None) @+ [ - t_intros_s (`Symbol ["_"]) @! t_apply_prept (`UG real_upto_sub); - t_trivial; - ]; - t_true; - ] - ] - ]) tc - -(* -------------------------------------------------------------------- *) -let destr_deno_bad2 env f = - try - let lhs , rhs = DestrReal.le f in - let fpr1, fpr2 = DestrReal.sub (DestrReal.abs lhs) in - let _pr1, pr2, prb = t3_map destr_pr (fpr1, fpr2, rhs) in - if not (NormMp.x_equal env pr2.pr_fun prb.pr_fun) then - raise (DestrError "pr"); - (fpr1, fpr2, rhs) - with DestrError _ -> raise (DestrError "destr_deno_bad2") - -(* -------------------------------------------------------------------- *) -let tc_destr_deno_bad2 tc env f = - try destr_deno_bad2 env f - with DestrError _ -> tc_error !!tc "invalid goal shape" - -(* -------------------------------------------------------------------- *) -let t_equiv_deno_bad2 pre bad1 tc = - let ml, mr = pre.ml, pre.mr in - let env, hyps, concl = FApi.tc1_eflat tc in - let fpr1, fpr2, fprb = tc_destr_deno_bad2 tc env concl in - let pr1 = destr_pr fpr1 and pr2 = destr_pr fpr2 and - prb = destr_pr fprb in - if not (pr2.pr_mem = prb.pr_mem) then - tc_error !!tc "invalid goal shape"; - let f1 = pr1.pr_fun and f2 = pr2.pr_fun in - let ev1 = pr1.pr_event and ev2 = pr2.pr_event in - let ev1 = ss_inv_rebind ev1 bad1.m in - let bad2 = prb.pr_event in - let bad2 = ss_inv_rebind bad2 ev2.m in - let post = - let bad1 = ss_inv_generalize_as_left bad1 ml mr in - let ev1 = ss_inv_generalize_as_left ev1 ml mr in - let bad2 = ss_inv_generalize_as_right bad2 ml mr in - let ev2 = ss_inv_generalize_as_right ev2 ml mr in - map_ts_inv2 f_and (map_ts_inv2 f_iff bad1 bad2) - (map_ts_inv2 f_imp (map_ts_inv1 f_not bad2) (map_ts_inv2 f_iff ev1 ev2)) in - let equiv = f_equivF pre f1 f2 post in - let cpre = cond_pre env pr1 pr2 pre in - let fpreb1 = f_pr pr1.pr_mem pr1.pr_fun pr1.pr_args (map_ss_inv2 f_and ev1 bad1) in - let fpren1 = f_pr pr1.pr_mem pr1.pr_fun pr1.pr_args (map_ss_inv2 f_and ev1 (map_ss_inv1 f_not bad1)) in - let fpreb2 = f_pr pr2.pr_mem pr2.pr_fun pr2.pr_args (map_ss_inv2 f_and ev2 bad2) in - let fpren2 = f_pr pr2.pr_mem pr2.pr_fun pr2.pr_args (map_ss_inv2 f_and ev2 (map_ss_inv1 f_not bad2)) in - let fabs' = - f_real_abs - (f_real_sub (f_real_add fpreb1 fpren1) (f_real_add fpreb2 fpren2)) in - let hequiv,hcpre = as_seq2 (EcEnv.LDecl.fresh_ids hyps ["_";"_"]) in - (t_cut equiv @+ - [ t_id; - t_cut cpre @+ - [ t_id; - t_intros_i [hcpre; hequiv] @! - t_real_le_trans fabs' @+ - [ t_apply_prept (`UG real_eq_le) @! - (process_congr PCongrDefault) @! (* abs *) - (process_congr PCongrDefault) @~ (* add *) - (t_last (process_congr PCongrDefault)) @~+ (* opp *) - [ t_pr_rewrite_i ("mu_split", Some bad1) @! t_reflex; - t_pr_rewrite_i ("mu_split", Some bad2) @! t_reflex ] ; - t_apply_prept (`UG real_upto) @+ - [ t_pr_pos; - t_pr_pos; - t_equiv_deno pre post @+ [ - t_apply_hyp hequiv; - t_apply_hyp hcpre; - t_intros_s (`Symbol ["_"; "_"]) @! - t_apply_prept (`UG real_upto_imp_bad) ]; - t_pr_rewrite ("mu_sub",None) @! t_trivial; - t_equiv_deno pre post @+ [ - t_apply_hyp hequiv; - t_apply_hyp hcpre; - t_intros_s (`Symbol ["_"; "_"]) @! - t_apply_prept (`UG real_upto_notbad) - ]; - ] - ] - ] - ]) tc - -(* -------------------------------------------------------------------- *) -let process_pre tc hyps prl prr pre post = - let fl = prl.pr_fun and fr = prr.pr_fun in - let ml, mr = post.ml, post.mr in - match pre with - | Some p -> - let penv, _ = LDecl.equivF ml mr fl fr hyps in - {ml;mr;inv=TTC.pf_process_formula !!tc penv p} - | None -> - let al = prl.pr_args and ar = prr.pr_args in - let pml = prl.pr_mem and pmr = prr.pr_mem in - - let env = LDecl.toenv hyps in - let eqs = ref [] in - let push f = eqs := f :: !eqs in - - let dopv m mi gen_o x ty = - if is_glob x then push (gen_o (map_ss_inv1 (fun f -> f_eq f (f_pvar x ty mi).inv) (f_pvar x ty m))) in - - let doglob m mi gen_o g = push (gen_o ((map_ss_inv1 (fun f -> f_eq f (NormMp.norm_glob env mi g).inv)) (NormMp.norm_glob env m g))) in - let dof f a m mi gen_o = - try - let fv = PV.remove env pv_res (PV.fv env m post.inv) in - PV.iter (dopv m mi gen_o) (doglob m mi gen_o) (eqobs_inF_refl env f fv); - if not (EcReduction.EqTest.for_type env a.f_ty tunit) then - push (map_ts_inv1 (fun f -> f_eq f a) (gen_o (f_pvarg a.f_ty m))) - with EcCoreGoal.TcError _ | EqObsInError -> () in - - let gen_r f = ss_inv_generalize_right f mr in - let gen_l f = ss_inv_generalize_left f ml in - dof fl al ml pml gen_r; dof fr ar mr pmr gen_l; - map_ts_inv ~ml ~mr f_ands !eqs - -(* -------------------------------------------------------------------- *) -let post_iff ml mr eq env evl evr = - let post = map_ts_inv2 f_iff evl evr in - try - if not eq then raise Not_found; - {ml;mr;inv=Mpv2.to_form - (Mpv2.needed_eq env post) ml mr f_true} - with Not_found -> post - -(* -------------------------------------------------------------------- *) -let process_equiv_deno1 info eq tc = - let process_cut (pre, post) = - let env, hyps, concl = FApi.tc1_eflat tc in - - let op, f1, f2 = - match concl.f_node with - | Fapp ({f_node = Fop (op, _)}, [f1; f2]) when is_pr f1 && is_pr f2 -> - (op, f1, f2) - - | _ -> tc_error !!tc "invalid goal shape" - in - - let ml , mr = EcIdent.create "&1", EcIdent.create "&2" in - - let { pr_fun = fl } as prl = destr_pr f1 in - let evl = ss_inv_generalize_as_left prl.pr_event ml mr in - let { pr_fun = fr } as prr = destr_pr f2 in - let evr = ss_inv_generalize_as_right prr.pr_event ml mr in - - let post = - match post with - | Some p -> - let _, qenv = LDecl.equivF ml mr fl fr hyps in - {ml;mr;inv=TTC.pf_process_formula !!tc qenv p} - | None -> - match op with - | _ when EcPath.p_equal op EcCoreLib.CI_Bool.p_eq -> - (post_iff ml mr eq env evl evr) - | _ when EcPath.p_equal op EcCoreLib.CI_Real.p_real_le -> - map_ts_inv2 f_imp evl evr - | _ -> - tc_error !!tc "not able to reconize a comparison operator" in - - let pre = process_pre tc hyps prl prr pre post in - - f_equivF pre fl fr post - in - - let pt, ax = - PT.tc1_process_full_closed_pterm_cut - ~prcut:process_cut tc info in - - let pre, post = - let ef = pf_as_equivF !!tc ax in - (ef_pr ef, ef_po ef) - in - - FApi.t_first (EcLowGoal.Apply.t_apply_bwd_hi ~dpe:true pt) (t_equiv_deno pre post tc) - -(* -------------------------------------------------------------------- *) -let process_equiv_deno_bad info tc = - let process_cut (pre, post) = - let env, hyps, concl = FApi.tc1_eflat tc in - let fpr1, fpr2, fprb = tc_destr_deno_bad tc env concl in - - let { pr_fun = fl ; pr_event = evl } as prl = destr_pr fpr1 in - let { pr_fun = fr ; pr_event = evr } as prr = destr_pr fpr2 in - - let ml , mr = EcIdent.create "&1", EcIdent.create "&2" in - - let post = - match post with - | Some p -> - let _, qenv = LDecl.equivF ml mr fl fr hyps in - {ml;mr;inv=TTC.pf_process_formula !!tc qenv p} - | None -> - let evl = ss_inv_generalize_as_left evl ml mr in - let evr = ss_inv_generalize_as_right evr ml mr in - let bad = ss_inv_generalize_as_right (destr_pr fprb).pr_event ml mr in - let f_imps' l = f_imps (List.tl l) (List.hd l) in - map_ts_inv f_imps' [evr; map_ts_inv1 f_not bad; evl] in - let pre = process_pre tc hyps prl prr pre post in - - f_equivF pre fl fr post - in - - let pt, ax = - PT.tc1_process_full_closed_pterm_cut - ~prcut:process_cut tc info in - - let equiv = pf_as_equivF !!tc ax in - let pre = (ef_pr equiv) in - - let torotate = ref 1 in - let t_sub = - FApi.t_or (EcLowGoal.Apply.t_apply_bwd_hi ~dpe:true pt) - (EcPhlConseq.t_equivF_conseq pre (ef_po equiv) @+ - [t_true; (fun tc -> incr torotate;t_id tc); - EcLowGoal.Apply.t_apply_bwd_hi ~dpe:true pt]) in - let gs = - t_last t_sub (t_rotate `Left 1 (t_equiv_deno_bad pre tc)) in - t_rotate `Left !torotate gs - -(* -------------------------------------------------------------------- *) -let process_equiv_deno info eq g = - let env, _hyps, concl = FApi.tc1_eflat g in - try ignore (destr_deno_bad env concl); - process_equiv_deno_bad info g - with DestrError _ -> - process_equiv_deno1 info eq g - -(* -------------------------------------------------------------------- *) -let process_equiv_deno_bad2 info eq bad1 tc = - let env, hyps, concl = FApi.tc1_eflat tc in - let fpr1, fpr2, fprb = tc_destr_deno_bad2 tc env concl in - - let { pr_fun = fl; pr_mem = ml ; pr_event = evl } as prl = destr_pr fpr1 in - let { pr_fun = fr; pr_event = evr } as prr = destr_pr fpr2 in - - let ml' , mr' = EcIdent.create "&1", EcIdent.create "&2" in - - let bad1 = - let _, qenv = LDecl.hoareF ml fl hyps in - {m=ml;inv=TTC.pf_process_formula !!tc qenv bad1} in - - let process_cut (pre, post) = - - let post = - match post with - | Some p -> - let _, qenv = LDecl.equivF ml' mr' fl fr hyps in - {ml=ml';mr=mr';inv=TTC.pf_process_formula !!tc qenv p} - | None -> - let evl = ss_inv_generalize_as_left evl ml' mr' in - let evr = ss_inv_generalize_as_right evr ml' mr' in - let bad1 = ss_inv_generalize_as_left bad1 ml' mr' in - let bad2 = ss_inv_generalize_as_right (destr_pr fprb).pr_event ml' mr' in - let iff = post_iff ml' mr' eq env evl evr in - map_ts_inv2 f_and (map_ts_inv2 f_iff bad1 bad2) (map_ts_inv2 f_imp (map_ts_inv1 f_not bad2) iff) in - - let pre = process_pre tc hyps prl prr pre post in - - f_equivF pre fl fr post - in - - let pt, ax = - PT.tc1_process_full_closed_pterm_cut - ~prcut:process_cut tc info in - - let equiv = pf_as_equivF !!tc ax in - let pre = (ef_pr equiv) in +(* The [deno] rules live in [rules//] (bdhoare, ehoare, equiv), + with their derived forms and elaboration. This module only keeps the + dispatcher and the legacy entry points. *) +let t_phoare_deno pre post = + EcBdHoareDeno.(t_bdhoare_deno_full { bdd_pre = pre; bdd_post = post; }) - let torotate = ref 1 in - let t_sub = - FApi.t_or (EcLowGoal.Apply.t_apply_bwd_hi ~dpe:true pt) - (EcPhlConseq.t_equivF_conseq pre (ef_po equiv) @+ - [t_true; (fun tc -> incr torotate;t_id tc); - EcLowGoal.Apply.t_apply_bwd_hi ~dpe:true pt]) in - let gs = - t_last t_sub (t_rotate `Left 1 (t_equiv_deno_bad2 pre bad1 tc)) in - t_rotate `Left !torotate gs +let t_equiv_deno pre post = + EcEquivDeno.(t_equiv_deno { eqd_pre = pre; eqd_post = post; }) (* -------------------------------------------------------------------- *) type denoff = deno_ppterm * bool * pformula option -let process_deno mode (info, eq, bad1) g = +let process_deno mode ((info, _, _) as denoff : denoff) tc = match mode with - | `PHoare -> process_phoare_deno info g - | `EHoare -> process_ehoare_deno info g - | `Equiv -> - match bad1 with - | None -> process_equiv_deno info eq g - | Some bad1 -> process_equiv_deno_bad2 info eq bad1 g + | `PHoare -> EcBdHoareDeno.process_bdhoare_deno info tc + | `EHoare -> EcEHoareDeno.process_ehoare_deno info tc + | `Equiv -> EcEquivDeno.process_equiv_deno denoff tc diff --git a/src/phl/rules/bdhoare/ecBdHoareDeno.ml b/src/phl/rules/bdhoare/ecBdHoareDeno.ml new file mode 100644 index 000000000..8f588769a --- /dev/null +++ b/src/phl/rules/bdhoare/ecBdHoareDeno.ml @@ -0,0 +1,167 @@ +(* -------------------------------------------------------------------- *) +open EcUtils +open EcParsetree +open EcAst +open EcTypes +open EcFol +open EcEnv +open EcPV +open EcSubst + +open EcCoreGoal +open EcLowGoal +open EcLowPhlGoal + +module PT = EcProofTerm +module TTC = EcProofTyping + +(* -------------------------------------------------------------------- *) +(* Parameters of the bdhoare [deno] rule: the pre- and postcondition of + the judgement on the procedure, in one memory. Already typed, nothing + to resolve: the same record is the rule argument and the node + payload. *) +type bdhoare_deno = { + bdd_pre : ss_inv; (* P *) + bdd_post : ss_inv; (* Q *) +} + +type EcCoreGoal.rule += RBdHoareDeno of bdhoare_deno + +(* -------------------------------------------------------------------- *) +(* The goals the rule applies to: [Pr[...] <= d], [d <= Pr[...]] and + [Pr[...] = d], with the comparison they state. *) +let destr_deno_goal (concl : form) = + match concl.f_node with + | Fapp ({f_node = Fop (op, _)}, [f; bd]) + when is_pr f && EcPath.p_equal op EcCoreLib.CI_Real.p_real_le -> + Some (FHle, destr_pr f, bd) + + | Fapp ({f_node = Fop (op, _)}, [bd; f]) + when is_pr f && EcPath.p_equal op EcCoreLib.CI_Real.p_real_le -> + Some (FHge, destr_pr f, bd) + + | Fapp ({f_node = Fop (op, _)}, [f; bd]) + when is_pr f && EcPath.p_equal op EcCoreLib.CI_Bool.p_eq -> + Some (FHeq, destr_pr f, bd) + + | _ -> None + +(* [P] and [Q] share their memory, which does not occur free in the goal + (it is bound by the judgement of the premise, around the bound [d]). *) +let valid_memories (concl : form) (n : bdhoare_deno) = + EcIdent.id_equal n.bdd_pre.m n.bdd_post.m + && not (EcIdent.Mid.mem n.bdd_pre.m concl.f_fv) + +(* -------------------------------------------------------------------- *) +(* Pure core shared by the rule and its checker. Its side conditions (the + shape of the goal and the memories of [P] and [Q]) are part of it, so + the checker re-validates them. *) +let bdhoare_deno_subgoals (hyps : LDecl.hyps) (concl : form) (n : bdhoare_deno) = + let env = LDecl.toenv hyps in + let cmp, pr, bd = + match destr_deno_goal concl with + | Some x -> x + | None -> failwith "bdhoare-deno: invalid goal shape" in + if not (valid_memories concl n) then + failwith "bdhoare-deno: invalid memories"; + let m = n.bdd_pre.m in + let concl_e = f_bdHoareF n.bdd_pre pr.pr_fun n.bdd_post cmp { m; inv = bd; } in + let fun_ = Fun.by_xpath pr.pr_fun env in + + (* P, with the arguments and the initial memory of the goal *) + let sargs = PVM.add env pv_arg m pr.pr_args PVM.empty in + let smem = Fsubst.f_bind_mem Fsubst.f_subst_id m pr.pr_mem in + let concl_pr = Fsubst.f_subst smem (PVM.subst env sargs n.bdd_pre.inv) in + + (* Q relates to the event of the goal, in every final memory *) + let ev = pr.pr_event in + let me = Fun.actmem_post ev.m fun_ in + let post = ss_inv_rebind n.bdd_post ev.m in + let concl_po = + match cmp with + | FHle -> map_ss_inv2 f_imp_simpl ev post + | FHge -> map_ss_inv2 f_imp_simpl post ev + | FHeq -> map_ss_inv2 f_iff_simpl ev post in + let concl_po = f_forall_mems_ss_inv me concl_po in + + [concl_e; concl_pr; concl_po] + +(* -------------------------------------------------------------------- *) +(* Rule (TCB). *) +let t_bdhoare_deno (r : bdhoare_deno) (tc : tcenv1) = + let concl = FApi.tc1_goal tc in + if Option.is_none (destr_deno_goal concl) then + tc_error !!tc "invalid goal shape"; + if not (valid_memories concl r) then + tc_error !!tc "invalid memories for the probabilistic judgement"; + FApi.xrule1 tc (RBdHoareDeno r) + (bdhoare_deno_subgoals (FApi.tc1_hyps tc) concl r) + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | RBdHoareDeno n -> + Some (EcPlRecheck.checker_of "bdhoare-deno" (fun _ concl -> concl) + (fun hyps concl -> bdhoare_deno_subgoals hyps concl n)) + | _ -> None) + +(* -------------------------------------------------------------------- *) +(* Derived (no proof-node): an equality with the probability on its + right-hand side is first turned around. *) +let t_bdhoare_deno_full (r : bdhoare_deno) (tc : tcenv1) = + match (FApi.tc1_goal tc).f_node with + | Fapp ({f_node = Fop (op, _)}, [f; _bd]) + when EcPath.p_equal op EcCoreLib.CI_Bool.p_eq && not (is_pr f) -> + FApi.t_seq t_symmetry (t_bdhoare_deno r) tc + + | _ -> t_bdhoare_deno r tc + +(* -------------------------------------------------------------------- *) +(* Elaboration: the judgement is given by a proof term, or cut from the + goal (precondition [true] and postcondition the event by default), + then the derived rule is applied and the premise closed with it. *) +let process_bdhoare_deno (info : deno_ppterm) (tc : tcenv1) = + let error () = + tc_error !!tc "the conclusion is not a suitable Pr expression" in + + let process_cut (pre, post) = + let hyps, concl = FApi.tc1_flat tc in + let cmp, f, bd = + match concl.f_node with + | Fapp ({f_node = Fop (op, _)}, [f1; f2]) + when EcPath.p_equal op EcCoreLib.CI_Bool.p_eq + -> + if is_pr f1 then (FHeq, f1, f2) + else if is_pr f2 then (FHeq, f2, f1) + else error () + + | Fapp({f_node = Fop (op, _)}, [f1; f2]) + when EcPath.p_equal op EcCoreLib.CI_Real.p_real_le + -> + if is_pr f1 then (FHle, f1, f2) (* f1 <= f2 *) + else if is_pr f2 then (FHge, f2, f1) (* f2 >= f1 *) + else error () + + | _ -> error () + in + + let { pr_fun = f } as pr = destr_pr f in + let event = pr.pr_event in + let m = event.m in + let penv, qenv = LDecl.hoareF m f hyps in + let pre = pre |> omap_dfl (fun p -> TTC.pf_process_formula !!tc penv p) f_true in + let post = post |> omap_dfl (fun p -> TTC.pf_process_formula !!tc qenv p) event.inv in + + f_bdHoareF { m; inv = pre; } f { m; inv = post; } cmp { m; inv = bd; } + in + + let pt, ax = + PT.tc1_process_full_closed_pterm_cut + ~prcut:process_cut tc info in + + let bhf = pf_as_bdhoareF !!tc ax in + + FApi.t_first + (EcLowGoal.Apply.t_apply_bwd_hi ~dpe:true pt) + (t_bdhoare_deno_full { bdd_pre = bhf_pr bhf; bdd_post = bhf_po bhf; } tc) diff --git a/src/phl/rules/bdhoare/ecBdHoareDeno.mli b/src/phl/rules/bdhoare/ecBdHoareDeno.mli new file mode 100644 index 000000000..5f63c16d6 --- /dev/null +++ b/src/phl/rules/bdhoare/ecBdHoareDeno.mli @@ -0,0 +1,53 @@ +(* -------------------------------------------------------------------- *) +open EcParsetree +open EcCoreGoal.FApi +open EcAst + +(* ==================================================================== *) +(* Rules (trusted) *) + +type bdhoare_deno = { + bdd_pre : ss_inv; (* P, in the memory &m of the judgement *) + bdd_post : ss_inv; (* Q, in the same memory *) +} + +(* [t_bdhoare_deno { bdd_pre = P; bdd_post = Q }] — a probability bounded + by a probabilistic judgement on the procedure, with [~] the goal's + comparison: + + phoare [f : P ==> Q] ~ d + P[&m := &n, arg := args] + forall &m', E [=>] Q + ------------------------------------------ + Pr[f(args) @ &n : E] [~] d + + where [Pr [~] d] is [Pr <= d] for [<=], [Pr = d] for [=] and + [d <= Pr] for [>=]; in the third premise, [&m'] is the final memory of + the event [E], [Q] is read in it, and [E [=>] Q] is [E => Q] for [<=], + [Q => E] for [>=] and [E <=> Q] for [=]. Side conditions: the goal has + one of the three shapes above; [P] and [Q] are in the same memory + [&m], which does not occur free in the goal (otherwise fails). + + Node: [RBdHoareDeno { bdd_pre = P; bdd_post = Q }]. + Checker: "bdhoare-deno". *) +val t_bdhoare_deno : bdhoare_deno -> backward + +(* ==================================================================== *) +(* Derived tactics *) + +(* [t_bdhoare_deno_full r] — on [d = Pr[...]], [d] not a probability: + first [EcLowGoal.t_symmetry], to [Pr[...] = d]; then [t_bdhoare_deno r]. + On any other goal, [t_bdhoare_deno r]. Visible goals: the premises of + [t_bdhoare_deno]. Emits no node of its own. *) +val t_bdhoare_deno_full : bdhoare_deno -> backward + +(* ==================================================================== *) +(* Elaboration *) + +(* [byphoare pt] (resp. [byphoare (_ : P ==> Q)]) on [Pr[f(args) @ &n : E] + ~ d] or [d ~ Pr[...]], [~] among [<=], [=]: the judgement + [phoare [f : P ==> Q] ~ d] is the type of the proof term [pt] (resp. + is cut, [P] and [Q] typed in the memory of the event, [true] and [E] + by default). Applies [t_bdhoare_deno_full], and closes its first + premise with [pt] (resp. leaves it as the first goal). *) +val process_bdhoare_deno : deno_ppterm -> backward diff --git a/src/phl/rules/ehoare/ecEHoareDeno.ml b/src/phl/rules/ehoare/ecEHoareDeno.ml new file mode 100644 index 000000000..a803d5ad7 --- /dev/null +++ b/src/phl/rules/ehoare/ecEHoareDeno.ml @@ -0,0 +1,140 @@ +(* -------------------------------------------------------------------- *) +open EcUtils +open EcParsetree +open EcAst +open EcTypes +open EcFol +open EcEnv +open EcPV +open EcSubst + +open EcCoreGoal +open EcLowGoal +open EcLowPhlGoal + +module PT = EcProofTerm +module TTC = EcProofTyping + +(* -------------------------------------------------------------------- *) +(* Parameters of the ehoare [deno] rule: the pre- and postcondition of + the judgement on the procedure, in one memory. Already typed, nothing + to resolve: the same record is the rule argument and the node + payload. *) +type ehoare_deno = { + ehd_pre : ss_inv; (* P *) + ehd_post : ss_inv; (* Q *) +} + +type EcCoreGoal.rule += REHoareDeno of ehoare_deno + +(* -------------------------------------------------------------------- *) +(* The goals the rule applies to: [Pr[...] <= d]. *) +let destr_deno_goal (concl : form) = + match concl.f_node with + | Fapp ({f_node = Fop (op, _)}, [f; bd]) + when is_pr f && EcPath.p_equal op EcCoreLib.CI_Real.p_real_le -> + Some (destr_pr f, bd) + + | _ -> None + +(* [P] and [Q] share their memory, which does not occur free in the goal + (it is bound around the event of the goal in the third premise). *) +let valid_memories (concl : form) (n : ehoare_deno) = + EcIdent.id_equal n.ehd_pre.m n.ehd_post.m + && not (EcIdent.Mid.mem n.ehd_pre.m concl.f_fv) + +(* -------------------------------------------------------------------- *) +(* Pure core shared by the rule and its checker. Its side conditions (the + shape of the goal and the memories of [P] and [Q]) are part of it, so + the checker re-validates them. *) +let ehoare_deno_subgoals (hyps : LDecl.hyps) (concl : form) (n : ehoare_deno) = + let env = LDecl.toenv hyps in + let pr, bd = + match destr_deno_goal concl with + | Some x -> x + | None -> failwith "ehoare-deno: invalid goal shape" in + if not (valid_memories concl n) then + failwith "ehoare-deno: invalid memories"; + let m = n.ehd_pre.m in + let concl_e = f_eHoareF n.ehd_pre pr.pr_fun n.ehd_post in + let _, mpo = Fun.hoareF_memenv m pr.pr_fun env in + + (* P <= d, with the arguments and the initial memory of the goal *) + let sargs = PVM.add env pv_arg m pr.pr_args PVM.empty in + let smem = Fsubst.f_bind_mem Fsubst.f_subst_id m pr.pr_mem in + let pre = Fsubst.f_subst smem (PVM.subst env sargs n.ehd_pre.inv) in + let concl_pr = f_xreal_le pre (f_r2xr bd) in + + (* forall &m, E%xr <= Q *) + let ev = ss_inv_rebind pr.pr_event m in + let concl_po = map_ss_inv2 f_xreal_le (map_ss_inv1 f_b2xr ev) n.ehd_post in + let concl_po = f_forall_mems_ss_inv mpo concl_po in + + (* 0%r <= d *) + let concl_nn = f_real_le f_r0 bd in + + [concl_e; concl_pr; concl_po; concl_nn] + +(* -------------------------------------------------------------------- *) +(* Rule (TCB). *) +let t_ehoare_deno (r : ehoare_deno) (tc : tcenv1) = + let concl = FApi.tc1_goal tc in + if Option.is_none (destr_deno_goal concl) then + tc_error !!tc "invalid goal shape"; + if not (valid_memories concl r) then + tc_error !!tc "invalid memories for the expectation judgement"; + FApi.xrule1 tc (REHoareDeno r) + (ehoare_deno_subgoals (FApi.tc1_hyps tc) concl r) + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | REHoareDeno n -> + Some (EcPlRecheck.checker_of "ehoare-deno" (fun _ concl -> concl) + (fun hyps concl -> ehoare_deno_subgoals hyps concl n)) + | _ -> None) + +(* -------------------------------------------------------------------- *) +(* Elaboration: the judgement is given by a proof term, or cut from the + goal (precondition the bound and postcondition the event by default), + then the rule is applied, its first premise closed with it, and its + last premise [0%r <= d] closed when trivial (a genuinely negative + bound is left as an unprovable goal). *) +let process_ehoare_deno (info : deno_ppterm) (tc : tcenv1) = + let error () = + tc_error !!tc "the conclusion is not a suitable Pr expression" in + + let process_cut (pre, post) = + let hyps, concl = FApi.tc1_flat tc in + let f, bd = + match concl.f_node with + | Fapp({f_node = Fop (op, _)}, [f1; f2]) + when EcPath.p_equal op EcCoreLib.CI_Real.p_real_le && is_pr f1 -> + (f1, f2) (* f1 <= f2 *) + | _ -> error () + in + + let { pr_fun = f } as pr = destr_pr f in + let event = pr.pr_event in + let m = event.m in + let penv, qenv = LDecl.hoareF m f hyps in + let smem = Fsubst.f_bind_mem Fsubst.f_subst_id pr.pr_mem m in + let dpre = { m; inv = f_r2xr (Fsubst.f_subst smem bd); } in + + let pre = pre |> omap_dfl (fun p -> { m; inv = TTC.pf_process_xreal !!tc penv p; }) dpre in + let post = post |> omap_dfl (fun p -> { m; inv = TTC.pf_process_xreal !!tc qenv p; }) (map_ss_inv1 f_b2xr event) in + + f_eHoareF pre f post + in + + let pt, ax = + PT.tc1_process_full_closed_pterm_cut + ~prcut:process_cut tc info in + + let hf = pf_as_ehoareF !!tc ax in + + FApi.t_last (FApi.t_try t_trivial) + (FApi.t_first + (EcLowGoal.Apply.t_apply_bwd_hi ~dpe:true pt) + (t_ehoare_deno { ehd_pre = ehf_pr hf; ehd_post = ehf_po hf; } tc)) diff --git a/src/phl/rules/ehoare/ecEHoareDeno.mli b/src/phl/rules/ehoare/ecEHoareDeno.mli new file mode 100644 index 000000000..f749d579e --- /dev/null +++ b/src/phl/rules/ehoare/ecEHoareDeno.mli @@ -0,0 +1,43 @@ +(* -------------------------------------------------------------------- *) +open EcParsetree +open EcCoreGoal.FApi +open EcAst + +(* ==================================================================== *) +(* Rules (trusted) *) + +type ehoare_deno = { + ehd_pre : ss_inv; (* P, in the memory &m of the judgement *) + ehd_post : ss_inv; (* Q, in the same memory *) +} + +(* [t_ehoare_deno { ehd_pre = P; ehd_post = Q }] — a probability bounded + by an expectation judgement on the procedure: + + ehoare [f : P ==> Q] + P[&m := &n, arg := args] <= d%xr + forall &m, E%xr <= Q + 0%r <= d + --------------------------------- + Pr[f(args) @ &n : E] <= d + + where, in the third premise, [&m] is the final memory of [f] and [E] + is read in it. Side conditions: the goal has the shape above; [P] and + [Q] are in the same memory [&m], which does not occur free in the goal + (otherwise fails). + + Node: [REHoareDeno { ehd_pre = P; ehd_post = Q }]. + Checker: "ehoare-deno". *) +val t_ehoare_deno : ehoare_deno -> backward + +(* ==================================================================== *) +(* Elaboration *) + +(* [byehoare pt] (resp. [byehoare (_ : P ==> Q)]) on + [Pr[f(args) @ &n : E] <= d]: the judgement [ehoare [f : P ==> Q]] is + the type of the proof term [pt] (resp. is cut, [P] and [Q] typed as + [xreal] in the memory of the event, [d%xr] and [E%xr] by default). + Applies [t_ehoare_deno], closes its first premise with [pt] (resp. + leaves it as the first goal) and tries [EcLowGoal.t_trivial] on its + last premise [0%r <= d] (left visible when not closed). *) +val process_ehoare_deno : deno_ppterm -> backward diff --git a/src/phl/rules/equiv/ecEquivDeno.ml b/src/phl/rules/equiv/ecEquivDeno.ml new file mode 100644 index 000000000..ec3d4a480 --- /dev/null +++ b/src/phl/rules/equiv/ecEquivDeno.ml @@ -0,0 +1,495 @@ +(* -------------------------------------------------------------------- *) +open EcUtils +open EcParsetree +open EcAst +open EcTypes +open EcFol +open EcEnv +open EcPV +open EcPhlPrRw +open EcHiGoal +open EcSubst + +open EcCoreGoal +open EcLowGoal +open EcLowPhlGoal +open EcCoreGoal.FApi + +module PT = EcProofTerm +module TTC = EcProofTyping + +(* -------------------------------------------------------------------- *) +(* Parameters of the equiv [deno] rule: the pre- and postcondition of the + judgement on the two procedures, in one pair of memories. Already + typed, nothing to resolve: the same record is the rule argument and the + node payload. *) +type equiv_deno = { + eqd_pre : ts_inv; (* P *) + eqd_post : ts_inv; (* Q *) +} + +type EcCoreGoal.rule += REquivDeno of equiv_deno + +(* -------------------------------------------------------------------- *) +(* The goals the rule applies to: [Pr[...] = Pr[...]] and + [Pr[...] <= Pr[...]]. *) +let destr_deno_goal (concl : form) = + match concl.f_node with + | Fapp ({f_node = Fop (op, _)}, [f1; f2]) when is_pr f1 && is_pr f2 -> + if EcPath.p_equal op EcCoreLib.CI_Bool.p_eq then Some (`Eq, destr_pr f1, destr_pr f2) + else if EcPath.p_equal op EcCoreLib.CI_Real.p_real_le then Some (`Le, destr_pr f1, destr_pr f2) + else None + + | _ -> None + +(* [P] and [Q] share their two memories, which are distinct and do not + occur free in the goal (they are bound around the events of the goal in + the third premise). *) +let valid_memories (concl : form) (n : equiv_deno) = + let { ml; mr } = n.eqd_pre in + EcIdent.id_equal ml n.eqd_post.ml + && EcIdent.id_equal mr n.eqd_post.mr + && not (EcIdent.id_equal ml mr) + && not (EcIdent.Mid.mem ml concl.f_fv) + && not (EcIdent.Mid.mem mr concl.f_fv) + +(* -------------------------------------------------------------------- *) +(* [P], with the arguments and the initial memories of [prl] and [prr]. *) +let cond_pre env prl prr pre = + let ml, mr = pre.ml, pre.mr in + let sargs = PVM.add env pv_arg ml prl.pr_args PVM.empty in + let sargs = PVM.add env pv_arg mr prr.pr_args sargs in + let smem = Fsubst.f_subst_id in + let smem = Fsubst.f_bind_mem smem ml prl.pr_mem in + let smem = Fsubst.f_bind_mem smem mr prr.pr_mem in + Fsubst.f_subst smem (PVM.subst env sargs pre.inv) + +(* -------------------------------------------------------------------- *) +(* Pure core shared by the rule and its checker. Its side conditions (the + shape of the goal and the memories of [P] and [Q]) are part of it, so + the checker re-validates them. *) +let equiv_deno_subgoals (hyps : LDecl.hyps) (concl : form) (n : equiv_deno) = + let env = LDecl.toenv hyps in + let cmp, prl, prr = + match destr_deno_goal concl with + | Some x -> x + | None -> failwith "equiv-deno: invalid goal shape" in + if not (valid_memories concl n) then + failwith "equiv-deno: invalid memories"; + let ml, mr = n.eqd_pre.ml, n.eqd_pre.mr in + let concl_e = f_equivF n.eqd_pre prl.pr_fun prr.pr_fun n.eqd_post in + let funl = Fun.by_xpath prl.pr_fun env in + let funr = Fun.by_xpath prr.pr_fun env in + + let concl_pr = cond_pre env prl prr n.eqd_pre in + + (* Q relates the two events, in every pair of final memories *) + let evl = ss_inv_generalize_as_left prl.pr_event ml mr in + let evr = ss_inv_generalize_as_right prr.pr_event ml mr in + let cmp = + match cmp with + | `Eq -> map_ts_inv2 f_iff evl evr + | `Le -> map_ts_inv2 f_imp evl evr in + let mel = Fun.actmem_post ml funl in + let mer = Fun.actmem_post mr funr in + let concl_po = + f_forall_mems_ts_inv mel mer (map_ts_inv2 f_imp n.eqd_post cmp) in + + [concl_e; concl_pr; concl_po] + +(* -------------------------------------------------------------------- *) +(* Rule (TCB). *) +let t_equiv_deno (r : equiv_deno) (tc : tcenv1) = + let concl = FApi.tc1_goal tc in + if Option.is_none (destr_deno_goal concl) then + tc_error !!tc "invalid goal shape"; + if not (valid_memories concl r) then + tc_error !!tc "invalid memories for the equivalence judgement"; + FApi.xrule1 tc (REquivDeno r) + (equiv_deno_subgoals (FApi.tc1_hyps tc) concl r) + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | REquivDeno n -> + Some (EcPlRecheck.checker_of "equiv-deno" (fun _ concl -> concl) + (fun hyps concl -> equiv_deno_subgoals hyps concl n)) + | _ -> None) + +(* ==================================================================== *) +(* Derived (no proof-node): the upto-bad forms, from the rule and the + lemmas of [Real] on probabilities. + + TEMPORARY: the probability rewritings still come from the + not-yet-migrated [EcPhlPrRw]. *) +let real_le_trans = EcCoreLib.CI_Real.real_order_lemma "ler_trans" +let real_ler_add = EcCoreLib.CI_Real.real_order_lemma "ler_add" +let real_eq_le = EcCoreLib.CI_Real.real_order_lemma "lerr_eq" +let real_upto = EcCoreLib.CI_Real.real_lemma "upto2_abs" +let real_upto_notbad = EcCoreLib.CI_Real.real_lemma "upto2_notbad" +let real_upto_imp_bad = EcCoreLib.CI_Real.real_lemma "upto2_imp_bad" +let real_upto_false = EcCoreLib.CI_Real.real_lemma "upto_bad_false" +let real_upto_or = EcCoreLib.CI_Real.real_lemma "upto_bad_or" +let real_upto_sub = EcCoreLib.CI_Real.real_lemma "upto_bad_sub" + +(* -------------------------------------------------------------------- *) +let t_real_le_trans f2 tc = + t_apply_prept (`App (`UG real_le_trans, [`F f2])) tc + +(* -------------------------------------------------------------------- *) +(* [Pr[f1 @ &1 : E1] <= Pr[f2 @ &2 : E2] + Pr[f2 @ &2 : B]], [f2] the + same procedure in the last two probabilities. *) +let destr_deno_bad env f = + try + let fpr1, (fpr2, fpr3) = snd_map DestrReal.add (DestrReal.le f) in + let _, pr2, pr3 = t3_map destr_pr (fpr1, fpr2, fpr3) in + + if not (NormMp.x_equal env pr2.pr_fun pr3.pr_fun) then + raise (DestrError ""); + (fpr1, fpr2, fpr3) + + with DestrError _ -> raise (DestrError "destr_deno_bad") + +(* -------------------------------------------------------------------- *) +let tc_destr_deno_bad tc env f = + try destr_deno_bad env f + with DestrError _ -> tc_error !!tc "invalid goal shape" + +(* -------------------------------------------------------------------- *) +(* [0%r <= Pr[...]] *) +let t_pr_pos tc = + let pr = + try + let _, fpr = DestrReal.le (tc1_goal tc) in + destr_pr fpr + with DestrError _ -> tc_error !!tc "invalid goal shape" in + let prf = f_pr_r { pr with pr_event = { m = pr.pr_event.m; inv = f_false; }; } in + (t_real_le_trans prf @+ + [ t_pr_rewrite ("mu_false", None) @! t_true; + t_pr_rewrite ("mu_sub", None) @! t_true]) tc + +(* -------------------------------------------------------------------- *) +let t_equiv_deno_bad pre tc = + let env, _hyps, concl = FApi.tc1_eflat tc in + let fpr1, fpr2, fprb = tc_destr_deno_bad tc env concl in + let pr1 = destr_pr fpr1 and pr2 = destr_pr fpr2 and prb = destr_pr fprb in + if not (pr2.pr_mem = prb.pr_mem) then + tc_error !!tc "invalid goal shape"; + let m = prb.pr_event.m in + let ev2 = ss_inv_rebind pr2.pr_event m in + let fand = map_ss_inv2 f_and ev2 (map_ss_inv1 f_not prb.pr_event) in + let pro = f_pr pr2.pr_mem pr2.pr_fun pr2.pr_args (map_ss_inv2 f_or fand prb.pr_event) in + let pra = f_pr pr2.pr_mem pr2.pr_fun pr2.pr_args fand in + let t_false tc = t_apply_prept (`UG real_upto_false) tc in + let ml, mr = pre.ml, pre.mr in + let post = + let ev1 = ss_inv_generalize_as_left pr1.pr_event ml mr in + let ev2 = ss_inv_generalize_as_right ev2 ml mr in + let bad2 = ss_inv_generalize_as_right prb.pr_event ml mr in + map_ts_inv2 f_imp (map_ts_inv1 f_not bad2) (map_ts_inv2 f_imp ev1 ev2) in + + (t_real_le_trans pro @+ + [t_equiv_deno { eqd_pre = pre; eqd_post = post; } @+ [ + t_id; + t_id; + t_intros_s (`Symbol ["_";"_"]) @! t_apply_prept (`UG real_upto_or) ]; + t_pr_rewrite_i ("mu_disjoint", None) @+ + [ t_intro_s (`Symbol "_") @! t_false; + t_apply_prept + (`App (`UG real_ler_add, [`F pra;`F fpr2;`F fprb;`F fprb; `H_; `H_])) + @+ [ + t_pr_rewrite_i ("mu_sub",None) @+ [ + t_intros_s (`Symbol ["_"]) @! t_apply_prept (`UG real_upto_sub); + t_trivial; + ]; + t_true; + ] + ] + ]) tc + +(* -------------------------------------------------------------------- *) +(* [`|Pr[f1 @ &1 : E1] - Pr[f2 @ &2 : E2]| <= Pr[f2 @ &2 : B]], [f2] the + same procedure in the last two probabilities. *) +let destr_deno_bad2 env f = + try + let lhs , rhs = DestrReal.le f in + let fpr1, fpr2 = DestrReal.sub (DestrReal.abs lhs) in + let _pr1, pr2, prb = t3_map destr_pr (fpr1, fpr2, rhs) in + if not (NormMp.x_equal env pr2.pr_fun prb.pr_fun) then + raise (DestrError "pr"); + (fpr1, fpr2, rhs) + with DestrError _ -> raise (DestrError "destr_deno_bad2") + +(* -------------------------------------------------------------------- *) +let tc_destr_deno_bad2 tc env f = + try destr_deno_bad2 env f + with DestrError _ -> tc_error !!tc "invalid goal shape" + +(* -------------------------------------------------------------------- *) +let t_equiv_deno_bad2 pre bad1 tc = + let ml, mr = pre.ml, pre.mr in + let env, hyps, concl = FApi.tc1_eflat tc in + let fpr1, fpr2, fprb = tc_destr_deno_bad2 tc env concl in + let pr1 = destr_pr fpr1 and pr2 = destr_pr fpr2 and + prb = destr_pr fprb in + if not (pr2.pr_mem = prb.pr_mem) then + tc_error !!tc "invalid goal shape"; + let f1 = pr1.pr_fun and f2 = pr2.pr_fun in + let ev1 = pr1.pr_event and ev2 = pr2.pr_event in + let ev1 = ss_inv_rebind ev1 bad1.m in + let bad2 = prb.pr_event in + let bad2 = ss_inv_rebind bad2 ev2.m in + let post = + let bad1 = ss_inv_generalize_as_left bad1 ml mr in + let ev1 = ss_inv_generalize_as_left ev1 ml mr in + let bad2 = ss_inv_generalize_as_right bad2 ml mr in + let ev2 = ss_inv_generalize_as_right ev2 ml mr in + map_ts_inv2 f_and (map_ts_inv2 f_iff bad1 bad2) + (map_ts_inv2 f_imp (map_ts_inv1 f_not bad2) (map_ts_inv2 f_iff ev1 ev2)) in + let equiv = f_equivF pre f1 f2 post in + let cpre = cond_pre env pr1 pr2 pre in + let fpreb1 = f_pr pr1.pr_mem pr1.pr_fun pr1.pr_args (map_ss_inv2 f_and ev1 bad1) in + let fpren1 = f_pr pr1.pr_mem pr1.pr_fun pr1.pr_args (map_ss_inv2 f_and ev1 (map_ss_inv1 f_not bad1)) in + let fpreb2 = f_pr pr2.pr_mem pr2.pr_fun pr2.pr_args (map_ss_inv2 f_and ev2 bad2) in + let fpren2 = f_pr pr2.pr_mem pr2.pr_fun pr2.pr_args (map_ss_inv2 f_and ev2 (map_ss_inv1 f_not bad2)) in + let fabs' = + f_real_abs + (f_real_sub (f_real_add fpreb1 fpren1) (f_real_add fpreb2 fpren2)) in + let t_deno = t_equiv_deno { eqd_pre = pre; eqd_post = post; } in + let hequiv,hcpre = as_seq2 (EcEnv.LDecl.fresh_ids hyps ["_";"_"]) in + (t_cut equiv @+ + [ t_id; + t_cut cpre @+ + [ t_id; + t_intros_i [hcpre; hequiv] @! + t_real_le_trans fabs' @+ + [ t_apply_prept (`UG real_eq_le) @! + (process_congr PCongrDefault) @! (* abs *) + (process_congr PCongrDefault) @~ (* add *) + (t_last (process_congr PCongrDefault)) @~+ (* opp *) + [ t_pr_rewrite_i ("mu_split", Some bad1) @! t_reflex; + t_pr_rewrite_i ("mu_split", Some bad2) @! t_reflex ] ; + t_apply_prept (`UG real_upto) @+ + [ t_pr_pos; + t_pr_pos; + t_deno @+ [ + t_apply_hyp hequiv; + t_apply_hyp hcpre; + t_intros_s (`Symbol ["_"; "_"]) @! + t_apply_prept (`UG real_upto_imp_bad) ]; + t_pr_rewrite ("mu_sub",None) @! t_trivial; + t_deno @+ [ + t_apply_hyp hequiv; + t_apply_hyp hcpre; + t_intros_s (`Symbol ["_"; "_"]) @! + t_apply_prept (`UG real_upto_notbad) + ]; + ] + ] + ] + ]) tc + +(* ==================================================================== *) +(* Elaboration. *) + +(* The default precondition: the equalities of the globals read by the two + procedures (for the variables the postcondition reads) and of their + arguments with those of the goal. *) +let process_pre tc hyps prl prr pre post = + let fl = prl.pr_fun and fr = prr.pr_fun in + let ml, mr = post.ml, post.mr in + match pre with + | Some p -> + let penv, _ = LDecl.equivF ml mr fl fr hyps in + { ml; mr; inv = TTC.pf_process_formula !!tc penv p; } + | None -> + let al = prl.pr_args and ar = prr.pr_args in + let pml = prl.pr_mem and pmr = prr.pr_mem in + + let env = LDecl.toenv hyps in + let eqs = ref [] in + let push f = eqs := f :: !eqs in + + let dopv m mi gen_o x ty = + if is_glob x then push (gen_o (map_ss_inv1 (fun f -> f_eq f (f_pvar x ty mi).inv) (f_pvar x ty m))) in + + let doglob m mi gen_o g = push (gen_o ((map_ss_inv1 (fun f -> f_eq f (NormMp.norm_glob env mi g).inv)) (NormMp.norm_glob env m g))) in + let dof f a m mi gen_o = + try + let fv = PV.remove env pv_res (PV.fv env m post.inv) in + PV.iter (dopv m mi gen_o) (doglob m mi gen_o) (eqobs_inF_refl env f fv); + if not (EcReduction.EqTest.for_type env a.f_ty tunit) then + push (map_ts_inv1 (fun f -> f_eq f a) (gen_o (f_pvarg a.f_ty m))) + with EcCoreGoal.TcError _ | EqObsInError -> () in + + let gen_r f = ss_inv_generalize_right f mr in + let gen_l f = ss_inv_generalize_left f ml in + dof fl al ml pml gen_r; dof fr ar mr pmr gen_l; + map_ts_inv ~ml ~mr f_ands !eqs + +(* -------------------------------------------------------------------- *) +(* The default postcondition of an equality: [E1 <=> E2], or the + equalities of the variables it needs when [eq]. *) +let post_iff ml mr eq env evl evr = + let post = map_ts_inv2 f_iff evl evr in + try + if not eq then raise Not_found; + { ml; mr; inv = Mpv2.to_form (Mpv2.needed_eq env post) ml mr f_true; } + with Not_found -> post + +(* -------------------------------------------------------------------- *) +let process_equiv_deno1 info eq tc = + let process_cut (pre, post) = + let env, hyps, concl = FApi.tc1_eflat tc in + + let op, f1, f2 = + match concl.f_node with + | Fapp ({f_node = Fop (op, _)}, [f1; f2]) when is_pr f1 && is_pr f2 -> + (op, f1, f2) + + | _ -> tc_error !!tc "invalid goal shape" + in + + let ml , mr = EcIdent.create "&1", EcIdent.create "&2" in + + let { pr_fun = fl } as prl = destr_pr f1 in + let evl = ss_inv_generalize_as_left prl.pr_event ml mr in + let { pr_fun = fr } as prr = destr_pr f2 in + let evr = ss_inv_generalize_as_right prr.pr_event ml mr in + + let post = + match post with + | Some p -> + let _, qenv = LDecl.equivF ml mr fl fr hyps in + { ml; mr; inv = TTC.pf_process_formula !!tc qenv p; } + | None -> + match op with + | _ when EcPath.p_equal op EcCoreLib.CI_Bool.p_eq -> + (post_iff ml mr eq env evl evr) + | _ when EcPath.p_equal op EcCoreLib.CI_Real.p_real_le -> + map_ts_inv2 f_imp evl evr + | _ -> + tc_error !!tc "not able to reconize a comparison operator" in + + let pre = process_pre tc hyps prl prr pre post in + + f_equivF pre fl fr post + in + + let pt, ax = + PT.tc1_process_full_closed_pterm_cut + ~prcut:process_cut tc info in + + let ef = pf_as_equivF !!tc ax in + + FApi.t_first + (EcLowGoal.Apply.t_apply_bwd_hi ~dpe:true pt) + (t_equiv_deno { eqd_pre = ef_pr ef; eqd_post = ef_po ef; } tc) + +(* -------------------------------------------------------------------- *) +(* The judgement is applied, or used through the consequence rule when it + does not match; the goals are rotated so that those of the judgement + come first. + + TEMPORARY: the consequence rule still comes from the not-yet-migrated + [EcPhlConseq]. *) +let t_deno_bad_sub pt (equiv : equivF) (t_bad : backward) (tc : tcenv1) = + let torotate = ref 1 in + let t_sub = + FApi.t_or (EcLowGoal.Apply.t_apply_bwd_hi ~dpe:true pt) + (EcPhlConseq.t_equivF_conseq (ef_pr equiv) (ef_po equiv) @+ + [t_true; (fun tc -> incr torotate; t_id tc); + EcLowGoal.Apply.t_apply_bwd_hi ~dpe:true pt]) in + let gs = t_last t_sub (t_rotate `Left 1 (t_bad tc)) in + t_rotate `Left !torotate gs + +(* -------------------------------------------------------------------- *) +let process_equiv_deno_bad info tc = + let process_cut (pre, post) = + let env, hyps, concl = FApi.tc1_eflat tc in + let fpr1, fpr2, fprb = tc_destr_deno_bad tc env concl in + + let { pr_fun = fl ; pr_event = evl } as prl = destr_pr fpr1 in + let { pr_fun = fr ; pr_event = evr } as prr = destr_pr fpr2 in + + let ml , mr = EcIdent.create "&1", EcIdent.create "&2" in + + let post = + match post with + | Some p -> + let _, qenv = LDecl.equivF ml mr fl fr hyps in + { ml; mr; inv = TTC.pf_process_formula !!tc qenv p; } + | None -> + let evl = ss_inv_generalize_as_left evl ml mr in + let evr = ss_inv_generalize_as_right evr ml mr in + let bad = ss_inv_generalize_as_right (destr_pr fprb).pr_event ml mr in + let f_imps' l = f_imps (List.tl l) (List.hd l) in + map_ts_inv f_imps' [evr; map_ts_inv1 f_not bad; evl] in + let pre = process_pre tc hyps prl prr pre post in + + f_equivF pre fl fr post + in + + let pt, ax = + PT.tc1_process_full_closed_pterm_cut + ~prcut:process_cut tc info in + + let equiv = pf_as_equivF !!tc ax in + + t_deno_bad_sub pt equiv (t_equiv_deno_bad (ef_pr equiv)) tc + +(* -------------------------------------------------------------------- *) +let process_equiv_deno_bad2 info eq bad1 tc = + let env, hyps, concl = FApi.tc1_eflat tc in + let fpr1, fpr2, fprb = tc_destr_deno_bad2 tc env concl in + + let { pr_fun = fl; pr_mem = ml ; pr_event = evl } as prl = destr_pr fpr1 in + let { pr_fun = fr; pr_event = evr } as prr = destr_pr fpr2 in + + let ml' , mr' = EcIdent.create "&1", EcIdent.create "&2" in + + let bad1 = + let _, qenv = LDecl.hoareF ml fl hyps in + { m = ml; inv = TTC.pf_process_formula !!tc qenv bad1; } in + + let process_cut (pre, post) = + + let post = + match post with + | Some p -> + let _, qenv = LDecl.equivF ml' mr' fl fr hyps in + { ml = ml'; mr = mr'; inv = TTC.pf_process_formula !!tc qenv p; } + | None -> + let evl = ss_inv_generalize_as_left evl ml' mr' in + let evr = ss_inv_generalize_as_right evr ml' mr' in + let bad1 = ss_inv_generalize_as_left bad1 ml' mr' in + let bad2 = ss_inv_generalize_as_right (destr_pr fprb).pr_event ml' mr' in + let iff = post_iff ml' mr' eq env evl evr in + map_ts_inv2 f_and (map_ts_inv2 f_iff bad1 bad2) (map_ts_inv2 f_imp (map_ts_inv1 f_not bad2) iff) in + + let pre = process_pre tc hyps prl prr pre post in + + f_equivF pre fl fr post + in + + let pt, ax = + PT.tc1_process_full_closed_pterm_cut + ~prcut:process_cut tc info in + + let equiv = pf_as_equivF !!tc ax in + + t_deno_bad_sub pt equiv (t_equiv_deno_bad2 (ef_pr equiv) bad1) tc + +(* -------------------------------------------------------------------- *) +let process_equiv_deno ((info, eq, bad1) : deno_ppterm * bool * pformula option) tc = + match bad1 with + | Some bad1 -> + process_equiv_deno_bad2 info eq bad1 tc + + | None -> + let env, _hyps, concl = FApi.tc1_eflat tc in + try ignore (destr_deno_bad env concl); + process_equiv_deno_bad info tc + with DestrError _ -> + process_equiv_deno1 info eq tc diff --git a/src/phl/rules/equiv/ecEquivDeno.mli b/src/phl/rules/equiv/ecEquivDeno.mli new file mode 100644 index 000000000..925ceeba8 --- /dev/null +++ b/src/phl/rules/equiv/ecEquivDeno.mli @@ -0,0 +1,101 @@ +(* -------------------------------------------------------------------- *) +open EcParsetree +open EcCoreGoal.FApi +open EcAst + +(* ==================================================================== *) +(* Rules (trusted) *) + +type equiv_deno = { + eqd_pre : ts_inv; (* P, in the memories &1 &2 of the judgement *) + eqd_post : ts_inv; (* Q, in the same memories *) +} + +(* [t_equiv_deno { eqd_pre = P; eqd_post = Q }] — two probabilities + compared through an equivalence of the two procedures, with [~] the + goal's comparison: + + equiv [f1 ~ f2 : P ==> Q] + P[&1 := &n1, &2 := &n2, arg{1} := args1, arg{2} := args2] + forall &1 &2, Q => (E1{1} [=>] E2{2}) + --------------------------------------------------------- + Pr[f1(args1) @ &n1 : E1] [~] Pr[f2(args2) @ &n2 : E2] + + where [~] is [=] or [<=], and [E1 [=>] E2] is [E1 <=> E2] for [=] and + [E1 => E2] for [<=]; in the third premise, [&1] and [&2] are the final + memories of [f1] and [f2], [E1] (resp. [E2]) read in [&1] (resp. + [&2]). Side conditions: the goal has one of the two shapes above; [P] + and [Q] are in the same memories [&1] and [&2], which are distinct and + do not occur free in the goal (otherwise fails). + + Node: [REquivDeno { eqd_pre = P; eqd_post = Q }]. + Checker: "equiv-deno". *) +val t_equiv_deno : equiv_deno -> backward + +(* ==================================================================== *) +(* Derived tactics *) + +(* [t_equiv_deno_bad P] — on + [Pr[f1(args1) @ &n1 : E1] <= Pr[f2(args2) @ &n2 : E2] + + Pr[f2(args2) @ &n2 : B]] + (the same procedure, arguments and memory in the last two + probabilities, otherwise fails), with + [Q = !B{2} => E1{1} => E2{2}]: + 1. transitivity ([ler_trans]) through + [Pr[f2(args2) @ &n2 : (E2 /\ !B) \/ B]]; + 2. on the first side, [t_equiv_deno { eqd_pre = P; eqd_post = Q }], + whose third premise is closed with [upto_bad_or]; + 3. on the second side, [mu_disjoint], [ler_add], [mu_sub] and the + lemmas [upto_bad_false], [upto_bad_sub], closed on the spot (by + [EcLowGoal.t_trivial] for the inclusion of the events). + Visible goals: the first two premises of [t_equiv_deno], in this + order. Emits no node of its own. *) +val t_equiv_deno_bad : ts_inv -> backward + +(* [t_equiv_deno_bad2 P B1] — on + [`|Pr[f1(args1) @ &n1 : E1] - Pr[f2(args2) @ &n2 : E2]| + <= Pr[f2(args2) @ &n2 : B2]] + (the same procedure, arguments and memory in the last two + probabilities, otherwise fails), [B1] an event of [f1], with + [Q = (B1{1} <=> B2{2}) /\ (!B2{2} => (E1{1} <=> E2{2}))]: + 1. cuts [equiv [f1 ~ f2 : P ==> Q]] and the precondition (first + premise of [t_equiv_deno]), and introduces them; + 2. splits each probability along [B1] (resp. [B2]) with [mu_split], + [lerr_eq] and congruence, then applies [upto2_abs], whose premises + are closed: positivity of probabilities ([mu_false], [mu_sub]), + [t_equiv_deno { eqd_pre = P; eqd_post = Q }] twice (premises + closed by the cut hypotheses and [upto2_imp_bad], resp. + [upto2_notbad]) and [mu_sub]. + Visible goals: the judgement, then the precondition. Emits no node of + its own. *) +val t_equiv_deno_bad2 : ts_inv -> ss_inv -> backward + +(* ==================================================================== *) +(* Elaboration *) + +(* [byequiv pt] (resp. [byequiv (_ : P ==> Q)]), with an optional [eq] + flag ([byequiv =>]) and an optional bad event [: B1], on a goal + relating two probabilities; the judgement is the type of the proof + term [pt] (resp. is cut, [P] and [Q] typed in the memories [&1] and + [&2]); by default, [P] equates the globals the procedures read (for the + variables [Q] reads) and their arguments with those of the goal: + - with [: B1], on [`|Pr[...] - Pr[...]| <= Pr[...]]: by default + [Q = (B1{1} <=> B{2}) /\ (!B{2} => (E1{1} <=> E2{2}))], the last + equivalence replaced by the equalities of the variables it needs + with [eq]. Applies [t_equiv_deno_bad2]; + - on [Pr[...] <= Pr[...] + Pr[...]]: by default + [Q = !B{2} => E1{1} => E2{2}]. Applies [t_equiv_deno_bad]; + - otherwise, on [Pr[...] = Pr[...]] or [Pr[...] <= Pr[...]]: by + default [Q = E1{1} <=> E2{2}] (or the equalities of the variables it + needs with [eq]), resp. [Q = E1{1} => E2{2}]. Applies + [t_equiv_deno]. + The judgement premise is closed with [pt] (resp. left as the first + goal). For the upto-bad forms, when the judgement does not match the + one the derived tactic needs (e.g. a default postcondition with + [eq]), it is used through the consequence rule + ([EcPhlConseq.t_equivF_conseq], with the judgement's own + precondition): the implication of the preconditions is closed by + [EcLowGoal.t_true] (the tactic fails otherwise), that of the + postconditions is left as the last goal. *) +val process_equiv_deno : + deno_ppterm * bool * pformula option -> backward diff --git a/tests/deno.ec b/tests/deno.ec new file mode 100644 index 000000000..e323c4635 --- /dev/null +++ b/tests/deno.ec @@ -0,0 +1,232 @@ +require import AllCore Distr DBool Xreal. + +module M = { + var g : int + var bad : bool + + proc f(x : int) : int = { + g <- x; + return x; + } + + proc h() : bool = { + var y; + y <$ {0,1}; + return y; + } + + proc u() : bool = { + var y; + bad <- false; + y <$ {0,1}; + if (y) { bad <- true; } + return y; + } + + proc v() : bool = { + var y; + bad <- false; + y <$ {0,1}; + if (y) { bad <- true; y <- false; } + return y; + } +}. + +(* -------------------------------------------------------------------- *) +(* [byphoare]: each comparison, both orientations, cut and proof term. *) + +lemma bdhoare_le &m : Pr[M.h() @ &m : res] <= 1%r / 2%r. +proof. +byphoare (_: true ==> res)=> //. +by proc; rnd; auto=> />; smt(dboolE). +qed. + +lemma bdhoare_ge &m : 1%r / 2%r <= Pr[M.h() @ &m : res]. +proof. +byphoare=> //. +by proc; rnd; auto=> />; smt(dboolE). +qed. + +lemma bdhoare_eq &m : Pr[M.h() @ &m : res] = 1%r / 2%r. +proof. +byphoare=> //. +by proc; rnd; auto=> />; smt(dboolE). +qed. + +lemma bdhoare_eq_sym &m : 1%r / 2%r = Pr[M.h() @ &m : res]. +proof. +byphoare=> //. +by proc; rnd; auto=> />; smt(dboolE). +qed. + +lemma h_half : phoare [M.h : true ==> res] = (1%r / 2%r). +proof. by proc; rnd; auto=> />; smt(dboolE). qed. + +lemma bdhoare_pterm &m : Pr[M.h() @ &m : res] = 1%r / 2%r. +proof. by byphoare h_half. qed. + +lemma bdhoare_pterm_sym &m : 1%r / 2%r = Pr[M.h() @ &m : res]. +proof. by byphoare h_half. qed. + +lemma bdhoare_args &m (a : int) : Pr[M.f(a) @ &m : res = a /\ M.g = a] = 1%r. +proof. +byphoare (_: arg = a ==> res = a /\ M.g = a)=> //. +by proc; auto. +qed. + +lemma bdhoare_errors &m : Pr[M.h() @ &m : res] < 1%r. +proof. +fail byphoare. +fail byphoare h_half. +abort. + +lemma bdhoare_errors_noprob (x : real) : x = x. +proof. +fail byphoare. +abort. + +(* -------------------------------------------------------------------- *) +(* [byehoare]: default and explicit cut, proof term, errors. *) + +lemma ehoare_default &m : Pr[M.h() @ &m : res] <= 1%r. +proof. +byehoare=> //. +proc; auto=> &hr /=. +by rewrite Ep_dbool /#. +qed. + +lemma ehoare_cut &m (a : int) : Pr[M.f(a) @ &m : res = a] <= 1%r. +proof. +byehoare (_: (arg = a)%xr ==> (res = a)%xr)=> //. +by proc; auto. +qed. + +lemma h_ehoare : ehoare [M.h : 1%xr ==> res%xr]. +proof. proc; auto=> &hr /=; by rewrite Ep_dbool /#. qed. + +lemma ehoare_pterm &m : Pr[M.h() @ &m : res] <= 1%r. +proof. by byehoare h_ehoare. qed. + +lemma ehoare_errors &m : 1%r <= Pr[M.h() @ &m : res]. +proof. +fail byehoare. +fail byehoare h_ehoare. +abort. + +(* -------------------------------------------------------------------- *) +(* [byequiv]: equality (with and without [eq]), inequality, pterm. *) + +lemma equiv_eq &m : Pr[M.f(1) @ &m : res = 1] = Pr[M.f(1) @ &m : res = 1]. +proof. +byequiv=> //. +by proc; auto. +qed. + +lemma equiv_eq_noeq &m : Pr[M.h() @ &m : res] = Pr[M.h() @ &m : res]. +proof. +byequiv [-eq]=> //. +by proc; auto. +qed. + +lemma equiv_le &m : Pr[M.u() @ &m : res] <= Pr[M.h() @ &m : res]. +proof. +byequiv (_: true ==> res{1} => res{2})=> //. +by proc; wp; rnd; auto=> /#. +qed. + +lemma equiv_default_le &m : Pr[M.u() @ &m : res] <= Pr[M.h() @ &m : res]. +proof. +byequiv=> //. +by proc; wp; rnd; auto=> /#. +qed. + +lemma equiv_args &m (a : int) : + Pr[M.f(a) @ &m : res = a] = Pr[M.f(a) @ &m : M.g = a]. +proof. +byequiv (_: ={arg} /\ arg{1} = a ==> res{1} = a <=> M.g{2} = a)=> //. +by proc; auto. +qed. + +lemma uh : equiv [M.u ~ M.h : true ==> ={res}]. +proof. by proc; wp; rnd; auto. qed. + +lemma equiv_pterm &m : Pr[M.u() @ &m : res] = Pr[M.h() @ &m : res]. +proof. by byequiv uh. qed. + +lemma equiv_errors &m : Pr[M.u() @ &m : res] < Pr[M.h() @ &m : res]. +proof. +fail byequiv. +fail byequiv uh. +abort. + +lemma equiv_errors_shape &m : Pr[M.u() @ &m : res] <= 1%r. +proof. +fail byequiv. +fail byequiv uh. +abort. + +(* -------------------------------------------------------------------- *) +(* [byequiv] upto bad: [Pr[..] <= Pr[..] + Pr[..: bad]] and *) +(* [`|Pr[..] - Pr[..]| <= Pr[..: bad]] (with [: bad1]). *) + +lemma equiv_bad &m : + Pr[M.u() @ &m : res] <= Pr[M.v() @ &m : res] + Pr[M.v() @ &m : M.bad]. +proof. +byequiv=> //. +proc; seq 2 2 : (={y} /\ !M.bad{2}); 1: by auto. +by if; auto=> /#. +qed. + +lemma equiv_bad_cut &m : + Pr[M.u() @ &m : res] <= Pr[M.v() @ &m : res] + Pr[M.v() @ &m : M.bad]. +proof. +byequiv (_: true ==> !M.bad{2} => res{1} => res{2})=> //. +proc; seq 2 2 : (={y} /\ !M.bad{2}); 1: by auto. +by if; auto=> /#. +qed. + +lemma uv : equiv [M.u ~ M.v : true ==> M.bad{1} = M.bad{2} /\ (!M.bad{2} => ={res})]. +proof. +proc; seq 2 2 : (={y} /\ !M.bad{1} /\ !M.bad{2}); 1: by auto. +by if; auto=> /#. +qed. + +lemma equiv_bad_pterm &m : + Pr[M.u() @ &m : res] <= Pr[M.v() @ &m : res] + Pr[M.v() @ &m : M.bad]. +proof. +(* the proof term does not match: through the consequence rule *) +byequiv uv=> //. +by move=> &1 &2 /#. +qed. + +lemma equiv_bad2 &m : + `|Pr[M.u() @ &m : res] - Pr[M.v() @ &m : res]| <= Pr[M.v() @ &m : M.bad]. +proof. +(* with [eq], the default judgement does not match the rule's: through + the consequence rule *) +byequiv : M.bad=> //. ++ proc; seq 2 2 : (={y} /\ !M.bad{1} /\ !M.bad{2}); 1: by auto. + by if; auto=> /#. +by move=> &1 &2 /#. +qed. + +lemma equiv_bad2_noeq &m : + `|Pr[M.u() @ &m : res] - Pr[M.v() @ &m : res]| <= Pr[M.v() @ &m : M.bad]. +proof. +byequiv [-eq] : M.bad=> //. +proc; seq 2 2 : (={y} /\ !M.bad{1} /\ !M.bad{2}); 1: by auto. +by if; auto=> /#. +qed. + +lemma equiv_bad2_pterm &m : + `|Pr[M.u() @ &m : res] - Pr[M.v() @ &m : res]| <= Pr[M.v() @ &m : M.bad]. +proof. +byequiv uv : M.bad=> //. +by move=> &1 &2 /#. +qed. + +lemma equiv_bad2_errors &m : + `|Pr[M.u() @ &m : res] - Pr[M.v() @ &m : res]| <= Pr[M.u() @ &m : M.bad]. +proof. +fail byequiv : M.bad. +abort.