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.