packages feed

lol 0.0.1.0 → 0.1.0.0

raw patch · 13 files changed

+337/−236 lines, 13 files

Files

+ CHANGES.md view
@@ -0,0 +1,9 @@+Changelog for lol project+================================++0.1.0.0+-----+ * Fixed bug in Box-Muller sampling routine.+ * Changed how we lift linear functions for better noise control.+ * Split entailment functions in Tensor.+ * Increased performance in FastCyc by better handling Sub constructors.
README view
@@ -24,11 +24,11 @@ * CTensor.hs, which gives an   implementation of the Tensor class using a C backend via Haskell's FFI. -* FiniteField.hs, which gives an unoptimized implementation of finite field-  arithmetic. To use this module, you will need an instance of IrreduciblePoly.-  These instances provide irreducible polynomials for various degrees and base fields.-  One instance is provided for characteristic 2 fields of size up to 2^32 in -  IrreducibleChar2.hs.+* FiniteField.hs, which gives an unoptimized implementation of finite+  field arithmetic. To use this module, you will need an instance of+  IrreduciblePoly.  These instances provide irreducible polynomials+  for various degrees and base fields.  One instance is provided for+  characteristic 2 fields of size up to 2^32 in IrreducibleChar2.hs.  * ZqBasic.hs, which is a basic implementation of Zq=Z/qZ arithmetic.
lol.cabal view
@@ -5,19 +5,19 @@ -- PVP summary:      +-+------- breaking API changes --                   | | +----- non-breaking API additions --                   | | | +--- code changes with no API change-version:             0.0.1.0-synopsis:            A general-purpose library for lattice cryptography.+version:             0.1.0.0+synopsis:            A library for lattice cryptography. homepage:            https://github.com/cpeikert/Lol Bug-Reports:         https://github.com/cpeikert/Lol/issues license:             GPL-2 license-file:        LICENSE-author:              Eric Crockett, Chris Peikert+author:              Eric Crockett <ecrockett0@gmail.com>, Chris Peikert <cpeikert@alum.mit.edu> maintainer:          Eric Crockett <ecrockett0@gmail.com> copyright:           Eric Crockett, Chris Peikert category:            Crypto stability:           experimental build-type:          Simple-extra-source-files:  README, +extra-source-files:  README, CHANGES.md,                      src/Crypto/Lol/Cyclotomic/Tensor/CTensor/tensorTypes.h,                      test-suite/CycTests.hs,                      test-suite/SHETests.hs,@@ -25,7 +25,7 @@                      test-suite/TestTypes.hs,                      test-suite/ZqTests.hs cabal-version:       >=1.10-description:         \\Lambda \\ocirc \\lambda is a general-purpose library for ring-based lattice cryptography.+description:         Λ ○ λ (Lol) is a general-purpose library for ring-based lattice cryptography. source-repository head   type: git   location: https://github.com/cpeikert/Lol
src/Crypto/Lol/Applications/SymmSHE.hs view
@@ -25,7 +25,7 @@ , embedSK, embedCT, twaceCT , tunnelCT -- * Constraint synonyms-, AddPublicCtx, MulPublicCtx, KeySwitchCtx, KSHintCtx, ModSwitchPTCtx+, AddPublicCtx, MulPublicCtx, InnerKeySwitchCtx, KeySwitchCtx, KSHintCtx, ModSwitchPTCtx , ToSDCtx, EncryptCtx, TunnelCtx, GenSKCtx, DecryptCtx , ErrorTermCtx ) where@@ -97,14 +97,14 @@    m `Divides` m')  -- | Encrypt a plaintext under a secret key.-encrypt :: forall t m m' z zp zq e rnd . (EncryptCtx t m m' z zp zq, MonadRandom rnd)+encrypt :: forall t m m' z zp zq rnd . (EncryptCtx t m m' z zp zq, MonadRandom rnd)            => SK (Cyc t m' z) -> PT (Cyc t m zp) -> rnd (CT m zp (Cyc t m' zq)) encrypt (SK svar s) =-  let sq = reduce s-  in (\pt -> do-         e <- errorCoset svar (embed pt :: PT (Cyc t m' zp))-         c1 <- getRandom-         return $! CT LSD zero one $ fromCoeffs [reduce e - c1 * sq, c1])+  let sq = adviseCRT $ reduce s+  in \pt -> do+    e <- errorCoset svar (embed pt :: PT (Cyc t m' zp))+    c1 <- getRandom+    return $! CT LSD zero one $ fromCoeffs [reduce e - c1 * sq, c1]  -- | Constraint synonym for extracting the error term of a ciphertext. type ErrorTermCtx t m' z zp zq =@@ -228,10 +228,11 @@ lweSample :: (LWECtx t m' z zq, MonadRandom rnd)              => SK (Cyc t m' z) -> rnd (Polynomial (Cyc t m' zq)) lweSample (SK svar s) =-  let sq = adviseCRT $ negate $ reduce s+  -- adviseCRT because we call `replicateM (lweSample s)` below, but only want to do CRT once. +  let sq = adviseCRT $ negate $ reduce s    in do     e <- errorRounded svar-    c1 <- getRandom+    c1 <- adviseCRT <$> getRandom -- we would like hints to be in CRT form     return $ fromCoeffs [c1 * sq + reduce (e `asTypeOf` s), c1]  -- | Constraint synonym for generating key-switch hints.@@ -245,7 +246,7 @@ ksHint :: (KSHintCtx gad t m' z zq, MonadRandom rnd)           => SK (Cyc t m' z) -> Cyc t m' z           -> rnd (Tagged gad [Polynomial (Cyc t m' zq)])-ksHint skout val = do           -- rnd monad+ksHint skout val = do -- rnd monad   let valq = reduce val       valgad = encode valq   -- CJP: clunky, but that's what we get without a MonadTagged@@ -261,6 +262,7 @@  knapsack :: forall t m' z zq' . (KnapsackCtx t m' z zq')             => [Polynomial (Cyc t m' zq')] -> [Cyc t m' z] -> Polynomial (Cyc t m' zq')+-- adviseCRT here because we are about to map (*) onto each polynomial coeff knapsack hint xs = sum (zipWith (*>>) (adviseCRT <$> reduce <$> xs) hint)  type InnerKeySwitchCtx gad t m' zq zq' =@@ -276,10 +278,7 @@  -- | Constraint synonym for key switching. type KeySwitchCtx gad t m' zp zq zq' =-  (ToSDCtx t m' zp zq,-   -- EAC: same as InnerKeySwitchCtx, but duplicated for haddock-   RescaleCyc (Cyc t) zq' zq, RescaleCyc (Cyc t) zq zq',-   Decompose gad zq', KnapsackCtx t m' (DecompOf zq') zq')+  (ToSDCtx t m' zp zq, InnerKeySwitchCtx gad t m' zq zq')  -- | Switch a linear ciphertext under @s_in@ to a linear one under @s_out@ keySwitchLinear :: forall gad t m' zp zq zq' z rnd m .@@ -451,9 +450,11 @@ twaceCT (CT d 0 l c) = CT d 0 l (twace <$> c) twaceCT _ = error "twaceCT requires 0 factors of g; call absorbGFactors first" + -- | Constraint synonym for ring tunneling. type TunnelCtx t e r s e' r' s' z zp zq zq' gad =   (ExtendLinIdx e r s e' r' s',     -- liftLin+   e' ~ (e * (r' / r)),             -- convenience; implied by prev constraint    KSHintCtx gad t r' z zq',        -- ksHint    Reduce z zq,                     -- Reduce on Linear    Lift zp z,                       -- liftLin@@ -473,6 +474,7 @@ tunnelCT f skout (SK _ sin) = tagT $ (do -- in rnd   -- generate hints   let f' = extendLin $ lift f :: Linear t z e' r' s'+      f'q = reduce f' :: Linear t zq e' r' s'       -- choice of basis here must match coeffsCyc basis below       ps = proxy powBasis (Proxy::Proxy e')       comps = (evalLin f' . (adviseCRT sin *)) <$> ps@@ -481,7 +483,7 @@     let CT MSD 0 s c = toMSD $ absorbGFactors ct'         [c0,c1] = coeffs c         -- apply E-linear function to constant term c0-        c0' = evalLin (reduce f' :: Linear t zq e' r' s') c0+        c0' = evalLin f'q c0         -- apply E-linear function to c1 via key-switching         -- this basis must match the basis used above to generate the hints         c1s = coeffsCyc Pow c1 :: [Cyc t e' zq]
src/Crypto/Lol/Cyclotomic/Cyc.hs view
@@ -18,7 +18,7 @@ -- * Basic operations , mulG, divG , scalarCyc, liftCyc-, adviseCRT+, advisePow, adviseDec, adviseCRT -- * Error sampling , tGaussian, errorRounded, errorCoset -- * Sub/extension rings@@ -48,10 +48,11 @@ newtype Cyc t m r = Cyc {    -- | Unsafe deconstructor for 'Cyc'.   unsafeUnCyc :: UCyc t m r }-                    deriving (Arbitrary, NFData, Random)+                    deriving (Arbitrary, Random)  -- See: https://ghc.haskell.org/trac/ghc/ticket/11008 -- for why I have to use StandaloneDeriving here+deriving instance NFData (UCyc t m a) => NFData (Cyc t m a) deriving instance Show (UCyc t m a) => Show (Cyc t m a) deriving instance Eq (UCyc t m a) => Eq (Cyc t m a) deriving instance Additive (UCyc t m a) => Additive.C (Cyc t m a)@@ -94,12 +95,20 @@  ---------- Core cyclotomic operations ---------- +adviseCRT, advisePow, adviseDec :: (Fact m, CElt t r) => Cyc t m r -> Cyc t m r+ -- | Yield an equivalent element that /may/ be in a CRT -- representation.  This can serve as an optimization hint. E.g., -- call 'adviseCRT' prior to multiplying the same value by many -- other values.-adviseCRT :: (Fact m, CElt t r) => Cyc t m r -> Cyc t m r adviseCRT = coerceCyc U.adviseCRT++-- | Same as 'adviseCRT', but for the powerful-basis representation.+advisePow = coerceCyc U.forcePow -- do it, but not required by contract++-- | Same as 'adviseCRT', but for the powerful-basis representation.+adviseDec = coerceCyc U.forceDec+  -- | Multiply by the special element @g@ of the @m@th cyclotomic. mulG :: (Fact m, CElt t r) => Cyc t m r -> Cyc t m r
src/Crypto/Lol/Cyclotomic/Linear.hs view
@@ -1,8 +1,8 @@ {-# LANGUAGE ConstraintKinds, DataKinds, FlexibleContexts,              GeneralizedNewtypeDeriving, KindSignatures,              MultiParamTypeClasses, NoImplicitPrelude, RoleAnnotations,-             ScopedTypeVariables, TypeFamilies, TypeOperators,-             UndecidableInstances #-}+             ScopedTypeVariables, StandaloneDeriving,+             TypeFamilies, TypeOperators, UndecidableInstances #-}  -- | Functions from one cyclotomic ring to another that are linear -- over a common subring.@@ -22,8 +22,9 @@  -- | An @E@-linear function from @R@ to @S@. newtype Linear t z (e::Factored) (r::Factored) (s::Factored) = D [Cyc t s z]-  deriving (NFData) +deriving instance (NFData (Cyc t s z)) => NFData (Linear t z e r s)+ -- TODO: have constructor for both relative Pow basis of R/E?  -- some params are phantom but matter for safety@@ -35,17 +36,17 @@ linearDec :: forall t z e r s .              (e `Divides` r, e `Divides` s, CElt t z)              => [Cyc t s z] -> Linear t z e r s-linearDec cs = let ps = proxy powBasis (Proxy::Proxy e) `asTypeOf` cs-               in if length cs <= length ps then D (adviseCRT <$> cs)+linearDec ys = let ps = proxy powBasis (Proxy::Proxy e) `asTypeOf` ys+               in if length ys <= length ps then D (adviseCRT <$> ys)                else error $ "linearDec: too many entries: "-                           ++ show (length cs) ++ " versus "+                           ++ show (length ys) ++ " versus "                            ++ show (length ps)  -- | Evaluates the given linear function on the input. evalLin :: forall t z e r s .            (e `Divides` r, e `Divides` s, CElt t z)            => Linear t z e r s -> Cyc t r z -> Cyc t s z-evalLin (D cs) r = sum (zipWith (*) cs $+evalLin (D ys) r = sum (zipWith (*) ys $                         embed <$> (coeffsCyc Dec r :: [Cyc t e z]))  instance Additive (Cyc t s z) => Additive.C (Linear t z e r s) where@@ -60,21 +61,19 @@  instance (Reduce z zq, Fact s, CElt t z, CElt t zq)          => Reduce (Linear t z e r s) (Linear t zq e r s) where-  reduce (D cs) = D $ reduce <$> cs+  reduce (D ys) = D $ reduce <$> ys  instance (CElt t zp, CElt t z, z ~ LiftOf zp, Lift zp z, Fact s)          => Lift' (Linear t zp e r s) where   type LiftOf (Linear t zp e r s) = Linear t (LiftOf zp) e r s -  lift (D cs) = D $ liftCyc Dec <$> cs+  lift (D ys) = D $ liftCyc Pow <$> ys  -- | A convenient constraint synonym for extending a linear function -- to larger rings. type ExtendLinIdx e r s e' r' s' =-  (e ~ FGCD r e', r' ~ FLCM r e', -- these imply R'=R\otimes_E E'-   e' ~ (e * (r' / r)), -- just to help GHC. This is implied by previous two constraints-   e' `Divides` s', s `Divides` s', -- these imply lcm(s,e')|s' <==> (S+E') \subseteq S'-   Fact r) -- need Fact r because nothing else gives it+  (Fact r, e ~ FGCD r e', r' ~ FLCM r e', -- these imply R'=R\otimes_E E'+   e' `Divides` s', s `Divides` s') -- lcm(s,e')|s' <=> (S+E') \subseteq S'  -- | Extend an @E@-linear function @R->S@ to an @E'@-linear function -- @R\'->S\'@.  (Mathematically, such extension only requires@@ -87,4 +86,4 @@ -- identical decoding bases, because R' \cong R \otimes_E E'.  If we -- relax the constraint on E then we'd have to change the -- implementation to something more difficult.-extendLin (D cs) = D (embed <$> cs)+extendLin (D ys) = D (embed <$> ys)
src/Crypto/Lol/Cyclotomic/Tensor.hs view
@@ -51,6 +51,7 @@ class (TElt t Double, TElt t (Complex Double))       => Tensor (t :: Factored -> * -> *) where +  -- | Constraints needed by @t@ to hold type @r@.   type TElt t r :: Constraint    -- | Properties that hold for any index. Use with '\\'.@@ -59,32 +60,39 @@      -- | Properties that hold for any (legal) fully-applied tensor. Use   -- with '\\'.-  entailFullT :: Tagged (t m r)-                 ((Fact m, TElt t r) :- -                  (Eq (t m r), ZeroTestable (t m r), Ring (t m r), -                   NFData (t m r), Random (t m r)))+  entailEqT :: Tagged (t m r)+               ((Eq r, Fact m, TElt t r) :- (Eq (t m r)))+  entailZTT :: Tagged (t m r)+               ((ZeroTestable r, Fact m, TElt t r) :- (ZeroTestable (t m r)))+  entailRingT :: Tagged (t m r)+                 ((Ring r, Fact m, TElt t r) :- (Ring (t m r)))+  entailNFDataT :: Tagged (t m r)+                   ((NFData r, Fact m, TElt t r) :- (NFData (t m r)))+  entailRandomT :: Tagged (t m r)+                   ((Random r, Fact m, TElt t r) :- (Random (t m r)))    -- | Converts a scalar to a tensor in the powerful basis-  scalarPow :: (Fact m, TElt t r) => r -> t m r+  scalarPow :: (Ring r, Fact m, TElt t r) => r -> t m r    -- | 'l' converts from decoding-basis representation to   -- powerful-basis representation; 'lInv' is its inverse.-  l, lInv :: (Fact m, TElt t r) => t m r -> t m r+  l, lInv :: (Ring r, Fact m, TElt t r) => t m r -> t m r    -- | Multiply by @g@ in the powerful/decoding basis-  mulGPow, mulGDec :: (Fact m, TElt t r) => t m r -> t m r+  mulGPow, mulGDec :: (Ring r, Fact m, TElt t r) => t m r -> t m r    -- | Divide by @g@ in the powerful/decoding basis.  The 'Maybe'   -- output indicates that the operation may fail, which happens   -- exactly when the input is not divisible by @g@.-  divGPow, divGDec :: (Fact m, TElt t r) => t m r -> Maybe (t m r)+  divGPow, divGDec :: (ZeroTestable r, IntegralDomain r, Fact m, TElt t r)+                      => t m r -> Maybe (t m r)    -- | A tuple of all the operations relating to the CRT basis, in a   -- single 'Maybe' value for safety.  Clients should typically not   -- use this method directly, but instead call the corresponding   -- top-level functions: the elements of the tuple correpond to the   -- functions 'scalarCRT', 'mulGCRT', 'divGCRT', 'crt', 'crtInv'.-  crtFuncs :: (Fact m, TElt t r, CRTrans r) =>+  crtFuncs :: (ZeroTestable r, IntegralDomain r, CRTrans r, Fact m, TElt t r) =>               Maybe (    r -> t m r, -- scalarCRT                      t m r -> t m r, -- mulGCRT                      t m r -> t m r, -- divGCRT@@ -93,17 +101,17 @@    -- | Sample from the "skewed" Gaussian error distribution @t*D@   -- in the decoding basis, where @D@ has scaled variance @v@.-  tGaussianDec :: (Fact m, OrdFloat q, Random q, TElt t q,-                   ToRational v, MonadRandom rnd)+  tGaussianDec :: (OrdFloat q, Random q, TElt t q,+                   ToRational v, Fact m, MonadRandom rnd)                   => v -> rnd (t m q)    -- | The @twace@ linear transformation, which is the same in both the   -- powerful and decoding bases.-  twacePowDec :: (m `Divides` m', TElt t r) => t m' r -> t m r+  twacePowDec :: (Ring r, m `Divides` m', TElt t r) => t m' r -> t m r    -- | The @embed@ linear transformations, for the powerful and   -- decoding bases.-  embedPow, embedDec :: (m `Divides` m', TElt t r)+  embedPow, embedDec :: (Ring r, m `Divides` m', TElt t r)                         => t m r -> t m' r    -- | A tuple of all the extension-related operations involving the@@ -111,21 +119,22 @@   -- method directly, but instead call the corresponding top-level   -- functions: the elements of the tuple correpond to the functions   -- 'twaceCRT', 'embedCRT'.-  crtExtFuncs :: (m `Divides` m', TElt t r, CRTrans r) =>+  crtExtFuncs :: (ZeroTestable r, IntegralDomain r, CRTrans r,+                  m `Divides` m', TElt t r) =>                  Maybe (t m' r -> t m  r, -- twaceCRT                         t m  r -> t m' r) -- embedCRT    -- | Map a tensor in the powerful\/decoding\/CRT basis, representing   -- an @O_m'@ element, to a vector of tensors representing @O_m@   -- elements in the same kind of basis.-  coeffs :: (m `Divides` m', TElt t r) => t m' r -> [t m r]+  coeffs :: (Ring r, m `Divides` m', TElt t r) => t m' r -> [t m r]    -- | The powerful extension basis w.r.t. the powerful basis.-  powBasisPow :: (m `Divides` m', TElt t r) => Tagged m [t m' r]+  powBasisPow :: (Ring r, TElt t r, m `Divides` m') => Tagged m [t m' r]    -- | A list of tensors representing the mod-@p@ CRT set of the   -- extension.-  crtSetDec :: (m `Divides` m', PrimeField fp,+  crtSetDec :: (PrimeField fp, m `Divides` m',                 Coprime (PToF (CharOf fp)) m', TElt t fp)                => Tagged m [t m' fp] @@ -137,7 +146,8 @@              => (a -> mon b) -> t m a -> mon (t m b)  -- | Convenience value indicating whether 'crtFuncs' exists.-hasCRTFuncs :: forall t m r . (Tensor t, Fact m, TElt t r, CRTrans r)+hasCRTFuncs :: forall t m r . (ZeroTestable r, IntegralDomain r, CRTrans r, +                               Tensor t, Fact m, TElt t r)                => TaggedT (t m r) Maybe () hasCRTFuncs = tagT $ do   (_ :: r -> t m r,_,_,_,_) <- crtFuncs@@ -145,11 +155,13 @@  -- | Yield a tensor for a scalar in the CRT basis.  (This function is -- simply an appropriate entry from 'crtFuncs'.)-scalarCRT :: (Tensor t, Fact m, TElt t r, CRTrans r) => Maybe (r -> t m r)+scalarCRT :: (ZeroTestable r, IntegralDomain r, CRTrans r, +              Tensor t, Fact m, TElt t r) => Maybe (r -> t m r) scalarCRT = (\(f,_,_,_,_) -> f) <$> crtFuncs  -mulGCRT, divGCRT, crt, crtInv :: (Tensor t, Fact m, TElt t r, CRTrans r)+mulGCRT, divGCRT, crt, crtInv ::+  (ZeroTestable r, IntegralDomain r, CRTrans r, Tensor t, Fact m, TElt t r)   => Maybe (t m r -> t m r) -- | Multiply by @g@ in the CRT basis. (This function is simply an -- appropriate entry from 'crtFuncs'.)@@ -168,17 +180,18 @@ -- For cyclotomic indices m | m', -- @Tw(x) = (mhat\/m\'hat) * Tr(g\'\/g * x)@. -- (This function is simply an appropriate entry from 'crtExtFuncs'.)-twaceCRT :: forall t r m m' . (Tensor t, m `Divides` m', TElt t r, CRTrans r)+twaceCRT :: forall t r m m' . (ZeroTestable r, IntegralDomain r, CRTrans r, +                               Tensor t, m `Divides` m', TElt t r)             => Maybe (t m' r -> t m r) twaceCRT = proxyT hasCRTFuncs (Proxy::Proxy (t m' r)) *>            proxyT hasCRTFuncs (Proxy::Proxy (t m  r)) *>            (fst <$> crtExtFuncs) - -- | Embed a tensor with index @m@ in the CRT basis to a tensor with -- index @m'@ in the CRT basis. -- (This function is simply an appropriate entry from 'crtExtFuncs'.)-embedCRT :: forall t r m m' . (Tensor t, m `Divides` m', TElt t r, CRTrans r)+embedCRT :: forall t r m m' . (ZeroTestable r, IntegralDomain r, CRTrans r, +                               Tensor t, m `Divides` m', TElt t r)             => Maybe (t m r -> t m' r) embedCRT = proxyT hasCRTFuncs (Proxy::Proxy (t m' r)) *>            proxyT hasCRTFuncs (Proxy::Proxy (t m  r)) *>
src/Crypto/Lol/Cyclotomic/Tensor/CTensor.hs view
@@ -164,13 +164,16 @@  instance Tensor CT where -  type TElt CT r = (IntegralDomain r, ZeroTestable r, -                    Eq r, Random r, NFData r,-                    Storable r, CRNS r)+  type TElt CT r = (Storable r, CRNS r)    entailIndexT = tag $ Sub Dict-  entailFullT = tag $ Sub Dict+  entailEqT = tag $ Sub Dict+  entailZTT = tag $ Sub Dict+  entailRingT = tag $ Sub Dict+  entailNFDataT = tag $ Sub Dict+  entailRandomT = tag $ Sub Dict +   scalarPow = CT . scalarPow' -- Vector code    l = wrap $ lgWrapper $ untag $ lgDispatch dl@@ -234,24 +237,24 @@ -- | Class to dispatch to the C backend for various element types. class CRNS r where -  zipWrapper :: (Fact m) => -    (forall a . (TElt CT a, Dispatch a) => CT' m a -> CT' m a -> CT' m a)+  zipWrapper :: (Fact m, Additive r) => +    (forall a . (TElt CT a, Dispatch a, Additive a) => CT' m a -> CT' m a -> CT' m a)     -> CT' m r -> CT' m r -> CT' m r -  crtWrapper :: (Fact m, CRTrans r) => -    (forall a . (TElt CT a, CRTrans a, Dispatch a) => Maybe (CT' m a -> CT' m a))+  crtWrapper :: (Fact m, CRTrans r, ZeroTestable r, IntegralDomain r) => +    (forall a . (TElt CT a, CRTrans a, Dispatch a, ZeroTestable a, IntegralDomain a) => Maybe (CT' m a -> CT' m a))     -> Maybe (CT' m r -> CT' m r) -  lgWrapper :: (Fact m) => -    (forall a . (TElt CT a, Dispatch a) => CT' m a -> CT' m a)+  lgWrapper :: (Fact m, Additive r) => +    (forall a . (TElt CT a, Dispatch a, Additive a) => CT' m a -> CT' m a)     -> CT' m r -> CT' m r -  divGWrapper :: (Fact m) => -    (forall a . (TElt CT a, Dispatch a) => CT' m a -> Maybe (CT' m a))+  divGWrapper :: (Fact m, IntegralDomain r, ZeroTestable r) => +    (forall a . (TElt CT a, Dispatch a, IntegralDomain a, ZeroTestable a) => CT' m a -> Maybe (CT' m a))     -> CT' m r -> Maybe (CT' m r) -  gaussWrapper :: (Fact m, MonadRandom rnd) => -    (forall a . (TElt CT a, Dispatch a, OrdFloat a, MonadRandom rnd) => rnd (CT' m a))+  gaussWrapper :: (Fact m, MonadRandom rnd, Random r) => +    (forall a . (TElt CT a, Dispatch a, OrdFloat a, MonadRandom rnd, Random a) => rnd (CT' m a))     -> rnd (CT' m r)  instance CRNS Double where@@ -283,7 +286,12 @@   divGWrapper f = f   gaussWrapper = error "Cannot call gaussianDec for ZqBasic" -instance (Storable a, Storable b, CRNS a, CRNS b, CRTrans a, CRTrans b) +instance (Storable a, Storable b, +          CRNS a, CRNS b, +          CRTrans a, CRTrans b, +          ZeroTestable a, ZeroTestable b, +          IntegralDomain a, IntegralDomain b,+          Random a, Random b)    => CRNS (a,b) where   zipWrapper f (CT' x :: CT' m (a,b)) (CT' y) =     let (a,b) = unzip x@@ -319,13 +327,13 @@     (CT' b) <- gaussWrapper f     return $ CT' $ zip a b -mulGPow' :: (TElt CT r, Fact m) => CT' m r -> CT' m r+mulGPow' :: (TElt CT r, Fact m, Additive r) => CT' m r -> CT' m r mulGPow' = lgWrapper $ untag $ lgDispatch dmulgpow -divGPow' :: forall m r . (TElt CT r, Fact m) => CT' m r -> Maybe (CT' m r)+divGPow' :: forall m r . (TElt CT r, Fact m, IntegralDomain r, ZeroTestable r) => CT' m r -> Maybe (CT' m r) divGPow' = divGWrapper $ untag $ checkDiv $ lgDispatch dginvpow -crt' :: forall m r . (TElt CT r, Fact m, CRTrans r) +crt' :: forall m r . (TElt CT r, Fact m, CRTrans r, ZeroTestable r, IntegralDomain r)    => TaggedT m Maybe (CT' m r -> CT' m r) crt' = tagT $ crtWrapper $ do   f <- proxyT ctCRT (Proxy::Proxy m)@@ -500,7 +508,7 @@         generate pp (\i -> wPow $ (-i*pow)))) $       pureT ppsFact -gCoeffsCRT, gInvCoeffsCRT :: (TElt CT r, CRTrans r, Fact m)+gCoeffsCRT, gInvCoeffsCRT :: (TElt CT r, CRTrans r, Fact m, ZeroTestable r, IntegralDomain r)   => TaggedT m Maybe (CT' m r) gCoeffsCRT = crt' <*> (return $ mulGPow' $ scalarPow' LP.one) -- It's necessary to call 'fromJust' here: otherwise @@ -519,7 +527,7 @@ -- we can't put this in Extension with the rest of the twace/embed fucntions because it needs access to  -- the C backend twaceCRT' :: forall m m' r .-             (TElt CT r, CRTrans r, m `Divides` m')+             (TElt CT r, CRTrans r, m `Divides` m', ZeroTestable r, IntegralDomain r)              => TaggedT '(m, m') Maybe (Vector r -> Vector r) twaceCRT' = tagT $ do -- Maybe monad   (CT' g') <- proxyT gCoeffsCRT (Proxy::Proxy m')
src/Crypto/Lol/Cyclotomic/Tensor/RepaTensor.hs view
@@ -75,12 +75,14 @@  instance Tensor RT where -  type TElt RT r = (IntegralDomain r, ZeroTestable r,-                    Eq r, Random r, NFData r,-                    Unbox r, Elt r)+  type TElt RT r = (Unbox r, Elt r)    entailIndexT  = tag $ Sub Dict-  entailFullT   = tag $ Sub Dict+  entailEqT = tag $ Sub Dict+  entailZTT = tag $ Sub Dict+  entailRingT = tag $ Sub Dict+  entailNFDataT = tag $ Sub Dict+  entailRandomT = tag $ Sub Dict    scalarPow = RT . scalarPow'
src/Crypto/Lol/Cyclotomic/UCyc.hs view
@@ -28,7 +28,7 @@ module Crypto.Lol.Cyclotomic.UCyc ( -- * Data type-  UCyc, CElt+  UCyc, CElt, RElt -- * Basic operations , mulG, divG , scalarCyc, liftCyc@@ -48,7 +48,7 @@ import           Crypto.Lol.Cyclotomic.Tensor  as T import qualified Crypto.Lol.Cyclotomic.Utility as U import           Crypto.Lol.Gadget-import           Crypto.Lol.LatticePrelude     as LP+import           Crypto.Lol.LatticePrelude     as LP hiding ((*>)) import           Crypto.Lol.Types.FiniteField import           Crypto.Lol.Types.ZPP @@ -56,7 +56,7 @@ import Algebra.Ring         as Ring (C) import Algebra.ZeroTestable as ZeroTestable (C) -import Control.Applicative    hiding ((*>))+import Control.Applicative import Control.DeepSeq import Control.Monad.Identity import Control.Monad.Random@@ -67,7 +67,7 @@ import Data.Typeable import Test.QuickCheck -import qualified Debug.Trace as DT+--import qualified Debug.Trace as DT  -- | A data type for representing cyclotomic rings such as @Z[zeta]@, -- @Zq[zeta]@, and @Q(zeta)@: @t@ is the 'Tensor' type for storing@@ -77,7 +77,7 @@   Pow  :: !(t m r) -> UCyc t m r -- representation wrt powerful basis   Dec  :: !(t m r) -> UCyc t m r -- decoding basis -  -- Invariant: use CRTr if and only if crtFuncs exists for (t m r);+  -- Invariant: use CRTr iff crtFuncs exists for (t m r);   -- otherwise use CRTe (because crtFuncs is guaranteed to exist for   -- (t m (CRTExt r))   CRTr :: !(t m r) -> UCyc t m r -- wrt CRT basis over r, if it exists@@ -96,15 +96,17 @@  -- | Shorthand for frequently reused constraints that are needed for --  change of basis.-type UCCtx t r = (Tensor t, CRTrans r, CRTrans (CRTExt r), CRTEmbed r,-                  ZeroTestable r, TElt t r, TElt t (CRTExt r))+type UCCtx t r = (Tensor t, RElt t r, RElt t (CRTExt r), CRTEmbed r) --- | Shorthand for frequently reused constraints that are needed for--- most functions involving 'UCyc' and 'Crypto.Lol.Cyclotomic.Cyc.Cyc'.+-- | Collection of constraints need to work on most functions over a+-- particular base ring @r@.+type RElt t r = (TElt t r, CRTrans r, IntegralDomain r, ZeroTestable r, NFData r) --- EAC: duplicated UCCtx for haddock-type CElt t r = (Tensor t, CRTrans r, CRTrans (CRTExt r), CRTEmbed r,-                 ZeroTestable r, TElt t r, TElt t (CRTExt r), Eq r, NFData r)+-- | Shorthand for frequently reused constraints that are needed for+-- most functions involving 'UCyc' and+-- 'Crypto.Lol.Cyclotomic.Cyc.Cyc'.+type CElt t r = (Tensor t, RElt t r, RElt t (CRTExt r),+                 CRTEmbed r, Eq r, Random r)  -- | Same as 'Crypto.Lol.Cyclotomic.Cyc.scalarCyc', but for 'UCyc'. scalarCyc :: (Fact m, CElt t a) => a -> UCyc t m a@@ -114,10 +116,11 @@ instance (UCCtx t r, Fact m, Eq r) => Eq (UCyc t m r) where   -- handle same bases when fidelity allows (i.e., *not* CRTe basis)   (Scalar v1) == (Scalar v2) = v1 == v2-  (Pow v1) == (Pow v2) = v1 == v2 \\ witness entailFullT v1-  (Dec v1) == (Dec v2) = v1 == v2 \\ witness entailFullT v1-  (CRTr v1) == (CRTr v2) = v1 == v2 \\ witness entailFullT v1+  (Pow v1) == (Pow v2) = v1 == v2 \\ witness entailEqT v1+  (Dec v1) == (Dec v2) = v1 == v2 \\ witness entailEqT v1+  (CRTr v1) == (CRTr v2) = v1 == v2 \\ witness entailEqT v1 +  -- compare in compositum   (Sub (c1 :: UCyc t l1 r)) == (Sub (c2 :: UCyc t l2 r)) =     (embed' c1 :: UCyc t (FLCM l1 l2) r) == embed' c2     \\ lcmDivides (Proxy::Proxy l1) (Proxy::Proxy l2)@@ -131,9 +134,9 @@ -- ZeroTestable instance instance (UCCtx t r, Fact m) => ZeroTestable.C (UCyc t m r) where   isZero (Scalar v) = isZero v-  isZero (Pow v) = isZero v \\ witness entailFullT v-  isZero (Dec v) = isZero v \\ witness entailFullT v-  isZero (CRTr v) = isZero v \\ witness entailFullT v+  isZero (Pow v) = isZero v \\ witness entailZTT v+  isZero (Dec v) = isZero v \\ witness entailZTT v+  isZero (CRTr v) = isZero v \\ witness entailZTT v   isZero x@(CRTe _) = isZero $ toPow' x   isZero (Sub c) = isZero c @@ -148,11 +151,10 @@    -- SAME CONSTRUCTORS   (Scalar c1) + (Scalar c2) = Scalar (c1+c2)-  (Pow v1) + (Pow v2) = Pow $ v1 + v2 \\ witness entailFullT v1-  (Dec v1) + (Dec v2) = Dec $ v1 + v2 \\ witness entailFullT v1-  (CRTr v1) + (CRTr v2) = CRTr $ v1 + v2 \\ witness entailFullT v1-  -- CJP: is this OK for precision?-  (CRTe v1) + (CRTe v2) = CRTe $ v1 + v2 \\ witness entailFullT v1+  (Pow v1) + (Pow v2) = Pow $ v1 + v2 \\ witness entailRingT v1+  (Dec v1) + (Dec v2) = Dec $ v1 + v2 \\ witness entailRingT v1+  (CRTr v1) + (CRTr v2) = CRTr $ v1 + v2 \\ witness entailRingT v1+  (CRTe v1) + (CRTe v2) = CRTe $ v1 + v2 \\ witness entailRingT v1   -- Sub plus Sub: work in compositum   (Sub (c1 :: UCyc t m1 r)) + (Sub (c2 :: UCyc t m2 r)) =     (Sub $ (embed' c1 :: UCyc t (FLCM m1 m2) r) + embed' c2)@@ -164,15 +166,15 @@   p1@(Scalar _) + p2@(Dec _) = toDec' p1 + p2   p1@(Scalar _) + p2@(CRTr _) = toCRT' p1 + p2   p1@(Scalar _) + p2@(CRTe _) = toCRT' p1 + p2-  (Scalar v1) + (Sub c2) = Sub $ Scalar v1 + c2+  (Scalar c1) + (Sub c2) = Sub $ Scalar c1 + c2 -- must re-wrap Scalar!    p1@(Pow _) + p2@(Scalar _) = p1 + toPow' p2   p1@(Dec _) + p2@(Scalar _) = p1 + toDec' p2   p1@(CRTr _) + p2@(Scalar _) = p1 + toCRT' p2   p1@(CRTe _) + p2@(Scalar _) = p1 + toCRT' p2-  (Sub c1) + (Scalar v2) = Sub $ c1 + Scalar v2+  (Sub c1) + (Scalar c2) = Sub $ c1 + Scalar c2 -  -- SUB PLUS SOMETHING ELSE (NON-SCALAR): work in full ring+  -- SUB PLUS NON-SUB, NON-SCALAR: work in full ring   (Sub c1) + c2 = embed' c1 + c2   c1 + (Sub c2) = c1 + embed' c2 @@ -205,36 +207,35 @@   _ * v2@(Scalar c2) | isZero c2 = v2    -- BOTH IN A CRT BASIS-  (CRTr v1) * (CRTr v2) = CRTr $ v1 * v2 \\ witness entailFullT v1-  (CRTe v1) * (CRTe v2) = toPow' $ CRTe $ v1 * v2 \\ witness entailFullT v1+  (CRTr v1) * (CRTr v2) = CRTr $ v1 * v2 \\ witness entailRingT v1+  (CRTe v1) * (CRTe v2) = toPow' $ CRTe $ v1 * v2 \\ witness entailRingT v1 +  -- CRTr/CRTe mixture+  (CRTr _) * (CRTe _) = error "UCyc.(*): mixed CRTr/CRTe"+  (CRTe _) * (CRTr _) = error "UCyc.(*): mixed CRTr/CRTe"+   -- AT LEAST ONE SCALAR   (Scalar c1) * (Scalar c2) = Scalar $ c1 * c2    (Scalar c) * (Pow v) = Pow $ fmapT (*c) v   (Scalar c) * (Dec v) = Dec $ fmapT (*c) v   (Scalar c) * (CRTr v) = CRTr $ fmapT (*c) v-  s@(Scalar _) * c'@(CRTe _) = s * toPow' c'-  (Scalar c) * (Sub c2) = Sub $ Scalar c * c2+  (Scalar c) * (CRTe v) = CRTe $ fmapT (* toExt c) v+  (Scalar c1) * (Sub c2) = Sub $ Scalar c1 * c2    (Pow v) * (Scalar c) = Pow $ fmapT (*c) v   (Dec v) * (Scalar c) = Dec $ fmapT (*c) v   (CRTr v) * (Scalar c) = CRTr $ fmapT (*c) v-  c'@(CRTe _) * s@(Scalar _) = toPow' c' * s-  (Sub c1) * (Scalar c) = Sub $ c1 * Scalar c--  -- AT LEAST ONE SUB+  (CRTe v) * (Scalar c) = CRTe $ fmapT (* toExt c) v+  (Sub c1) * (Scalar c2) = Sub $ c1 * Scalar c2 -  -- two Subs: work in compositum+  -- TWO SUBS: work in a CRT rep for compositum   (Sub (c1 :: UCyc t m1 r)) * (Sub (c2 :: UCyc t m2 r)) =-    (Sub $ (embed' c1 :: UCyc t (FLCM m1 m2) r) * embed' c2)+    -- re-wrap c1, c2 as Subs of the composition, and force them to CRT+    (Sub $ (toCRT' $ Sub c1 :: UCyc t (FLCM m1 m2) r) * toCRT' (Sub c2))     \\ lcm2Divides (Proxy::Proxy m1) (Proxy::Proxy m2) (Proxy::Proxy m) -  -- Sub times something else (non-Scalar): work in full ring-  (Sub c1) * p2 = embed' c1 * p2-  p1 * (Sub c2) = p1 * embed' c2--  -- ELSE: work in appropriate CRT basis+  -- ELSE: work in appropriate CRT rep   p1 * p2 = toCRT' p1 * toCRT' p2    fromInteger = Scalar . fromInteger@@ -243,7 +244,10 @@ instance (Reduce a b, Fact m, CElt t a, CElt t b)   => Reduce (UCyc t m a) (UCyc t m b) where -  reduce = fmapC reduce . forceAny+  -- optimized for subring constructors+  reduce (Scalar c) = Scalar $ reduce c+  reduce (Sub (c :: UCyc t l a)) = Sub (reduce c :: UCyc t l b)+  reduce x = fmapC reduce $ forceAny x  -- promote Gadget from base ring instance (Gadget gad zq, Fact m, CElt t zq) => Gadget gad (UCyc t m zq) where@@ -252,14 +256,20 @@   encode s = ((* adviseCRT s) <$>) <$> gadget  -- promote Decompose, using the powerful basis-instance (Decompose gad zq, Fact m, CElt t zq,-          Reduce (UCyc t m (DecompOf zq)) (UCyc t m zq))+instance (Decompose gad zq, Fact m,+         -- these imply (superclass) Reduce on UCyc; needed for Sub case+          CElt t zq, CElt t (DecompOf zq), Reduce (DecompOf zq) zq)   => Decompose gad (UCyc t m zq) where    type DecompOf (UCyc t m zq) = UCyc t m (DecompOf zq) +  -- faster implementations: decompose directly in subring, which is+  -- correct because we decompose in powerful basis+  decompose (Scalar c) = pasteT $ Scalar <$> peelT (decompose c)+  decompose (Sub c) = pasteT $ Sub <$> peelT (decompose c)+   -- traverse: Traversable (c m) and Applicative (Tagged gad ZL)-  decompose = fromZL . traverse (toZL . decompose) . forcePow+  decompose x = fromZL $ traverse (toZL . decompose) $ forcePow x     where toZL :: Tagged s [a] -> TaggedT s ZipList a           toZL = coerce           fromZL :: TaggedT s ZipList a -> Tagged s [a]@@ -269,35 +279,55 @@ instance (Correct gad zq, Fact m, CElt t zq)          => Correct gad (UCyc t m zq) where   -- sequenceA: Applicative (c m) and Traversable (TaggedT [])-  correct bs = (correct . pasteT) <$> (sequenceA $ forceDec <$> peelT bs)+  correct bs = (correct . pasteT) <$> sequenceA (forceDec <$> peelT bs)  -- generic RescaleCyc instance  instance {-# OVERLAPS #-} (Rescale a b, CElt t a, CElt t b)          => U.RescaleCyc (UCyc t) a b where-  rescaleCyc b = fmapC rescale . forceBasis (Just b) +  -- Optimized for subring constructors, for powerful basis.+  -- Analogs for decoding basis are not quite correct, because (* -1)+  -- doesn't commute with 'rescale' due to tiebreakers!+  rescaleCyc U.Pow (Scalar c) = Scalar $ rescale c+  rescaleCyc U.Pow (Sub (c :: UCyc t l a)) =+    Sub (U.rescaleCyc U.Pow c :: UCyc t l b)++  rescaleCyc b x = fmapC rescale $ forceBasis (Just b) x+ -- specialized instance for product rings: ~2x faster algorithm-instance (Mod a, Field b, Lift a z, Reduce z b,-          CElt t a, CElt t b, CElt t (a,b), CElt t z)+instance (Mod a, Field b, Lift a (ModRep a), Reduce (LiftOf a) b,+          CElt t a, CElt t b, CElt t (a,b), CElt t (LiftOf a))          => U.RescaleCyc (UCyc t) (a,b) b where-  rescaleCyc bas =++  -- optimized for subrings and powerful basis (see comments in other+  -- instance for why this doesn't work for decoding basis)+  rescaleCyc U.Pow (Scalar c) = Scalar $ rescale c+  rescaleCyc U.Pow (Sub (c :: UCyc t l (a,b))) =+    Sub (U.rescaleCyc U.Pow c :: UCyc t l b)++  rescaleCyc bas x =     let aval = proxy modulus (Proxy::Proxy a)   -- CJP: could use unzipC here to get (a,b) in one pass, but it   -- requires adding that method, and unzipT to Tensor and all its   -- instances. Probably not worth it.-    in \x -> let y = forceAny x-                 a = fmapC fst y-                 b = fmapC snd y-                 z = liftCyc bas a-             in (pure (recip (fromIntegral aval))) * (b - reduce z)+        y = forceAny x+        a = fmapC fst y+        b = fmapC snd y+        z = liftCyc bas a+    in Scalar (recip (reduce aval)) * (b - reduce z)  -- | Same as 'Crypto.Lol.Cyclotomic.Cyc.liftCyc', but for 'UCyc'. liftCyc :: (Lift b a, Fact m, CElt t a, CElt t b)            => U.Basis -> UCyc t m b -> UCyc t m a-liftCyc U.Pow = fmapC lift . forceBasis (Just U.Pow)-liftCyc U.Dec = fmapC lift . forceBasis (Just U.Dec)+-- optimized for subrings and powerful basis (see comments in+-- RescaleCyc instances for why this doesn't work for decoding)+liftCyc U.Pow (Scalar c) = Scalar $ lift c+liftCyc U.Pow (Sub c) = Sub $ liftCyc U.Pow c +liftCyc U.Pow x = fmapC lift $ forceBasis (Just U.Pow) x+liftCyc U.Dec x = fmapC lift $ forceBasis (Just U.Dec) x+ -- | Same as 'Crypto.Lol.Cyclotomic.Cyc.adviseCRT', but for 'UCyc'. adviseCRT :: (Fact m, CElt t r) => UCyc t m r -> UCyc t m r adviseCRT x@(Scalar _) = x@@ -310,9 +340,9 @@ mulG (Sub c) = mulG $ embed' c                -- must go to full ring mulG (Pow v) = Pow $ mulGPow v mulG (Dec v) = Dec $ mulGDec v--- fromJust is safe here because we're already in CRTr-mulG (CRTr v) = CRTr $ fromMaybe (error "FC.mulG CRTr") mulGCRT v-mulG (CRTe v) = CRTe $ fromMaybe (error "FC.mulG CRTe") mulGCRT v+-- fromMaybe is safe here because we're already in CRTr+mulG (CRTr v) = CRTr $ fromJust' "UCyc.mulG CRTr" mulGCRT v+mulG (CRTe v) = CRTe $ fromJust' "UCyc.mulG CRTe" mulGCRT v  -- | Same as 'Crypto.Lol.Cyclotomic.Cyc.divG', but for 'UCyc'. divG :: (Fact m, CElt t r) => UCyc t m r -> Maybe (UCyc t m r)@@ -320,9 +350,9 @@ divG (Sub c) = divG $ embed' c                      -- full ring divG (Pow v) = Pow <$> divGPow v divG (Dec v) = Dec <$> divGDec v--- fromJust is safe here because we're already in CRTr-divG (CRTr v) = Just $ CRTr $ fromMaybe (error "FC.divG CRTr") divGCRT v-divG (CRTe v) = Just $ CRTe $ fromMaybe (error "FC.divG CRTe") divGCRT v+-- fromMaybe is safe here because we're already in CRTr+divG (CRTr v) = Just $ CRTr $ fromJust' "UCyc.divG CRTr" divGCRT v+divG (CRTe v) = Just $ CRTe $ fromJust' "UCyc.divG CRTe" divGCRT v  -- | Same as 'Crypto.Lol.Cyclotomic.Cyc.tGaussian', but for 'UCyc'. tGaussian :: (Fact m, OrdFloat q, Random q, CElt t q,@@ -334,7 +364,7 @@ errorRounded :: forall v rnd t m z .                 (ToInteger z, Fact m, CElt t z, ToRational v, MonadRandom rnd)                 => v -> rnd (UCyc t m z)-errorRounded svar = +errorRounded svar =   fmapC (roundMult one) <$> (tGaussian svar :: rnd (UCyc t m Double))  -- | Same as 'Crypto.Lol.Cyclotomic.Cyc.errorCoset', but for 'UCyc'.@@ -373,14 +403,17 @@   \\ gcdDivides (Proxy::Proxy l) (Proxy::Proxy m) twace (Pow v) = Pow $ twacePowDec v twace (Dec v) = Dec $ twacePowDec v--- stay in CRTr only if it's possible, otherwise go to Pow+-- stay in CRTr only iff it's valid for target, else go to Pow twace x@(CRTr v) =   fromMaybe (twace $ toPow' x) (CRTr <$> (twaceCRT <*> pure v))--- CJP: stay in CRTe: precision OK?-twace (CRTe v) = CRTe $ fromMaybe (error "FC.twace CRTe") twaceCRT v+-- stay in CRTe iff CRTr is invalid for target, else go to Pow+twace x@(CRTe v) =+  fromMaybe (CRTe $ fromJust' "UCyc.twace CRTe" twaceCRT v)+            (proxy (pasteT hasCRTFuncs) (Proxy::Proxy (t m r)) *>+             pure (twace $ toPow' x))  -- | Same as 'Crypto.Lol.Cyclotomic.Cyc.coeffsCyc', but for 'UCyc'.-coeffsCyc :: (m `Divides` m', CElt t r) +coeffsCyc :: (m `Divides` m', CElt t r)              => U.Basis -> UCyc t m' r -> [UCyc t m r] coeffsCyc U.Pow (Pow v) = LP.map Pow $ coeffs v coeffsCyc U.Dec (Dec v) = LP.map Dec $ coeffs v@@ -393,7 +426,7 @@  -- | Same as 'Crypto.Lol.Cyclotomic.Cyc.crtSet', but for 'UCyc'. crtSet :: forall t m m' r p mbar m'bar .-           (m `Divides` m', ZPP r, p ~ CharOf (ZPOf r), +           (m `Divides` m', ZPP r, p ~ CharOf (ZPOf r),             mbar ~ PFree p m, m'bar ~ PFree p m',             CElt t r, CElt t (ZPOf r))            => Tagged m [UCyc t m' r]@@ -422,6 +455,7 @@ forceBasis (Just U.Pow) x = toPow' x forceBasis (Just U.Dec) x = toDec' x forceBasis Nothing x@(Scalar _) = toPow' x+-- force as outermost op to ensure we get an r-basis forceBasis Nothing (Sub c) = forceBasis Nothing $ embed' c forceBasis Nothing x@(CRTe _) = toPow' x forceBasis Nothing x = x@@ -470,20 +504,21 @@  ---------- HELPER FUNCTIONS (NOT FOR EXPORT) ---------- --- | Force embed, to a non-Sub constructor.+-- | Force embed, to a non-'Sub' constructor.  Preserves Scalar, Pow,+-- Dec constructors, and CRTr/CRTe constructor if valid in both source+-- and target ring (we rely on this in toCRT'). embed' :: forall t r l m .           (UCCtx t r, l `Divides` m) => UCyc t l r -> UCyc t m r-embed' (Scalar v) = Scalar v+embed' (Scalar x) = Scalar x    -- must re-wrap! embed' (Pow v) = Pow $ embedPow v embed' (Dec v) = Dec $ embedDec v -- stay in CRTr only if it's possible, otherwise go to Pow embed' x@(CRTr v) =     fromMaybe (embed' $ toPow' x) (CRTr <$> (embedCRT <*> pure v))--- Staying in CRTe might not be safe, because the target tensor--- might have implemented a CRTr even if the source tensor--- hasn't.  Mathematically this is impossible (because target has--- CRTr only if source does), so this is purely about implementation.-embed' x@(CRTe _) = embed' $ toPow' x+embed' x@(CRTe v) = -- go to CRTe iff CRTr is invalid for target index+    fromMaybe (CRTe $ fromJust' "UCyc.embed' CRTe" embedCRT v)+              (proxy (pasteT hasCRTFuncs) (Proxy::Proxy (t m r)) *>+               pure (embed' $ toPow' x)) embed' (Sub (c :: UCyc t k r)) = embed' c   \\ transDivides (Proxy::Proxy k) (Proxy::Proxy l) (Proxy::Proxy m) @@ -493,57 +528,68 @@ toPow', toDec' :: (UCCtx t r, Fact m) => UCyc t m r -> UCyc t m r -- forces the argument into the powerful basis toPow' (Scalar c) = Pow $ scalarPow c-toPow' (Sub c) = toPow' $ embed' c+toPow' (Sub c) = embed' $ toPow' c -- OK: embed' preserves Pow toPow' x@(Pow _) = x toPow' (Dec v) = Pow $ l v-toPow' (CRTr v) = Pow $ fromMaybe (error "FC.toPow'") crtInv v-toPow' (CRTe v) = Pow $ fmapT fromExt $ fromMaybe (error "FC.toPow'") crtInv v+toPow' (CRTr v) = Pow $ fromJust' "UCyc.toPow'" crtInv v+toPow' (CRTe v) =+    Pow $ fmapT fromExt $ fromJust' "UCyc.toPow' CRTe" crtInv v --- forces the argument into the decoding basis-toDec' x@(Scalar _) = toDec' $ toPow' x -- use scalarDec instead-toDec' (Sub c) = toDec' $ embed' c+-- | Force the argument into the decoding basis.+toDec' x@(Scalar _) = toDec' $ toPow' x -- TODO: use scalarDec instead+toDec' (Sub c) = embed' $ toDec' c      -- OK: embed' preserves Dec toDec' (Pow v) = Dec $ lInv v toDec' x@(Dec _) = x-toDec' (CRTr v) = Dec $ lInv $ fromMaybe (error "FC.toDec'") crtInv v-toDec' (CRTe v) = Dec $ lInv $ fmapT fromExt $ fromMaybe (error "FC.toDec'") crtInv v+toDec' x@(CRTr _) = toDec' $ toPow' x+toDec' x@(CRTe _) = toDec' $ toPow' x --- forces the argument into a CRT basis, according to the invariant--- about which one should be used+-- | Force the argument into the "valid" CRT basis for our invariant. toCRT' :: forall t m r . (UCCtx t r, Fact m) => UCyc t m r -> UCyc t m r-toCRT' (Sub c) = toCRT' $ embed' c toCRT' x@(CRTr _) = x toCRT' x@(CRTe _) = x+toCRT' (Sub (c :: UCyc t l r)) =+    case (proxyT hasCRTFuncs (Proxy::Proxy (t l r)),+          proxyT hasCRTFuncs (Proxy::Proxy (t m r))) of+      (Just _, Just _) -> embed' $ toCRT' c -- fastest; embed' preserves CRTr+      (_, Nothing) -> embed' $ toCRTe c -- faster; temp violate CRTr/e invariant+      _ -> toCRT' $ embed' c            -- fallback toCRT' x = fromMaybe (toCRTe x) (toCRTr <*> pure x)-  -- CJP: defining these helpers internally so they can't be called-  -- from anywhere else.  Therefore, the only way to convert to a-  -- CRT basis is through the toCRT' method.-  where-    toCRTr = do -- Maybe monad-      crt' <- crt-      scalarCRT' <- scalarCRT-      return $ \x -> case x of-        (Scalar c) -> CRTr $ scalarCRT' c-        (Pow v) -> CRTr $ crt' v-        (Dec v) -> CRTr $ crt' $ l v-          -- deliberately omit CRTe case, which should-          -- never happen by internal invariant, so trigger-          -- error if it does-    toCRTe = let m = proxy valueFact (Proxy::Proxy m)-                 crt' = fromMaybe (error $ "FC.toCRT': no crt': " ++ (show m)) crt :: t m (CRTExt r) -> t m (CRTExt r) -- must exist-                 scalarCRT' = fromMaybe (error "FC.toCRT': no scalar crt'") scalarCRT :: CRTExt r -> t m (CRTExt r)-             in \x -> case x of-               (Scalar c) -> CRTe $ scalarCRT' $ toExt c-               (Pow v) -> CRTe $ crt' $ fmapT toExt v-               (Dec v) -> CRTe $ crt' $ fmapT toExt $ l v +toCRTr :: forall t m r . (UCCtx t r, Fact m) => Maybe (UCyc t m r -> UCyc t m r)+toCRTr = do -- Maybe monad+  crt' <- crt+  scalarCRT' <- scalarCRT+  return $ \x -> case x of+                   (Scalar c) -> CRTr $ scalarCRT' c+                   (Pow v) -> CRTr $ crt' v+                   (Dec v) -> CRTr $ crt' $ l v+                   c@(CRTr _) -> c+                   c@(CRTe _) -> fromJust' "UCyc.toCRTr CRTe" toCRTr $ toPow' c+                   (Sub _) -> error "UCyc.toCRTr: Sub"++toCRTe :: forall t m r . (UCCtx t r, Fact m) => UCyc t m r -> UCyc t m r+toCRTe = let m = proxy valueFact (Proxy::Proxy m)+             crt' = fromJust' ("UCyc.toCRTe: no crt': " ++ show m) crt+                  :: t m (CRTExt r) -> t m (CRTExt r) -- must exist+             scalarCRT' = fromJust' "UCyc.toCRTe: no scalarCRT" scalarCRT+                        :: CRTExt r -> t m (CRTExt r)+         in \x -> case x of+                    (Scalar c) -> CRTe $ scalarCRT' $ toExt c+                    (Pow v) -> CRTe $ crt' $ fmapT toExt v+                    (Dec v) -> CRTe $ crt' $ fmapT toExt $ l v+                    c@(CRTr _) -> toCRTe $ toPow' c+                    c@(CRTe _) -> c+                    (Sub _) -> error "UCyc.toCRTe: Sub"+ ---------- "Container" instances ----------  instance (Tensor t, Fact m) => Functor (UCyc t m) where   -- Functor instance is implied by Applicative laws   fmap f x = pure f <*> x +errApp :: String -> a errApp name = error $ "UCyc.Applicative: can't/won't handle " ++ name ++-              "; call forcePow|Dec first"+              "; call forcePow|Dec|Any first"  instance (Tensor t, Fact m) => Applicative (UCyc t m) where @@ -595,12 +641,11 @@   (CRTr v) <*> (Scalar a) = CRTr $ v <*> pure a \\ witness entailIndexT v    -- cases we can't/won't handle-  (Pow _) <*> (Dec _) = error "UCyc.Applicative: Pow/Dec combo"-  (Dec _) <*> (Pow _) = error "UCyc.Applicative: Pow/Dec combo"   (Sub _) <*> _  = errApp "Sub"   _ <*> (Sub _)  = errApp "Sub"   (CRTe _) <*> _ = errApp "CRTe"   _ <*> (CRTe _) = errApp "CRTe"+  _ <*> _ = errApp "mismatched Pow/Dec/CRTr bases"  instance (Tensor t, Fact m) => Foldable (UCyc t m) where   foldr f b (Scalar r) = f r b@@ -620,13 +665,13 @@  ---------- Utility instances ---------- -instance (Tensor t, Fact m, TElt t r, CRTrans r) => Random (UCyc t m r) where+instance (Tensor t, Fact m, TElt t r, CRTrans r, Random r, ZeroTestable r, IntegralDomain r) => Random (UCyc t m r) where    -- create in CRTr basis if legal, otherwise in powerful   random = let cons = fromMaybe Pow                       (proxyT hasCRTFuncs (Proxy::Proxy (t m r)) >> Just CRTr)            in \g -> let (v,g') = random g-                                 \\ proxy entailFullT (Proxy::Proxy (t m r))+                                 \\ proxy entailRandomT (Proxy::Proxy (t m r))                     in (cons v, g')    randomR _ = error "randomR non-sensical for cyclotomic rings"@@ -645,11 +690,11 @@   arbitrary = liftM Pow arbitrary   shrink = shrinkNothing -instance (Tensor t, Fact m, NFData r, TElt t r, TElt t (CRTExt r))+instance (Tensor t, Fact m, TElt t r, TElt t (CRTExt r), NFData r, NFData (CRTExt r))          => NFData (UCyc t m r) where-  rnf (Pow x)    = rnf x \\ witness entailFullT x-  rnf (Dec x)    = rnf x \\ witness entailFullT x-  rnf (CRTr x)   = rnf x \\ witness entailFullT x-  rnf (CRTe x)   = rnf x \\ witness entailFullT x+  rnf (Pow x)    = rnf x \\ witness entailNFDataT x+  rnf (Dec x)    = rnf x \\ witness entailNFDataT x+  rnf (CRTr x)   = rnf x \\ witness entailNFDataT x+  rnf (CRTe x)   = rnf x \\ witness entailNFDataT x   rnf (Scalar x) = rnf x   rnf (Sub x)    = rnf x
src/Crypto/Lol/GaussRandom.hs view
@@ -26,7 +26,13 @@     in do (u,v) <- iterateWhile uvGuard getUV           let t = u*u+v*v               com = sqrt (-var * log t / t)-          return (u * com, v * com)+          -- we can either sample u,v from [-1,1]+          -- or generate sign bits for the outputs+          s1 <- getRandom+          s2 <- getRandom+          let u' = if s1 then u else -u+              v' = if s2 then v else -v+          return (u'*com,v'*com)     where getUV = do u <- getRandomR (zero,one)                      v <- getRandomR (zero,one)                      return (u,v)
src/Crypto/Lol/LatticePrelude.hs view
@@ -24,7 +24,7 @@ , module Crypto.Lol.Factored -- * Miscellaneous , rescaleMod, roundCoset-, pureT, peelT, pasteT, withWitness, withWitnessT+, fromJust', pureT, peelT, pasteT, withWitness, withWitnessT , module Data.Functor.Trans.Tagged , module Data.Proxy ) where@@ -221,6 +221,10 @@   randomR ((loa,lob), (hia,hib)) g = let (a,g') = randomR (loa,hia) g                                          (b,g'') = randomR (lob,hib) g'                                      in ((a,b),g'')++-- | Version of 'fromJust' with an error message.+fromJust' :: String -> Maybe a -> a+fromJust' str = fromMaybe (error str)  -- | Apply any applicative to a Tagged value. pureT :: Applicative f => TaggedT t Identity a -> TaggedT t f a
test-suite/TensorTests.hs view
@@ -47,13 +47,14 @@    ]  -type TMRCtx t m r = (Tensor t, Fact m, m `Divides` m, CRTrans r, TElt t r, CRTEmbed r, TElt t (CRTExt r))+type TMRCtx t m r = (Tensor t, Fact m, m `Divides` m, CRTrans r, TElt t r, CRTEmbed r, +                     TElt t (CRTExt r), Eq r, ZeroTestable r, IntegralDomain r)  prop_fmap :: (TMRCtx t m r) => t m r -> Bool-prop_fmap x = fmapT id x == x \\ witness entailFullT x \\ witness entailIndexT x+prop_fmap x = fmapT id x == x \\ witness entailEqT x \\ witness entailIndexT x  prop_fmap2 :: (TMRCtx t m r) => t m r -> Bool-prop_fmap2 x = (fmapT id x) == (fmap id x) \\ witness entailFullT x \\ witness entailIndexT x+prop_fmap2 x = (fmapT id x) == (fmap id x) \\ witness entailEqT x \\ witness entailIndexT x  -- tests that multiplication in the extension ring matches CRT multiplication prop_mul_ext :: forall t m r . (TMRCtx t m r)@@ -64,7 +65,10 @@        Nothing -> error "mul have a CRT to call prop_mul_ext"        Just _ -> (let z = x * y                       z' = fmapT fromExt $ (fmapT toExt x) * (fmapT toExt y)-                  in z == z') \\ witness entailFullT x \\ witness entailFullT (fmap toExt x) \\ witness entailIndexT x+                  in z == z') \\ witness entailEqT x +                              \\ witness entailRingT x+                              \\ witness entailRingT (fmap toExt x)+                              \\ witness entailIndexT x  gInvGTests = testGroup "GInv.G == id" [   testGroup "Pow basis" $ groupTMR $ wrapTmrToBool prop_ginv_pow,@@ -74,30 +78,30 @@ -- divG . mulG == id in Pow basis prop_ginv_pow :: (TMRCtx t m r) => t m r -> Bool prop_ginv_pow x = (fromMaybe (error "could not divide by G in prop_ginv_pow") $ -  divGPow $ mulGPow x) == x \\ witness entailFullT x+  divGPow $ mulGPow x) == x \\ witness entailEqT x  -- divG . mulG == id in Dec basis prop_ginv_dec :: (TMRCtx t m r) => t m r -> Bool prop_ginv_dec x = (fromMaybe (error "could not divide by G in prop_ginv_dec") $ -  divGDec $ mulGDec x) == x \\ witness entailFullT x+  divGDec $ mulGDec x) == x \\ witness entailEqT x  -- divG . mulG == id in CRT basis prop_ginv_crt :: (TMRCtx t m r) => t m r -> Bool prop_ginv_crt x = fromMaybe (error "no CRT in prop_ginv_crt") $ do   divGCRT' <- divGCRT   mulGCRT' <- mulGCRT-  return $ (divGCRT' $ mulGCRT' x) == x \\ witness entailFullT x+  return $ (divGCRT' $ mulGCRT' x) == x \\ witness entailEqT x  -- crtInv . crt == id prop_crt_inv :: (TMRCtx t m r) => t m r -> Bool prop_crt_inv x = fromMaybe (error "no CRT in prop_crt_inv") $ do   crt' <- crt   crtInv' <- crtInv-  return $ (crtInv' $ crt' x) == x \\ witness entailFullT x+  return $ (crtInv' $ crt' x) == x \\ witness entailEqT x  -- lInv . l == id prop_l_inv :: (TMRCtx t m r) => t m r -> Bool-prop_l_inv x = (lInv $ l x) == x \\ witness entailFullT x+prop_l_inv x = (lInv $ l x) == x \\ witness entailEqT x  -- scalarCRT = crt . scalarPow prop_scalar_crt :: forall t m r . (TMRCtx t m r)@@ -106,7 +110,7 @@   scalarCRT' <- scalarCRT   crt' <- crt   return $ (scalarCRT' r :: t m r) == (crt' $ scalarPow r)-  \\ proxy entailFullT (Proxy::Proxy (t m r))+  \\ proxy entailEqT (Proxy::Proxy (t m r))  gCommuteTests = testGroup "G commutes with L" [   testGroup "Dec basis" $ groupTMR $ wrapTmrToBool prop_g_dec,@@ -114,14 +118,14 @@  -- mulGDec == lInv. mulGPow . l prop_g_dec :: (TMRCtx t m r) => t m r -> Bool-prop_g_dec x = (mulGDec x) == (lInv $ mulGPow $ l x) \\ witness entailFullT x+prop_g_dec x = (mulGDec x) == (lInv $ mulGPow $ l x) \\ witness entailEqT x  prop_g_crt :: (TMRCtx t m r) => t m r -> Bool prop_g_crt x = fromMaybe (error "no CRT in prop_g_crt") $ do   mulGCRT' <- mulGCRT   crt' <- crt   crtInv' <- crtInv-  return $ (mulGCRT' x) == (crt' $ mulGPow $ crtInv' x) \\ witness entailFullT x+  return $ (mulGCRT' x) == (crt' $ mulGPow $ crtInv' x) \\ witness entailEqT x  type TMRWrapCtx t m r = (TMRCtx t m r, Show (t m r), Arbitrary (t m r), Show r, Arbitrary r) @@ -192,7 +196,7 @@   -type TMM'RCtx t m m' r = (Tensor t, m `Divides` m', TElt t r, Ring r, CRTrans r)+type TMM'RCtx t m m' r = (Tensor t, m `Divides` m', TElt t r, Ring r, CRTrans r, Eq r, ZeroTestable r, IntegralDomain r)  -- groups related tests tremTests = testGroup "Tr.Em == id" [@@ -203,18 +207,18 @@ -- tests that twace . embed == id in the Pow basis prop_trem_pow :: forall t m m' r . (TMM'RCtx t m m' r)   => Proxy m' -> t m r -> Bool-prop_trem_pow _ x = (twacePowDec $ (embedPow x :: t m' r)) == x \\ witness entailFullT x+prop_trem_pow _ x = (twacePowDec $ (embedPow x :: t m' r)) == x \\ witness entailEqT x  -- tests that twace . embed == id in the Dec basis prop_trem_dec :: forall t m m' r . (TMM'RCtx t m m' r)   => Proxy m' -> t m r -> Bool-prop_trem_dec _ x = (twacePowDec $ (embedDec x :: t m' r)) == x \\ witness entailFullT x+prop_trem_dec _ x = (twacePowDec $ (embedDec x :: t m' r)) == x \\ witness entailEqT x  -- tests that twace . embed == id in the CRT basis prop_trem_crt :: forall t m m' r . (TMM'RCtx t m m' r)   => Proxy m' -> t m r -> Bool prop_trem_crt _ x = fromMaybe (error "no CRT in prop_trem_crt") $-  (x==) <$> (twaceCRT <*> (embedCRT <*> pure x :: Maybe (t m' r))) \\ witness entailFullT x+  (x==) <$> (twaceCRT <*> (embedCRT <*> pure x :: Maybe (t m' r))) \\ witness entailEqT x  embedCommuteTests = testGroup "Em commutes with L" [   testGroup "Dec basis" $ groupTMM'R $ wrapTmm'rToBool prop_embed_dec,@@ -223,7 +227,7 @@ -- embedDec == lInv . embedPow . l prop_embed_dec :: forall t m m' r . (TMM'RCtx t m m' r) => Proxy m' -> t m r -> Bool prop_embed_dec _ x = (embedDec x :: t m' r) == (lInv $ embedPow $ l x) -  \\ proxy entailFullT (Proxy::Proxy (t m' r))+  \\ proxy entailEqT (Proxy::Proxy (t m' r))  -- embedCRT = crt . embedPow . crtInv prop_embed_crt :: forall t m m' r . (TMM'RCtx t m m' r) => Proxy m' -> t m r -> Bool@@ -232,7 +236,7 @@   crtInv' <- crtInv   embedCRT' <- embedCRT   return $ (embedCRT' x :: t m' r) == (crt' $ embedPow $ crtInv' x) -    \\ proxy entailFullT (Proxy::Proxy (t m' r))+    \\ proxy entailEqT (Proxy::Proxy (t m' r))  twaceCommuteTests = testGroup "Tw commutes with L" [   testGroup "Dec basis" $ groupTMM'R $ wrapTm'mrToBool prop_twace_dec,@@ -241,7 +245,7 @@ -- twacePowDec = lInv . twacePowDec . l prop_twace_dec :: forall t m m' r . (TMM'RCtx t m m' r) => Proxy m -> t m' r -> Bool prop_twace_dec _ x = (twacePowDec x :: t m r) == (lInv $ twacePowDec $ l x)-  \\ proxy entailFullT (Proxy::Proxy (t m r))+  \\ proxy entailEqT (Proxy::Proxy (t m r))  -- twaceCRT = crt . twacePowDec . crtInv prop_twace_crt :: forall t m m' r . (TMM'RCtx t m m' r) => Proxy m -> t m' r -> Bool@@ -250,7 +254,7 @@   crt' <- crt   crtInv' <- crtInv   return $ (twaceCRT' x :: t m r) == (crt' $ twacePowDec $ crtInv' x)-    \\ proxy entailFullT (Proxy::Proxy (t m r))+    \\ proxy entailEqT (Proxy::Proxy (t m r))  twaceInvarTests = testGroup "Twace invariants" [   testGroup "Tw and Em ID for equal indices" $ groupTMR $ wrapTmrToBool $ prop_twEmID,@@ -261,12 +265,12 @@   testGroup "Invar2 CRT basis" $ groupTMM'R $ wrapProxyTmm'rToBool prop_twace_invar2_crt   ] -prop_twEmID :: forall t m r . (Tensor t, TElt t r, CRTrans r, Fact m, m `Divides` m) => t m r -> Bool+prop_twEmID :: forall t m r . (Tensor t, TElt t r, CRTrans r, Fact m, m `Divides` m, Eq r, ZeroTestable r, IntegralDomain r) => t m r -> Bool prop_twEmID x = ((twacePowDec x) == x) &&                   (((fromMaybe (error "twemid_crt") twaceCRT) x) == x) &&                   ((embedPow x) == x) &&                   ((embedDec x) == x) &&-                  (((fromMaybe (error "twemid_crt") embedCRT) x) == x) \\ witness entailFullT x+                  (((fromMaybe (error "twemid_crt") embedCRT) x) == x) \\ witness entailEqT x  -- twace mhat'/g' = mhat*totm'/totm/g (Pow basis) prop_twace_invar1_pow :: forall t m m' r . (TMM'RCtx t m m' r) => Proxy m' -> Proxy (t m r) -> Bool@@ -277,7 +281,7 @@       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 entailFullT (Proxy::Proxy (t m r))+  return $ (twacePowDec input) == output \\ proxy entailEqT (Proxy::Proxy (t m r))  -- twace mhat'/g' = mhat*totm'/totm/g (Dec basis) prop_twace_invar1_dec :: forall t m m' r . (TMM'RCtx t m m' r) => Proxy m' -> Proxy (t m r) -> Bool@@ -288,7 +292,7 @@       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 entailFullT (Proxy::Proxy (t m r))+  return $ (twacePowDec input) == output \\ proxy entailEqT (Proxy::Proxy (t m r))  -- twace mhat'/g' = mhat*totm'/totm/g (CRT basis) prop_twace_invar1_crt :: forall t m m' r . (TMM'RCtx t m m' r) => Proxy m' -> Proxy (t m r) -> Bool@@ -304,14 +308,14 @@   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 entailFullT (Proxy::Proxy (t m r))+  return $ (twaceCRT' input) == output \\ proxy entailEqT (Proxy::Proxy (t m r))  -- twace preserves scalars in Pow/Dec basis prop_twace_invar2_powdec :: forall t m m' r . (TMM'RCtx t m m' r) => Proxy m' -> Proxy (t m r) -> Bool prop_twace_invar2_powdec _ _ =    let output = scalarPow $ one :: t m r       input = scalarPow $ one :: t m' r-  in (twacePowDec input) == output \\ proxy entailFullT (Proxy::Proxy (t m r))+  in (twacePowDec input) == output \\ proxy entailEqT (Proxy::Proxy (t m r))  -- twace preserves scalars in Pow/Dec basis prop_twace_invar2_crt :: forall t m m' r . (TMM'RCtx t m m' r) => Proxy m' -> Proxy (t m r) -> Bool@@ -320,7 +324,7 @@   scalarCRT2 <- scalarCRT   let input = scalarCRT1 one :: t m' r       output = scalarCRT2 one :: t m r-  return $ (twacePowDec input) == output \\ proxy entailFullT (Proxy::Proxy (t m r))+  return $ (twacePowDec input) == output \\ proxy entailEqT (Proxy::Proxy (t m r))  type TMM'RWrapCtx t m m' r = (TMM'RCtx t m m' r, Show (t m' r), Show (t m r), Arbitrary (t m' r), Arbitrary (t m r))