From d00f51394102db50359dfc325ff4f276ac453620 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Fri, 9 Oct 2026 09:44:11 +0200 Subject: [PATCH] refactor(pl): prrw as a recheckable rule PR of the program-logic reorganization stack (see src/phl/REFACTORING.md). It migrates the `prrw` tactic class (`rewrite Pr`): - new module src/phl/rules/bdhoare/EcBdHoarePrFact: the axiom schema of the facts on the probabilities of one procedure (mu_eq, mu_sub, mu_false, mu_not, mu_or, mu_disjoint, mu_split, mu_ge0, mu_le1, muE, mu1_le_eq_mu1, mu_has_le) as the trusted rule t_bdhoare_pr_fact, without premise; its node RBdHoarePrFact records the schema and its resolved parameters (procedure, arguments, initial memory, events, and the binders the fact introduces, so that the fact is a deterministic function of the node), checker "bdhoare-pr-fact". The pure core regenerates the fact, rechecks the side conditions of the schema (events in one memory, the value of mu1_le_eq_mu1 and the list of mu_has_le independent of the memory of the event, the binders not captured) and compares it with the goal; this replaces the opaque `` `RwPr `` node closing the cut of the fact; - the facts are statements on the probability of an event of one procedure, the object of the phoare logic (mu1_le_eq_mu1 has a phoare premise), hence the module lives in rules/bdhoare/, as byphoare and fel do; - `rewrite Pr` is derived (t_pr_rewrite, process_pr_rewrite): it selects the probability, resolves the parameters and rewrites with the cut fact, closed on the spot by the rule; - byupto (EcEquivUpto) and byequiv (EcEquivDeno) call the new module; their TEMPORARY dependencies on EcPhlPrRw are dropped; - EcPhlPrRw reduced to the legacy entry points, interface unchanged. Behaviour is preserved: the same facts are generated, hence the same goals, with the same error messages in the same order (compared with the reference build on every error path of the new test). Validation: new test tests/pr-rewrite.ec (every lemma, both disjunctions, and every error path) passes with the reference build and this one under EC_RECHECK=1, as do the examples using `rewrite Pr`, byupto or byequiv with a bad event; stdlib and unit pass under EC_RECHECK=1 with no RecheckFailure. The checker, when broken, is caught only under EC_RECHECK=1 (stdlib: 19 files; unit: 4 files, tests/pr-rewrite.ec, tests/rw_mu_has_le.ec, tests/deno.ec and tests/upto.ec). --- src/phl/README.md | 3 + src/phl/REFACTORING.md | 8 + src/phl/ecPhlPrRw.ml | 358 +---------------- src/phl/rules/bdhoare/ecBdHoarePrFact.ml | 461 ++++++++++++++++++++++ src/phl/rules/bdhoare/ecBdHoarePrFact.mli | 106 +++++ src/phl/rules/equiv/ecEquivDeno.ml | 21 +- src/phl/rules/equiv/ecEquivDeno.mli | 7 +- src/phl/rules/equiv/ecEquivUpto.ml | 10 +- src/phl/rules/equiv/ecEquivUpto.mli | 5 +- tests/pr-rewrite.ec | 174 ++++++++ 10 files changed, 776 insertions(+), 377 deletions(-) create mode 100644 src/phl/rules/bdhoare/ecBdHoarePrFact.ml create mode 100644 src/phl/rules/bdhoare/ecBdHoarePrFact.mli create mode 100644 tests/pr-rewrite.ec diff --git a/src/phl/README.md b/src/phl/README.md index f70c495c3..562fd8486 100644 --- a/src/phl/README.md +++ b/src/phl/README.md @@ -168,5 +168,8 @@ src/phl/ - The upto rule of `byupto` (`EcEquivUpto`, a premise-free rule concluding `Pr[f1 : E /\ !bad] = Pr[f2 : E /\ !bad]` for procedures equal up to `bad`) is relational: it lives in `rules/equiv/`. +- The facts on probabilities of `rewrite Pr` (`EcBdHoarePrFact`, a + premise-free axiom schema on the probabilities of one procedure) live + in `rules/bdhoare/`; `rewrite Pr` itself is derived. - 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 8f09c5d28..d644e6dfb 100644 --- a/src/phl/REFACTORING.md +++ b/src/phl/REFACTORING.md @@ -197,6 +197,14 @@ uniform across logics or relate several judgements: equality of probabilities of two procedures, is relational and lives in `rules/equiv/`; the forms of `byupto` other than `Pr[_] = Pr[_]` are derived (a lemma of the real theory, the rule and `rewrite Pr`); +- the facts on probabilities of `rewrite Pr` (`EcBdHoarePrFact`, an + axiom schema without premise: `mu_eq`, `mu_sub`, `mu_split`, `muE`, + …; the node records the schema and its resolved parameters, binders + included, and the checker regenerates the fact and compares it with + the goal) are statements on the probability of an event of one + procedure, the object of the phoare logic: they live in + `rules/bdhoare/`; `rewrite Pr` is derived (a rewriting with the cut + fact, closed by the rule), and `byupto` / `byequiv` use it; - program transformations go through the transformation rule of each logic (`EcTransform`); only their catalogue entries live in `rules/transforms/`. diff --git a/src/phl/ecPhlPrRw.ml b/src/phl/ecPhlPrRw.ml index 8709cce9e..d96cefb6c 100644 --- a/src/phl/ecPhlPrRw.ml +++ b/src/phl/ecPhlPrRw.ml @@ -1,355 +1,5 @@ (* -------------------------------------------------------------------- *) -open EcUtils -open EcAst -open EcFol -open EcEnv - -open EcCoreGoal -open EcLowGoal - -module Mid = EcIdent.Mid - -(* -------------------------------------------------------------------- *) -let t_pr_lemma lemma tc = - let concl = FApi.tc1_goal tc in - assert (f_equal concl lemma); - FApi.xmutate1 tc `RwPr [] - -(* -------------------------------------------------------------------- *) -let pr_eq env pr_m f args p1 p2 = - let m = p1.m in - let mem = Fun.prF_memenv m f env in - let hyp = EcSubst.f_forall_mems_ss_inv mem (map_ss_inv2 f_iff p1 p2) in - let concl = f_eq (f_pr pr_m f args p1) (f_pr pr_m f args p2) in - f_imp hyp (f_eq concl f_true) - -let pr_sub env pr_m f args p1 p2 = - let m = p1.m in - let mem = Fun.prF_memenv m f env in - let hyp = EcSubst.f_forall_mems_ss_inv mem (map_ss_inv2 f_imp p1 p2) in - let concl = f_real_le (f_pr pr_m f args p1) (f_pr pr_m f args p2) in - f_imp hyp (f_eq concl f_true) - -let pr_false pr_m f args = - let m = EcIdent.create "&hr" in - f_eq (f_pr pr_m f args {m;inv=f_false}) f_r0 - -let pr_not pr_m f args p = - let m = p.m in - f_eq - (f_pr pr_m f args (map_ss_inv1 f_not p)) - (f_real_sub (f_pr pr_m f args {m;inv=f_true}) (f_pr pr_m f args p)) - -let pr_or pr_m f args por p1 p2 = - let pr1 = f_pr pr_m f args p1 in - let pr2 = f_pr pr_m f args p2 in - let pr12 = f_pr pr_m f args (map_ss_inv2 f_and p1 p2) in - let pr = f_real_sub (f_real_add pr1 pr2) pr12 in - f_eq (f_pr pr_m f args (por p1 p2)) pr - -let pr_disjoint env pr_m f args por p1 p2 = - let m = p1.m in - let mem = Fun.prF_memenv m f env in - let hyp = EcSubst.f_forall_mems_ss_inv mem (map_ss_inv1 f_not (map_ss_inv2 f_and p1 p2)) in - let pr1 = f_pr pr_m f args p1 in - let pr2 = f_pr pr_m f args p2 in - let pr = f_real_add pr1 pr2 in - f_imp hyp (f_eq (f_pr pr_m f args (por p1 p2)) pr) - -let pr_split pr_m f args ev1 ev2 = - let pr = f_pr pr_m f args ev1 in - let pr1 = f_pr pr_m f args (map_ss_inv2 f_and ev1 ev2) in - let pr2 = f_pr pr_m f args (map_ss_inv2 f_and ev1 (map_ss_inv1 f_not ev2)) in - f_eq pr (f_real_add pr1 pr2) - -let pr_ge0 pr_m f args ev = - let pr = f_pr pr_m f args ev in - f_eq (f_real_le f_r0 pr) f_true - -let pr_le1 pr_m f args ev = - let pr = f_pr pr_m f args ev in - f_eq (f_real_le pr f_r1) f_true - -let pr_sum env pr = - let prf = EcEnv.Fun.by_xpath pr.pr_fun env in - let xty = prf.f_sig.fs_ret in - let x = EcIdent.create "x" in - let ev = pr.pr_event in - let m = ev.m in - let fx = {m;inv=f_local x xty} in - let prx = - let event = - map_ss_inv2 f_and_simpl - ev - (map_ss_inv2 f_eq (f_pvar EcTypes.pv_res xty ev.m) fx) - in f_pr pr.pr_mem pr.pr_fun pr.pr_args event in - - let prx = - EcFol.f_app - (EcFol.f_op EcCoreLib.CI_Sum.p_sum [ xty ] - (EcTypes.tfun (EcTypes.tfun xty EcTypes.treal) EcTypes.treal)) - [ EcFol.f_lambda [ (x, GTty xty) ] prx ] - EcTypes.treal - in - - f_eq (f_pr_r pr) prx - -let pr_mu1_le_eq_mu1 pr_m f args resv k fresh_id d = - let m = resv.m in - let kfresh = f_local fresh_id k.f_ty in - let f_ll = f_bdHoareF {m;inv=f_true} f {m;inv=f_true} FHeq {m;inv=f_r1} - and f_le_mu1 = f_forall [ (fresh_id, gtty k.f_ty) ] - (f_real_le (f_pr pr_m f args {m;inv=f_eq resv.inv kfresh}) (f_mu_x d kfresh)) - and concl = - f_eq (f_pr pr_m f args {m;inv=f_eq resv.inv k}) (f_mu_x d k) in - f_imp f_ll (f_imp f_le_mu1 concl) - -let p_List = [EcCoreLib.i_top; "List"] -let p_BRA = [EcCoreLib.i_top; "StdBigop"; "Bigreal"; "BRA"] -let p_list_has = EcPath.fromqsymbol (p_List, "has") -let p_BRA_big = EcPath.fromqsymbol (p_BRA, "big") - -let destr_pr_has pr = - let m = pr.pr_event.m in - match pr.pr_event.inv.f_node with - | Fapp ({ f_node = Fop(op, [ty_elem]) }, [f_f; f_l]) -> - if EcPath.p_equal p_list_has op && not (Mid.mem m f_l.f_fv) then - Some(ty_elem, {m;inv=f_f}, f_l) - else None - | _ -> None - -let is_eq_w_const_rhs (f: ss_inv): bool = - try - let _, rhs = destr_eq f.inv in - not (Mid.mem f.m rhs.f_fv) - with DestrError _ -> false - -(* - lemma mu_has_le ['a 'b] (P : 'a -> 'b -> bool) (d : 'a distr) (s : 'b list) : - mu d (fun a => has (P a) s) <= BRA.big predT (fun b => mu d (fun a => P a b)) s. - Pr [f(args)@ &m : has Pa s] <= BRA.big predT (fun b => Pr [f(args) &m : Pa b]) s -*) -let pr_has_le f_pr = - let pr = destr_pr f_pr in - let ty_elem, f_f, f_l = oget (destr_pr_has pr) in - let idx = EcIdent.create "x" in - let x = f_local idx ty_elem in - let pr_event = map_ss_inv1 (fun f -> f_app f [x] EcTypes.tbool) f_f in - let f_pr1 = f_pr_r {pr with pr_event} in - let f_fsum = f_lambda [idx, GTty ty_elem] f_pr1 in - let f_sum = - f_app (f_op p_BRA_big [ty_elem] EcTypes.treal) [f_predT ty_elem; f_fsum; f_l] EcTypes.treal in - f_real_le f_pr f_sum - -(* -------------------------------------------------------------------- *) -exception FoundPr of form - -let select_pr on_ev sid f = - match f.f_node with - | Fpr { pr_event = ev } -> - if on_ev ev && Mid.set_disjoint f.f_fv sid then raise (FoundPr f) - else false - | _ -> false - -let select_pr_cmp on_cmp sid f = - match f.f_node with - | Fapp - ({ f_node = Fop (op, _) }, [ { f_node = Fpr pr1 }; { f_node = Fpr pr2 } ]) - -> - if on_cmp op - && EcIdent.id_equal pr1.pr_mem pr2.pr_mem - && EcPath.x_equal pr1.pr_fun pr2.pr_fun - && f_equal pr1.pr_args pr2.pr_args - && Mid.set_disjoint f.f_fv sid - then raise (FoundPr f) - else false - | _ -> false - -let select_pr_ge0 sid f = - match f.f_node with - | Fapp ({ f_node = Fop (op, _) }, [ f'; { f_node = Fpr _ } ]) -> - if EcPath.p_equal EcCoreLib.CI_Real.p_real_le op - && f_equal f' f_r0 - && Mid.set_disjoint f.f_fv sid - then raise (FoundPr f) - else false - | _ -> false - -let select_pr_le1 sid f = - match f.f_node with - | Fapp ({ f_node = Fop (op, _) }, [ { f_node = Fpr _ }; f' ]) -> - if EcPath.p_equal EcCoreLib.CI_Real.p_real_le op - && f_equal f' f_r1 - && Mid.set_disjoint f.f_fv sid - then raise (FoundPr f) - else false - | _ -> false - -let select_pr_muhasle sid f = - match f.f_node with - | Fapp ({ f_node = Fop (op, _) }, [ { f_node = Fpr pr } as f_pr; _ ]) -> - if EcPath.p_equal EcCoreLib.CI_Real.p_real_le op then - match destr_pr_has pr with - | Some (_, _, f_l) when - Mid.set_disjoint f_l.f_fv sid -> - raise (FoundPr f_pr) - | _ -> false - else false - | _ -> false - -(* -------------------------------------------------------------------- *) -let pr_rewrite_lemma = - [ - ("mu1_le_eq_mu1", `Mu1LeEqMu1); - ("muE", `MuSum); - ("mu_disjoint", `MuDisj); - ("mu_eq", `MuEq); - ("mu_false", `MuFalse); - ("mu_ge0", `MuGe0); - ("mu_le1", `MuLe1); - ("mu_not", `MuNot); - ("mu_or", `MuOr); - ("mu_split", `MuSplit); - ("mu_sub", `MuSub); - ("mu_has_le", `MuHasLe) - ] - -(* -------------------------------------------------------------------- *) -let t_pr_rewrite_low (s, (dof: (_ -> _ -> _ -> ss_inv) option)) tc = - let kind = - try List.assoc s pr_rewrite_lemma - with Not_found -> - tc_error !!tc "Pr-rewrite: `%s` is not a suitable probability lemma" s - in - - let expect_arg = function `MuSplit | `Mu1LeEqMu1 -> true | _ -> false in - (if not (is_some dof = expect_arg kind) then - let neg = if is_some dof then "no " else "" in - tc_error !!tc "Pr-rewrite: %sargument expected for `%s`" neg s); - - let select = - match kind with - | `Mu1LeEqMu1 -> select_pr is_eq_w_const_rhs - | `MuDisj | `MuOr -> select_pr (fun inv -> is_or inv.inv) - | `MuEq -> select_pr_cmp (EcPath.p_equal EcCoreLib.CI_Bool.p_eq) - | `MuFalse -> select_pr (fun inv -> is_false inv.inv) - | `MuGe0 -> select_pr_ge0 - | `MuLe1 -> select_pr_le1 - | `MuNot -> select_pr (fun inv -> is_not inv.inv) - | `MuSplit -> select_pr (fun _ev -> true) - | `MuSub -> select_pr_cmp (EcPath.p_equal EcCoreLib.CI_Real.p_real_le) - | `MuSum -> select_pr (fun _ev -> true) - | `MuHasLe -> select_pr_muhasle - in - - let select xs fp = if select xs fp then `Accept (-1) else `Continue in - let env, hyps, concl = FApi.tc1_eflat tc in - let torw = - try - ignore (EcMatching.FPosition.select select concl); - tc_error !!tc "Pr-rewrite: cannot find a pattern for `%s`" s - with FoundPr f -> f in - - let lemma, args = - match kind with - | `Mu1LeEqMu1 -> - let { pr_fun; pr_args; pr_mem } as pr = destr_pr torw in - let (resv, k) = map_ss_inv_destr2 destr_eq pr.pr_event in - let k_id = EcEnv.LDecl.fresh_id hyps "k" in - let d = (oget dof) tc torw (EcTypes.tdistr k.inv.f_ty) in - (* Check that k and d do not reference the post-execution memory. - Otherwise the rewrite is unsound: the event `res = k` would use - k from the post-state, but `mu1 d k` treats k as a constant. *) - if Mid.mem k.m k.inv.f_fv then - (* This case should already be filtered by selection *) - assert false; - if Mid.mem d.m d.inv.f_fv then - tc_error !!tc - "Pr-rewrite: the distribution must not depend on memories"; - (pr_mu1_le_eq_mu1 pr_mem pr_fun pr_args resv k.inv k_id d.inv, 2) - - | (`MuEq | `MuSub as kind) -> begin - match torw.f_node with - | Fapp(_, [{f_node = Fpr pr1 }; - {f_node = Fpr pr2 };]) - -> begin - let { pr_mem = m ; pr_fun = f; pr_args = args } = pr1 in - let ev1 = pr1.pr_event in - let ev2 = EcSubst.ss_inv_rebind pr2.pr_event ev1.m in - match kind with - | `MuEq -> (pr_eq env m f args ev1 ev2, 1) - | `MuSub -> (pr_sub env m f args ev1 ev2, 1) - end - | _ -> assert false - end - - | `MuFalse -> - let { pr_mem = m ; pr_fun = f; pr_args = args } = destr_pr torw in - (pr_false m f args, 0) - - | `MuNot -> - let { pr_mem = m ; pr_fun = f; pr_args = args; } as pr = destr_pr torw in - let ev = map_ss_inv1 destr_not pr.pr_event in - (pr_not m f args ev, 0) - - | `MuOr -> - let { pr_mem = m ; pr_fun = f; pr_args = args; } as pr = destr_pr torw in - let asym = fst (destr_or_r pr.pr_event.inv) in - let (ev1, ev2) = map_ss_inv_destr2 (fun prev -> snd (destr_or_r prev)) pr.pr_event in - (pr_or m f args (match asym with | `Asym -> map_ss_inv2 f_ora | `Sym -> map_ss_inv2 f_or) ev1 ev2, 0) - - | `MuDisj -> - let { pr_mem = m ; pr_fun = f; pr_args = args; } as pr = destr_pr torw in - let asym = fst (destr_or_r pr.pr_event.inv) in - let (ev1, ev2) = map_ss_inv_destr2 (fun prev -> snd (destr_or_r prev)) pr.pr_event in - (pr_disjoint env m f args (match asym with | `Asym -> map_ss_inv2 f_ora | `Sym -> map_ss_inv2 f_or) ev1 ev2, 1) - - | `MuSplit -> - let pr = destr_pr torw in - let ev' = EcSubst.ss_inv_rebind ((oget dof) tc torw EcTypes.tbool) pr.pr_event.m in - (pr_split pr.pr_mem pr.pr_fun pr.pr_args pr.pr_event ev', 0) - - | `MuGe0 -> begin - match torw.f_node with - | Fapp({f_node = Fop _}, [_; {f_node = Fpr pr}]) -> - let { pr_mem = m; pr_fun = f; pr_args = args } = pr in - (pr_ge0 m f args pr.pr_event, 0) - | _ -> assert false - end - - | `MuLe1 -> begin - match torw.f_node with - | Fapp({f_node = Fop _}, [{f_node = Fpr pr}; _]) -> - let { pr_mem = m; pr_fun = f; pr_args = args } = pr in - (pr_le1 m f args pr.pr_event, 0) - | _ -> assert false - end - - | `MuSum -> - (pr_sum env (destr_pr torw), 0) - - | `MuHasLe -> - (pr_has_le torw, 0) - - in - - let rwpt = EcCoreGoal.ptcut ~args:(List.make args (PASub None)) lemma in - - FApi.t_first - (t_pr_lemma lemma) - (t_rewrite rwpt (`LtoR, None) tc) - -let t_pr_rewrite_i (s, f) tc = - let do_ev = omap (fun f _ _ _ -> f) f in - t_pr_rewrite_low (s, do_ev) tc - -let t_pr_rewrite (s, f) tc = - let to_env f tc torw ty = - let env, hyps, _ = FApi.tc1_eflat tc in - let pr = destr_pr torw in - let m = EcIdent.create "&hr" in - let mp = EcEnv.Fun.prF_memenv m pr.pr_fun env in - let hyps = LDecl.push_active_ss mp hyps in - {m;inv=EcProofTyping.process_form hyps f ty} - in - t_pr_rewrite_low (s, omap to_env f) tc +(* Legacy entry points of [rewrite Pr]: adapters onto + [EcBdHoarePrFact]. *) +let t_pr_rewrite_i = EcBdHoarePrFact.t_pr_rewrite +let t_pr_rewrite = EcBdHoarePrFact.process_pr_rewrite diff --git a/src/phl/rules/bdhoare/ecBdHoarePrFact.ml b/src/phl/rules/bdhoare/ecBdHoarePrFact.ml new file mode 100644 index 000000000..02bc64b8b --- /dev/null +++ b/src/phl/rules/bdhoare/ecBdHoarePrFact.ml @@ -0,0 +1,461 @@ +(* -------------------------------------------------------------------- *) +open EcUtils +open EcAst +open EcFol +open EcEnv + +open EcCoreGoal +open EcLowGoal + +module Mid = EcIdent.Mid + +(* -------------------------------------------------------------------- *) +(* The facts of the [pr-fact] rule: an axiom schema of facts on the + probabilities [Pr[f(args) @ &m : _]] of one procedure, from one + initial memory and with the same arguments. Each schema carries its + resolved parameters: the events (in the final memory of [f]) and the + binders it introduces, so that the fact is a deterministic function of + the node. *) +type pr_fact = + | PFMuEq of ss_inv * ss_inv + | PFMuSub of ss_inv * ss_inv + | PFMuFalse of memory + | PFMuNot of ss_inv + | PFMuOr of [`Sym | `Asym] * ss_inv * ss_inv + | PFMuDisj of [`Sym | `Asym] * ss_inv * ss_inv + | PFMuSplit of ss_inv * ss_inv + | PFMuGe0 of ss_inv + | PFMuLe1 of ss_inv + | PFMuSum of ss_inv * EcIdent.t + | PFMu1LeEqMu1 of ss_inv * form * EcIdent.t * form + | PFMuHasLe of ss_inv * EcIdent.t + +(* Parameters of the rule: already resolved and typed, the same record is + the rule argument and the node payload. *) +type pr_fact_node = { + pfn_mem : memory; (* initial memory &m *) + pfn_fun : EcPath.xpath; + pfn_args : form; + pfn_fact : pr_fact; +} + +type EcCoreGoal.rule += RBdHoarePrFact of pr_fact_node + +exception InvalidPrFact of string + +(* -------------------------------------------------------------------- *) +let p_List = [EcCoreLib.i_top; "List"] +let p_BRA = [EcCoreLib.i_top; "StdBigop"; "Bigreal"; "BRA"] +let p_list_has = EcPath.fromqsymbol (p_List, "has") +let p_BRA_big = EcPath.fromqsymbol (p_BRA, "big") + +(* [has P s], [s] not depending on the memory of the event. *) +let destr_ev_has (ev : ss_inv) = + let m = ev.m in + match ev.inv.f_node with + | Fapp ({ f_node = Fop(op, [ty_elem]) }, [f_f; f_l]) -> + if EcPath.p_equal p_list_has op && not (Mid.mem m f_l.f_fv) then + Some(ty_elem, {m;inv=f_f}, f_l) + else None + | _ -> None + +(* -------------------------------------------------------------------- *) +(* The schemas. *) +let pr_eq env pr_m f args p1 p2 = + let m = p1.m in + let mem = Fun.prF_memenv m f env in + let hyp = EcSubst.f_forall_mems_ss_inv mem (map_ss_inv2 f_iff p1 p2) in + let concl = f_eq (f_pr pr_m f args p1) (f_pr pr_m f args p2) in + f_imp hyp (f_eq concl f_true) + +let pr_sub env pr_m f args p1 p2 = + let m = p1.m in + let mem = Fun.prF_memenv m f env in + let hyp = EcSubst.f_forall_mems_ss_inv mem (map_ss_inv2 f_imp p1 p2) in + let concl = f_real_le (f_pr pr_m f args p1) (f_pr pr_m f args p2) in + f_imp hyp (f_eq concl f_true) + +let pr_false pr_m f args m = + f_eq (f_pr pr_m f args {m;inv=f_false}) f_r0 + +let pr_not pr_m f args p = + let m = p.m in + f_eq + (f_pr pr_m f args (map_ss_inv1 f_not p)) + (f_real_sub (f_pr pr_m f args {m;inv=f_true}) (f_pr pr_m f args p)) + +let pr_or pr_m f args por p1 p2 = + let pr1 = f_pr pr_m f args p1 in + let pr2 = f_pr pr_m f args p2 in + let pr12 = f_pr pr_m f args (map_ss_inv2 f_and p1 p2) in + let pr = f_real_sub (f_real_add pr1 pr2) pr12 in + f_eq (f_pr pr_m f args (por p1 p2)) pr + +let pr_disjoint env pr_m f args por p1 p2 = + let m = p1.m in + let mem = Fun.prF_memenv m f env in + let hyp = EcSubst.f_forall_mems_ss_inv mem (map_ss_inv1 f_not (map_ss_inv2 f_and p1 p2)) in + let pr1 = f_pr pr_m f args p1 in + let pr2 = f_pr pr_m f args p2 in + let pr = f_real_add pr1 pr2 in + f_imp hyp (f_eq (f_pr pr_m f args (por p1 p2)) pr) + +let pr_split pr_m f args ev1 ev2 = + let pr = f_pr pr_m f args ev1 in + let pr1 = f_pr pr_m f args (map_ss_inv2 f_and ev1 ev2) in + let pr2 = f_pr pr_m f args (map_ss_inv2 f_and ev1 (map_ss_inv1 f_not ev2)) in + f_eq pr (f_real_add pr1 pr2) + +let pr_ge0 pr_m f args ev = + let pr = f_pr pr_m f args ev in + f_eq (f_real_le f_r0 pr) f_true + +let pr_le1 pr_m f args ev = + let pr = f_pr pr_m f args ev in + f_eq (f_real_le pr f_r1) f_true + +let pr_sum env pr_m f args ev x = + let prf = EcEnv.Fun.by_xpath f env in + let xty = prf.f_sig.fs_ret in + let m = ev.m in + let fx = {m;inv=f_local x xty} in + let prx = + let event = + map_ss_inv2 f_and_simpl + ev + (map_ss_inv2 f_eq (f_pvar EcTypes.pv_res xty ev.m) fx) + in f_pr pr_m f args event in + + let prx = + EcFol.f_app + (EcFol.f_op EcCoreLib.CI_Sum.p_sum [ xty ] + (EcTypes.tfun (EcTypes.tfun xty EcTypes.treal) EcTypes.treal)) + [ EcFol.f_lambda [ (x, GTty xty) ] prx ] + EcTypes.treal + in + + f_eq (f_pr pr_m f args ev) prx + +let pr_mu1_le_eq_mu1 pr_m f args resv k fresh_id d = + let m = resv.m in + let kfresh = f_local fresh_id k.f_ty in + let f_ll = f_bdHoareF {m;inv=f_true} f {m;inv=f_true} FHeq {m;inv=f_r1} + and f_le_mu1 = f_forall [ (fresh_id, gtty k.f_ty) ] + (f_real_le (f_pr pr_m f args {m;inv=f_eq resv.inv kfresh}) (f_mu_x d kfresh)) + and concl = + f_eq (f_pr pr_m f args {m;inv=f_eq resv.inv k}) (f_mu_x d k) in + f_imp f_ll (f_imp f_le_mu1 concl) + +(* + lemma mu_has_le ['a 'b] (P : 'a -> 'b -> bool) (d : 'a distr) (s : 'b list) : + mu d (fun a => has (P a) s) <= BRA.big predT (fun b => mu d (fun a => P a b)) s. + Pr [f(args)@ &m : has Pa s] <= BRA.big predT (fun b => Pr [f(args) &m : Pa b]) s +*) +let pr_has_le pr_m f args ev ty_elem f_f f_l idx = + let x = f_local idx ty_elem in + let pr_event = map_ss_inv1 (fun f -> f_app f [x] EcTypes.tbool) f_f in + let f_pr1 = f_pr pr_m f args pr_event in + let f_fsum = f_lambda [idx, GTty ty_elem] f_pr1 in + let f_sum = + f_app (f_op p_BRA_big [ty_elem] EcTypes.treal) [f_predT ty_elem; f_fsum; f_l] EcTypes.treal in + f_real_le (f_pr pr_m f args ev) f_sum + +(* -------------------------------------------------------------------- *) +(* Pure core shared by the rule and its checker: the fact of the node. + The side conditions of the schemas (the events sharing one memory, the + constants not depending on it, the binders not captured) are checked + here, raising [InvalidPrFact], so the checker re-validates them. *) +let pr_fact (hyps : LDecl.hyps) (n : pr_fact_node) : form = + let env = LDecl.toenv hyps in + let fail = fun msg -> raise (InvalidPrFact msg) in + let pr_m, f, args = n.pfn_mem, n.pfn_fun, n.pfn_args in + let same_mem (p1 : ss_inv) (p2 : ss_inv) = + if not (EcIdent.id_equal p1.m p2.m) then + fail "the events are not in the same memory" in + let fresh x fs = + if List.exists (fun (g : form) -> Mid.mem x g.f_fv) fs then + fail "the bound variable is not fresh" in + + match n.pfn_fact with + | PFMuEq (p1, p2) -> + same_mem p1 p2; pr_eq env pr_m f args p1 p2 + | PFMuSub (p1, p2) -> + same_mem p1 p2; pr_sub env pr_m f args p1 p2 + | PFMuFalse m -> + pr_false pr_m f args m + | PFMuNot p -> + pr_not pr_m f args p + | PFMuOr (asym, p1, p2) -> + let por = match asym with `Asym -> f_ora | `Sym -> f_or in + same_mem p1 p2; pr_or pr_m f args (map_ss_inv2 por) p1 p2 + | PFMuDisj (asym, p1, p2) -> + let por = match asym with `Asym -> f_ora | `Sym -> f_or in + same_mem p1 p2; pr_disjoint env pr_m f args (map_ss_inv2 por) p1 p2 + | PFMuSplit (ev1, ev2) -> + same_mem ev1 ev2; pr_split pr_m f args ev1 ev2 + | PFMuGe0 ev -> + pr_ge0 pr_m f args ev + | PFMuLe1 ev -> + pr_le1 pr_m f args ev + | PFMuSum (ev, x) -> + fresh x [args; ev.inv]; pr_sum env pr_m f args ev x + | PFMu1LeEqMu1 (resv, k, k', d) -> + if Mid.mem resv.m k.f_fv then + fail "the value depends on the memory of the event"; + fresh k' [args; resv.inv; d]; + pr_mu1_le_eq_mu1 pr_m f args resv k k' d + | PFMuHasLe (ev, x) -> + let ty_elem, f_f, f_l = + match destr_ev_has ev with + | Some x -> x + | None -> fail "the event is not of the form [has P s]" in + fresh x [args; f_f.inv]; + pr_has_le pr_m f args ev ty_elem f_f f_l x + +(* The rule has no premise: the goal must be the fact of the node. *) +let bdhoare_pr_fact_subgoals (hyps : LDecl.hyps) (concl : form) (n : pr_fact_node) = + if not (f_equal concl (pr_fact hyps n)) then + raise (InvalidPrFact "the goal is not the fact"); + [] + +(* -------------------------------------------------------------------- *) +(* Rule (TCB). *) +let t_bdhoare_pr_fact (n : pr_fact_node) (tc : tcenv1) = + let subgoals = + try bdhoare_pr_fact_subgoals (FApi.tc1_hyps tc) (FApi.tc1_goal tc) n + with InvalidPrFact msg -> tc_error !!tc "Pr-rewrite: %s" msg in + FApi.xrule1 tc (RBdHoarePrFact n) subgoals + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | RBdHoarePrFact n -> + Some (EcPlRecheck.checker_of "bdhoare-pr-fact" (fun _ concl -> concl) + (fun hyps concl -> bdhoare_pr_fact_subgoals hyps concl n)) + | _ -> None) + +(* ==================================================================== *) +(* Derived (no proof-node): [rewrite Pr], rewriting with a fact of the + rule. *) +exception FoundPr of form + +let select_pr on_ev sid f = + match f.f_node with + | Fpr { pr_event = ev } -> + if on_ev ev && Mid.set_disjoint f.f_fv sid then raise (FoundPr f) + else false + | _ -> false + +let select_pr_cmp on_cmp sid f = + match f.f_node with + | Fapp + ({ f_node = Fop (op, _) }, [ { f_node = Fpr pr1 }; { f_node = Fpr pr2 } ]) + -> + if on_cmp op + && EcIdent.id_equal pr1.pr_mem pr2.pr_mem + && EcPath.x_equal pr1.pr_fun pr2.pr_fun + && f_equal pr1.pr_args pr2.pr_args + && Mid.set_disjoint f.f_fv sid + then raise (FoundPr f) + else false + | _ -> false + +let select_pr_ge0 sid f = + match f.f_node with + | Fapp ({ f_node = Fop (op, _) }, [ f'; { f_node = Fpr _ } ]) -> + if EcPath.p_equal EcCoreLib.CI_Real.p_real_le op + && f_equal f' f_r0 + && Mid.set_disjoint f.f_fv sid + then raise (FoundPr f) + else false + | _ -> false + +let select_pr_le1 sid f = + match f.f_node with + | Fapp ({ f_node = Fop (op, _) }, [ { f_node = Fpr _ }; f' ]) -> + if EcPath.p_equal EcCoreLib.CI_Real.p_real_le op + && f_equal f' f_r1 + && Mid.set_disjoint f.f_fv sid + then raise (FoundPr f) + else false + | _ -> false + +let select_pr_muhasle sid f = + match f.f_node with + | Fapp ({ f_node = Fop (op, _) }, [ { f_node = Fpr pr } as f_pr; _ ]) -> + if EcPath.p_equal EcCoreLib.CI_Real.p_real_le op then + match destr_ev_has pr.pr_event with + | Some (_, _, f_l) when + Mid.set_disjoint f_l.f_fv sid -> + raise (FoundPr f_pr) + | _ -> false + else false + | _ -> false + +let is_eq_w_const_rhs (f: ss_inv): bool = + try + let _, rhs = destr_eq f.inv in + not (Mid.mem f.m rhs.f_fv) + with DestrError _ -> false + +(* -------------------------------------------------------------------- *) +let pr_rewrite_lemma = + [ + ("mu1_le_eq_mu1", `Mu1LeEqMu1); + ("muE", `MuSum); + ("mu_disjoint", `MuDisj); + ("mu_eq", `MuEq); + ("mu_false", `MuFalse); + ("mu_ge0", `MuGe0); + ("mu_le1", `MuLe1); + ("mu_not", `MuNot); + ("mu_or", `MuOr); + ("mu_split", `MuSplit); + ("mu_sub", `MuSub); + ("mu_has_le", `MuHasLe) + ] + +(* -------------------------------------------------------------------- *) +(* [dof tc torw ty] is the argument of the lemma ([mu_split] and + [mu1_le_eq_mu1]), for the selected probability [torw]. *) +let t_pr_rewrite_low (s, (dof: (_ -> _ -> _ -> ss_inv) option)) tc = + let kind = + try List.assoc s pr_rewrite_lemma + with Not_found -> + tc_error !!tc "Pr-rewrite: `%s` is not a suitable probability lemma" s + in + + let expect_arg = function `MuSplit | `Mu1LeEqMu1 -> true | _ -> false in + (if not (is_some dof = expect_arg kind) then + let neg = if is_some dof then "no " else "" in + tc_error !!tc "Pr-rewrite: %sargument expected for `%s`" neg s); + + let select = + match kind with + | `Mu1LeEqMu1 -> select_pr is_eq_w_const_rhs + | `MuDisj | `MuOr -> select_pr (fun inv -> is_or inv.inv) + | `MuEq -> select_pr_cmp (EcPath.p_equal EcCoreLib.CI_Bool.p_eq) + | `MuFalse -> select_pr (fun inv -> is_false inv.inv) + | `MuGe0 -> select_pr_ge0 + | `MuLe1 -> select_pr_le1 + | `MuNot -> select_pr (fun inv -> is_not inv.inv) + | `MuSplit -> select_pr (fun _ev -> true) + | `MuSub -> select_pr_cmp (EcPath.p_equal EcCoreLib.CI_Real.p_real_le) + | `MuSum -> select_pr (fun _ev -> true) + | `MuHasLe -> select_pr_muhasle + in + + let select xs fp = if select xs fp then `Accept (-1) else `Continue in + let hyps, concl = FApi.tc1_flat tc in + let torw = + try + ignore (EcMatching.FPosition.select select concl); + tc_error !!tc "Pr-rewrite: cannot find a pattern for `%s`" s + with FoundPr f -> f in + + let node pr fact = + { pfn_mem = pr.pr_mem; pfn_fun = pr.pr_fun; pfn_args = pr.pr_args; + pfn_fact = fact; } in + + let node, args = + match kind with + | `Mu1LeEqMu1 -> + let pr = destr_pr torw in + let (resv, k) = map_ss_inv_destr2 destr_eq pr.pr_event in + let k_id = EcEnv.LDecl.fresh_id hyps "k" in + let d = (oget dof) tc torw (EcTypes.tdistr k.inv.f_ty) in + (* Check that k and d do not reference the post-execution memory. + Otherwise the rewrite is unsound: the event `res = k` would use + k from the post-state, but `mu1 d k` treats k as a constant. *) + if Mid.mem k.m k.inv.f_fv then + (* This case should already be filtered by selection *) + assert false; + if Mid.mem d.m d.inv.f_fv then + tc_error !!tc + "Pr-rewrite: the distribution must not depend on memories"; + (node pr (PFMu1LeEqMu1 (resv, k.inv, k_id, d.inv)), 2) + + | (`MuEq | `MuSub as kind) -> begin + match torw.f_node with + | Fapp(_, [{f_node = Fpr pr1 }; + {f_node = Fpr pr2 };]) + -> begin + let ev1 = pr1.pr_event in + let ev2 = EcSubst.ss_inv_rebind pr2.pr_event ev1.m in + match kind with + | `MuEq -> (node pr1 (PFMuEq (ev1, ev2)), 1) + | `MuSub -> (node pr1 (PFMuSub (ev1, ev2)), 1) + end + | _ -> assert false + end + + | `MuFalse -> + (node (destr_pr torw) (PFMuFalse (EcIdent.create "&hr")), 0) + + | `MuNot -> + let pr = destr_pr torw in + (node pr (PFMuNot (map_ss_inv1 destr_not pr.pr_event)), 0) + + | (`MuOr | `MuDisj) as kind -> + let pr = destr_pr torw in + let asym = fst (destr_or_r pr.pr_event.inv) in + let (ev1, ev2) = map_ss_inv_destr2 (fun prev -> snd (destr_or_r prev)) pr.pr_event in + begin match kind with + | `MuOr -> (node pr (PFMuOr (asym, ev1, ev2)), 0) + | `MuDisj -> (node pr (PFMuDisj (asym, ev1, ev2)), 1) + end + + | `MuSplit -> + let pr = destr_pr torw in + let ev' = EcSubst.ss_inv_rebind ((oget dof) tc torw EcTypes.tbool) pr.pr_event.m in + (node pr (PFMuSplit (pr.pr_event, ev')), 0) + + | `MuGe0 -> begin + match torw.f_node with + | Fapp({f_node = Fop _}, [_; {f_node = Fpr pr}]) -> + (node pr (PFMuGe0 pr.pr_event), 0) + | _ -> assert false + end + + | `MuLe1 -> begin + match torw.f_node with + | Fapp({f_node = Fop _}, [{f_node = Fpr pr}; _]) -> + (node pr (PFMuLe1 pr.pr_event), 0) + | _ -> assert false + end + + | `MuSum -> + let pr = destr_pr torw in + (node pr (PFMuSum (pr.pr_event, EcIdent.create "x")), 0) + + | `MuHasLe -> + let pr = destr_pr torw in + (node pr (PFMuHasLe (pr.pr_event, EcIdent.create "x")), 0) + + in + + let lemma = pr_fact hyps node in + let rwpt = EcCoreGoal.ptcut ~args:(List.make args (PASub None)) lemma in + + FApi.t_first + (t_bdhoare_pr_fact node) + (t_rewrite rwpt (`LtoR, None) tc) + +let t_pr_rewrite (s, f) tc = + let do_ev = omap (fun f _ _ _ -> f) f in + t_pr_rewrite_low (s, do_ev) tc + +(* ==================================================================== *) +(* Elaboration: [rewrite Pr s [f]], the argument typed in the final + memory of the selected probability. *) +let process_pr_rewrite (s, f) tc = + let to_env f tc torw ty = + let env, hyps, _ = FApi.tc1_eflat tc in + let pr = destr_pr torw in + let m = EcIdent.create "&hr" in + let mp = EcEnv.Fun.prF_memenv m pr.pr_fun env in + let hyps = LDecl.push_active_ss mp hyps in + {m;inv=EcProofTyping.process_form hyps f ty} + in + t_pr_rewrite_low (s, omap to_env f) tc diff --git a/src/phl/rules/bdhoare/ecBdHoarePrFact.mli b/src/phl/rules/bdhoare/ecBdHoarePrFact.mli new file mode 100644 index 000000000..56c2a428a --- /dev/null +++ b/src/phl/rules/bdhoare/ecBdHoarePrFact.mli @@ -0,0 +1,106 @@ +(* -------------------------------------------------------------------- *) +open EcSymbols +open EcAst +open EcCoreGoal.FApi + +(* ==================================================================== *) +(* Rules (trusted) *) + +(* The facts of the rule, on the probabilities of one procedure [f], from + one initial memory [&m] and with the same arguments [args]; [Pr[E]] + stands for [Pr[f(args) @ &m : E]], the events are read in the final + memory [&m'] of [f] (bound by each probability). *) +type pr_fact = + | PFMuEq of ss_inv * ss_inv + (* mu_eq [E1; E2]: + (forall &m', E1 <=> E2) => (Pr[E1] = Pr[E2]) = true *) + | PFMuSub of ss_inv * ss_inv + (* mu_sub [E1; E2]: + (forall &m', E1 => E2) => (Pr[E1] <= Pr[E2]) = true *) + | PFMuFalse of memory + (* mu_false [&m']: Pr[false] = 0%r *) + | PFMuNot of ss_inv + (* mu_not [E]: Pr[!E] = Pr[true] - Pr[E] *) + | PFMuOr of [`Sym | `Asym] * ss_inv * ss_inv + (* mu_or [E1; E2]: + Pr[E1 \/ E2] = Pr[E1] + Pr[E2] - Pr[E1 /\ E2] + ([||] instead of [\/] for [`Asym]) *) + | PFMuDisj of [`Sym | `Asym] * ss_inv * ss_inv + (* mu_disjoint [E1; E2]: + (forall &m', !(E1 /\ E2)) => Pr[E1 \/ E2] = Pr[E1] + Pr[E2] + ([||] instead of [\/] for [`Asym]) *) + | PFMuSplit of ss_inv * ss_inv + (* mu_split [E; B]: Pr[E] = Pr[E /\ B] + Pr[E /\ !B] *) + | PFMuGe0 of ss_inv + (* mu_ge0 [E]: (0%r <= Pr[E]) = true *) + | PFMuLe1 of ss_inv + (* mu_le1 [E]: (Pr[E] <= 1%r) = true *) + | PFMuSum of ss_inv * EcIdent.t + (* muE [E; x]: Pr[E] = sum (fun x => Pr[E /\ res = x]) + ([E /\ res = x] simplified to [res = x] when [E] is [true]) *) + | PFMu1LeEqMu1 of ss_inv * form * EcIdent.t * form + (* mu1_le_eq_mu1 [e; k; k'; d]: + phoare [f : true ==> true] = 1%r + => (forall k', Pr[e = k'] <= mu1 d k') + => Pr[e = k] = mu1 d k *) + | PFMuHasLe of ss_inv * EcIdent.t + (* mu_has_le [has P s; x]: + Pr[has P s] <= BRA.big predT (fun x => Pr[P x]) s *) + +type pr_fact_node = { + pfn_mem : memory; (* initial memory &m *) + pfn_fun : EcPath.xpath; (* procedure f *) + pfn_args : form; (* arguments args *) + pfn_fact : pr_fact; (* the fact and its parameters *) +} + +(* [t_bdhoare_pr_fact n] — the axiom schema of the facts on + probabilities, [F] the fact of [n] (above): + + --------- (no premise) + F + + Side conditions (otherwise fails): the events of [mu_eq], [mu_sub], + [mu_or], [mu_disjoint] and [mu_split] are in the same memory; in + [mu1_le_eq_mu1], [k] does not depend on the memory of the event [e], + and [k'] is free neither in [args], [e] nor [d]; in [muE] (resp. + [mu_has_le]), [x] is free neither in [args] nor [E] (resp. [P]); the + event of [mu_has_le] has the form [has P s], [s] not depending on the + memory of the event; the goal is [F] (syntactically). + + Node: [RBdHoarePrFact n]. Checker: "bdhoare-pr-fact". *) +val t_bdhoare_pr_fact : pr_fact_node -> backward + +(* ==================================================================== *) +(* Derived tactics *) + +(* [t_pr_rewrite (s, a)] — [rewrite Pr s a]: selects in the goal the + first subterm the lemma [s] applies to, among + - [mu_eq] (resp. [mu_sub]): [Pr[E1] = Pr[E2]] (resp. [<=]), the same + procedure, arguments and initial memory on both sides; + - [mu_false], [mu_not], [mu_or], [mu_disjoint]: [Pr[false]], + [Pr[!E]], [Pr[E1 \/ E2]] (or [||]); + - [mu_split] (argument [B]), [muE]: any [Pr[E]]; + - [mu_ge0], [mu_le1]: [0%r <= Pr[E]], [Pr[E] <= 1%r]; + - [mu1_le_eq_mu1] (argument [d], not depending on its memory): + [Pr[e = k]], [k] not depending on the memory of the event; + - [mu_has_le]: [Pr[has P s]] on the left of [<=], [s] not depending + on the memory of the event; + resolves the parameters of the fact [F] of the lemma for it (an + argument [B] being read in the memory of the event), and rewrites + the goal (left to right) with the cut [F], closed on the spot by + [t_bdhoare_pr_fact]. Visible goals: the hypotheses of [F] (none, one + for [mu_eq], [mu_sub], [mu_disjoint], two for [mu1_le_eq_mu1]), then + the rewritten goal, as for [rewrite] with a lemma. Fails when [s] is + not one of these lemmas, when an argument is given to a lemma that + takes none (or conversely), or when no subterm matches. Emits no node + of its own. *) +val t_pr_rewrite : symbol * ss_inv option -> backward + +(* ==================================================================== *) +(* Elaboration *) + +(* [rewrite Pr s [a]]: [t_pr_rewrite], the argument [a] typed in the final + memory of the selected probability (with the type [bool] for + [mu_split], [ty distr] for [mu1_le_eq_mu1], [ty] the type of [k]). *) +val process_pr_rewrite : symbol * EcParsetree.pformula option -> backward diff --git a/src/phl/rules/equiv/ecEquivDeno.ml b/src/phl/rules/equiv/ecEquivDeno.ml index ec3d4a480..9f3f1d13d 100644 --- a/src/phl/rules/equiv/ecEquivDeno.ml +++ b/src/phl/rules/equiv/ecEquivDeno.ml @@ -6,7 +6,6 @@ open EcTypes open EcFol open EcEnv open EcPV -open EcPhlPrRw open EcHiGoal open EcSubst @@ -119,10 +118,8 @@ let () = (* ==================================================================== *) (* 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]. *) + lemmas of [Real] on probabilities, the probability rewritings being + [rewrite Pr] ([EcBdHoarePrFact]). *) 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" @@ -166,8 +163,8 @@ let t_pr_pos tc = 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 + [ EcBdHoarePrFact.t_pr_rewrite ("mu_false", None) @! t_true; + EcBdHoarePrFact.t_pr_rewrite ("mu_sub", None) @! t_true]) tc (* -------------------------------------------------------------------- *) let t_equiv_deno_bad pre tc = @@ -194,12 +191,12 @@ let t_equiv_deno_bad pre tc = t_id; t_id; t_intros_s (`Symbol ["_";"_"]) @! t_apply_prept (`UG real_upto_or) ]; - t_pr_rewrite_i ("mu_disjoint", None) @+ + EcBdHoarePrFact.t_pr_rewrite ("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) @+ [ + EcBdHoarePrFact.t_pr_rewrite ("mu_sub",None) @+ [ t_intros_s (`Symbol ["_"]) @! t_apply_prept (`UG real_upto_sub); t_trivial; ]; @@ -268,8 +265,8 @@ let t_equiv_deno_bad2 pre bad1 tc = (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 ] ; + [ EcBdHoarePrFact.t_pr_rewrite ("mu_split", Some bad1) @! t_reflex; + EcBdHoarePrFact.t_pr_rewrite ("mu_split", Some bad2) @! t_reflex ] ; t_apply_prept (`UG real_upto) @+ [ t_pr_pos; t_pr_pos; @@ -278,7 +275,7 @@ let t_equiv_deno_bad2 pre bad1 tc = t_apply_hyp hcpre; t_intros_s (`Symbol ["_"; "_"]) @! t_apply_prept (`UG real_upto_imp_bad) ]; - t_pr_rewrite ("mu_sub",None) @! t_trivial; + EcBdHoarePrFact.t_pr_rewrite ("mu_sub",None) @! t_trivial; t_deno @+ [ t_apply_hyp hequiv; t_apply_hyp hcpre; diff --git a/src/phl/rules/equiv/ecEquivDeno.mli b/src/phl/rules/equiv/ecEquivDeno.mli index 925ceeba8..394d6d724 100644 --- a/src/phl/rules/equiv/ecEquivDeno.mli +++ b/src/phl/rules/equiv/ecEquivDeno.mli @@ -45,9 +45,10 @@ val t_equiv_deno : equiv_deno -> backward [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). + 3. on the second side, [mu_disjoint], [ler_add], [mu_sub] + ([EcBdHoarePrFact.t_pr_rewrite]) 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 diff --git a/src/phl/rules/equiv/ecEquivUpto.ml b/src/phl/rules/equiv/ecEquivUpto.ml index 5e82392db..59c7733f3 100644 --- a/src/phl/rules/equiv/ecEquivUpto.ml +++ b/src/phl/rules/equiv/ecEquivUpto.ml @@ -11,7 +11,6 @@ open EcFol open EcCoreGoal open EcLowGoal open EcHiGoal -open EcPhlPrRw open EcCoreLib.CI_Real (* -------------------------------------------------------------------- *) @@ -381,16 +380,15 @@ let destr_sub_maxr f1 f2 = let fe2nb = f_pr pre2.pr_mem pre2.pr_fun pre2.pr_args fenb in fe1, fe1b, fe1nb, fe2, fe2b, fe2nb, fbad, fe1b', fe2b' -(* TEMPORARY: the facts on probabilities are closed by [rewrite Pr], from - the not-yet-migrated [EcPhlPrRw]. *) +(* The facts on probabilities are closed by [rewrite Pr]. *) let t_split_pr fbad = - t_pr_rewrite_i ("mu_split", Some fbad) @! t_trivial + EcBdHoarePrFact.t_pr_rewrite ("mu_split", Some fbad) @! t_trivial let t_ge0_pr = - t_pr_rewrite_i ("mu_ge0", None) @! t_trivial + EcBdHoarePrFact.t_pr_rewrite ("mu_ge0", None) @! t_trivial let t_sub_pr = - t_pr_rewrite_i ("mu_sub", None) @! t_trivial + EcBdHoarePrFact.t_pr_rewrite ("mu_sub", None) @! t_trivial let process_upto (tc : tcenv1) = let concl = FApi.tc1_goal tc in diff --git a/src/phl/rules/equiv/ecEquivUpto.mli b/src/phl/rules/equiv/ecEquivUpto.mli index 2dc68dc03..dc0ba7780 100644 --- a/src/phl/rules/equiv/ecEquivUpto.mli +++ b/src/phl/rules/equiv/ecEquivUpto.mli @@ -42,8 +42,9 @@ val t_equiv_upto : backward first apply a lemma of the real theory ([eq_upto], [upto_le], [upto_abs], [upto_maxr]), whose instance of the rule is closed by [t_equiv_upto], and whose facts on probabilities are closed by - [rewrite Pr mu_split bad] (resp. [mu_sub], [mu_ge0]) then [trivial] - (what [trivial] leaves remains visible). Here [E'] is [E /\ !bad]. + [rewrite Pr mu_split bad] (resp. [mu_sub], [mu_ge0]; + [EcBdHoarePrFact.t_pr_rewrite]) then [trivial] (what [trivial] leaves + remains visible). Here [E'] is [E /\ !bad]. - [Pr[f1 : E'] = Pr[f2 : E']]: [t_equiv_upto]; - [Pr[f1 : E] - Pr[f2 : E] = Pr[f1 : E /\ bad] - Pr[f2 : E /\ bad]]: [eq_upto], splitting both probabilities on [bad]; diff --git a/tests/pr-rewrite.ec b/tests/pr-rewrite.ec new file mode 100644 index 000000000..5d78fb525 --- /dev/null +++ b/tests/pr-rewrite.ec @@ -0,0 +1,174 @@ +(* [rewrite Pr]: the facts of the bdhoare pr-fact rule (t_bdhoare_pr_fact), + one per lemma, and the error paths of the tactic. *) +require import AllCore List Distr DInterval StdBigop RealSeries. +import Bigreal. + +(* -------------------------------------------------------------------- *) +module M = { + var g : int + + proc f(a : int) : int = { + var x : int; + x <$ [0..a]; + g <- x; + return x; + } + + proc h() : int = { + var x : int; + x <$ [0..1]; + return x; + } +}. + +(* -------------------------------------------------------------------- *) +(* mu_eq: one premise, the equivalence of the events. *) +lemma t_mu_eq &m : + Pr[M.f(1) @ &m : res = 0 /\ M.g = res] = Pr[M.f(1) @ &m : M.g = res /\ res = 0]. +proof. +rewrite Pr[mu_eq]. +- by move=> &hr; split=> [[-> ->]|[-> ->]]. +- by []. +qed. + +(* mu_sub: one premise, the inclusion of the events. *) +lemma t_mu_sub &m : + Pr[M.f(1) @ &m : res = 0] <= Pr[M.f(1) @ &m : 0 <= res]. +proof. +rewrite Pr[mu_sub]. +- by move=> &hr ->. +- by []. +qed. + +(* mu_false *) +lemma t_mu_false &m : Pr[M.f(1) @ &m : false] = 0%r. +proof. by rewrite Pr[mu_false]. qed. + +(* mu_not *) +lemma t_mu_not &m : + Pr[M.f(1) @ &m : !(res = 0)] + = Pr[M.f(1) @ &m : true] - Pr[M.f(1) @ &m : res = 0]. +proof. by rewrite Pr[mu_not]. qed. + +(* mu_or, symmetric and asymmetric disjunctions *) +lemma t_mu_or &m : + Pr[M.f(1) @ &m : res = 0 \/ M.g = 1] + = Pr[M.f(1) @ &m : res = 0] + Pr[M.f(1) @ &m : M.g = 1] + - Pr[M.f(1) @ &m : res = 0 /\ M.g = 1]. +proof. by rewrite Pr[mu_or]. qed. + +lemma t_mu_ora &m : + Pr[M.f(1) @ &m : res = 0 || M.g = 1] + = Pr[M.f(1) @ &m : res = 0] + Pr[M.f(1) @ &m : M.g = 1] + - Pr[M.f(1) @ &m : res = 0 /\ M.g = 1]. +proof. by rewrite Pr[mu_or]. qed. + +(* mu_disjoint: one premise, the disjointness of the events. *) +lemma t_mu_disjoint &m : + Pr[M.f(1) @ &m : res = 0 \/ res = 1] + = Pr[M.f(1) @ &m : res = 0] + Pr[M.f(1) @ &m : res = 1]. +proof. +rewrite Pr[mu_disjoint]. +- by move=> &hr /#. +- by []. +qed. + +lemma t_mu_disjoint_a &m : + Pr[M.f(1) @ &m : res = 0 || res = 1] + = Pr[M.f(1) @ &m : res = 0] + Pr[M.f(1) @ &m : res = 1]. +proof. +rewrite Pr[mu_disjoint]. +- by move=> &hr /#. +- by []. +qed. + +(* mu_split, the argument read in the memory of the event *) +lemma t_mu_split &m : + Pr[M.f(1) @ &m : res = 0] + = Pr[M.f(1) @ &m : res = 0 /\ M.g = res] + Pr[M.f(1) @ &m : res = 0 /\ !M.g = res]. +proof. by rewrite Pr[mu_split (M.g = res)]. qed. + +(* mu_ge0, mu_le1 *) +lemma t_mu_ge0 &m : 0%r <= Pr[M.f(1) @ &m : res = 0]. +proof. by rewrite Pr[mu_ge0]. qed. + +lemma t_mu_le1 &m : Pr[M.f(1) @ &m : res = 0] <= 1%r. +proof. by rewrite Pr[mu_le1]. qed. + +(* muE, with and without a trivial event *) +lemma t_muE &m : + Pr[M.f(1) @ &m : 0 <= res] + = sum (fun x => Pr[M.f(1) @ &m : 0 <= res /\ res = x]). +proof. by rewrite Pr[muE]. qed. + +lemma t_muE_true &m : + Pr[M.f(1) @ &m : true] = sum (fun x => Pr[M.f(1) @ &m : res = x]). +proof. by rewrite Pr[muE]. qed. + +(* mu1_le_eq_mu1: two premises, losslessness and the bound. *) +lemma t_mu1_le_eq_mu1 &m : + Pr[M.h() @ &m : res = 0] = mu1 [0..1] 0. +proof. +rewrite Pr[mu1_le_eq_mu1 [0..1]]. +- by proc; auto=> />; rewrite dinter_ll. +- move=> k; byphoare (_ : true ==> res = k)=> //. + by proc; rnd (pred1 k); auto. +- by []. +qed. + +(* mu_has_le *) +op l : int list. + +lemma t_mu_has_le &m : + Pr[M.f(1) @ &m : has (fun x => res = x) l] + <= BRA.big predT (fun x => Pr[M.f(1) @ &m : res = x]) l. +proof. by rewrite Pr[mu_has_le]. qed. + +(* The first matching subterm is rewritten. *) +lemma t_first &m : + Pr[M.f(1) @ &m : false] + Pr[M.f(2) @ &m : false] = 0%r. +proof. by rewrite Pr[mu_false] Pr[mu_false]. qed. + +(* -------------------------------------------------------------------- *) +(* Error paths. *) + +(* not a probability lemma *) +lemma e_unknown &m : Pr[M.f(1) @ &m : false] = 0%r. +proof. fail rewrite Pr[mu_foo]. abort. + +(* argument expected *) +lemma e_arg &m : Pr[M.f(1) @ &m : res = 0] = 0%r. +proof. fail rewrite Pr[mu_split]. fail rewrite Pr[mu1_le_eq_mu1]. abort. + +(* no argument expected *) +lemma e_noarg &m : Pr[M.f(1) @ &m : false] = 0%r. +proof. fail rewrite Pr[mu_false true]. abort. + +(* no pattern *) +lemma e_nopattern &m : Pr[M.f(1) @ &m : res = 0] = 0%r. +proof. +fail rewrite Pr[mu_false]. fail rewrite Pr[mu_not]. fail rewrite Pr[mu_or]. +fail rewrite Pr[mu_disjoint]. fail rewrite Pr[mu_eq]. fail rewrite Pr[mu_sub]. +fail rewrite Pr[mu_ge0]. fail rewrite Pr[mu_le1]. fail rewrite Pr[mu_has_le]. +abort. + +(* a probability under a binder it depends on is not selected *) +lemma e_bound &m : forall a, Pr[M.f(a) @ &m : false] = 0%r. +proof. fail rewrite Pr[mu_false]. abort. + +(* mu1_le_eq_mu1: the value depends on the memory of the event *) +lemma e_mu1_value &m : Pr[M.f(1) @ &m : res = M.g] = 0%r. +proof. fail rewrite Pr[mu1_le_eq_mu1 [0..1]]. abort. + +(* mu1_le_eq_mu1: the distribution depends on a memory *) +lemma e_mu1_distr &m : Pr[M.f(1) @ &m : res = 0] = 0%r. +proof. fail rewrite Pr[mu1_le_eq_mu1 [0..M.g]]. abort. + +(* mu_has_le: the list depends on the memory of the event *) +lemma e_has_le &m : + Pr[M.f(1) @ &m : has (fun x => res = x) [M.g]] <= 1%r. +proof. fail rewrite Pr[mu_has_le]. abort. + +(* not in a hypothesis *) +lemma e_hyp &m : Pr[M.f(1) @ &m : false] = 0%r => true. +proof. move=> h. fail rewrite Pr[mu_false] in h. abort.