diff --git a/src/phl/ecPhlRnd.ml b/src/phl/ecPhlRnd.ml index a658cf7c7..7f4745587 100644 --- a/src/phl/ecPhlRnd.ml +++ b/src/phl/ecPhlRnd.ml @@ -3,17 +3,17 @@ open EcUtils open EcParsetree open EcAst open EcTypes -open EcModules -open EcFol -open EcPV -open EcSubst open EcMatching.Position open EcCoreGoal -open EcLowGoal -open EcLowPhlGoal -module TTC = EcProofTyping +(* -------------------------------------------------------------------- *) +(* The [rnd] and [rndsem] rules live, one module per logic, in + [rules//]: each owns its parameter records, pure subgoal builder, + recheckable proof-node, checker, derived forms and elaboration. This + module only keeps the legacy entry points (adapters onto those modules, + so external callers and this module's interface are unchanged) and the + logic-agnostic dispatchers. *) (* -------------------------------------------------------------------- *) type bhl_infos_t = (ss_inv, ty -> ss_inv option, ty -> ss_inv) rnd_tac_info @@ -22,727 +22,41 @@ type mkbij_t = EcTypes.ty -> EcTypes.ty -> ts_inv type semrndpos = (bool * codegap1) doption (* -------------------------------------------------------------------- *) -module Core = struct - - (* -------------------------------------------------------------------- *) - let t_hoare_rnd_r tc = - let env = FApi.tc1_env tc in - let hs = tc1_as_hoareS tc in - let m = fst hs.hs_m in - let (lv, distr), s = tc1_last_rnd tc hs.hs_s in - let ty_distr = proj_distr_ty env (e_ty distr) in - let x_id = EcIdent.create (symbol_of_lv lv) in - let x = {m; inv=f_local x_id ty_distr} in - let distr = EcFol.ss_inv_of_expr m distr in - if (not (POE.is_empty (hs_po hs).hsi_inv)) then - tc_error !!tc "exceptions are not supported"; - let post = (hs_po hs).hsi_inv.main in - let post = { m = (hs_po hs).hsi_m; inv = post} in - let post = subst_form_lv env lv x post in - let post = map_ss_inv2 f_imp (map_ss_inv2 f_in_supp x distr) post in - let post = map_ss_inv1 (f_forall_simpl [(x_id,GTty ty_distr)]) post in - let post = POE.lift post in - let concl = f_hoareS (snd hs.hs_m) (hs_pr hs) s post in - FApi.xmutate1 tc `Rnd [concl] - - (* -------------------------------------------------------------------- *) - let t_ehoare_rnd_r tc = - let env = FApi.tc1_env tc in - let hs = tc1_as_ehoareS tc in - let (lv, distr), s = tc1_last_rnd tc hs.ehs_s in - let ty_distr = proj_distr_ty env (e_ty distr) in - let x_id = EcIdent.create (symbol_of_lv lv) in - let x = f_local x_id ty_distr in - let m = fst hs.ehs_m in - let distr = EcFol.ss_inv_of_expr m distr in - let post = subst_form_lv env lv {m;inv=x} (ehs_po hs) in - let post = map_ss_inv2 (f_Ep ty_distr) distr - (map_ss_inv1 (f_lambda [(x_id,GTty ty_distr)]) post) in - let concl = f_eHoareS (snd hs.ehs_m) (ehs_pr hs) s post in - FApi.xmutate1 tc `Rnd [concl] - - (* -------------------------------------------------------------------- *) - let wp_equiv_disj_rnd_r side tc = - let env = FApi.tc1_env tc in - let es = tc1_as_equivS tc in - let ml, mr = fst es.es_ml, fst es.es_mr in - let m, mo, s = - match side with - | `Left -> es.es_ml, fst es.es_mr, es.es_sl - | `Right -> es.es_mr, fst es.es_ml, es.es_sr - in - let subst_form_lv_side = sideif side subst_form_lv_left subst_form_lv_right in - let ss_inv_generalize_other = - sideif side ss_inv_generalize_right ss_inv_generalize_left in - (* FIXME: exception when not rnds found *) - let (lv, distr), s = tc1_last_rnd tc s in - let ty_distr = proj_distr_ty env (e_ty distr) in - - let x_id = EcIdent.create (symbol_of_lv lv) in - let x = {ml; mr; inv=f_local x_id ty_distr} in - - let distr = EcFol.ss_inv_of_expr (EcMemory.memory m) distr in - let distr = ss_inv_generalize_other distr mo in - let post = subst_form_lv_side env lv x (es_po es) in - let post = map_ts_inv2 f_imp (map_ts_inv2 f_in_supp x distr) post in - let post = map_ts_inv1 (f_forall_simpl [(x_id,GTty ty_distr)]) post in - let post = map_ts_inv2 f_anda (map_ts_inv1 (f_lossless ty_distr) distr) post in - let concl = - match side with - | `Left -> f_equivS (snd es.es_ml) (snd es.es_mr) (es_pr es) s es.es_sr post - | `Right -> f_equivS (snd es.es_ml) (snd es.es_mr) (es_pr es) es.es_sl s post - in - FApi.xmutate1 tc `Rnd [concl] - - (* -------------------------------------------------------------------- *) - let wp_equiv_rnd_r bij tc = - let env = FApi.tc1_env tc in - let es = tc1_as_equivS tc in - let ml, mr = fst es.es_ml, fst es.es_mr in - let (lvL, muL), sl' = tc1_last_rnd tc es.es_sl in - let (lvR, muR), sr' = tc1_last_rnd tc es.es_sr in - let tyL = proj_distr_ty env (e_ty muL) in - let tyR = proj_distr_ty env (e_ty muR) in - let xL_id = EcIdent.create (symbol_of_lv lvL ^ "L") - and xR_id = EcIdent.create (symbol_of_lv lvR ^ "R") in - let xL = {ml;mr;inv=f_local xL_id tyL} in - let xR = {ml;mr;inv=f_local xR_id tyR} in - let muL = EcFol.ss_inv_of_expr ml muL in - let muR = EcFol.ss_inv_of_expr mr muR in - - let tf, tfinv = - match bij with - | Some (f, finv) -> (f tyL tyR, finv tyR tyL) - | None -> - if not (EcReduction.EqTest.for_type env tyL tyR) then - tc_error !!tc "%s, %s" - "support are not compatible" - "an explicit bijection is required"; - ({ml;mr;inv=EcFol.f_identity ~name:"z" tyL}, - {ml;mr;inv=EcFol.f_identity ~name:"z" tyR}) - in - - (* (∀ x₂, x₂ ∈ ℑ(D₂) ⇒ x₂ = f(f⁻¹(x₂)) - * && (∀ x₂, x₂ ∈ ℑ(D₂) ⇒ μ(x₂, D₂) = μ(f⁻¹(x₂), D₁)) - * && (∀ x₁, x₁ ∈ ℑ(D₁) ⇒ f(x₁) ∈ ℑ(D₂) && x₁ = f⁻¹(f(x₁)) && φ(x₁, f(x₁))) - *) - - let f_app_simpl' ty f t = f_app_simpl f [t] ty in - let f t = map_ts_inv2 (f_app_simpl' tyR) tf t in - let finv t = map_ts_inv2 (f_app_simpl' tyL) tfinv t in - - let post = subst_form_lv_left env lvL xL (es_po es) in - let post = subst_form_lv_right env lvR (f xL) post in - - let muL = ss_inv_generalize_right muL mr in - let muR = ss_inv_generalize_left muR ml in - - let cond_fbij = map_ts_inv2 f_eq xL (finv (f xL)) in - let cond_fbij_inv = map_ts_inv2 f_eq xR (f (finv xR)) in - - let cond1 = map_ts_inv2 f_imp (map_ts_inv2 f_in_supp xR muR) cond_fbij_inv in - let cond2 = map_ts_inv2 f_imp (map_ts_inv2 f_in_supp xR muR) (map_ts_inv2 f_eq (map_ts_inv2 f_mu_x muR xR) (map_ts_inv2 f_mu_x muL (finv xR))) in - let cond3 = map_ts_inv f_andas [map_ts_inv2 f_in_supp (f xL) muR; cond_fbij; post] in - let cond3 = map_ts_inv2 f_imp (map_ts_inv2 f_in_supp xL muL) cond3 in - - let concl = map_ts_inv f_andas - [map_ts_inv1 (f_forall_simpl [(xR_id, GTty tyR)]) cond1; - map_ts_inv1 (f_forall_simpl [(xR_id, GTty tyR)]) cond2; - map_ts_inv1 (f_forall_simpl [(xL_id, GTty tyL)]) cond3] in - - let concl = f_equivS (snd es.es_ml) (snd es.es_mr) (es_pr es) sl' sr' concl in - - FApi.xmutate1 tc `Rnd [concl] - - (* -------------------------------------------------------------------- *) - let t_bdhoare_rnd_r tac_info tc = - let env = FApi.tc1_env tc in - let bhs = tc1_as_bdhoareS tc in - let (lv,distr),s = tc1_last_rnd tc bhs.bhs_s in - let ty_distr = proj_distr_ty env (e_ty distr) in - let distr = EcFol.ss_inv_of_expr (EcMemory.memory bhs.bhs_m) distr in - let m = fst bhs.bhs_m in - let mk_event_cond event = - let v_id = EcIdent.create "v" in - let v = {m; inv=f_local v_id ty_distr} in - let post_v = subst_form_lv env lv v (bhs_po bhs) in - let f_app' fl = f_app (List.hd fl) (List.tl fl) tbool in - let event_v = map_ss_inv f_app' [event ;v] in - let v_in_supp = map_ss_inv2 f_in_supp v distr in - map_ss_inv1 (f_forall_simpl [v_id,GTty ty_distr]) - begin - let f_imps_simpl' fl = f_imps_simpl (List.tl fl) (List.hd fl) in - match bhs.bhs_cmp with - | FHle -> map_ss_inv f_imps_simpl' [event_v; v_in_supp;post_v] - | FHge -> map_ss_inv f_imps_simpl' [post_v; v_in_supp;event_v] - | FHeq -> map_ss_inv2 f_imp_simpl v_in_supp (map_ss_inv2 f_iff_simpl event_v post_v) - end - in - let f_cmp = match bhs.bhs_cmp with - | FHle -> f_real_le - | FHge -> fun x y -> f_real_le y x - | FHeq -> f_eq - in - let is_post_indep = - let fv = EcPV.PV.fv env (bhs_po bhs).m (bhs_po bhs).inv in - match lv with - | LvVar (x,_) -> not (EcPV.PV.mem_pv env x fv) - | LvTuple pvs -> - List.for_all (fun (x,_) -> not (EcPV.PV.mem_pv env x fv)) pvs - in - let is_bd_indep = - let fv_bd = PV.fv env (bhs_bd bhs).m (bhs_bd bhs).inv in - let modif_s = s_write env s in - PV.indep env modif_s fv_bd - in - let mk_event ?(simpl=true) ty = - let x = EcIdent.create "x" in - if is_post_indep && simpl then f_predT ty - else match lv with - | LvVar (pv,_) -> - f_lambda [x,GTty ty] - (EcPV.PVM.subst1 env pv m (f_local x ty) (bhs_po bhs).inv) - | _ -> tc_error !!tc "cannot infer a valid event, it must be provided" - in - let bound,pre_bound,binders = - if is_bd_indep then - bhs_bd bhs, {m;inv=f_true}, [] - else - let bd_id = EcIdent.create "bd" in - let bd = {m;inv=f_local bd_id treal} in - bd, map_ss_inv2 f_eq (bhs_bd bhs) bd, [(bd_id,GTty treal)] - in - let nonneg_concl = - f_forall_mems_ss_inv bhs.bhs_m - (map_ss_inv2 f_real_le {m;inv=f_r0} (bhs_bd bhs)) in - match tac_info, bhs.bhs_cmp with - | PNoRndParams, FHle -> - if is_post_indep then - (* event is true *) - let concl = f_bdHoareS (snd bhs.bhs_m) - (bhs_pr bhs) s (bhs_po bhs) bhs.bhs_cmp (bhs_bd bhs) in - FApi.xmutate1 tc `Rnd [concl] - else - let event = {m; inv=mk_event ty_distr} in - let bounded_distr = map_ss_inv2 f_real_le (map_ss_inv2 (f_mu env) distr event) bound in - let pre = map_ss_inv2 f_and (bhs_pr bhs) pre_bound in - let post = map_ss_inv2 f_anda bounded_distr (mk_event_cond event) in - let post = POE.lift post in - let concl = f_hoareS (snd bhs.bhs_m) pre s post in - let concl = f_forall_simpl binders concl in - (* the hoare post only constrains the terminating runs of [s]: also - require [0%r <= bd] (in every memory); closed here when trivial *) - FApi.t_last (FApi.t_try t_trivial) (FApi.xmutate1 tc `Rnd [concl; nonneg_concl]) - | PNoRndParams, _ -> - if is_post_indep then - (* event is true *) - let event = {m;inv=mk_event ty_distr} in - let f_r1 = {m;inv=f_r1} in - let bounded_distr = map_ss_inv2 f_eq (map_ss_inv2 (f_mu env) distr event) f_r1 in - let post = map_ss_inv2 f_and (bhs_po bhs) bounded_distr in - let concl = f_bdHoareS (snd bhs.bhs_m) (bhs_pr bhs) s post bhs.bhs_cmp (bhs_bd bhs) in - FApi.xmutate1 tc `Rnd [concl] - else - let event = {m;inv=mk_event ty_distr} in - let bounded_distr = map_ss_inv2 f_cmp (map_ss_inv2 (f_mu env) distr event) bound in - let pre = map_ss_inv2 f_and (bhs_pr bhs) pre_bound in - let post = map_ss_inv2 f_anda bounded_distr (mk_event_cond event) in - let concl = f_bdHoareS (snd bhs.bhs_m) pre s post bhs.bhs_cmp {m;inv=f_r1} in - let concl = f_forall_simpl binders concl in - FApi.xmutate1 tc `Rnd [concl] - | PSingleRndParam event, FHle -> - let event = event ty_distr in - let bounded_distr = map_ss_inv2 f_real_le (map_ss_inv2 (f_mu env) distr event) bound in - let pre = map_ss_inv2 f_and (bhs_pr bhs) pre_bound in - let post = map_ss_inv2 f_anda bounded_distr (mk_event_cond event) in - let post = POE.lift post in - let concl = f_hoareS (snd bhs.bhs_m) pre s post in - let concl = f_forall_simpl binders concl in - (* the hoare post only constrains the terminating runs of [s]: also - require [0%r <= bd] (in every memory); closed here when trivial *) - FApi.t_last (FApi.t_try t_trivial) (FApi.xmutate1 tc `Rnd [concl; nonneg_concl]) - | PSingleRndParam event, _ -> - let event = event ty_distr in - let bounded_distr = map_ss_inv2 f_cmp (map_ss_inv2 (f_mu env) distr event) bound in - let pre = map_ss_inv2 f_and (bhs_pr bhs) pre_bound in - let post = map_ss_inv2 f_anda bounded_distr (mk_event_cond event) in - let concl = f_bdHoareS (snd bhs.bhs_m) pre s post FHeq {m;inv=f_r1} in - let concl = f_forall_simpl binders concl in - FApi.xmutate1 tc `Rnd [concl] - | PMultRndParams ((phi,d1,d2,d3,d4),event), _ -> - (* [d2] and [d4] are interpreted after [s] in [sgoal2] and [sgoal4], - and in the initial memory in [bd_sgoal]: the two coincide only if - [s] does not write them. *) - List.iter (fun (d : ss_inv) -> - if not (PV.indep env (s_write env s) (PV.fv env d.m d.inv)) then - tc_error !!tc - "The bounds on the probability of the sampling (third and \ - fifth arguments) cannot depend on variables written by the \ - statements preceding the sampling") - [d2; d4]; - let event = match event ty_distr with - | None -> {m;inv=mk_event ~simpl:false ty_distr} | Some event -> event - in - let bd_sgoal = map_ss_inv2 f_cmp (map_ss_inv2 f_real_add (map_ss_inv2 f_real_mul d1 d2) (map_ss_inv2 f_real_mul d3 d4)) (bhs_bd bhs) in - let bd_sgoal = f_forall_mems_ss_inv (bhs.bhs_m) bd_sgoal in - let sgoal1 = f_bdHoareS (snd bhs.bhs_m) (bhs_pr bhs) s phi bhs.bhs_cmp d1 in - let sgoal2 = - let bounded_distr = map_ss_inv2 f_cmp (map_ss_inv2 (f_mu env) distr event) d2 in - let post = map_ss_inv2 f_anda bounded_distr (mk_event_cond event) in - f_forall_mems_ss_inv (bhs.bhs_m) (map_ss_inv2 f_imp phi post) - in - let sgoal3 = f_bdHoareS (snd bhs.bhs_m) (bhs_pr bhs) s (map_ss_inv1 f_not phi) bhs.bhs_cmp d3 in - let sgoal4 = - let bounded_distr = map_ss_inv2 f_cmp (map_ss_inv2 (f_mu env) distr event) d4 in - let post = map_ss_inv2 f_anda bounded_distr (mk_event_cond event) in - f_forall_mems_ss_inv bhs.bhs_m (map_ss_inv2 f_imp (map_ss_inv1 f_not phi) post) in - let sgoal5 = - let f_inbound x = - let f_r1, f_r0 = {m;inv=f_r1}, {m;inv=f_r0} in - map_ss_inv2 f_anda (map_ss_inv2 f_real_le f_r0 x) (map_ss_inv2 f_real_le x f_r1) in - map_ss_inv f_ands (List.map f_inbound [d1; d2; d3; d4]) - in - let sgoal5 = f_forall_mems_ss_inv (bhs.bhs_m) sgoal5 in - FApi.xmutate1 tc `Rnd [bd_sgoal;sgoal1;sgoal2;sgoal3;sgoal4;sgoal5] - - | _, _ -> tc_error !!tc "invalid arguments" - - (* -------------------------------------------------------------------- *) - let semrnd tc mem used (s : instr list) : EcMemory.memenv * instr list = - let error () = tc_error !!tc "semrnd" in - - let env = FApi.tc1_env tc in - let wr, gwr = PV.elements (is_write env s) in - let wr = - match used with - | None -> wr - | Some used -> List.filter (fun (pv, _) -> PV.mem_pv env pv used) wr in - - if not (List.is_empty gwr) then - error (); - - let open EcPV in - - let wr = - let add (m, idx) pv = - if is_some (PVMap.find pv m) - then (m, idx) - else (PVMap.add pv idx m, idx+1) in - - let m, idx = - List.fold_left (fun (m, idx) { i_node = i } -> - match i with - | Sasgn (lv, _) | Srnd (lv, _) -> - List.fold_left add (m, idx) (lv_to_list lv) - | _ -> (m, idx) - ) - (PVMap.create env, 0) s in - - let m, _ = - List.fold_left - (fun (m, idx) (pv, _) -> add (m, idx) pv) - (m, idx) - wr in - - List.sort - (fun (pv1, _) (pv2, _) -> - compare (PVMap.find pv1 m) (PVMap.find pv2 m)) - wr in - - let rec do1 (m: memory) (subst : PVM.subst) (s : instr list) = - match s with - | [] -> - let tuple = - List.map (fun (pv, _) -> - PVM.find env pv m subst) wr in - {m;inv=f_dunit (f_tuple tuple)} - - | { i_node = Sasgn (lv, e) } :: s -> - let e = ss_inv_of_expr m e in - let e = map_ss_inv1 (PVM.subst env subst) e in - let subst = - match lv with - | LvVar (pv, _) -> - PVM.add env pv m e.inv subst - | LvTuple pvs -> - List.fold_lefti (fun subst i (pv, ty) -> - PVM.add env pv m (f_proj e.inv i ty) subst - ) subst pvs - in - do1 m subst s - - | { i_node = Srnd (lv, d) } :: s -> - let d = ss_inv_of_expr m d in - let d = map_ss_inv1 (PVM.subst env subst) d in - let x = EcIdent.create (name_of_lv lv) in - let subst, xty = - match lv with - | LvVar (pv, ty) -> - let x = f_local x ty in - (PVM.add env pv m x subst, ty) - | LvTuple pvs -> - let ty = ttuple (List.snd pvs) in - let x = f_local x ty in - let subst = - List.fold_lefti (fun subst i (pv, ty) -> - PVM.add env pv m (f_proj x i ty) subst - ) subst pvs in - (subst, ty) - in - let body = do1 m subst s in - - map_ss_inv2 - (f_dlet_simpl - xty - (ttuple (List.snd wr))) - d - (map_ss_inv1 (f_lambda [(x, GTty xty)]) body) - - | _ :: _ -> - error () - - in - - let mhr = EcIdent.create "&hr" in - let distr = do1 mhr PVM.empty s in - let distr = expr_of_ss_inv distr in - - match lv_of_list wr with - | None -> - let x = { ov_name = Some "x"; ov_type = tunit; } in - let mem, x = EcMemory.bind_fresh x mem in - let x, xty = pv_loc (oget x.ov_name), x.ov_type in - (mem, [i_rnd (LvVar (x, xty), distr)]) - | Some wr -> - (mem, [i_rnd (wr, distr)]) - - (* -------------------------------------------------------------------- *) - let t_hoare_rndsem_r reduce pos tc = - let env = FApi.tc1_env tc in - let hs = tc1_as_hoareS tc in - let s1, s2 = o_split env (Some pos) hs.hs_s in - if (not (POE.is_empty (hs_po hs).hsi_inv)) then - tc_error !!tc "exceptions are not supported"; - let post = POE.lower (hs_po hs) in - let fv = - if reduce then - Some (PV.fv (FApi.tc1_env tc) (fst hs.hs_m) post.inv) - else None in - let (_, mt), s2 = semrnd tc hs.hs_m fv s2 in - let concl = - f_hoareS mt (hs_pr hs) (stmt (s1 @ s2)) (hs_po hs) - in - FApi.xmutate1 tc (`RndSem pos) [concl] - - (* -------------------------------------------------------------------- *) - let t_bdhoare_rndsem_r reduce pos tc = - let env = FApi.tc1_env tc in - let bhs = tc1_as_bdhoareS tc in - let s1, s2 = o_split env (Some pos) bhs.bhs_s in - let fv = - if reduce then - Some (PV.fv (FApi.tc1_env tc) (fst bhs.bhs_m) (bhs_po bhs).inv) - else None in - let (_,mt), s2 = semrnd tc bhs.bhs_m fv s2 in - let concl = f_bdHoareS mt (bhs_pr bhs) (stmt (s1 @ s2)) (bhs_po bhs) bhs.bhs_cmp (bhs_bd bhs) in - FApi.xmutate1 tc (`RndSem pos) [concl] - - (* -------------------------------------------------------------------- *) - let t_equiv_rndsem_r reduce side pos tc = - let env = FApi.tc1_env tc in - let es = tc1_as_equivS tc in - let s, m = - match side with - | `Left -> es.es_sl, es.es_ml - | `Right -> es.es_sr, es.es_mr in - let s1, s2 = o_split env (Some pos) s in - let fv = - if reduce then - Some (PV.fv (FApi.tc1_env tc) (fst m) (es_po es).inv) - else None in - let (_,mt), s2 = semrnd tc m fv s2 in - let s = stmt (s1 @ s2) in - let concl = - match side with - | `Left -> f_equivS mt (snd es.es_mr) (es_pr es) s es.es_sr (es_po es) - | `Right -> f_equivS (snd es.es_ml) mt (es_pr es) es.es_sl s (es_po es) in - FApi.xmutate1 tc (`RndSem pos) [concl] - -end (* Core *) +let wp_equiv_disj_rnd = EcEquivRnd.t_equiv_rnd_onesided_last +let wp_equiv_rnd = EcEquivRnd.t_equiv_rnd_last (* -------------------------------------------------------------------- *) -module E = struct exception Abort end - -let solve n f tc = - let tt = - FApi.t_seqs - [EcLowGoal.t_intros_n n; - EcLowGoal.t_solve ~bases:["random"] ~depth:2; - EcLowGoal.t_fail] in +let t_hoare_rnd = EcHoareRnd.t_hoare_rnd_last - let subtc, hd = FApi.newgoal tc f in +let t_bdhoare_rnd (info : bhl_infos_t) = + EcBdHoareRnd.(t_bdhoare_rnd_full { brr_info = info }) - try - let subtc = - FApi.t_last - (fun tc1 -> - match FApi.t_try_base tt tc1 with - | `Failure _ -> raise E.Abort - | `Success tc -> tc) - subtc - in (subtc, Some hd) - - with E.Abort -> tc, None - -let t_apply_prept pt tc = - Apply.t_apply_bwd_r (EcProofTerm.pt_of_prept tc pt) tc - -(* -------------------------------------------------------------------- *) -let wp_equiv_disj_rnd_r side tc = - - let tc = Core.wp_equiv_disj_rnd_r side tc in - let es = tc1_as_equivS (FApi.as_tcenv1 tc) in - let (c1, c2) = map_ts_inv_destr2 destr_and (es_po es) in - let newc1 = EcSubst.f_forall_mems_ts_inv es.es_ml es.es_mr c1 in - - let subtc = tc in - let subtc, hdc1 = solve 2 newc1 subtc in - - match hdc1 with - | None -> tc - | Some hd -> - let po = c2 in - FApi.t_onalli (function - | 0 -> fun tc -> EcLowGoal.t_trivial tc - | 1 -> - let open EcProofTerm.Prept in - let m1 = EcIdent.create "_" in - let m2 = EcIdent.create "_" in - let h = EcIdent.create "_" in - let h1 = EcIdent.create "_" in - (t_intros_i [m1; m2; h] @! - (t_split @+ - [ t_apply_prept (hdl hd @ [amem m1; amem m2]); - t_intros_i [h1] @! t_apply_hyp h])) - - | _ -> EcLowGoal.t_id) - (FApi.t_first - (EcPhlConseq.t_equivS_conseq (es_pr es) po) - subtc) - -(* -------------------------------------------------------------------- *) -let wp_equiv_rnd_r bij tc = - let tc = Core.wp_equiv_rnd_r bij tc in - let es = tc1_as_equivS (FApi.as_tcenv1 tc) in - - let c1, c2, c3 = map_ts_inv_destr3 destr_and3 (es_po es) in - let (x, xty, _) = destr_forall1 c3.inv in - let c3 = map_ts_inv1 (fun c3 -> let (_,_,d) = destr_forall1 c3 in d) c3 in - let (ind, c3) = map_ts_inv_destr2 destr_imp c3 in - let (c3, c4) = map_ts_inv_destr2 destr_and c3 in - let newc2 = EcSubst.f_forall_mems_ts_inv es.es_ml es.es_mr c2 in - let newc3 = EcSubst.f_forall_mems_ts_inv es.es_ml es.es_mr - (map_ts_inv1 (f_forall [x, xty]) (map_ts_inv2 f_imp ind c3)) in - - let subtc = tc in - let subtc, hdc2 = solve 4 newc2 subtc in - let subtc, hdc3 = solve 4 newc3 subtc in - - let po = - match hdc2, hdc3 with - | None , None -> None - | Some _, Some _ -> - Some (map_ts_inv2 f_anda c1 (map_ts_inv1 (f_forall [x, xty]) (map_ts_inv2 f_imp ind c4))) - | Some _, None -> - Some (map_ts_inv2 f_anda c1 (map_ts_inv1 (f_forall [x, xty]) (map_ts_inv2 f_imp ind (map_ts_inv2 f_anda c3 c4)))) - | None , Some _ -> - Some (map_ts_inv f_andas [c1; c2; map_ts_inv1 (f_forall [x, xty]) (map_ts_inv2 f_imp ind c4)]) - in - - match po with None -> tc | Some po -> - - let m1 = EcIdent.create "_" in - let m2 = EcIdent.create "_" in - let h = EcIdent.create "_" in - let h1 = EcIdent.create "_" in - let h2 = EcIdent.create "_" in - let x = EcIdent.create "_" in - let hin = EcIdent.create "_" in - - FApi.t_onalli (function - | 0 -> fun tc -> EcLowGoal.t_trivial tc - | 1 -> - let open EcProofTerm.Prept in - - let t_c2 = - let pt = - match hdc2 with - | None -> hyp h2 - | Some hd -> hdl hd @ [amem m1; amem m2] in - t_apply_prept pt in - - let t_c3_c4 = - match hdc3 with - | None -> t_apply_prept (hyp h) - | Some hd -> - let fx = f_local x (gty_as_ty xty) in - t_intros_i [x; hin] @! t_split - @+ [ t_apply_prept (hdl hd @ [amem m1; amem m2; aform fx; ahyp hin]); - t_intros_n 1 @! - t_apply_prept ((hyp h) @ [aform fx; ahyp hin])] - in - - let t_case_c2 = - match hdc2 with - | None -> t_elim_and @! t_intros_i [h2; h] - | Some _ -> t_intros_i [h] in - - t_intros_i [m1; m2] @! t_elim_and @! t_intros_i [h1] @! t_case_c2 @! t_split @+ - [ t_apply_prept (hyp h1); - t_intros_n 1 @! t_split @+ - [ t_c2; - t_intros_n 1 @! t_c3_c4 - ] - ] - - | _ -> EcLowGoal.t_id) - - (FApi.t_first - (EcPhlConseq.t_equivS_conseq (es_pr es) po) - subtc) - -(* -------------------------------------------------------------------- *) -let t_equiv_rnd_r side (pos: semrndpos option) bij_info tc = - match side, pos, bij_info with - | Some side, None, (None, None) -> - wp_equiv_disj_rnd_r side tc - | Some _side, None, _ -> - tc_error !!tc "one-sided rnd takes no arguments" - | None, _, _ -> begin - let pos = - match pos with - | None -> None - | Some (Single i) -> Some (i, i) - | Some (Double (il, ir)) -> Some (il, ir) in - - let tc = - match pos with - | None -> - t_id tc - | Some ((bl, il), (br, ir)) -> - FApi.t_seq - (Core.t_equiv_rndsem_r bl `Left il) - (Core.t_equiv_rndsem_r br `Right ir) - tc in - - let bij = - match bij_info with - | Some f, Some finv -> Some (f, finv) - | Some bij, None | None, Some bij -> Some (bij, bij) - | None, None -> None - in - FApi.t_first (wp_equiv_rnd_r bij) tc - end - - | _ -> - tc_error !!tc "two-sided rnd requires a bijection" - -(* -------------------------------------------------------------------- *) -let wp_equiv_disj_rnd = FApi.t_low1 "wp-equiv-disj-rnd" wp_equiv_disj_rnd_r -let wp_equiv_rnd = FApi.t_low1 "wp-equiv-rnd" wp_equiv_rnd_r - -(* -------------------------------------------------------------------- *) -let t_hoare_rnd = FApi.t_low0 "hoare-rnd" Core.t_hoare_rnd_r -let t_ehoare_rnd = FApi.t_low0 "ehoare-rnd" Core.t_ehoare_rnd_r -let t_bdhoare_rnd = FApi.t_low1 "bdhoare-rnd" Core.t_bdhoare_rnd_r - -let t_equiv_rnd ?pos side bij_info = - (FApi.t_low3 "equiv-rnd" t_equiv_rnd_r) side pos bij_info +let t_equiv_rnd = EcEquivRnd.t_equiv_rnd_full (* -------------------------------------------------------------------- *) +(* Dispatch on the goal kind only; each logic owns its surface-syntax + handling. *) let process_rnd (side : side option) (pos : psemrndpos option) - (tac_info : _) + (tac_info : rnd_infos_t) (tc : tcenv1) = - let concl = FApi.tc1_goal tc in - - match side, pos, tac_info with - | None, None, PNoRndParams when is_hoareS concl -> - t_hoare_rnd tc - - | None, None, PNoRndParams when is_eHoareS concl -> - t_ehoare_rnd tc - - | None, None, _ when is_bdHoareS concl -> - let tac_info = - match tac_info with - | PNoRndParams -> - PNoRndParams - - | PSingleRndParam fp -> - PSingleRndParam - (fun t -> snd (TTC.tc1_process_Xhl_form tc (tfun t tbool) fp)) - - | PMultRndParams ((phi, d1, d2, d3, d4), p) -> - let p t = p |> omap (fun p -> snd (TTC.tc1_process_Xhl_form tc (tfun t tbool) p)) in - let _, phi = TTC.tc1_process_Xhl_form tc tbool phi in - let _, d1 = TTC.tc1_process_Xhl_form tc treal d1 in - let _, d2 = TTC.tc1_process_Xhl_form tc treal d2 in - let _, d3 = TTC.tc1_process_Xhl_form tc treal d3 in - let _, d4 = TTC.tc1_process_Xhl_form tc treal d4 in - PMultRndParams ((phi, d1, d2, d3, d4), p) - - | _ -> tc_error !!tc "invalid arguments" - in - t_bdhoare_rnd tac_info tc - - | _, _, _ when is_equivS concl -> - let process_form f ty1 ty2 = - TTC.tc1_process_prhl_form tc (tfun ty1 ty2) f in - - let bij_info = - match tac_info with - | PNoRndParams -> None, None - | PSingleRndParam f -> Some (process_form f), None - | PTwoRndParams (f, finv) -> Some (process_form f), Some (process_form finv) - | _ -> tc_error !!tc "invalid arguments" - in - - let pos = pos |> Option.map (function - | Single (b, p) -> - let p = - if Option.is_some side then - EcLowPhlGoal.tc1_process_codegap1 tc (side, p) - else EcTyping.trans_codegap1 (FApi.tc1_env tc) p - in Single (b, p) - | Double ((b1, p1), (b2, p2)) -> - let p1 = EcLowPhlGoal.tc1_process_codegap1 tc (Some `Left , p1) in - let p2 = EcLowPhlGoal.tc1_process_codegap1 tc (Some `Right, p2) in - Double ((b1, p1), (b2, p2)) - ) - in - - t_equiv_rnd side ?pos bij_info tc - + match (FApi.tc1_goal tc).f_node with + | FhoareS _ -> EcHoareRnd.process_hoare_rnd side pos tac_info tc + | FeHoareS _ -> EcEHoareRnd.process_ehoare_rnd side pos tac_info tc + | FbdHoareS _ -> EcBdHoareRnd.process_bdhoare_rnd side pos tac_info tc + | FequivS _ -> EcEquivRnd.process_equiv_rnd side pos tac_info tc | _ -> tc_error !!tc "invalid arguments" (* -------------------------------------------------------------------- *) -let t_hoare_rndsem = FApi.t_low2 "hoare-rndsem" Core.t_hoare_rndsem_r -let t_bdhoare_rndsem = FApi.t_low2 "bdhoare-rndsem" Core.t_bdhoare_rndsem_r -let t_equiv_rndsem = FApi.t_low3 "equiv-rndsem" Core.t_equiv_rndsem_r - -(* -------------------------------------------------------------------- *) -let process_rndsem ~reduce side pos tc = - let concl = FApi.tc1_goal tc in - let pos = EcLowPhlGoal.tc1_process_codegap1 tc (side, pos) in - - match side with - | None when is_hoareS concl -> - t_hoare_rndsem reduce pos tc - | None when is_bdHoareS concl -> - t_bdhoare_rndsem reduce pos tc - | Some side when is_equivS concl -> - t_equiv_rndsem reduce side pos tc - | _ -> tc_error !!tc "invalid arguments" +let process_rndsem ~reduce side pos (tc : tcenv1) = + match (FApi.tc1_goal tc).f_node with + | FhoareS _ -> EcHoareRndSem.process_hoare_rndsem ~reduce side pos tc + | FbdHoareS _ -> EcBdHoareRndSem.process_bdhoare_rndsem ~reduce side pos tc + | FequivS _ -> EcEquivRndSem.process_equiv_rndsem ~reduce side pos tc + | _ -> + (* The position is typed first, as before the migration: this reports + a goal of the wrong kind, when it is not a program-logic one. *) + ignore (EcLowPhlGoal.tc1_process_codegap1 tc (side, pos) : codegap1); + tc_error !!tc "invalid arguments" diff --git a/src/phl/rules/bdhoare/ecBdHoareRnd.ml b/src/phl/rules/bdhoare/ecBdHoareRnd.ml new file mode 100644 index 000000000..bce5ee663 --- /dev/null +++ b/src/phl/rules/bdhoare/ecBdHoareRnd.ml @@ -0,0 +1,298 @@ +(* -------------------------------------------------------------------- *) +open EcParsetree +open EcTypes +open EcModules +open EcFol +open EcAst +open EcEnv +open EcPV +open EcSubst + +open EcCoreGoal +open EcLowGoal +open EcLowPhlGoal + +module TTC = EcProofTyping + +(* -------------------------------------------------------------------- *) +(* Parameters of the bdhoare [rnd] rule as supplied by the caller: high level, + the event and the bounds may depend on the (not yet known) type of the + sampled values. *) +type bdhoare_rnd_rule = { + brr_info : (ss_inv, ty -> ss_inv option, ty -> ss_inv) rnd_tac_info; +} + +(* Low-level parameters recorded in the proof-node: the event and the bounds + instantiated at the type of the sampled values. *) +type bdhoare_rnd_split = { + brs_phi : ss_inv; (* condition splitting the prefix runs *) + brs_d1 : ss_inv; (* bound for the prefix, under phi *) + brs_d2 : ss_inv; (* bound for the sampling, under phi *) + brs_d3 : ss_inv; (* bound for the prefix, under !phi *) + brs_d4 : ss_inv; (* bound for the sampling, under !phi *) + brs_event : ss_inv option; (* event (inferred when absent) *) +} + +type bdhoare_rnd_node = + | BRndInfer (* no argument: the event is inferred *) + | BRndEvent of ss_inv (* the event *) + | BRndSplit of bdhoare_rnd_split + +type EcCoreGoal.rule += RBdHoareRnd of bdhoare_rnd_node + +(* -------------------------------------------------------------------- *) +(* Raised when the event must be inferred from the postcondition, but the + sampling assigns a tuple. *) +exception CannotInferEvent + +(* Raised when the bounds [d2] / [d4] of form (5) depend on variables + written by the statements preceding the sampling. *) +exception BoundWrittenByPrefix + +(* -------------------------------------------------------------------- *) +(* The postcondition does not mention the sampled variables. *) +let bdhoare_rnd_post_indep env (bhs : bdHoareS) (lv : lvalue) = + let fv = PV.fv env (bhs_po bhs).m (bhs_po bhs).inv in + match lv with + | LvVar (x,_) -> not (PV.mem_pv env x fv) + | LvTuple pvs -> + List.for_all (fun (x,_) -> not (PV.mem_pv env x fv)) pvs + +(* -------------------------------------------------------------------- *) +(* Pure core shared by the rule and its checker. Its side conditions (the + last instruction is a sampling; an event can be inferred when needed) are + part of it, so the checker re-validates them. *) +let bdhoare_rnd_subgoals + (hyps : LDecl.hyps) (bhs : bdHoareS) (n : bdhoare_rnd_node) : form list += + let env = LDecl.toenv hyps in + let (lv, distr), s = + match s_last destr_rnd bhs.bhs_s with + | Some x -> x + | None -> failwith "bdhoare-rnd: the last instruction is not a sampling" in + let m = fst bhs.bhs_m in + let rb (f : ss_inv) = ss_inv_rebind f m in + let ty_distr = proj_distr_ty env (e_ty distr) in + let distr = EcFol.ss_inv_of_expr m distr in + let mk_event_cond event = + let v_id = EcIdent.create "v" in + let v = {m; inv=f_local v_id ty_distr} in + let post_v = subst_form_lv env lv v (bhs_po bhs) in + let f_app' fl = f_app (List.hd fl) (List.tl fl) tbool in + let event_v = map_ss_inv f_app' [event ;v] in + let v_in_supp = map_ss_inv2 f_in_supp v distr in + map_ss_inv1 (f_forall_simpl [v_id,GTty ty_distr]) + begin + let f_imps_simpl' fl = f_imps_simpl (List.tl fl) (List.hd fl) in + match bhs.bhs_cmp with + | FHle -> map_ss_inv f_imps_simpl' [event_v; v_in_supp;post_v] + | FHge -> map_ss_inv f_imps_simpl' [post_v; v_in_supp;event_v] + | FHeq -> map_ss_inv2 f_imp_simpl v_in_supp (map_ss_inv2 f_iff_simpl event_v post_v) + end + in + let f_cmp = match bhs.bhs_cmp with + | FHle -> f_real_le + | FHge -> fun x y -> f_real_le y x + | FHeq -> f_eq + in + let is_post_indep = bdhoare_rnd_post_indep env bhs lv in + let is_bd_indep = + let fv_bd = PV.fv env (bhs_bd bhs).m (bhs_bd bhs).inv in + let modif_s = s_write env s in + PV.indep env modif_s fv_bd + in + let mk_event ?(simpl=true) ty = + let x = EcIdent.create "x" in + if is_post_indep && simpl then f_predT ty + else match lv with + | LvVar (pv,_) -> + f_lambda [x,GTty ty] + (EcPV.PVM.subst1 env pv m (f_local x ty) (bhs_po bhs).inv) + | _ -> raise CannotInferEvent + in + let bound,pre_bound,binders = + if is_bd_indep then + bhs_bd bhs, {m;inv=f_true}, [] + else + let bd_id = EcIdent.create "bd" in + let bd = {m;inv=f_local bd_id treal} in + bd, map_ss_inv2 f_eq (bhs_bd bhs) bd, [(bd_id,GTty treal)] + in + let nonneg_concl = + f_forall_mems_ss_inv bhs.bhs_m + (map_ss_inv2 f_real_le {m;inv=f_r0} (bhs_bd bhs)) in + match n, bhs.bhs_cmp with + | BRndInfer, FHle -> + if is_post_indep then + (* event is true *) + let concl = f_bdHoareS (snd bhs.bhs_m) + (bhs_pr bhs) s (bhs_po bhs) bhs.bhs_cmp (bhs_bd bhs) in + [concl] + else + let event = {m; inv=mk_event ty_distr} in + let bounded_distr = map_ss_inv2 f_real_le (map_ss_inv2 (f_mu env) distr event) bound in + let pre = map_ss_inv2 f_and (bhs_pr bhs) pre_bound in + let post = map_ss_inv2 f_anda bounded_distr (mk_event_cond event) in + let post = POE.lift post in + let concl = f_hoareS (snd bhs.bhs_m) pre s post in + let concl = f_forall_simpl binders concl in + [concl; nonneg_concl] + | BRndInfer, _ -> + if is_post_indep then + (* event is true *) + let event = {m;inv=mk_event ty_distr} in + let f_r1 = {m;inv=f_r1} in + let bounded_distr = map_ss_inv2 f_eq (map_ss_inv2 (f_mu env) distr event) f_r1 in + let post = map_ss_inv2 f_and (bhs_po bhs) bounded_distr in + let concl = f_bdHoareS (snd bhs.bhs_m) (bhs_pr bhs) s post bhs.bhs_cmp (bhs_bd bhs) in + [concl] + else + let event = {m;inv=mk_event ty_distr} in + let bounded_distr = map_ss_inv2 f_cmp (map_ss_inv2 (f_mu env) distr event) bound in + let pre = map_ss_inv2 f_and (bhs_pr bhs) pre_bound in + let post = map_ss_inv2 f_anda bounded_distr (mk_event_cond event) in + let concl = f_bdHoareS (snd bhs.bhs_m) pre s post bhs.bhs_cmp {m;inv=f_r1} in + let concl = f_forall_simpl binders concl in + [concl] + | BRndEvent event, FHle -> + let event = rb event in + let bounded_distr = map_ss_inv2 f_real_le (map_ss_inv2 (f_mu env) distr event) bound in + let pre = map_ss_inv2 f_and (bhs_pr bhs) pre_bound in + let post = map_ss_inv2 f_anda bounded_distr (mk_event_cond event) in + let post = POE.lift post in + let concl = f_hoareS (snd bhs.bhs_m) pre s post in + let concl = f_forall_simpl binders concl in + [concl; nonneg_concl] + | BRndEvent event, _ -> + let event = rb event in + let bounded_distr = map_ss_inv2 f_cmp (map_ss_inv2 (f_mu env) distr event) bound in + let pre = map_ss_inv2 f_and (bhs_pr bhs) pre_bound in + let post = map_ss_inv2 f_anda bounded_distr (mk_event_cond event) in + let concl = f_bdHoareS (snd bhs.bhs_m) pre s post FHeq {m;inv=f_r1} in + let concl = f_forall_simpl binders concl in + [concl] + | BRndSplit sp, _ -> + let phi, d1, d2, d3, d4 = + rb sp.brs_phi, rb sp.brs_d1, rb sp.brs_d2, rb sp.brs_d3, rb sp.brs_d4 in + (* [d2] and [d4] are interpreted after [s] in [sgoal2] and [sgoal4], + and in the initial memory in [bd_sgoal]: the two coincide only if + [s] does not write them. *) + List.iter (fun (d : ss_inv) -> + if not (PV.indep env (s_write env s) (PV.fv env d.m d.inv)) then + raise BoundWrittenByPrefix) + [d2; d4]; + let event = match sp.brs_event with + | None -> {m;inv=mk_event ~simpl:false ty_distr} + | Some event -> rb event + in + let bd_sgoal = map_ss_inv2 f_cmp (map_ss_inv2 f_real_add (map_ss_inv2 f_real_mul d1 d2) (map_ss_inv2 f_real_mul d3 d4)) (bhs_bd bhs) in + let bd_sgoal = f_forall_mems_ss_inv (bhs.bhs_m) bd_sgoal in + let sgoal1 = f_bdHoareS (snd bhs.bhs_m) (bhs_pr bhs) s phi bhs.bhs_cmp d1 in + let sgoal2 = + let bounded_distr = map_ss_inv2 f_cmp (map_ss_inv2 (f_mu env) distr event) d2 in + let post = map_ss_inv2 f_anda bounded_distr (mk_event_cond event) in + f_forall_mems_ss_inv (bhs.bhs_m) (map_ss_inv2 f_imp phi post) + in + let sgoal3 = f_bdHoareS (snd bhs.bhs_m) (bhs_pr bhs) s (map_ss_inv1 f_not phi) bhs.bhs_cmp d3 in + let sgoal4 = + let bounded_distr = map_ss_inv2 f_cmp (map_ss_inv2 (f_mu env) distr event) d4 in + let post = map_ss_inv2 f_anda bounded_distr (mk_event_cond event) in + f_forall_mems_ss_inv bhs.bhs_m (map_ss_inv2 f_imp (map_ss_inv1 f_not phi) post) in + let sgoal5 = + let f_inbound x = + let f_r1, f_r0 = {m;inv=f_r1}, {m;inv=f_r0} in + map_ss_inv2 f_anda (map_ss_inv2 f_real_le f_r0 x) (map_ss_inv2 f_real_le x f_r1) in + map_ss_inv f_ands (List.map f_inbound [d1; d2; d3; d4]) + in + let sgoal5 = f_forall_mems_ss_inv (bhs.bhs_m) sgoal5 in + [bd_sgoal;sgoal1;sgoal2;sgoal3;sgoal4;sgoal5] + +(* -------------------------------------------------------------------- *) +(* Rule (TCB): instantiate the event and the bounds at the type of the + sampled values, record them in the node, and build the subgoals through + the shared core. *) +let t_bdhoare_rnd (r : bdhoare_rnd_rule) (tc : tcenv1) = + let env = FApi.tc1_env tc in + let bhs = tc1_as_bdhoareS tc in + let (_, distr), _ = tc1_last_rnd tc bhs.bhs_s in + let ty_distr = proj_distr_ty env (e_ty distr) in + let n = + match r.brr_info with + | PNoRndParams -> + BRndInfer + | PSingleRndParam event -> + BRndEvent (event ty_distr) + | PMultRndParams ((phi, d1, d2, d3, d4), event) -> + BRndSplit { brs_phi = phi; brs_d1 = d1; brs_d2 = d2; + brs_d3 = d3; brs_d4 = d4; brs_event = event ty_distr; } + | PTwoRndParams _ -> + tc_error !!tc "invalid arguments" in + let sg = + try bdhoare_rnd_subgoals (FApi.tc1_hyps tc) bhs n + with + | CannotInferEvent -> + tc_error !!tc "cannot infer a valid event, it must be provided" + | BoundWrittenByPrefix -> + tc_error !!tc + "The bounds on the probability of the sampling (third and \ + fifth arguments) cannot depend on variables written by the \ + statements preceding the sampling" in + FApi.xrule1 tc (RBdHoareRnd n) sg + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | RBdHoareRnd n -> + Some (EcPlRecheck.checker_of "bdhoare-rnd" pf_as_bdhoareS + (fun hyps bhs -> bdhoare_rnd_subgoals hyps bhs n)) + | _ -> None) + +(* -------------------------------------------------------------------- *) +(* Derived (no proof-node): the rule, then an attempt to close its + non-negativity premise [forall &m, 0%r <= d], when it has one (the [<=] + forms reducing the goal to a hoare judgement), with [t_trivial]. *) +let t_bdhoare_rnd_full (r : bdhoare_rnd_rule) (tc : tcenv1) = + let gs = t_bdhoare_rnd r tc in + let env = FApi.tc1_env tc in + let bhs = tc1_as_bdhoareS tc in + let (lv, _), _ = tc1_last_rnd tc bhs.bhs_s in + let nonneg = + bhs.bhs_cmp = FHle && + match r.brr_info with + | PNoRndParams -> not (bdhoare_rnd_post_indep env bhs lv) + | PSingleRndParam _ -> true + | _ -> false in + if nonneg then FApi.t_last (FApi.t_try t_trivial) gs else gs + +(* -------------------------------------------------------------------- *) +(* Elaboration: the goal is known to be a [bdHoareS]. [rnd] takes no side + and no position; the event ([ty -> bool]) and the bounds are typed in + the goal's memory, the event once the type [ty] of the sampled values is + known. *) +let process_bdhoare_rnd + (side : oside) (pos : psemrndpos option) (info : rnd_tac_info_f) tc += + if EcUtils.is_some side || EcUtils.is_some pos then + tc_error !!tc "invalid arguments"; + let info = + match info with + | PNoRndParams -> + PNoRndParams + + | PSingleRndParam fp -> + PSingleRndParam + (fun t -> snd (TTC.tc1_process_Xhl_form tc (tfun t tbool) fp)) + + | PMultRndParams ((phi, d1, d2, d3, d4), p) -> + let p t = p |> EcUtils.omap (fun p -> snd (TTC.tc1_process_Xhl_form tc (tfun t tbool) p)) in + let _, phi = TTC.tc1_process_Xhl_form tc tbool phi in + let _, d1 = TTC.tc1_process_Xhl_form tc treal d1 in + let _, d2 = TTC.tc1_process_Xhl_form tc treal d2 in + let _, d3 = TTC.tc1_process_Xhl_form tc treal d3 in + let _, d4 = TTC.tc1_process_Xhl_form tc treal d4 in + PMultRndParams ((phi, d1, d2, d3, d4), p) + + | _ -> tc_error !!tc "invalid arguments" + in + t_bdhoare_rnd_full { brr_info = info } tc diff --git a/src/phl/rules/bdhoare/ecBdHoareRnd.mli b/src/phl/rules/bdhoare/ecBdHoareRnd.mli new file mode 100644 index 000000000..a0d96e70e --- /dev/null +++ b/src/phl/rules/bdhoare/ecBdHoareRnd.mli @@ -0,0 +1,102 @@ +(* -------------------------------------------------------------------- *) +open EcParsetree +open EcCoreGoal.FApi +open EcAst + +(* ==================================================================== *) +(* Rules (trusted) *) + +type bdhoare_rnd_rule = { + brr_info : (ss_inv, ty -> ss_inv option, ty -> ss_inv) rnd_tac_info; + (* the event [E : ty -> bool] and the bounds, [ty] being the type of the + sampled values; [PTwoRndParams] is rejected *) +} + +(* [t_bdhoare_rnd { brr_info }] — sampling at the end of the statement. + + UNLIKE the hoare, ehoare and equiv [rnd] rules, this rule is stated over + [c; x <$ d], keeping the prefix [c] (an implicit [seq]): its premises are + judgements on [c] (a hoare one, for the [<=] forms), which the bdhoare + [seq] rule ([EcBdHoareSeq.t_bdhoare_seq]: invariant, event, four bounds, + bound arithmetic and non-modification premises) cannot reproduce. Some + forms also rely on [c] not writing the bound [d] (an implicit frame, see + [d0] below). + + Below, [~] is the goal's comparison, [d] its bound, [ty] the type of the + sampled values, [Q_v := Q[x := v]], and [C(E)] the event condition + <= : forall v, E v => v \in d => Q_v + >= : forall v, Q_v => v \in d => E v + = : forall v, v \in d => (E v <=> Q_v) + The rule binds [d0] as [d] itself when [c] does not write the variables + of [d], and otherwise as a fresh real [bd], with [P0 := P /\ d = bd] and + [forall bd] in front of the premise ([P0 := P] in the first case). When + no event is given, it is inferred: [E := predT] when [Q] does not + mention [x], [E := fun v => Q_v] when [x] is a variable, and the rule + fails otherwise. + + (1) no event, [<=], [x] not in [Q]: + + phoare [c : P ==> Q] <= d + ------------------------------ + phoare [c; x <$ d : P ==> Q] <= d + + (2) [<=], event [E] (given, or inferred and [x] in [Q]): + + hoare [c : P0 ==> mu d E <= d0 /\ C(E)] forall &m, 0%r <= d + ---------------------------------------------------------------- + phoare [c; x <$ d : P ==> Q] <= d + + (3) no event, [=] or [>=], [x] not in [Q]: + + phoare [c : P ==> Q /\ mu d predT = 1%r] ~ d + -------------------------------------------- + phoare [c; x <$ d : P ==> Q] ~ d + + (4) [=] or [>=], event [E] (given, or inferred and [x] in [Q]): + + phoare [c : P0 ==> mu d E ~ d0 /\ C(E)] ~' 1%r + ---------------------------------------------- + phoare [c; x <$ d : P ==> Q] ~ d + + where [~'] is [~] for an inferred event, and [=] for a given one. + + (5) [phi d1 d2 d3 d4 [E]] (event inferred, [x] a variable, when absent; + [E := fun v => Q_v] — no [predT] simplification): + + forall &m, d1 * d2 + d3 * d4 ~ d + phoare [c : P ==> phi] ~ d1 + forall &m, phi => mu d E ~ d2 /\ C(E) + phoare [c : P ==> !phi] ~ d3 + forall &m, !phi => mu d E ~ d4 /\ C(E) + forall &m, 0 <= d1 <= 1 /\ 0 <= d2 <= 1 /\ 0 <= d3 <= 1 /\ 0 <= d4 <= 1 + ------------------------------------------------------------------------ + phoare [c; x <$ d : P ==> Q] ~ d + + Premises are produced in the order displayed. Side conditions: the last + instruction is a sampling, an event can be inferred when needed, and, + for (5), [d2] and [d4] do not depend on variables written by [c] (they + are read both after [c] and in the initial memory). + + Node: [RBdHoareRnd n], with [n] the event / bounds instantiated at [ty]: + [BRndInfer], [BRndEvent E] or [BRndSplit { brs_phi; brs_d1; ...; + brs_event }]. Checker: "bdhoare-rnd"; it recomputes the written + variables of [c] and the inferred event from the goal's context. *) +val t_bdhoare_rnd : bdhoare_rnd_rule -> backward + +(* ==================================================================== *) +(* Derived tactics *) + +(* [t_bdhoare_rnd_full r] — [t_bdhoare_rnd r], then, for forms (2), an + attempt to close the premise [forall &m, 0%r <= d] with [t_trivial] + (left open when it fails). Emits no node of its own. *) +val t_bdhoare_rnd_full : bdhoare_rnd_rule -> backward + +(* ==================================================================== *) +(* Elaboration *) + +(* [rnd], [rnd E] or [rnd phi d1 d2 d3 d4 [E]] on a [bdHoareS] goal: no + side, no position. The event [E] is typed as a [ty -> bool] function, + [phi] as a formula, the bounds as reals, all in the goal's memory. + Applies [t_bdhoare_rnd_full]. *) +val process_bdhoare_rnd : + oside -> psemrndpos option -> rnd_tac_info_f -> backward diff --git a/src/phl/rules/bdhoare/ecBdHoareRndSem.ml b/src/phl/rules/bdhoare/ecBdHoareRndSem.ml new file mode 100644 index 000000000..e585fcd96 --- /dev/null +++ b/src/phl/rules/bdhoare/ecBdHoareRndSem.ml @@ -0,0 +1,74 @@ +(* -------------------------------------------------------------------- *) +open EcUtils +open EcParsetree +open EcFol +open EcAst +open EcEnv + +open EcCoreGoal +open EcLowPhlGoal + +(* -------------------------------------------------------------------- *) +(* Parameters of the bdhoare [rndsem] rule as supplied by the caller: high + level, the position is still a symbolic code gap that must be resolved. *) +type bdhoare_rndsem_rule = { + brsr_at : EcMatching.Position.codegap1; (* start of the suffix *) + brsr_reduce : bool; (* sample only the variables of Q *) +} + +(* Low-level parameters recorded in the proof-node: the position is the + RESOLVED integer index. *) +type bdhoare_rndsem_node = { + brsn_at : EcMatching.Position.nm_codegap1; (* resolved index *) + brsn_reduce : bool; +} + +type EcCoreGoal.rule += RBdHoareRndSem of bdhoare_rndsem_node + +(* -------------------------------------------------------------------- *) +(* Pure core shared by the rule and its checker: replace the suffix by its + semantic sampling. Its side condition (a straight-line suffix writing no + global) is part of it, so the checker re-validates it. *) +let bdhoare_rndsem_subgoals + (hyps : LDecl.hyps) (bhs : bdHoareS) (n : bdhoare_rndsem_node) += + let env = LDecl.toenv hyps in + let s1, s2 = EcMatching.Position.split_at_nmcgap1 n.brsn_at bhs.bhs_s in + let fv = + if n.brsn_reduce + then Some (EcPV.PV.fv env (fst bhs.bhs_m) (bhs_po bhs).inv) + else None in + let (_, mt), s2 = EcPlRndSem.semrnd env bhs.bhs_m fv s2 in + [f_bdHoareS mt (bhs_pr bhs) (stmt (s1 @ s2)) (bhs_po bhs) bhs.bhs_cmp (bhs_bd bhs)] + +(* -------------------------------------------------------------------- *) +(* Rule (TCB): resolve the code gap to an index, record the resolved node, + and build its subgoal through the shared core. *) +let t_bdhoare_rndsem (r : bdhoare_rndsem_rule) (tc : tcenv1) = + let env = FApi.tc1_env tc in + let bhs = tc1_as_bdhoareS tc in + let n = { brsn_at = s_split_index env r.brsr_at bhs.bhs_s; + brsn_reduce = r.brsr_reduce; } in + let sg = + try bdhoare_rndsem_subgoals (FApi.tc1_hyps tc) bhs n + with EcPlRndSem.InvalidSemRnd -> tc_error !!tc "semrnd" in + FApi.xrule1 tc (RBdHoareRndSem n) sg + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | RBdHoareRndSem n -> + Some (EcPlRecheck.checker_of "bdhoare-rndsem" pf_as_bdhoareS + (fun hyps bhs -> bdhoare_rndsem_subgoals hyps bhs n)) + | _ -> None) + +(* -------------------------------------------------------------------- *) +(* Elaboration: the goal is known to be a [bdHoareS]. The position is typed + first (with the side, which then makes a sided call fail there), then the + rule is applied. *) +let process_bdhoare_rndsem ~reduce (side : oside) pos (tc : tcenv1) = + let pos = tc1_process_codegap1 tc (side, pos) in + if is_some side then + tc_error !!tc "invalid arguments"; + t_bdhoare_rndsem { brsr_at = pos; brsr_reduce = reduce } tc diff --git a/src/phl/rules/bdhoare/ecBdHoareRndSem.mli b/src/phl/rules/bdhoare/ecBdHoareRndSem.mli new file mode 100644 index 000000000..04de03370 --- /dev/null +++ b/src/phl/rules/bdhoare/ecBdHoareRndSem.mli @@ -0,0 +1,39 @@ +(* -------------------------------------------------------------------- *) +open EcParsetree +open EcCoreGoal.FApi +open EcMatching.Position + +(* ==================================================================== *) +(* Rules (trusted) *) + +type bdhoare_rndsem_rule = { + brsr_at : codegap1; (* start k of the suffix *) + brsr_reduce : bool; (* sample only the variables of the post *) +} + +(* [t_bdhoare_rndsem { brsr_at = k; brsr_reduce = red }] — semantic + sampling of a straight-line suffix, with [~] the goal's comparison: + + phoare [c1; wr <$ D(c2) : P ==> Q] ~ d + ------------------------------------------ c = c1; c2 (c1 = c[0..k)) + phoare [c : P ==> Q] ~ d + + where [c2] consists of assignments and samplings only and writes no + global, [wr] are the variables written by [c2] — only those occurring + in [Q] when [red] — and [D(c2)] is the distribution of their final + values (see [EcPlRndSem.semrnd]). When [wr] is empty, a fresh [unit] + variable is added to the memory and sampled instead. + + As for hoare, the suffix is rewritten in place, keeping the prefix + [c1]: a program transformation, not expressible through [seq]. + + Node: [RBdHoareRndSem { brsn_at = k (resolved index); brsn_reduce = red }]. + Checker: "bdhoare-rndsem". *) +val t_bdhoare_rndsem : bdhoare_rndsem_rule -> backward + +(* ==================================================================== *) +(* Elaboration *) + +(* [rndsem[*] k] on a [bdHoareS] goal (the star sets [reduce]): no side. + Applies [t_bdhoare_rndsem]. *) +val process_bdhoare_rndsem : reduce:bool -> oside -> pcodegap1 -> backward diff --git a/src/phl/rules/ecPlRndSem.ml b/src/phl/rules/ecPlRndSem.ml new file mode 100644 index 000000000..e1168a4b3 --- /dev/null +++ b/src/phl/rules/ecPlRndSem.ml @@ -0,0 +1,118 @@ +(* -------------------------------------------------------------------- *) +open EcUtils +open EcAst +open EcTypes +open EcModules +open EcFol +open EcPV + +(* -------------------------------------------------------------------- *) +(* Semantic sampling of a straight-line statement, shared by the [rndsem] + rules of every logic: [s] (assignments and samplings only, no global + write) is read as the single sampling [wr <$ D(s)] of the variables it + writes, [D(s)] being [s] as nested [dlet] / [dunit]. *) +exception InvalidSemRnd + +let semrnd env (mem : memenv) (used : PV.t option) (s : instr list) = + let wr, gwr = PV.elements (is_write env s) in + let wr = + match used with + | None -> wr + | Some used -> List.filter (fun (pv, _) -> PV.mem_pv env pv used) wr in + + if not (List.is_empty gwr) then + raise InvalidSemRnd; + + (* The written variables, in order of first write. *) + let wr = + let add (m, idx) pv = + if is_some (PVMap.find pv m) + then (m, idx) + else (PVMap.add pv idx m, idx+1) in + + let m, idx = + List.fold_left (fun (m, idx) { i_node = i } -> + match i with + | Sasgn (lv, _) | Srnd (lv, _) -> + List.fold_left add (m, idx) (lv_to_list lv) + | _ -> (m, idx) + ) + (PVMap.create env, 0) s in + + let m, _ = + List.fold_left + (fun (m, idx) (pv, _) -> add (m, idx) pv) + (m, idx) + wr in + + List.sort + (fun (pv1, _) (pv2, _) -> + compare (PVMap.find pv1 m) (PVMap.find pv2 m)) + wr in + + let rec do1 (m: memory) (subst : PVM.subst) (s : instr list) = + match s with + | [] -> + let tuple = + List.map (fun (pv, _) -> + PVM.find env pv m subst) wr in + {m;inv=f_dunit (f_tuple tuple)} + + | { i_node = Sasgn (lv, e) } :: s -> + let e = ss_inv_of_expr m e in + let e = map_ss_inv1 (PVM.subst env subst) e in + let subst = + match lv with + | LvVar (pv, _) -> + PVM.add env pv m e.inv subst + | LvTuple pvs -> + List.fold_lefti (fun subst i (pv, ty) -> + PVM.add env pv m (f_proj e.inv i ty) subst + ) subst pvs + in + do1 m subst s + + | { i_node = Srnd (lv, d) } :: s -> + let d = ss_inv_of_expr m d in + let d = map_ss_inv1 (PVM.subst env subst) d in + let x = EcIdent.create (name_of_lv lv) in + let subst, xty = + match lv with + | LvVar (pv, ty) -> + let x = f_local x ty in + (PVM.add env pv m x subst, ty) + | LvTuple pvs -> + let ty = ttuple (List.snd pvs) in + let x = f_local x ty in + let subst = + List.fold_lefti (fun subst i (pv, ty) -> + PVM.add env pv m (f_proj x i ty) subst + ) subst pvs in + (subst, ty) + in + let body = do1 m subst s in + + map_ss_inv2 + (f_dlet_simpl + xty + (ttuple (List.snd wr))) + d + (map_ss_inv1 (f_lambda [(x, GTty xty)]) body) + + | _ :: _ -> + raise InvalidSemRnd + + in + + let mhr = EcIdent.create "&hr" in + let distr = do1 mhr PVM.empty s in + let distr = expr_of_ss_inv distr in + + match lv_of_list wr with + | None -> + let x = { ov_name = Some "x"; ov_type = tunit; } in + let mem, x = EcMemory.bind_fresh x mem in + let x, xty = pv_loc (oget x.ov_name), x.ov_type in + (mem, [i_rnd (LvVar (x, xty), distr)]) + | Some wr -> + (mem, [i_rnd (wr, distr)]) diff --git a/src/phl/rules/ecPlRndSem.mli b/src/phl/rules/ecPlRndSem.mli new file mode 100644 index 000000000..e560c0de9 --- /dev/null +++ b/src/phl/rules/ecPlRndSem.mli @@ -0,0 +1,24 @@ +(* -------------------------------------------------------------------- *) +open EcAst +open EcEnv + +(* -------------------------------------------------------------------- *) +(* Semantic sampling of a straight-line statement, shared by the [rndsem] + rules of every logic. + + [semrnd env me used s] — [s] must consist of assignments and samplings + only, and write no global. Returns the single sampling + + wr <$ D(s) + + where [wr] are the program variables written by [s] (only those in [used], + when given), in order of first write, and [D(s)] is the distribution of + their final values: [s] read as nested [dlet] / [dunit]. When [wr] is + empty, a fresh [unit] variable is bound in [me] and sampled instead; the + (possibly extended) memory is returned with the instruction. + + Raises [InvalidSemRnd] when [s] is not of the expected form. *) +exception InvalidSemRnd + +val semrnd : + env -> memenv -> EcPV.PV.t option -> instr list -> memenv * instr list diff --git a/src/phl/rules/ehoare/ecEHoareRnd.ml b/src/phl/rules/ehoare/ecEHoareRnd.ml new file mode 100644 index 000000000..9cddea96e --- /dev/null +++ b/src/phl/rules/ehoare/ecEHoareRnd.ml @@ -0,0 +1,86 @@ +(* -------------------------------------------------------------------- *) +open EcParsetree +open EcTypes +open EcModules +open EcFol +open EcAst +open EcEnv + +open EcCoreGoal +open EcLowGoal +open EcLowPhlGoal + +(* -------------------------------------------------------------------- *) +(* The ehoare [rnd] rule has no parameters: it is an axiom on a single + sampling, whose precondition is determined by the postcondition. *) +type EcCoreGoal.rule += REHoareRnd + +(* -------------------------------------------------------------------- *) +(* Weakest pre-expectation of [x <$ d] for the postcondition [post]: + Ep d (fun v => post[x := v]) *) +let ehoare_rnd_wp env ((lv, d) : lvalue * expr) (post : ss_inv) : ss_inv = + let m = post.m in + let ty = proj_distr_ty env (e_ty d) in + let x_id = EcIdent.create (symbol_of_lv lv) in + let x = f_local x_id ty in + let d = ss_inv_of_expr m d in + let post = subst_form_lv env lv { m; inv = x } post in + map_ss_inv2 (f_Ep ty) d (map_ss_inv1 (f_lambda [(x_id, GTty ty)]) post) + +(* -------------------------------------------------------------------- *) +(* Pure core shared by the rule and its checker. Its side conditions (the + statement is a single sampling, the precondition is its weakest + pre-expectation) are part of it, so the checker re-validates them. *) +let ehoare_rnd_subgoals (hyps : LDecl.hyps) (hs : eHoareS) : form list = + let env = LDecl.toenv hyps in + let rnd = + match hs.ehs_s.s_node with + | [{ i_node = Srnd (lv, d) }] -> (lv, d) + | _ -> failwith "ehoare-rnd: the statement is not a single sampling" in + let wp = ehoare_rnd_wp env rnd (ehs_po hs) in + if not (EcReduction.ss_inv_alpha_eq hyps wp (ehs_pr hs)) then + failwith "ehoare-rnd: the precondition is not the expected one"; + [] + +(* -------------------------------------------------------------------- *) +(* Rule (TCB). *) +let t_ehoare_rnd (tc : tcenv1) = + let hs = tc1_as_ehoareS tc in + let sg = + try ehoare_rnd_subgoals (FApi.tc1_hyps tc) hs + with Failure msg -> tc_error !!tc "%s" msg in + FApi.xrule1 tc REHoareRnd sg + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | REHoareRnd -> + Some (EcPlRecheck.checker_of "ehoare-rnd" pf_as_ehoareS + (fun hyps hs -> ehoare_rnd_subgoals hyps hs)) + | _ -> None) + +(* -------------------------------------------------------------------- *) +(* Derived (no proof-node): on [c; x <$ d], [seq] before the sampling with + its weakest pre-expectation as intermediate expectation, then close the + sampling with the rule. *) +let t_ehoare_rnd_last (tc : tcenv1) = + let env = FApi.tc1_env tc in + let hs = tc1_as_ehoareS tc in + let rnd, _ = tc1_last_rnd tc hs.ehs_s in + let mid = ehoare_rnd_wp env rnd (ehs_po hs) in + let at = EcMatching.Position.gap_before_last_n 1 in + FApi.t_seqsub + (EcEHoareSeq.t_ehoare_seq { ehsr_at = at; ehsr_mid = mid }) + [t_id; t_ehoare_rnd] + tc + +(* -------------------------------------------------------------------- *) +(* Elaboration: the goal is known to be an [eHoareS]. [rnd] takes no side, + no position and no argument. *) +let process_ehoare_rnd + (side : oside) (pos : psemrndpos option) (info : rnd_tac_info_f) tc += + match side, pos, info with + | None, None, PNoRndParams -> t_ehoare_rnd_last tc + | _ -> tc_error !!tc "invalid arguments" diff --git a/src/phl/rules/ehoare/ecEHoareRnd.mli b/src/phl/rules/ehoare/ecEHoareRnd.mli new file mode 100644 index 000000000..e59abeb1e --- /dev/null +++ b/src/phl/rules/ehoare/ecEHoareRnd.mli @@ -0,0 +1,40 @@ +(* -------------------------------------------------------------------- *) +open EcParsetree +open EcCoreGoal.FApi + +(* ==================================================================== *) +(* Rules (trusted) *) + +(* [t_ehoare_rnd] — single sampling: + + ------------------------------------------------ + ehoare [x <$ d : Ep d (fun v => Q[x := v]) ==> Q] + + Side conditions: the statement is the single sampling [x <$ d], and the + precondition is, up to alpha-conversion, the one displayed (otherwise + fails). + + Node: [REHoareRnd]. Checker: "ehoare-rnd". *) +val t_ehoare_rnd : backward + +(* ==================================================================== *) +(* Derived tactics *) + +(* [t_ehoare_rnd_last] — on [ehoare [c; x <$ d : P ==> Q]], with + R := Ep d (fun v => Q[x := v]): + 1. [EcEHoareSeq.t_ehoare_seq] before the sampling, with intermediate + expectation [R], giving + (a) ehoare [c : P ==> R] — left open, + (b) ehoare [x <$ d : R ==> Q]; + 2. [t_ehoare_rnd] closes (b). + Visible goal: (a). Fails if the last instruction is not a sampling. + Emits no node of its own. *) +val t_ehoare_rnd_last : backward + +(* ==================================================================== *) +(* Elaboration *) + +(* [rnd] on an [eHoareS] goal: no side, no position, no argument. Applies + [t_ehoare_rnd_last]. *) +val process_ehoare_rnd : + oside -> psemrndpos option -> rnd_tac_info_f -> backward diff --git a/src/phl/rules/equiv/ecEquivRnd.ml b/src/phl/rules/equiv/ecEquivRnd.ml new file mode 100644 index 000000000..a55031412 --- /dev/null +++ b/src/phl/rules/equiv/ecEquivRnd.ml @@ -0,0 +1,434 @@ +(* -------------------------------------------------------------------- *) +open EcUtils +open EcParsetree +open EcTypes +open EcModules +open EcFol +open EcAst +open EcEnv +open EcSubst + +open EcMatching.Position +open EcCoreGoal +open EcLowGoal +open EcLowPhlGoal + +module TTC = EcProofTyping + +(* -------------------------------------------------------------------- *) +type mkbij_t = ty -> ty -> ts_inv +type semrndpos = (bool * codegap1) doption + +(* Parameters of the two-sided equiv [rnd] rule: the bijection [f] between + the sampled values and its inverse, instantiated at their types. Already + typed, nothing to resolve: the same record is the rule argument and the + node payload. *) +type equiv_rnd = { + ern_f : ts_inv; (* f : tyL -> tyR *) + ern_finv : ts_inv; (* finv : tyR -> tyL *) +} + +(* Parameters of the one-sided equiv [rnd] rule: the side of the sampling. *) +type equiv_rnd_onesided = { + eros_side : side; +} + +type EcCoreGoal.rule += + | REquivRnd of equiv_rnd + | REquivRndOneSided of equiv_rnd_onesided + +(* -------------------------------------------------------------------- *) +(* Weakest precondition of [xL <$ dL ~ xR <$ dR] for the relation [post], + along the bijection [f] / [finv]: + (forall xR, xR \in dR => xR = f (finv xR)) + /\ (forall xR, xR \in dR => mu1 dR xR = mu1 dL (finv xR)) + /\ (forall xL, xL \in dL => + f xL \in dR /\ xL = finv (f xL) /\ post[xL<1> := xL, xR<2> := f xL]) *) +let equiv_rnd_wp env ((lvL, muL), (lvR, muR)) (n : equiv_rnd) (post : ts_inv) = + let ml, mr = post.ml, post.mr in + let tyL = proj_distr_ty env (e_ty muL) in + let tyR = proj_distr_ty env (e_ty muR) in + let xL_id = EcIdent.create (symbol_of_lv lvL ^ "L") + and xR_id = EcIdent.create (symbol_of_lv lvR ^ "R") in + let xL = {ml;mr;inv=f_local xL_id tyL} in + let xR = {ml;mr;inv=f_local xR_id tyR} in + let muL = EcFol.ss_inv_of_expr ml muL in + let muR = EcFol.ss_inv_of_expr mr muR in + + let f_app_simpl' ty f t = f_app_simpl f [t] ty in + let f t = map_ts_inv2 (f_app_simpl' tyR) n.ern_f t in + let finv t = map_ts_inv2 (f_app_simpl' tyL) n.ern_finv t in + + let post = subst_form_lv_left env lvL xL post in + let post = subst_form_lv_right env lvR (f xL) post in + + let muL = ss_inv_generalize_right muL mr in + let muR = ss_inv_generalize_left muR ml in + + let cond_fbij = map_ts_inv2 f_eq xL (finv (f xL)) in + let cond_fbij_inv = map_ts_inv2 f_eq xR (f (finv xR)) in + + let cond1 = map_ts_inv2 f_imp (map_ts_inv2 f_in_supp xR muR) cond_fbij_inv in + let cond2 = map_ts_inv2 f_imp (map_ts_inv2 f_in_supp xR muR) (map_ts_inv2 f_eq (map_ts_inv2 f_mu_x muR xR) (map_ts_inv2 f_mu_x muL (finv xR))) in + let cond3 = map_ts_inv f_andas [map_ts_inv2 f_in_supp (f xL) muR; cond_fbij; post] in + let cond3 = map_ts_inv2 f_imp (map_ts_inv2 f_in_supp xL muL) cond3 in + + map_ts_inv f_andas + [map_ts_inv1 (f_forall_simpl [(xR_id, GTty tyR)]) cond1; + map_ts_inv1 (f_forall_simpl [(xR_id, GTty tyR)]) cond2; + map_ts_inv1 (f_forall_simpl [(xL_id, GTty tyL)]) cond3] + +(* Weakest precondition of [x <$ d ~ skip] (for [`Left]; symmetrically for + [`Right]) for the relation [post]: + is_lossless d /\ forall v, v \in d => post[x<1> := v] *) +let equiv_rnd_onesided_wp env side ((lv, distr) : lvalue * expr) (post : ts_inv) = + let ml, mr = post.ml, post.mr in + let m, mo = sideif side (ml, mr) (mr, ml) in + let subst_form_lv_side = sideif side subst_form_lv_left subst_form_lv_right in + let ss_inv_generalize_other = + sideif side ss_inv_generalize_right ss_inv_generalize_left in + let ty_distr = proj_distr_ty env (e_ty distr) in + + let x_id = EcIdent.create (symbol_of_lv lv) in + let x = {ml; mr; inv=f_local x_id ty_distr} in + + let distr = EcFol.ss_inv_of_expr m distr in + let distr = ss_inv_generalize_other distr mo in + let post = subst_form_lv_side env lv x post in + let post = map_ts_inv2 f_imp (map_ts_inv2 f_in_supp x distr) post in + let post = map_ts_inv1 (f_forall_simpl [(x_id,GTty ty_distr)]) post in + map_ts_inv2 f_anda (map_ts_inv1 (f_lossless ty_distr) distr) post + +(* -------------------------------------------------------------------- *) +let single_rnd (who : string) (s : stmt) = + match s.s_node with + | [{ i_node = Srnd (lv, d) }] -> (lv, d) + | _ -> failwith (Printf.sprintf "%s: the statement is not a single sampling" who) + +(* Pure cores shared by the rules and their checkers. Their side conditions + (the statements are single samplings — resp. a single sampling and the + empty statement —, the bijection is well-typed, the precondition is the + weakest precondition) are part of them, so the checkers re-validate + them. *) +let equiv_rnd_subgoals (hyps : LDecl.hyps) (es : equivS) (n : equiv_rnd) = + let env = LDecl.toenv hyps in + let (_, muL) as rndL = single_rnd "equiv-rnd" es.es_sl in + let (_, muR) as rndR = single_rnd "equiv-rnd" es.es_sr in + let ml, mr = fst es.es_ml, fst es.es_mr in + let n = { ern_f = ts_inv_rebind n.ern_f ml mr; + ern_finv = ts_inv_rebind n.ern_finv ml mr; } in + let tyL = proj_distr_ty env (e_ty muL) in + let tyR = proj_distr_ty env (e_ty muR) in + if not (EcReduction.EqTest.for_type env n.ern_f.inv.f_ty (tfun tyL tyR)) || + not (EcReduction.EqTest.for_type env n.ern_finv.inv.f_ty (tfun tyR tyL)) then + failwith "equiv-rnd: the bijection is ill-typed"; + let wp = equiv_rnd_wp env (rndL, rndR) n (es_po es) in + if not (EcReduction.ts_inv_alpha_eq hyps wp (es_pr es)) then + failwith "equiv-rnd: the precondition is not the expected one"; + [] + +let equiv_rnd_onesided_subgoals + (hyps : LDecl.hyps) (es : equivS) (n : equiv_rnd_onesided) += + let env = LDecl.toenv hyps in + let s, so = sideif n.eros_side (es.es_sl, es.es_sr) (es.es_sr, es.es_sl) in + let rnd = single_rnd "equiv-rnd-onesided" s in + if not (List.is_empty so.s_node) then + failwith "equiv-rnd-onesided: the other statement is not empty"; + let wp = equiv_rnd_onesided_wp env n.eros_side rnd (es_po es) in + if not (EcReduction.ts_inv_alpha_eq hyps wp (es_pr es)) then + failwith "equiv-rnd-onesided: the precondition is not the expected one"; + [] + +(* -------------------------------------------------------------------- *) +(* Rules (TCB). *) +let t_equiv_rnd (n : equiv_rnd) (tc : tcenv1) = + let es = tc1_as_equivS tc in + let sg = + try equiv_rnd_subgoals (FApi.tc1_hyps tc) es n + with Failure msg -> tc_error !!tc "%s" msg in + FApi.xrule1 tc (REquivRnd n) sg + +let t_equiv_rnd_onesided (n : equiv_rnd_onesided) (tc : tcenv1) = + let es = tc1_as_equivS tc in + let sg = + try equiv_rnd_onesided_subgoals (FApi.tc1_hyps tc) es n + with Failure msg -> tc_error !!tc "%s" msg in + FApi.xrule1 tc (REquivRndOneSided n) sg + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | REquivRnd n -> + Some (EcPlRecheck.checker_of "equiv-rnd" pf_as_equivS + (fun hyps es -> equiv_rnd_subgoals hyps es n)) + | REquivRndOneSided n -> + Some (EcPlRecheck.checker_of "equiv-rnd-onesided" pf_as_equivS + (fun hyps es -> equiv_rnd_onesided_subgoals hyps es n)) + | _ -> None) + +(* -------------------------------------------------------------------- *) +(* Derived (no proof-node): [seq] before the final samplings, with their + weakest precondition as intermediate relation, then close the samplings + with the rules. *) +let t_equiv_rnd_seq bij (tc : tcenv1) = + let env = FApi.tc1_env tc in + let es = tc1_as_equivS tc in + let ml, mr = fst es.es_ml, fst es.es_mr in + let rndL, _ = tc1_last_rnd tc es.es_sl in + let rndR, _ = tc1_last_rnd tc es.es_sr in + let tyL = proj_distr_ty env (e_ty (snd rndL)) in + let tyR = proj_distr_ty env (e_ty (snd rndR)) in + let n = + match bij with + | Some (f, finv) -> { ern_f = f tyL tyR; ern_finv = finv tyR tyL; } + | None -> + if not (EcReduction.EqTest.for_type env tyL tyR) then + tc_error !!tc "%s, %s" + "support are not compatible" + "an explicit bijection is required"; + { ern_f = {ml;mr;inv=EcFol.f_identity ~name:"z" tyL}; + ern_finv = {ml;mr;inv=EcFol.f_identity ~name:"z" tyR}; } + in + let mid = equiv_rnd_wp env (rndL, rndR) n (es_po es) in + let at = gap_before_last_n 1 in + FApi.t_seqsub + (EcEquivSeq.t_equiv_seq { esr_at = (at, at); esr_mid = mid }) + [t_id; t_equiv_rnd n] + tc + +let t_equiv_rnd_onesided_seq side (tc : tcenv1) = + let env = FApi.tc1_env tc in + let es = tc1_as_equivS tc in + let rnd, _ = tc1_last_rnd tc (sideif side es.es_sl es.es_sr) in + let mid = equiv_rnd_onesided_wp env side rnd (es_po es) in + let at = sideif side + (gap_before_last_n 1, codegap1_end) + (codegap1_end, gap_before_last_n 1) in + FApi.t_seqsub + (EcEquivSeq.t_equiv_seq { esr_at = at; esr_mid = mid }) + [t_id; t_equiv_rnd_onesided { eros_side = side }] + tc + +(* -------------------------------------------------------------------- *) +(* Simplification of the remaining relation (derived): its side conditions + that [t_solve] proves on their own are turned into separate, closed + goals, and the relation is weakened accordingly with [conseq]. + + TEMPORARY: the consequence rule still comes from the not-yet-migrated + [EcPhlConseq]. *) +module E = struct exception Abort end + +let solve n f tc = + let tt = + FApi.t_seqs + [EcLowGoal.t_intros_n n; + EcLowGoal.t_solve ~bases:["random"] ~depth:2; + EcLowGoal.t_fail] in + + let subtc, hd = FApi.newgoal tc f in + + try + let subtc = + FApi.t_last + (fun tc1 -> + match FApi.t_try_base tt tc1 with + | `Failure _ -> raise E.Abort + | `Success tc -> tc) + subtc + in (subtc, Some hd) + + with E.Abort -> tc, None + +let t_apply_prept pt tc = + Apply.t_apply_bwd_r (EcProofTerm.pt_of_prept tc pt) tc + +(* -------------------------------------------------------------------- *) +let t_equiv_rnd_onesided_last side tc = + + let tc = t_equiv_rnd_onesided_seq side tc in + let es = tc1_as_equivS (FApi.as_tcenv1 tc) in + let (c1, c2) = map_ts_inv_destr2 destr_and (es_po es) in + let newc1 = EcSubst.f_forall_mems_ts_inv es.es_ml es.es_mr c1 in + + let subtc = tc in + let subtc, hdc1 = solve 2 newc1 subtc in + + match hdc1 with + | None -> tc + | Some hd -> + let po = c2 in + FApi.t_onalli (function + | 0 -> fun tc -> EcLowGoal.t_trivial tc + | 1 -> + let open EcProofTerm.Prept in + let m1 = EcIdent.create "_" in + let m2 = EcIdent.create "_" in + let h = EcIdent.create "_" in + let h1 = EcIdent.create "_" in + (t_intros_i [m1; m2; h] @! + (t_split @+ + [ t_apply_prept (hdl hd @ [amem m1; amem m2]); + t_intros_i [h1] @! t_apply_hyp h])) + + | _ -> EcLowGoal.t_id) + (FApi.t_first + (EcPhlConseq.t_equivS_conseq (es_pr es) po) + subtc) + +(* -------------------------------------------------------------------- *) +let t_equiv_rnd_last bij tc = + let tc = t_equiv_rnd_seq bij tc in + let es = tc1_as_equivS (FApi.as_tcenv1 tc) in + + let c1, c2, c3 = map_ts_inv_destr3 destr_and3 (es_po es) in + let (x, xty, _) = destr_forall1 c3.inv in + let c3 = map_ts_inv1 (fun c3 -> let (_,_,d) = destr_forall1 c3 in d) c3 in + let (ind, c3) = map_ts_inv_destr2 destr_imp c3 in + let (c3, c4) = map_ts_inv_destr2 destr_and c3 in + let newc2 = EcSubst.f_forall_mems_ts_inv es.es_ml es.es_mr c2 in + let newc3 = EcSubst.f_forall_mems_ts_inv es.es_ml es.es_mr + (map_ts_inv1 (f_forall [x, xty]) (map_ts_inv2 f_imp ind c3)) in + + let subtc = tc in + let subtc, hdc2 = solve 4 newc2 subtc in + let subtc, hdc3 = solve 4 newc3 subtc in + + let po = + match hdc2, hdc3 with + | None , None -> None + | Some _, Some _ -> + Some (map_ts_inv2 f_anda c1 (map_ts_inv1 (f_forall [x, xty]) (map_ts_inv2 f_imp ind c4))) + | Some _, None -> + Some (map_ts_inv2 f_anda c1 (map_ts_inv1 (f_forall [x, xty]) (map_ts_inv2 f_imp ind (map_ts_inv2 f_anda c3 c4)))) + | None , Some _ -> + Some (map_ts_inv f_andas [c1; c2; map_ts_inv1 (f_forall [x, xty]) (map_ts_inv2 f_imp ind c4)]) + in + + match po with None -> tc | Some po -> + + let m1 = EcIdent.create "_" in + let m2 = EcIdent.create "_" in + let h = EcIdent.create "_" in + let h1 = EcIdent.create "_" in + let h2 = EcIdent.create "_" in + let x = EcIdent.create "_" in + let hin = EcIdent.create "_" in + + FApi.t_onalli (function + | 0 -> fun tc -> EcLowGoal.t_trivial tc + | 1 -> + let open EcProofTerm.Prept in + + let t_c2 = + let pt = + match hdc2 with + | None -> hyp h2 + | Some hd -> hdl hd @ [amem m1; amem m2] in + t_apply_prept pt in + + let t_c3_c4 = + match hdc3 with + | None -> t_apply_prept (hyp h) + | Some hd -> + let fx = f_local x (gty_as_ty xty) in + t_intros_i [x; hin] @! t_split + @+ [ t_apply_prept (hdl hd @ [amem m1; amem m2; aform fx; ahyp hin]); + t_intros_n 1 @! + t_apply_prept ((hyp h) @ [aform fx; ahyp hin])] + in + + let t_case_c2 = + match hdc2 with + | None -> t_elim_and @! t_intros_i [h2; h] + | Some _ -> t_intros_i [h] in + + t_intros_i [m1; m2] @! t_elim_and @! t_intros_i [h1] @! t_case_c2 @! t_split @+ + [ t_apply_prept (hyp h1); + t_intros_n 1 @! t_split @+ + [ t_c2; + t_intros_n 1 @! t_c3_c4 + ] + ] + + | _ -> EcLowGoal.t_id) + + (FApi.t_first + (EcPhlConseq.t_equivS_conseq (es_pr es) po) + subtc) + +(* -------------------------------------------------------------------- *) +(* The surface two-sided / one-sided [rnd], optionally preceded by [rndsem] + on both sides (derived, no proof-node). *) +let t_equiv_rnd_full ?pos side bij_info tc = + match side, pos, bij_info with + | Some side, None, (None, None) -> + t_equiv_rnd_onesided_last side tc + | Some _side, None, _ -> + tc_error !!tc "one-sided rnd takes no arguments" + | None, _, _ -> begin + let pos = + match pos with + | None -> None + | Some (Single i) -> Some (i, i) + | Some (Double (il, ir)) -> Some (il, ir) in + + let tc = + match pos with + | None -> + t_id tc + | Some ((bl, il), (br, ir)) -> + let open EcEquivRndSem in + FApi.t_seq + (t_equiv_rndsem { ersr_side = `Left ; ersr_at = il; ersr_reduce = bl }) + (t_equiv_rndsem { ersr_side = `Right; ersr_at = ir; ersr_reduce = br }) + tc in + + let bij = + match bij_info with + | Some f, Some finv -> Some (f, finv) + | Some bij, None | None, Some bij -> Some (bij, bij) + | None, None -> None + in + FApi.t_first (t_equiv_rnd_last bij) tc + end + + | _ -> + tc_error !!tc "two-sided rnd requires a bijection" + +(* -------------------------------------------------------------------- *) +(* Elaboration: the goal is known to be an [equivS]. The bijection(s) are + typed in the goal's memories once the types of the sampled values are + known; the positions of [rndsem] (if any) in the memory of their side — + a single position without side in the bare environment (behaviour + preserved). *) +let process_equiv_rnd + (side : oside) (pos : psemrndpos option) (info : rnd_tac_info_f) tc += + let process_form f ty1 ty2 = + TTC.tc1_process_prhl_form tc (tfun ty1 ty2) f in + + let bij_info = + match info with + | PNoRndParams -> None, None + | PSingleRndParam f -> Some (process_form f), None + | PTwoRndParams (f, finv) -> Some (process_form f), Some (process_form finv) + | _ -> tc_error !!tc "invalid arguments" + in + + let pos = pos |> Option.map (function + | Single (b, p) -> + let p = + if Option.is_some side then + EcLowPhlGoal.tc1_process_codegap1 tc (side, p) + else EcTyping.trans_codegap1 (FApi.tc1_env tc) p + in Single (b, p) + | Double ((b1, p1), (b2, p2)) -> + let p1 = EcLowPhlGoal.tc1_process_codegap1 tc (Some `Left , p1) in + let p2 = EcLowPhlGoal.tc1_process_codegap1 tc (Some `Right, p2) in + Double ((b1, p1), (b2, p2)) + ) + in + + t_equiv_rnd_full side ?pos bij_info tc diff --git a/src/phl/rules/equiv/ecEquivRnd.mli b/src/phl/rules/equiv/ecEquivRnd.mli new file mode 100644 index 000000000..086233b80 --- /dev/null +++ b/src/phl/rules/equiv/ecEquivRnd.mli @@ -0,0 +1,110 @@ +(* -------------------------------------------------------------------- *) +open EcUtils +open EcParsetree +open EcCoreGoal.FApi +open EcMatching.Position +open EcAst + +(* -------------------------------------------------------------------- *) +type mkbij_t = ty -> ty -> ts_inv (* bijection, at given types *) +type semrndpos = (bool * codegap1) doption (* [rndsem] positions *) + +(* ==================================================================== *) +(* Rules (trusted) *) + +type equiv_rnd = { + ern_f : ts_inv; (* f : tyL -> tyR *) + ern_finv : ts_inv; (* finv : tyR -> tyL *) +} + +(* [t_equiv_rnd { ern_f = f; ern_finv = finv }] — two-sided sampling, + along a bijection: + + --------------------------------------------------------------------- + equiv [xL <$ dL ~ xR <$ dR : + (forall v, v \in dR => v = f (finv v)) + /\ (forall v, v \in dR => mu1 dR v = mu1 dL (finv v)) + /\ (forall v, v \in dL => + f v \in dR /\ v = finv (f v) /\ Q[xL<1> := v, xR<2> := f v]) + ==> Q] + + ([/\] is the asymmetric conjunction [&&].) Side conditions: both + statements are single samplings, [f : tyL -> tyR] and + [finv : tyR -> tyL] where [dL : tyL distr] and [dR : tyR distr], and the + precondition is, up to alpha-conversion, the one displayed (otherwise + fails). + + Node: [REquivRnd { ern_f = f; ern_finv = finv }]. Checker: "equiv-rnd". *) +val t_equiv_rnd : equiv_rnd -> backward + +type equiv_rnd_onesided = { + eros_side : side; (* side of the sampling *) +} + +(* [t_equiv_rnd_onesided { eros_side = `Left }] — one-sided sampling: + + ------------------------------------------------------------------------- + equiv [x <$ d ~ skip : is_lossless d /\ (forall v, v \in d => Q[x<1> := v]) ==> Q] + + (symmetrically for [`Right]; [/\] is [&&]). Side conditions: that side is + a single sampling, the other one is empty, and the precondition is, up to + alpha-conversion, the one displayed (otherwise fails). + + Node: [REquivRndOneSided { eros_side }]. Checker: "equiv-rnd-onesided". *) +val t_equiv_rnd_onesided : equiv_rnd_onesided -> backward + +(* ==================================================================== *) +(* Derived tactics *) + +(* [t_equiv_rnd_last bij] — on [equiv [c; xL <$ dL ~ c'; xR <$ dR : P ==> Q]], + with [f, finv] the bijection [bij] instantiated at the types [tyL], [tyR] + of the sampled values — the identity when [bij] is [None], which + requires [tyL = tyR] — and [R] the precondition of [t_equiv_rnd]: + 1. [EcEquivSeq.t_equiv_seq] before both samplings, with intermediate + relation [R], giving + (a) equiv [c ~ c' : P ==> R], + (b) equiv [xL <$ dL ~ xR <$ dR : R ==> Q]; + 2. [t_equiv_rnd] closes (b); + 3. on (a), the second conjunct of [R] (the [mu1] condition) and the + [f v \in dR /\ v = finv (f v)] part of the third one are each + dropped from the relation when [t_solve ~bases:["random"]] proves it + on its own (as a lemma over the memories), with + [EcPhlConseq.t_equivS_conseq] (whose side conditions are closed). + Visible goal: (a), with the relation simplified by step 3. *) +val t_equiv_rnd_last : (mkbij_t pair) option -> backward + +(* [t_equiv_rnd_onesided_last side] — on [equiv [c; x <$ d ~ c' : P ==> Q]] + (for [`Left]; symmetrically for [`Right]), with [R] the precondition of + [t_equiv_rnd_onesided]: + 1. [EcEquivSeq.t_equiv_seq] before the sampling on that side and at the + end of the other one, with intermediate relation [R], giving + (a) equiv [c ~ c' : P ==> R], + (b) equiv [x <$ d ~ skip : R ==> Q]; + 2. [t_equiv_rnd_onesided] closes (b); + 3. on (a), when [t_solve ~bases:["random"]] proves [is_lossless d] + (as a stand-alone lemma over the memories), it is dropped from the + relation with [EcPhlConseq.t_equivS_conseq] (side conditions closed). + Visible goal: (a), with the relation simplified by step 3. *) +val t_equiv_rnd_onesided_last : side -> backward + +(* [t_equiv_rnd_full ?pos side (f, finv)] — the surface [rnd] on equiv: + - one-sided ([side] given, no position, no bijection): + [t_equiv_rnd_onesided_last side]; + - two-sided (no side): [EcEquivRndSem.t_equiv_rndsem] on the left, then + on the right, at the positions [pos] (a single one is used on both + sides) when given, then [t_equiv_rnd_last] with the bijection [f] / + [finv] (either one standing for both when the other is absent). + Fails on any other combination. *) +val t_equiv_rnd_full : + ?pos:semrndpos -> oside -> (mkbij_t option) pair -> backward + +(* ==================================================================== *) +(* Elaboration *) + +(* [rnd{i}], [rnd [f [finv]]] and [rnd [f [finv]] : [*]k [[*]k'] ] on an + [equivS] goal. The bijections are typed as [tyL -> tyR] / [tyR -> tyL] + functions in the goal's memories; the positions in the memory of their + side (a single position with no side, in the bare environment). Applies + [t_equiv_rnd_full]. *) +val process_equiv_rnd : + oside -> psemrndpos option -> rnd_tac_info_f -> backward diff --git a/src/phl/rules/equiv/ecEquivRndSem.ml b/src/phl/rules/equiv/ecEquivRndSem.ml new file mode 100644 index 000000000..aae088d36 --- /dev/null +++ b/src/phl/rules/equiv/ecEquivRndSem.ml @@ -0,0 +1,85 @@ +(* -------------------------------------------------------------------- *) +open EcParsetree +open EcFol +open EcAst +open EcEnv + +open EcCoreGoal +open EcLowPhlGoal + +(* -------------------------------------------------------------------- *) +(* Parameters of the equiv [rndsem] rule as supplied by the caller: high + level, the position is still a symbolic code gap that must be resolved. *) +type equiv_rndsem_rule = { + ersr_side : side; (* rewritten side *) + ersr_at : EcMatching.Position.codegap1; (* start of the suffix *) + ersr_reduce : bool; (* sample only the variables of Q *) +} + +(* Low-level parameters recorded in the proof-node: the position is the + RESOLVED integer index. *) +type equiv_rndsem_node = { + ersn_side : side; + ersn_at : EcMatching.Position.nm_codegap1; (* resolved index *) + ersn_reduce : bool; +} + +type EcCoreGoal.rule += REquivRndSem of equiv_rndsem_node + +(* -------------------------------------------------------------------- *) +(* Pure core shared by the rule and its checker: replace the suffix of the + chosen side by its semantic sampling. Its side condition (a straight-line + suffix writing no global) is part of it, so the checker re-validates it. *) +let equiv_rndsem_subgoals + (hyps : LDecl.hyps) (es : equivS) (n : equiv_rndsem_node) += + let env = LDecl.toenv hyps in + let s, m = + match n.ersn_side with + | `Left -> es.es_sl, es.es_ml + | `Right -> es.es_sr, es.es_mr in + let s1, s2 = EcMatching.Position.split_at_nmcgap1 n.ersn_at s in + let fv = + if n.ersn_reduce + then Some (EcPV.PV.fv env (fst m) (es_po es).inv) + else None in + let (_, mt), s2 = EcPlRndSem.semrnd env m fv s2 in + let s = stmt (s1 @ s2) in + match n.ersn_side with + | `Left -> [f_equivS mt (snd es.es_mr) (es_pr es) s es.es_sr (es_po es)] + | `Right -> [f_equivS (snd es.es_ml) mt (es_pr es) es.es_sl s (es_po es)] + +(* -------------------------------------------------------------------- *) +(* Rule (TCB): resolve the code gap to an index, record the resolved node, + and build its subgoal through the shared core. *) +let t_equiv_rndsem (r : equiv_rndsem_rule) (tc : tcenv1) = + let env = FApi.tc1_env tc in + let es = tc1_as_equivS tc in + let s = sideif r.ersr_side es.es_sl es.es_sr in + let n = { ersn_side = r.ersr_side; + ersn_at = s_split_index env r.ersr_at s; + ersn_reduce = r.ersr_reduce; } in + let sg = + try equiv_rndsem_subgoals (FApi.tc1_hyps tc) es n + with EcPlRndSem.InvalidSemRnd -> tc_error !!tc "semrnd" in + FApi.xrule1 tc (REquivRndSem n) sg + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | REquivRndSem n -> + Some (EcPlRecheck.checker_of "equiv-rndsem" pf_as_equivS + (fun hyps es -> equiv_rndsem_subgoals hyps es n)) + | _ -> None) + +(* -------------------------------------------------------------------- *) +(* Elaboration: the goal is known to be an [equivS]. The position is typed + first, in the memory of the side (which then makes an unsided call fail + there), then the rule is applied. *) +let process_equiv_rndsem ~reduce (side : oside) pos (tc : tcenv1) = + let pos = tc1_process_codegap1 tc (side, pos) in + match side with + | None -> tc_error !!tc "invalid arguments" + | Some side -> + t_equiv_rndsem { ersr_side = side; ersr_at = pos; ersr_reduce = reduce } tc diff --git a/src/phl/rules/equiv/ecEquivRndSem.mli b/src/phl/rules/equiv/ecEquivRndSem.mli new file mode 100644 index 000000000..339425b33 --- /dev/null +++ b/src/phl/rules/equiv/ecEquivRndSem.mli @@ -0,0 +1,42 @@ +(* -------------------------------------------------------------------- *) +open EcParsetree +open EcCoreGoal.FApi +open EcMatching.Position + +(* ==================================================================== *) +(* Rules (trusted) *) + +type equiv_rndsem_rule = { + ersr_side : side; (* rewritten side *) + ersr_at : codegap1; (* start k of the suffix, on that side *) + ersr_reduce : bool; (* sample only the variables of the post *) +} + +(* [t_equiv_rndsem { ersr_side = `Left; ersr_at = k; ersr_reduce = red }] + — semantic sampling of a straight-line suffix of one side: + + equiv [c1; wr <$ D(c2) ~ c' : P ==> Q] + ------------------------------------------ c = c1; c2 (c1 = c[0..k)) + equiv [c ~ c' : P ==> Q] + + (symmetrically for [`Right]), where [c2] consists of assignments and + samplings only and writes no global, [wr] are the variables written by + [c2] — only those occurring in [Q] (on that side) when [red] — and + [D(c2)] is the distribution of their final values (see + [EcPlRndSem.semrnd]). When [wr] is empty, a fresh [unit] variable is + added to the memory of that side and sampled instead. + + As for hoare, the suffix is rewritten in place, keeping the prefix + [c1]: a program transformation, not expressible through [seq]. + + Node: [REquivRndSem { ersn_side; ersn_at = k (resolved index); + ersn_reduce = red }]. + Checker: "equiv-rndsem". *) +val t_equiv_rndsem : equiv_rndsem_rule -> backward + +(* ==================================================================== *) +(* Elaboration *) + +(* [rndsem[*]{i} k] on an [equivS] goal (the star sets [reduce]): side + required. Applies [t_equiv_rndsem]. *) +val process_equiv_rndsem : reduce:bool -> oside -> pcodegap1 -> backward diff --git a/src/phl/rules/hoare/ecHoareRnd.ml b/src/phl/rules/hoare/ecHoareRnd.ml new file mode 100644 index 000000000..56ebae385 --- /dev/null +++ b/src/phl/rules/hoare/ecHoareRnd.ml @@ -0,0 +1,89 @@ +(* -------------------------------------------------------------------- *) +open EcParsetree +open EcTypes +open EcModules +open EcFol +open EcAst +open EcEnv + +open EcCoreGoal +open EcLowGoal +open EcLowPhlGoal + +(* -------------------------------------------------------------------- *) +(* The hoare [rnd] rule has no parameters: it is an axiom on a single + sampling, whose precondition is determined by the postcondition. *) +type EcCoreGoal.rule += RHoareRnd + +(* -------------------------------------------------------------------- *) +(* Weakest precondition of [x <$ d] for the postcondition [post]: + forall v, v \in d => post[x := v] *) +let hoare_rnd_wp env ((lv, d) : lvalue * expr) (post : ss_inv) : ss_inv = + let m = post.m in + let ty = proj_distr_ty env (e_ty d) in + let x_id = EcIdent.create (symbol_of_lv lv) in + let x = { m; inv = f_local x_id ty } in + let d = ss_inv_of_expr m d in + let post = subst_form_lv env lv x post in + let post = map_ss_inv2 f_imp (map_ss_inv2 f_in_supp x d) post in + map_ss_inv1 (f_forall_simpl [(x_id, GTty ty)]) post + +(* -------------------------------------------------------------------- *) +(* Pure core shared by the rule and its checker. Its side conditions (the + statement is a single sampling, the precondition is its weakest + precondition) are part of it, so the checker re-validates them. *) +let hoare_rnd_subgoals (hyps : LDecl.hyps) (hs : sHoareS) : form list = + let env = LDecl.toenv hyps in + let rnd = + match hs.hs_s.s_node with + | [{ i_node = Srnd (lv, d) }] -> (lv, d) + | _ -> failwith "hoare-rnd: the statement is not a single sampling" in + let wp = hoare_rnd_wp env rnd (POE.lower (hs_po hs)) in + if not (EcReduction.ss_inv_alpha_eq hyps wp (hs_pr hs)) then + failwith "hoare-rnd: the precondition is not the expected one"; + [] + +(* -------------------------------------------------------------------- *) +(* Rule (TCB). *) +let t_hoare_rnd (tc : tcenv1) = + let hs = tc1_as_hoareS tc in + let sg = + try hoare_rnd_subgoals (FApi.tc1_hyps tc) hs + with Failure msg -> tc_error !!tc "%s" msg in + FApi.xrule1 tc RHoareRnd sg + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | RHoareRnd -> + Some (EcPlRecheck.checker_of "hoare-rnd" pf_as_hoareS + (fun hyps hs -> hoare_rnd_subgoals hyps hs)) + | _ -> None) + +(* -------------------------------------------------------------------- *) +(* Derived (no proof-node): on [c; x <$ d], [seq] before the sampling with + its weakest precondition as intermediate assertion, then close the + sampling with the rule. *) +let t_hoare_rnd_last (tc : tcenv1) = + let env = FApi.tc1_env tc in + let hs = tc1_as_hoareS tc in + let rnd, _ = tc1_last_rnd tc hs.hs_s in + if not (POE.is_empty (hs_po hs).hsi_inv) then + tc_error !!tc "exceptions are not supported"; + let mid = hoare_rnd_wp env rnd (POE.lower (hs_po hs)) in + let at = EcMatching.Position.gap_before_last_n 1 in + FApi.t_seqsub + (EcHoareSeq.t_hoare_seq { hsr_at = at; hsr_mid = mid }) + [t_id; t_hoare_rnd] + tc + +(* -------------------------------------------------------------------- *) +(* Elaboration: the goal is known to be a [hoareS]. [rnd] takes no side, no + position and no argument. *) +let process_hoare_rnd + (side : oside) (pos : psemrndpos option) (info : rnd_tac_info_f) tc += + match side, pos, info with + | None, None, PNoRndParams -> t_hoare_rnd_last tc + | _ -> tc_error !!tc "invalid arguments" diff --git a/src/phl/rules/hoare/ecHoareRnd.mli b/src/phl/rules/hoare/ecHoareRnd.mli new file mode 100644 index 000000000..8831961a9 --- /dev/null +++ b/src/phl/rules/hoare/ecHoareRnd.mli @@ -0,0 +1,41 @@ +(* -------------------------------------------------------------------- *) +open EcParsetree +open EcCoreGoal.FApi + +(* ==================================================================== *) +(* Rules (trusted) *) + +(* [t_hoare_rnd] — single sampling: + + ---------------------------------------------------------- + hoare [x <$ d : (forall v, v \in d => Q[x := v]) ==> Q | E] + + The exceptional postconditions [E] play no role: a sampling raises + nothing. Side conditions: the statement is the single sampling + [x <$ d], and the precondition is, up to alpha-conversion, the one + displayed (otherwise fails). + + Node: [RHoareRnd]. Checker: "hoare-rnd". *) +val t_hoare_rnd : backward + +(* ==================================================================== *) +(* Derived tactics *) + +(* [t_hoare_rnd_last] — on [hoare [c; x <$ d : P ==> Q]] (no exceptional + postcondition), with R := forall v, v \in d => Q[x := v]: + 1. [EcHoareSeq.t_hoare_seq] before the sampling, with intermediate + assertion [R], giving + (a) hoare [c : P ==> R] — left open, + (b) hoare [x <$ d : R ==> Q]; + 2. [t_hoare_rnd] closes (b). + Visible goal: (a). Fails if the last instruction is not a sampling, or + if the goal has exceptional postconditions. Emits no node of its own. *) +val t_hoare_rnd_last : backward + +(* ==================================================================== *) +(* Elaboration *) + +(* [rnd] on a [hoareS] goal: no side, no position, no argument. Applies + [t_hoare_rnd_last]. *) +val process_hoare_rnd : + oside -> psemrndpos option -> rnd_tac_info_f -> backward diff --git a/src/phl/rules/hoare/ecHoareRndSem.ml b/src/phl/rules/hoare/ecHoareRndSem.ml new file mode 100644 index 000000000..20b0f4379 --- /dev/null +++ b/src/phl/rules/hoare/ecHoareRndSem.ml @@ -0,0 +1,76 @@ +(* -------------------------------------------------------------------- *) +open EcUtils +open EcParsetree +open EcFol +open EcAst +open EcEnv + +open EcCoreGoal +open EcLowPhlGoal + +(* -------------------------------------------------------------------- *) +(* Parameters of the hoare [rndsem] rule as supplied by the caller: high + level, the position is still a symbolic code gap that must be resolved. *) +type hoare_rndsem_rule = { + hrsr_at : EcMatching.Position.codegap1; (* start of the suffix *) + hrsr_reduce : bool; (* sample only the variables of Q *) +} + +(* Low-level parameters recorded in the proof-node: the position is the + RESOLVED integer index. *) +type hoare_rndsem_node = { + hrsn_at : EcMatching.Position.nm_codegap1; (* resolved index *) + hrsn_reduce : bool; +} + +type EcCoreGoal.rule += RHoareRndSem of hoare_rndsem_node + +(* -------------------------------------------------------------------- *) +(* Pure core shared by the rule and its checker: replace the suffix by its + semantic sampling. Its side conditions (no exceptional postcondition, a + straight-line suffix writing no global) are part of it, so the checker + re-validates them. *) +let hoare_rndsem_subgoals (hyps : LDecl.hyps) (hs : sHoareS) (n : hoare_rndsem_node) = + let env = LDecl.toenv hyps in + if not (POE.is_empty (hs_po hs).hsi_inv) then + failwith "hoare-rndsem: exceptions are not supported"; + let s1, s2 = EcMatching.Position.split_at_nmcgap1 n.hrsn_at hs.hs_s in + let post = POE.lower (hs_po hs) in + let fv = + if n.hrsn_reduce then Some (EcPV.PV.fv env (fst hs.hs_m) post.inv) else None in + let (_, mt), s2 = EcPlRndSem.semrnd env hs.hs_m fv s2 in + [f_hoareS mt (hs_pr hs) (stmt (s1 @ s2)) (hs_po hs)] + +(* -------------------------------------------------------------------- *) +(* Rule (TCB): resolve the code gap to an index, record the resolved node, + and build its subgoal through the shared core. *) +let t_hoare_rndsem (r : hoare_rndsem_rule) (tc : tcenv1) = + let env = FApi.tc1_env tc in + let hs = tc1_as_hoareS tc in + let n = { hrsn_at = s_split_index env r.hrsr_at hs.hs_s; + hrsn_reduce = r.hrsr_reduce; } in + if not (POE.is_empty (hs_po hs).hsi_inv) then + tc_error !!tc "exceptions are not supported"; + let sg = + try hoare_rndsem_subgoals (FApi.tc1_hyps tc) hs n + with EcPlRndSem.InvalidSemRnd -> tc_error !!tc "semrnd" in + FApi.xrule1 tc (RHoareRndSem n) sg + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | RHoareRndSem n -> + Some (EcPlRecheck.checker_of "hoare-rndsem" pf_as_hoareS + (fun hyps hs -> hoare_rndsem_subgoals hyps hs n)) + | _ -> None) + +(* -------------------------------------------------------------------- *) +(* Elaboration: the goal is known to be a [hoareS]. The position is typed + first (with the side, which then makes a sided call fail there), then the + rule is applied. *) +let process_hoare_rndsem ~reduce (side : oside) pos (tc : tcenv1) = + let pos = tc1_process_codegap1 tc (side, pos) in + if is_some side then + tc_error !!tc "invalid arguments"; + t_hoare_rndsem { hrsr_at = pos; hrsr_reduce = reduce } tc diff --git a/src/phl/rules/hoare/ecHoareRndSem.mli b/src/phl/rules/hoare/ecHoareRndSem.mli new file mode 100644 index 000000000..cce727baf --- /dev/null +++ b/src/phl/rules/hoare/ecHoareRndSem.mli @@ -0,0 +1,42 @@ +(* -------------------------------------------------------------------- *) +open EcParsetree +open EcCoreGoal.FApi +open EcMatching.Position + +(* ==================================================================== *) +(* Rules (trusted) *) + +type hoare_rndsem_rule = { + hrsr_at : codegap1; (* start k of the suffix *) + hrsr_reduce : bool; (* sample only the variables of the post *) +} + +(* [t_hoare_rndsem { hrsr_at = k; hrsr_reduce = red }] — semantic sampling + of a straight-line suffix: + + hoare [c1; wr <$ D(c2) : P ==> Q] + ------------------------------------- c = c1; c2 (c1 = c[0..k)) + hoare [c : P ==> Q] + + where [c2] consists of assignments and samplings only and writes no + global, [wr] are the variables written by [c2] — only those occurring + in [Q] when [red] — and [D(c2)] is the distribution of their final + values, [c2] read as nested [dlet] / [dunit] (see [EcPlRndSem.semrnd]). + When [wr] is empty, a fresh [unit] variable is added to the memory and + sampled instead. Side condition: no exceptional postcondition. + + This rule rewrites the suffix [c2] in place, keeping the prefix [c1]: it + is a program transformation (replacing [c2] by an equivalent sampling), + which is not expressible through [seq] without an intermediate assertion + after [c1] that the tactic does not have. + + Node: [RHoareRndSem { hrsn_at = k (resolved index); hrsn_reduce = red }]. + Checker: "hoare-rndsem". *) +val t_hoare_rndsem : hoare_rndsem_rule -> backward + +(* ==================================================================== *) +(* Elaboration *) + +(* [rndsem[*] k] on a [hoareS] goal (the star sets [reduce]): no side. + Applies [t_hoare_rndsem]. *) +val process_hoare_rndsem : reduce:bool -> oside -> pcodegap1 -> backward diff --git a/tests/rnd.ec b/tests/rnd.ec new file mode 100644 index 000000000..3cba8162e --- /dev/null +++ b/tests/rnd.ec @@ -0,0 +1,392 @@ +(* The `rnd` and `rndsem` tactics, in every logic and form, with their + failing cases. Each `rnd` is a separate sentence, so that the goals it + leaves can be compared across builds. *) +require import AllCore Distr DBool Xreal. + +op d : int distr. +axiom d_ll : is_lossless d. + +exception e. + +module H = { + var g : int + + proc f() : int = { + var x, y : int; + y <- 1; + x <$ d; + return x + y; + } + + proc s() : int = { + var x : int; + x <$ d; + return x; + } + + proc b() : bool = { + var x : bool; + x <$ {0,1}; + return x; + } + + proc t() : int * int = { + var x, y : int; + (x, y) <$ d `*` d; + return (x, y); + } + + proc nr() : int = { + var x : int; + x <$ d; + x <- x + 1; + return x; + } + + proc w() : int = { + var x : int; + g <- 0; + x <$ d; + return x; + } + + proc sem() : int = { + var x, y : int; + y <- 1; + x <$ d; + x <- x + y; + return x; + } + + proc semg() : int = { + var x : int; + x <$ d; + g <- x; + return x; + } + + proc semc() : int = { + var x : int; + x <$ d; + if (x = 0) x <- 1; + return x; + } + + proc z() : int = { + return 0; + } + + proc pb() : unit = { + var x : bool; + g <- 1; + x <$ {0,1}; + } + + proc pbx() : bool = { + var x : bool; + g <- 1; + x <$ {0,1}; + return x; + } +}. + +(* -------------------------------------------------------------------- *) +(* hoare *) +lemma hoare_rnd : hoare [H.f : true ==> res - 1 \in d]. +proof. +proc. +rnd. +by wp; skip => /> v hv; smt(). +qed. + +lemma hoare_rnd_single : hoare [H.s : true ==> res \in d]. +proof. +proc. +rnd. +by skip => />. +qed. + +lemma hoare_rnd_errors : hoare [H.nr : true ==> true]. +proof. +proc. +fail rnd. (* the last instruction is not a sampling *) +fail rnd (fun _ => true). +fail rnd{1}. +abort. + +lemma hoare_rnd_exn : hoare [H.s : true ==> true | e => true]. +proof. +proc. +fail rnd. (* exceptions are not supported *) +abort. + +(* -------------------------------------------------------------------- *) +(* ehoare *) +lemma ehoare_rnd : ehoare [H.s : (Ep d (fun v => (v = 0)%xr)) ==> (res = 0)%xr]. +proof. +proc. +rnd. +by skip. +qed. + +lemma ehoare_rnd_errors : ehoare [H.nr : (1%xr) ==> (1%xr)]. +proof. +proc. +fail rnd. +fail rnd (fun _ => true). +abort. + +(* -------------------------------------------------------------------- *) +(* bdhoare *) + +(* (1) <=, no event, the post does not mention the sampled variable. *) +lemma bd_le_indep : phoare [H.pb : true ==> H.g = 2] <= 0%r. +proof. +proc. +rnd. +by hoare; wp; skip. +qed. + +(* (2) <=, inferred event; the non-negativity premise is closed. *) +lemma bd_le_infer : phoare [H.pbx : true ==> res] <= 1%r. +proof. +proc. +rnd. +by wp; skip => />; smt(le1_mu). +qed. + +(* (2) <=, given event; the non-negativity premise is left open. *) +lemma bd_le_event : phoare [H.pbx : true ==> res] <= (1%r/2%r). +proof. +proc. +rnd (pred1 true). ++ by wp; skip => />; smt(dbool1E). ++ by move=> &hr; smt(). +qed. + +(* (2) <=, a bound written by the prefix (generalized), whose + non-negativity premise is not closed. *) +lemma bd_le_dep : phoare [H.pbx : true ==> res] <= (H.g%r / 2%r). +proof. +proc. +rnd (pred1 true). +abort. + +(* (3) = and >=, no event, the post does not mention the sampled variable. *) +lemma bd_eq_indep : phoare [H.pb : true ==> H.g = 1] = 1%r. +proof. +proc. +rnd. +by wp; skip => />; apply dbool_ll. +qed. + +lemma bd_ge_indep : phoare [H.pb : true ==> H.g = 1] >= 1%r. +proof. +proc. +rnd. +by wp; skip => />; apply dbool_ll. +qed. + +(* (4) = and >=, inferred and given event. *) +lemma bd_eq_infer : phoare [H.pbx : true ==> res] = (1%r/2%r). +proof. +proc. +rnd. +by wp; skip => />; smt(dbool1E). +qed. + +lemma bd_ge_event : phoare [H.pbx : true ==> res] >= (1%r/2%r). +proof. +proc. +rnd (pred1 true). +by wp; skip => />; smt(dbool1E). +qed. + +(* (5) phi d1 d2 d3 d4, without and with event. *) +lemma bd_split : phoare [H.pbx : true ==> res] = (1%r/2%r). +proof. +proc. +rnd true 1%r (1%r/2%r) 0%r 1%r. +abort. + +lemma bd_split_event : phoare [H.pbx : true ==> res] <= (1%r/2%r). +proof. +proc. +rnd true 1%r (1%r/2%r) 0%r 1%r (pred1 true). +abort. + +(* A tuple sampling: the event cannot be inferred. *) +lemma bd_tuple : phoare [H.t : true ==> res.`1 = 0] <= 1%r. +proof. +proc. +fail rnd. +rnd (fun (p : int * int) => p.`1 = 0). +by skip => />; smt(le1_mu). +qed. + +lemma bd_errors : phoare [H.pbx : true ==> res] = (1%r/2%r). +proof. +proc. +fail rnd (pred1 true) (pred1 true). +fail rnd{1}. +fail rnd : 0. +abort. + +(* -------------------------------------------------------------------- *) +(* equiv, two-sided *) +lemma eq_rnd_id : equiv [H.b ~ H.b : true ==> ={res}]. +proof. +proc. +rnd. +by skip => />. +qed. + +lemma eq_rnd_prefix : equiv [H.f ~ H.f : true ==> ={res}]. +proof. +proc. +rnd. +by wp; skip => />. +qed. + +lemma eq_rnd_bij : equiv [H.b ~ H.b : true ==> res{1} = !res{2}]. +proof. +proc. +rnd (fun b => !b). +by skip => />. +qed. + +lemma eq_rnd_bij2 : equiv [H.b ~ H.b : true ==> res{1} = !res{2}]. +proof. +proc. +rnd (fun b => !b) (fun b => !b). +by skip => />. +qed. + +lemma eq_rnd_errors : equiv [H.b ~ H.s : true ==> true]. +proof. +proc. +fail rnd. (* incompatible supports *) +fail rnd{1} (fun b => b). +fail rnd{1} : 0. +abort. + +(* two-sided, after rndsem on both sides *) +lemma eq_rnd_pos : equiv [H.sem ~ H.sem : true ==> ={res}]. +proof. +proc. +rnd : 1 1. +by wp; skip => />. +qed. + +lemma eq_rnd_pos1 : equiv [H.sem ~ H.sem : true ==> ={res}]. +proof. +proc. +rnd : *1. +by wp; skip => />. +qed. + +(* equiv, one-sided *) +lemma eq_rnd_left : equiv [H.s ~ H.b : true ==> true]. +proof. +proc. +rnd{1}. +rnd{2}. +by skip => />; smt(d_ll). +qed. + +lemma eq_rnd_right : equiv [H.b ~ H.f : true ==> true]. +proof. +proc. +rnd{2}. +wp. +rnd{1}. +by skip => />; smt(d_ll). +qed. + +(* auto *) +lemma eq_auto : equiv [H.b ~ H.b : true ==> ={res}]. +proof. +proc. +by auto. +qed. + +lemma eq_auto_onesided : equiv [H.s ~ H.z : true ==> true]. +proof. +proc. +by auto => />; apply d_ll. +qed. + +lemma bd_auto : phoare [H.pbx : true ==> true] = 1%r. +proof. +proc. +by auto => />; apply dbool_ll. +qed. + +(* -------------------------------------------------------------------- *) +(* rndsem *) +lemma hoare_rndsem : hoare [H.sem : true ==> res - 1 \in d]. +proof. +proc. +rndsem 1. +rnd. +wp; skip => /> v. +by rewrite supp_dmap => -[x [? ->]] /#. +qed. + +lemma hoare_rndsem_red : hoare [H.sem : true ==> true]. +proof. +proc. +rndsem* 0. +rnd. +by skip. +qed. + +lemma bd_rndsem : phoare [H.sem : true ==> true] = 1%r. +proof. +proc. +rndsem 0. +rnd. +by skip => />; smt(dmap_ll d_ll). +qed. + +lemma eq_rndsem : equiv [H.sem ~ H.sem : true ==> ={res}]. +proof. +proc. +rndsem{1} 1. +rndsem*{2} 1. +rnd. +by wp; skip. +qed. + +lemma rndsem_global : hoare [H.semg : true ==> true]. +proof. +proc. +fail rndsem{1} 0. +rndsem 0. +rnd. +by skip. +qed. + +lemma rndsem_errors_if : hoare [H.semc : true ==> true]. +proof. +proc. +fail rndsem 0. (* not straight-line *) +abort. + +lemma rndsem_errors_exn : hoare [H.sem : true ==> true | e => true]. +proof. +proc. +fail rndsem 0. (* exceptions are not supported *) +abort. + +lemma rndsem_errors_eq : equiv [H.sem ~ H.sem : true ==> true]. +proof. +proc. +fail rndsem 0. +abort. + +lemma rndsem_errors_eh : ehoare [H.sem : (1%xr) ==> (1%xr)]. +proof. +proc. +fail rndsem 0. +abort.