Axiom nonce reuse make axiom tracking difficult

[xrchz]

Thm.mk_axiom_thm accepts a caller-supplied Nonce.t, but the nonce is neither consumed nor permanently bound to the axiom proposition. The same nonce can therefore introduce multiple unrelated propositions.

I am unsure whether this is best classified as a soundness issue or as an API/design issue, but as it stands there isn't a clean story for axiom tracking that one might have hoped for from Tag.

To see what I mean, consider running:

   open HolKernel;

   val n = Nonce.mk "ETA_AX";

   (* Register n for the genuine standard ETA axiom. *)
   val eta =
       Thm.mk_axiom_thm (n, Thm.concl boolTheory.ETA_AX);

   val _ = Theory.register_replayed_axiom eta;

   (* Reuse n for an unrelated proposition. *)
   val bad = Thm.mk_axiom_thm (n, boolSyntax.F);

This would enable:

  null (Thm.hyp bad);                    (* true *)
  Term.aconv (Thm.concl bad) boolSyntax.F;
  Tag.dest_tag (Thm.tag bad);            (* ([], ["ETA_AX"]) *)
  Theory.uptodate_thm bad;                (* true *)

Theory.current_axioms() also does not show the replayed-axiom registry.

I'm guessing with a name like "nonce" the intention for this mechanism was more to be actually one-shot, e.g.:

1. Nonce.mk name creates a fresh nonce.
2. The first mk_axiom_thm (n, proposition) atomically binds n to that proposition.
3. Any later call to mk_axiom_thm with n fails.
4. register_replayed_axiom verifies that the theorem's conclusion matches the proposition already bound to its nonce.
5. Propagating the nonce through theorem tags remains unrestricted.

(Obviously, consumption should be thread-safe and should not be undone by Context.restore.)

Alternatively, mk_axiom_thm could accept (name, proposition) and mint the nonce internally.

[xrchz]

A few additional observations from a source audit:

• This does not depend on the proof-replay registry. In a fresh ordinary theory, the same problem is reachable through the older public APIs alone:

  val _ = Theory.new_theory "nonce_reuse";
  val ax = Theory.new_axiom
      ("BOOL_CASES_AX", Thm.concl boolTheory.BOOL_CASES_AX);
  val [n] = Tag.axioms_of (Thm.tag ax);
  val bad = Thm.mk_axiom_thm (n, boolSyntax.F);

  Here the proposition registered for n is exactly the standard Boolean-cases axiom, but bad is [] |- F with no oracle tag. While building bool from source, the exact original nonce from the genuine BOOL_CASES_AX can likewise be extracted and reused. (A normally disk-loaded boolTheory.BOOL_CASES_AX has lost its nonce, so direct extraction from that loaded theorem does not work.)

• Theory.uptodate_thm bad succeeds, and Theory.save_thm accepts it while the registering theory is current, so the impact is not limited to misleading tag display.

• There is a close historical precedent: commit 2b19fe8 changed mk_oracle_thm so it no longer accepted a caller-supplied tag, specifically to prevent reusing an axiom tag to manufacture [] |- F: 2b19fe8

This makes the current behaviour look like a soundness issue rather than only an axiom-tracking inconvenience. Hardening only register_replayed_axiom would not close the new_axiom -> axioms_of -> mk_axiom_thm route. Removing mk_axiom_thm from FinalThm, or enforcing atomic one-shot nonce binding as suggested above, would address the capability reuse directly.