From 0587206bb463c11d267134d58baf608031f79d16 Mon Sep 17 00:00:00 2001
From: Pierre-Yves Strub <pierre-yves@strub.nu>
Date: Tue, 3 Nov 2026 12:01:17 +0100
Subject: [PATCH] fix(crush): the activated simplify databases apply to every
 reduction of crush

The head reductions that expose the goal's shape in t_lazy_match (split,
elim, ... under `/>` and `progress`) and the closing simplification of
t_crush / t_crush_fwd took the proof-local simplify context reduced to
its opacity overrides, that is the default database only. A rule of a
database activated with `hint +db` was then invisible exactly where delta
happens: a rule whose argument needs an unfolding first (`g (sw c c).`2`
with `g c = true` in `db`) never applied inside crush, while the same rule
in the default database did.

These reductions now take the goal's whole simplify context (activated
databases, local rules, opacity overrides), as the simplification passes
do. Regression test in tests/hint-db-crush.ec.
---
 src/ecLowGoal.ml       | 20 +++++++++-----------
 tests/hint-db-crush.ec | 17 +++++++++++++++++
 2 files changed, 26 insertions(+), 11 deletions(-)
 create mode 100644 tests/hint-db-crush.ec

diff --git a/src/ecLowGoal.ml b/src/ecLowGoal.ml
index 3b7db3c4a..0ef1c9067 100644
--- a/src/ecLowGoal.ml
+++ b/src/ecLowGoal.ml
@@ -423,13 +423,11 @@ let rec t_lazy_match ?(reduce = `Full) ?(texn = fun _ -> raise InvalidGoalShape)
       | `None    -> raise InvalidGoalShape
       | `Full    -> EcReduction.full_red
       | `NoDelta -> EcReduction.nodelta in
-    (* honor proof-local [-delta op] opacity overrides without changing
-       which simplify databases the strategy consults *)
+    (* the proof-local simplify context (activated databases, local
+       rules, opacity overrides) applies to these head reductions too *)
     let strategy =
       { strategy with
-          EcReduction.user_local =
-            EcEnv.SimplifyContext.opacity_only
-              (FApi.tc1_simplify_context tc) } in
+          EcReduction.user_local = FApi.tc1_simplify_context tc } in
     FApi.t_seq (FApi.t_or (t_hred_with_info strategy) texn) (t_lazy_match ~reduce tx) tc
 
 (* -------------------------------------------------------------------- *)
@@ -2549,11 +2547,11 @@ let t_crush ?(delta = true) ?tsolve (tc : tcenv1) =
     { cs_undosubst = Sid.empty (*Sid.of_list (List.map fst (LDecl.tohyps (FApi.tc1_hyps tc)).h_local)*) ;
       cs_sbeq = (* Sid.of_list (List.map fst (LDecl.tohyps (FApi.tc1_hyps tc)).h_local)*) Sid.empty;
     } in
+  (* the closing pass sees the proof-local simplify context (activated
+     databases, local rules, opacity overrides), as the entry pass does *)
   let final =
     { EcReduction.nodelta with
-        EcReduction.user_local =
-          EcEnv.SimplifyContext.opacity_only
-            (FApi.tc1_simplify_context tc) } in
+        EcReduction.user_local = FApi.tc1_simplify_context tc } in
   FApi.t_seq (entry state) (t_simplify_with_info final) tc
 
 
@@ -2926,11 +2924,11 @@ let t_crush_fwd ?(delta = true) nb_intros (tc : tcenv1) =
     | _ -> t_fail tc
   in
 
+  (* the closing pass sees the proof-local simplify context (activated
+     databases, local rules, opacity overrides), as the entry pass does *)
   let final =
     { EcReduction.nodelta with
-        EcReduction.user_local =
-          EcEnv.SimplifyContext.opacity_only
-            (FApi.tc1_simplify_context tc) } in
+        EcReduction.user_local = FApi.tc1_simplify_context tc } in
   FApi.t_seq
     (aux0 nb_intros)
     (t_simplify_with_info final) tc
diff --git a/tests/hint-db-crush.ec b/tests/hint-db-crush.ec
new file mode 100644
index 000000000..05b3458f8
--- /dev/null
+++ b/tests/hint-db-crush.ec
@@ -0,0 +1,17 @@
+(* A rule of an activated database applies inside crush even when the
+   term it rewrites only appears after a delta step: the head reductions
+   of split/elim see the activated databases too. *)
+require import AllCore.
+
+op c : int.
+op g : int -> bool.
+op sw (x y : int) = (y, x).
+
+axiom gE : g c = true.
+hint simplify in db : gE.
+
+lemma crush_db : g (sw c c).`2.
+proof. hint +db. by move=> />. qed.
+
+lemma crush_db_split (b : bool) : b => g (sw c c).`2 /\ b.
+proof. hint +db. by move=> />. qed.