fix(clone): proof * [-tag] should force (realize) untagged axioms

[namasikanam]

Summary

clone ... proof * [-tag]. leaves untagged axioms as they are. This lets a clone
instantiate a false instance of an untagged axiom (e.g. FinType.enum_spec) and derive
false (see the example below).

require import AllCore List FinType.


clone FinType as F with
  type t <- int,
  op enum <- [0]
  proof * [-dummy] by smt().

lemma bad : false.
proof.
have h := F.enum_spec 1.                               (* forall x, count (pred1 x) [0] = 1 *)
have : count (pred1 1) [0] = 1 by apply h.     (* count (pred1 1) [0] = 0, not 1    *)
by rewrite /count /pred1 /=.
qed.

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/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.

[namasikanam]

I've fixed the PR description and commit message. I think it's indeed a soundness issue. Look at the example in the PR description.

[oskgo]

Even though it looks like you have an axiom-free proof of false here, you don't actually have one.

In your example if you do print axiom or print the entire theory you'll see that the false enum_spec axiom is still here. It would be a soundness issue if it turned the axiom into a lemma or removed it without requiring you to prove it during the clone.

I like François' term of "perceptual soundness". The logic is still solid, but the presentation is not.

[fdupress]

Just to reinforce the point, the following is not a soundness issue.

axiom toto: false.

lemma titi: false by exact: toto.

The example in your PR description is that, with a rug placed over the axiom toto bit. But we already have mechanisms to lift that kind of rugs. (print axiom, for one.)

I do dislike the fact that the current behaviour is not what one would expect, which means that we currently expect the user to use print axiom to be convinced that we didn't hide anything. But that is not a soundness issue.