diff --git a/src/phl/ecPhlConseq.ml b/src/phl/ecPhlConseq.ml
index f820393dc..cff256371 100644
--- a/src/phl/ecPhlConseq.ml
+++ b/src/phl/ecPhlConseq.ml
@@ -404,245 +404,52 @@ let t_conseq (pre : inv) (post : inv) (tc : tcenv1) =
 (* -------------------------------------------------------------------- *)
 
 
-(* Build the non-modification side-condition for equivF:
- * universally quantify the pre-memories, substitute the result variables,
- * then generalize over program variables modified by each procedure.
- * Returns (cond, bound_mems, other_bindings). *)
+(* The notmod rules are the frame rules of [EcHoareFrame], [EcBdHoareFrame]
+   and [EcEquivFrame]; their conditions are built by [EcPlFrame]. The
+   functions below are adapters keeping this module's legacy entry points. *)
+
 let cond_equivF_notmod ?(mk_other=false) (tc : tcenv1) (cond : ts_inv) =
   let (env, hyps, _) = FApi.tc1_eflat tc in
-  let ef = tc1_as_equivF tc in
-  let fl, fr = ef.ef_fl, ef.ef_fr in
-  let (mprl,mprr),(mpol,mpor) = Fun.equivF_memenv ef.ef_ml ef.ef_mr fl fr env in
-  let fsigl = (Fun.by_xpath fl env).f_sig in
-  let fsigr = (Fun.by_xpath fr env).f_sig in
-  let pvresl = pv_res and pvresr = pv_res in
-  let vresl = LDecl.fresh_id hyps "result_L" in
-  let vresr = LDecl.fresh_id hyps "result_R" in
-  let fresl = f_local vresl fsigl.fs_ret in
-  let fresr = f_local vresr fsigr.fs_ret in
-  let ml, mr = fst mpol, fst mpor in
-  assert (ml = cond.ml && mr = cond.mr);
-  let s = PVM.add env pvresl ml fresl (PVM.add env pvresr mr fresr PVM.empty) in
-  let cond = map_ts_inv1 (PVM.subst env s) cond in
-  let modil, modir = f_write env fl, f_write env fr in
-  let cond, bdgr, bder = generalize_mod_right_ env modir cond in
-  let cond, bdgl, bdel = generalize_mod_left_ env modil cond in
-  let cond =
-    map_ts_inv1 (f_forall_simpl
-      [(vresl, GTty fsigl.fs_ret);
-       (vresr, GTty fsigr.fs_ret)])
-      cond in
-  assert (fst mprl = ml && fst mprr = mr);
-  let cond = f_forall_mems_ts_inv mprl mprr (map_ts_inv2 f_imp (ef_pr ef) cond) in
-  let bmem = [ml;mr] in
-  let bother =
-    if mk_other then
-      mk_bind_pvar ml vresl (pvresl, fsigl.fs_ret) ::
-      mk_bind_pvar mr vresr (pvresr, fsigr.fs_ret) ::
-      List.flatten [mk_bind_globs env ml bdgl; mk_bind_pvars ml bdel;
-                    mk_bind_globs env mr bdgr; mk_bind_pvars mr bder]
-    else [] in
-  cond, bmem, bother
-
-(* equivF notmod rule:
- *
- *   ∀ml mr, P ml mr ⇒
- *     ∀(res_L : ret_L) (res_R : ret_R) (x1 ... xn : modified vars),
- *       Q' ml mr ⇒ Q ml mr
- *   equiv[f1 ~ f2] P ==> Q'
- *   ——————————————————————————————————————————————————————————————————
- *                    equiv[f1 ~ f2] P ==> Q
- *
- * The first premise universally quantifies over the return values and
- * all program variables modified by f1/f2, then checks that Q' ⇒ Q
- * holds under those bindings. *)
-let t_equivF_notmod (post : ts_inv) (tc : tcenv1) =
-  let ef = tc1_as_equivF tc in
-  let post = ts_inv_rebind post ef.ef_ml ef.ef_mr in
-  let cond1, _, _ = cond_equivF_notmod tc (map_ts_inv2 f_imp post (ef_po ef)) in
-  let cond2 = f_equivF (ef_pr ef) ef.ef_fl ef.ef_fr post in
-  FApi.xmutate1 tc `HlNotmod [cond1; cond2]
+  EcPlFrame.ts_frame_cond_F ~mk_other env hyps (tc1_as_equivF tc) cond
 
-(* -------------------------------------------------------------------- *)
 let cond_equivS_notmod ?(mk_other=false) (tc : tcenv1) (cond : ts_inv) =
-  let env = FApi.tc1_env tc in
-  let es = tc1_as_equivS tc in
-  let sl, sr = es.es_sl, es.es_sr in
-  let ml, mr = fst es.es_ml, fst es.es_mr in
-  assert (ml = cond.ml && mr = cond.mr);
-  let modil, modir = s_write env sl, s_write env sr in
-  let cond, bdgr, bder = generalize_mod_right_ env modir cond in
-  let cond, bdgl, bdel = generalize_mod_left_ env modil cond in
-  let cond = f_forall_mems_ts_inv es.es_ml es.es_mr (map_ts_inv2 f_imp (es_pr es) cond) in
-  let bmem = [ml;mr] in
-  let bother =
-    if mk_other then
-      List.flatten [mk_bind_globs env ml bdgl; mk_bind_pvars ml bdel;
-                    mk_bind_globs env mr bdgr; mk_bind_pvars mr bder]
-    else [] in
-  cond, bmem, bother
-
-(* equivS notmod rule: same as equivF_notmod but for statements
- * (no result variable generalization needed). *)
-let t_equivS_notmod (post : ts_inv) (tc : tcenv1) =
-  let es = tc1_as_equivS tc in
-  let post = ts_inv_rebind post (fst es.es_ml) (fst es.es_mr) in
-  let cond1,_,_ = cond_equivS_notmod tc (map_ts_inv2 f_imp post (es_po es)) in
-  let cond2 = f_equivS (snd es.es_ml) (snd es.es_mr) (es_pr es) es.es_sl es.es_sr post in
-  FApi.xmutate1 tc `HlNotmod [cond1; cond2]
-
-(* -------------------------------------------------------------------- *)
-(* Shared core for F-level notmod: substitutes the result variable,     *)
-(* generalizes over modified variables, quantifies over the result,     *)
-(* and builds the implication with the precondition.                    *)
-(*                                                                      *)
-(* Returns (cond, bmem, bother) where:                                  *)
-(*   cond   : the fully quantified side-condition formula               *)
-(*   bmem   : memories bound in the quantification ([m])               *)
-(*   bother : when ~mk_other, bindings for result + modified vars;     *)
-(*            otherwise []                                              *)
-
-let cond_F_notmod_core
-    ~(mk_other : bool)
-    (env       : env)
-    (hyps      : LDecl.hyps)
-    (f         : EcPath.xpath)
-    (m         : memory)
-    (pre       : ss_inv)
-    (cond      : ss_inv)
-=
-  let mpr,mpo = Fun.hoareF_memenv m f env in
-  let fsig = (Fun.by_xpath f env).f_sig in
-  let pvres = pv_res in
-  let vres = LDecl.fresh_id hyps "result" in
-  let fres = f_local vres fsig.fs_ret in
-  let m    = fst mpo in
-  let s = PVM.add env pvres m fres PVM.empty in
-  let cond = map_ss_inv1 (PVM.subst env s) cond in
-  let modi = f_write env f in
-  let cond, bdg, bde = generalize_mod_ env modi cond in
-  let cond = map_ss_inv1 (f_forall_simpl [(vres, GTty fsig.fs_ret)]) cond in
-  assert (fst mpr = m);
-  let cond = f_forall_mems_ss_inv mpr (map_ss_inv2 f_imp pre cond) in
-  let bmem = [m] in
-  let bother =
-    if mk_other then
-      mk_bind_pvar m vres (pvres, fsig.fs_ret) ::
-      List.flatten [mk_bind_globs env m bdg; mk_bind_pvars m bde]
-    else [] in
-  cond, bmem, bother
+  EcPlFrame.ts_frame_cond_S ~mk_other (FApi.tc1_env tc) (tc1_as_equivS tc) cond
 
 let cond_hoareF_notmod ?(mk_other=false) (tc : tcenv1) (cond : ss_inv) =
   let (env, hyps, _) = FApi.tc1_eflat tc in
   let hf = tc1_as_hoareF tc in
-  cond_F_notmod_core ~mk_other env hyps hf.hf_f hf.hf_m (hf_pr hf) cond
-
-(* hoareF notmod rule:
- *
- *   ∀m, P m ⇒
- *     ∀(res : ret) (x1 ... xn : modified vars),
- *       Q' m ⇒ Q m  [∧ Qe_i' ⇒ Qe_i for each exception]
- *   hoare[f] P ==> Q' / Qe'
- *   ———————————————————————————————————————————————————————
- *                hoare[f] P ==> Q / Qe
- *
- * Q / Qe denotes the normal postcondition Q together with the
- * per-exception postconditions Qe_i (if any). *)
-let t_hoareF_notmod (post : hs_inv) (tc : tcenv1) =
-  let hf = tc1_as_hoareF tc in
-  let p = hs_inv_rebind post hf.hf_m in
-  let post, epost = POE.destruct p.hsi_inv in
-  let fpost, fepost = POE.destruct (hf_po hf).hsi_inv in
-  let cond = f_imp post fpost in
-  let econd1 = TTC.merge2_poe_list fepost epost in
-  let cond1 = List.fold f_and cond econd1 in
-  let cond1, _, _ = cond_hoareF_notmod tc {m=hf.hf_m;inv=cond1} in
-  let cond2 = f_hoareF (hf_pr hf) hf.hf_f p in
-  FApi.xmutate1 tc `HlNotmod [cond1; cond2]
-
-(* -------------------------------------------------------------------- *)
-(* Shared core for S-level notmod: generalizes over modified variables  *)
-(* and builds the implication with the precondition.                    *)
-
-let cond_S_notmod_core
-    ~(mk_other : bool)
-    (env       : env)
-    (stmt      : stmt)
-    (memenv    : memenv)
-    (pre       : ss_inv)
-    (cond      : ss_inv)
-=
-  let m = fst memenv in
-  let modi = s_write env stmt in
-  let cond, bdg, bde = generalize_mod_ env modi cond in
-  let cond = f_forall_mems_ss_inv memenv (map_ss_inv2 f_imp pre cond) in
-  let bmem = [m] in
-  let bother =
-    if mk_other then
-      List.flatten [mk_bind_globs env m bdg; mk_bind_pvars m bde]
-    else [] in
-  cond, bmem, bother
+  EcPlFrame.ss_frame_cond_F ~mk_other env hyps hf.hf_f hf.hf_m (hf_pr hf) cond
 
 let cond_hoareS_notmod ?(mk_other=false) (tc : tcenv1) (cond : ss_inv) =
-  let env = FApi.tc1_env tc in
-  let hs = tc1_as_hoareS tc in
-  cond_S_notmod_core ~mk_other env hs.hs_s hs.hs_m (hs_pr hs) cond
-
-(* hoareS notmod rule: same as hoareF_notmod but for statements. *)
-let t_hoareS_notmod (post : hs_inv) (tc : tcenv1) =
   let hs = tc1_as_hoareS tc in
-  let p = hs_inv_rebind post (fst hs.hs_m) in
-  let post, epost = POE.destruct p.hsi_inv in
-  let fpost, fepost = POE.destruct (hs_po hs).hsi_inv in
-  let cond = f_imp post fpost in
-  let econd1 = TTC.merge2_poe_list fepost epost in
-  let cond1 = List.fold f_and cond econd1 in
-  let cond1, _, _ = cond_hoareS_notmod tc {m=fst hs.hs_m;inv=cond1} in
-  let cond2 = f_hoareS (snd hs.hs_m) (hs_pr hs) hs.hs_s p in
-  FApi.xmutate1 tc `HlNotmod [cond1; cond2]
+  EcPlFrame.ss_frame_cond_S ~mk_other (FApi.tc1_env tc) hs.hs_s hs.hs_m (hs_pr hs) cond
 
