From 00b4471c7e565ddeaf142fbdffb8dbf8783990aa Mon Sep 17 00:00:00 2001
From: Benjamin Gregoire <Benjamin.Gregoire@inria.fr>
Date: Tue, 22 Sep 2026 06:38:31 +0200
Subject: [PATCH] fix(phl): `proc rewrite /=` honors the proof-local simplify
 context

`process_rewrite_simpl` reduced with a bare `EcReduction.nodelta`, whose
`user_local` is `SimplifyContext.empty`. The lemmas and databases added by
`hint ...` or by `with hint ... (...)` were therefore invisible to it, unlike
every other reduction tactic (`t_cbv`, `t_cbn`, `simplify`, `cbv`), which all
thread `FApi.tc1_simplify_context`.

The same `ri` is reused by the `t_change` that discharges the side goal, so
the discharge stays consistent with the rewriting performed.

The tests keep the rule in a named database and drop the hint before the
closing `apply`, so that only a rewriting of the program itself can close
the goal; each of them fails without the fix.
---
 src/phl/ecPhlRewrite.ml    |  7 +++-
 tests/procrewrite-simpl.ec | 75 ++++++++++++++++++++++++++++++++++++++
 2 files changed, 81 insertions(+), 1 deletion(-)

diff --git a/src/phl/ecPhlRewrite.ml b/src/phl/ecPhlRewrite.ml
index 7da93a3046..ebc874cfe5 100644
--- a/src/phl/ecPhlRewrite.ml
+++ b/src/phl/ecPhlRewrite.ml
@@ -204,7 +204,12 @@ let process_rewrite_simpl
   (pos  : pcodepos_or_range option)
   (tc   : tcenv1)
 =
-  let ri = EcReduction.nodelta in
+  (* thread the proof-local simplify overlay (hint +db, local rules) so
+     that [hint ...] and [with hint ... (proc rewrite /=)] are honored,
+     as they are by [simplify]/[cbv] *)
+  let ri =
+    { EcReduction.nodelta with
+        EcReduction.user_local = FApi.tc1_simplify_context tc } in
 
   let change (e : expr) ((hyps, me) : LDecl.hyps * memenv) =
     let f = ss_inv_of_expr (fst me) e in
diff --git a/tests/procrewrite-simpl.ec b/tests/procrewrite-simpl.ec
index 065282da49..ca6bbf0c49 100644
--- a/tests/procrewrite-simpl.ec
+++ b/tests/procrewrite-simpl.ec
@@ -12,3 +12,78 @@ proof.
 proc.
 proc rewrite 1 /=.
 abort.
+
+(* -------------------------------------------------------------------- *)
+(* [proc rewrite /=] must honor the proof-local simplify context, the way
+   [simplify]/[cbv] do.
+
+   Abstract operators (no body) and a rule kept in a named DB, so that
+   kernel conversion never reduces [f] on its own: the goals below close
+   only if the rule really fired on the *program*. The hint is dropped
+   again before the closing [apply], otherwise it is the [apply]'s own
+   conversion -- which does see the local context -- that would close the
+   goal, and the test would pass even without the rewrite. *)
+
+op f : int -> int.
+op g : int -> int.
+op P : int -> bool.
+
+axiom fE (x : int) : f x = g x.
+axiom Pg : P (g 1).
+
+hint simplify in dbF : fE.
+
+module N = {
+  var x : int
+
+  proc p () : unit = {
+    x <- f 1;
+  }
+}.
+
+(* Without the rule, nothing reduces and the postcondition stays on [f]. *)
+lemma simpl_needs_the_hint : hoare[N.p : true ==> P N.x].
+proof.
+proc.
+fail (proc rewrite 1 /=; wp; skip => _ _; apply Pg).
+abort.
+
+(* [hint +db] activates the database for the rest of the proof. *)
+lemma simpl_uses_local_hint_db : hoare[N.p : true ==> P N.x].
+proof.
+proc.
+hint +dbF.
+proc rewrite 1 /=.
+hint -dbF.
+wp; skip => _ _.
+apply Pg.
+qed.
+
+(* Per-proof lemma addition to the default DB. *)
+lemma simpl_uses_local_hint_lemma : hoare[N.p : true ==> P N.x].
+proof.
+proc.
+hint {fE}.
+proc rewrite 1 /=.
+hint clear.
+wp; skip => _ _.
+apply Pg.
+qed.
+
+(* Scoped form: [with hint ... (proc rewrite /=)]. The context is restored
+   on exit, so the closing [apply] cannot benefit from it. *)
+lemma simpl_uses_scoped_hint_db : hoare[N.p : true ==> P N.x].
+proof.
+proc.
+with hint +dbF (proc rewrite 1 /=).
+wp; skip => _ _.
+apply Pg.
+qed.
+
+lemma simpl_uses_scoped_hint_lemma : hoare[N.p : true ==> P N.x].
+proof.
+proc.
+with hint {fE} (proc rewrite 1 /=).
+wp; skip => _ _.
+apply Pg.
+qed.