`proc rewrite /=` ignores the proof-local simplify hint configuration (named databases, local lemma adds)

[strub]

proc rewrite <pos> /= runs conversion (EcCallbyValue.norm_cbv) with a hard-coded EcReduction.nodelta reduction info (src/phl/ecPhlRewrite.ml, process_rewrite_simpl) and never consults the goal's simplify context (FApi.tc1_simplify_context). As a result, the proof-local hint configuration that simplify honours — hint +db, with hint +db (...), hint {lemma}, with hint {lemma} (...) — has no effect on proc rewrite /=: only rules in the default database fire.

Observed on llm-interactive @ 5243be5 (contains the named/local database work, 4d580f83c "Make proof-local simplify hint databases visible to conversion", and the new block form of proc rewrite).

Reproducer

require import AllCore.

op foo : int -> int.   (* rule in the named database [db] only *)
op bar : int -> int.   (* rule in the default database          *)

axiom fooE (x : int) : foo x = x + 1.
axiom barE (x : int) : bar x = x + 2.

hint simplify in db : fooE.
hint simplify barE.

module M = {
  proc f(a : int) : int = { var c : int; c <- foo a; return c; }
  proc f'(a : int) : int = { var c : int; c <- a + 1; return c; }
  proc g(a : int) : int = { var c : int; c <- bar a; return c; }
  proc g'(a : int) : int = { var c : int; c <- a + 2; return c; }
}.

(* Control: the named rule and its activation work for [simplify]. *)
lemma ambient (x : int) : foo x = x + 1.
proof. hint +db. simplify. done. qed.

(* Control: [proc rewrite /=] fires rules of the default database. *)
lemma default_db : equiv[M.g ~ M.g' : ={arg} ==> ={res}].
proof. proc. proc rewrite {1} /=. by sim. qed.

(* BUG: none of the proof-local forms reaches [proc rewrite /=]:
   [c <- foo a] is left untouched and [sim] fails. *)
lemma named_db_activate : equiv[M.f ~ M.f' : ={arg} ==> ={res}].
proof. proc. hint +db. proc rewrite {1} /=. by sim. qed.

lemma named_db_scoped : equiv[M.f ~ M.f' : ={arg} ==> ={res}].
proof. proc. with hint +db (proc rewrite {1} /=). by sim. qed.

lemma local_lemma_add : equiv[M.f ~ M.f' : ={arg} ==> ={res}].
proof. proc. hint {fooE}. proc rewrite {1} /=. by sim. qed.

lemma local_lemma_scoped : equiv[M.f ~ M.f' : ={arg} ==> ={res}].
proof. proc. with hint {fooE} (proc rewrite {1} /=). by sim. qed.

The two control lemmas pass; named_db_activate fails at its by sim (and so do the other three when tried individually).

Expected

proc rewrite /= should build its reduction info the way simplify does (EcHiGoal.process_simplify_info, the user_db computation from tc1_simplify_context and the hint clause), so that proof-local activations and lemma adds apply. An explicit use-site clause, proc rewrite {1} /= hint db, would be a natural complement. Other program-transforming tactics calling norm_cbv with a bare nodelta under src/phl/ are likely affected the same way.

Context

Wanted for clone-based proofs in goldbachJasmin: the constants of a cloned generic module are evaluated by rules kept in a named database (registered inside the abstract theory, they survive cloning with substitution), and proc rewrite {2} /= + sim closes the bridge to the extracted procedure. Today the rules have to be re-registered in the default database of the leaf file.