Skip to content

fix(crush): the activated simplify databases apply to every reduction of crush #1227

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
strub merged 1 commit into from
Nov 3, 2026
Merged

fix(crush): the activated simplify databases apply to every reduction of crush #1227

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
20 changes: 9 additions & 11 deletions src/ecLowGoal.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

(* -------------------------------------------------------------------- *)
Expand Down Expand Up @@ -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


Expand Down Expand Up @@ -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
17 changes: 17 additions & 0 deletions tests/hint-db-crush.ec
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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.
Loading