mattc-try · Oct 30, 2026
diff --git a/examples/ChaChaPoly/chacha_poly.ec b/examples/ChaChaPoly/chacha_poly.ec
@@ -89,8 +89,10 @@ theory C.
 
   clone FinType with 
     type t  = counter,
-    op enum = List.map ofintd (iota_ 0 (max_counter + 1))
+    op enum = List.map ofintd (iota_ 0 (max_counter + 1)),
+    op card = size (List.map ofintd (iota_ 0 (max_counter + 1)))
     proof *.
+  realize card_spec by rewrite /card /enum.
   realize enum_spec.  
   proof.
     move=> c; rewrite count_uniq_mem.

diff --git a/examples/MEE-CBC/FunctionalSpec.ec b/examples/MEE-CBC/FunctionalSpec.ec
@@ -32,11 +32,13 @@ qed.
 clone import Word as Block with
   type Alphabet.t    <- octet,
   op   Alphabet.enum <- Octet.octets,
+  op   Alphabet.card <- Octet.card,
   op   n             <- 16
 rename "word" as "block"
 rename "Word" as "Block"
 proof *.
 realize Alphabet.enum_spec by exact/Octet.enum_spec.
+realize Alphabet.card_spec by exact/Octet.card_spec.
 realize ge0_n by trivial.
 
 abbrev dblock = DBlock.dunifin.
@@ -125,11 +127,13 @@ instance bring with block
 clone import Word as Tag with
   type Alphabet.t    <- octet,
   op   Alphabet.enum <- Octet.octets,
+  op   Alphabet.card <- Octet.card,
   op   n             <- 32
 rename "word" as "tag"
 rename "Word" as "Tag"
 proof *.
 realize Alphabet.enum_spec by exact/Octet.enum_spec.
+realize Alphabet.card_spec by exact/Octet.card_spec.
 realize ge0_n by trivial.
 
 (** Messages are just octet lists **)

diff --git a/tests/fintype-shared-card.ec b/tests/fintype-shared-card.ec
@@ -0,0 +1,22 @@
+require import AllCore IntDiv Group.
+
+type g1, g2.
+
+op p : int.
+
+axiom prime_p : prime p.
+
+clone CyclicGroup as G1 with
+  type group <= g1,
+  op order <= p.
+
+clone G1.PowZMod as ZP with
+  lemma prime_order <- prime_p.
+
+clone CyclicGroup as G2 with
+  type group <= g2,
+  op order <= p,
+  theory PowZMod.ZModE <= ZP.ZModE.
+
+lemma order_eq : G1.order = G2.order.
+proof. by []. qed.
diff --git a/theories/algebra/Group.ec b/theories/algebra/Group.ec
@@ -301,7 +301,7 @@ op log (x : group) = choiceb (log_spec x) 0.
 
 lemma gt0_order : 0 < order.
 proof.
-rewrite /order ltr_neqAle size_ge0 /= eq_sym size_eq0.
+rewrite order_spec ltr_neqAle size_ge0 /= eq_sym size_eq0.
 by apply/negP=> z_elems; have := elemsP g; rewrite z_elems.
 qed.
 
@@ -321,7 +321,7 @@ have nz: forall k, 1 <= k < order => g ^ k <> e.
   * rewrite &(uniq_perm_eq) ?(undup_uniq, elems_uniq).
     move=> x; rewrite elemsP /= mem_undup; apply/mapP.
     by case: (mg x)=> l mg_x; exists l; rewrite mem_range.
-  move/perm_eq_size; rewrite -/order => orderE.
+  move/perm_eq_size; rewrite -order_spec => orderE.
   rewrite -(@ltrr order) {1}orderE (ler_lt_trans _ _ _ (size_undup _)).
   by rewrite size_map size_range /= ler_maxr 1:ltrW /=; case: rg_k.
 rewrite map_inj_in_uniq 2:range_uniq => /= i j.
@@ -351,7 +351,7 @@ have /perm_eq_size := perm_filterC (mem s) elems.
 have: perm_eq (filter (mem s) elems) (filter (mem elems) s).
 + rewrite &(uniq_perm_eq) ?filter_uniq ?(elems_uniq, uniq_cg).
   by move=> x; rewrite !mem_filter andbC.
-rewrite -/order eq_sym size_cat => /perm_eq_size ->.
+rewrite -order_spec eq_sym size_cat => /perm_eq_size ->.
 rewrite eq_in_filter_predT => [x _|]; 1: by rewrite elemsP.
 rewrite size_map size_range /= ler_maxr 1:ge0_order.
 rewrite -{1}(addr0 order) eq_sym => /addrI.
@@ -621,6 +621,7 @@ import ZModpRing.
 clone CyclicGroup as ZModC with
   type group <- zmod,
   op   elems <- map ZModRing.inzmod (range 0 order),
+  op   order <- order,
   op   e     =  ZModRing.zero,
   op   ( * ) =  ZModRing.( + ),
   op   inv   =  ZModRing.([-]),
