From 723a3c6195d638d38ca257c57a11c9289f9c865d Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Wed, 7 Oct 2026 00:22:21 +0200 Subject: [PATCH] refactor(pl): pr bridges as recheckable per-logic rules PR of the program-logic reorganization stack (see src/phl/REFACTORING.md). It migrates the bridge tactics relating judgements: `bypr`, `pr_bounded`, `hoare`, `phoare split` and `hoare split`: - rules/hoare/ecHoareOfBdHoare.ml: `hoare [c : P ==> Q]` from `phoare [c : P ==> !Q] = 0%r` (no exceptional postcondition); rules/bdhoare/ecBdHoareOfHoare.ml: the converse. The `hoare` tactic on a phoare goal is derived: the bound-changing consequence to `= 0%r`, then the rule. - rules/bdhoare/ecBdHoarePr.ml: `phoare [f : P ==> Q] ~ d` from forall &m, 0%r <= d /\ (P => Pr[f(args) @ &m : Q] ~ d) rules/hoare/ecHoarePr.ml derives the hoare form from it and the view above. rules/equiv/ecEquivPr.ml: `equiv [f1 ~ f2 : P ==> Q]` from the equality of the distributions of two observed expressions; the node records their common type, re-checked by the builder. - rules/bdhoare/ecBdHoarePrBounded.ml: a probability is in [0, 1] and that of `false` is 0, plus the premise forms `P => 1%r <= d` / `P => d <= 0%r` (the bound-changing consequence would add a `0%r <= d` conjunct, so they are kept as rules). - rules/bdhoare/ecBdHoareSplit.ml: inclusion-exclusion on a conjunction or a disjunction, and the complement rule; the bound change and the `phoare split b1 b2 : R` case analysis are derived. - rules/hoare/ecHoareSplit.ml: `hoare split`, derived from the consequence rules (no rule of its own). - Each rule (statement and/or procedure form) is documented as an inference rule in its .mli and emits a node with a registered checker; side conditions (bound `= 0%r`, shape of the postcondition, bound combining the premises' bounds, ...) are part of the subgoal builders, so the checkers re-validate them. - EcPhlPr, EcPhlCoreView, EcPhlBdHoare, EcPhlHiBdHoare and EcPhlHoare are reduced to dispatchers and adapters; their interfaces are unchanged. Behaviour is preserved: on the new test, goals after every bridge tactic and the error messages of every failing invocation are identical to those of the unmodified build. A new test, tests/pr-bridges.ec, exercises every rule reachable from the surface syntax and the error paths (the procedure forms of the split rules are not reachable: `phoare split` cannot type its bounds on a procedure goal). The stdlib, the unit tests and the examples pass under EC_RECHECK=1 with no RecheckFailure. Each of the 14 checkers, when deliberately broken, is caught only under EC_RECHECK (on the new test, except the unreachable ones; on the stdlib where the rule is used there: hoareF-of-bdhoare 2 files, bdhoareS-of-hoare 9, bdhoareF-of-hoare 4, bdhoareF-pr 9, equivF-pr 8, bdhoareS-prbounded 6, bdhoareF-prbounded 4, bdhoareS-split-or 1). --- src/ecLowPhlGoal.ml | 9 + src/phl/ecPhlBdHoare.ml | 180 ++---------- src/phl/ecPhlCoreView.ml | 73 +---- src/phl/ecPhlHiBdHoare.ml | 79 +---- src/phl/ecPhlHoare.ml | 32 +-- src/phl/ecPhlPr.ml | 127 +-------- src/phl/rules/bdhoare/ecBdHoareOfHoare.ml | 83 ++++++ src/phl/rules/bdhoare/ecBdHoareOfHoare.mli | 45 +++ src/phl/rules/bdhoare/ecBdHoarePr.ml | 50 ++++ src/phl/rules/bdhoare/ecBdHoarePr.mli | 18 ++ src/phl/rules/bdhoare/ecBdHoarePrBounded.ml | 88 ++++++ src/phl/rules/bdhoare/ecBdHoarePrBounded.mli | 43 +++ src/phl/rules/bdhoare/ecBdHoareSplit.ml | 285 +++++++++++++++++++ src/phl/rules/bdhoare/ecBdHoareSplit.mli | 116 ++++++++ src/phl/rules/equiv/ecEquivPr.ml | 104 +++++++ src/phl/rules/equiv/ecEquivPr.mli | 40 +++ src/phl/rules/hoare/ecHoareOfBdHoare.ml | 59 ++++ src/phl/rules/hoare/ecHoareOfBdHoare.mli | 27 ++ src/phl/rules/hoare/ecHoarePr.ml | 8 + src/phl/rules/hoare/ecHoarePr.mli | 19 ++ src/phl/rules/hoare/ecHoareSplit.ml | 32 +++ src/phl/rules/hoare/ecHoareSplit.mli | 22 ++ tests/pr-bridges.ec | 281 ++++++++++++++++++ 23 files changed, 1372 insertions(+), 448 deletions(-) create mode 100644 src/phl/rules/bdhoare/ecBdHoareOfHoare.ml create mode 100644 src/phl/rules/bdhoare/ecBdHoareOfHoare.mli create mode 100644 src/phl/rules/bdhoare/ecBdHoarePr.ml create mode 100644 src/phl/rules/bdhoare/ecBdHoarePr.mli create mode 100644 src/phl/rules/bdhoare/ecBdHoarePrBounded.ml create mode 100644 src/phl/rules/bdhoare/ecBdHoarePrBounded.mli create mode 100644 src/phl/rules/bdhoare/ecBdHoareSplit.ml create mode 100644 src/phl/rules/bdhoare/ecBdHoareSplit.mli create mode 100644 src/phl/rules/equiv/ecEquivPr.ml create mode 100644 src/phl/rules/equiv/ecEquivPr.mli create mode 100644 src/phl/rules/hoare/ecHoareOfBdHoare.ml create mode 100644 src/phl/rules/hoare/ecHoareOfBdHoare.mli create mode 100644 src/phl/rules/hoare/ecHoarePr.ml create mode 100644 src/phl/rules/hoare/ecHoarePr.mli create mode 100644 src/phl/rules/hoare/ecHoareSplit.ml create mode 100644 src/phl/rules/hoare/ecHoareSplit.mli create mode 100644 tests/pr-bridges.ec diff --git a/src/ecLowPhlGoal.ml b/src/ecLowPhlGoal.ml index acfe87d868..42a45b169c 100644 --- a/src/ecLowPhlGoal.ml +++ b/src/ecLowPhlGoal.ml @@ -379,6 +379,15 @@ let hs_observes_exn (po : hs_inv) = (fun _ f -> not (f_equal (snd (decompose_lambda f)) f_true)) po.hsi_inv.exnmap +(* -------------------------------------------------------------------- *) +(* The argument of a call to [fun_], as passed to [Pr[fun_(...) @ &m : _]], + read off [arg], the value of its (tuple) argument variable. *) +let pr_args_of_fun (fun_ : function_) (arg : form) = + match fun_.f_sig.fs_anames with + | [] -> f_tt + | [_] -> arg + | lv -> f_tuple (List.mapi (fun i v -> f_proj arg i v.ov_type) lv) + (* -------------------------------------------------------------------- *) type logicS = [ | `Hoare of sHoareS diff --git a/src/phl/ecPhlBdHoare.ml b/src/phl/ecPhlBdHoare.ml index fa5fa52019..ebfea547b9 100644 --- a/src/phl/ecPhlBdHoare.ml +++ b/src/phl/ecPhlBdHoare.ml @@ -1,175 +1,27 @@ (* -------------------------------------------------------------------- *) open EcAst -open EcFol open EcCoreGoal -open EcLowGoal -open EcLowPhlGoal - -open EcPhlCoreView -open EcPhlConseq - -module TTC = EcProofTyping - -(* -------------------------------------------------------------------- *) -(* The top-level tactic *) -let t_hoare_bd_hoare tc = - let concl = FApi.tc1_goal tc in - - match concl.f_node with - | FbdHoareF bhf -> - if bhf.bhf_cmp = FHeq && f_equal (bhf_bd bhf).inv f_r0 - then t_hoare_of_bdhoareF tc - else - FApi.t_seqsub - (t_bdHoareF_conseq_bd FHeq {m=bhf.bhf_m; inv=f_r0}) - [FApi.t_try EcPhlAuto.t_pl_trivial; t_hoare_of_bdhoareF] - tc - - | FbdHoareS bhs -> - if bhs.bhs_cmp = FHeq && f_equal (bhs_bd bhs).inv f_r0 - then t_hoare_of_bdhoareS tc - else - FApi.t_seqsub - (t_bdHoareS_conseq_bd FHeq {m=fst bhs.bhs_m; inv=f_r0}) - [FApi.t_try EcPhlAuto.t_pl_trivial; t_hoare_of_bdhoareS] - tc - - | FhoareF _ -> t_bdhoare_of_hoareF tc - | FhoareS _ -> t_bdhoare_of_hoareS tc - - | _ -> tc_error !!tc "a hoare or phoare judgment was expected" - -(* -------------------------------------------------------------------- *) -type 'a split_t = { - as_bdh : proofenv -> form -> 'a * ss_inv * hoarecmp * ss_inv; - mk_bdh : 'a * ss_inv * hoarecmp * ss_inv -> form; -} - -type 'a destr_t = { - as_bop : proofenv -> ss_inv -> ss_inv * ss_inv; - mk_bop : ss_inv -> ss_inv -> ss_inv; -} - -(* -------------------------------------------------------------------- *) -let t_bdhoare_split_bop sp dt b1 b2 b3 tc = - let concl = FApi.tc1_goal tc in - let bh, po, cmp, bd = sp.as_bdh !!tc concl in - let a, b = dt.as_bop !!tc po in - - let g1 = sp.mk_bdh (bh, a, cmp, b1) in - let g2 = sp.mk_bdh (bh, b, cmp, b2) in - let g3 = sp.mk_bdh (bh, dt.mk_bop a b, hoarecmp_opp cmp, b3) in - let nb = map_ss_inv2 f_real_sub (map_ss_inv2 f_real_add b1 b2) b3 in - - assert (f_equal nb.inv bd.inv); - FApi.xmutate1 tc `BdHoareSplit [g1; g2; g3] (* -------------------------------------------------------------------- *) -let t_bdhoare_split_bop_conseq t_conseq_bd sp dt b1 b2 b3 tc = - let concl = FApi.tc1_goal tc in - let _, _, cmp, b = sp.as_bdh !!tc concl in - let nb = map_ss_inv2 f_real_sub (map_ss_inv2 f_real_add b1 b2) b3 in - let t_main = t_bdhoare_split_bop sp dt b1 b2 b3 in - - if f_equal nb.inv b.inv - then t_main tc - else FApi.t_seqsub (t_conseq_bd cmp nb) [t_id; t_main] tc - -(* -------------------------------------------------------------------- *) -let bdhoare_kind tc = +(* The rules behind the [hoare] tactic (views between hoare and + probability-0 bdhoare judgements) and the bdhoare [split] rules live in + [rules//]. This module only keeps the dispatcher and the legacy + positional entry points. *) +let t_hoare_bd_hoare (tc : tcenv1) = match (FApi.tc1_goal tc).f_node with - | FbdHoareS _ -> true - | FbdHoareF _ -> false - | _ -> tc_error !!tc "the conclusion should be a bdhoare judgment" - -(* -------------------------------------------------------------------- *) -let gen_S tactic = - let as_bdh pf f = - let bh = pf_as_bdhoareS pf f in - (bh, (bhs_po bh), bh.bhs_cmp, bhs_bd bh) - - and mk_bdh (bh, po, cmp, b) = - f_bdHoareS (snd bh.bhs_m) (bhs_pr bh) bh.bhs_s po cmp b in - - tactic t_bdHoareS_conseq_bd { as_bdh; mk_bdh; } - -(* -------------------------------------------------------------------- *) -let gen_F tactic = - let as_bdh pf f = - let bh = pf_as_bdhoareF pf f in - (bh, (bhf_po bh), bh.bhf_cmp, bhf_bd bh) in - - let mk_bdh (bh, po, cmp, b) = - f_bdHoareF (bhf_pr bh) bh.bhf_f po cmp b in - - tactic t_bdHoareF_conseq_bd { as_bdh; mk_bdh; } - -(* -------------------------------------------------------------------- *) -let and_dt = - let destr_and pf f = - try - let f1 = map_ss_inv1 (fun f -> fst (destr_and f)) f in - let f2 = map_ss_inv1 (fun f -> snd (destr_and f)) f in - (f1, f2) - with DestrError _ -> - tc_error pf "the postcondition must be a conjunction" - in - { as_bop = destr_and; mk_bop = map_ss_inv2 f_or; } - -let t_bdhoareS_and = gen_S t_bdhoare_split_bop_conseq and_dt -let t_bdhoareF_and = gen_F t_bdhoare_split_bop_conseq and_dt - -let t_bdhoare_and b1 b2 b3 tc = - if bdhoare_kind tc - then t_bdhoareS_and b1 b2 b3 tc - else t_bdhoareF_and b1 b2 b3 tc - -(* -------------------------------------------------------------------- *) -let or_dt = - let destr_or pf f = - try - let f1 = map_ss_inv1 (fun f -> fst (destr_or f)) f in - let f2 = map_ss_inv1 (fun f -> snd (destr_or f)) f in - (f1, f2) - with DestrError _ -> - tc_error pf "the postcondition must be a disjunction" - in - { as_bop = destr_or; mk_bop = map_ss_inv2 f_and; } - -let t_bdhoareS_or = gen_S t_bdhoare_split_bop_conseq or_dt -let t_bdhoareF_or = gen_F t_bdhoare_split_bop_conseq or_dt - -let t_bdhoare_or b1 b2 b3 tc = - if bdhoare_kind tc - then t_bdhoareS_or b1 b2 b3 tc - else t_bdhoareF_or b1 b2 b3 tc + | FbdHoareF _ -> EcBdHoareOfHoare.t_bdhoareF_of_hoare_full tc + | FbdHoareS _ -> EcBdHoareOfHoare.t_bdhoareS_of_hoare_full tc + | FhoareF _ -> EcHoareOfBdHoare.t_hoareF_of_bdhoare tc + | FhoareS _ -> EcHoareOfBdHoare.t_hoareS_of_bdhoare tc + | _ -> tc_error !!tc "a hoare or phoare judgment was expected" (* -------------------------------------------------------------------- *) -let t_bdhoare_split_not split b1 b2 tc = - let bh, po, cmp, bd = split.as_bdh !!tc (FApi.tc1_goal tc) in - let g1 = split.mk_bdh (bh, map_ss_inv1 (fun _ -> f_true) po, cmp, b1) in - let g2 = split.mk_bdh (bh, map_ss_inv1 f_not_simpl po, hoarecmp_opp cmp, b2) in - let nb = map_ss_inv2 f_real_sub b1 b2 in - - assert (f_equal nb.inv bd.inv); - FApi.xmutate1 tc `BdHoareSplit [g1; g2] - -let t_bdhoare_split_not_conseq t_conseq_bd split b1 b2 tc = - let hyps = FApi.tc1_hyps tc in - let _, _, cmp, b = split.as_bdh !!tc (FApi.tc1_goal tc) in - let nb = map_ss_inv2 f_real_sub b1 b2 in - let t_main = t_bdhoare_split_not split b1 b2 in +let t_bdhoare_and b1 b2 b3 = + EcBdHoareSplit.(t_bdhoare_split_and { bsb_b1 = b1; bsb_b2 = b2; bsb_b3 = b3; }) - if EcReduction.ss_inv_alpha_eq hyps nb b - then t_main tc - else FApi.t_seqsub (t_conseq_bd cmp nb) [t_id; t_main] tc - -(* -------------------------------------------------------------------- *) -let t_bdhoareS_not = gen_S t_bdhoare_split_not_conseq -let t_bdhoareF_not = gen_F t_bdhoare_split_not_conseq +let t_bdhoare_or b1 b2 b3 = + EcBdHoareSplit.(t_bdhoare_split_or { bsb_b1 = b1; bsb_b2 = b2; bsb_b3 = b3; }) -let t_bdhoare_not b1 b2 tc = - if bdhoare_kind tc - then t_bdhoareS_not b1 b2 tc - else t_bdhoareF_not b1 b2 tc +let t_bdhoare_not b1 b2 = + EcBdHoareSplit.(t_bdhoare_split_not { bnt_b1 = b1; bnt_b2 = b2; }) diff --git a/src/phl/ecPhlCoreView.ml b/src/phl/ecPhlCoreView.ml index 49022b9994..d3e837f6ae 100644 --- a/src/phl/ecPhlCoreView.ml +++ b/src/phl/ecPhlCoreView.ml @@ -1,65 +1,10 @@ (* -------------------------------------------------------------------- *) -open EcFol - -open EcCoreGoal -open EcLowPhlGoal -open EcAst - -(* -------------------------------------------------------------------- *) -let t_hoare_of_bdhoareS_r tc = - let bhs = tc1_as_bdhoareS tc in - if not (bhs.bhs_cmp = FHeq && f_equal (bhs_bd bhs).inv f_r0) then - tc_error !!tc "%s" "bound must be equal to 0%r"; - let post = (map_ss_inv1 f_not (bhs_po bhs)) in - let concl = - f_hoareS ( - snd bhs.bhs_m) - (bhs_pr bhs) - bhs.bhs_s - { hsi_m = post.m; hsi_inv = POE.empty post.inv; } - in - FApi.xmutate1 tc `ViewBdHoare [concl] - -(* -------------------------------------------------------------------- *) -let t_hoare_of_bdhoareF_r tc = - let bhf = tc1_as_bdhoareF tc in - if not (bhf.bhf_cmp = FHeq && f_equal (bhf_bd bhf).inv f_r0) then - tc_error !!tc "%s" "bound must be equal to 0%r"; - let post = map_ss_inv1 f_not (bhf_po bhf) in - let concl = - f_hoareF - (bhf_pr bhf) bhf.bhf_f - { hsi_m = post.m; hsi_inv = POE.empty post.inv; } - in - FApi.xmutate1 tc `ViewBdHoare [concl] - -(* -------------------------------------------------------------------- *) -let t_bdhoare_of_hoareS_r tc = - let hs = tc1_as_hoareS tc in - let { main = inv } as post = (hs_po hs).hsi_inv in - if not (POE.is_empty post) then - tc_error !!tc "Exceptions are not permitted"; - let m = (hs_po hs).hsi_m in - let concl = - f_bdHoareS - (snd hs.hs_m) (hs_pr hs) hs.hs_s - (map_ss_inv1 f_not {m;inv}) FHeq { m = fst hs.hs_m; inv = f_r0; } - in - FApi.xmutate1 tc `ViewBdHoare [concl] - -(* -------------------------------------------------------------------- *) -let t_bdhoare_of_hoareF_r tc = - let hf = tc1_as_hoareF tc in - let { main = inv } as post = (hf_po hf).hsi_inv in - if not (POE.is_empty post) then - tc_error !!tc "Exceptions are not permitted"; - let m = (hf_po hf).hsi_m in - let concl = - f_bdHoareF (hf_pr hf) hf.hf_f (map_ss_inv1 f_not {m;inv}) FHeq {m=hf.hf_m;inv=f_r0} in - FApi.xmutate1 tc `ViewBdHoare [concl] - -(* -------------------------------------------------------------------- *) -let t_hoare_of_bdhoareS = FApi.t_low0 "hoare-bdhoareS" t_hoare_of_bdhoareS_r -let t_hoare_of_bdhoareF = FApi.t_low0 "hoare-bdhoareF" t_hoare_of_bdhoareF_r -let t_bdhoare_of_hoareS = FApi.t_low0 "bdhoare-hoareS" t_bdhoare_of_hoareS_r -let t_bdhoare_of_hoareF = FApi.t_low0 "bdhoare-hoareF" t_bdhoare_of_hoareF_r +(* The views between hoare and probability-0 bdhoare judgements live in + [rules/hoare/ecHoareOfBdHoare] (a hoare goal from a bdhoare premise) + and [rules/bdhoare/ecBdHoareOfHoare] (a bdhoare goal from a hoare + premise). This module only keeps the legacy entry points, named after + the goal they turn into: [t_hoare_of_bdhoare*] acts on a bdhoare goal. *) +let t_hoare_of_bdhoareS = EcBdHoareOfHoare.t_bdhoareS_of_hoare +let t_hoare_of_bdhoareF = EcBdHoareOfHoare.t_bdhoareF_of_hoare +let t_bdhoare_of_hoareS = EcHoareOfBdHoare.t_hoareS_of_bdhoare +let t_bdhoare_of_hoareF = EcHoareOfBdHoare.t_hoareF_of_bdhoare diff --git a/src/phl/ecPhlHiBdHoare.ml b/src/phl/ecPhlHiBdHoare.ml index e0a0e20454..a698e8c6bd 100644 --- a/src/phl/ecPhlHiBdHoare.ml +++ b/src/phl/ecPhlHiBdHoare.ml @@ -1,77 +1,4 @@ (* -------------------------------------------------------------------- *) -open EcUtils -open EcTypes -open EcFol -open EcAst - -open EcCoreGoal -open EcLowGoal - -module TTC = EcProofTyping - -(* -------------------------------------------------------------------- *) -let process_bdhoare_split info tc = - let _, concl = FApi.tc1_flat tc in - - let pr, po = - match concl.f_node with - | FbdHoareS bhs -> - (bhs_pr bhs, bhs_po bhs) - - | FbdHoareF bhf -> - (bhf_pr bhf, bhf_po bhf) - - | _ -> - tc_error !!tc "the conclusion must be a bdhoare judgment" in - - match info with - | EcParsetree.BDH_split_bop (b1, b2, b3) -> - let t = - if is_and po.inv then EcPhlBdHoare.t_bdhoare_and - else if is_or po.inv then EcPhlBdHoare.t_bdhoare_or - else - tc_error !!tc - "the postcondition must be a conjunction or a disjunction" - in - let _,b1 = TTC.tc1_process_Xhl_form tc treal b1 in - let _,b2 = TTC.tc1_process_Xhl_form tc treal b2 in - let b3 = b3 |> omap (fun f -> snd ( TTC.tc1_process_Xhl_form tc treal f)) |> odfl {m=b1.m;inv=f_r0} in - - t b1 b2 b3 tc - - | EcParsetree.BDH_split_or_case (b1, b2, f) -> - let _, b1 = TTC.tc1_process_Xhl_form tc treal b1 in - let _, b2 = TTC.tc1_process_Xhl_form tc treal b2 in - let _, f = TTC.tc1_process_Xhl_formula tc f in - - let t_conseq po lemma tactic = - let rwtt tc = - let pt = ptglobal ~tys:[] lemma in - - let rwtt = [ - EcLowGoal.t_intros_i [EcIdent.create "_"]; - EcHiGoal.LowRewrite.t_rewrite (`LtoR, None, None) pt; - t_true; - ] in FApi.t_seqs rwtt tc - in - - FApi.t_seqsub - (EcPhlConseq.t_conseq (Inv_ss pr) (Inv_ss po)) - [t_true; rwtt; tactic] - in - - t_conseq - (map_ss_inv2 f_or (map_ss_inv2 f_and f po) (map_ss_inv2 f_and (map_ss_inv1 f_not f) po)) - (EcCoreLib.CI_Logic.mk_logic "orDandN") - (FApi.t_on1seq 3 - (EcPhlBdHoare.t_bdhoare_or b1 b2 {m=b1.m;inv=f_r0}) - (t_conseq - {inv=f_false;m=b1.m} - (EcCoreLib.CI_Logic.mk_logic "andDorN") - EcHiGoal.process_trivial)) - tc - - | EcParsetree.BDH_split_not (b1, b2) -> - let _,b2 = TTC.tc1_process_Xhl_form tc treal b2 in - let b1 = b1 |> omap (fun f -> snd (TTC.tc1_process_Xhl_form tc treal f)) |> odfl {m=b2.m;inv=f_r1} in - EcPhlBdHoare.t_bdhoare_not b1 b2 tc +(* The elaboration of [phoare split] lives in [rules/bdhoare/ecBdHoareSplit]. + This module only keeps the legacy entry point. *) +let process_bdhoare_split = EcBdHoareSplit.process_bdhoare_split diff --git a/src/phl/ecPhlHoare.ml b/src/phl/ecPhlHoare.ml index 7394fa5556..46c68065aa 100644 --- a/src/phl/ecPhlHoare.ml +++ b/src/phl/ecPhlHoare.ml @@ -1,30 +1,6 @@ (* ------------------------------------------------------------------------ *) -open EcUtils -open EcAst -open EcFol -open EcLowPhlGoal -open EcCoreGoal +(* Splitting a hoare postcondition lives in [rules/hoare/ecHoareSplit]. This + module only keeps the legacy entry points. *) +let t_hoaresplit = EcHoareSplit.t_hoare_split -(* ------------------------------------------------------------------------ *) -let t_hoaresplit (tc : tcenv1) = - let hoare = tc1_as_hoareS tc in - let pre = hs_pr hoare in - let post = POE.lower (hs_po hoare) in - - match sform_of_form post.inv with - | SFand (`Sym, (f1, f2)) -> - let dp = map_ss_inv2 f_and pre pre in - let cl = update_hs_ss { post with inv = f1 } (hs_po hoare) in - let cr = update_hs_ss { post with inv = f2 } (hs_po hoare) in - - EcPhlConseq.t_hoareS_conseq dp (hs_po hoare) tc - |> FApi.t_firsts EcHiGoal.process_done 2 - |> FApi.as_tcenv1 - |> EcPhlConseq.t_hoareS_conseq_conj (hs_pr hoare) cr (hs_pr hoare) cl - - | _ -> - tc_error !!tc "post-condition should be a conjunction" - -(* ------------------------------------------------------------------------ *) -let process_hoaresplit (tc : tcenv1) = - t_hoaresplit tc +let process_hoaresplit = EcHoareSplit.t_hoare_split diff --git a/src/phl/ecPhlPr.ml b/src/phl/ecPhlPr.ml index 592f0635ae..e359af9c1b 100644 --- a/src/phl/ecPhlPr.ml +++ b/src/phl/ecPhlPr.ml @@ -1,129 +1,24 @@ (* -------------------------------------------------------------------- *) -open EcUtils -open EcModules -open EcFol -open EcEnv -open EcAst -open EcCoreGoal open EcLowPhlGoal -open EcSubst - -module TTC = EcProofTyping - -(* -------------------------------------------------------------------- *) -let to_args fun_ arg = - match fun_.f_sig.fs_anames with - | [] -> f_tt - | [_] -> arg - | lv -> f_tuple (List.mapi (fun i v -> f_proj arg i v.ov_type) lv) - -(* -------------------------------------------------------------------- *) -let t_bdhoare_ppr_r tc = - let env = FApi.tc1_env tc in - let bhf = tc1_as_bdhoareF tc in - let f_xpath = bhf.bhf_f in - let fun_ = EcEnv.Fun.by_xpath f_xpath env in - let penv,_qenv = EcEnv.Fun.hoareF_memenv bhf.bhf_m f_xpath env in - let m = EcIdent.create "&hr" in - let args = map_ss_inv1 (to_args fun_) (f_pvarg fun_.f_sig.fs_arg m) in - let pre,post = (bhf_pr bhf), (bhf_po bhf) in - let fop = match bhf.bhf_cmp with - | FHle -> f_real_le - | FHge -> fun x y -> f_real_le y x - | FHeq -> f_eq - in - let bd = ss_inv_rebind (bhf_bd bhf) m in - let concl = map_ss_inv2 fop (map_ss_inv1 (fun args -> f_pr m f_xpath args post) args) - bd in - let pre = ss_inv_rebind pre m in - let concl = map_ss_inv2 f_imp pre concl in - let concl = map_ss_inv2 f_and (map_ss_inv1 (f_real_le f_r0) bd) concl in - let concl = EcSubst.f_forall_mems_ss_inv (m,snd penv) concl in - FApi.xmutate1 tc `PPR [concl] - -(* -------------------------------------------------------------------- *) -let t_hoare_ppr_r tc = - ignore (tc1_as_hoareF tc); - FApi.t_seq EcPhlCoreView.t_bdhoare_of_hoareF t_bdhoare_ppr_r tc (* -------------------------------------------------------------------- *) -let t_equiv_ppr_r ty phi_l phi_r tc = - let env = FApi.tc1_env tc in - let ef = tc1_as_equivF tc in - let (fl, fr) = (ef.ef_fl, ef.ef_fr) in - let funl = EcEnv.Fun.by_xpath fl env in - let funr = EcEnv.Fun.by_xpath fr env in - let (penvl,penvr), (qenvl,qenvr) = EcEnv.Fun.equivF_memenv ef.ef_ml ef.ef_mr fl fr env in - let m = EcIdent.create "&hr" in - let argsl = map_ss_inv1 (to_args funl) (f_pvarg funl.f_sig.fs_arg (fst penvl)) in - let argsr = map_ss_inv1 (to_args funr) (f_pvarg funr.f_sig.fs_arg (fst penvr)) in - let a_id = EcIdent.create "a" in - let a_f = f_local a_id ty in - let pr1_ev = EcSubst.ss_inv_rebind (map_ss_inv1 (fun p -> f_eq p a_f) phi_l) m in - let pr1 = f_pr (fst penvl) fl argsl.inv pr1_ev in - let pr2_ev = EcSubst.ss_inv_rebind (map_ss_inv1 (fun p -> f_eq p a_f) phi_r) m in - let pr2 = f_pr (fst penvr) fr argsr.inv pr2_ev in - let concl_pr = - f_forall_mems_ts_inv penvl penvr - (map_ts_inv1 (f_forall_simpl [a_id,GTty ty]) - (map_ts_inv1 (fun pr -> f_imp_simpl pr (f_eq_simpl pr1 pr2)) (ef_pr ef))) in - let phi_l = ss_inv_generalize_as_left phi_l ef.ef_ml ef.ef_mr in - let phi_r = ss_inv_generalize_as_right phi_r ef.ef_ml ef.ef_mr in - let concl_po = f_forall_mems_ts_inv qenvl qenvr (map_ts_inv3 (fun phi_l phi_r po -> - (f_forall_simpl [a_id, GTty ty] - (f_imps_simpl [f_eq phi_l a_f;f_eq phi_r a_f] po))) phi_l phi_r (ef_po ef)) in - FApi.xmutate1 tc `PPR [concl_po; concl_pr] +(* The [pr] rules (bdhoare, equiv) and the [prbounded] rules live in + [rules//]; the hoare [pr] tactic is derived. This module only + keeps the dispatcher and the legacy entry points. *) +let t_hoare_ppr = EcHoarePr.t_hoareF_pr +let t_bdhoare_ppr = EcBdHoarePr.t_bdhoareF_pr -(* -------------------------------------------------------------------- *) -let t_hoare_ppr = FApi.t_low0 "hoare-ppr" t_hoare_ppr_r -let t_bdhoare_ppr = FApi.t_low0 "bdhoare-ppr" t_bdhoare_ppr_r -let t_equiv_ppr = FApi.t_low3 "equiv-ppr" t_equiv_ppr_r +let t_equiv_ppr ty phi_l phi_r = + EcEquivPr.(t_equivF_pr { epr_ty = ty; epr_left = phi_l; epr_right = phi_r; }) (* -------------------------------------------------------------------- *) let process_ppr info tc = match info with | None -> - t_hF_or_bhF_or_eF ~th:t_hoare_ppr ~tbh:t_bdhoare_ppr tc + t_hF_or_bhF_or_eF ~th:t_hoare_ppr ~tbh:t_bdhoare_ppr tc - | Some (phi1, phi2) -> - let hyps = FApi.tc1_hyps tc in - let ef = tc1_as_equivF tc in - let qenvl = snd (LDecl.hoareF ef.ef_ml ef.ef_fl hyps) in - let qenvr = snd (LDecl.hoareF ef.ef_mr ef.ef_fr hyps) in - let phi1 = TTC.pf_process_form_opt !!tc qenvl None phi1 in - let phi2 = TTC.pf_process_form_opt !!tc qenvr None phi2 in - if not (EcReduction.EqTest.for_type (LDecl.toenv hyps) phi1.f_ty phi2.f_ty) then - tc_error !!tc "formulas must have convertible types"; - t_equiv_ppr phi1.f_ty {m=ef.ef_ml;inv=phi1} {m=ef.ef_mr;inv=phi2} tc + | Some phis -> + EcEquivPr.process_equivF_pr phis tc (* -------------------------------------------------------------------- *) -let t_prbounded_r conseq tc = - let (env, _, concl) = FApi.tc1_eflat tc in - - let (m, pr, po, cmp, bd) = - match concl.f_node with - | FbdHoareF hf -> - let m = fst (Fun.hoareF_memenv hf.bhf_m hf.bhf_f env) in - (m, bhf_pr hf, bhf_po hf, hf.bhf_cmp, bhf_bd hf) - - | FbdHoareS hf -> - (hf.bhs_m, bhs_pr hf, bhs_po hf, hf.bhs_cmp, bhs_bd hf) - - | _ -> tc_error_noXhl ~kinds:[`PHoare `Any] !!tc - in - - let cond = - (* FIXME: use the [conseq] result when possible *) - match cmp with - | FHle when f_equal bd.inv f_r1 -> [] - | FHge when f_equal bd.inv f_r0 -> [] - | _ when f_equal po.inv f_false && f_equal bd.inv f_r0 -> [] - | FHle when conseq -> [f_forall_mems_ss_inv m (map_ss_inv2 f_imp pr (map_ss_inv2 f_real_le {m=fst m;inv=f_r1} bd))] - | FHge when conseq -> [f_forall_mems_ss_inv m (map_ss_inv2 f_imp pr (map_ss_inv2 f_real_le bd {m=fst m;inv=f_r0}))] - - | _ -> tc_error !!tc "cannot solve the probabilistic judgement" - in - - FApi.xmutate1 tc `PrBounded cond - -let t_prbounded = FApi.t_low1 "pr-bounded" t_prbounded_r +let t_prbounded conseq = EcBdHoarePrBounded.t_bdhoare_prbounded ~conseq diff --git a/src/phl/rules/bdhoare/ecBdHoareOfHoare.ml b/src/phl/rules/bdhoare/ecBdHoareOfHoare.ml new file mode 100644 index 0000000000..440de139a1 --- /dev/null +++ b/src/phl/rules/bdhoare/ecBdHoareOfHoare.ml @@ -0,0 +1,83 @@ +(* -------------------------------------------------------------------- *) +open EcFol +open EcAst + +open EcCoreGoal +open EcLowPhlGoal + +(* -------------------------------------------------------------------- *) +(* The rules deriving a probability-0 judgement from a hoare one have no + parameters. *) +type EcCoreGoal.rule += + | RBdHoareSOfHoare + | RBdHoareFOfHoare + +(* -------------------------------------------------------------------- *) +(* The goal states that its postcondition has probability exactly 0. *) +let is_eq_zero (cmp : hoarecmp) (bd : ss_inv) = + cmp = FHeq && f_equal bd.inv f_r0 + +(* Pure cores shared by the rules and their checkers. The side condition + (the bound is [= 0%r]) is part of them, so the checker re-validates it. *) +let bdhoareS_of_hoare_subgoals (bhs : bdHoareS) : form list = + if not (is_eq_zero bhs.bhs_cmp (bhs_bd bhs)) then + failwith "bdhoareS-of-hoare: the bound is not = 0%r"; + let post = map_ss_inv1 f_not (bhs_po bhs) in + [f_hoareS (snd bhs.bhs_m) (bhs_pr bhs) bhs.bhs_s + { hsi_m = post.m; hsi_inv = POE.empty post.inv; }] + +let bdhoareF_of_hoare_subgoals (bhf : bdHoareF) : form list = + if not (is_eq_zero bhf.bhf_cmp (bhf_bd bhf)) then + failwith "bdhoareF-of-hoare: the bound is not = 0%r"; + let post = map_ss_inv1 f_not (bhf_po bhf) in + [f_hoareF (bhf_pr bhf) bhf.bhf_f + { hsi_m = post.m; hsi_inv = POE.empty post.inv; }] + +(* -------------------------------------------------------------------- *) +let not_eq_zero tc = tc_error !!tc "%s" "bound must be equal to 0%r" + +(* Rules (TCB). *) +let t_bdhoareS_of_hoare (tc : tcenv1) = + let bhs = tc1_as_bdhoareS tc in + if not (is_eq_zero bhs.bhs_cmp (bhs_bd bhs)) then not_eq_zero tc; + FApi.xrule1 tc RBdHoareSOfHoare (bdhoareS_of_hoare_subgoals bhs) + +let t_bdhoareF_of_hoare (tc : tcenv1) = + let bhf = tc1_as_bdhoareF tc in + if not (is_eq_zero bhf.bhf_cmp (bhf_bd bhf)) then not_eq_zero tc; + FApi.xrule1 tc RBdHoareFOfHoare (bdhoareF_of_hoare_subgoals bhf) + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | RBdHoareSOfHoare -> + Some (EcPlRecheck.checker_of "bdhoareS-of-hoare" pf_as_bdhoareS + (fun _hyps bhs -> bdhoareS_of_hoare_subgoals bhs)) + | RBdHoareFOfHoare -> + Some (EcPlRecheck.checker_of "bdhoareF-of-hoare" pf_as_bdhoareF + (fun _hyps bhf -> bdhoareF_of_hoare_subgoals bhf)) + | _ -> None) + +(* -------------------------------------------------------------------- *) +(* Derived (no proof-node): unless the bound already is [= 0%r], first + turn the goal into [phoare [...] = 0%r] with the bound-changing + consequence, try to close its side condition, then apply the rule. + + TEMPORARY: the bound-changing consequence still comes from the + not-yet-migrated [EcPhlConseq]. *) +let t_bdhoareS_of_hoare_full (tc : tcenv1) = + let bhs = tc1_as_bdhoareS tc in + if is_eq_zero bhs.bhs_cmp (bhs_bd bhs) then t_bdhoareS_of_hoare tc else + FApi.t_seqsub + (EcPhlConseq.t_bdHoareS_conseq_bd FHeq { m = fst bhs.bhs_m; inv = f_r0; }) + [FApi.t_try EcPhlAuto.t_pl_trivial; t_bdhoareS_of_hoare] + tc + +let t_bdhoareF_of_hoare_full (tc : tcenv1) = + let bhf = tc1_as_bdhoareF tc in + if is_eq_zero bhf.bhf_cmp (bhf_bd bhf) then t_bdhoareF_of_hoare tc else + FApi.t_seqsub + (EcPhlConseq.t_bdHoareF_conseq_bd FHeq { m = bhf.bhf_m; inv = f_r0; }) + [FApi.t_try EcPhlAuto.t_pl_trivial; t_bdhoareF_of_hoare] + tc diff --git a/src/phl/rules/bdhoare/ecBdHoareOfHoare.mli b/src/phl/rules/bdhoare/ecBdHoareOfHoare.mli new file mode 100644 index 0000000000..b1b5db541b --- /dev/null +++ b/src/phl/rules/bdhoare/ecBdHoareOfHoare.mli @@ -0,0 +1,45 @@ +(* -------------------------------------------------------------------- *) +open EcCoreGoal.FApi + +(* ==================================================================== *) +(* Rules (trusted) *) + +(* [t_bdhoareS_of_hoare] — an event has probability 0 when its negation + always holds: + + hoare [c : P ==> !Q] + ---------------------------- + phoare [c : P ==> Q] = 0%r + + Side condition: the goal's bound is syntactically [= 0%r] (otherwise + fails). + + Node: [RBdHoareSOfHoare]. Checker: "bdhoareS-of-hoare". *) +val t_bdhoareS_of_hoare : backward + +(* [t_bdhoareF_of_hoare] — same for a procedure: + + hoare [f : P ==> !Q] + ---------------------------- + phoare [f : P ==> Q] = 0%r + + Node: [RBdHoareFOfHoare]. Checker: "bdhoareF-of-hoare". *) +val t_bdhoareF_of_hoare : backward + +(* ==================================================================== *) +(* Derived tactics *) + +(* [t_bdhoareS_of_hoare_full] — on [phoare [c : P ==> Q] ~ d]: + 1. unless [~ d] is syntactically [= 0%r], the bound-changing consequence + (currently [EcPhlConseq.t_bdHoareS_conseq_bd]) to + [phoare [c : P ==> Q] = 0%r], whose side condition (relating [~ d] to + [= 0%r]) is closed when [EcPhlAuto.t_pl_trivial] does, and left open + otherwise; + 2. then [t_bdhoareS_of_hoare]. + Visible goals: the bound side condition if not closed, then + [hoare [c : P ==> !Q]]. Emits no node of its own. *) +val t_bdhoareS_of_hoare_full : backward + +(* [t_bdhoareF_of_hoare_full] — same for a procedure, with + [EcPhlConseq.t_bdHoareF_conseq_bd] and [t_bdhoareF_of_hoare]. *) +val t_bdhoareF_of_hoare_full : backward diff --git a/src/phl/rules/bdhoare/ecBdHoarePr.ml b/src/phl/rules/bdhoare/ecBdHoarePr.ml new file mode 100644 index 0000000000..bc67d2d434 --- /dev/null +++ b/src/phl/rules/bdhoare/ecBdHoarePr.ml @@ -0,0 +1,50 @@ +(* -------------------------------------------------------------------- *) +open EcFol +open EcAst +open EcEnv +open EcSubst + +open EcCoreGoal +open EcLowPhlGoal + +(* -------------------------------------------------------------------- *) +(* The bdhoare [pr] rule has no parameters. *) +type EcCoreGoal.rule += RBdHoareFPr + +(* -------------------------------------------------------------------- *) +(* Pure core shared by the rule and its checker. The memory [&m] the + premise quantifies over is fresh at each call: the checker compares up + to alpha-conversion. *) +let bdhoareF_pr_subgoals (hyps : LDecl.hyps) (bhf : bdHoareF) : form list = + let env = LDecl.toenv hyps in + let fun_ = Fun.by_xpath bhf.bhf_f env in + let penv, _ = Fun.hoareF_memenv bhf.bhf_m bhf.bhf_f env in + let m = EcIdent.create "&hr" in + let args = map_ss_inv1 (pr_args_of_fun fun_) (f_pvarg fun_.f_sig.fs_arg m) in + let fop = + match bhf.bhf_cmp with + | FHle -> f_real_le + | FHge -> fun x y -> f_real_le y x + | FHeq -> f_eq + in + let bd = ss_inv_rebind (bhf_bd bhf) m in + let pr = map_ss_inv1 (fun args -> f_pr m bhf.bhf_f args (bhf_po bhf)) args in + let concl = map_ss_inv2 fop pr bd in + let concl = map_ss_inv2 f_imp (ss_inv_rebind (bhf_pr bhf) m) concl in + let concl = map_ss_inv2 f_and (map_ss_inv1 (f_real_le f_r0) bd) concl in + [f_forall_mems_ss_inv (m, snd penv) concl] + +(* -------------------------------------------------------------------- *) +(* Rule (TCB). *) +let t_bdhoareF_pr (tc : tcenv1) = + let bhf = tc1_as_bdhoareF tc in + FApi.xrule1 tc RBdHoareFPr (bdhoareF_pr_subgoals (FApi.tc1_hyps tc) bhf) + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | RBdHoareFPr -> + Some (EcPlRecheck.checker_of "bdhoareF-pr" pf_as_bdhoareF + (fun hyps bhf -> bdhoareF_pr_subgoals hyps bhf)) + | _ -> None) diff --git a/src/phl/rules/bdhoare/ecBdHoarePr.mli b/src/phl/rules/bdhoare/ecBdHoarePr.mli new file mode 100644 index 0000000000..ad45fa8ada --- /dev/null +++ b/src/phl/rules/bdhoare/ecBdHoarePr.mli @@ -0,0 +1,18 @@ +(* -------------------------------------------------------------------- *) +open EcCoreGoal.FApi + +(* ==================================================================== *) +(* Rules (trusted) *) + +(* [t_bdhoareF_pr] — a probabilistic judgement on a procedure from the + probability of its postcondition, with [~] the goal's comparison: + + forall &m, 0%r <= d /\ (P => Pr[f(args) @ &m : Q] [~] d) + ------------------------------------------------------- + phoare [f : P ==> Q] ~ d + + where [args] are the arguments of [f] read in [&m], and [x [~] d] is + [x <= d] for [<=], [x = d] for [=] and [d <= x] for [>=]. + + Node: [RBdHoareFPr]. Checker: "bdhoareF-pr". *) +val t_bdhoareF_pr : backward diff --git a/src/phl/rules/bdhoare/ecBdHoarePrBounded.ml b/src/phl/rules/bdhoare/ecBdHoarePrBounded.ml new file mode 100644 index 0000000000..bbce7d228b --- /dev/null +++ b/src/phl/rules/bdhoare/ecBdHoarePrBounded.ml @@ -0,0 +1,88 @@ +(* -------------------------------------------------------------------- *) +open EcFol +open EcAst +open EcEnv + +open EcCoreGoal +open EcLowPhlGoal + +(* -------------------------------------------------------------------- *) +(* The bdhoare [prbounded] rules have no parameters. *) +type EcCoreGoal.rule += + | RBdHoareSPrBounded + | RBdHoareFPrBounded + +(* -------------------------------------------------------------------- *) +(* The judgement holds for every program: a probability is at most [1%r], + at least [0%r], and is [0%r] for the [false] event. *) +let is_trivial (cmp : hoarecmp) (po : ss_inv) (bd : ss_inv) = + match cmp with + | FHle when f_equal bd.inv f_r1 -> true + | FHge when f_equal bd.inv f_r0 -> true + | _ -> f_equal po.inv f_false && f_equal bd.inv f_r0 + +(* Pure core shared by the rules and their checkers, over the memory [m] + the premise quantifies over. Its side condition (the judgement is + trivial, or the comparison is [<=] or [>=]) is part of it, so the + checker re-validates it. *) +let prbounded_subgoals + (m : memenv) (pr : ss_inv) (po : ss_inv) (cmp : hoarecmp) (bd : ss_inv) += + let one = { m = fst m; inv = f_r1; } in + let zero = { m = fst m; inv = f_r0; } in + if is_trivial cmp po bd then [] else + match cmp with + | FHle -> + [EcSubst.f_forall_mems_ss_inv m + (map_ss_inv2 f_imp pr (map_ss_inv2 f_real_le one bd))] + | FHge -> + [EcSubst.f_forall_mems_ss_inv m + (map_ss_inv2 f_imp pr (map_ss_inv2 f_real_le bd zero))] + | FHeq -> + failwith "bdhoare-prbounded: non-trivial judgement with = bound" + +let bdhoareS_prbounded_subgoals (bhs : bdHoareS) : form list = + prbounded_subgoals bhs.bhs_m (bhs_pr bhs) (bhs_po bhs) bhs.bhs_cmp (bhs_bd bhs) + +let bdhoareF_prbounded_subgoals (hyps : LDecl.hyps) (bhf : bdHoareF) = + let m = fst (Fun.hoareF_memenv bhf.bhf_m bhf.bhf_f (LDecl.toenv hyps)) in + prbounded_subgoals m (bhf_pr bhf) (bhf_po bhf) bhf.bhf_cmp (bhf_bd bhf) + +(* -------------------------------------------------------------------- *) +(* The rule applies to a non-trivial judgement only when the caller allows + a premise ([conseq]), and never to an [=] one. *) +let check_applies tc ~conseq cmp po bd = + if not (is_trivial cmp po bd || (conseq && cmp <> FHeq)) then + tc_error !!tc "cannot solve the probabilistic judgement" + +(* Rules (TCB). *) +let t_bdhoareS_prbounded ~(conseq : bool) (tc : tcenv1) = + let bhs = tc1_as_bdhoareS tc in + check_applies tc ~conseq bhs.bhs_cmp (bhs_po bhs) (bhs_bd bhs); + FApi.xrule1 tc RBdHoareSPrBounded (bdhoareS_prbounded_subgoals bhs) + +let t_bdhoareF_prbounded ~(conseq : bool) (tc : tcenv1) = + let bhf = tc1_as_bdhoareF tc in + check_applies tc ~conseq bhf.bhf_cmp (bhf_po bhf) (bhf_bd bhf); + FApi.xrule1 tc RBdHoareFPrBounded + (bdhoareF_prbounded_subgoals (FApi.tc1_hyps tc) bhf) + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | RBdHoareSPrBounded -> + Some (EcPlRecheck.checker_of "bdhoareS-prbounded" pf_as_bdhoareS + (fun _hyps bhs -> bdhoareS_prbounded_subgoals bhs)) + | RBdHoareFPrBounded -> + Some (EcPlRecheck.checker_of "bdhoareF-prbounded" pf_as_bdhoareF + (fun hyps bhf -> bdhoareF_prbounded_subgoals hyps bhf)) + | _ -> None) + +(* -------------------------------------------------------------------- *) +(* Dispatcher (no node of its own). *) +let t_bdhoare_prbounded ~(conseq : bool) (tc : tcenv1) = + match (FApi.tc1_goal tc).f_node with + | FbdHoareF _ -> t_bdhoareF_prbounded ~conseq tc + | FbdHoareS _ -> t_bdhoareS_prbounded ~conseq tc + | _ -> tc_error_noXhl ~kinds:[`PHoare `Any] !!tc diff --git a/src/phl/rules/bdhoare/ecBdHoarePrBounded.mli b/src/phl/rules/bdhoare/ecBdHoarePrBounded.mli new file mode 100644 index 0000000000..fafb9227ad --- /dev/null +++ b/src/phl/rules/bdhoare/ecBdHoarePrBounded.mli @@ -0,0 +1,43 @@ +(* -------------------------------------------------------------------- *) +open EcCoreGoal.FApi + +(* ==================================================================== *) +(* Rules (trusted) *) + +(* [t_bdhoareS_prbounded ~conseq] — a probability lies in [[0%r, 1%r]], + and the probability of [false] is [0%r]: + + ------------------------------ --------------------------------- + phoare [c : P ==> Q] <= 1%r phoare [c : P ==> Q] >= 0%r + + --------------------------------- (~ any comparison) + phoare [c : P ==> false] ~ 0%r + + and, more generally, for a bound that is not syntactically one of the + above: + + forall &m, P => 1%r <= d forall &m, P => d <= 0%r + ------------------------------ --------------------------------- + phoare [c : P ==> Q] <= d phoare [c : P ==> Q] >= d + + The bounds [0%r], [1%r] and the postcondition [false] are matched + syntactically. Side condition: one of the premise-free forms applies, + or the comparison is [<=] or [>=] (otherwise fails). With + [~conseq:false], the premise forms are not used (the tactic fails + instead). + + Node: [RBdHoareSPrBounded]. Checker: "bdhoareS-prbounded". *) +val t_bdhoareS_prbounded : conseq:bool -> backward + +(* [t_bdhoareF_prbounded ~conseq] — same for a procedure (the premise + quantifies over its initial memory). + + Node: [RBdHoareFPrBounded]. Checker: "bdhoareF-prbounded". *) +val t_bdhoareF_prbounded : conseq:bool -> backward + +(* ==================================================================== *) +(* Derived tactics *) + +(* [t_bdhoare_prbounded ~conseq] — [t_bdhoareS_prbounded ~conseq] or + [t_bdhoareF_prbounded ~conseq], depending on the goal. *) +val t_bdhoare_prbounded : conseq:bool -> backward diff --git a/src/phl/rules/bdhoare/ecBdHoareSplit.ml b/src/phl/rules/bdhoare/ecBdHoareSplit.ml new file mode 100644 index 0000000000..9ef8c39097 --- /dev/null +++ b/src/phl/rules/bdhoare/ecBdHoareSplit.ml @@ -0,0 +1,285 @@ +(* -------------------------------------------------------------------- *) +open EcUtils +open EcTypes +open EcFol +open EcAst +open EcEnv +open EcSubst + +open EcCoreGoal +open EcLowGoal +open EcLowPhlGoal + +module TTC = EcProofTyping + +(* -------------------------------------------------------------------- *) +(* Parameters of the bdhoare [split] rules: the bounds of the premises. + Already typed, nothing to resolve: the same records are the rule + arguments and the node payloads. *) +type bdhoare_split_bop = { + bsb_b1 : ss_inv; (* bound for the left operand *) + bsb_b2 : ss_inv; (* bound for the right operand *) + bsb_b3 : ss_inv; (* opposite bound for the dual connective *) +} + +type bdhoare_split_not = { + bnt_b1 : ss_inv; (* bound for [true] *) + bnt_b2 : ss_inv; (* opposite bound for the negated postcondition *) +} + +type EcCoreGoal.rule += + | RBdHoareSSplitAnd of bdhoare_split_bop + | RBdHoareFSplitAnd of bdhoare_split_bop + | RBdHoareSSplitOr of bdhoare_split_bop + | RBdHoareFSplitOr of bdhoare_split_bop + | RBdHoareSSplitNot of bdhoare_split_not + | RBdHoareFSplitNot of bdhoare_split_not + +(* -------------------------------------------------------------------- *) +(* What the split rules read from a statement or procedure judgement: + its memory, postcondition, comparison and bound, and how to restate it + (same program and precondition) with another postcondition and bound. *) +type bdhoare_view = { + bv_m : memory; + bv_po : ss_inv; + bv_cmp : hoarecmp; + bv_bd : ss_inv; + bv_mk : ss_inv -> hoarecmp -> ss_inv -> form; +} + +let view_S (bhs : bdHoareS) = { + bv_m = fst bhs.bhs_m; + bv_po = bhs_po bhs; + bv_cmp = bhs.bhs_cmp; + bv_bd = bhs_bd bhs; + bv_mk = (fun po cmp bd -> + f_bdHoareS (snd bhs.bhs_m) (bhs_pr bhs) bhs.bhs_s po cmp bd); +} + +let view_F (bhf : bdHoareF) = { + bv_m = bhf.bhf_m; + bv_po = bhf_po bhf; + bv_cmp = bhf.bhf_cmp; + bv_bd = bhf_bd bhf; + bv_mk = (fun po cmp bd -> f_bdHoareF (bhf_pr bhf) bhf.bhf_f po cmp bd); +} + +(* -------------------------------------------------------------------- *) +(* The two binary connectives, each with its dual. *) +type bop = [`And | `Or] + +let bop_destr (op : bop) (po : ss_inv) = + let destr = match op with `And -> destr_and | `Or -> destr_or in + let f1, f2 = destr po.inv in + ({ po with inv = f1 }, { po with inv = f2 }) + +let bop_dual (op : bop) = + match op with `And -> map_ss_inv2 f_or | `Or -> map_ss_inv2 f_and + +let bop_bound (b1 : ss_inv) (b2 : ss_inv) (b3 : ss_inv) = + map_ss_inv2 f_real_sub (map_ss_inv2 f_real_add b1 b2) b3 + +(* Pure cores shared by the rules and their checkers. Their side + conditions (the shape of the postcondition, the goal's bound being the + combination of the premises' bounds, up to alpha-conversion) are part of + them, so the checker re-validates them. *) +let split_bop_subgoals + (op : bop) (hyps : LDecl.hyps) (v : bdhoare_view) (n : bdhoare_split_bop) += + let b1 = ss_inv_rebind n.bsb_b1 v.bv_m in + let b2 = ss_inv_rebind n.bsb_b2 v.bv_m in + let b3 = ss_inv_rebind n.bsb_b3 v.bv_m in + let a, b = bop_destr op v.bv_po in + if not (EcReduction.ss_inv_alpha_eq hyps (bop_bound b1 b2 b3) v.bv_bd) then + failwith "bdhoare-split: the bound is not (b1 + b2) - b3"; + [ v.bv_mk a v.bv_cmp b1; + v.bv_mk b v.bv_cmp b2; + v.bv_mk (bop_dual op a b) (hoarecmp_opp v.bv_cmp) b3 ] + +let split_not_subgoals + (hyps : LDecl.hyps) (v : bdhoare_view) (n : bdhoare_split_not) += + let b1 = ss_inv_rebind n.bnt_b1 v.bv_m in + let b2 = ss_inv_rebind n.bnt_b2 v.bv_m in + if not (EcReduction.ss_inv_alpha_eq hyps (map_ss_inv2 f_real_sub b1 b2) v.bv_bd) then + failwith "bdhoare-split-not: the bound is not b1 - b2"; + [ v.bv_mk (map_ss_inv1 (fun _ -> f_true) v.bv_po) v.bv_cmp b1; + v.bv_mk (map_ss_inv1 f_not_simpl v.bv_po) (hoarecmp_opp v.bv_cmp) b2 ] + +(* -------------------------------------------------------------------- *) +(* Rules (TCB). The side conditions are checked first, for the error + messages. *) +let t_split_bop + (op : bop) (mk : bdhoare_split_bop -> rule) + (v : bdhoare_view) (r : bdhoare_split_bop) (tc : tcenv1) += + let hyps = FApi.tc1_hyps tc in + (try ignore (bop_destr op v.bv_po) with DestrError _ -> + tc_error !!tc "the postcondition must be a %s" + (match op with `And -> "conjunction" | `Or -> "disjunction")); + let b1 = ss_inv_rebind r.bsb_b1 v.bv_m in + let b2 = ss_inv_rebind r.bsb_b2 v.bv_m in + let b3 = ss_inv_rebind r.bsb_b3 v.bv_m in + if not (EcReduction.ss_inv_alpha_eq hyps (bop_bound b1 b2 b3) v.bv_bd) then + tc_error !!tc "the bound must be of the form (b1 + b2) - b3"; + FApi.xrule1 tc (mk r) (split_bop_subgoals op hyps v r) + +let t_bdhoareS_split_and r tc = + t_split_bop `And (fun n -> RBdHoareSSplitAnd n) (view_S (tc1_as_bdhoareS tc)) r tc +let t_bdhoareF_split_and r tc = + t_split_bop `And (fun n -> RBdHoareFSplitAnd n) (view_F (tc1_as_bdhoareF tc)) r tc +let t_bdhoareS_split_or r tc = + t_split_bop `Or (fun n -> RBdHoareSSplitOr n) (view_S (tc1_as_bdhoareS tc)) r tc +let t_bdhoareF_split_or r tc = + t_split_bop `Or (fun n -> RBdHoareFSplitOr n) (view_F (tc1_as_bdhoareF tc)) r tc + +let t_split_not + (mk : bdhoare_split_not -> rule) + (v : bdhoare_view) (r : bdhoare_split_not) (tc : tcenv1) += + let hyps = FApi.tc1_hyps tc in + let b1 = ss_inv_rebind r.bnt_b1 v.bv_m in + let b2 = ss_inv_rebind r.bnt_b2 v.bv_m in + if not (EcReduction.ss_inv_alpha_eq hyps (map_ss_inv2 f_real_sub b1 b2) v.bv_bd) then + tc_error !!tc "the bound must be of the form b1 - b2"; + FApi.xrule1 tc (mk r) (split_not_subgoals hyps v r) + +let t_bdhoareS_split_not r tc = + t_split_not (fun n -> RBdHoareSSplitNot n) (view_S (tc1_as_bdhoareS tc)) r tc +let t_bdhoareF_split_not r tc = + t_split_not (fun n -> RBdHoareFSplitNot n) (view_F (tc1_as_bdhoareF tc)) r tc + +(* -------------------------------------------------------------------- *) +let () = + let bop name op destr view n = + EcPlRecheck.checker_of name destr + (fun hyps j -> split_bop_subgoals op hyps (view j) n) in + let not_ name destr view n = + EcPlRecheck.checker_of name destr + (fun hyps j -> split_not_subgoals hyps (view j) n) in + register_rule_checker + (function + | RBdHoareSSplitAnd n -> + Some (bop "bdhoareS-split-and" `And pf_as_bdhoareS view_S n) + | RBdHoareFSplitAnd n -> + Some (bop "bdhoareF-split-and" `And pf_as_bdhoareF view_F n) + | RBdHoareSSplitOr n -> + Some (bop "bdhoareS-split-or" `Or pf_as_bdhoareS view_S n) + | RBdHoareFSplitOr n -> + Some (bop "bdhoareF-split-or" `Or pf_as_bdhoareF view_F n) + | RBdHoareSSplitNot n -> + Some (not_ "bdhoareS-split-not" pf_as_bdhoareS view_S n) + | RBdHoareFSplitNot n -> + Some (not_ "bdhoareF-split-not" pf_as_bdhoareF view_F n) + | _ -> None) + +(* -------------------------------------------------------------------- *) +(* Derived (no proof-node): unless the goal's bound already is the + combination of the given bounds, first change it into that combination + with the bound-changing consequence (its side condition is left open), + then apply the rule. + + TEMPORARY: the bound-changing consequence still comes from the + not-yet-migrated [EcPhlConseq]. *) +let not_bdhoare tc = + tc_error !!tc "the conclusion should be a bdhoare judgment" + +let t_with_bound ~(same : ss_inv -> ss_inv -> bool) nb tS tF (tc : tcenv1) = + let with_bound t_conseq_bd t_main (v : bdhoare_view) = + if same nb v.bv_bd + then t_main tc + else FApi.t_seqsub (t_conseq_bd v.bv_cmp nb) [t_id; t_main] tc + in + match (FApi.tc1_goal tc).f_node with + | FbdHoareS bhs -> with_bound EcPhlConseq.t_bdHoareS_conseq_bd tS (view_S bhs) + | FbdHoareF bhf -> with_bound EcPhlConseq.t_bdHoareF_conseq_bd tF (view_F bhf) + | _ -> not_bdhoare tc + +let t_bdhoare_split_and (r : bdhoare_split_bop) = + t_with_bound ~same:(fun nb bd -> f_equal nb.inv bd.inv) + (bop_bound r.bsb_b1 r.bsb_b2 r.bsb_b3) + (t_bdhoareS_split_and r) (t_bdhoareF_split_and r) + +let t_bdhoare_split_or (r : bdhoare_split_bop) = + t_with_bound ~same:(fun nb bd -> f_equal nb.inv bd.inv) + (bop_bound r.bsb_b1 r.bsb_b2 r.bsb_b3) + (t_bdhoareS_split_or r) (t_bdhoareF_split_or r) + +let t_bdhoare_split_not (r : bdhoare_split_not) (tc : tcenv1) = + t_with_bound ~same:(EcReduction.ss_inv_alpha_eq (FApi.tc1_hyps tc)) + (map_ss_inv2 f_real_sub r.bnt_b1 r.bnt_b2) + (t_bdhoareS_split_not r) (t_bdhoareF_split_not r) tc + +(* -------------------------------------------------------------------- *) +(* Elaboration: the goal is expected to be a bdhoare judgement. Type the + bounds in its memory, then apply the derived split tactic matching the + surface form. *) +let process_bdhoare_split (info : EcParsetree.bdh_split) (tc : tcenv1) = + let _, concl = FApi.tc1_flat tc in + + let pr, po = + match concl.f_node with + | FbdHoareS bhs -> (bhs_pr bhs, bhs_po bhs) + | FbdHoareF bhf -> (bhf_pr bhf, bhf_po bhf) + | _ -> tc_error !!tc "the conclusion must be a bdhoare judgment" in + + match info with + | EcParsetree.BDH_split_bop (b1, b2, b3) -> + let t = + if is_and po.inv then t_bdhoare_split_and + else if is_or po.inv then t_bdhoare_split_or + else + tc_error !!tc + "the postcondition must be a conjunction or a disjunction" + in + let _, b1 = TTC.tc1_process_Xhl_form tc treal b1 in + let _, b2 = TTC.tc1_process_Xhl_form tc treal b2 in + let b3 = + b3 |> omap (fun f -> snd (TTC.tc1_process_Xhl_form tc treal f)) + |> odfl { m = b1.m; inv = f_r0; } in + + t { bsb_b1 = b1; bsb_b2 = b2; bsb_b3 = b3; } tc + + | EcParsetree.BDH_split_or_case (b1, b2, f) -> + let _, b1 = TTC.tc1_process_Xhl_form tc treal b1 in + let _, b2 = TTC.tc1_process_Xhl_form tc treal b2 in + let _, f = TTC.tc1_process_Xhl_formula tc f in + + (* TEMPORARY: the consequence rule still comes from the + not-yet-migrated [EcPhlConseq]. *) + let t_conseq po lemma tactic = + let rwtt tc = + let pt = ptglobal ~tys:[] lemma in + + let rwtt = [ + EcLowGoal.t_intros_i [EcIdent.create "_"]; + EcHiGoal.LowRewrite.t_rewrite (`LtoR, None, None) pt; + t_true; + ] in FApi.t_seqs rwtt tc + in + + FApi.t_seqsub + (EcPhlConseq.t_conseq (Inv_ss pr) (Inv_ss po)) + [t_true; rwtt; tactic] + in + + t_conseq + (map_ss_inv2 f_or + (map_ss_inv2 f_and f po) + (map_ss_inv2 f_and (map_ss_inv1 f_not f) po)) + (EcCoreLib.CI_Logic.mk_logic "orDandN") + (FApi.t_on1seq 3 + (t_bdhoare_split_or + { bsb_b1 = b1; bsb_b2 = b2; bsb_b3 = { m = b1.m; inv = f_r0; } }) + (t_conseq + { inv = f_false; m = b1.m; } + (EcCoreLib.CI_Logic.mk_logic "andDorN") + EcHiGoal.process_trivial)) + tc + + | EcParsetree.BDH_split_not (b1, b2) -> + let _, b2 = TTC.tc1_process_Xhl_form tc treal b2 in + let b1 = + b1 |> omap (fun f -> snd (TTC.tc1_process_Xhl_form tc treal f)) + |> odfl { m = b2.m; inv = f_r1; } in + t_bdhoare_split_not { bnt_b1 = b1; bnt_b2 = b2; } tc diff --git a/src/phl/rules/bdhoare/ecBdHoareSplit.mli b/src/phl/rules/bdhoare/ecBdHoareSplit.mli new file mode 100644 index 0000000000..ea1b68d3bc --- /dev/null +++ b/src/phl/rules/bdhoare/ecBdHoareSplit.mli @@ -0,0 +1,116 @@ +(* -------------------------------------------------------------------- *) +open EcCoreGoal.FApi +open EcAst + +(* ==================================================================== *) +(* Rules (trusted) *) + +type bdhoare_split_bop = { + bsb_b1 : ss_inv; (* bound b1 for the left operand A *) + bsb_b2 : ss_inv; (* bound b2 for the right operand B *) + bsb_b3 : ss_inv; (* opposite bound b3 for the dual connective *) +} + +(* In the rules below, [~] is the goal's comparison and [~'] its opposite + ([<=] and [>=] are swapped, [=] stays). *) + +(* [t_bdhoareS_split_and { bsb_b1 = b1; bsb_b2 = b2; bsb_b3 = b3 }] — + inclusion-exclusion on a conjunction: + + phoare [c : P ==> A] ~ b1 + phoare [c : P ==> B] ~ b2 + phoare [c : P ==> A \/ B] ~' b3 + ------------------------------- d = (b1 + b2) - b3 + phoare [c : P ==> A /\ B] ~ d + + Side conditions: the postcondition is a conjunction, and the bound [d] + is [(b1 + b2) - b3] up to alpha-conversion (otherwise fails). + + Node: [RBdHoareSSplitAnd { bsb_b1 = b1; bsb_b2 = b2; bsb_b3 = b3 }]. + Checker: "bdhoareS-split-and". *) +val t_bdhoareS_split_and : bdhoare_split_bop -> backward + +(* [t_bdhoareF_split_and] — same for a procedure. + Node: [RBdHoareFSplitAnd]. Checker: "bdhoareF-split-and". *) +val t_bdhoareF_split_and : bdhoare_split_bop -> backward + +(* [t_bdhoareS_split_or { bsb_b1 = b1; bsb_b2 = b2; bsb_b3 = b3 }] — + inclusion-exclusion on a disjunction: + + phoare [c : P ==> A] ~ b1 + phoare [c : P ==> B] ~ b2 + phoare [c : P ==> A /\ B] ~' b3 + ------------------------------- d = (b1 + b2) - b3 + phoare [c : P ==> A \/ B] ~ d + + Side conditions: the postcondition is a disjunction, and the bound [d] + is [(b1 + b2) - b3] up to alpha-conversion (otherwise fails). + + Node: [RBdHoareSSplitOr { bsb_b1 = b1; bsb_b2 = b2; bsb_b3 = b3 }]. + Checker: "bdhoareS-split-or". *) +val t_bdhoareS_split_or : bdhoare_split_bop -> backward + +(* [t_bdhoareF_split_or] — same for a procedure. + Node: [RBdHoareFSplitOr]. Checker: "bdhoareF-split-or". *) +val t_bdhoareF_split_or : bdhoare_split_bop -> backward + +type bdhoare_split_not = { + bnt_b1 : ss_inv; (* bound b1 for [true] *) + bnt_b2 : ss_inv; (* opposite bound b2 for the negated postcondition *) +} + +(* [t_bdhoareS_split_not { bnt_b1 = b1; bnt_b2 = b2 }] — complement: + + phoare [c : P ==> true] ~ b1 + phoare [c : P ==> !Q] ~' b2 + ---------------------------- d = b1 - b2 + phoare [c : P ==> Q] ~ d + + where [!Q] is simplified ([!!Q'] is [Q'], ...). Side condition: the + bound [d] is [b1 - b2] up to alpha-conversion (otherwise fails). + + Node: [RBdHoareSSplitNot { bnt_b1 = b1; bnt_b2 = b2 }]. + Checker: "bdhoareS-split-not". *) +val t_bdhoareS_split_not : bdhoare_split_not -> backward + +(* [t_bdhoareF_split_not] — same for a procedure. + Node: [RBdHoareFSplitNot]. Checker: "bdhoareF-split-not". *) +val t_bdhoareF_split_not : bdhoare_split_not -> backward + +(* ==================================================================== *) +(* Derived tactics *) + +(* [t_bdhoare_split_and r] — on a statement or procedure goal + [phoare [_ : P ==> A /\ B] ~ d]: + 1. unless [d] is syntactically [(b1 + b2) - b3], the bound-changing + consequence (currently [EcPhlConseq.t_bdHoare{S,F}_conseq_bd]) to + that bound, whose side condition is left open; + 2. then [t_bdhoare{S,F}_split_and r]. + Visible goals: the bound side condition if any, then the three + premises. Emits no node of its own. *) +val t_bdhoare_split_and : bdhoare_split_bop -> backward + +(* [t_bdhoare_split_or r] — same, with [t_bdhoare{S,F}_split_or]. *) +val t_bdhoare_split_or : bdhoare_split_bop -> backward + +(* [t_bdhoare_split_not r] — same, with [t_bdhoare{S,F}_split_not]; the + bound is compared with [b1 - b2] up to alpha-conversion. *) +val t_bdhoare_split_not : bdhoare_split_not -> backward + +(* ==================================================================== *) +(* Elaboration *) + +(* [phoare split ...] on a bdhoare goal [phoare [_ : P ==> Q] ~ d], the + bounds being typed in the goal's memory: + - [phoare split b1 b2 b3?]: [Q] is a conjunction (resp. disjunction), + [b3] defaults to [0%r]; applies [t_bdhoare_split_and] (resp. + [t_bdhoare_split_or]); + - [phoare split b1 b2 : R]: the consequence rule (currently + [EcPhlConseq.t_conseq]) to [(R /\ Q) \/ (!R /\ Q)] (closing its side + conditions by [orDandN]), [t_bdhoare_split_or] with [b3 = 0%r], and + the consequence rule on its third premise to [false] (closing it with + [andDorN] and [trivial]). Visible goals: the bounds side condition if + any, then [phoare [_ : P ==> R /\ Q] ~ b1] and + [phoare [_ : P ==> !R /\ Q] ~ b2]; + - [phoare split ! b1 b2]: applies [t_bdhoare_split_not]. *) +val process_bdhoare_split : EcParsetree.bdh_split -> backward diff --git a/src/phl/rules/equiv/ecEquivPr.ml b/src/phl/rules/equiv/ecEquivPr.ml new file mode 100644 index 0000000000..e457693597 --- /dev/null +++ b/src/phl/rules/equiv/ecEquivPr.ml @@ -0,0 +1,104 @@ +(* -------------------------------------------------------------------- *) +open EcParsetree +open EcFol +open EcAst +open EcEnv +open EcSubst + +open EcCoreGoal +open EcLowPhlGoal + +module TTC = EcProofTyping + +(* -------------------------------------------------------------------- *) +(* Parameters of the equiv [pr] rule: the two observed expressions, typed + in the final memory of each side, and their common type. Already typed, + nothing to resolve: the same record is the rule argument and the node + payload. *) +type equiv_pr = { + epr_ty : ty; (* the common type of [epr_left] and [epr_right] *) + epr_left : ss_inv; (* phi_l, observed on the left *) + epr_right : ss_inv; (* phi_r, observed on the right *) +} + +type EcCoreGoal.rule += REquivFPr of equiv_pr + +(* -------------------------------------------------------------------- *) +(* Pure core shared by the rule and its checker. Its side condition (both + expressions have the recorded type) is part of it, so the checker + re-validates it. The memory of the events and the value [a] are fresh at + each call: the checker compares up to alpha-conversion. *) +let equivF_pr_subgoals (hyps : LDecl.hyps) (ef : equivF) (n : equiv_pr) = + let env = LDecl.toenv hyps in + if not ( EcReduction.EqTest.for_type env n.epr_ty n.epr_left.inv.f_ty + && EcReduction.EqTest.for_type env n.epr_ty n.epr_right.inv.f_ty) then + failwith "equivF-pr: the expressions do not have the recorded type"; + let (fl, fr) = (ef.ef_fl, ef.ef_fr) in + let funl = Fun.by_xpath fl env in + let funr = Fun.by_xpath fr env in + let (penvl, penvr), (qenvl, qenvr) = + Fun.equivF_memenv ef.ef_ml ef.ef_mr fl fr env in + let m = EcIdent.create "&hr" in + let argsl = + map_ss_inv1 (pr_args_of_fun funl) (f_pvarg funl.f_sig.fs_arg (fst penvl)) in + let argsr = + map_ss_inv1 (pr_args_of_fun funr) (f_pvarg funr.f_sig.fs_arg (fst penvr)) in + let a_id = EcIdent.create "a" in + let a_f = f_local a_id n.epr_ty in + let pr1_ev = ss_inv_rebind (map_ss_inv1 (fun p -> f_eq p a_f) n.epr_left) m in + let pr1 = f_pr (fst penvl) fl argsl.inv pr1_ev in + let pr2_ev = ss_inv_rebind (map_ss_inv1 (fun p -> f_eq p a_f) n.epr_right) m in + let pr2 = f_pr (fst penvr) fr argsr.inv pr2_ev in + let concl_pr = + f_forall_mems_ts_inv penvl penvr + (map_ts_inv1 (f_forall_simpl [a_id, GTty n.epr_ty]) + (map_ts_inv1 (fun pr -> f_imp_simpl pr (f_eq_simpl pr1 pr2)) (ef_pr ef))) in + let phi_l = ss_inv_generalize_as_left n.epr_left ef.ef_ml ef.ef_mr in + let phi_r = ss_inv_generalize_as_right n.epr_right ef.ef_ml ef.ef_mr in + let concl_po = + f_forall_mems_ts_inv qenvl qenvr + (map_ts_inv3 (fun phi_l phi_r po -> + f_forall_simpl [a_id, GTty n.epr_ty] + (f_imps_simpl [f_eq phi_l a_f; f_eq phi_r a_f] po)) + phi_l phi_r (ef_po ef)) in + [concl_po; concl_pr] + +(* -------------------------------------------------------------------- *) +let not_convertible tc = tc_error !!tc "formulas must have convertible types" + +(* Rule (TCB). *) +let t_equivF_pr (r : equiv_pr) (tc : tcenv1) = + let env = FApi.tc1_env tc in + let ef = tc1_as_equivF tc in + if not ( EcReduction.EqTest.for_type env r.epr_ty r.epr_left.inv.f_ty + && EcReduction.EqTest.for_type env r.epr_ty r.epr_right.inv.f_ty) then + not_convertible tc; + FApi.xrule1 tc (REquivFPr r) (equivF_pr_subgoals (FApi.tc1_hyps tc) ef r) + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | REquivFPr n -> + Some (EcPlRecheck.checker_of "equivF-pr" pf_as_equivF + (fun hyps ef -> equivF_pr_subgoals hyps ef n)) + | _ -> None) + +(* -------------------------------------------------------------------- *) +(* Elaboration: the goal is expected to be an [equivF]. Type the two + expressions in the final memory of their side, check that their types + are convertible, then apply the rule. *) +let process_equivF_pr ((phi1, phi2) : pformula * pformula) (tc : tcenv1) = + let hyps = FApi.tc1_hyps tc in + let ef = tc1_as_equivF tc in + let qenvl = snd (LDecl.hoareF ef.ef_ml ef.ef_fl hyps) in + let qenvr = snd (LDecl.hoareF ef.ef_mr ef.ef_fr hyps) in + let phi1 = TTC.pf_process_form_opt !!tc qenvl None phi1 in + let phi2 = TTC.pf_process_form_opt !!tc qenvr None phi2 in + if not (EcReduction.EqTest.for_type (LDecl.toenv hyps) phi1.f_ty phi2.f_ty) then + not_convertible tc; + t_equivF_pr + { epr_ty = phi1.f_ty; + epr_left = { m = ef.ef_ml; inv = phi1; }; + epr_right = { m = ef.ef_mr; inv = phi2; }; } + tc diff --git a/src/phl/rules/equiv/ecEquivPr.mli b/src/phl/rules/equiv/ecEquivPr.mli new file mode 100644 index 0000000000..cda77cfb2b --- /dev/null +++ b/src/phl/rules/equiv/ecEquivPr.mli @@ -0,0 +1,40 @@ +(* -------------------------------------------------------------------- *) +open EcParsetree +open EcCoreGoal.FApi +open EcAst + +(* ==================================================================== *) +(* Rules (trusted) *) + +type equiv_pr = { + epr_ty : ty; (* the common type t of phi_l and phi_r *) + epr_left : ss_inv; (* phi_l, in the left final memory *) + epr_right : ss_inv; (* phi_r, in the right final memory *) +} + +(* [t_equivF_pr { epr_ty = t; epr_left = phi_l; epr_right = phi_r }] — an + equivalence of two procedures, reduced to the equality of the + distributions of [phi_l] and [phi_r]: + + forall &1 &2, forall (a : t), phi_l = a => phi_r = a => Q + forall &1 &2, forall (a : t), + P => Pr[f1(args1) @ &1 : phi_l = a] = Pr[f2(args2) @ &2 : phi_r = a] + -------------------------------------------------------------------- + equiv [f1 ~ f2 : P ==> Q] + + where [args1] (resp. [args2]) are the arguments of [f1] (resp. [f2]) + read in [&1] (resp. [&2]); in the first premise, [&1] and [&2] are the + final memories. Side condition: [phi_l] and [phi_r] have type [t] + (otherwise fails). + + Node: [REquivFPr { epr_ty = t; epr_left = phi_l; epr_right = phi_r }]. + Checker: "equivF-pr". *) +val t_equivF_pr : equiv_pr -> backward + +(* ==================================================================== *) +(* Elaboration *) + +(* [bypr phi_l phi_r] on an [equivF] goal: [phi_l] (resp. [phi_r]) is + typed in the left (resp. right) final memory, and their types must be + convertible. Applies [t_equivF_pr]. *) +val process_equivF_pr : pformula * pformula -> backward diff --git a/src/phl/rules/hoare/ecHoareOfBdHoare.ml b/src/phl/rules/hoare/ecHoareOfBdHoare.ml new file mode 100644 index 0000000000..2031bde616 --- /dev/null +++ b/src/phl/rules/hoare/ecHoareOfBdHoare.ml @@ -0,0 +1,59 @@ +(* -------------------------------------------------------------------- *) +open EcFol +open EcAst + +open EcCoreGoal +open EcLowPhlGoal + +(* -------------------------------------------------------------------- *) +(* The rules deriving a hoare judgement from a probabilistic one have no + parameters. *) +type EcCoreGoal.rule += + | RHoareSOfBdHoare + | RHoareFOfBdHoare + +(* -------------------------------------------------------------------- *) +(* Pure cores shared by the rules and their checkers. The side condition + (no exceptional postcondition) is part of them, so the checker + re-validates it. *) +let hoareS_of_bdhoare_subgoals (hs : sHoareS) : form list = + let { main = inv } as post = (hs_po hs).hsi_inv in + if not (POE.is_empty post) then + failwith "hoareS-of-bdhoare: exceptional postconditions"; + let m = (hs_po hs).hsi_m in + [f_bdHoareS (snd hs.hs_m) (hs_pr hs) hs.hs_s + (map_ss_inv1 f_not { m; inv }) FHeq { m = fst hs.hs_m; inv = f_r0; }] + +let hoareF_of_bdhoare_subgoals (hf : sHoareF) : form list = + let { main = inv } as post = (hf_po hf).hsi_inv in + if not (POE.is_empty post) then + failwith "hoareF-of-bdhoare: exceptional postconditions"; + let m = (hf_po hf).hsi_m in + [f_bdHoareF (hf_pr hf) hf.hf_f + (map_ss_inv1 f_not { m; inv }) FHeq { m = hf.hf_m; inv = f_r0; }] + +(* -------------------------------------------------------------------- *) +let no_exceptions tc = tc_error !!tc "Exceptions are not permitted" + +(* Rules (TCB). *) +let t_hoareS_of_bdhoare (tc : tcenv1) = + let hs = tc1_as_hoareS tc in + if not (POE.is_empty (hs_po hs).hsi_inv) then no_exceptions tc; + FApi.xrule1 tc RHoareSOfBdHoare (hoareS_of_bdhoare_subgoals hs) + +let t_hoareF_of_bdhoare (tc : tcenv1) = + let hf = tc1_as_hoareF tc in + if not (POE.is_empty (hf_po hf).hsi_inv) then no_exceptions tc; + FApi.xrule1 tc RHoareFOfBdHoare (hoareF_of_bdhoare_subgoals hf) + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | RHoareSOfBdHoare -> + Some (EcPlRecheck.checker_of "hoareS-of-bdhoare" pf_as_hoareS + (fun _hyps hs -> hoareS_of_bdhoare_subgoals hs)) + | RHoareFOfBdHoare -> + Some (EcPlRecheck.checker_of "hoareF-of-bdhoare" pf_as_hoareF + (fun _hyps hf -> hoareF_of_bdhoare_subgoals hf)) + | _ -> None) diff --git a/src/phl/rules/hoare/ecHoareOfBdHoare.mli b/src/phl/rules/hoare/ecHoareOfBdHoare.mli new file mode 100644 index 0000000000..3387a393d6 --- /dev/null +++ b/src/phl/rules/hoare/ecHoareOfBdHoare.mli @@ -0,0 +1,27 @@ +(* -------------------------------------------------------------------- *) +open EcCoreGoal.FApi + +(* ==================================================================== *) +(* Rules (trusted) *) + +(* [t_hoareS_of_bdhoare] — a hoare judgement holds when its postcondition + is reached with probability 0 on its negation: + + phoare [c : P ==> !Q] = 0%r + --------------------------- + hoare [c : P ==> Q] + + Side condition: the goal has no exceptional postcondition (otherwise + fails). + + Node: [RHoareSOfBdHoare]. Checker: "hoareS-of-bdhoare". *) +val t_hoareS_of_bdhoare : backward + +(* [t_hoareF_of_bdhoare] — same for a procedure: + + phoare [f : P ==> !Q] = 0%r + --------------------------- + hoare [f : P ==> Q] + + Node: [RHoareFOfBdHoare]. Checker: "hoareF-of-bdhoare". *) +val t_hoareF_of_bdhoare : backward diff --git a/src/phl/rules/hoare/ecHoarePr.ml b/src/phl/rules/hoare/ecHoarePr.ml new file mode 100644 index 0000000000..b7a5cf8403 --- /dev/null +++ b/src/phl/rules/hoare/ecHoarePr.ml @@ -0,0 +1,8 @@ +(* -------------------------------------------------------------------- *) +open EcCoreGoal + +(* -------------------------------------------------------------------- *) +(* Derived (no proof-node): a hoare judgement is a probability-0 one, + which is then stated on the probability of the negated postcondition. *) +let t_hoareF_pr (tc : tcenv1) = + FApi.t_seq EcHoareOfBdHoare.t_hoareF_of_bdhoare EcBdHoarePr.t_bdhoareF_pr tc diff --git a/src/phl/rules/hoare/ecHoarePr.mli b/src/phl/rules/hoare/ecHoarePr.mli new file mode 100644 index 0000000000..cf565cedeb --- /dev/null +++ b/src/phl/rules/hoare/ecHoarePr.mli @@ -0,0 +1,19 @@ +(* -------------------------------------------------------------------- *) +open EcCoreGoal.FApi + +(* ==================================================================== *) +(* Rules (trusted) *) + +(* None: the hoare [pr] tactic is derived from the bdhoare one. *) + +(* ==================================================================== *) +(* Derived tactics *) + +(* [t_hoareF_pr] — on [hoare [f : P ==> Q]]: + 1. [EcHoareOfBdHoare.t_hoareF_of_bdhoare], to + [phoare [f : P ==> !Q] = 0%r]; + 2. then [EcBdHoarePr.t_bdhoareF_pr]. + Visible goal: + [forall &m, 0%r <= 0%r /\ (P => Pr[f(args) @ &m : !Q] = 0%r)]. + Emits no node of its own. *) +val t_hoareF_pr : backward diff --git a/src/phl/rules/hoare/ecHoareSplit.ml b/src/phl/rules/hoare/ecHoareSplit.ml new file mode 100644 index 0000000000..b5822987e5 --- /dev/null +++ b/src/phl/rules/hoare/ecHoareSplit.ml @@ -0,0 +1,32 @@ +(* -------------------------------------------------------------------- *) +open EcUtils +open EcAst +open EcFol +open EcLowPhlGoal +open EcCoreGoal + +(* -------------------------------------------------------------------- *) +(* Derived (no proof-node): duplicate the precondition with the + consequence rule, then split the postcondition with the conjunctive + consequence rule. + + TEMPORARY: both consequence rules still come from the not-yet-migrated + [EcPhlConseq]. *) +let t_hoare_split (tc : tcenv1) = + let hoare = tc1_as_hoareS tc in + let pre = hs_pr hoare in + let post = POE.lower (hs_po hoare) in + + match sform_of_form post.inv with + | SFand (`Sym, (f1, f2)) -> + let dp = map_ss_inv2 f_and pre pre in + let cl = update_hs_ss { post with inv = f1 } (hs_po hoare) in + let cr = update_hs_ss { post with inv = f2 } (hs_po hoare) in + + EcPhlConseq.t_hoareS_conseq dp (hs_po hoare) tc + |> FApi.t_firsts EcHiGoal.process_done 2 + |> FApi.as_tcenv1 + |> EcPhlConseq.t_hoareS_conseq_conj (hs_pr hoare) cr (hs_pr hoare) cl + + | _ -> + tc_error !!tc "post-condition should be a conjunction" diff --git a/src/phl/rules/hoare/ecHoareSplit.mli b/src/phl/rules/hoare/ecHoareSplit.mli new file mode 100644 index 0000000000..927b074ecb --- /dev/null +++ b/src/phl/rules/hoare/ecHoareSplit.mli @@ -0,0 +1,22 @@ +(* -------------------------------------------------------------------- *) +open EcCoreGoal.FApi + +(* ==================================================================== *) +(* Rules (trusted) *) + +(* None: splitting a hoare postcondition is derived from the consequence + rules. *) + +(* ==================================================================== *) +(* Derived tactics *) + +(* [t_hoare_split] — on [hoare [c : P ==> A /\ B | Q_e]] (a symmetric + conjunction [/\], not [&&]): + 1. the consequence rule (currently [EcPhlConseq.t_hoareS_conseq]) to + [hoare [c : P /\ P ==> A /\ B | Q_e]], closing its two side + conditions with [done] (fails if it does not); + 2. the conjunctive consequence rule (currently + [EcPhlConseq.t_hoareS_conseq_conj]) on [P /\ P]. + Visible goals: [hoare [c : P ==> B | Q_e]], then + [hoare [c : P ==> A | Q_e]]. Emits no node of its own. *) +val t_hoare_split : backward diff --git a/tests/pr-bridges.ec b/tests/pr-bridges.ec new file mode 100644 index 0000000000..0d9475fa7d --- /dev/null +++ b/tests/pr-bridges.ec @@ -0,0 +1,281 @@ +require import AllCore Distr DBool. + +exception ex. + +module M = { + proc f() : int = { + var x; + x <- 1; + return x; + } + + proc g(a : int, b : bool) : int = { + return a; + } + + proc h(a : int) : bool = { + var y; + y <$ {0,1}; + return y; + } + + proc e() = { + raise ex; + } +}. + +(* -------------------------------------------------------------------- *) +(* [bypr]: hoare, phoare (each comparison) and equiv, procedure forms. *) + +lemma hoareF_pr : hoare [M.f : true ==> res = 1]. +proof. +bypr=> &m /=. +by byphoare=> //; hoare; proc; auto. +qed. + +lemma bdhoareF_pr_eq : phoare [M.f : true ==> res = 1] = 1%r. +proof. +bypr=> &m /=. +by byphoare=> //; proc; auto. +qed. + +lemma bdhoareF_pr_le (a0 : int) : phoare [M.h : a = a0 ==> res] <= (1%r/2%r). +proof. +bypr=> &m; split=> [/#|h]. +byphoare (_: arg = a0 ==> res)=> //. +by proc; rnd; auto=> />; smt(dboolE). +qed. + +lemma bdhoareF_pr_ge : phoare [M.g : 0 <= a ==> 0 <= res] >= 1%r. +proof. +bypr=> &m; split=> // hpos. +byphoare (_: 0 <= arg.`1 ==> 0 <= res)=> //. +by proc; auto. +qed. + +lemma equivF_pr : equiv [M.g ~ M.g : ={a, b} ==> ={res}]. +proof. +bypr (res{1}) (res{2})=> //. +move=> &1 &2 r [] eqa eqb. +by byequiv (_: ={a, b} ==> ={res})=> //; proc; auto. +qed. + +lemma pr_errors : hoare [M.f : true ==> res = 1]. +proof. +fail bypr (res{1}) (res{2}). +proc. +fail bypr. +abort. + +lemma pr_errors_equiv : equiv [M.g ~ M.g : ={a, b} ==> ={res}]. +proof. +fail bypr (res{1}) (true). +fail bypr. +abort. + +(* -------------------------------------------------------------------- *) +(* [pr_bounded]: statement and procedure forms, premise-free and with a *) +(* premise; [trivial] uses the premise-free forms only. *) + +lemma bdhoareF_prbounded_le : phoare [M.f : true ==> res = 1] <= 1%r. +proof. by pr_bounded. qed. + +lemma bdhoareS_prbounded_le : phoare [M.f : true ==> res = 1] <= 1%r. +proof. by proc; pr_bounded. qed. + +lemma bdhoareF_prbounded_ge : phoare [M.f : true ==> res = 1] >= 0%r. +proof. by pr_bounded. qed. + +lemma bdhoareS_prbounded_ge : phoare [M.f : true ==> res = 1] >= 0%r. +proof. by proc; pr_bounded. qed. + +lemma bdhoareF_prbounded_false : phoare [M.f : true ==> false] = 0%r. +proof. by pr_bounded. qed. + +lemma bdhoareS_prbounded_false : phoare [M.f : true ==> false] = 0%r. +proof. by proc; pr_bounded. qed. + +lemma bdhoareF_prbounded_le_premise (d : real) : + 1%r <= d => phoare [M.f : true ==> res = 1] <= d. +proof. by move=> hd; pr_bounded=> &m. qed. + +lemma bdhoareS_prbounded_ge_premise (d : real) : + d <= 0%r => phoare [M.f : true ==> res = 1] >= d. +proof. by move=> hd; proc; pr_bounded=> &m. qed. + +lemma bdhoare_prbounded_trivial : phoare [M.f : true ==> res = 1] <= 1%r. +proof. by trivial. qed. + +lemma prbounded_errors (d : real) : phoare [M.f : true ==> res = 1] = d. +proof. +fail pr_bounded. +proc. +fail pr_bounded. +abort. + +lemma prbounded_errors_trivial (d : real) : + 1%r <= d => phoare [M.f : true ==> res = 1] <= d. +proof. +move=> hd. +fail by trivial. +proc. +fail by trivial. +abort. + +lemma prbounded_errors_kind : hoare [M.f : true ==> res = 1]. +proof. +fail pr_bounded. +abort. + +(* -------------------------------------------------------------------- *) +(* [hoare]: in both directions, statement and procedure forms. *) + +lemma hoareF_hoare : hoare [M.f : true ==> res = 1]. +proof. +hoare. +by hoare; proc; auto. +qed. + +lemma hoareS_hoare : hoare [M.f : true ==> res = 1]. +proof. +proc; hoare. +by hoare; auto; smt(). +qed. + +lemma bdhoareF_hoare_le (d : real) : + phoare [M.f : true ==> res <> 1] <= (d * d). +proof. +hoare. ++ by move=> &m /=; smt(). +by proc; auto. +qed. + +lemma bdhoareF_hoare_eq0 : phoare [M.f : true ==> res <> 1] = 0%r. +proof. by hoare; proc; auto. qed. + +lemma bdhoareS_hoare_eq0 : phoare [M.f : true ==> res <> 1] = 0%r. +proof. by proc; hoare; auto. qed. + +lemma bdhoareS_hoare_ge : phoare [M.f : true ==> res <> 1] >= 0%r. +proof. +proc; hoare. +by auto. +qed. + +lemma hoare_errors : equiv [M.f ~ M.f : true ==> ={res}]. +proof. +fail hoare. +abort. + +lemma hoare_errors_exn : hoare [M.e : true ==> false | ex => true]. +proof. +fail hoare. +proc. +fail hoare. +abort. + +(* -------------------------------------------------------------------- *) +(* [phoare split]: and / or / not, with and without a change of bound. *) +(* Statement form only: the surface tactic cannot type its bounds on a *) +(* procedure goal. *) + +lemma bdhoareS_split_and : + phoare [M.h : true ==> res /\ true] = (1%r/2%r + 1%r - 1%r). +proof. +proc. +phoare split (1%r/2%r) 1%r 1%r. ++ by rnd; auto=> />; smt(dboolE). ++ by rnd; auto=> />; smt(dbool_ll). +by rnd; auto=> />; smt(dbool_ll). +qed. + +lemma bdhoareS_split_and_bound : + phoare [M.h : true ==> res /\ true] = (1%r/2%r). +proof. +proc. +phoare split (1%r/2%r) 1%r 1%r. ++ by move=> &m /=; smt(). ++ by rnd; auto=> />; smt(dboolE). ++ by rnd; auto=> />; smt(dbool_ll). +by rnd; auto=> />; smt(dbool_ll). +qed. + +lemma bdhoareS_split_or : + phoare [M.h : true ==> res \/ !res] = (1%r/2%r + 1%r/2%r - 0%r). +proof. +proc. +phoare split (1%r/2%r) (1%r/2%r) 0%r. ++ by rnd; auto=> />; smt(dboolE). ++ by rnd; auto=> />; smt(dboolE). +by hoare; auto; smt(). +qed. + +lemma bdhoareS_split_or_bound : + phoare [M.h : true ==> res \/ !res] = 1%r. +proof. +proc. +phoare split (1%r/2%r) (1%r/2%r). ++ by move=> &m /=; smt(). ++ by rnd; auto=> />; smt(dboolE). ++ by rnd; auto=> />; smt(dboolE). +by hoare; auto; smt(). +qed. + +lemma bdhoareS_split_or_case : + phoare [M.h : a = 0 ==> res] = (1%r/2%r). +proof. +proc. +phoare split (1%r/2%r) 0%r : (a = 0). ++ by move=> &m /=; smt(). ++ by rnd; auto=> />; smt(dboolE). +by hoare; auto; smt(). +qed. + +lemma bdhoareS_split_not : + phoare [M.h : true ==> res] = (1%r - 1%r/2%r). +proof. +proc. +phoare split ! 1%r (1%r/2%r). ++ by rnd; auto=> />; smt(dbool_ll). +by rnd; auto=> />; smt(dboolE). +qed. + +lemma bdhoareS_split_not_bound : + phoare [M.h : true ==> res] = (1%r/2%r). +proof. +proc. +phoare split ! 1%r (1%r/2%r). ++ by move=> &m /=; smt(). ++ by rnd; auto=> />; smt(dbool_ll). +by rnd; auto=> />; smt(dboolE). +qed. + +lemma split_errors : phoare [M.h : true ==> res] = (1%r/2%r). +proof. +fail phoare split (1%r/2%r) 0%r. +proc. +fail phoare split (1%r/2%r) 0%r. +abort. + +lemma split_errors_kind : hoare [M.h : true ==> res /\ true]. +proof. +fail phoare split 1%r 1%r 1%r. +fail phoare split ! 1%r 1%r. +abort. + +(* -------------------------------------------------------------------- *) +(* [hoare split]: statement form. *) + +lemma hoareS_split : hoare [M.f : true ==> res = 1 /\ 0 < res]. +proof. +proc; hoare split. ++ by auto. +by auto. +qed. + +lemma hoare_split_errors : hoare [M.f : true ==> res = 1]. +proof. +fail hoare split. +proc. +fail hoare split. +abort.