From 52b98039e9622a7d627ba80016bcba8e2426d791 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Tue, 6 Oct 2026 17:38:24 +0200 Subject: [PATCH] refactor(pl): seq as recheckable per-logic rules Second PR of the program-logic reorganization stack (see src/phl/REFACTORING.md), on top of the recheckable proof-node basis. It migrates the whole `seq` tactic class: - rules/hoare/ecHoareSeq.ml, rules/ehoare/ecEHoareSeq.ml, rules/bdhoare/ecBdHoareSeq.ml, rules/equiv/ecEquivSeq.ml: one module per logic, each with a rule-arguments record, a node record holding the resolved data (split indices, typed assertions and bounds), a pure subgoal builder shared by the rule and its registered checker, and an elaboration entry taking the parse-tree seq_info. Code positions are resolved once in the rule (s_split_index), so the checker never redoes code resolution. - The one-sided equiv form is derived (two-sided rule + conseq) and lives in ecEquivSeq.ml without a node of its own. The bdhoare rule leaves its non-modification subgoal open; the derived t_bdhoare_seq_full used by the tactic then tries to discharge it. Both derived forms temporarily depend on the unmigrated EcPhlConseq. - The seq parse info becomes a record (seq_info); EcPhlSeq is reduced to the logic-agnostic dispatcher and the legacy positional adapters, so its interface and external callers are unchanged. The no-op FApi.t_low* wrappers are dropped. - Each module's .mli documents its trusted rule as an inference rule (premises, conclusion, side conditions, node, checker), separately from its derived tactics (with what they expand to) and its elaboration entry point. Behaviour is preserved, except that malformed ehoare / bdhoare seq now report the same error messages as hoare. Two-sided equiv seq still types its right position in the left memory (flagged in a comment). New tests tests/seq-{ehoare,equiv,bdhoare}.ec exercise the rules directly. The stdlib and the unit tests pass under EC_RECHECK=1 with no RecheckFailure; for each logic, a deliberately wrong checker is caught only under EC_RECHECK. --- src/ecLowPhlGoal.ml | 8 + src/ecParser.mly | 2 +- src/ecParsetree.ml | 8 +- src/phl/ecPhlSeq.ml | 292 +++---------------------- src/phl/rules/bdhoare/ecBdHoareSeq.ml | 232 ++++++++++++++++++++ src/phl/rules/bdhoare/ecBdHoareSeq.mli | 66 ++++++ src/phl/rules/ehoare/ecEHoareSeq.ml | 85 +++++++ src/phl/rules/ehoare/ecEHoareSeq.mli | 30 +++ src/phl/rules/equiv/ecEquivSeq.ml | 146 +++++++++++++ src/phl/rules/equiv/ecEquivSeq.mli | 55 +++++ src/phl/rules/hoare/ecHoareSeq.ml | 87 ++++++++ src/phl/rules/hoare/ecHoareSeq.mli | 33 +++ tests/seq-bdhoare.ec | 41 ++++ tests/seq-ehoare.ec | 25 +++ tests/seq-equiv.ec | 39 ++++ 15 files changed, 884 insertions(+), 265 deletions(-) create mode 100644 src/phl/rules/bdhoare/ecBdHoareSeq.ml create mode 100644 src/phl/rules/bdhoare/ecBdHoareSeq.mli create mode 100644 src/phl/rules/ehoare/ecEHoareSeq.ml create mode 100644 src/phl/rules/ehoare/ecEHoareSeq.mli create mode 100644 src/phl/rules/equiv/ecEquivSeq.ml create mode 100644 src/phl/rules/equiv/ecEquivSeq.mli create mode 100644 src/phl/rules/hoare/ecHoareSeq.ml create mode 100644 src/phl/rules/hoare/ecHoareSeq.mli create mode 100644 tests/seq-bdhoare.ec create mode 100644 tests/seq-ehoare.ec create mode 100644 tests/seq-equiv.ec diff --git a/src/ecLowPhlGoal.ml b/src/ecLowPhlGoal.ml index c0ed0208a..e9308baa4 100644 --- a/src/ecLowPhlGoal.ml +++ b/src/ecLowPhlGoal.ml @@ -399,6 +399,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.