[mattc-try]

Closes #1223.

What: FinType.card is now an abstract operator with axiom card_spec : card = size enum (order_spec in CyclicGroup). This allows CyclicGroup clones with an abstract order, e.g. two groups sharing one order and one ZModE for a pairing (tests/fintype-shared-card.ec, which hits anomaly: CoreIncompatible on main).

Stdlib adaptations (12 files): proofs that unfolded or folded card/order use card_spec/order_spec; proof * clones that fixed enum also fix card; clones that already set card discharge card_spec. The commit message lists the affected theories.

Testing: make unit, make stdlib and make examples pass on this branch and on main (e704d26) with the provers pinned in easycrypt.project (CVC5 1.1.2, Z3 4.16.0, Alt-Ergo 2.6.4). The new test passes here and fails on main.

Breaking change / external projects (run locally against each project's current default branch):

• jasmin eclib, sha3: unaffected.
• cryptobox: one failure (Cryptobox.ec:1248) that also occurs with main, so unrelated.
• xsalsa (2 files), formosa-xmss (2 files), formosa-slh-dsa (6 files): break, and pass with small patches. Almost all are FinType clones under proof * that set enum but not card; the fix is op card <= size (<same list>) plus realize card_spec. Two slh-dsa proofs also need card_spec passed to smt.

The patches are ready; we can send them to the maintainers or provide them as merge-feat/fintype-abstract-card branches, whichever you prefer.

[oskgo]

You can already get this behaviour by introducing an abstract enum, axiomatizing it's order to be p and then instantiating the theory with enum.

I think that leaving both p and enum abstract is worse than what we have currently, but an alternative design where enum is made concrete using the choice operator could be considered.

[mattc-try]

Hello @oskgo, I agree this works for independent groups. I think perhaps the issue/PR did not make clear enough that sharing is the problem

In the pairing setting the second group must reuse the first group's exponents (theory PowZMod.ZModE <= ...), so that e.g. e (g^x) f = (e g f)^x uses the same x in both groups. To accept that, EasyCrypt checks that the two exponent subtypes have the same predicate, which requires G1.order and G2.order to be convertible. With your workaround they are size elems1 and size elems2: two different abstract lists, equal only through two axioms, so the clone is rejected. On current main:

require import AllCore List IntDiv Group.
type g1, g2.
op p : int.
axiom prime_p : prime p.
op elems1 : g1 list.
op elems2 : g2 list.
axiom size1 : size elems1 = p.
axiom size2 : size elems2 = p.
clone CyclicGroup as G1 with type group <= g1, op elems <= elems1.
lemma prime_order1 : prime G1.order. proof. by rewrite /G1.order size1 prime_p. qed.
clone G1.PowZMod as ZP with lemma prime_order <- prime_order1.
clone CyclicGroup as G2 with
  type group <= g2, op elems <= elems2,
  theory PowZMod.ZModE <= ZP.ZModE.

type `PowZMod.ZModE.exp` incompatible predicate for subtypes. The predicate for the subtype is
fun (x : int) => 0 <= x < G1.order instead of fun (x : int) => 0 <= x < order

Variants fail the same way, e.g. building the exponent ring first with p and plugging it into the group. In every variant order is size <some abstract list>, which is never convertible to anything else.

Our PR fixes this. I agree it is extra work for every FinType clone, but it is contained: the PR adapts the stdlib and examples, and we have patches for the three affected downstream projects (see #1223).

As for your alternative i'm not sure I understand your idea: do you mean card given at clone time and enum defined with choiceb? That would also fix our case, but many clones give a concrete enum today (Bool, BitWord, Word, ZModP ...) and could no longer do so, it might also need proof work, so it doesn't seem better. Could you give more details?

Happy to rework the PR in that direction if the maintainers prefer it.

[oskgo]

Making both enum and card abstract means that every instantiating clone has to instantiate both, even though choosing one essentially fixes the other up to equality (you can choose the ordering of enum, but users shouldn't rely on this). I'd really like to avoid this if possible. I guess that this argument would lead one to want both enum and card to be concrete too, since they could both be determined by the type. The counter here is that we should prefer explicit operator + axiom rather than existential axiom, which I guess is also an argument against my suggestion.

I now understand the use case of having isomorphic, but not equal, groups with a convertible theory of exponents. I agree that we should support this.

Maybe it would be better to keep the additional abstract declaration in the theory we want to be convertible? We can stop instantiating p in the clone of ZModP.ZModField in CyclicGroup and instead add an axiom stating equality. That would avoid putting an unnecessary burden on other users of FinType.

[fdupress]

@strub what are your thoughts on this? (Other than "We should really do this with typeclasses.")