Abstract Cyclic-Group Parameters

GroupParam axiomatizes a finite cyclic group of prime order together with its scalar field, packaged as a single structure so protocol definitions can quantify over an arbitrary such group. The carrier G is the group; Scalar is the field ℤ/qℤ where q = |g|; exp x = gᣞ is generator exponentiation and groupExp h x is exponentiation of an arbitrary element. The structure records the group and scalar-field axioms as fields, so a concrete instantiation discharges them once and every downstream proof reasons purely equationally.

This is the abstract group interface used by the UC examples over discrete-log groups (Pedersen commitment, dual-mode oblivious transfer).

structure CatCrypt.Examples.GroupParam : Type 1

Parameters for a finite cyclic group of prime order together with its scalar field ℤ/qℤ. The carrier G is the group with generator generator; Scalar is the field of exponents; exp is generator exponentiation and groupExp is exponentiation of an arbitrary group element. The remaining fields record the group and field axioms needed for equational reasoning.

• G : Type

  The group carrier.

• Scalar : Type

  The scalar field ℤ/qℤ, where q is the order of the generator.

• finG : Fintype self.G

  G is finite.

• neG : Nonempty self.G

  G is nonempty.

• decG : DecidableEq self.G

  G has decidable equality.

• finScalar : Fintype self.Scalar

  Scalar is finite.

• neScalar : Nonempty self.Scalar

  Scalar is nonempty.

• decScalar : DecidableEq self.Scalar

  Scalar has decidable equality.

• generator : self.G

  The generator g.

• identity : self.G

  The group identity element.

• exp : self.Scalar → self.G

  Generator exponentiation g ^ x.

• groupExp : self.G → self.Scalar → self.G

  Exponentiation of an arbitrary element h ^ x.

• scalarAdd : self.Scalar → self.Scalar → self.Scalar

  Scalar addition.

• scalarMul : self.Scalar → self.Scalar → self.Scalar

  Scalar multiplication.

• scalarSub : self.Scalar → self.Scalar → self.Scalar

  Scalar subtraction.

• scalarDiv : self.Scalar → self.Scalar → self.Scalar

  Scalar division (well-defined by primality of the order).

• scalarNeg : self.Scalar → self.Scalar

  Scalar negation.

• scalarZero : self.Scalar

  The additive identity scalar.

• groupMul : self.G → self.G → self.G

  Group multiplication.

• groupInv : self.G → self.G

  Group inverse.

• scalarOne : self.Scalar

  The multiplicative identity scalar.

• exp_add (x y : self.Scalar) : self.exp (self.scalarAdd x y) = self.groupMul (self.exp x) (self.exp y)

  Generator exponentiation is a homomorphism: g ^ (x + y) = gᣞ · gᣩ.

• exp_zero : self.exp self.scalarZero = self.identity

  g ^ 0 = 1.

• div_mul_cancel (x y : self.Scalar) : y ≠ self.scalarZero → self.scalarMul (self.scalarDiv x y) y = x

  Division is a right inverse to multiplication: (x / y) · y = x for y ≠ 0.

• groupExp_generator (x : self.Scalar) : self.exp x = self.groupExp self.generator x

  Generator exponentiation is a special case of general exponentiation.

• groupExp_exp (w e : self.Scalar) : self.groupExp (self.exp w) e = self.exp (self.scalarMul w e)

  Exponentiation of a power: (g ^ w) ^ e = g ^ (w · e).

• groupExp_one (h : self.G) : self.groupExp h self.scalarOne = h

  h ^ 1 = h.

• groupExp_add (h : self.G) (a b : self.Scalar) : self.groupExp h (self.scalarAdd a b) = self.groupMul (self.groupExp h a) (self.groupExp h b)

  General exponentiation is additive in the exponent.

• scalarSub_ne_zero (a b : self.Scalar) : a ≠ b → self.scalarSub a b ≠ self.scalarZero

  Distinct scalars have nonzero difference.

• groupMul_identity (a : self.G) : self.groupMul a self.identity = a

  Right identity for group multiplication.

• identity_groupMul (a : self.G) : self.groupMul self.identity a = a

  Left identity for group multiplication.

• groupMul_inv (a : self.G) : self.groupMul a (self.groupInv a) = self.identity

  Right inverse for group multiplication.

• inv_groupMul (a : self.G) : self.groupMul (self.groupInv a) a = self.identity

  Left inverse for group multiplication.

