From 70586cc7af9d03a448d061d3a5183d045609d8e8 Mon Sep 17 00:00:00 2001
From: Xingyu Xie <namasikanam@gmail.com>
Date: Fri, 21 Aug 2026 14:57:10 +0200
Subject: [PATCH] fix(clone): proof * [tag] must not drop untagged axioms

`check_evtags` (`ecTheoryReplay.ml`) decided whether an axiom was forced by a
bracketed `proof * [tag]` directive by mapping the directive's tag test over
the *axiom's own* tag list `src`. For an untagged axiom `src = []`, the test
`List.mem true (List.map _ [])` is `false`, so the axiom was silently NOT
forced and the correct default `dfl` was never consulted. A clone could then
assume an untagged axiom without proof (e.g. instantiate `FinType.enum_spec`
falsely and derive `false`).

Fold the directive tags starting from the default `dfl`, testing membership of
each directive tag in the axiom's `src`. Untagged axioms now fall back to the
default (forced); explicit `[-tag]` exclusions still apply to tagged axioms.

Regression: tests/clone-proofstar-tagdrop.ec (asserts the bracketed clone that
dropped the untagged axiom now fails, via the `fail` idiom).

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
---
 src/ecTheoryReplay.ml            | 16 +++++++---------
 tests/clone-proofstar-tagdrop.ec | 14 ++++++++++++++
 2 files changed, 21 insertions(+), 9 deletions(-)
 create mode 100644 tests/clone-proofstar-tagdrop.ec

diff --git a/src/ecTheoryReplay.ml b/src/ecTheoryReplay.ml
index 380bc501d..ac5046ef0 100644
--- a/src/ecTheoryReplay.ml
+++ b/src/ecTheoryReplay.ml
@@ -351,15 +351,13 @@ let check_evtags ?(tags : evtags option) (src : symbol list) =
       let dfl =
         not (List.mem explicit src) &&
         not (List.exists (fun (mode, _) -> mode = `Include) tags) in
-      let stt =
-        List.map (fun src ->
-          let do1 status (mode, dst) =
-            match mode with
-            | `Exclude -> if sym_equal src dst then raise Reject; status
-            | `Include -> status || (sym_equal src dst)
-          in List.fold_left do1 dfl tags)
-          src
-      in List.mem true stt
+      let has_tag dst = List.exists (fun s -> sym_equal s dst) src in
+      let do1 status (mode, dst) =
+        match mode with
+        | `Exclude -> if has_tag dst then raise Reject; status
+        | `Include -> status || has_tag dst
+      in
+      List.fold_left do1 dfl tags
 
   with Reject -> false
 
diff --git a/tests/clone-proofstar-tagdrop.ec b/tests/clone-proofstar-tagdrop.ec
new file mode 100644
index 000000000..ce57e736d
--- /dev/null
+++ b/tests/clone-proofstar-tagdrop.ec
@@ -0,0 +1,14 @@
+(* Regression for the clone `proof * [tag]` untagged-axiom drop.
+
+   Under a bracketed prove-all directive (`proof * [-dummy]`) the UNTAGGED
+   FinType.enum_spec axiom must still be FORCED. With `enum <- [0]` it is
+   false, so the discharging `by smt()` cannot prove it and the whole `clone`
+   command must fail. Before the fix the untagged axiom was silently dropped,
+   so this clone was accepted (and `F.enum_spec` could be used to prove
+   `false`). *)
+require import AllCore List FinType.
+
+fail clone FinType as F with
+  type t <- int,
+  op enum <- [0]
+  proof * [-dummy] by smt().