@@ -636,6 +637,9 @@ rewrite !mem_range => rgx rgy /= /(congr1 asint).
 by rewrite !inzmodK !pmod_small.
 qed.
 
+realize order_spec.
+proof. by rewrite size_map size_range; smt(ge2_order). qed.
+
 realize mulcC by apply: ZModRing.ZModpRing.addrC.
 realize mul1c by apply: ZModRing.ZModpRing.add0r.
 realize mulcA by apply: ZModRing.ZModpRing.addrA.

diff --git a/theories/algebra/ZModP.ec b/theories/algebra/ZModP.ec
@@ -249,7 +249,8 @@ proof. by move=> ih n; rewrite -(asintK n) &(ih) rg_asint. qed.
 theory DZmodP.
 clone include MFinite with
   type t <- zmod,
-    op Support.enum = map inzmod (range 0 p)
+    op Support.enum = map inzmod (range 0 p),
+    op Support.card = p
 
   proof *.
 
@@ -262,10 +263,13 @@ rewrite !mem_range => rgm rgn /(congr1 asint).
 by rewrite !inzmodK !pmod_small.
 qed.
 
+realize Support.card_spec.
+proof. by rewrite /Support.card /Support.enum size_map size_range; smt(ge2_p). qed.
+
 require import DInterval.
 
 lemma cardE : Support.card = p.
-proof. by rewrite /Support.card size_map size_range; smt(ge2_p). qed.
+proof. by rewrite /Support.card. qed.
 
 lemma dzmodE : dunifin = dmap [0..p-1] inzmod.
 proof.

diff --git a/theories/core/Bool.ec b/theories/core/Bool.ec
@@ -23,5 +23,5 @@ clone FinType as BoolFin with
   type t    <- bool,
   op enum <- List.(::) true (List.(::) false List."[]"),
   op card <- 2
-proof enum_spec by case.
+proof enum_spec by case, card_spec by done.
 
diff --git a/theories/crypto/ROM.eca b/theories/crypto/ROM.eca
@@ -160,8 +160,9 @@ clone import FinType with
 import Lazy.
 
 clone include FiniteEager with
-  op enum <- enum
-proof * by exact/enum_spec.
+  op enum <- enum,
+  op card <- card
+proof * by (exact/enum_spec || exact/card_spec).
 
 section.
 declare module D <: Distinguisher { -LRO, -ERO }.

diff --git a/theories/datatypes/BitWord.eca b/theories/datatypes/BitWord.eca
@@ -15,7 +15,7 @@ clone include Word with
   op   n             <- n,
   op   dchar         <- false
 
-proof Alphabet.* by case, ge0_n by apply/ltzW/gt0_n.
+proof Alphabet.* by (done || case), ge0_n by apply/ltzW/gt0_n.
 
 (* -------------------------------------------------------------------- *)
 op zerow: word = offun (fun i => false).

diff --git a/theories/datatypes/Tuple.eca b/theories/datatypes/Tuple.eca
@@ -52,7 +52,7 @@ move=> i le0_i ih; rewrite wordnS // size_flatten /=.
 rewrite -map_comp (@eq_map _ (fun x => card^i)).
   by move=> x /=; rewrite /(\o) size_map.
 rewrite Bigint.sumzE big_map /(\o) /predT /=.
-by rewrite Bigint.big_constz count_predT -/card mulzC exprS.
+by rewrite Bigint.big_constz count_predT -card_spec mulzC exprS.
 qed.
 
 (* -------------------------------------------------------------------- *)

diff --git a/theories/datatypes/Word.eca b/theories/datatypes/Word.eca
@@ -183,15 +183,19 @@ qed.
 (* -------------------------------------------------------------------- *)
 clone Tuple as Enum with
   type t <- t,
-    op Support.enum <- enum
-proof * by exact/enum_spec.
+    op Support.enum <- enum,
+    op Support.card <- card
+proof * by (exact/enum_spec || exact/card_spec).
 
 (* -------------------------------------------------------------------- *)
 clone include FinType with
   type t    <- word,
-  op enum = List.map mkword (Enum.wordn n)
+  op enum = List.map mkword (Enum.wordn n),
+  op card = size (List.map mkword (Enum.wordn n))
 proof * rename [op] "enum" as "words".
 
+realize card_spec by rewrite /card /words.
+
 realize enum_spec.
 proof.
 move=> x; rewrite count_map -(Enum.word_spec n (ofword x) _).
@@ -209,7 +213,7 @@ clone MFinite as DWord with
   type t <- word,
   op   Support.enum = List.map mkword (Enum.wordn n),
   op   Support.card <- card
-proof Support.enum_spec by exact/enum_spec.
+proof Support.enum_spec by exact/enum_spec, Support.card_spec by exact/card_spec.
 
 (* -------------------------------------------------------------------- *)
 theory ListSample.

diff --git a/theories/distributions/DBool.ec b/theories/distributions/DBool.ec
@@ -12,7 +12,7 @@ clone include Distr.MFinite with
   rename "dunifinE" as "dboolE_count"
   rename "dunifin" as "dbool"
   rename "cunifin" as "cdbool"
