fix(clone): proof * [-tag] should not drop untagged axioms

[namasikanam]

Summary

clone ... proof * [tag]. silently drops untagged axioms from the set of obligations it
forces, so a cloned theory's untagged axiom can be assumed without proof. This lets a clone
instantiate a false instance of an untagged axiom (e.g. FinType.enum_spec) and derive
false.

Root cause

check_evtags (src/ecTheoryReplay.ml) decides whether an axiom is forced by mapping the
directive's tag test over the axiom's own tag list src. For an untagged axiom src = [],
List.mem true (List.map _ []) = false, so it is never forced — and the correct default
(dfl) is never consulted.

Fix (src/ecTheoryReplay.ml)

Rewrite the tag-matching so the directive is folded starting from the default dfl, testing
membership of each directive tag in the axiom's src. Untagged axioms now correctly fall
back to the default (forced), while explicit [-tag] exclusions still apply to tagged
axioms.

Test

tests/ko/clone-proofstar-tagdrop.ec (must-fail): a proof * [-dummy] clone that previously
dropped an untagged axiom is now rejected. Contrast: the no-bracket proof * form already
rejected, confirming this was a genuine drop rather than the by-design "clone assumes its
axioms" behaviour.

[strub]

I don't understand the problem here:

require import AllCore.

theory T.
  axiom A : false.
end T.

clone T as U proof * [foo].

print U.

gives:

theory U.
  (* import *) axiom A: false.
end U.

[oskgo]

Yeah. This one isn't a soundness issue. I would consider it unexpected that proof * [-foo] excludes not just axioms tagged foo but also those without a tag though.

[namasikanam]

I'm trying to understand and getting confused. What are the expected behavior of clone ... proof * [tag] and clone ... proof * [-tag]?

[strub]

I'm trying to understand and getting confused. What are the expected behavior of clone ... proof * [tag] and clone ... proof * [-tag]?

• proof * [tag] -> realize the axioms tagged with foo
• proof * [-tag] -> realize the axioms not tagged with foo

As @oskgo said, with your PR, proof * [-tag] remove the untagged lemmas from the realization set.

Closing this PR. This is not a soundness issue and this is the desired behavior.

[oskgo]

@strub It's the other way around. The current behaviour is that proof * [-tag] excludes the untagged axioms from the realization set. The PR changes it so only the axioms tagged by tag are removed.

[fdupress]

I fixed the title, but I'll leave it to @namasikanam to fix the description. Please do check those for accuracy—it helps with triaging and review.

This is still not a logical soundness bug, although it may be a "perceptual soundness" issue: the axioms still exist, they are simply not discharged when a reader/reviewer might expect them to be.

[strub]

Ah yes I tested with this PR binary.