From 1942171e08d4dced4c34a23e7a610098936a0a32 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 force untagged axioms
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

`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 when the bracket list is exclusion-only); positive include
lists (`proof * [tag]`) are unaffected, since their default is not-forced.

Regression: tests/clone-proofstar-tagdrop.ec — self-contained: a local theory
with an untagged unprovable axiom must make `clone ... proof * [-foo] by done`
fail (via the `fail` idiom), while the include-list clone `proof * [foo]`
still succeeds with the untagged axiom left assumed.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
---
 src/ecTheoryReplay.ml            | 16 +++++++---------
 tests/clone-proofstar-tagdrop.ec | 19 +++++++++++++++++++
 2 files changed, 26 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..719acb15c
--- /dev/null
+++ b/tests/clone-proofstar-tagdrop.ec
@@ -0,0 +1,19 @@
+(* Regression for `proof * [-tag]` failing to force untagged axioms.
+
+   An exclusion-only bracket list (`proof * [-foo]`) means "force every axiom
+   except those tagged `foo`", so the untagged axiom `A` must be FORCED into a
+   proof obligation. `A` is unprovable, so the discharging tactic fails and
+   the whole `clone` command must fail. Before the fix the untagged axiom was
+   silently kept as an assumed axiom in the clone, so this clone was accepted
+   (and `U.A` could be used to prove `false`). *)
+require import AllCore.
+
+theory T.
+  axiom A : false.
+end T.
+
+fail clone T as U proof * [-foo] by done.
+
+(* An include list (`proof * [foo]`) forces ONLY the axioms tagged `foo`:
+   the untagged `A` is intentionally not forced and stays an axiom. *)
+clone T as V proof * [foo] by done.