module GroupTests where

import Protolude

import Curve
import GaloisField
import Group
import Group.Field
import Math.NumberTheory.Primes.Testing
import Test.Tasty
import Test.Tasty.HUnit
import Test.Tasty.QuickCheck

identities :: Eq a => (a -> a -> a) -> a -> a -> Bool
identities op e x = op x e == x && op e x == x

inverses :: Eq a => (a -> a -> a) -> (a -> a) -> a -> a -> Bool
inverses op neg e x = op x (neg x) == e && op (neg x) x == e

commutativity :: Eq a => (a -> a -> a) -> a -> a -> Bool
commutativity op x y = op x y == op y x

associativity :: Eq a => (a -> a -> a) -> a -> a -> a -> Bool
associativity op x y z = op x (op y z) == op (op x y) z

groupAxioms :: forall g . Group g => g -> TestTree
groupAxioms _ = testGroup "Group axioms"
  [ testCase "identity closure" $
    def (mempty :: g) @?= True
  , testProperty "point closure" $
    (def :: g -> Bool)
  , testProperty "inversion closure" $
    def . (inv :: g -> g)
  , testProperty "addition closure" $
    (.) def . ((<>) :: g -> g -> g)
  , testProperty "doubling closure" $
    def . (join (<>) :: g -> g)
  , testProperty "multiplication closure" $
    def . (flip mul' (-3) :: g -> g)
  , testProperty "identity" $
    identities ((<>) :: g -> g -> g) mempty
  , testProperty "inverses" $
    inverses ((<>) :: g -> g -> g) inv mempty
  , testProperty "commutativity" $
    commutativity ((<>) :: g -> g -> g)
  , testProperty "associativity" $
    associativity ((<>) :: g -> g -> g)
  ]

hasseTheorem :: Integer -> Integer -> Integer -> Bool
hasseTheorem h r q = join (*) (h * r - q - 1) <= 4 * q

doubleIdentities :: (Eq a, Eq b) => (a -> b) -> (b -> a) -> a -> b -> Bool
doubleIdentities f t e e' = f e == e' && t e' == e

doubleDefined :: (a -> Bool) -> (b -> Bool) -> (b -> a) -> b -> Bool
doubleDefined d d' t x = d' x && d (t x)

doubleInverses :: (Eq a, Eq b) => (a -> b) -> (b -> a) -> b -> Bool
doubleInverses f t x = f (t x) == x && t (f (t x)) == t x

doubleHomeomorphism :: (Eq a, Eq b) => (a -> a) -> (b -> b) -> (a -> b) -> (b -> a) -> b -> Bool
doubleHomeomorphism op op' f t x = t (op' x) == op (t x) && f (op (t x)) == op' x

curveParameters :: forall f c e q r . (Curve f 'Affine e q r, Curve f c e q r)
  => Point f c e q r -> Integer -> Integer -> Integer -> TestTree
curveParameters g h q r = testGroup "Curve parameters"
  [ testCase "generator is parametrised" $
    gen @?= g
  , testCase "cofactor is parametrised" $
    cof g @?= h
  , testCase "characteristic is parametrised" $
    Curve.char g @?= q
  , testCase "order is parametrised" $
    Group.order g @?= r
  , testCase "characteristic is prime" $
    isPrime q @?= True
  , testCase "discriminant is nonzero" $
    disc g /= 0 @?= True
  , testCase "generator is well-defined" $
    def g @?= True
  , testCase "generator is in cyclic subgroup" $
    mul' g r @?= mempty
  , testCase "cyclic subgroup has prime order" $
    isPrime r @?= True
  , testCase "hasse theorem holds" $
    hasseTheorem h r (GaloisField.order (witness :: q)) @?= True
  , testCase "affine transformation is doubly identity-preserving" $
    doubleIdentities fromA (toA :: Point f c e q r -> Point f 'Affine e q r) mempty mempty @?= True
  , testProperty "affine transformation is doubly well-defined" $
    doubleDefined def def (toA :: Point f c e q r -> Point f 'Affine e q r)
  , testProperty "affine transformation is doubly invertible" $
    doubleInverses fromA (toA :: Point f c e q r -> Point f 'Affine e q r)
  , testProperty "affine transformation is doubly homeomorphic" $
    doubleHomeomorphism (flip mul 3) (flip mul 3) fromA (toA :: Point f c e q r -> Point f 'Affine e q r)
  ]

test :: (Curve f c e q r, Curve f 'Affine e q r)
  => TestName -> Point f c e q r -> Integer -> Integer -> Integer -> TestTree
test s g h q r = testGroup s [groupAxioms g, curveParameters g h q r]

fieldParameters :: forall q r . FGroup r q
  => Element r q -> Integer -> Integer -> Integer -> TestTree
fieldParameters g h q r = testGroup "Group parameters"
  [ testCase "generator is parametrised" $
    gen @?= g
  , testCase "characteristic is parametrised" $
    GaloisField.char (witness :: q) @?= q
  , testCase "order is parametrised" $
    Group.order g @?= r
  , testCase "characteristic is prime" $
    isPrime q @?= True
  , testCase "generator is well-defined" $
    def g @?= True
  , testCase "generator is in cyclic subgroup" $
    mul' g r @?= mempty
  , testCase "cyclic subgroup has prime order" $
    isPrime r @?= True
  , testCase "hasse theorem holds" $
    hasseTheorem h r (GaloisField.order (witness :: q)) @?= True
  ]

test' :: FGroup r q
  => TestName -> Element r q -> Integer -> Integer -> Integer -> TestTree
test' s g h q r = testGroup s [groupAxioms g, fieldParameters g h q r]