-proof Support.enum_spec by case.
+proof Support.enum_spec by case, Support.card_spec by done.
 
 lemma dboolE (E : bool -> bool):
   mu dbool E =   (if E true  then 1%r/2%r else 0%r)

diff --git a/theories/distributions/Distr.ec b/theories/distributions/Distr.ec
@@ -894,11 +894,11 @@ clone import FinType as Support with type t <- t.
 op dunifin : t distr = MUniform.duniform enum.
 
 lemma dunifin1E (x : t) : mu1 dunifin x = 1%r / card%r.
-proof. by rewrite MUniform.duniform1E enumP /= undup_id // enum_uniq. qed.
+proof. by rewrite card_spec MUniform.duniform1E enumP /= undup_id // enum_uniq. qed.
 
 lemma dunifinE (E : t -> bool) :
   mu dunifin E = (count E enum)%r / card%r.
-proof. by rewrite MUniform.duniformE ?undup_id // enum_uniq. qed.
+proof. by rewrite card_spec MUniform.duniformE ?undup_id // enum_uniq. qed.
 
 lemma supp_dunifin x: x \in dunifin.
 proof.
@@ -908,7 +908,7 @@ qed.
 lemma dunifin_ll : is_lossless dunifin.
 proof.
 rewrite MUniform.duniform_ll -size_eq0 -lt0n.
-  by rewrite size_ge0. by rewrite Support.card_gt0.
+  by rewrite size_ge0. by rewrite -Support.card_spec Support.card_gt0.
 qed.
 
 lemma dunifin_uni : is_uniform dunifin.
@@ -2377,8 +2377,8 @@ lemma tofunK ['u] us :
   size us = FinT.card => offun<:'u> (tofun us) = us.
 proof.
 move=> sz_us; apply/(eq_from_nth witness).
-- by rewrite size_map sz_us.
-rewrite size_map -/FinT.card => i rg_i.
+- by rewrite size_map sz_us FinT.card_spec.
+rewrite size_map => i rg_i.
 rewrite /offun (@nth_map witness) // /tofun.
 by rewrite index_uniq // FinT.enum_uniq.
 qed.
@@ -2389,7 +2389,7 @@ proof.
 apply: eq_distr => f; rewrite dfun1E_djoin dmap1E /(\o) /pred1.
 apply: mu_eq_support => l /supp_djoinmap [hsz _] /=.
 apply eq_iff; split => [-> | <-]; first by apply offunK.
-by rewrite -/(offun (tofun l)) tofunK // -hsz.
+by rewrite -/(offun (tofun l)) tofunK // FinT.card_spec -hsz.
 qed.
 
 lemma dfun_supp ['u] (d : t -> 'u distr) (f : t -> 'u) :
@@ -2431,7 +2431,7 @@ rewrite -dmapE; congr; apply/eq_distr=> f.
 rewrite dfun1E_djoin dmap1E &(mu_eq_support) /pred1.
 move=> us /supp_djoinmap [/eq_sym sz_us /allP h] @/(\o) /=.
 apply/eq_iff; split => [->|]; first by apply/offunK.
-by move/(congr1 offun); rewrite tofunK.
+by move/(congr1 offun); rewrite tofunK // FinT.card_spec.
 qed.
 
 lemma dfunE ['u] du (p : t -> 'u -> bool) :

diff --git a/theories/structure/FinType.ec b/theories/structure/FinType.ec
@@ -7,7 +7,9 @@ type t.
 
 op enum : t list.
 
-op card : int = size enum.
+op card : int.
+
+axiom card_spec : card = size enum.
 
 axiom enum_spec : forall x, count (pred1 x) enum = 1.
 
@@ -23,7 +25,7 @@ proof. by apply/count_mem_uniq=> x; rewrite enumP enum_spec. qed.
 
 lemma card_gt0 : 0 < card.
 proof.
-rewrite /card; have: mem enum witness by rewrite enumP.
+rewrite card_spec; have: mem enum witness by rewrite enumP.
 by case: enum=> //= x s _; rewrite addzC ltzS size_ge0.
 qed.
 
@@ -49,7 +51,7 @@ apply: uniq_perm_eq.
 qed.
 
 lemma card_size_to_seq : card = size (Finite.to_seq<:t> predT).
-proof. by apply/perm_eq_size/perm_eq_enum_to_seq. qed.
+proof. by rewrite card_spec; apply/perm_eq_size/perm_eq_enum_to_seq. qed.
 end FinType.
 
 (* ==================================================================== *)
@@ -61,9 +63,13 @@ clone FinType as FT2 with type t <- t2.
 
 clone include FinType
   with type t    = t1 * t2,
-         op enum = allpairs (fun x y => (x, y)) FT1.enum FT2.enum
+         op enum = allpairs (fun x y => (x, y)) FT1.enum FT2.enum,
+         op card = FT1.card * FT2.card
   proof *.
 
+realize card_spec.
+proof. by rewrite /card /enum FT1.card_spec FT2.card_spec size_allpairs. qed.
+
 realize enum_spec.
 proof.
 case=> x y; rewrite count_uniq_mem.