diff --git a/src/ecLowPhlGoal.ml b/src/ecLowPhlGoal.ml index b90fc276a..acfe87d86 100644 --- a/src/ecLowPhlGoal.ml +++ b/src/ecLowPhlGoal.ml @@ -436,6 +436,14 @@ let s_split env i s = try Pos.split_at_cgap1 env i s with Pos.InvalidCPos -> raise (InvalidSplit (`Gap i)) +(* Resolve a (symbolic) code gap to its normalized integer index. This is the + env-dependent "code resolution" step; splitting a statement at the resulting + index ([EcMatching.Position.split_at_nmcgap1]) needs no environment. *) +let s_split_index env i s = + let module Pos = EcMatching.Position in + try Pos.normalize_cgap1 env i s + with Pos.InvalidCPos -> raise (InvalidSplit (`Gap i)) + (* -------------------------------------------------------------------- *) let s_split_i env i s = let module Pos = EcMatching.Position in diff --git a/src/ecParser.mly b/src/ecParser.mly index 9b180e226..735cc2980 100644 --- a/src/ecParser.mly +++ b/src/ecParser.mly @@ -3139,7 +3139,7 @@ direction: { Pfun `Code } | SEQ s=side? pos=s_codegap1_0before COLON p=form_or_double_form f=app_bd_info - { Pseq (s, pos, p, f) } + { Pseq { seqi_side = s; seqi_at = pos; seqi_mid = p; seqi_bd = f; } } | WP n=s_codegap1_0before? { Pwp n } diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml index b4a7ab105..2a97e9136 100644 --- a/src/ecParsetree.ml +++ b/src/ecParsetree.ml @@ -706,8 +706,12 @@ type fun_info = [ ] (* -------------------------------------------------------------------- *) -type seq_info = - oside * pcodegap1 doption * pformula doption * p_seq_xt_info +type seq_info = { + seqi_side : oside; (* side (prhl only) *) + seqi_at : pcodegap1 doption; (* split position(s) *) + seqi_mid : pformula doption; (* intermediate assertion / (pre, post) *) + seqi_bd : p_seq_xt_info; (* bound information (bdhoare only) *) +} (* -------------------------------------------------------------------- *) type pcond_info = [ diff --git a/src/phl/ecPhlSeq.ml b/src/phl/ecPhlSeq.ml index 0b14bf08e..71fc35ffe 100644 --- a/src/phl/ecPhlSeq.ml +++ b/src/phl/ecPhlSeq.ml @@ -1,277 +1,45 @@ (* -------------------------------------------------------------------- *) -open EcUtils -open EcLocation open EcParsetree -open EcTypes -open EcFol open EcAst -open EcSubst open EcCoreGoal -open EcLowGoal -open EcLowPhlGoal - -module TTC = EcProofTyping (* -------------------------------------------------------------------- *) -(* [t_hoare_seq_r gap phi]: splits the statement at [gap]; the first - subgoal covers instructions before the gap, the second after. *) -let t_hoare_seq_r i phi tc = - let env = FApi.tc1_env tc in - let hs = tc1_as_hoareS tc in - let phi = ss_inv_rebind phi (fst hs.hs_m) in - let s1, s2 = s_split env i hs.hs_s in - let post = update_hs_ss phi (hs_po hs) in - let a = f_hoareS (snd hs.hs_m) (hs_pr hs) (stmt s1) post in - let b = f_hoareS (snd hs.hs_m) phi (stmt s2) (hs_po hs) in - FApi.xmutate1 tc `HlApp [a; b] - -let t_hoare_seq = FApi.t_low2 "hoare-seq" t_hoare_seq_r +(* The [seq] rules live, one module per logic, in [rules//]: each + owns its parameter records, pure subgoal builder, recheckable proof-node, + checker and elaboration. This module only keeps the legacy positional + entry points (adapters onto those rules, so external callers and this + module's interface are unchanged) and the logic-agnostic dispatcher. *) (* -------------------------------------------------------------------- *) -let t_ehoare_seq_r i phi tc = - let env = FApi.tc1_env tc in - let hs = tc1_as_ehoareS tc in - let s1, s2 = s_split env i hs.ehs_s in - let phi = ss_inv_rebind phi (fst hs.ehs_m) in - let a = f_eHoareS (snd hs.ehs_m) (ehs_pr hs) (stmt s1) phi in - let b = f_eHoareS (snd hs.ehs_m) phi (stmt s2) (ehs_po hs) in - FApi.xmutate1 tc `HlApp [a; b] +let t_hoare_seq i phi = + EcHoareSeq.(t_hoare_seq { hsr_at = i; hsr_mid = phi }) -let t_ehoare_seq = FApi.t_low2 "hoare-seq" t_ehoare_seq_r +let t_ehoare_seq i phi = + EcEHoareSeq.(t_ehoare_seq { ehsr_at = i; ehsr_mid = phi }) -(* -------------------------------------------------------------------- *) -let t_bdhoare_seq_r_low i (phi, pR, f1, f2, g1, g2) tc = - let env = FApi.tc1_env tc in - let bhs = tc1_as_bdhoareS tc in - let m = fst bhs.bhs_m in - let phi = ss_inv_rebind phi m in - let pR = ss_inv_rebind pR m in - let f1 = ss_inv_rebind f1 m in - let f2 = ss_inv_rebind f2 m in - let g1 = ss_inv_rebind g1 m in - let g2 = ss_inv_rebind g2 m in - let s1, s2 = s_split env i bhs.bhs_s in - let s1, s2 = stmt s1, stmt s2 in - let nR = map_ss_inv1 f_not pR in - let mt = snd bhs.bhs_m in - let post = POE.lift phi in - let cond_phi = f_hoareS mt (bhs_pr bhs) s1 post in - let condf1 = f_bdHoareS mt (bhs_pr bhs) s1 pR bhs.bhs_cmp f1 in - let condg1 = f_bdHoareS mt (bhs_pr bhs) s1 nR bhs.bhs_cmp g1 in - let condf2 = f_bdHoareS mt (map_ss_inv2 f_and_simpl phi pR) s2 (bhs_po bhs) bhs.bhs_cmp f2 in - let condg2 = f_bdHoareS mt (map_ss_inv2 f_and_simpl phi nR) s2 (bhs_po bhs) bhs.bhs_cmp g2 in - let bd = - (map_ss_inv2 f_real_add_simpl (map_ss_inv2 f_real_mul_simpl f1 f2) (map_ss_inv2 f_real_mul_simpl g1 g2)) in - let condbd = - match bhs.bhs_cmp with - | FHle -> map_ss_inv2 f_real_le bd (bhs_bd bhs) - | FHeq -> map_ss_inv2 f_eq bd (bhs_bd bhs) - | FHge -> map_ss_inv2 f_real_le (bhs_bd bhs) bd in - let condbd = map_ss_inv2 f_imp (bhs_pr bhs) condbd in - let (ir1, ir2) = EcIdent.create "r", EcIdent.create "r" in - let (r1 , r2 ) = f_local ir1 treal, f_local ir2 treal in - let condnm = - let eqs = map_ss_inv2 f_and (map_ss_inv1 ((EcUtils.flip f_eq) r1) f2) - (map_ss_inv1 ((EcUtils.flip f_eq) r2) g2) in - let post = empty_hs eqs in - f_forall - [(ir1, GTty treal); (ir2, GTty treal)] - (f_hoareS (snd bhs.bhs_m) - (map_ss_inv2 f_and (bhs_pr bhs) eqs) s1 post) - in - let conds = [EcSubst.f_forall_mems_ss_inv bhs.bhs_m condbd; condnm] in - let conds = - if f_equal g1.inv f_r0 - then condg1 :: conds - else if f_equal g2.inv f_r0 - then condg2 :: conds - else condg1 :: condg2 :: conds in +(* Adapts onto the derived form: rule + discharge of the non-modification + subgoal. *) +let t_bdhoare_seq i (phi, pR, f1, f2, g1, g2) = + EcBdHoareSeq.(t_bdhoare_seq_full + { bsr_at = i; bsr_phi = phi; bsr_r = pR; + bsr_f1 = f1; bsr_f2 = f2; bsr_g1 = g1; bsr_g2 = g2; }) - let conds = - if f_equal f1.inv f_r0 - then condf1 :: conds - else if f_equal f2.inv f_r0 - then condf2 :: conds - else condf1 :: condf2 :: conds in +let t_equiv_seq (i, j) phi = + EcEquivSeq.(t_equiv_seq { esr_at = (i, j); esr_mid = phi }) - let conds = cond_phi :: conds in - - FApi.xmutate1 tc `HlApp conds +let t_equiv_seq_onesided = EcEquivSeq.t_equiv_seq_onesided (* -------------------------------------------------------------------- *) -let t_bdhoare_seq_r i info tc = - let tactic tc = - let hs = tc1_as_hoareS tc in - let tt1 = - EcPhlConseq.t_hoareS_conseq_nm - (hs_pr hs) - { hsi_m = (fst hs.hs_m); hsi_inv = POE.empty f_true; } - in - let tt2 = EcPhlAuto.t_pl_trivial in - FApi.t_seqs [tt1; tt2; t_fail] tc - in - - FApi.t_last - (FApi.t_try (t_intros_s_seq (`Symbol ["_"; "_"]) tactic)) - (t_bdhoare_seq_r_low i info tc) - -let t_bdhoare_seq = FApi.t_low2 "bdhoare-seq" t_bdhoare_seq_r - -(* -------------------------------------------------------------------- *) -let t_equiv_seq (i, j) phi tc = - let env = FApi.tc1_env tc in - let es = tc1_as_equivS tc in - let sl1,sl2 = s_split env i es.es_sl in - let sr1,sr2 = s_split env j es.es_sr in - let mtl, mtr = snd es.es_ml, snd es.es_mr in - let a = f_equivS mtl mtr (es_pr es) (stmt sl1) (stmt sr1) phi in - let b = f_equivS mtl mtr phi (stmt sl2) (stmt sr2) (es_po es) in - - FApi.xmutate1 tc `HlApp [a; b] - -let t_equiv_seq_onesided side i pre post 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 s, _s', p', q' = - match side with - | `Left -> - let p' = ss_inv_generalize_as_left pre ml mr in - let q' = ss_inv_generalize_as_left post ml mr in - es.es_sl, es.es_sr, p', q' - | `Right -> - let p' = ss_inv_generalize_as_right pre ml mr in - let q' = ss_inv_generalize_as_right post ml mr in - es.es_sr, es.es_sl, p', q' - in - let generalize_mod_side= sideif side generalize_mod_left generalize_mod_right in - let ij = - match side with - | `Left -> (i, EcMatching.Position.codegap1_end) - | `Right -> (EcMatching.Position.codegap1_end, i) in - let _s1, s2 = s_split env i s in - - let modi = EcPV.s_write env (EcModules.stmt s2) in - let r = map_ts_inv2 f_and p' (generalize_mod_side env modi (map_ts_inv2 f_imp q' (es_po es))) in - FApi.t_seqsub (t_equiv_seq ij r) - [t_id; (* s1 ~ s' : pr ==> r *) - FApi.t_seqsub (EcPhlConseq.t_equivS_conseq_nm p' q') - [(* r => forall mod, post => post' *) t_trivial; - (* r => p' *) t_trivial; - (* s1 ~ [] : p' ==> q' *) EcPhlConseq.t_equivS_conseq_bd side pre post - ] - ] tc - -(* -------------------------------------------------------------------- *) -let process_phl_bd_info bd_info tc = - match bd_info with - | PSeqNone -> - let hs = tc1_as_bdhoareS tc in - let m = fst hs.bhs_m in - let f1, f2 = bhs_bd hs, {m;inv=f_r1} in - (* The last argument will not be used *) - ({m;inv=f_true}, f1, f2, {m;inv=f_r0}, {m;inv=f_r1}) - - | PSeqSingle f -> - let hs = tc1_as_bdhoareS tc in - let m = fst hs.bhs_m in - let f = snd (TTC.tc1_process_Xhl_form tc treal f) in - let f1, f2 = (map_ss_inv2 f_real_div (bhs_bd hs) f, f) in - ({m;inv=f_true}, f1, f2, {m;inv=f_r0}, {m;inv=f_r1}) - - | PSeqMult (phi, f1, f2, g1, g2) -> - let hs = tc1_as_bdhoareS tc in - let m = fst hs.bhs_m in - let phi = - phi |> omap (fun f -> snd (TTC.tc1_process_Xhl_formula tc f)) - |> odfl {m;inv=f_true} in - - let check_0 f = - if not (f_equal f f_r0) then - tc_error !!tc "the formula must be 0%%r" in - - let process_f (f1,f2) = - match f1, f2 with - | None, None -> assert false - - | Some fp, None -> - let _, f = TTC.tc1_process_Xhl_form tc treal fp in - reloc fp.pl_loc check_0 f.inv; (f, {m;inv=f_r1}) - - | None, Some fp -> - let _, f = TTC.tc1_process_Xhl_form tc treal fp in - reloc fp.pl_loc check_0 f.inv; ({m;inv=f_r1}, f) - - | Some f1, Some f2 -> - let _, f1 = TTC.tc1_process_Xhl_form tc treal f1 in - let _, f2 = TTC.tc1_process_Xhl_form tc treal f2 in - (f1, f2) - in - - let f1, f2 = process_f (f1, f2) in - let g1, g2 = process_f (g1, g2) in - - (phi, f1, f2, g1, g2) - -(* -------------------------------------------------------------------- *) -let process_seq ((side, k, phi, bd_info) : seq_info) (tc : tcenv1) = - let concl = FApi.tc1_goal tc in - - let get_single phi = - match phi with - | Single phi -> phi - | Double _ -> tc_error !!tc "seq: a single formula is expected" in - - let check_side side = - if EcUtils.is_some side then - tc_error !!tc "seq: no side information expected" in - - match k, bd_info with - | Single i, PSeqNone when is_hoareS concl -> - check_side side; - let _, phi = TTC.tc1_process_Xhl_formula tc (get_single phi) in - let i = EcLowPhlGoal.tc1_process_codegap1 tc (side, i) in - t_hoare_seq i phi tc - - | Single i, PSeqNone when is_eHoareS concl -> - check_side side; - let _, phi = TTC.tc1_process_Xhl_formula_xreal tc (get_single phi) in - let i = EcLowPhlGoal.tc1_process_codegap1 tc (side, i) in - t_ehoare_seq i phi tc - - | Single i, PSeqNone when is_equivS concl -> - let pre, post = - match phi with - | Single _ -> tc_error !!tc "seq onsided: a pre and a post is expected" - | Double (pre, post) -> - let _, pre = TTC.tc1_process_Xhl_formula ?side tc pre in - let _, post = TTC.tc1_process_Xhl_formula ?side tc post in - (pre, post) in - let side = - match side with - | None -> tc_error !!tc "seq onsided: side information expected" - | Some side -> side in - let i = EcLowPhlGoal.tc1_process_codegap1 tc (Some side, i) in - t_equiv_seq_onesided side i pre post tc - - | Single i, _ when is_bdHoareS concl -> - check_side side; - let _, pia = TTC.tc1_process_Xhl_formula tc (get_single phi) in - let (ra, f1, f2, f3, f4) = process_phl_bd_info bd_info tc in - let i = EcLowPhlGoal.tc1_process_codegap1 tc (side, i) in - t_bdhoare_seq i (ra, pia, f1, f2, f3, f4) tc - - | Double (i, j), PSeqNone when is_equivS concl -> - check_side side; - let phi = TTC.tc1_process_prhl_formula tc (get_single phi) in - let i = EcLowPhlGoal.tc1_process_codegap1 tc (Some `Left, i) in - let j = EcLowPhlGoal.tc1_process_codegap1 tc (Some `Left, j) in - t_equiv_seq (i, j) phi tc - - | Single _, PSeqNone - | Double _, PSeqNone -> - tc_error !!tc "invalid `position' parameter" - - | _, _ -> - tc_error !!tc "optional bound parameter not supported" +(* Dispatch on the goal kind only; each logic owns its surface-syntax + handling and takes the whole [seq_info] record. *) +let process_seq (info : seq_info) (tc : tcenv1) = + match (FApi.tc1_goal tc).f_node with + | FhoareS _ -> EcHoareSeq.process_hoare_seq info tc + | FeHoareS _ -> EcEHoareSeq.process_ehoare_seq info tc + | FbdHoareS _ -> EcBdHoareSeq.process_bdhoare_seq info tc + | FequivS _ -> EcEquivSeq.process_equiv_seq info tc + | _ -> + match info.seqi_bd with + | PSeqNone -> tc_error !!tc "invalid `position' parameter" + | _ -> tc_error !!tc "optional bound parameter not supported" diff --git a/src/phl/rules/bdhoare/ecBdHoareSeq.ml b/src/phl/rules/bdhoare/ecBdHoareSeq.ml new file mode 100644 index 000000000..f9bb7e886 --- /dev/null +++ b/src/phl/rules/bdhoare/ecBdHoareSeq.ml @@ -0,0 +1,232 @@ +(* -------------------------------------------------------------------- *) +open EcUtils +open EcLocation +open EcParsetree +open EcTypes +open EcFol +open EcAst +open EcSubst + +open EcCoreGoal +open EcLowGoal +open EcLowPhlGoal + +module TTC = EcProofTyping + +(* -------------------------------------------------------------------- *) +(* Parameters of the bdhoare [seq] rule as supplied by the caller: high level, + the split position is still a symbolic code gap that must be resolved. + + The prefix [s1] is split on the event [r]: with probability bounded by + [f1] (resp. [g1]) it ends in [r] (resp. [!r]), and from there the suffix + [s2] reaches the post with probability bounded by [f2] (resp. [g2]); + [phi] is an invariant established by [s1]. *) +type bdhoare_seq_rule = { + bsr_at : EcMatching.Position.codegap1; (* split position *) + bsr_phi : ss_inv; (* invariant after the prefix *) + bsr_r : ss_inv; (* event splitting the prefix *) + bsr_f1 : ss_inv; (* bound for [r] after the prefix *) + bsr_f2 : ss_inv; (* bound for the suffix from [r] *) + bsr_g1 : ss_inv; (* bound for [!r] after the prefix *) + bsr_g2 : ss_inv; (* bound for the suffix from [!r] *) +} + +(* Low-level parameters recorded in the proof-node: as [bdhoare_seq_rule], but + the split position is the RESOLVED integer index. *) +type bdhoare_seq_node = { + bsn_at : EcMatching.Position.nm_codegap1; (* resolved split index *) + bsn_phi : ss_inv; + bsn_r : ss_inv; + bsn_f1 : ss_inv; + bsn_f2 : ss_inv; + bsn_g1 : ss_inv; + bsn_g2 : ss_inv; +} + +type EcCoreGoal.rule += RBdHoareSeq of bdhoare_seq_node + +(* -------------------------------------------------------------------- *) +(* Pure low-level core shared by the rule and its checker. Needs no + environment — code resolution happened upstream, in the rule. The + subgoals for a branch whose prefix bound ([f1] / [g1]) or suffix bound + ([f2] / [g2]) is syntactically [0%r] are omitted. The two reals bound in + the non-modification subgoal are fresh at each call: the checker compares + up to alpha-conversion. *) +let bdhoare_seq_subgoals (bhs : bdHoareS) (n : bdhoare_seq_node) : form list = + let m = fst bhs.bhs_m in + let phi = ss_inv_rebind n.bsn_phi m in + let pR = ss_inv_rebind n.bsn_r m in + let f1 = ss_inv_rebind n.bsn_f1 m in + let f2 = ss_inv_rebind n.bsn_f2 m in + let g1 = ss_inv_rebind n.bsn_g1 m in + let g2 = ss_inv_rebind n.bsn_g2 m in + let s1, s2 = EcMatching.Position.split_at_nmcgap1 n.bsn_at bhs.bhs_s in + let s1, s2 = stmt s1, stmt s2 in + let nR = map_ss_inv1 f_not pR in + let mt = snd bhs.bhs_m in + let post = POE.lift phi in + let cond_phi = f_hoareS mt (bhs_pr bhs) s1 post in + let condf1 = f_bdHoareS mt (bhs_pr bhs) s1 pR bhs.bhs_cmp f1 in + let condg1 = f_bdHoareS mt (bhs_pr bhs) s1 nR bhs.bhs_cmp g1 in + let condf2 = f_bdHoareS mt (map_ss_inv2 f_and_simpl phi pR) s2 (bhs_po bhs) bhs.bhs_cmp f2 in + let condg2 = f_bdHoareS mt (map_ss_inv2 f_and_simpl phi nR) s2 (bhs_po bhs) bhs.bhs_cmp g2 in + let bd = + (map_ss_inv2 f_real_add_simpl (map_ss_inv2 f_real_mul_simpl f1 f2) (map_ss_inv2 f_real_mul_simpl g1 g2)) in + let condbd = + match bhs.bhs_cmp with + | FHle -> map_ss_inv2 f_real_le bd (bhs_bd bhs) + | FHeq -> map_ss_inv2 f_eq bd (bhs_bd bhs) + | FHge -> map_ss_inv2 f_real_le (bhs_bd bhs) bd in + let condbd = map_ss_inv2 f_imp (bhs_pr bhs) condbd in + let (ir1, ir2) = EcIdent.create "r", EcIdent.create "r" in + let (r1 , r2 ) = f_local ir1 treal, f_local ir2 treal in + let condnm = + let eqs = map_ss_inv2 f_and (map_ss_inv1 ((EcUtils.flip f_eq) r1) f2) + (map_ss_inv1 ((EcUtils.flip f_eq) r2) g2) in + let post = empty_hs eqs in + f_forall + [(ir1, GTty treal); (ir2, GTty treal)] + (f_hoareS (snd bhs.bhs_m) + (map_ss_inv2 f_and (bhs_pr bhs) eqs) s1 post) + in + let conds = [EcSubst.f_forall_mems_ss_inv bhs.bhs_m condbd; condnm] in + let conds = + if f_equal g1.inv f_r0 + then condg1 :: conds + else if f_equal g2.inv f_r0 + then condg2 :: conds + else condg1 :: condg2 :: conds in + + let conds = + if f_equal f1.inv f_r0 + then condf1 :: conds + else if f_equal f2.inv f_r0 + then condf2 :: conds + else condf1 :: condf2 :: conds in + + cond_phi :: conds + +(* -------------------------------------------------------------------- *) +(* Rule (TCB): resolve the code gap to an index (the env-dependent step), + record the resolved node, and build its subgoals through the shared core. + The non-modification subgoal (last) is left open; see [t_bdhoare_seq_full]. *) +let t_bdhoare_seq (r : bdhoare_seq_rule) tc = + let env = FApi.tc1_env tc in + let bhs = tc1_as_bdhoareS tc in + let n = { bsn_at = s_split_index env r.bsr_at bhs.bhs_s; + bsn_phi = r.bsr_phi; + bsn_r = r.bsr_r; + bsn_f1 = r.bsr_f1; + bsn_f2 = r.bsr_f2; + bsn_g1 = r.bsr_g1; + bsn_g2 = r.bsr_g2; } in + FApi.xrule1 tc (RBdHoareSeq n) (bdhoare_seq_subgoals bhs n) + +(* -------------------------------------------------------------------- *) +(* Checker: rerun ONLY the low-level core on the recorded node (see + [EcPlRecheck]). *) +let () = + register_rule_checker + (function + | RBdHoareSeq n -> + Some (EcPlRecheck.checker_of "bdhoare-seq" pf_as_bdhoareS + (fun _hyps bhs -> bdhoare_seq_subgoals bhs n)) + | _ -> None) + +(* -------------------------------------------------------------------- *) +(* Derived (no proof-node): the rule, then a best-effort discharge of its last + (non-modification) subgoal, which holds trivially when the prefix does not + write the bounds [f2] / [g2]. This is what the surface [seq] tactic and the + legacy positional entry (EcPhlSeq.t_bdhoare_seq) use. + + TEMPORARY: depends on the not-yet-migrated [EcPhlConseq]. *) +let t_bdhoare_seq_full (r : bdhoare_seq_rule) tc = + let tactic tc = + let hs = tc1_as_hoareS tc in + let tt1 = + EcPhlConseq.t_hoareS_conseq_nm + (hs_pr hs) + { hsi_m = (fst hs.hs_m); hsi_inv = POE.empty f_true; } + in + let tt2 = EcPhlAuto.t_pl_trivial in + FApi.t_seqs [tt1; tt2; t_fail] tc + in + + FApi.t_last + (FApi.t_try (t_intros_s_seq (`Symbol ["_"; "_"]) tactic)) + (t_bdhoare_seq r tc) + +(* -------------------------------------------------------------------- *) +(* Elaboration of the optional bound information of a bdhoare [seq]. Returns + the invariant [phi] and the bounds [f1], [f2], [g1], [g2]. *) +let process_bd_info (bd_info : p_seq_xt_info) tc = + match bd_info with + | PSeqNone -> + let hs = tc1_as_bdhoareS tc in + let m = fst hs.bhs_m in + let f1, f2 = bhs_bd hs, {m;inv=f_r1} in + (* The last argument will not be used *) + ({m;inv=f_true}, f1, f2, {m;inv=f_r0}, {m;inv=f_r1}) + + | PSeqSingle f -> + let hs = tc1_as_bdhoareS tc in + let m = fst hs.bhs_m in + let f = snd (TTC.tc1_process_Xhl_form tc treal f) in + let f1, f2 = (map_ss_inv2 f_real_div (bhs_bd hs) f, f) in + ({m;inv=f_true}, f1, f2, {m;inv=f_r0}, {m;inv=f_r1}) + + | PSeqMult (phi, f1, f2, g1, g2) -> + let hs = tc1_as_bdhoareS tc in + let m = fst hs.bhs_m in + let phi = + phi |> omap (fun f -> snd (TTC.tc1_process_Xhl_formula tc f)) + |> odfl {m;inv=f_true} in + + let check_0 f = + if not (f_equal f f_r0) then + tc_error !!tc "the formula must be 0%%r" in + + let process_f (f1,f2) = + match f1, f2 with + | None, None -> assert false + + | Some fp, None -> + let _, f = TTC.tc1_process_Xhl_form tc treal fp in + reloc fp.pl_loc check_0 f.inv; (f, {m;inv=f_r1}) + + | None, Some fp -> + let _, f = TTC.tc1_process_Xhl_form tc treal fp in + reloc fp.pl_loc check_0 f.inv; ({m;inv=f_r1}, f) + + | Some f1, Some f2 -> + let _, f1 = TTC.tc1_process_Xhl_form tc treal f1 in + let _, f2 = TTC.tc1_process_Xhl_form tc treal f2 in + (f1, f2) + in + + let f1, f2 = process_f (f1, f2) in + let g1, g2 = process_f (g1, g2) in + + (phi, f1, f2, g1, g2) + +(* -------------------------------------------------------------------- *) +(* Elaboration: the goal is known to be a [bdHoareS]. Validate the seq surface + syntax for that logic (no side, single position and event), type the event, + the bound information and the split position, then apply the rule. *) +let process_bdhoare_seq (info : seq_info) tc = + let i = + match info.seqi_at with + | Single i -> i + | Double _ -> tc_error !!tc "seq: a single position is expected" in + if is_some info.seqi_side then + tc_error !!tc "seq: no side information expected"; + let r = + match info.seqi_mid with + | Single r -> r + | Double _ -> tc_error !!tc "seq: a single formula is expected" in + let _, r = TTC.tc1_process_Xhl_formula tc r in + let (phi, f1, f2, g1, g2) = process_bd_info info.seqi_bd tc in + let i = EcLowPhlGoal.tc1_process_codegap1 tc (info.seqi_side, i) in + t_bdhoare_seq_full + { bsr_at = i; bsr_phi = phi; bsr_r = r; + bsr_f1 = f1; bsr_f2 = f2; bsr_g1 = g1; bsr_g2 = g2; } tc diff --git a/src/phl/rules/bdhoare/ecBdHoareSeq.mli b/src/phl/rules/bdhoare/ecBdHoareSeq.mli new file mode 100644 index 000000000..787228ed0 --- /dev/null +++ b/src/phl/rules/bdhoare/ecBdHoareSeq.mli @@ -0,0 +1,66 @@ +(* -------------------------------------------------------------------- *) +open EcParsetree +open EcCoreGoal.FApi +open EcMatching.Position +open EcAst + +(* ==================================================================== *) +(* Rules (trusted) *) + +type bdhoare_seq_rule = { + bsr_at : codegap1; (* split position k *) + bsr_phi : ss_inv; (* invariant phi established by the prefix *) + bsr_r : ss_inv; (* event R splitting the prefix *) + bsr_f1 : ss_inv; (* bound for reaching R with the prefix *) + bsr_f2 : ss_inv; (* bound for the suffix, from phi /\ R *) + bsr_g1 : ss_inv; (* bound for reaching !R with the prefix *) + bsr_g2 : ss_inv; (* bound for the suffix, from phi /\ !R *) +} + +(* [t_bdhoare_seq { bsr_at = k; bsr_phi = phi; bsr_r = R; + bsr_f1 = f1; bsr_f2 = f2; bsr_g1 = g1; bsr_g2 = g2 }] + — sequence, splitting on the event [R]. With [c = c1; c2], + [c1 = c[0..k)], and [~] the goal's comparison ([<=], [=] or [>=]): + + (H) hoare [c1 : P ==> phi] + (F1) phoare [c1 : P ==> R] ~ f1 + (F2) phoare [c2 : phi /\ R ==> Q] ~ f2 + (G1) phoare [c1 : P ==> !R] ~ g1 + (G2) phoare [c2 : phi /\ !R ==> Q] ~ g2 + (B) forall &m, P => (f1 * f2 + g1 * g2) ~ d + (N) forall r1 r2, hoare [c1 : P /\ f2 = r1 /\ g2 = r2 ==> f2 = r1 /\ g2 = r2] + ------------------------------------------------------------------------ + phoare [c : P ==> Q] ~ d + + (N) states that the prefix does not change the suffix bounds. Of the pair + (F1, F2), only (F1) is kept when [f1] is syntactically [0%r], only (F2) + when [f2] is; likewise for (G1, G2) with [g1], [g2]. Premises, in order: + (H), the kept F's, the kept G's, (B), (N). + + Node: [RBdHoareSeq { bsn_at = k (resolved index); bsn_phi; bsn_r; bsn_f1; + bsn_f2; bsn_g1; bsn_g2 }]. + Checker: "bdhoare-seq". *) +val t_bdhoare_seq : bdhoare_seq_rule -> backward + +(* ==================================================================== *) +(* Derived tactics *) + +(* [t_bdhoare_seq_full r] — [t_bdhoare_seq r], then a best-effort discharge + of (N): introduce [r1 r2], apply the framed consequence (currently + [EcPhlConseq.t_hoareS_conseq_nm]) down to [hoare [c1 : _ ==> true]], and + close everything with [EcPhlAuto.t_pl_trivial] — which succeeds when [c1] + does not write the variables of [f2] / [g2]. Otherwise (N) is left open + unchanged. Emits no node of its own. *) +val t_bdhoare_seq_full : bdhoare_seq_rule -> backward + +(* ==================================================================== *) +(* Elaboration *) + +(* [seq k : R [bound info]] on a [bdHoareS] goal: no side, single position + and event. The optional bound information gives [phi] and the bounds: + - none: phi = true, f1 = d, f2 = 1, g1 = 0, g2 = 1; + - a single [f]: phi = true, f1 = d / f, f2 = f, g1 = 0, g2 = 1; + - [phi f1 f2 g1 g2] (each optional, [_] for a bound defaulting to 1 when + the other one of its pair is given as 0). + Applies [t_bdhoare_seq_full]. *) +val process_bdhoare_seq : seq_info -> backward diff --git a/src/phl/rules/ehoare/ecEHoareSeq.ml b/src/phl/rules/ehoare/ecEHoareSeq.ml new file mode 100644 index 000000000..d5cfd0e4d --- /dev/null +++ b/src/phl/rules/ehoare/ecEHoareSeq.ml @@ -0,0 +1,85 @@ +(* -------------------------------------------------------------------- *) +open EcUtils +open EcParsetree +open EcFol +open EcAst +open EcSubst + +open EcCoreGoal +open EcLowPhlGoal + +module TTC = EcProofTyping + +(* -------------------------------------------------------------------- *) +(* Parameters of the ehoare [seq] rule as supplied by the caller: high level, + the split position is still a symbolic code gap that must be resolved. *) +type ehoare_seq_rule = { + ehsr_at : EcMatching.Position.codegap1; (* split position *) + ehsr_mid : ss_inv; (* intermediate assertion *) +} + +(* Low-level parameters recorded in the proof-node: the split position is the + RESOLVED integer index. The checker recomputes the subgoals from this, so it + never redoes code resolution. *) +type ehoare_seq_node = { + ehsn_at : EcMatching.Position.nm_codegap1; (* resolved split index *) + ehsn_mid : ss_inv; (* intermediate assertion *) +} + +type EcCoreGoal.rule += REHoareSeq of ehoare_seq_node + +(* -------------------------------------------------------------------- *) +(* Pure low-level core shared by the rule and its checker: split the statement + at the already-resolved index and build the pre/mid and mid/post subgoals. + Needs no environment — code resolution happened upstream, in the rule. *) +let ehoare_seq_subgoals (hs : eHoareS) (n : ehoare_seq_node) : form list = + let phi = ss_inv_rebind n.ehsn_mid (fst hs.ehs_m) in + let s1, s2 = EcMatching.Position.split_at_nmcgap1 n.ehsn_at hs.ehs_s in + let a = f_eHoareS (snd hs.ehs_m) (ehs_pr hs) (stmt s1) phi in + let b = f_eHoareS (snd hs.ehs_m) phi (stmt s2) (ehs_po hs) in + [a; b] + +(* -------------------------------------------------------------------- *) +(* Rule (TCB): resolve the code gap to an index (the env-dependent step), record + the resolved node, and build its subgoals through the shared core. The + canonical rule takes the high-level record; the legacy positional interface + (EcPhlSeq.t_ehoare_seq) adapts onto it. *) +let t_ehoare_seq (r : ehoare_seq_rule) tc = + let env = FApi.tc1_env tc in + let hs = tc1_as_ehoareS tc in + let n = { ehsn_at = s_split_index env r.ehsr_at hs.ehs_s; + ehsn_mid = r.ehsr_mid; } in + FApi.xrule1 tc (REHoareSeq n) (ehoare_seq_subgoals hs n) + +(* -------------------------------------------------------------------- *) +(* Checker: rerun ONLY the low-level core on the recorded index (see + [EcPlRecheck]). *) +let () = + register_rule_checker + (function + | REHoareSeq n -> + Some (EcPlRecheck.checker_of "ehoare-seq" pf_as_ehoareS + (fun _hyps hs -> ehoare_seq_subgoals hs n)) + | _ -> None) + +(* -------------------------------------------------------------------- *) +(* Elaboration: the goal is known to be an [eHoareS]. Validate the seq surface + syntax for that logic (no side, no bound, single position and assertion), + type the assertion and the split position, then apply the rule. *) +let process_ehoare_seq (info : seq_info) tc = + if is_some info.seqi_side then + tc_error !!tc "seq: no side information expected"; + begin match info.seqi_bd with + | PSeqNone -> () + | _ -> tc_error !!tc "seq: no bound information expected" end; + let i = + match info.seqi_at with + | Single i -> i + | Double _ -> tc_error !!tc "seq: a single position is expected" in + let phi = + match info.seqi_mid with + | Single phi -> phi + | Double _ -> tc_error !!tc "seq: a single formula is expected" in + let _, phi = TTC.tc1_process_Xhl_formula_xreal tc phi in + let i = EcLowPhlGoal.tc1_process_codegap1 tc (info.seqi_side, i) in + t_ehoare_seq { ehsr_at = i; ehsr_mid = phi } tc diff --git a/src/phl/rules/ehoare/ecEHoareSeq.mli b/src/phl/rules/ehoare/ecEHoareSeq.mli new file mode 100644 index 000000000..ebaab2ce5 --- /dev/null +++ b/src/phl/rules/ehoare/ecEHoareSeq.mli @@ -0,0 +1,30 @@ +(* -------------------------------------------------------------------- *) +open EcParsetree +open EcCoreGoal.FApi +open EcMatching.Position +open EcAst + +(* ==================================================================== *) +(* Rules (trusted) *) + +type ehoare_seq_rule = { + ehsr_at : codegap1; (* split position k *) + ehsr_mid : ss_inv; (* intermediate expectation R *) +} + +(* [t_ehoare_seq { ehsr_at = k; ehsr_mid = R }] — sequence: + + ehoare [c1 : P ==> R] ehoare [c2 : R ==> Q] + -------------------------------------------------- c = c1; c2 + ehoare [c : P ==> Q] (c1 = c[0..k)) + + Node: [REHoareSeq { ehsn_at = k (resolved index); ehsn_mid = R }]. + Checker: "ehoare-seq". *) +val t_ehoare_seq : ehoare_seq_rule -> backward + +(* ==================================================================== *) +(* Elaboration *) + +(* [seq k : R] on an [eHoareS] goal: no side, no bound information, a single + position and a single (xreal) expectation. Applies [t_ehoare_seq]. *) +val process_ehoare_seq : seq_info -> backward diff --git a/src/phl/rules/equiv/ecEquivSeq.ml b/src/phl/rules/equiv/ecEquivSeq.ml new file mode 100644 index 000000000..fda89a500 --- /dev/null +++ b/src/phl/rules/equiv/ecEquivSeq.ml @@ -0,0 +1,146 @@ +(* -------------------------------------------------------------------- *) +open EcUtils +open EcParsetree +open EcFol +open EcAst +open EcSubst + +open EcCoreGoal +open EcLowGoal +open EcLowPhlGoal + +module TTC = EcProofTyping + +(* -------------------------------------------------------------------- *) +(* Parameters of the equiv [seq] rule as supplied by the caller: high level, + the split positions (left, right) are still symbolic code gaps. *) +type equiv_seq_rule = { + esr_at : EcMatching.Position.codegap1 pair; (* split positions *) + esr_mid : ts_inv; (* intermediate relation *) +} + +(* Low-level parameters recorded in the proof-node: the split positions are + the RESOLVED integer indices. *) +type equiv_seq_node = { + esn_at : EcMatching.Position.nm_codegap1 pair; (* resolved split indices *) + esn_mid : ts_inv; (* intermediate relation *) +} + +type EcCoreGoal.rule += REquivSeq of equiv_seq_node + +(* -------------------------------------------------------------------- *) +(* Pure low-level core shared by the rule and its checker: split both + statements at the already-resolved indices and build the pre/mid and + mid/post subgoals. Needs no environment. *) +let equiv_seq_subgoals (es : equivS) (n : equiv_seq_node) : form list = + let il, ir = n.esn_at in + let sl1, sl2 = EcMatching.Position.split_at_nmcgap1 il es.es_sl in + let sr1, sr2 = EcMatching.Position.split_at_nmcgap1 ir es.es_sr in + let mtl, mtr = snd es.es_ml, snd es.es_mr in + let a = f_equivS mtl mtr (es_pr es) (stmt sl1) (stmt sr1) n.esn_mid in + let b = f_equivS mtl mtr n.esn_mid (stmt sl2) (stmt sr2) (es_po es) in + [a; b] + +(* -------------------------------------------------------------------- *) +(* Rule (TCB): resolve both code gaps to indices (the env-dependent step), + record the resolved node, and build its subgoals through the shared core. + The legacy positional interface (EcPhlSeq.t_equiv_seq) adapts onto it. *) +let t_equiv_seq (r : equiv_seq_rule) tc = + let env = FApi.tc1_env tc in + let es = tc1_as_equivS tc in + let gl, gr = r.esr_at in + let n = { esn_at = (s_split_index env gl es.es_sl, + s_split_index env gr es.es_sr); + esn_mid = r.esr_mid; } in + FApi.xrule1 tc (REquivSeq n) (equiv_seq_subgoals es n) + +(* -------------------------------------------------------------------- *) +(* Checker: rerun ONLY the low-level core on the recorded indices (see + [EcPlRecheck]). *) +let () = + register_rule_checker + (function + | REquivSeq n -> + Some (EcPlRecheck.checker_of "equiv-seq" pf_as_equivS + (fun _hyps es -> equiv_seq_subgoals es n)) + | _ -> None) + +(* -------------------------------------------------------------------- *) +(* One-sided [seq] (derived, no proof-node): split one side only, at [i], + with the one-sided intermediate assertions [pre] / [post]. Expands to the + two-sided rule (the other side split at its end) followed by [conseq] + steps that discharge the one-sided part. + + TEMPORARY: depends on the not-yet-migrated [EcPhlConseq]. *) +let t_equiv_seq_onesided side i pre post 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 s, p', q' = + match side with + | `Left -> + let p' = ss_inv_generalize_as_left pre ml mr in + let q' = ss_inv_generalize_as_left post ml mr in + es.es_sl, p', q' + | `Right -> + let p' = ss_inv_generalize_as_right pre ml mr in + let q' = ss_inv_generalize_as_right post ml mr in + es.es_sr, p', q' + in + let generalize_mod_side = sideif side generalize_mod_left generalize_mod_right in + let ij = + match side with + | `Left -> (i, EcMatching.Position.codegap1_end) + | `Right -> (EcMatching.Position.codegap1_end, i) in + let _s1, s2 = s_split env i s in + + let modi = EcPV.s_write env (EcModules.stmt s2) in + let r = map_ts_inv2 f_and p' (generalize_mod_side env modi (map_ts_inv2 f_imp q' (es_po es))) in + FApi.t_seqsub (t_equiv_seq { esr_at = ij; esr_mid = r }) + [t_id; (* s1 ~ s' : pr ==> r *) + FApi.t_seqsub (EcPhlConseq.t_equivS_conseq_nm p' q') + [(* r => forall mod, post => post' *) t_trivial; + (* r => p' *) t_trivial; + (* s1 ~ [] : p' ==> q' *) EcPhlConseq.t_equivS_conseq_bd side pre post + ] + ] tc + +(* -------------------------------------------------------------------- *) +(* Elaboration: the goal is known to be an [equivS]. A single position is the + one-sided form (side required, pre and post assertions); a pair of + positions is the two-sided form (no side, single relation). *) +let process_equiv_seq (info : seq_info) tc = + begin match info.seqi_bd with + | PSeqNone -> () + | _ -> tc_error !!tc "optional bound parameter not supported" end; + + match info.seqi_at with + | Single i -> + let side = + match info.seqi_side with + | None -> tc_error !!tc "seq onsided: side information expected" + | Some side -> side in + let pre, post = + match info.seqi_mid with + | Single _ -> tc_error !!tc "seq onsided: a pre and a post is expected" + | Double (pre, post) -> + let _, pre = TTC.tc1_process_Xhl_formula ~side tc pre in + let _, post = TTC.tc1_process_Xhl_formula ~side tc post in + (pre, post) in + let i = EcLowPhlGoal.tc1_process_codegap1 tc (Some side, i) in + t_equiv_seq_onesided side i pre post tc + + | Double (i, j) -> + if is_some info.seqi_side then + tc_error !!tc "seq: no side information expected"; + let phi = + match info.seqi_mid with + | Single phi -> phi + | Double _ -> tc_error !!tc "seq: a single formula is expected" in + let phi = TTC.tc1_process_prhl_formula tc phi in + (* NB: both positions are typed in the left memory, as before the + migration (behaviour preserved; the right one should probably use + the right memory). *) + let i = EcLowPhlGoal.tc1_process_codegap1 tc (Some `Left, i) in + let j = EcLowPhlGoal.tc1_process_codegap1 tc (Some `Left, j) in + t_equiv_seq { esr_at = (i, j); esr_mid = phi } tc diff --git a/src/phl/rules/equiv/ecEquivSeq.mli b/src/phl/rules/equiv/ecEquivSeq.mli new file mode 100644 index 000000000..acbe7d0bd --- /dev/null +++ b/src/phl/rules/equiv/ecEquivSeq.mli @@ -0,0 +1,55 @@ +(* -------------------------------------------------------------------- *) +open EcUtils +open EcParsetree +open EcCoreGoal.FApi +open EcMatching.Position +open EcAst + +(* ==================================================================== *) +(* Rules (trusted) *) + +type equiv_seq_rule = { + esr_at : codegap1 pair; (* split positions (k, k') *) + esr_mid : ts_inv; (* intermediate relation R *) +} + +(* [t_equiv_seq { esr_at = (k, k'); esr_mid = R }] — sequence: + + equiv [c1 ~ c1' : P ==> R] equiv [c2 ~ c2' : R ==> Q] + ------------------------------------------------------------ c = c1; c2 (c1 = c [0..k )) + equiv [c ~ c' : P ==> Q] c' = c1'; c2' (c1' = c'[0..k')) + + Node: [REquivSeq { esn_at = (k, k') (resolved indices); esn_mid = R }]. + Checker: "equiv-seq". *) +val t_equiv_seq : equiv_seq_rule -> backward + +(* ==================================================================== *) +(* Derived tactics *) + +(* [t_equiv_seq_onesided `Left k pre post] — one-sided sequence on the goal + [equiv [c1; c2 ~ c' : P ==> Q]], with [c1 = c[0..k)] (symmetrically for + [`Right]). Expands to: + + 1. [t_equiv_seq] at [(k, end)], with the relation + R := pre<1> /\ forall (mod c2)<1>, post<1> => Q + giving (a) equiv [c1 ~ c' : P ==> R] — left open, + (b) equiv [c2 ~ skip : R ==> Q]; + 2. on (b), the framed consequence (currently [EcPhlConseq.t_equivS_conseq_nm]) + to [equiv [c2 ~ skip : pre<1> ==> post<1>]]; its side conditions + [R => pre<1>] and [R => forall (mod c2)<1>, post<1> => Q] are closed + by [t_trivial]; + 3. then [EcPhlConseq.t_equivS_conseq_bd] to + (c) phoare [c2 : pre ==> post] = 1%r — left open. + + Visible goals: (a) and (c). Emits no node of its own. *) +val t_equiv_seq_onesided : side -> codegap1 -> ss_inv -> ss_inv -> backward + +(* ==================================================================== *) +(* Elaboration *) + +(* On an [equivS] goal, no bound information: + - [seq k k' : R] (no side, single relation): applies [t_equiv_seq]; both + positions are typed in the left memory (behaviour preserved); + - [seq{i} k : (pre ==> post)] (side required): applies + [t_equiv_seq_onesided]. *) +val process_equiv_seq : seq_info -> backward diff --git a/src/phl/rules/hoare/ecHoareSeq.ml b/src/phl/rules/hoare/ecHoareSeq.ml new file mode 100644 index 000000000..b18d24426 --- /dev/null +++ b/src/phl/rules/hoare/ecHoareSeq.ml @@ -0,0 +1,87 @@ +(* -------------------------------------------------------------------- *) +open EcUtils +open EcParsetree +open EcFol +open EcAst +open EcSubst + +open EcCoreGoal +open EcLowPhlGoal + +module TTC = EcProofTyping + +(* -------------------------------------------------------------------- *) +(* Parameters of the hoare [seq] rule as supplied by the caller: high level, the + split position is still a symbolic code gap that must be resolved. *) +type hoare_seq_rule = { + hsr_at : EcMatching.Position.codegap1; (* split position *) + hsr_mid : ss_inv; (* intermediate assertion *) +} + +(* Low-level parameters recorded in the proof-node: the split position is the + RESOLVED integer index. The checker recomputes the subgoals from this, so it + never redoes code resolution. *) +type hoare_seq_node = { + hsn_at : EcMatching.Position.nm_codegap1; (* resolved split index *) + hsn_mid : ss_inv; (* intermediate assertion *) +} + +type EcCoreGoal.rule += RHoareSeq of hoare_seq_node + +(* -------------------------------------------------------------------- *) +(* Pure low-level core shared by the rule and its checker: split the statement + at the already-resolved index and build the pre/mid and mid/post subgoals. + Needs no environment — code resolution happened upstream, in the rule. *) +let hoare_seq_subgoals (hs : sHoareS) (n : hoare_seq_node) : form list = + let phi = ss_inv_rebind n.hsn_mid (fst hs.hs_m) in + let s1, s2 = EcMatching.Position.split_at_nmcgap1 n.hsn_at hs.hs_s in + let post = update_hs_ss phi (hs_po hs) in + let a = f_hoareS (snd hs.hs_m) (hs_pr hs) (stmt s1) post in + let b = f_hoareS (snd hs.hs_m) phi (stmt s2) (hs_po hs) in + [a; b] + +(* -------------------------------------------------------------------- *) +(* Rule (TCB): resolve the code gap to an index (the env-dependent step), record + the resolved node, and build its subgoals through the shared core. The + canonical rule takes the high-level record; the legacy positional interface + (EcPhlSeq.t_hoare_seq) adapts onto it. *) +let t_hoare_seq (r : hoare_seq_rule) tc = + let env = FApi.tc1_env tc in + let hs = tc1_as_hoareS tc in + let n = { hsn_at = s_split_index env r.hsr_at hs.hs_s; + hsn_mid = r.hsr_mid; } in + FApi.xrule1 tc (RHoareSeq n) (hoare_seq_subgoals hs n) + +(* -------------------------------------------------------------------- *) +(* Checker: rerun ONLY the low-level core on the recorded index (see + [EcPlRecheck]). It never redoes code resolution, so [normalize_cgap1] stays + out of its trust boundary. *) +let () = + register_rule_checker + (function + | RHoareSeq n -> + Some (EcPlRecheck.checker_of "hoare-seq" pf_as_hoareS + (fun _hyps hs -> hoare_seq_subgoals hs n)) + | _ -> None) + +(* -------------------------------------------------------------------- *) +(* Elaboration: the goal is known to be a [hoareS]. Validate the seq surface + syntax for that logic (no side, no bound, single position and assertion), + type the assertion and the split position, then apply the rule. *) +let process_hoare_seq (info : seq_info) tc = + if is_some info.seqi_side then + tc_error !!tc "seq: no side information expected"; + begin match info.seqi_bd with + | PSeqNone -> () + | _ -> tc_error !!tc "seq: no bound information expected" end; + let i = + match info.seqi_at with + | Single i -> i + | Double _ -> tc_error !!tc "seq: a single position is expected" in + let phi = + match info.seqi_mid with + | Single phi -> phi + | Double _ -> tc_error !!tc "seq: a single formula is expected" in + let _, phi = TTC.tc1_process_Xhl_formula tc phi in + let i = EcLowPhlGoal.tc1_process_codegap1 tc (info.seqi_side, i) in + t_hoare_seq { hsr_at = i; hsr_mid = phi } tc diff --git a/src/phl/rules/hoare/ecHoareSeq.mli b/src/phl/rules/hoare/ecHoareSeq.mli new file mode 100644 index 000000000..66c23d3be --- /dev/null +++ b/src/phl/rules/hoare/ecHoareSeq.mli @@ -0,0 +1,33 @@ +(* -------------------------------------------------------------------- *) +open EcParsetree +open EcCoreGoal.FApi +open EcMatching.Position +open EcAst + +(* ==================================================================== *) +(* Rules (trusted) *) + +type hoare_seq_rule = { + hsr_at : codegap1; (* split position k *) + hsr_mid : ss_inv; (* intermediate assertion R *) +} + +(* [t_hoare_seq { hsr_at = k; hsr_mid = R }] — sequence: + + hoare [c1 : P ==> R | E] hoare [c2 : R ==> Q | E] + ---------------------------------------------------------- c = c1; c2 + hoare [c : P ==> Q | E] (c1 = c[0..k)) + + where [E] are the exceptional postconditions of the goal, kept unchanged + in both premises. + + Node: [RHoareSeq { hsn_at = k (resolved index); hsn_mid = R }]. + Checker: "hoare-seq". *) +val t_hoare_seq : hoare_seq_rule -> backward + +(* ==================================================================== *) +(* Elaboration *) + +(* [seq k : R] on a [hoareS] goal: no side, no bound information, a single + position and a single assertion. Applies [t_hoare_seq]. *) +val process_hoare_seq : seq_info -> backward diff --git a/tests/seq-bdhoare.ec b/tests/seq-bdhoare.ec new file mode 100644 index 000000000..fb5f9a0cb --- /dev/null +++ b/tests/seq-bdhoare.ec @@ -0,0 +1,41 @@ +require import AllCore Distr DBool. + +module M = { + proc f() : bool = { + var x, y; + x <- true; + y <$ {0,1}; + return x /\ y; + } +}. + +(* No bound information. *) +lemma no_bound : phoare [M.f : true ==> true] = 1%r. +proof. +proc. +seq 1 : (x = true). ++ by wp. ++ by wp; skip. ++ by rnd; skip => />; apply: dbool_ll. ++ by hoare; wp; skip. +by trivial. +qed. + +(* Explicit bounds, with the [!r] branch of the prefix bounded by 0: the + corresponding suffix subgoal is omitted. *) +lemma mult_bounds : phoare [M.f : true ==> true] = 1%r. +proof. +proc. +seq 1 : (x = true) 1%r 1%r 0%r _ (true) => //. ++ by wp. ++ by rnd; skip => />; apply: dbool_ll. +by hoare; wp; skip. +qed. + +lemma errors : phoare [M.f : true ==> true] = 1%r. +proof. +proc. +fail seq 1 1 : (x = true). +fail seq{1} 1 : (x = true). +fail seq 1 : (_: true ==> true). +abort. diff --git a/tests/seq-ehoare.ec b/tests/seq-ehoare.ec new file mode 100644 index 000000000..1dfc99862 --- /dev/null +++ b/tests/seq-ehoare.ec @@ -0,0 +1,25 @@ +require import AllCore Xreal. + +module M = { + proc f() : int = { + var x; + x <- 1; + x <- x + 1; + return x; + } +}. + +lemma L : ehoare [M.f : (1%xr) ==> (1%xr)]. +proof. +proc. +seq 1 : (1%xr). ++ by wp; skip. +by wp; skip. +qed. + +lemma Lerr1 : ehoare [M.f : (1%xr) ==> (1%xr)]. +proof. +proc. +fail seq 1 1 : (1%xr). +fail seq 1 : (1%xr) (1%xr). +abort. diff --git a/tests/seq-equiv.ec b/tests/seq-equiv.ec new file mode 100644 index 000000000..84f9e37bf --- /dev/null +++ b/tests/seq-equiv.ec @@ -0,0 +1,39 @@ +require import AllCore. + +module M = { + proc f() : int = { + var x; + x <- 1; + x <- x + 1; + return x; + } +}. + +lemma two_sided : equiv [M.f ~ M.f : true ==> ={res}]. +proof. +proc. +seq 1 1 : (={x} /\ x{1} = 1). ++ by wp; skip. +by wp; skip. +qed. + +lemma one_sided_left : equiv [M.f ~ M.f : true ==> res{1} = 2 /\ res{2} = 2]. +proof. +proc. +seq{1} 1 : (_: x = 1 ==> x = 2); auto. +qed. + +lemma one_sided_right : equiv [M.f ~ M.f : true ==> res{1} = 2 /\ res{2} = 2]. +proof. +proc. +seq{2} 1 : (_: x = 1 ==> x = 2); auto. +qed. + +lemma errors : equiv [M.f ~ M.f : true ==> ={res}]. +proof. +proc. +fail seq 1 : (true). +fail seq{1} 1 : (true). +fail seq{1} 1 1 : (true). +fail seq 1 1 : (_: true ==> true). +abort.