fix(phl): proc rewrite /= honors the proof-local simplify context

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

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.