AMZubSqSel.v 661 Bytes
Newer Older
Benoit Viguier's avatar
Benoit Viguier committed
1
Require Import ZArith.
Benoit Viguier's avatar
Benoit Viguier committed
2
3
4

Open Scope Z.

Benoit Viguier's avatar
Benoit Viguier committed
5
Class Ops (T T': Type) (Mod: T -> T):=
Benoit Viguier's avatar
Benoit Viguier committed
6
7
8
9
10
{
  A : T -> T -> T;
  M : T -> T -> T;
  Zub : T -> T -> T;
  Sq : T -> T;
Benoit Viguier's avatar
Benoit Viguier committed
11
12
13
  C_0 : T;
  C_1 : T;
  C_121665: T;
Benoit Viguier's avatar
Benoit Viguier committed
14
  Sel25519 : Z -> T -> T -> T;
Benoit Viguier's avatar
Benoit Viguier committed
15
16
17
18
19
20
21
22
  Getbit : Z -> T' -> Z;

  Mod_ZSel25519_eq : forall b p q,  Mod (Sel25519 b p q) = Sel25519 b (Mod p) (Mod q);
  Mod_ZA_eq : forall p q,  Mod (A p q) = Mod (A (Mod p) (Mod q));
  Mod_ZM_eq : forall p q,  Mod (M p q) = Mod (M (Mod p) (Mod q));
  Mod_ZZub_eq : forall p q,  Mod (Zub p q) = Mod (Zub (Mod p) (Mod q));
  Mod_ZSq_eq : forall p,  Mod (Sq p) = Mod (Sq (Mod p));
  Mod_red : forall p,  Mod (Mod p) = (Mod p)
Benoit Viguier's avatar
Benoit Viguier committed
23
24
}.

Benoit Viguier's avatar
Benoit Viguier committed
25
26
Close Scope Z.