-(* -------------------------------------------------------------------- *)
 let cond_bdHoareF_notmod ?(mk_other=false) (tc : tcenv1) (cond : ss_inv) =
   let (env, hyps, _) = FApi.tc1_eflat tc in
   let hf = tc1_as_bdhoareF tc in
-  cond_F_notmod_core ~mk_other env hyps hf.bhf_f hf.bhf_m (bhf_pr hf) cond
-
+  EcPlFrame.ss_frame_cond_F ~mk_other env hyps hf.bhf_f hf.bhf_m (bhf_pr hf) cond
 
-(* bdHoareF notmod rule:
- *
- *   ∀m, P m ⇒
- *     ∀(res : ret) (x1 ... xn : modified vars),
- *       Q' m ⇒/⇔/⇐ Q m
- *   phoare[f] P ==> Q' cmp bd
- *   ——————————————————————————————————————————————
- *            phoare[f] P ==> Q cmp bd
- *
- * The direction of the postcondition implication depends on cmp:
- *   FHle (≤): Q' ⇒ Q    FHeq (=): Q' ⇔ Q    FHge (≥): Q ⇒ Q' *)
-let t_bdHoareF_notmod (post : ss_inv) (tc : tcenv1) =
-  let hf = tc1_as_bdhoareF tc in
-  let post = ss_inv_rebind post hf.bhf_m in
-  let _, cond =
-    bdHoare_conseq_conds hf.bhf_cmp (bhf_pr hf) (bhf_po hf) (bhf_pr hf) post in
-  let cond1, _, _ = cond_bdHoareF_notmod tc cond in
-  let cond2 = f_bdHoareF (bhf_pr hf) hf.bhf_f post hf.bhf_cmp (bhf_bd hf) in
-  FApi.xmutate1 tc `HlNotmod [cond1; cond2]
-
-(* -------------------------------------------------------------------- *)
 let cond_bdHoareS_notmod ?(mk_other=false) (tc : tcenv1) (cond : ss_inv) =
-  let env = FApi.tc1_env tc in
   let hs = tc1_as_bdhoareS tc in
-  cond_S_notmod_core ~mk_other env hs.bhs_s hs.bhs_m (bhs_pr hs) cond
+  EcPlFrame.ss_frame_cond_S ~mk_other (FApi.tc1_env tc) hs.bhs_s hs.bhs_m (bhs_pr hs) cond
 
-(* bdHoareS notmod rule: same as bdHoareF_notmod but for statements. *)
-let t_bdHoareS_notmod (post : ss_inv) (tc : tcenv1) =
-  let hs = tc1_as_bdhoareS tc in
-  let post = ss_inv_rebind post (fst hs.bhs_m) in
-  let _, cond =
-    bdHoare_conseq_conds hs.bhs_cmp (bhs_pr hs) (bhs_po hs) (bhs_pr hs) post in
-  let cond1, _, _ = cond_bdHoareS_notmod tc cond in
-  let cond2 = f_bdHoareS (snd hs.bhs_m) (bhs_pr hs) hs.bhs_s post hs.bhs_cmp (bhs_bd hs) in
-  FApi.xmutate1 tc `HlNotmod [cond1; cond2]
+let t_equivF_notmod (post : ts_inv) =
+  EcEquivFrame.t_equivF_frame { efr_post = post }
+
+let t_equivS_notmod (post : ts_inv) =
+  EcEquivFrame.t_equivS_frame { efr_post = post }
+
+let t_hoareF_notmod (post : hs_inv) =
+  EcHoareFrame.t_hoareF_frame { hfr_post = post }
+
+let t_hoareS_notmod (post : hs_inv) =
+  EcHoareFrame.t_hoareS_frame { hfr_post = post }
+
+let t_bdHoareF_notmod (post : ss_inv) =
+  EcBdHoareFrame.t_bdhoareF_frame { bfr_post = post }
+
+let t_bdHoareS_notmod (post : ss_inv) =
+  EcBdHoareFrame.t_bdhoareS_frame { bfr_post = post }
 
 (* -------------------------------------------------------------------- *)
 let gen_conseq_nm
diff --git a/src/phl/rules/bdhoare/ecBdHoareFrame.ml b/src/phl/rules/bdhoare/ecBdHoareFrame.ml
new file mode 100644
index 000000000..9924771e5
--- /dev/null
+++ b/src/phl/rules/bdhoare/ecBdHoareFrame.ml
@@ -0,0 +1,83 @@
+(* -------------------------------------------------------------------- *)
+open EcFol
+open EcAst
+open EcEnv
+open EcSubst
+
+open EcCoreGoal
+open EcLowPhlGoal
+
+(* -------------------------------------------------------------------- *)
+(* Parameters of the bdhoare frame rules: the new postcondition [Q']. Already
+   typed, nothing to resolve: the same record is the rule argument and the
+   node payload. *)
+type bdhoare_frame = {
+  bfr_post : ss_inv;
+}
+
+type EcCoreGoal.rule +=
+  | RBdHoareSFrame of bdhoare_frame
+  | RBdHoareFFrame of bdhoare_frame
+
+(* -------------------------------------------------------------------- *)
+(* The postcondition condition, before framing. Its direction follows the
+   comparison: an upper bound needs [Q] to imply [Q'], a lower bound the
+   converse, an equality both. *)
+let bdhoare_frame_post_cond (cmp : hoarecmp) (q : ss_inv) (q' : ss_inv) =
+  match cmp with
+  | FHle -> map_ss_inv2 f_imp q  q'
+  | FHeq -> map_ss_inv2 f_iff q  q'
+  | FHge -> map_ss_inv2 f_imp q' q
+
+(* -------------------------------------------------------------------- *)
+(* Pure core shared by the rule and its checker. *)
+let bdhoareS_frame_subgoals
+    (hyps : LDecl.hyps) (hs : bdHoareS) (n : bdhoare_frame)
+=
+  let env  = LDecl.toenv hyps in
+  let post = ss_inv_rebind n.bfr_post (fst hs.bhs_m) in
+  let cond = bdhoare_frame_post_cond hs.bhs_cmp (bhs_po hs) post in
+  let cond1, _, _ =
+    EcPlFrame.ss_frame_cond_S ~mk_other:false
+      env hs.bhs_s hs.bhs_m (bhs_pr hs) cond in
+  let cond2 =
+    f_bdHoareS (snd hs.bhs_m) (bhs_pr hs) hs.bhs_s post hs.bhs_cmp (bhs_bd hs) in
+  [cond1; cond2]
+
+let bdhoareF_frame_subgoals
+    (hyps : LDecl.hyps) (hf : bdHoareF) (n : bdhoare_frame)
+=
+  let env  = LDecl.toenv hyps in
+  let post = ss_inv_rebind n.bfr_post hf.bhf_m in
+  let cond = bdhoare_frame_post_cond hf.bhf_cmp (bhf_po hf) post in
+  let cond1, _, _ =
+    EcPlFrame.ss_frame_cond_F ~mk_other:false
+      env hyps hf.bhf_f hf.bhf_m (bhf_pr hf) cond in
+  let cond2 = f_bdHoareF (bhf_pr hf) hf.bhf_f post hf.bhf_cmp (bhf_bd hf) in
+  [cond1; cond2]
+
+(* -------------------------------------------------------------------- *)
+(* Rules (TCB). *)
+let t_bdhoareS_frame (r : bdhoare_frame) (tc : tcenv1) =
+  let hs = tc1_as_bdhoareS tc in
+  FApi.xrule1 tc (RBdHoareSFrame r)
+    (bdhoareS_frame_subgoals (FApi.tc1_hyps tc) hs r)
+
+let t_bdhoareF_frame (r : bdhoare_frame) (tc : tcenv1) =
+  let hf = tc1_as_bdhoareF tc in
+  FApi.xrule1 tc (RBdHoareFFrame r)
+    (bdhoareF_frame_subgoals (FApi.tc1_hyps tc) hf r)
+
+(* -------------------------------------------------------------------- *)
+(* Checkers: rerun the core, which recomputes the variables written by the
+   program from the goal's own context. *)
+let () =
+  register_rule_checker
+    (function
+     | RBdHoareSFrame n ->
+         Some (EcPlRecheck.checker_of "bdhoareS-frame" pf_as_bdhoareS
+                 (fun hyps hs -> bdhoareS_frame_subgoals hyps hs n))
+     | RBdHoareFFrame n ->
+         Some (EcPlRecheck.checker_of "bdhoareF-frame" pf_as_bdhoareF
+                 (fun hyps hf -> bdhoareF_frame_subgoals hyps hf n))
+     | _ -> None)
diff --git a/src/phl/rules/bdhoare/ecBdHoareFrame.mli b/src/phl/rules/bdhoare/ecBdHoareFrame.mli
new file mode 100644
index 000000000..f66cb3ef8
--- /dev/null
+++ b/src/phl/rules/bdhoare/ecBdHoareFrame.mli
@@ -0,0 +1,36 @@
+(* -------------------------------------------------------------------- *)
+open EcCoreGoal.FApi
+open EcAst
+
+(* ==================================================================== *)
+(* Rules (trusted)                                                      *)
+
+type bdhoare_frame = {
+  bfr_post : ss_inv;   (* new postcondition Q' *)
+}
+
+(* [t_bdhoareS_frame { bfr_post = Q' }] — framed change of the
+   postcondition, with [~] the goal's comparison:
+
+     forall &m, P => forall (mod c), Q [~>] Q'
+     phoare [c : P ==> Q'] ~ d
+     -----------------------------------------
+          phoare [c : P ==> Q] ~ d
+
+   where [mod c] are the program variables and globals written by [c], and
+   [Q [~>] Q'] is [Q => Q'] for [<=], [Q <=> Q'] for [=], [Q' => Q] for [>=].
+
+   Node: [RBdHoareSFrame { bfr_post = Q' }]. Checker: "bdhoareS-frame"; it
+   recomputes [mod c] from the goal's context. *)
+val t_bdhoareS_frame : bdhoare_frame -> backward
+
+(* [t_bdhoareF_frame { bfr_post = Q' }] — same for a procedure [f], also
+   quantifying over its result:
+
+     forall &m, P => forall (res : ret) (mod f), (Q [~>] Q')[res/result]
+     phoare [f : P ==> Q'] ~ d
+     -------------------------------------------------------------------
+                       phoare [f : P ==> Q] ~ d
+
+   Node: [RBdHoareFFrame { bfr_post = Q' }]. Checker: "bdhoareF-frame". *)
+val t_bdhoareF_frame : bdhoare_frame -> backward
diff --git a/src/phl/rules/bdhoare/ecBdHoareSeq.ml b/src/phl/rules/bdhoare/ecBdHoareSeq.ml
index f9bb7e886..8b30becc5 100644
--- a/src/phl/rules/bdhoare/ecBdHoareSeq.ml
+++ b/src/phl/rules/bdhoare/ecBdHoareSeq.ml
@@ -139,7 +139,8 @@ let () =
    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]. *)
+   TEMPORARY: the consequence rule still comes from 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
diff --git a/src/phl/rules/bdhoare/ecBdHoareSeq.mli b/src/phl/rules/bdhoare/ecBdHoareSeq.mli
index 787228ed0..fc5496c22 100644
--- a/src/phl/rules/bdhoare/ecBdHoareSeq.mli
+++ b/src/phl/rules/bdhoare/ecBdHoareSeq.mli
@@ -46,8 +46,9 @@ 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
+   of (N): introduce [r1 r2], apply the framed consequence
+   [EcPhlConseq.t_hoareS_conseq_nm] (the frame rule
+   [EcHoareFrame.t_hoareS_frame], then the consequence rule) 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. *)
diff --git a/src/phl/rules/ecPlFrame.ml b/src/phl/rules/ecPlFrame.ml
new file mode 100644
index 000000000..b95bc16eb
--- /dev/null
+++ b/src/phl/rules/ecPlFrame.ml
@@ -0,0 +1,144 @@
+(* -------------------------------------------------------------------- *)
+open EcUtils
+open EcAst
+open EcTypes
+open EcFol
+open EcEnv
+open EcPV
+open EcSubst
+open EcLowPhlGoal
+
+(* -------------------------------------------------------------------- *)
+(* Framing conditions, shared by the frame rules of every logic (and by
+   [conseq auto]). Framing — generalizing a condition over the variables a
+   program writes — is done here and nowhere else.
+
+   Each builder returns [(cond, bmem, bother)]: the closed side condition,
+   the memories it quantifies over, and (only when [~mk_other]) bindings for
+   the other quantified variables (result, modified globals and variables),
+   used by [conseq auto] to introduce them. *)
+
+type frame_cond = form * memory list * (EcIdent.t * ss_inv) list
+
+(* -------------------------------------------------------------------- *)
+(* One-sided, statement: forall &m, pre => forall (mod s), cond. *)
+let ss_frame_cond_S
+    ~(mk_other : bool)
+    (env       : env)
+    (s         : stmt)
+    (memenv    : memenv)
+    (pre       : ss_inv)
+    (cond      : ss_inv)
+=
+  let m = fst memenv in
+  let modi = s_write env s in
+  let cond, bdg, bde = generalize_mod_ env modi cond in
+  let cond = f_forall_mems_ss_inv memenv (map_ss_inv2 f_imp pre cond) in
+  let bmem = [m] in
+  let bother =
+    if mk_other then
+      List.flatten [mk_bind_globs env m bdg; mk_bind_pvars m bde]
+    else [] in
+  cond, bmem, bother
+
+(* -------------------------------------------------------------------- *)
+(* One-sided, procedure:
+   forall &m, pre => forall (res : ret) (mod f), cond[res/result]. *)
+let ss_frame_cond_F
+    ~(mk_other : bool)
+    (env       : env)
+    (hyps      : LDecl.hyps)
+    (f         : EcPath.xpath)
+    (m         : memory)
+    (pre       : ss_inv)
+    (cond      : ss_inv)
+=
+  let mpr,mpo = Fun.hoareF_memenv m f env in
+  let fsig = (Fun.by_xpath f env).f_sig in
+  let pvres = pv_res in
+  let vres = LDecl.fresh_id hyps "result" in
+  let fres = f_local vres fsig.fs_ret in
+  let m    = fst mpo in
+  let s = PVM.add env pvres m fres PVM.empty in
+  let cond = map_ss_inv1 (PVM.subst env s) cond in
+  let modi = f_write env f in
+  let cond, bdg, bde = generalize_mod_ env modi cond in
+  let cond = map_ss_inv1 (f_forall_simpl [(vres, GTty fsig.fs_ret)]) cond in
+  assert (fst mpr = m);
+  let cond = f_forall_mems_ss_inv mpr (map_ss_inv2 f_imp pre cond) in
+  let bmem = [m] in
+  let bother =
+    if mk_other then
+      mk_bind_pvar m vres (pvres, fsig.fs_ret) ::
+      List.flatten [mk_bind_globs env m bdg; mk_bind_pvars m bde]
+    else [] in
+  cond, bmem, bother
+
+(* -------------------------------------------------------------------- *)
+(* Two-sided, statements:
+   forall &1 &2, pre => forall (mod sl)<1> (mod sr)<2>, cond. *)
+let ts_frame_cond_S
+    ~(mk_other : bool)
+    (env       : env)
+    (es        : equivS)
+    (cond      : ts_inv)
+=
+  let sl, sr = es.es_sl, es.es_sr in
+  let ml, mr = fst es.es_ml, fst es.es_mr in
+  assert (ml = cond.ml && mr = cond.mr);
+  let modil, modir = s_write env sl, s_write env sr in
+  let cond, bdgr, bder = generalize_mod_right_ env modir cond in
+  let cond, bdgl, bdel = generalize_mod_left_ env modil cond in
+  let cond = f_forall_mems_ts_inv es.es_ml es.es_mr (map_ts_inv2 f_imp (es_pr es) cond) in
+  let bmem = [ml;mr] in
+  let bother =
+    if mk_other then
+      List.flatten [mk_bind_globs env ml bdgl; mk_bind_pvars ml bdel;
+                    mk_bind_globs env mr bdgr; mk_bind_pvars mr bder]
+    else [] in
+  cond, bmem, bother
+
+(* -------------------------------------------------------------------- *)
+(* Two-sided, procedures:
+   forall &1 &2, pre =>
+     forall (res_L : retl) (res_R : retr) (mod fl)<1> (mod fr)<2>,
+       cond[res_L/result<1>, res_R/result<2>]. *)
+let ts_frame_cond_F
+    ~(mk_other : bool)
+    (env       : env)
+    (hyps      : LDecl.hyps)
+    (ef        : equivF)
+    (cond      : ts_inv)
+=
+  let fl, fr = ef.ef_fl, ef.ef_fr in
+  let (mprl,mprr),(mpol,mpor) = Fun.equivF_memenv ef.ef_ml ef.ef_mr fl fr env in
+  let fsigl = (Fun.by_xpath fl env).f_sig in
+  let fsigr = (Fun.by_xpath fr env).f_sig in
+  let pvresl = pv_res and pvresr = pv_res in
+  let vresl = LDecl.fresh_id hyps "result_L" in
+  let vresr = LDecl.fresh_id hyps "result_R" in
+  let fresl = f_local vresl fsigl.fs_ret in
+  let fresr = f_local vresr fsigr.fs_ret in
+  let ml, mr = fst mpol, fst mpor in
+  assert (ml = cond.ml && mr = cond.mr);
+  let s = PVM.add env pvresl ml fresl (PVM.add env pvresr mr fresr PVM.empty) in
+  let cond = map_ts_inv1 (PVM.subst env s) cond in
+  let modil, modir = f_write env fl, f_write env fr in
+  let cond, bdgr, bder = generalize_mod_right_ env modir cond in
+  let cond, bdgl, bdel = generalize_mod_left_ env modil cond in
+  let cond =
+    map_ts_inv1 (f_forall_simpl
+      [(vresl, GTty fsigl.fs_ret);
+       (vresr, GTty fsigr.fs_ret)])
+      cond in
+  assert (fst mprl = ml && fst mprr = mr);
+  let cond = f_forall_mems_ts_inv mprl mprr (map_ts_inv2 f_imp (ef_pr ef) cond) in
+  let bmem = [ml;mr] in
+  let bother =
+    if mk_other then
+      mk_bind_pvar ml vresl (pvresl, fsigl.fs_ret) ::
+      mk_bind_pvar mr vresr (pvresr, fsigr.fs_ret) ::
+      List.flatten [mk_bind_globs env ml bdgl; mk_bind_pvars ml bdel;
+                    mk_bind_globs env mr bdgr; mk_bind_pvars mr bder]
+    else [] in
+  cond, bmem, bother
diff --git a/src/phl/rules/ecPlFrame.mli b/src/phl/rules/ecPlFrame.mli
new file mode 100644
index 000000000..ec29364a0
--- /dev/null
+++ b/src/phl/rules/ecPlFrame.mli
@@ -0,0 +1,37 @@
+(* -------------------------------------------------------------------- *)
+open EcAst
+open EcEnv
+
+(* -------------------------------------------------------------------- *)
+(* Framing conditions, shared by the frame rules of every logic (and by
+   [conseq auto]). Framing — generalizing a condition over the variables a
+   program writes — is done here and nowhere else.
+
+   Each builder returns [(cond, bmem, bother)]: the closed side condition,
+   the memories it quantifies over, and — only when [~mk_other] — bindings
+   for the other quantified variables (result, modified globals and program
+   variables), used by [conseq auto] to introduce them. *)
+
+type frame_cond = form * memory list * (EcIdent.t * ss_inv) list
+
+(* Statement [s] in memory [memenv]:
+     forall &m, pre => forall (mod s), cond *)
+val ss_frame_cond_S :
+  mk_other:bool -> env -> stmt -> memenv -> ss_inv -> ss_inv -> frame_cond
+
+(* Procedure [f], postcondition memory [m]:
+     forall &m, pre => forall (res : ret) (mod f), cond[res / result] *)
+val ss_frame_cond_F :
+  mk_other:bool -> env -> LDecl.hyps -> EcPath.xpath -> memory
+  -> ss_inv -> ss_inv -> frame_cond
+
+(* Two-sided, statements of [es], under its precondition:
+     forall &1 &2, pre => forall (mod sl)<1> (mod sr)<2>, cond *)
+val ts_frame_cond_S : mk_other:bool -> env -> equivS -> ts_inv -> frame_cond
+
+(* Two-sided, procedures of [ef], under its precondition:
+     forall &1 &2, pre =>
+       forall (res_L : retl) (res_R : retr) (mod fl)<1> (mod fr)<2>,
+         cond[res_L / result<1>, res_R / result<2>] *)
+val ts_frame_cond_F :
+  mk_other:bool -> env -> LDecl.hyps -> equivF -> ts_inv -> frame_cond
diff --git a/src/phl/rules/equiv/ecEquivFrame.ml b/src/phl/rules/equiv/ecEquivFrame.ml
new file mode 100644
index 000000000..02ebfb375
--- /dev/null
+++ b/src/phl/rules/equiv/ecEquivFrame.ml
@@ -0,0 +1,67 @@
+(* -------------------------------------------------------------------- *)
+open EcFol
+open EcAst
+open EcEnv
+open EcSubst
+
+open EcCoreGoal
+open EcLowPhlGoal
+
+(* -------------------------------------------------------------------- *)
+(* Parameters of the equiv frame rules: the new postcondition [Q']. Already
+   typed, nothing to resolve: the same record is the rule argument and the
+   node payload. *)
+type equiv_frame = {
+  efr_post : ts_inv;
+}
+
+type EcCoreGoal.rule +=
+  | REquivSFrame of equiv_frame
+  | REquivFFrame of equiv_frame
+
+(* -------------------------------------------------------------------- *)
+(* Pure core shared by the rule and its checker. *)
+let equivS_frame_subgoals (hyps : LDecl.hyps) (es : equivS) (n : equiv_frame) =
+  let env  = LDecl.toenv hyps in
+  let post = ts_inv_rebind n.efr_post (fst es.es_ml) (fst es.es_mr) in
+  let cond1, _, _ =
+    EcPlFrame.ts_frame_cond_S ~mk_other:false
+      env es (map_ts_inv2 f_imp post (es_po es)) in
+  let cond2 =
+    f_equivS (snd es.es_ml) (snd es.es_mr) (es_pr es) es.es_sl es.es_sr post in
+  [cond1; cond2]
+
+let equivF_frame_subgoals (hyps : LDecl.hyps) (ef : equivF) (n : equiv_frame) =
+  let env  = LDecl.toenv hyps in
+  let post = ts_inv_rebind n.efr_post ef.ef_ml ef.ef_mr in
+  let cond1, _, _ =
+    EcPlFrame.ts_frame_cond_F ~mk_other:false
+      env hyps ef (map_ts_inv2 f_imp post (ef_po ef)) in
+  let cond2 = f_equivF (ef_pr ef) ef.ef_fl ef.ef_fr post in
+  [cond1; cond2]
+
+(* -------------------------------------------------------------------- *)
+(* Rules (TCB). *)
+let t_equivS_frame (r : equiv_frame) (tc : tcenv1) =
+  let es = tc1_as_equivS tc in
+  FApi.xrule1 tc (REquivSFrame r)
+    (equivS_frame_subgoals (FApi.tc1_hyps tc) es r)
+
+let t_equivF_frame (r : equiv_frame) (tc : tcenv1) =
+  let ef = tc1_as_equivF tc in
+  FApi.xrule1 tc (REquivFFrame r)
+    (equivF_frame_subgoals (FApi.tc1_hyps tc) ef r)
+
+(* -------------------------------------------------------------------- *)
+(* Checkers: rerun the core, which recomputes the variables written by both
+   programs from the goal's own context. *)
+let () =
+  register_rule_checker
+    (function
+     | REquivSFrame n ->
+         Some (EcPlRecheck.checker_of "equivS-frame" pf_as_equivS
+                 (fun hyps es -> equivS_frame_subgoals hyps es n))
+     | REquivFFrame n ->
+         Some (EcPlRecheck.checker_of "equivF-frame" pf_as_equivF
+                 (fun hyps ef -> equivF_frame_subgoals hyps ef n))
+     | _ -> None)
diff --git a/src/phl/rules/equiv/ecEquivFrame.mli b/src/phl/rules/equiv/ecEquivFrame.mli
new file mode 100644
index 000000000..a65b475b1
--- /dev/null
+++ b/src/phl/rules/equiv/ecEquivFrame.mli
@@ -0,0 +1,38 @@
+(* -------------------------------------------------------------------- *)
+open EcCoreGoal.FApi
+open EcAst
+
+(* ==================================================================== *)
+(* Rules (trusted)                                                      *)
+
+type equiv_frame = {
+  efr_post : ts_inv;   (* new postcondition Q' *)
+}
+
+(* [t_equivS_frame { efr_post = Q' }] — framed weakening of the
+   postcondition:
+
+     forall &1 &2, P => forall (mod c)<1> (mod c')<2>, Q' => Q
+     equiv [c ~ c' : P ==> Q']
+     ---------------------------------------------------------
+                equiv [c ~ c' : P ==> Q]
+
+   where [mod c] / [mod c'] are the program variables and globals written by
+   each side.
+
+   Node: [REquivSFrame { efr_post = Q' }]. Checker: "equivS-frame"; it
+   recomputes [mod c], [mod c'] from the goal's context. *)
+val t_equivS_frame : equiv_frame -> backward
+
+(* [t_equivF_frame { efr_post = Q' }] — same for procedures [f ~ f'], also
+   quantifying over their results:
+
+     forall &1 &2, P =>
+       forall (res_L : ret) (res_R : ret') (mod f)<1> (mod f')<2>,
+         (Q' => Q)[res_L/result<1>, res_R/result<2>]
+     equiv [f ~ f' : P ==> Q']
+     ---------------------------------------------------------------
+                    equiv [f ~ f' : P ==> Q]
+
+   Node: [REquivFFrame { efr_post = Q' }]. Checker: "equivF-frame". *)
+val t_equivF_frame : equiv_frame -> backward
diff --git a/src/phl/rules/equiv/ecEquivSeq.ml b/src/phl/rules/equiv/ecEquivSeq.ml
index fda89a500..76926fb25 100644
--- a/src/phl/rules/equiv/ecEquivSeq.ml
+++ b/src/phl/rules/equiv/ecEquivSeq.ml
@@ -71,7 +71,8 @@ let () =
    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]. *)
+   TEMPORARY: the consequence rule still comes from 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
diff --git a/src/phl/rules/equiv/ecEquivSeq.mli b/src/phl/rules/equiv/ecEquivSeq.mli
index acbe7d0bd..ce38a14e0 100644
--- a/src/phl/rules/equiv/ecEquivSeq.mli
+++ b/src/phl/rules/equiv/ecEquivSeq.mli
@@ -34,7 +34,8 @@ val t_equiv_seq : equiv_seq_rule -> backward
         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])
+   2. on (b), the framed consequence [EcPhlConseq.t_equivS_conseq_nm] (the
+      frame rule [EcEquivFrame.t_equivS_frame], then the consequence rule)
       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];
diff --git a/src/phl/rules/hoare/ecHoareFrame.ml b/src/phl/rules/hoare/ecHoareFrame.ml
new file mode 100644
index 000000000..a0441b16e
--- /dev/null
+++ b/src/phl/rules/hoare/ecHoareFrame.ml
@@ -0,0 +1,82 @@
+(* -------------------------------------------------------------------- *)
+open EcUtils
+open EcFol
+open EcAst
+open EcEnv
+open EcSubst
+
+open EcCoreGoal
+open EcLowPhlGoal
+
+module TTC = EcProofTyping
+
+(* -------------------------------------------------------------------- *)
+(* Parameters of the hoare frame rules: the new postcondition [Q'] (normal
+   and exceptional parts). Already typed, nothing to resolve: the same record
+   is the rule argument and the node payload. *)
+type hoare_frame = {
+  hfr_post : hs_inv;
+}
+
+type EcCoreGoal.rule +=
+  | RHoareSFrame of hoare_frame
+  | RHoareFFrame of hoare_frame
+
+(* -------------------------------------------------------------------- *)
+(* The postcondition condition, before framing:
+     (Q' => Q) /\ (for each exception e, Q'_e => Q_e) *)
+let hoare_frame_post_cond (post : exnpost) (fpost : exnpost) : form =
+  let post , epost  = POE.destruct post  in
+  let fpost, fepost = POE.destruct fpost in
+  let cond   = f_imp post fpost in
+  let econd1 = TTC.merge2_poe_list fepost epost in
+  List.fold f_and cond econd1
+
+(* -------------------------------------------------------------------- *)
+(* Pure core shared by the rule and its checker. *)
+let hoareS_frame_subgoals (hyps : LDecl.hyps) (hs : sHoareS) (n : hoare_frame) =
+  let env  = LDecl.toenv hyps in
+  let p    = hs_inv_rebind n.hfr_post (fst hs.hs_m) in
+  let cond = hoare_frame_post_cond p.hsi_inv (hs_po hs).hsi_inv in
+  let cond1, _, _ =
+    EcPlFrame.ss_frame_cond_S ~mk_other:false
+      env hs.hs_s hs.hs_m (hs_pr hs) { m = fst hs.hs_m; inv = cond } in
+  let cond2 = f_hoareS (snd hs.hs_m) (hs_pr hs) hs.hs_s p in
+  [cond1; cond2]
+
+let hoareF_frame_subgoals (hyps : LDecl.hyps) (hf : sHoareF) (n : hoare_frame) =
+  let env  = LDecl.toenv hyps in
+  let p    = hs_inv_rebind n.hfr_post hf.hf_m in
+  let cond = hoare_frame_post_cond p.hsi_inv (hf_po hf).hsi_inv in
+  let cond1, _, _ =
+    EcPlFrame.ss_frame_cond_F ~mk_other:false
+      env hyps hf.hf_f hf.hf_m (hf_pr hf) { m = hf.hf_m; inv = cond } in
+  let cond2 = f_hoareF (hf_pr hf) hf.hf_f p in
+  [cond1; cond2]
+
+(* -------------------------------------------------------------------- *)
+(* Rules (TCB). *)
+let t_hoareS_frame (r : hoare_frame) (tc : tcenv1) =
+  let hs = tc1_as_hoareS tc in
+  FApi.xrule1 tc (RHoareSFrame r)
+    (hoareS_frame_subgoals (FApi.tc1_hyps tc) hs r)
+
+let t_hoareF_frame (r : hoare_frame) (tc : tcenv1) =
+  let hf = tc1_as_hoareF tc in
+  FApi.xrule1 tc (RHoareFFrame r)
+    (hoareF_frame_subgoals (FApi.tc1_hyps tc) hf r)
+
+(* -------------------------------------------------------------------- *)
+(* Checkers: rerun the core, which recomputes the variables written by the
+   program — the soundness-critical part of framing — from the goal's own
+   context. *)
+let () =
+  register_rule_checker
+    (function
+     | RHoareSFrame n ->
+         Some (EcPlRecheck.checker_of "hoareS-frame" pf_as_hoareS
+                 (fun hyps hs -> hoareS_frame_subgoals hyps hs n))
+     | RHoareFFrame n ->
+         Some (EcPlRecheck.checker_of "hoareF-frame" pf_as_hoareF
+                 (fun hyps hf -> hoareF_frame_subgoals hyps hf n))
+     | _ -> None)
diff --git a/src/phl/rules/hoare/ecHoareFrame.mli b/src/phl/rules/hoare/ecHoareFrame.mli
new file mode 100644
index 000000000..2f9ff6095
--- /dev/null
+++ b/src/phl/rules/hoare/ecHoareFrame.mli
@@ -0,0 +1,37 @@
+(* -------------------------------------------------------------------- *)
+open EcCoreGoal.FApi
+open EcAst
+
+(* ==================================================================== *)
+(* Rules (trusted)                                                      *)
+
+type hoare_frame = {
+  hfr_post : hs_inv;   (* new postcondition Q' (normal and exceptional) *)
+}
+
+(* [t_hoareS_frame { hfr_post = Q' }] — framed weakening of the
+   postcondition:
+
+     forall &m, P => forall (mod c), (Q' => Q) /\ (forall e, Q'_e => Q_e)
+     hoare [c : P ==> Q' | Q'_e]
+     ---------------------------------------------------------------------
+                       hoare [c : P ==> Q | Q_e]
+
+   where [mod c] are the program variables and globals written by [c], and
+   [Q_e] / [Q'_e] the exceptional postconditions.
+
+   Node: [RHoareSFrame { hfr_post = Q' }]. Checker: "hoareS-frame"; it
+   recomputes [mod c] from the goal's context. *)
+val t_hoareS_frame : hoare_frame -> backward
+
+(* [t_hoareF_frame { hfr_post = Q' }] — same for a procedure [f], also
+   quantifying over its result:
+
+     forall &m, P =>
+       forall (res : ret) (mod f), ((Q' => Q) /\ (forall e, Q'_e => Q_e))[res/result]
+     hoare [f : P ==> Q' | Q'_e]
+     ---------------------------------------------------------------------
+                       hoare [f : P ==> Q | Q_e]
+
+   Node: [RHoareFFrame { hfr_post = Q' }]. Checker: "hoareF-frame". *)
+val t_hoareF_frame : hoare_frame -> backward