module Crypto.Lol.Tests.TensorTests where
import Crypto.Lol.Tests
import Crypto.Lol.Utils.ShowType
import Crypto.Lol
import Crypto.Lol.Cyclotomic.Tensor
import Control.Applicative
import Data.Maybe
import qualified Test.Framework as TF
tensorTests1 :: forall t m r . _ => Proxy '(m,r) -> Proxy t -> TF.Test
tensorTests1 _ _ =
let ptmr = Proxy :: Proxy '(t,m,r)
in testGroup (showType ptmr) $ ($ ptmr) <$> [
genTestArgs "fmapT comparison" prop_fmapT,
genTestArgs "fmap comparison" prop_fmap,
nestGroup "GInv.G == id" [
genTestArgs "Pow basis" prop_ginv_pow,
genTestArgs "Dec basis" prop_ginv_dec,
genTestArgs "CRT basis" prop_ginv_crt],
genTestArgs "CRTInv.CRT == id" prop_crt_inv,
genTestArgs "LInv.L == id" prop_l_inv,
genTestArgs "Scalar" prop_scalar_crt,
nestGroup "G commutes with L" [
genTestArgs "Dec basis" prop_g_dec,
genTestArgs "CRT basis" prop_g_crt],
genTestArgs "Tw and Em ID for equal indices" prop_twEmID
]
tensorTests2 :: forall t m m' r . _ => Proxy '(m,m',r) -> Proxy t -> TF.Test
tensorTests2 _ _ =
let ptmr = Proxy :: Proxy '(t,m,m',r)
in testGroup (showType ptmr) $ ($ ptmr) <$> [
nestGroup "Tw.Em == id" [
genTestArgs "Pow basis" prop_trem_pow,
genTestArgs "Dec basis" prop_trem_dec,
genTestArgs "CRT basis" prop_trem_crt],
nestGroup "Em commutes with L" [
genTestArgs "Dec basis" prop_embed_dec,
genTestArgs "CRT basis" prop_embed_crt],
nestGroup "Tw commutes with L" [
genTestArgs "Dec basis" prop_twace_dec,
genTestArgs "CRT basis" prop_twace_crt],
nestGroup "Twace invariants" [
genTestArgs "Invar1 Pow basis" prop_twace_invar1_pow,
genTestArgs "Invar1 Dec basis" prop_twace_invar1_dec,
genTestArgs "Invar1 CRT basis" prop_twace_invar1_crt,
genTestArgs "Invar2 Pow/Dec basis" prop_twace_invar2_powdec,
genTestArgs "Invar2 CRT basis" prop_twace_invar2_crt]
]
prop_fmapT :: _ => t m r -> Test '(t,m,r)
prop_fmapT x = test $ fmapT id x == x \\ witness entailEqT x \\ witness entailIndexT x
prop_fmap :: _ => t m r -> Test '(t,m,r)
prop_fmap x = test $ (fmap id x) == x \\ witness entailEqT x \\ witness entailIndexT x
prop_ginv_pow :: _ => t m r -> Test '(t,m,r)
prop_ginv_pow x = test $ (fromMaybe (error "could not divide by G in prop_ginv_pow") $
divGPow $ mulGPow x) == x \\ witness entailEqT x
prop_ginv_dec :: _ => t m r -> Test '(t,m,r)
prop_ginv_dec x = test $ (fromMaybe (error "could not divide by G in prop_ginv_dec") $
divGDec $ mulGDec x) == x \\ witness entailEqT x
prop_ginv_crt :: _ => t m r -> Test '(t,m,r)
prop_ginv_crt x = test $ fromMaybe (error "no CRT in prop_ginv_crt") $ do
divGCRT' <- divGCRT
mulGCRT' <- mulGCRT
return $ (divGCRT' $ mulGCRT' x) == x \\ witness entailEqT x
prop_g_dec :: _ => t m r -> Test '(t,m,r)
prop_g_dec x = test $ (mulGDec x) == (lInv $ mulGPow $ l x) \\ witness entailEqT x
prop_g_crt :: _ => t m r -> Test '(t,m,r)
prop_g_crt x = test $ fromMaybe (error "no CRT in prop_g_crt") $ do
mulGCRT' <- mulGCRT
crt' <- crt
crtInv' <- crtInv
return $ (mulGCRT' x) == (crt' $ mulGPow $ crtInv' x) \\ witness entailEqT x
prop_crt_inv :: _ => t m r -> Test '(t,m,r)
prop_crt_inv x = test $ fromMaybe (error "no CRT in prop_crt_inv") $ do
crt' <- crt
crtInv' <- crtInv
return $ (crtInv' $ crt' x) == x \\ witness entailEqT x
prop_l_inv :: _ => t m r -> Test '(t,m,r)
prop_l_inv x = test $ (lInv $ l x) == x \\ witness entailEqT x
prop_scalar_crt :: forall t m r . (Tensor t, Fact m, _) => r -> Test '(t,m,r)
prop_scalar_crt r = test $ fromMaybe (error "no CRT in prop_scalar_crt") $ do
scalarCRT' <- scalarCRT
crt' <- crt
return $ (scalarCRT' r :: t m r) == (crt' $ scalarPow r)
\\ proxy entailEqT (Proxy::Proxy (t m r))
prop_trem_pow :: forall t m m' r . (Fact m, Fact m', _) => t m r -> Test '(t,m,m',r)
prop_trem_pow x = test $ (twacePowDec $ (embedPow x :: t m' r)) == x \\ witness entailEqT x
prop_trem_dec :: forall t m m' r . (Fact m, Fact m', _) => t m r -> Test '(t,m,m',r)
prop_trem_dec x = test $ (twacePowDec $ (embedDec x :: t m' r)) == x \\ witness entailEqT x
prop_trem_crt :: forall t m m' r . (Fact m, Fact m', _) => t m r -> Test '(t,m,m',r)
prop_trem_crt x = test $ fromMaybe (error "no CRT in prop_trem_crt") $
(x==) <$> (twaceCRT <*> (embedCRT <*> pure x :: Maybe (t m' r))) \\ witness entailEqT x
prop_embed_dec :: forall t m m' r . (Fact m, Fact m', _) => t m r -> Test '(t,m,m',r)
prop_embed_dec x = test $ (embedDec x :: t m' r) == (lInv $ embedPow $ l x)
\\ proxy entailEqT (Proxy::Proxy (t m' r))
prop_embed_crt :: forall t m m' r . (Fact m, Fact m', _) => t m r -> Test '(t,m,m',r)
prop_embed_crt x = test $ fromMaybe (error "no CRT in prop_embed_crt") $ do
crt' <- crt
crtInv' <- crtInv
embedCRT' <- embedCRT
return $ (embedCRT' x :: t m' r) == (crt' $ embedPow $ crtInv' x)
\\ proxy entailEqT (Proxy::Proxy (t m' r))
prop_twace_dec :: forall t m m' r . (Fact m, Fact m', _) => t m' r -> Test '(t,m,m',r)
prop_twace_dec x = test $ (twacePowDec x :: t m r) == (lInv $ twacePowDec $ l x)
\\ proxy entailEqT (Proxy::Proxy (t m r))
prop_twace_crt :: forall t m m' r . (Fact m, Fact m', _) => t m' r -> Test '(t,m,m',r)
prop_twace_crt x = test $ fromMaybe (error "no CRT in prop_trace_crt") $ do
twaceCRT' <- twaceCRT
crt' <- crt
crtInv' <- crtInv
return $ (twaceCRT' x :: t m r) == (crt' $ twacePowDec $ crtInv' x)
\\ proxy entailEqT (Proxy::Proxy (t m r))
prop_twEmID :: forall t m r . _ => t m r -> Test '(t,m,r)
prop_twEmID x = test $
((twacePowDec x) == x) &&
(((fromMaybe (error "twemid_crt") twaceCRT) x) == x) &&
((embedPow x) == x) &&
((embedDec x) == x) &&
(((fromMaybe (error "twemid_crt") embedCRT) x) == x) \\ witness entailEqT x
prop_twace_invar1_pow :: forall t m m' r . _ => Test '(t,m,m',r)
prop_twace_invar1_pow = test $ fromMaybe (error "could not divide by G in prop_twace_invar1_pow") $ do
let mhat = proxy valueHatFact (Proxy::Proxy m)
mhat' = proxy valueHatFact (Proxy::Proxy m')
totm = proxy totientFact (Proxy::Proxy m)
totm' = proxy totientFact (Proxy::Proxy m')
output :: t m r <- divGPow $ scalarPow $ fromIntegral $ mhat * totm' `div` totm
input :: t m' r <- divGPow $ scalarPow $ fromIntegral mhat'
return $ (twacePowDec input) == output \\ proxy entailEqT (Proxy::Proxy (t m r))
prop_twace_invar1_dec :: forall t m m' r . _ => Test '(t,m,m',r)
prop_twace_invar1_dec = test $ fromMaybe (error "could not divide by G in prop_twace_invar1_dec") $ do
let mhat = proxy valueHatFact (Proxy::Proxy m)
mhat' = proxy valueHatFact (Proxy::Proxy m')
totm = proxy totientFact (Proxy::Proxy m)
totm' = proxy totientFact (Proxy::Proxy m')
output :: t m r <- divGDec $ lInv $ scalarPow $ fromIntegral $ mhat * totm' `div` totm
input :: t m' r <- divGDec $ lInv $ scalarPow $ fromIntegral mhat'
return $ (twacePowDec input) == output \\ proxy entailEqT (Proxy::Proxy (t m r))
prop_twace_invar1_crt :: forall t m m' r . _ => Test '(t,m,m',r)
prop_twace_invar1_crt = test $ fromMaybe (error "no CRT in prop_twace_invar1_crt") $ do
let mhat = proxy valueHatFact (Proxy::Proxy m)
mhat' = proxy valueHatFact (Proxy::Proxy m')
totm = proxy totientFact (Proxy::Proxy m)
totm' = proxy totientFact (Proxy::Proxy m')
scalarCRT1 <- scalarCRT
scalarCRT2 <- scalarCRT
divGCRT1 <- divGCRT
divGCRT2 <- divGCRT
twaceCRT' <- twaceCRT
let output :: t m r = divGCRT1 $ scalarCRT1 $ fromIntegral $ mhat * totm' `div` totm
input :: t m' r = divGCRT2 $ scalarCRT2 $ fromIntegral mhat'
return $ (twaceCRT' input) == output \\ proxy entailEqT (Proxy::Proxy (t m r))
prop_twace_invar2_powdec :: forall t m m' r . (Tensor t, Fact m, Fact m', Ring r, _) => Test '(t,m,m',r)
prop_twace_invar2_powdec = test $
let output = scalarPow $ one :: t m r
input = scalarPow $ one :: t m' r
in (twacePowDec input) == output \\ proxy entailEqT (Proxy::Proxy (t m r))
prop_twace_invar2_crt :: forall t m m' r . (Tensor t, Fact m, Fact m', Ring r, _) => Test '(t,m,m',r)
prop_twace_invar2_crt = test $ fromMaybe (error "no CRT in prop_twace_invar2_crt") $ do
scalarCRT1 <- scalarCRT
scalarCRT2 <- scalarCRT
let input = scalarCRT1 one :: t m' r
output = scalarCRT2 one :: t m r
return $ (twacePowDec input) == output \\ proxy entailEqT (Proxy::Proxy (t m r))