diff --git a/src/phl/ecPhlSp.ml b/src/phl/ecPhlSp.ml index 3eae4f7c7..38545a70d 100644 --- a/src/phl/ecPhlSp.ml +++ b/src/phl/ecPhlSp.ml @@ -2,308 +2,55 @@ open EcUtils open EcParsetree open EcAst -open EcTypes -open EcModules -open EcFol -open EcEnv open EcCoreGoal open EcLowPhlGoal -(* - * SP carries four elements, - * - bds: a set of existential binders - * - assoc: a set of pairs (x,e) such that x=e holds - * for instance after an assignment x <- e - * - pre: the actual precondition (progressively weakened) - * - * After an assignment of the form x <- e the four elements are updated: - * 1) a new fresh local x' is added to the list of existential binders - * 2) (x, e) is added to the assoc list, and every other (y,d) is replaced - * by (y[x->x'], d[x->x']) - * 3) pre is replaced by pre[x->x'] - * - * The simplification of this version comes from two tricks: - * - * 1) the replacement of (y[x->x']) introduces a simplification - * opportunity. There is no need to keep (x', d[x->x']) as a - * conjuction x' = d[x->x']: it is enough to perform the substitution - * of d[x->x'] for x' in place (it is a mess however to implement this - * idea with simultaneous assigns) - * 2) $MISSING... - *) - (* -------------------------------------------------------------------- *) -module LowInternal = struct - (* ------------------------------------------------------------------ *) - exception No_sp - - (* ------------------------------------------------------------------ *) - type assignable = - | APVar of (prog_var * ty) - | ALocal of (EcIdent.t * ty) - - and assignables = assignable list - - (* ------------------------------------------------------------------ *) - let isAPVar = function APVar _ -> true | _ -> false - let isALocal = function ALocal _ -> true | _ -> false - - (* ------------------------------------------------------------------ *) - let sp_asgn ?mc (memenv : EcMemory.memenv) env lv e (bds, assoc, pre) = - let m = fst memenv in - let subst_in_assoc lv new_id_exp new_ids ((ass : assignables), f) = - let replace_assignable var = - match var with - | APVar (pv', ty) -> begin - match lv,new_ids with - | LvVar (pv ,_), [new_id,_] when NormMp.pv_equal env pv pv' -> - ALocal (new_id,ty) - - | LvVar _, _ -> - var - - | LvTuple vs, _ -> begin - let aux = List.map2 (fun x y -> (fst x, fst y)) vs new_ids in - try - let new_id = snd (List.find (NormMp.pv_equal env pv' -| fst) aux) in - ALocal (new_id, ty) - with Not_found -> var - end - end - | _ -> var - - in let ass = List.map replace_assignable ass in - let f = (subst_form_lv ?mc env lv {m;inv=new_id_exp} {m;inv=f}).inv in - (ass, f) - in - - let rec simplify_assoc (assoc, bds, pre) = - match assoc with - | [] -> - ([], bds, pre) - - | (ass, f) :: assoc -> - let assoc, bds, pre = simplify_assoc (assoc, bds, pre) in - - let destr_ass = - try List.combine (List.map in_seq1 ass) (destr_tuple f) - with Invalid_argument _ | DestrError _ -> [(ass, f)] - in - - let do_subst_or_accum (assoc, bds, pre) (a, f) = - match a with - | [ALocal (id, _)] -> - let subst = EcFol.Fsubst.f_subst_id in - let subst = EcFol.Fsubst.f_bind_local subst id f in - (List.map (snd_map (EcFol.Fsubst.f_subst subst)) assoc, - List.filter ((<>) id -| fst) bds, - EcFol.Fsubst.f_subst subst pre) - - | _ -> ((a, f) :: assoc, bds, pre) - in - List.fold_left do_subst_or_accum (assoc, bds, pre) destr_ass - in - - let for_lvars vs = - let m = EcMemory.memory memenv in - let fresh pv = EcIdent.create (EcIdent.name (id_of_pv ?mc pv m)) in - - let newids = List.map (fst_map fresh) vs in - let bds = newids @ bds in - let astuple = f_tuple (List.map (curry f_local) newids) in - let pre = (subst_form_lv ?mc env lv {m;inv=astuple} {m;inv=pre}).inv in - let e_form = EcFol.ss_inv_of_expr m e in - let e_form = (subst_form_lv ?mc env lv {m;inv=astuple} e_form).inv in - - let assoc = - (List.map (fun x -> APVar x) vs, e_form) - :: (List.map (subst_in_assoc lv astuple newids) assoc) in - - let assoc, bds, pre = simplify_assoc (List.rev assoc, bds, pre) in - - (bds, List.rev assoc, pre) - in - - match lv with - | LvVar v -> for_lvars [v] - | LvTuple vs -> for_lvars vs - - (* ------------------------------------------------------------------ *) - let build_sp (memenv : EcMemory.memenv) bds assoc pre = - let f_assoc = function - | APVar (pv, pv_ty) -> (f_pvar pv pv_ty (EcMemory.memory memenv)).inv - | ALocal (lv, lv_ty) -> f_local lv lv_ty - in - - let rem_ex (assoc, f) (x_id, x_ty) = - try - let rec partition_on_x = function - | [] -> - raise Not_found - | (a, e) :: assoc when f_equal e (f_local x_id x_ty) -> - (a, assoc) - | x :: assoc -> - let a, assoc = partition_on_x assoc in (a, x::assoc) - in - let a,assoc = partition_on_x assoc in - let a = f_tuple (List.map f_assoc a) in - let subst = EcFol.Fsubst.f_subst_id in - let subst = EcFol.Fsubst.f_bind_local subst x_id a in - let f = EcFol.Fsubst.f_subst subst f in - let assoc = List.map (snd_map (EcFol.Fsubst.f_subst subst)) assoc in - (assoc, f) - - with Not_found -> (assoc, f) - in - - let assoc, pre = List.fold_left rem_ex (assoc, pre) bds in - let pre = - let merge_assoc f (a, e) = - f_and_simpl (f_eq_simpl (f_tuple (List.map f_assoc a)) e) f - in List.fold_left merge_assoc pre assoc in - - EcFol.f_exists_simpl (List.map (snd_map (fun t -> GTty t)) bds) pre - - (* ------------------------------------------------------------------ *) - let rec sp_stmt ?mc (memenv : EcMemory.memenv) env (bds, assoc, pre) stmt = - match stmt with - | [] -> - ([], (bds, assoc, pre)) - - | i :: is -> - try - let bds, assoc, pre = - sp_instr ?mc memenv env (bds, assoc, pre) i in - sp_stmt ?mc memenv env (bds, assoc, pre) is - with No_sp -> - (stmt, (bds, assoc, pre)) - - and sp_instr ?mc (memenv : EcMemory.memenv) env (bds,assoc,pre) instr = - match instr.i_node with - | Sasgn (lv, e) -> - let bds, assoc, pre = sp_asgn ?mc memenv env lv e (bds, assoc, pre) in - - bds, assoc, pre - - | Sif (e, s1, s2) -> - let e_form = (EcFol.ss_inv_of_expr (EcMemory.memory memenv) e).inv in - let pre_t = - build_sp memenv bds assoc (f_and_simpl e_form pre) in - let pre_f = - build_sp memenv bds assoc (f_and_simpl (f_not e_form) pre) in - let stmt_t, (bds_t, assoc_t, pre_t) = - sp_stmt ?mc memenv env (bds, assoc, pre_t) s1.s_node in - let stmt_f, (bds_f, assoc_f, pre_f) = - sp_stmt ?mc memenv env (bds, assoc, pre_f) s2.s_node in - if not (List.is_empty stmt_t && List.is_empty stmt_f) then raise No_sp; - let sp_t = build_sp memenv bds_t assoc_t pre_t in - let sp_f = build_sp memenv bds_f assoc_f pre_f in - ([], [], f_or_simpl sp_t sp_f) - - | _ -> raise No_sp - - let sp_stmt ?mc (memenv : EcMemory.memenv) env stmt f = - let stmt, (bds, assoc, pre) = - sp_stmt ?mc memenv env ([], [], f) stmt in - let pre = build_sp memenv bds assoc pre in - stmt, pre -end +(* The [sp] rules live, one module per logic, in [rules//] (the + strongest-postcondition calculus they share is [EcPlSp]). This module + only keeps the legacy entry point and the logic-agnostic dispatchers, + which route on the goal kind and on the shape of the position (single + for hoare / bdhoare, a pair for equiv). *) (* -------------------------------------------------------------------- *) -let t_sp_side pos tc = - let module LI = LowInternal in - - let env, _, concl = FApi.tc1_eflat tc in - - let as_single = function Single i -> i | _ -> assert false - and as_double = function Double i -> i | _ -> assert false in - - let check_sp_progress ?side pos stmt = - if is_some pos && not (List.is_empty stmt) then - tc_error_lazy !!tc (fun fmt -> - let side = side |> (function - | None -> "remaining" - | Some (`Left ) -> "remaining on the left" - | Some (`Right) -> "remaining on the right") - in - - Format.fprintf fmt - "%d instruction(s) %s, change your [sp] bound" - (List.length stmt) side) - in - - let check_form_indep stmt mem form = - let write_set = EcPV.s_write env (EcModules.stmt stmt) in - let read_set = EcPV.PV.fv env (EcMemory.memory mem) form in - if not (EcPV.PV.indep env write_set read_set) then - tc_error !!tc "the bound should not be modified by the statement \ - targeted by [sp]" in - - match concl.f_node, pos with - | FhoareS hs, (None | Some (Single _)) -> - let pos = pos |> omap as_single in - let stmt1, stmt2 = o_split ~rev:true env pos hs.hs_s in - let stmt1, hs_pr = LI.sp_stmt hs.hs_m env stmt1 (hs_pr hs).inv in - check_sp_progress pos stmt1; - let m = fst hs.hs_m in - let subgoal = - f_hoareS - (snd hs.hs_m) - {m;inv=hs_pr} - (stmt (stmt1@stmt2)) - (hs_po hs) - in - FApi.xmutate1 tc `Sp [subgoal] +let as_single = function Single i -> i | Double _ -> assert false +let as_double = function Double i -> i | Single _ -> assert false - - | FbdHoareS bhs, (None | Some (Single _)) -> - let pos = pos |> omap as_single in - let stmt1, stmt2 = o_split ~rev:true env pos bhs.bhs_s in - check_form_indep stmt1 bhs.bhs_m (bhs_bd bhs).inv; - let stmt1, bhs_pr = LI.sp_stmt bhs.bhs_m env stmt1 (bhs_pr bhs).inv in - check_sp_progress pos stmt1; - let m = fst bhs.bhs_m in - let subgoal = f_bdHoareS (snd bhs.bhs_m) {m;inv=bhs_pr} (stmt (stmt1@stmt2)) (bhs_po bhs) bhs.bhs_cmp (bhs_bd bhs) in - FApi.xmutate1 tc `Sp [subgoal] - - | FequivS es, (None | Some (Double _)) -> - let pos = pos |> omap as_double in - let posL = pos |> omap fst in - let posR = pos |> omap snd in - - let stmtL1, stmtL2 = o_split ~rev:true env posL es.es_sl in - let stmtR1, stmtR2 = o_split ~rev:true env posR es.es_sr in - - let es_pr = (es_pr es) in - let ml, mr = fst es.es_ml, fst es.es_mr in - let stmtL1, es_pr = LI.sp_stmt ~mc:(ml, mr) es.es_ml env stmtL1 es_pr.inv in - let stmtR1, es_pr = LI.sp_stmt ~mc:(ml, mr) es.es_mr env stmtR1 es_pr in - - let ml, mr = fst es.es_ml, fst es.es_mr in - - check_sp_progress ~side:`Left pos stmtL1; - check_sp_progress ~side:`Right pos stmtR1; - - let subgoal = f_equivS (snd es.es_ml) (snd es.es_mr) {ml;mr;inv=es_pr} (stmt (stmtL1@stmtL2)) (stmt (stmtR1@stmtR2)) (es_po es) in - - FApi.xmutate1 tc `Sp [subgoal] - - | _, Some (Single _) -> +(* -------------------------------------------------------------------- *) +let t_sp_unsupported (pos : 'a doption option) (tc : tcenv1) = + match pos with + | Some (Single _) -> tc_error_noXhl ~kinds:[`Hoare `Stmt; `PHoare `Stmt] !!tc - - | _, Some (Double _) -> + | Some (Double _) -> tc_error_noXhl ~kinds:[`Equiv `Stmt] !!tc - - | _, None -> + | None -> tc_error_noXhl ~kinds:(hlkinds_Xhl_r `Stmt) !!tc (* -------------------------------------------------------------------- *) -let t_sp = FApi.t_low1 "sp" t_sp_side +let t_sp (pos : EcMatching.Position.codegap1 doption option) (tc : tcenv1) = + match (FApi.tc1_goal tc).f_node, pos with + | FhoareS _, (None | Some (Single _)) -> + EcHoareSp.t_hoare_sp_prefix (omap as_single pos) tc + | FbdHoareS _, (None | Some (Single _)) -> + EcBdHoareSp.t_bdhoare_sp_prefix (omap as_single pos) tc + | FequivS _, (None | Some (Double _)) -> + EcEquivSp.t_equiv_sp_prefix (omap as_double pos) tc + | _ -> + t_sp_unsupported pos tc (* -------------------------------------------------------------------- *) (* [process_sp gap]: splits the statement at [gap]; instructions after the gap are kept, sp is applied to instructions before the gap. *) -let process_sp (cpos : pcodegap1 doption option) (tc : tcenv1) = - let env = FApi.tc1_env tc in - let cpos = Option.map (EcTyping.trans_dcodegap1 env) cpos in - t_sp cpos tc +let process_sp (pos : pcodegap1 doption option) (tc : tcenv1) = + match (FApi.tc1_goal tc).f_node, pos with + | FhoareS _, (None | Some (Single _)) -> + EcHoareSp.process_hoare_sp (omap as_single pos) tc + | FbdHoareS _, (None | Some (Single _)) -> + EcBdHoareSp.process_bdhoare_sp (omap as_single pos) tc + | FequivS _, (None | Some (Double _)) -> + EcEquivSp.process_equiv_sp (omap as_double pos) tc + | _ -> + (* The position is still typed first, as before the migration, so + that its errors take precedence. *) + let env = FApi.tc1_env tc in + t_sp_unsupported (omap (EcTyping.trans_dcodegap1 env) pos) tc diff --git a/src/phl/rules/bdhoare/ecBdHoareSp.ml b/src/phl/rules/bdhoare/ecBdHoareSp.ml new file mode 100644 index 000000000..3b701e5b1 --- /dev/null +++ b/src/phl/rules/bdhoare/ecBdHoareSp.ml @@ -0,0 +1,98 @@ +(* -------------------------------------------------------------------- *) +open EcUtils +open EcFol +open EcAst +open EcEnv + +open EcCoreGoal +open EcLowPhlGoal + +(* -------------------------------------------------------------------- *) +(* Parameters of the bdhoare [sp] rule as supplied by the caller: high + level, the split position is still a symbolic code gap. + + Unlike the hoare and equiv [sp] rules, this rule is stated on [c1; c2] + (it keeps an implicit [seq]): the bdhoare [seq] rule has extra premises + that a derived composition cannot close without changing the visible + goals (see the .mli). *) +type bdhoare_sp_rule = { + bspr_at : EcMatching.Position.codegap1; (* end of the sp-able prefix *) +} + +(* Low-level parameters recorded in the proof-node: the split position is + the RESOLVED integer index. *) +type bdhoare_sp_node = { + bspn_at : EcMatching.Position.nm_codegap1; (* resolved split index *) +} + +type EcCoreGoal.rule += RBdHoareSp of bdhoare_sp_node + +(* -------------------------------------------------------------------- *) +(* [true] when the bound is not written by [s]. *) +let bound_indep env (bhs : bdHoareS) (s : instr list) = + let write = EcPV.s_write env (EcModules.stmt s) in + let read = EcPV.PV.fv env (fst bhs.bhs_m) (bhs_bd bhs).inv in + EcPV.PV.indep env write read + +(* -------------------------------------------------------------------- *) +(* Pure core shared by the rule and its checker. Its side conditions (the + prefix does not write the bound and is sp-able) are part of it, so the + checker re-validates them. *) +let bdhoare_sp_subgoals + (hyps : LDecl.hyps) (bhs : bdHoareS) (n : bdhoare_sp_node) : form list += + let env = LDecl.toenv hyps in + let c1, c2 = EcMatching.Position.split_at_nmcgap1 n.bspn_at bhs.bhs_s in + if not (bound_indep env bhs c1) then + failwith "bdhoare-sp: the bound is written by the prefix"; + let rest, sp = EcPlSp.sp_stmt bhs.bhs_m env c1 (bhs_pr bhs).inv in + if not (List.is_empty rest) then + failwith "bdhoare-sp: the prefix is not sp-able"; + let pre = { m = fst bhs.bhs_m; inv = sp } in + [f_bdHoareS (snd bhs.bhs_m) pre (stmt c2) (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_sp (r : bdhoare_sp_rule) (tc : tcenv1) = + let hyps = FApi.tc1_hyps tc in + let bhs = tc1_as_bdhoareS tc in + let n = { bspn_at = s_split_index (LDecl.toenv hyps) r.bspr_at bhs.bhs_s } in + let subgoals = + try bdhoare_sp_subgoals hyps bhs n + with Failure msg -> tc_error !!tc "%s" msg in + FApi.xrule1 tc (RBdHoareSp n) subgoals + +(* -------------------------------------------------------------------- *) +(* Checker: rerun ONLY the low-level core on the recorded index (see + [EcPlRecheck]). *) +let () = + register_rule_checker + (function + | RBdHoareSp n -> + Some (EcPlRecheck.checker_of "bdhoare-sp" pf_as_bdhoareS + (fun hyps bhs -> bdhoare_sp_subgoals hyps bhs n)) + | _ -> None) + +(* -------------------------------------------------------------------- *) +(* Derived (no proof-node): check, with the user-facing errors, that the + bound is not written by the statement up to [at] and that sp gets that + far, then apply the rule at the end of the longest sp-able prefix. *) +let t_bdhoare_sp_prefix (at : EcMatching.Position.codegap1 option) tc = + let env = FApi.tc1_env tc in + let bhs = tc1_as_bdhoareS tc in + let c1, _ = o_split ~rev:true env at bhs.bhs_s in + if not (bound_indep env bhs c1) then + tc_error !!tc "the bound should not be modified by the statement \ + targeted by [sp]"; + let rest, _ = EcPlSp.sp_stmt bhs.bhs_m env c1 (bhs_pr bhs).inv in + EcPlSp.check_sp_progress tc (is_some at) rest; + let k = List.length c1 - List.length rest in + t_bdhoare_sp { bspr_at = EcPlSp.gap_at k } tc + +(* -------------------------------------------------------------------- *) +(* Elaboration: the goal is known to be a [bdHoareS], the position (if + any) is a single one. *) +let process_bdhoare_sp (at : EcParsetree.pcodegap1 option) tc = + let at = Option.map (EcTyping.trans_codegap1 (FApi.tc1_env tc)) at in + t_bdhoare_sp_prefix at tc diff --git a/src/phl/rules/bdhoare/ecBdHoareSp.mli b/src/phl/rules/bdhoare/ecBdHoareSp.mli new file mode 100644 index 000000000..d27a001cc --- /dev/null +++ b/src/phl/rules/bdhoare/ecBdHoareSp.mli @@ -0,0 +1,57 @@ +(* -------------------------------------------------------------------- *) +open EcParsetree +open EcCoreGoal.FApi +open EcMatching.Position + +(* ==================================================================== *) +(* Rules (trusted) *) + +type bdhoare_sp_rule = { + bspr_at : codegap1; (* split position k: end of the sp-able prefix *) +} + +(* [t_bdhoare_sp { bspr_at = k }] — strongest postcondition of a prefix, + with [~] the goal's comparison: + + phoare [c2 : sp(c1, P) ==> Q] ~ d + ----------------------------------------- c = c1; c2 (c1 = c[0..k)) + phoare [c : P ==> Q] ~ d c1 sp-able, d not written by c1 + + where [sp] is [EcPlSp.sp_stmt]. Side conditions: [c1] is entirely + sp-able and does not write the variables of the bound [d] (otherwise + fails). + + RETAINED IMPLICIT SEQ. Unlike the hoare and equiv [sp] rules, this rule + is stated on [c1; c2]. [EcBdHoareSeq.t_bdhoare_seq] with phi := true, + R := sp(c1, P), f1 := 1, f2 := d, g1 := 0, g2 := 1 has this rule's + premise as its (F2), but deriving the rule from it would also need + closing, on the spot: (H) by [EcHoareTrue]; (F1) + [phoare [c1 : P ==> sp(c1, P)] ~ 1] by a further trusted bdhoare rule; + (G1) [phoare [c1 : P ==> !sp(c1, P)] ~ 0] through the not yet migrated + hoare-to-phoare consequence; and the arithmetic (B) + [P => 1 * d + 0 * 1 ~ d] and non-modification (N) premises with + best-effort tactics, which do not reliably close them (so the visible + goals could change). The rule is kept on [c1; c2] until this can be + done exactly. Its side condition on [d] is what (N) would express. + + Node: [RBdHoareSp { bspn_at = k (resolved index) }]. + Checker: "bdhoare-sp". *) +val t_bdhoare_sp : bdhoare_sp_rule -> backward + +(* ==================================================================== *) +(* Derived tactics *) + +(* [t_bdhoare_sp_prefix at] — on [phoare [c : P ==> Q] ~ d], with [c0] the + prefix of [c] up to [at] (the whole of [c] when [at] is [None]), and + [c1] the longest sp-able prefix of [c0]: [t_bdhoare_sp] at [|c1|]. + Fails (before applying the rule) when [c0] writes the bound [d], or + when [at] is given and [c0] is not entirely sp-able. Visible goal: the + premise of the rule. Emits no node of its own. *) +val t_bdhoare_sp_prefix : codegap1 option -> backward + +(* ==================================================================== *) +(* Elaboration *) + +(* [sp] / [sp k] on a [bdHoareS] goal (a single position): applies + [t_bdhoare_sp_prefix]. *) +val process_bdhoare_sp : pcodegap1 option -> backward diff --git a/src/phl/rules/ecPlSp.ml b/src/phl/rules/ecPlSp.ml new file mode 100644 index 000000000..645d7d519 --- /dev/null +++ b/src/phl/rules/ecPlSp.ml @@ -0,0 +1,219 @@ +(* -------------------------------------------------------------------- *) +open EcUtils +open EcAst +open EcTypes +open EcModules +open EcFol +open EcEnv +open EcCoreGoal +open EcLowPhlGoal + +(* -------------------------------------------------------------------- *) +(* Strongest-postcondition calculus, shared by the [sp] rules of every + logic (it is part of their trusted subgoal builders). + + SP carries three elements, + - bds: a set of existential binders + - assoc: a set of pairs (x,e) such that x=e holds + for instance after an assignment x <- e + - pre: the actual precondition (progressively weakened) + + After an assignment of the form x <- e the three elements are updated: + 1) a new fresh local x' is added to the list of existential binders + 2) (x, e) is added to the assoc list, and every other (y,d) is replaced + by (y[x->x'], d[x->x']) + 3) pre is replaced by pre[x->x'] + + The simplification of this version comes from one trick: the + replacement of (y[x->x']) introduces a simplification opportunity. + There is no need to keep (x', d[x->x']) as a conjuction + x' = d[x->x']: it is enough to perform the substitution of d[x->x'] + for x' in place (it is a mess however to implement this idea with + simultaneous assigns). *) + +(* -------------------------------------------------------------------- *) +exception No_sp + +(* -------------------------------------------------------------------- *) +type assignable = +| APVar of (prog_var * ty) +| ALocal of (EcIdent.t * ty) + +and assignables = assignable list + +(* -------------------------------------------------------------------- *) +let sp_asgn ?mc (memenv : EcMemory.memenv) env lv e (bds, assoc, pre) = + let m = fst memenv in + let subst_in_assoc lv new_id_exp new_ids ((ass : assignables), f) = + let replace_assignable var = + match var with + | APVar (pv', ty) -> begin + match lv,new_ids with + | LvVar (pv ,_), [new_id,_] when NormMp.pv_equal env pv pv' -> + ALocal (new_id,ty) + + | LvVar _, _ -> + var + + | LvTuple vs, _ -> begin + let aux = List.map2 (fun x y -> (fst x, fst y)) vs new_ids in + try + let new_id = snd (List.find (NormMp.pv_equal env pv' -| fst) aux) in + ALocal (new_id, ty) + with Not_found -> var + end + end + | _ -> var + + in let ass = List.map replace_assignable ass in + let f = (subst_form_lv ?mc env lv {m;inv=new_id_exp} {m;inv=f}).inv in + (ass, f) + in + + let rec simplify_assoc (assoc, bds, pre) = + match assoc with + | [] -> + ([], bds, pre) + + | (ass, f) :: assoc -> + let assoc, bds, pre = simplify_assoc (assoc, bds, pre) in + + let destr_ass = + try List.combine (List.map in_seq1 ass) (destr_tuple f) + with Invalid_argument _ | DestrError _ -> [(ass, f)] + in + + let do_subst_or_accum (assoc, bds, pre) (a, f) = + match a with + | [ALocal (id, _)] -> + let subst = EcFol.Fsubst.f_subst_id in + let subst = EcFol.Fsubst.f_bind_local subst id f in + (List.map (snd_map (EcFol.Fsubst.f_subst subst)) assoc, + List.filter ((<>) id -| fst) bds, + EcFol.Fsubst.f_subst subst pre) + + | _ -> ((a, f) :: assoc, bds, pre) + in + List.fold_left do_subst_or_accum (assoc, bds, pre) destr_ass + in + + let for_lvars vs = + let m = EcMemory.memory memenv in + let fresh pv = EcIdent.create (EcIdent.name (id_of_pv ?mc pv m)) in + + let newids = List.map (fst_map fresh) vs in + let bds = newids @ bds in + let astuple = f_tuple (List.map (curry f_local) newids) in + let pre = (subst_form_lv ?mc env lv {m;inv=astuple} {m;inv=pre}).inv in + let e_form = EcFol.ss_inv_of_expr m e in + let e_form = (subst_form_lv ?mc env lv {m;inv=astuple} e_form).inv in + + let assoc = + (List.map (fun x -> APVar x) vs, e_form) + :: (List.map (subst_in_assoc lv astuple newids) assoc) in + + let assoc, bds, pre = simplify_assoc (List.rev assoc, bds, pre) in + + (bds, List.rev assoc, pre) + in + + match lv with + | LvVar v -> for_lvars [v] + | LvTuple vs -> for_lvars vs + +(* -------------------------------------------------------------------- *) +let build_sp (memenv : EcMemory.memenv) bds assoc pre = + let f_assoc = function + | APVar (pv, pv_ty) -> (f_pvar pv pv_ty (EcMemory.memory memenv)).inv + | ALocal (lv, lv_ty) -> f_local lv lv_ty + in + + let rem_ex (assoc, f) (x_id, x_ty) = + try + let rec partition_on_x = function + | [] -> + raise Not_found + | (a, e) :: assoc when f_equal e (f_local x_id x_ty) -> + (a, assoc) + | x :: assoc -> + let a, assoc = partition_on_x assoc in (a, x::assoc) + in + let a,assoc = partition_on_x assoc in + let a = f_tuple (List.map f_assoc a) in + let subst = EcFol.Fsubst.f_subst_id in + let subst = EcFol.Fsubst.f_bind_local subst x_id a in + let f = EcFol.Fsubst.f_subst subst f in + let assoc = List.map (snd_map (EcFol.Fsubst.f_subst subst)) assoc in + (assoc, f) + + with Not_found -> (assoc, f) + in + + let assoc, pre = List.fold_left rem_ex (assoc, pre) bds in + let pre = + let merge_assoc f (a, e) = + f_and_simpl (f_eq_simpl (f_tuple (List.map f_assoc a)) e) f + in List.fold_left merge_assoc pre assoc in + + EcFol.f_exists_simpl (List.map (snd_map (fun t -> GTty t)) bds) pre + +(* -------------------------------------------------------------------- *) +let rec sp_stmt_r ?mc (memenv : EcMemory.memenv) env (bds, assoc, pre) stmt = + match stmt with + | [] -> + ([], (bds, assoc, pre)) + + | i :: is -> + try + let bds, assoc, pre = + sp_instr ?mc memenv env (bds, assoc, pre) i in + sp_stmt_r ?mc memenv env (bds, assoc, pre) is + with No_sp -> + (stmt, (bds, assoc, pre)) + +and sp_instr ?mc (memenv : EcMemory.memenv) env (bds,assoc,pre) instr = + match instr.i_node with + | Sasgn (lv, e) -> + let bds, assoc, pre = sp_asgn ?mc memenv env lv e (bds, assoc, pre) in + + bds, assoc, pre + + | Sif (e, s1, s2) -> + let e_form = (EcFol.ss_inv_of_expr (EcMemory.memory memenv) e).inv in + let pre_t = + build_sp memenv bds assoc (f_and_simpl e_form pre) in + let pre_f = + build_sp memenv bds assoc (f_and_simpl (f_not e_form) pre) in + let stmt_t, (bds_t, assoc_t, pre_t) = + sp_stmt_r ?mc memenv env (bds, assoc, pre_t) s1.s_node in + let stmt_f, (bds_f, assoc_f, pre_f) = + sp_stmt_r ?mc memenv env (bds, assoc, pre_f) s2.s_node in + if not (List.is_empty stmt_t && List.is_empty stmt_f) then raise No_sp; + let sp_t = build_sp memenv bds_t assoc_t pre_t in + let sp_f = build_sp memenv bds_f assoc_f pre_f in + ([], [], f_or_simpl sp_t sp_f) + + | _ -> raise No_sp + +(* -------------------------------------------------------------------- *) +let sp_stmt ?mc (memenv : EcMemory.memenv) env (s : instr list) (pre : form) = + let rest, (bds, assoc, pre) = sp_stmt_r ?mc memenv env ([], [], pre) s in + rest, build_sp memenv bds assoc pre + +(* -------------------------------------------------------------------- *) +let check_sp_progress ?side (tc : tcenv1) (bounded : bool) (rest : instr list) = + if bounded && not (List.is_empty rest) then + tc_error_lazy !!tc (fun fmt -> + let side = side |> (function + | None -> "remaining" + | Some (`Left ) -> "remaining on the left" + | Some (`Right) -> "remaining on the right") + in + + Format.fprintf fmt + "%d instruction(s) %s, change your [sp] bound" + (List.length rest) side) + +(* -------------------------------------------------------------------- *) +let gap_at (k : int) : EcMatching.Position.codegap1 = + EcMatching.Position.(gap_before_pos (cpos1 k)) diff --git a/src/phl/rules/ecPlSp.mli b/src/phl/rules/ecPlSp.mli new file mode 100644 index 000000000..adc813332 --- /dev/null +++ b/src/phl/rules/ecPlSp.mli @@ -0,0 +1,30 @@ +(* -------------------------------------------------------------------- *) +open EcAst +open EcEnv +open EcCoreGoal + +(* -------------------------------------------------------------------- *) +(* Strongest postcondition, shared by the [sp] rules of every logic. + + An instruction is sp-able when it is an assignment, or a conditional + whose two branches are (entirely) sp-able. *) + +(* [sp_stmt ?mc me env c P] = [(rest, sp(c1, P))], where [c = c1; rest], + [c1] is the longest sp-able prefix of [c], and [sp(c1, P)] is the + strongest postcondition of [c1] from [P] (a formula in the memory of + [me]). The variables existentially quantified in [sp(c1, P)] are fresh + at each call: two calls on the same arguments agree up to + alpha-conversion. [mc] gives the two memories of a two-sided goal (it + only affects the names of these variables). *) +val sp_stmt : + ?mc:(memory * memory) -> memenv -> env + -> instr list -> form -> instr list * form + +(* [check_sp_progress ?side tc bounded rest] — when the user gave a bound + ([bounded]), fails (user-facing error) if [rest] is not empty. *) +val check_sp_progress : + ?side:[`Left | `Right] -> tcenv1 -> bool -> instr list -> unit + +(* [gap_at k] — the code gap before the [k]-th instruction (0-based), i.e. + splitting at [gap_at k] keeps the first [k] instructions as prefix. *) +val gap_at : int -> EcMatching.Position.codegap1 diff --git a/src/phl/rules/equiv/ecEquivSp.ml b/src/phl/rules/equiv/ecEquivSp.ml new file mode 100644 index 000000000..00c79b1b2 --- /dev/null +++ b/src/phl/rules/equiv/ecEquivSp.ml @@ -0,0 +1,80 @@ +(* -------------------------------------------------------------------- *) +open EcUtils +open EcAst +open EcEnv + +open EcCoreGoal +open EcLowPhlGoal + +(* -------------------------------------------------------------------- *) +(* The equiv [sp] rule has no parameters: it is stated on the whole + statements, which must be sp-able. *) +type EcCoreGoal.rule += REquivSp + +(* -------------------------------------------------------------------- *) +(* Two-sided strongest postcondition: the left statement first, then the + right one. Returns the parts of the statements that are not sp-able. *) +let equiv_sp env (es : equivS) (sl : instr list) (sr : instr list) = + let mc = (fst es.es_ml, fst es.es_mr) in + let restl, sp = EcPlSp.sp_stmt ~mc es.es_ml env sl (es_pr es).inv in + let restr, sp = EcPlSp.sp_stmt ~mc es.es_mr env sr sp in + (restl, restr), sp + +(* -------------------------------------------------------------------- *) +(* Pure core shared by the rule and its checker. Its side conditions (both + statements are sp-able, the postcondition is their strongest + postcondition) are part of it, so the checker re-validates them. *) +let equiv_sp_subgoals (hyps : LDecl.hyps) (es : equivS) : form list = + let env = LDecl.toenv hyps in + let (restl, restr), sp = equiv_sp env es es.es_sl.s_node es.es_sr.s_node in + if not (List.is_empty restl && List.is_empty restr) then + failwith "equiv-sp: the statements are not sp-able"; + if not (EcReduction.is_conv hyps sp (es_po es).inv) then + failwith "equiv-sp: the postcondition is not the strongest postcondition"; + [] + +(* -------------------------------------------------------------------- *) +(* Rule (TCB). *) +let t_equiv_sp (tc : tcenv1) = + let es = tc1_as_equivS tc in + let subgoals = + try equiv_sp_subgoals (FApi.tc1_hyps tc) es + with Failure msg -> tc_error !!tc "%s" msg in + FApi.xrule1 tc REquivSp subgoals + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | REquivSp -> + Some (EcPlRecheck.checker_of "equiv-sp" pf_as_equivS + equiv_sp_subgoals) + | _ -> None) + +(* -------------------------------------------------------------------- *) +(* Derived (no proof-node): compute the longest sp-able prefixes [c1] / + [c1'] of the statements up to [at], split there with the [seq] rule + using [sp(c1, c1', P)] as intermediate relation, and close the first + premise with the rule. *) +let t_equiv_sp_prefix (at : EcMatching.Position.codegap1 pair option) tc = + let env = FApi.tc1_env tc in + let es = tc1_as_equivS tc in + let sl1, _ = o_split ~rev:true env (omap fst at) es.es_sl in + let sr1, _ = o_split ~rev:true env (omap snd at) es.es_sr in + let (restl, restr), sp = equiv_sp env es sl1 sr1 in + EcPlSp.check_sp_progress ~side:`Left tc (is_some at) restl; + EcPlSp.check_sp_progress ~side:`Right tc (is_some at) restr; + let kl = List.length sl1 - List.length restl in + let kr = List.length sr1 - List.length restr in + let r = EcEquivSeq.{ + esr_at = (EcPlSp.gap_at kl, EcPlSp.gap_at kr); + esr_mid = { ml = fst es.es_ml; mr = fst es.es_mr; inv = sp }; } in + FApi.t_seqsub (EcEquivSeq.t_equiv_seq r) [t_equiv_sp; EcLowGoal.t_id] tc + +(* -------------------------------------------------------------------- *) +(* Elaboration: the goal is known to be an [equivS], the positions (if + any) are a pair. *) +let process_equiv_sp (at : EcParsetree.pcodegap1 pair option) tc = + let env = FApi.tc1_env tc in + let at = Option.map (pair_map (EcTyping.trans_codegap1 env)) at in + t_equiv_sp_prefix at tc diff --git a/src/phl/rules/equiv/ecEquivSp.mli b/src/phl/rules/equiv/ecEquivSp.mli new file mode 100644 index 000000000..d009dc713 --- /dev/null +++ b/src/phl/rules/equiv/ecEquivSp.mli @@ -0,0 +1,45 @@ +(* -------------------------------------------------------------------- *) +open EcUtils +open EcParsetree +open EcCoreGoal.FApi +open EcMatching.Position + +(* ==================================================================== *) +(* Rules (trusted) *) + +(* [t_equiv_sp] — strongest postcondition: + + ------------------------------------------- c, c' sp-able + equiv [c ~ c' : P ==> sp<2>(c', sp<1>(c, P))] + + where [sp] is [EcPlSp.sp_stmt] in the memory of side [i]: the left + statement is traversed first, then the right one from the result. No + premise. Side conditions: [c] and [c'] are entirely sp-able, and the + postcondition is convertible to [sp<2>(c', sp<1>(c, P))] (otherwise + fails). + + Node: [REquivSp]. Checker: "equiv-sp". *) +val t_equiv_sp : backward + +(* ==================================================================== *) +(* Derived tactics *) + +(* [t_equiv_sp_prefix at] — on [equiv [c ~ c' : P ==> Q]], with [c0] / + [c0'] the prefixes of [c] / [c'] up to the positions [at] (the whole + statements when [at] is [None]), and [c1] / [c1'] their longest sp-able + prefixes, [c = c1; c2], [c' = c1'; c2']: + 1. [EcEquivSeq.t_equiv_seq] at [(|c1|, |c1'|)], with + [R := sp<2>(c1', sp<1>(c1, P))], giving + (a) equiv [c1 ~ c1' : P ==> R], + (b) equiv [c2 ~ c2' : R ==> Q]; + 2. on (a), [t_equiv_sp]. + Visible goal: (b). Fails (before applying any rule) when [at] is given + and [c0] or [c0'] is not entirely sp-able. Emits no node of its own. *) +val t_equiv_sp_prefix : codegap1 pair option -> backward + +(* ==================================================================== *) +(* Elaboration *) + +(* [sp] / [sp k k'] on an [equivS] goal (a pair of positions): applies + [t_equiv_sp_prefix]. *) +val process_equiv_sp : pcodegap1 pair option -> backward diff --git a/src/phl/rules/hoare/ecHoareSp.ml b/src/phl/rules/hoare/ecHoareSp.ml new file mode 100644 index 000000000..5d9649eed --- /dev/null +++ b/src/phl/rules/hoare/ecHoareSp.ml @@ -0,0 +1,65 @@ +(* -------------------------------------------------------------------- *) +open EcUtils +open EcAst +open EcEnv + +open EcCoreGoal +open EcLowPhlGoal + +(* -------------------------------------------------------------------- *) +(* The hoare [sp] rule has no parameters: it is stated on the whole + statement, which must be sp-able. *) +type EcCoreGoal.rule += RHoareSp + +(* -------------------------------------------------------------------- *) +(* Pure core shared by the rule and its checker. Its side conditions (the + statement is sp-able, the postcondition is its strongest postcondition) + are part of it, so the checker re-validates them. *) +let hoare_sp_subgoals (hyps : LDecl.hyps) (hs : sHoareS) : form list = + let env = LDecl.toenv hyps in + let rest, sp = EcPlSp.sp_stmt hs.hs_m env hs.hs_s.s_node (hs_pr hs).inv in + if not (List.is_empty rest) then + failwith "hoare-sp: the statement is not sp-able"; + if not (EcReduction.is_conv hyps sp (POE.lower (hs_po hs)).inv) then + failwith "hoare-sp: the postcondition is not the strongest postcondition"; + [] + +(* -------------------------------------------------------------------- *) +(* Rule (TCB). *) +let t_hoare_sp (tc : tcenv1) = + let hs = tc1_as_hoareS tc in + let subgoals = + try hoare_sp_subgoals (FApi.tc1_hyps tc) hs + with Failure msg -> tc_error !!tc "%s" msg in + FApi.xrule1 tc RHoareSp subgoals + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | RHoareSp -> + Some (EcPlRecheck.checker_of "hoare-sp" pf_as_hoareS + hoare_sp_subgoals) + | _ -> None) + +(* -------------------------------------------------------------------- *) +(* Derived (no proof-node): compute the longest sp-able prefix [c1] of the + statement up to [at], split there with the [seq] rule using [sp(c1, P)] + as intermediate assertion, and close the first premise with the rule. *) +let t_hoare_sp_prefix (at : EcMatching.Position.codegap1 option) tc = + let env = FApi.tc1_env tc in + let hs = tc1_as_hoareS tc in + let c1, _ = o_split ~rev:true env at hs.hs_s in + let rest, sp = EcPlSp.sp_stmt hs.hs_m env c1 (hs_pr hs).inv in + EcPlSp.check_sp_progress tc (is_some at) rest; + let k = List.length c1 - List.length rest in + let r = EcHoareSeq.{ hsr_at = EcPlSp.gap_at k; + hsr_mid = { m = fst hs.hs_m; inv = sp }; } in + FApi.t_seqsub (EcHoareSeq.t_hoare_seq r) [t_hoare_sp; EcLowGoal.t_id] tc + +(* -------------------------------------------------------------------- *) +(* Elaboration: the goal is known to be a [hoareS], the position (if any) + is a single one. *) +let process_hoare_sp (at : EcParsetree.pcodegap1 option) tc = + let at = Option.map (EcTyping.trans_codegap1 (FApi.tc1_env tc)) at in + t_hoare_sp_prefix at tc diff --git a/src/phl/rules/hoare/ecHoareSp.mli b/src/phl/rules/hoare/ecHoareSp.mli new file mode 100644 index 000000000..40b980f3b --- /dev/null +++ b/src/phl/rules/hoare/ecHoareSp.mli @@ -0,0 +1,41 @@ +(* -------------------------------------------------------------------- *) +open EcParsetree +open EcCoreGoal.FApi +open EcMatching.Position + +(* ==================================================================== *) +(* Rules (trusted) *) + +(* [t_hoare_sp] — strongest postcondition: + + ------------------------------------ c sp-able + hoare [c : P ==> sp(c, P) | Q_e] + + where [sp] is [EcPlSp.sp_stmt]. The exceptional postconditions [Q_e] + play no role: an sp-able statement (assignments and conditionals) raises + nothing. No premise. Side conditions: [c] is entirely sp-able, and the + postcondition is convertible to [sp(c, P)] (otherwise fails). + + Node: [RHoareSp]. Checker: "hoare-sp". *) +val t_hoare_sp : backward + +(* ==================================================================== *) +(* Derived tactics *) + +(* [t_hoare_sp_prefix at] — on [hoare [c : P ==> Q | Q_e]], with [c0] the + prefix of [c] up to [at] (the whole of [c] when [at] is [None]), and + [c1] the longest sp-able prefix of [c0], [c = c1; c2]: + 1. [EcHoareSeq.t_hoare_seq] at [|c1|], with [R := sp(c1, P)], giving + (a) hoare [c1 : P ==> sp(c1, P) | Q_e], + (b) hoare [c2 : sp(c1, P) ==> Q | Q_e]; + 2. on (a), [t_hoare_sp]. + Visible goal: (b). Fails (before applying any rule) when [at] is given + and [c0] is not entirely sp-able. Emits no node of its own. *) +val t_hoare_sp_prefix : codegap1 option -> backward + +(* ==================================================================== *) +(* Elaboration *) + +(* [sp] / [sp k] on a [hoareS] goal (a single position): applies + [t_hoare_sp_prefix]. *) +val process_hoare_sp : pcodegap1 option -> backward diff --git a/tests/sp.ec b/tests/sp.ec new file mode 100644 index 000000000..201528445 --- /dev/null +++ b/tests/sp.ec @@ -0,0 +1,152 @@ +require import AllCore Distr DBool Xreal. + +exception exn1. + +module M = { + var g : int + + proc h() : int = { return 0; } + + proc f(a : int) : int = { + var x, y, z, b; + x <- a; + (y, z) <- (x + 1, x); + if (x = 0) { y <- 1; } else { y <- 2; z <- 3; } + g <- y; + b <$ {0,1}; + x <- x + 1; + return x + y + z; + } + + proc k(a : int) : int = { + var x; + x <@ h(); + x <- a; + return x; + } + + proc e(a : int) : int = { + var x; + x <- a; + g <- x; + if (x = 0) { raise exn1; } + return x; + } +}. + +(* -------------------------------------------------------------------- *) +(* hoare *) + +lemma hoare_sp_all : hoare [M.f : 0 <= a ==> 0 < res]. +proof. +proc; sp. +(* sp stops at the sampling: 2 instructions are left. *) +seq 1 : (0 <= x /\ 0 < y /\ 0 <= z); first by auto => /> /#. +by wp; skip => /> /#. +qed. + +lemma hoare_sp_pos : hoare [M.f : 0 <= a ==> 0 < res]. +proof. +proc; sp 2; sp 1; sp 0; sp. +by auto => /> /#. +qed. + +(* Bound past the sp-able prefix: no progress allowed. *) +lemma hoare_sp_noprogress : hoare [M.f : 0 <= a ==> 0 < res]. +proof. +proc. +fail sp 5. +fail sp 1 1. +sp 4. +fail sp 1. +abort. + +(* Nothing to do: the statement starts with a call. *) +lemma hoare_sp_none : hoare [M.k : a = 3 ==> res = 3]. +proof. +proc; sp. +by inline *; auto. +qed. + +(* Exceptional postconditions are kept. *) +lemma hoare_sp_exn : hoare [M.e : true ==> res <> 0 | exn1 => M.g = 0]. +proof. +proc; sp 2. +by auto. +qed. + +(* -------------------------------------------------------------------- *) +(* phoare *) + +lemma phoare_sp_all : phoare [M.f : 0 <= a ==> 0 < res] = 1%r. +proof. +proc; sp. +by auto => />; smt(dbool_ll). +qed. + +lemma phoare_sp_le : phoare [M.f : 0 <= a ==> 0 < res] <= 1%r. +proof. +proc; sp 3; sp. +by wp; rnd; skip => />; smt(mu_bounded). +qed. + +lemma phoare_sp_noprogress : phoare [M.f : 0 <= a ==> 0 < res] = 1%r. +proof. +proc. +fail sp 5. +fail sp 1 1. +abort. + +(* The bound must not be modified by the targeted statement. *) +lemma phoare_sp_bound : phoare [M.f : 0 <= a ==> 0 < res] = (if M.g = 0 then 1%r else 1%r). +proof. +proc. +fail sp. +fail sp 4. +sp 3. +abort. + +(* -------------------------------------------------------------------- *) +(* equiv *) + +lemma equiv_sp_all : equiv [M.f ~ M.f : ={a} ==> ={res}]. +proof. +proc; sp. +by auto => /> /#. +qed. + +lemma equiv_sp_pos : equiv [M.f ~ M.f : ={a} ==> ={res}]. +proof. +proc; sp 1 0; sp 0 2; sp 3 2; sp. +by auto => /> /#. +qed. + +lemma equiv_sp_asym : equiv [M.k ~ M.f : ={a} ==> true]. +proof. +proc; sp. +by inline *; auto. +qed. + +lemma equiv_sp_noprogress : equiv [M.f ~ M.f : ={a} ==> ={res}]. +proof. +proc. +fail sp 5 0. +fail sp 0 5. +fail sp 1. +abort. + +(* -------------------------------------------------------------------- *) +(* unsupported goals *) + +lemma ehoare_sp : ehoare [M.f : (1%xr) ==> (1%xr)]. +proof. +proc. +fail sp. +fail sp 1. +fail sp 1 1. +abort. + +lemma hoareF_sp : hoare [M.f : 0 <= a ==> 0 < res]. +proof. +fail sp. +abort.