• groupMul_assoc (a b c : self.G) : self.groupMul (self.groupMul a b) c = self.groupMul a (self.groupMul b c)

  Group multiplication is associative.

• groupExp_zero (h : self.G) : self.groupExp h self.scalarZero = self.identity

  h ^ 0 = 1.

• scalarMul_one (a : self.Scalar) : self.scalarMul a self.scalarOne = a

  a · 1 = a.

• groupInv_groupExp (h : self.G) (e : self.Scalar) : self.groupInv (self.groupExp h e) = self.groupExp h (self.scalarNeg e)

  Inverse of a power: (h ^ e)⁻¹ = h ^ (-e).

• scalarSub_eq (a b : self.Scalar) : self.scalarSub a b = self.scalarAdd a (self.scalarNeg b)

  Subtraction as addition of the negation.

• scalarAdd_neg (a : self.Scalar) : self.scalarAdd a (self.scalarNeg a) = self.scalarZero

  Right negation cancels: a + (-a) = 0.

• exp_surj (h : self.G) : ∃ (x : self.Scalar), self.exp x = h

  Generator exponentiation is surjective.

• exp_inj (x y : self.Scalar) : self.exp x = self.exp y → x = y

  Generator exponentiation is injective (prime order).

• scalarAdd_comm (a b : self.Scalar) : self.scalarAdd a b = self.scalarAdd b a

  Scalar addition is commutative.

• scalarAdd_assoc (a b c : self.Scalar) : self.scalarAdd (self.scalarAdd a b) c = self.scalarAdd a (self.scalarAdd b c)

  Scalar addition is associative.

• scalarMul_add (a b c : self.Scalar) : self.scalarMul a (self.scalarAdd b c) = self.scalarAdd (self.scalarMul a b) (self.scalarMul a c)

  Scalar multiplication distributes over addition on the left.

• scalarAdd_mul (a b c : self.Scalar) : self.scalarMul (self.scalarAdd a b) c = self.scalarAdd (self.scalarMul a c) (self.scalarMul b c)

  Scalar multiplication distributes over addition on the right.

• scalarMul_comm (a b : self.Scalar) : self.scalarMul a b = self.scalarMul b a

  Scalar multiplication is commutative.

• scalarAdd_zero (a : self.Scalar) : self.scalarAdd a self.scalarZero = a

  Right additive identity: a + 0 = a.

• scalarZero_add (a : self.Scalar) : self.scalarAdd self.scalarZero a = a

  Left additive identity: 0 + a = a.

• scalarNeg_add (a : self.Scalar) : self.scalarAdd (self.scalarNeg a) a = self.scalarZero

  Left negation cancels: (-a) + a = 0.

• scalarNeg_zero : self.scalarNeg self.scalarZero = self.scalarZero

  Negation of zero is zero.

• scalarNeg_add_distrib (a b : self.Scalar) : self.scalarNeg (self.scalarAdd a b) = self.scalarAdd (self.scalarNeg a) (self.scalarNeg b)

  Negation distributes over addition.

• scalarMul_zero (a : self.Scalar) : self.scalarMul a self.scalarZero = self.scalarZero

  a · 0 = 0.

• scalarZero_mul (a : self.Scalar) : self.scalarMul self.scalarZero a = self.scalarZero

  0 · a = 0.

• mul_div_cancel (a b : self.Scalar) : b ≠ self.scalarZero → self.scalarDiv (self.scalarMul a b) b = a

  Division cancels multiplication: (a · b) / b = a for b ≠ 0.

• scalarMul_assoc (a b c : self.Scalar) : self.scalarMul (self.scalarMul a b) c = self.scalarMul a (self.scalarMul b c)

  Scalar multiplication is associative.

Derived scalar-field lemmas

theorem CatCrypt.Examples.scalarMul_neg (gp : GroupParam) (a b : gp.Scalar) : gp.scalarMul a (gp.scalarNeg b) = gp.scalarNeg (gp.scalarMul a b)

Multiplication distributes over negation: a · (-b) = -(a · b).

theorem CatCrypt.Examples.scalarNeg_mul (gp : GroupParam) (a b : gp.Scalar) : gp.scalarMul (gp.scalarNeg a) b = gp.scalarNeg (gp.scalarMul a b)

Multiplication distributes over negation on the left: (-a) · b = -(a · b).