content: {-|
  Module      : Crypto.Lol.Cyclotomic.CycRep
  Description : A low-level implementation of cyclotomic rings.
  Copyright   : (c) Eric Crockett, 2011-2017
                    Chris Peikert, 2011-2017
  License     : GPL-3
  Maintainer  : ecrockett0@gmail.com
  Stability   : experimental
  Portability : POSIX
  
    \( \def\Z{\mathbb{Z}} \)
    \( \def\F{\mathbb{F}} \)
    \( \def\Q{\mathbb{Q}} \)
    \( \def\O{\mathcal{O}} \)
  
  A low-level implementation of cyclotomic rings that allows (and
  requires) the programmer to control the underlying representation
  of ring elements, i.e., powerful, decoding, or CRT basis.
  
  __WARNING:__ as with all fixed-point arithmetic, the functions
  associated with 'CycRep' may result in overflow (and thereby
  incorrect answers and potential security flaws) if the input
  arguments are too close to the bounds imposed by the base type.
  The acceptable range of inputs for each function is determined by
  the internal linear transforms and other operations it performs.
  -}
  
  {-# LANGUAGE AllowAmbiguousTypes        #-}
  {-# LANGUAGE ConstraintKinds            #-}
  {-# LANGUAGE DataKinds                  #-}
  {-# LANGUAGE FlexibleContexts           #-}
  {-# LANGUAGE FlexibleInstances          #-}
  {-# LANGUAGE GADTs                      #-}
  {-# LANGUAGE GeneralizedNewtypeDeriving #-}
  {-# LANGUAGE InstanceSigs               #-}
  {-# LANGUAGE MultiParamTypeClasses      #-}
  {-# LANGUAGE PolyKinds                  #-}
  {-# LANGUAGE RankNTypes                 #-}
  {-# LANGUAGE RebindableSyntax           #-}
  {-# LANGUAGE ScopedTypeVariables        #-}
  {-# LANGUAGE TypeApplications           #-}
  {-# LANGUAGE TypeFamilies               #-}
  {-# LANGUAGE TypeOperators              #-}
  {-# LANGUAGE UndecidableInstances       #-}
  
  module Crypto.Lol.Cyclotomic.CycRep
  (
  -- * Data types and constraints
    CycRep, P, D, C, E, CycRepEC, CycRepPC, CRTElt
  -- * Changing representation
  , toPow, toDec, toCRT
  -- * Scalars
  , scalarPow, scalarCRT
  -- * Basic operations
  , mulGPow, mulGDec, mulGCRTC, divGPow, divGDec, divGCRTC, gSqNormDec
  -- * Error sampling
  , tweakedGaussian, roundedGaussian, cosetGaussian
  -- * Inter-ring operations and values
  , embedPow, embedCRTC, embedCRTE
  , twacePow, twaceDec, twaceCRTC, twaceCRTE
  , coeffsPow, coeffsDec, powBasis, crtSet
  ) where
  
  import Crypto.Lol.CRTrans
  import Crypto.Lol.Cyclotomic.CRTSentinel
  import Crypto.Lol.Cyclotomic.Tensor      hiding (divGDec, divGPow,
                                            embedCRT, embedPow, gSqNormDec,
                                            mulGDec, mulGPow, scalarCRT,
                                            scalarPow, twaceCRT)
  import Crypto.Lol.Prelude                as LP
  import Crypto.Lol.Reflects
  import Crypto.Lol.Types.FiniteField
  import Crypto.Lol.Types.IFunctor
  import Crypto.Lol.Types.Proto
  import Crypto.Lol.Types.Unsafe.ZqBasic
  
  import qualified Crypto.Lol.Cyclotomic.Tensor as T
  
  import qualified Algebra.Additive     as Additive (C)
  import qualified Algebra.Module       as Module (C)
  import qualified Algebra.Ring         as Ring (C)
  import qualified Algebra.ZeroTestable as ZeroTestable (C)
  
  import Control.Applicative    as A
  import Control.DeepSeq
  import Control.Monad.Identity (Identity (..))
  import Control.Monad.Random   hiding (ap, lift)
  import Data.Foldable          as F
  import Data.Traversable
  
  --import qualified Debug.Trace as DT
  
  -- | Represents a cyclotomic ring such as \(\Z[\zeta_m]\),
  -- \(\Z_q[\zeta_m]\), and \(\Q(\zeta_m)\) in an explicit
  -- representation: @t@ is the 'TensorPowDec' type for storing coefficient
  -- tensors; @m@ is the cyclotomic index; @rep@ is the representation
  -- (e.g., 'P', 'D', 'C', 'E'); @r@ is the base ring of the
  -- coefficients (e.g., \(\Z\), \(\Z_q\)).
  
  -- | Nullary index type representing the powerful basis.
  data P
  -- | Nullary index type representing the decoding basis.
  data D
  -- | Nullary index type representing the CRT basis over base ring.
  data C
  -- | Nullary index type representing the CRT basis over extension of
  -- base ring.
  data E
  
  data family CycRep (t :: Factored -> * -> *) rep (m :: Factored) r
  
  newtype instance CycRep t P m r = Pow  (t m r) deriving (Eq, ZeroTestable.C)
  newtype instance CycRep t D m r = Dec  (t m r) deriving (Eq, ZeroTestable.C)
  
  -- C/ESentinel enforces invariant that exactly one of the following
  -- two can be created for a given (t,m,r).
  data    instance CycRep t C m r = CRTC !(CSentinel t m r) !(t m r) deriving (Eq)
  -- can't derive ZT due to sentinel
  
  data    instance CycRep t E m r = CRTE !(ESentinel t m r) !(t m (CRTExt r))
  -- no Eq due to precision
  
  {- CJP: old GADT definition of CycRep, which seems less
     runtime-efficient than the data family definition.
  
  data CycRep t rep (m :: Factored) r where
    Pow  :: !(t m r) -> CycRep t P m r
    Dec  :: !(t m r) -> CycRep t D m r
    CRTC :: !(CSentinel t m r) -> !(t m r) -> CycRep t C m r
    CRTE :: !(ESentinel t m r) -> !(t m (CRTExt r)) -> CycRep t E m r
  -}
  
  -- | Convenient synonym for either CRT representation.
  type CycRepEC t m r = Either (CycRep t E m r) (CycRep t C m r)
  
  -- | Convenient synonym for random sampling.
  type CycRepPC t m r = Either (CycRep t P m r) (CycRep t C m r)
  
  -- | Constraints needed for CRT-related operations on 'CycRep' data.
  type CRTElt t r = (TensorG t r, CRTEmbed r,
                     TensorCRT t Maybe r, TensorCRT t Identity (CRTExt r))
  
  -- | Embed a scalar from the base ring.
  scalarPow :: (TensorPowDec t r, Fact m) => r -> CycRep t P m r
  scalarPow = Pow . T.scalarPow
  {-# INLINABLE scalarPow #-}
  
  -- | Embed a scalar from the base ring.
  scalarCRT :: (Fact m, CRTElt t r) => r -> CycRepEC t m r
  scalarCRT r = case crtSentinel of
    Right s -> Right $ CRTC s $ scalarCRTCS s r
    Left  s -> Left  $ CRTE s $ runIdentity T.scalarCRT $ toExt r
  {-# INLINABLE scalarCRT #-}
  
  
  ---------- Numeric Prelude instances ----------
  
  -- ZeroTestable instances
  
  {- CJP: only need these instances for GADT version of CycRep; for data
     family they are auto-derived.
  
  instance ZeroTestable (t m r) => ZeroTestable.C (CycRep t P m r) where
    isZero (Pow v) = isZero v
    {-# INLINABLE isZero #-}
  
  instance ZeroTestable (t m r) => ZeroTestable.C (CycRep t D m r) where
    isZero (Dec v) = isZero v
    {-# INLINABLE isZero #-}
  
  -}
  
  -- ZT for P,D auto-derived
  
  instance ZeroTestable (t m r) => ZeroTestable.C (CycRep t C m r) where
    -- can't derive this because of sentinel
    isZero (CRTC _ v) = isZero v
    {-# INLINABLE isZero #-}
  
  -- no ZT instance for E due to precision
  
  -- Additive instances
  
  -- TODO: replace these implementations to use Additive instance of
  -- underlying tensor? Would this require (forall m . Fact m => Additive (t m))?
  
  instance (TensorPowDec t r, Fact m) => Additive.C (CycRep t P m r) where
    {-# SPECIALIZE instance (TensorPowDec t Int64, Fact m) => Additive.C (CycRep t P m Int64) #-}
    {-# SPECIALIZE instance (TensorPowDec t Double, Fact m) => Additive.C (CycRep t P m Double) #-}
    {-# SPECIALIZE instance (TensorPowDec t (ZqBasic q Int64), Fact m) => Additive.C (CycRep t P m (ZqBasic q Int64)) #-}
  
    zero = Pow $ T.scalarPow zero
    (Pow v1) + (Pow v2) = Pow $ zipWithI (+) v1 v2
    (Pow v1) - (Pow v2) = Pow $ zipWithI (-) v1 v2
    negate (Pow v) = Pow $ fmapI negate v
    {-# INLINABLE zero #-}
    {-# INLINABLE (+) #-}
    {-# INLINABLE (-) #-}
    {-# INLINABLE negate #-}
  
  instance (TensorPowDec t r, Fact m) => Additive.C (CycRep t D m r) where
    {-# SPECIALIZE instance (TensorPowDec t Int64, Fact m) => Additive.C (CycRep t D m Int64) #-}
    {-# SPECIALIZE instance (TensorPowDec t Double, Fact m) => Additive.C (CycRep t D m Double) #-}
    {-# SPECIALIZE instance (TensorPowDec t (ZqBasic q Int64), Fact m) => Additive.C (CycRep t D m (ZqBasic q Int64)) #-}
  
    zero = Dec $ T.scalarPow zero -- scalarPow works because it's zero
    (Dec v1) + (Dec v2) = Dec $ zipWithI (+) v1 v2
    (Dec v1) - (Dec v2) = Dec $ zipWithI (-) v1 v2
    negate (Dec v) = Dec $ fmapI negate v
    {-# INLINABLE zero #-}
    {-# INLINABLE (+) #-}
    {-# INLINABLE (-) #-}
    {-# INLINABLE negate #-}
  
  -- | only for appropriate CRT representation (otherwise 'zero' would
  -- violate internal invariant)
  instance (Fact m, CRTElt t r) => Additive.C (CycRepEC t m r) where
    {-# SPECIALIZE instance (Fact m, CRTElt t Int64) => Additive.C (CycRepEC t m Int64) #-}
    {-# SPECIALIZE instance (Fact m, CRTElt t Double) => Additive.C (CycRepEC t m Double) #-}
    {-# SPECIALIZE instance (Fact m, CRTElt t (ZqBasic q Int64)) => Additive.C (CycRepEC t m (ZqBasic q Int64)) #-}
  
    zero = scalarCRT zero
  
    -- CJP: precision OK?  Alternatively, switch to pow and back after
    -- adding/subtracting.  Expensive, but necessary given output type.
    (Right (CRTC s v1)) + (Right (CRTC _ v2)) = Right $ CRTC s $ zipWithI (+) v1 v2
    (Left (CRTE s v1)) + (Left (CRTE _ v2)) = Left $ CRTE s $ zipWithI (+) v1 v2
    _ + _ = error "CycRep (+) internal error: mixed CRTC/CRTE"
  
    (Right (CRTC s v1)) - (Right (CRTC _ v2)) = Right $ CRTC s $ zipWithI (-) v1 v2
    (Left (CRTE s v1)) - (Left (CRTE _ v2)) = Left $ CRTE s $ zipWithI (-) v1 v2
    _ - _ = error "CycRep (-) internal error: mixed CRTC/CRTE"
  
    negate (Right (CRTC s v)) = Right $ CRTC s $ fmapI negate v
    negate (Left (CRTE s v))  = Left $ CRTE s $ fmapI negate v
  
    {-# INLINABLE zero #-}
    {-# INLINABLE (+) #-}
    {-# INLINABLE (-) #-}
    {-# INLINABLE negate #-}
  
  -- | only for appropriate CRT representation
  instance (Fact m, CRTElt t r) => Ring.C (CycRepEC t m r) where
    {-# SPECIALIZE instance (Fact m, CRTElt t Int64) => Ring.C (CycRepEC t m Int64) #-}
    {-# SPECIALIZE instance (Fact m, CRTElt t Double) => Ring.C (CycRepEC t m Double) #-}
    {-# SPECIALIZE instance (Fact m, CRTElt t (ZqBasic q Int64)) => Ring.C (CycRepEC t m (ZqBasic q Int64)) #-}
  
    one = scalarCRT one
    fromInteger c = scalarCRT $ fromInteger c
  
    (Right (CRTC s v1)) * (Right (CRTC _ v2)) = Right $ CRTC s $ zipWithI (*) v1 v2
    (Left (CRTE s v1)) * (Left (CRTE _ v2)) = Left $ CRTE s $ zipWithI (*) v1 v2
    _ * _ = error "CycRep internal error: mixed CRTC/CRTE"
  
    {-# INLINABLE one #-}
    {-# INLINABLE fromInteger #-}
    {-# INLINABLE (*) #-}
  
  
  instance (Ring r, TensorPowDec t r, Fact m) => Module.C r (CycRep t P m r) where
    {-# SPECIALIZE instance (Fact m, TensorPowDec t Int64) => Module.C Int64 (CycRep t P m Int64) #-}
    {-# SPECIALIZE instance (Fact m, TensorPowDec t Double) => Module.C Double (CycRep t P m Double) #-}
    {-# SPECIALIZE instance (Fact m, TensorPowDec t (ZqBasic q Int64), Reflects q Int64) => Module.C (ZqBasic q Int64) (CycRep t P m (ZqBasic q Int64)) #-}
  
    r *> (Pow v) = Pow $ fmapI (r *) v
    {-# INLINABLE (*>) #-}
  
  instance (Ring r, TensorPowDec t r, Fact m) => Module.C r (CycRep t D m r) where
    {-# SPECIALIZE instance (Fact m, TensorPowDec t Int64) => Module.C Int64 (CycRep t D m Int64) #-}
    {-# SPECIALIZE instance (Fact m, TensorPowDec t Double) => Module.C Double (CycRep t D m Double) #-}
    {-# SPECIALIZE instance (Fact m, TensorPowDec t (ZqBasic q Int64), Reflects q Int64) => Module.C (ZqBasic q Int64) (CycRep t D m (ZqBasic q Int64)) #-}
  
    r *> (Dec v) = Dec $ fmapI (r *) v
    {-# INLINABLE (*>) #-}
  
  instance (CRTElt t r, Fact m) => Module.C r (CycRepEC t m r) where
    {-# SPECIALIZE instance (CRTElt t Int64, Fact m) => Module.C Int64 (CycRepEC t m Int64) #-}
    {-# SPECIALIZE instance (CRTElt t Double, Fact m) => Module.C Double (CycRepEC t m Double) #-}
    {-# SPECIALIZE instance (CRTElt t (ZqBasic q Int64), Fact m) => Module.C (ZqBasic q Int64) (CycRepEC t m (ZqBasic q Int64)) #-}
  
    r *> (Right (CRTC s v)) = Right $ CRTC s $ fmapI (r *) v
    r *> (Left (CRTE s v)) = Left $ CRTE s $ fmapI (toExt r *) v
    {-# INLINABLE (*>) #-}
  
  -- | \(R_p\) is an \(\F_{p^d}\)-module when \(d\) divides \(\varphi(m)\), by
  -- applying \(d\)-dimensional \(\F_p\)-linear transform on \(d\)-dim chunks of
  -- powerful basis coeffs.
  instance (GFCtx fp d, Fact m, TensorPowDec t fp, Module (GF fp d) (t m fp))
           => Module.C (GF fp d) (CycRep t P m fp) where
    -- can use any r-basis to define module mult, but must be
    -- consistent.
    r *> (Pow v) = Pow $ r LP.*> v
  
  
  instance (Fact m, Reduce a b, IFunctor t, IFElt t a, IFElt t b)
           => Reduce (CycRep t P m a) (CycRep t P m b) where
    {-# SPECIALIZE instance (Fact m, Reflects q Int64, IFunctor t, IFElt t Int64, IFElt t (ZqBasic q Int64)) => Reduce (CycRep t P m Int64) (CycRep t P m (ZqBasic q Int64)) #-}
  
    reduce (Pow v) = Pow $ fmapI reduce v
    {-# INLINABLE reduce #-}
  
  instance (Fact m, Reduce a b, IFunctor t, IFElt t a, IFElt t b)
      => Reduce (CycRep t D m a) (CycRep t D m b) where
    {-# SPECIALIZE instance (Fact m, Reflects q Int64, IFunctor t, IFElt t Int64, IFElt t (ZqBasic q Int64)) => Reduce (CycRep t D m Int64) (CycRep t D m (ZqBasic q Int64)) #-}
  
    reduce (Dec v) = Dec $ fmapI reduce v
    {-# INLINABLE reduce #-}
  
  -- CJP: no Reduce for C because CRT basis may not exist for target
  -- type
  
  type instance LiftOf (CycRep t P m r) = CycRep t P m (LiftOf r)
  type instance LiftOf (CycRep t D m r) = CycRep t D m (LiftOf r)
  
  instance (Fact m, Lift' r, IFunctor t, IFElt t r, IFElt t (LiftOf r))
           => Lift' (CycRep t P m r) where
    {-# SPECIALIZE instance (Fact m, Reflects q Int64, IFunctor t, IFElt t Int64, IFElt t (ZqBasic q Int64)) => Lift' (CycRep t P m (ZqBasic q Int64)) #-}
  
    lift (Pow v) = Pow $ fmapI lift v
    {-# INLINABLE lift #-}
  
  instance (Lift' r, IFunctor t, IFElt t r, IFElt t (LiftOf r), Fact m)
           => Lift' (CycRep t D m r) where
    {-# SPECIALIZE instance (Fact m, Reflects q Int64, IFunctor t, IFElt t Int64, IFElt t (ZqBasic q Int64)) => Lift' (CycRep t D m (ZqBasic q Int64)) #-}
  
    lift (Dec v) = Dec $ fmapI lift v
    {-# INLINABLE lift #-}
  
  -- CJP: no Lift' for C because CRT basis may not exist for target type
  
  instance (Rescale a b, TensorPowDec t a, TensorPowDec t b, Fact m)
           => Rescale (CycRep t P m a) (CycRep t P m b) where
    rescale (Pow v) = Pow $ fmapI rescale v
    {-# INLINABLE rescale #-}
  
  instance (Rescale a b, TensorPowDec t a, TensorPowDec t b, Fact m)
           => Rescale (CycRep t D m a) (CycRep t D m b) where
    rescale (Dec v) = Dec $ fmapI rescale v
    {-# INLINABLE rescale #-}
  
  -- CJP: no Rescale for C because CRT basis may not exist for target
  -- type
  
  -- CJP: we don't instantiate RescaleCyc because it requires changing bases
  
  -- CJP: we don't instantiate Gadget etc., because (1) their methods
  -- wouldn't be efficient, and (2) their superclass constraints are not
  -- satisfied anyway (e.g., Ring for P rep).
  
  -- | multiply by the special element @g@
  mulGPow :: (Fact m, TensorG t r) => CycRep t P m r -> CycRep t P m r
  {-# INLINABLE mulGPow #-}
  mulGPow (Pow v) = Pow $ T.mulGPow v
  
  -- | multiply by the special element @g@
  mulGDec :: (Fact m, TensorG t r) => CycRep t D m r -> CycRep t D m r
  {-# INLINABLE mulGDec #-}
  mulGDec (Dec v) = Dec $ T.mulGDec v
  
  -- | multiply by the special element @g@
  mulGCRTC :: (Fact m, TensorCRT t Maybe r)
           => CycRep t C m r -> CycRep t C m r
  {-# INLINABLE mulGCRTC #-}
  mulGCRTC (CRTC s v) = CRTC s $ mulGCRTCS s v
  
  -- Note: We do not implement divGCRTE because we can't tell whether
  -- the element is actually divisible by g when using the CRT extension
  -- basis.
  
  -- | Divide by the special element \(g_m\).
  -- WARNING: this implementation is not a constant-time algorithm, so
  -- information about the argument may be leaked through a timing
  -- channel.
  divGPow :: (Fact m, TensorG t r) => CycRep t P m r -> Maybe (CycRep t P m r)
  {-# INLINABLE divGPow #-}
  divGPow (Pow v) = Pow <$> T.divGPow v
  
  -- | Similar to 'divGPow'.
  divGDec :: (Fact m, TensorG t r) => CycRep t D m r -> Maybe (CycRep t D m r)
  {-# INLINABLE divGDec #-}
  divGDec (Dec v) = Dec <$> T.divGDec v
  
  -- | Similar to 'divGPow'.
  divGCRTC :: (Fact m, CRTElt t r) => CycRep t C m r -> CycRep t C m r
  {-# INLINE divGCRTC #-}
  divGCRTC (CRTC s v) = CRTC s $ divGCRTCS s v
  
  -- | Yield the scaled squared norm of \(g_m \cdot e\) under
  -- the canonical embedding, namely,
  -- \(\hat{m}^{-1} \cdot \| \sigma(g_m \cdot e) \|^2\) .
  gSqNormDec :: (TensorGSqNorm t r, Fact m) => CycRep t D m r -> r
  {-# INLINABLE gSqNormDec #-}
  gSqNormDec (Dec v) = T.gSqNormDec v
  
  -- | Sample from the "tweaked" Gaussian error distribution \(t\cdot D\) in
  -- the decoding basis, where \(D\) has scaled variance \(v\).
  tweakedGaussian :: (TensorGaussian t q, MonadRandom rnd, Fact m, ToRational v)
                     => v -> rnd (CycRep t D m q)
  {-# INLINABLE tweakedGaussian #-}
  tweakedGaussian = fmap Dec . tweakedGaussianDec
  
  -- | Sample from the tweaked Gaussian with given scaled variance,
  -- deterministically rounded using the decoding basis. (This
  -- implementation uses 'Double' precision to generate the Gaussian
  -- sample, which might not be sufficient for rigorous proof-based
  -- security.)
  roundedGaussian :: forall v rnd t m z .
    (TensorGaussian t Double, IFElt t Double, IFunctor t, ToInteger z,
     IFElt t z, Fact m, ToRational v, MonadRandom rnd)
    => v -> rnd (CycRep t D m z)
  {-# INLINABLE roundedGaussian #-}
  roundedGaussian svar =
    Dec . fmapI (roundMult one) <$> (tweakedGaussianDec svar :: rnd (t m Double))
  
  -- | Sample from the tweaked Gaussian with scaled variance \(v \cdot
  -- p^2\), deterministically rounded to the given coset of \(R_p\)
  -- using the decoding basis. (This implementation uses 'Double'
  -- precision to generate the Gaussian sample, which may not be
  -- sufficient for rigorous proof-based security.)
  cosetGaussian :: forall t m zp z v rnd .
    (TensorGaussian t Double, IFElt t Double, IFunctor t, Lift zp z, Mod zp,
     z ~ ModRep zp, IFElt t zp, IFElt t z, Fact m, ToRational v, MonadRandom rnd)
    => v -> CycRep t D m zp -> rnd (CycRep t D m z)
  {-# INLINABLE cosetGaussian #-}
  cosetGaussian =
    let pval = fromIntegral $ modulus @zp
    in \ svar (Dec c) ->
      Dec . zipWithI roundCoset c <$>
      (tweakedGaussianDec (svar*pval*pval) :: rnd (t m Double))
  
  
  ----- inter-ring operations
  
  -- | Embed into an extension ring, for the powerful basis.
  embedPow :: (TensorPowDec t r, m `Divides` m') => CycRep t P m r -> CycRep t P m' r
  embedPow (Pow v) = Pow $ T.embedPow v
  {-# INLINABLE embedPow #-}
  
  -- | Embed into an extension ring, for the CRT basis.  (The output is
  -- an 'Either' because the extension ring might not support 'C'.)
  embedCRTC :: (m `Divides` m', CRTElt t r)
               => CycRep t C m r -> Either (CycRep t P m' r) (CycRep t C m' r)
  {-# INLINABLE embedCRTC #-}
  embedCRTC x@(CRTC s v) =
    case crtSentinel of
      -- go to CRTC if valid, else go to Pow
      Left  _  -> Left $ embedPow $ toPow x
      Right s' -> Right $ CRTC s' $ embedCRTCS s s' v
  
  -- | Similar to 'embedCRTC'.  (The output is an 'Either' because the
  -- extension ring might support 'C', in which case we never use 'E'.)
  embedCRTE :: forall m m' t r . (m `Divides` m', CRTElt t r)
               => CycRep t E m r -> Either (CycRep t P m' r) (CycRep t E m' r)
  {-# INLINABLE embedCRTE #-}
  embedCRTE x@(CRTE _ v) =
    case crtSentinel of
      -- go to CRTE if valid, else go to Pow
      Left  s -> Right $ CRTE s $ runIdentity T.embedCRT v
      Right _ -> Left $ embedPow $ toPow x
  
  -- | Twace into a subring, for the powerful basis.
  twacePow :: (TensorPowDec t r, m `Divides` m')
           => CycRep t P m' r -> CycRep t P m r
  {-# INLINABLE twacePow #-}
  twacePow (Pow v) = Pow $ twacePowDec v
  
  -- | Twace into a subring, for the decoding basis.
  twaceDec :: (TensorPowDec t r, m `Divides` m') => CycRep t D m' r -> CycRep t D m r
  {-# INLINABLE twaceDec #-}
  twaceDec (Dec v) = Dec $ twacePowDec v
  
  -- | Twace into a subring, for the CRT basis.  (The output is an
  -- 'Either' because the subring might not support 'C'.)
  twaceCRTC :: (m `Divides` m', CRTElt t r) => CycRep t C m' r -> CycRepPC t m r
  {-# INLINE twaceCRTC #-}
  twaceCRTC x@(CRTC s' v) =
    case crtSentinel of
      -- go to CRTC if valid for target, else go to Pow
      Left  _ -> Left $ twacePow $ toPow x
      Right s -> Right $ CRTC s $ twaceCRTCS s' s v
  
  -- | Similar to 'twaceCRTC'.  (The output is an 'Either' because the
  -- subring might support 'C', in which case we never use 'E'.)
  twaceCRTE :: forall t m m' r . (m `Divides` m', CRTElt t r)
               => CycRep t E m' r -> Either (CycRep t P m r) (CycRep t E m r)
  {-# INLINABLE twaceCRTE #-}
  twaceCRTE x@(CRTE _ v) =
    case crtSentinel of
      -- go to CRTE if valid for target, else go to Pow
      Left  s -> Right $ CRTE s $ runIdentity T.twaceCRT v
      Right _ -> Left $ twacePow $ toPow x
  
  -- | Yield the \(\O_m\)-coefficients of an \(\O_{m'}\)-element,
  -- with respect to the relative powerful \(\O_m\)-basis.
  coeffsPow :: (TensorPowDec t r, m `Divides` m') => CycRep t P m' r -> [CycRep t P m r]
  {-# INLINABLE coeffsPow #-}
  coeffsPow (Pow v) = Pow <$> coeffs v
  
  -- | Yield the \(\O_m\)-coefficients of an \(\O_{m'}\) element,
  -- with respect to the relative decoding \(\O_m\)-basis.
  coeffsDec :: (TensorPowDec t r, m `Divides` m') => CycRep t D m' r -> [CycRep t D m r]
  {-# INLINABLE coeffsDec #-}
  coeffsDec (Dec v) = Dec <$> coeffs v
  
  -- | The relative powerful basis of \(\O_{m'} / \O_m\).
  powBasis :: forall m m' t r .
    (TensorPowDec t r, m `Divides` m') => [CycRep t P m' r]
  {-# INLINABLE powBasis #-}
  powBasis = fmap Pow $ untag $ powBasisPow @t @r @m
  
  -- | The relative mod-\(r\) CRT set of \(\O_{m'} / \O_m\),
  -- represented with respect to the powerful basis (which seems to be
  -- the best choice for typical use cases).
  crtSet :: forall m m' pp p mbar m'bar t z zpp .
            (m `Divides` m', p ~ PrimePP pp, mbar ~ PFree p m, m'bar ~ PFree p m',
             PPow pp, Prime p, zpp ~ ZqBasic pp z,
             ToInteger z, CRTElt t zpp, TensorCRTSet t (ZqBasic p z))
         => [CycRep t P m' (ZqBasic pp z)]
  {-# INLINABLE crtSet #-}
  crtSet =
    -- CJP: consider using traceEvent or traceMarker
    --DT.trace ("CycRep.crtSet: m = " ++
    --          show (proxy valueFact (Proxy::Proxy m)) ++ ", m'= " ++
    --          show (proxy valueFact (Proxy::Proxy m'))) $
    let (p,e) = ppPPow @pp
        -- raise to the p^(e-1) power iteratively (one factor of p at a
        -- time), switching back to pow basis each time so that we don't
        -- lose precision!  (This fixes a bug witnessed for moderate
        -- values of e.)
        expon :: (Fact m'bar, ToPowDec t rep (ZqBasic pp z))
          => Int -> CycRep t rep m'bar zpp -> CycRep t P m'bar zpp
        expon 1  = toPow
        expon e' = toPowCE . (^p) . toCRT . expon (e'-1)
    in embedPow . expon e . Dec . fmapI (ZqB . unZqB) <$> -- safe!
       (untag $ crtSetDec @t @_ @mbar :: [t m'bar (ZqBasic p z)])
       \\ pFreeDivides @p @m @m' \\ pSplitTheorems @p @m \\ pSplitTheorems @p @m'
  
  
  --------- Changing representation ------------------
  
  class ToPowDec t rep r where
    -- | Convert to powerful-basis representation.
    toPow :: (Fact m) => CycRep t rep m r -> CycRep t P m r
    -- | Convert to decoding-basis representation.
    toDec :: (Fact m) => CycRep t rep m r -> CycRep t D m r
  
  -- | separate class because some base rings don't have a CRT basis
  class ToCRT t rep r where
    -- | Convert to an appropriate CRT-basis representation.
    toCRT :: (Fact m) => CycRep t rep m r -> Either (CycRep t E m r) (CycRep t C m r)
  
  instance TensorPowDec t r => ToPowDec t P r where
    toPow = id
    toDec (Pow v) = Dec $ powToDec v
    {-# INLINABLE toPow #-}
    {-# INLINABLE toDec #-}
  
  instance CRTElt t r => ToCRT t P r where
    toCRT (Pow v) = case crtSentinel of
                      Right s -> Right $ CRTC s $ crtCS s v
                      Left  s -> Left  $ CRTE s $ runIdentity crt $ fmapI toExt v
    {-# INLINABLE toCRT #-}
  
  instance TensorPowDec t r => ToPowDec t D r where
    toPow (Dec v) = Pow $ decToPow v
    toDec = id
    {-# INLINABLE toPow #-}
    {-# INLINABLE toDec #-}
  
  instance CRTElt t r => ToCRT t D r where
    toCRT = toCRT . toPow
    {-# INLINABLE toCRT #-}
  
  instance CRTElt t r => ToPowDec t C r where
    toPow (CRTC s v) = Pow $ crtInvCS s v
    toDec = toDec . toPow
    {-# INLINABLE toPow #-}
    {-# INLINABLE toDec #-}
  
  instance ToCRT t C r where
    toCRT = Right
    {-# INLINABLE toCRT #-}
  
  instance CRTElt t r => ToPowDec t E r where
    toPow (CRTE _ v) = Pow $ fmapI fromExt $ runIdentity crtInv v
    toDec = toDec . toPow
    {-# INLINABLE toPow #-}
    {-# INLINABLE toDec #-}
  
  instance ToCRT t E r where
    toCRT = Left
    {-# INLINABLE toCRT #-}
  
  {- CJP: non-class-based toPow etc., which can be defined for CycRep as a
     GADT or data family. But it doesn't quite work for us because the
     'CRTElt t r' constraint is too strong for 'r ~ RRq q Double', which
     can't have a CRTrans instance.
  
  {-# INLINABLE toPow #-}
  toPow :: (Fact m, CRTElt t r) => CycRep t rep m r -> CycRep t P m r
  toPow = \case
    c@(Pow _)  -> c
    (Dec  v)   -> Pow $ decToPow v
    (CRTC s v) -> Pow $ crtInvCS s v
    (CRTE _ v) -> Pow $ fmapI fromExt $ runIdentity crtInv v
  
  {-# INLINABLE toDec #-}
  toDec :: (Fact m, CRTElt t r) => CycRep t rep m r -> CycRep t D m r
  toDec = \case
    c@(Dec _)  -> c
    (Pow  v)   -> Dec $ powToDec v
    (CRTC s v) -> Dec $ powToDec $ crtInvCS s v
    (CRTE _ v) -> Dec $ powToDec $ fmapI fromExt $ runIdentity crtInv v
  
  {-# INLINABLE toCRT #-}
  toCRT :: (Fact m, CRTElt t r) => CycRep t rep m r -> CycRepEC t m r
  toCRT = \case
    c@(CRTC _ _) -> Right c
    c@(CRTE _ _) -> Left c
    (Pow v)      -> go v
    (Dec v)      -> go $ decToPow v
    where go v =
            case crtSentinel of
              Right s -> Right $ CRTC s $ crtCS s v
              Left  s -> Left  $ CRTE s $ runIdentity crt $ fmapI toExt v
  -}
  
  -- | Convenient version of 'toPow' for 'Either' CRT basis type.
  toPowCE :: (Fact m, CRTElt t r) => CycRepEC t m r -> CycRep t P m r
  {-# INLINABLE toPowCE #-}
  toPowCE (Left u)  = toPow u
  toPowCE (Right u) = toPow u
  
  
  ---------- Category-theoretic instances ----------
  
  ----- No instances for E because types (and math) don't make sense.
  
  -- | apply coefficient-wise
  instance IFunctor t => IFunctor (CycRep t P) where
    type IFElt (CycRep t P) a = IFElt t a
    fmapI    f (Pow v)         = Pow $ fmapI f v
    zipWithI f (Pow v) (Pow w) = Pow $ zipWithI f v w
  
  -- | apply coefficient-wise
  instance IFunctor t => IFunctor (CycRep t D) where
    type IFElt (CycRep t D) a = IFElt t a
    fmapI    f (Dec v)         = Dec $ fmapI f v
    zipWithI f (Dec v) (Dec w) = Dec $ zipWithI f v w
  
  -- | apply coefficient-wise
  instance Functor (t m) => Functor (CycRep t P m) where
    {-# INLINABLE fmap #-}
    fmap f (Pow x) = Pow $ f <$> x
  
  -- | apply coefficient-wise
  instance Functor (t m) => Functor (CycRep t D m) where
    {-# INLINABLE fmap #-}
    fmap f (Dec x) = Dec $ f <$> x
  
  -- No Functor instance for C, because CRTrans a doesn't imply CRTrans b.
  
  instance Applicative (t m) => Applicative (CycRep t P m) where
    pure = Pow . pure
    (Pow f) <*> (Pow v) = Pow $ f <*> v
    {-# INLINABLE pure #-}
    {-# INLINABLE (<*>) #-}
  
  instance Applicative (t m) => Applicative (CycRep t D m) where
    pure = Dec . pure
    (Dec f) <*> (Dec v) = Dec $ f <*> v
    {-# INLINABLE pure #-}
    {-# INLINABLE (<*>) #-}
  
  -- CJP: no Applicative instance for C, because 'pure' would circumvent
  -- the invariant.  Moreover, `CRTrans (a -> b)` and `CRTrans a`
  -- doesn't imply `CRTrans b`.
  
  instance Foldable (t m) => Foldable (CycRep t P m) where
    foldr f z (Pow x) = foldr f z x
  
  instance Foldable (t m) => Foldable (CycRep t D m) where
    foldr f z (Dec x) = foldr f z x
  
  -- no Traversable for C, but it is Foldable
  instance Foldable (t m) => Foldable (CycRep t C m) where
    foldr f b (CRTC _ v) = foldr f b v
  
  instance Traversable (t m) => Traversable (CycRep t P m) where
    {-# INLINABLE traverse #-}
    traverse f (Pow v) = Pow <$> traverse f v
  
  instance Traversable (t m) => Traversable (CycRep t D m) where
    {-# INLINABLE traverse #-}
    traverse f (Dec v) = Dec <$> traverse f v
  
  -- CJP: no Traversable instance for C, because no Functor instance
  -- (see above)
  
  
  ---------- Utility instances ----------
  
  instance (Random (t m r)) => Random (CycRep t P m r) where
    random g = let (v,g') = random g
               in (Pow v, g')
    randomR _ = error "randomR non-sensical for CycRep"
  
  instance (Random (t m r)) => Random (CycRep t D m r) where
    random g = let (v,g') = random g
               in (Dec v, g')
    randomR _ = error "randomR non-sensical for CycRep"
  
  instance (Random (t m r), Fact m, TensorCRT t Maybe r)
    => Random (CycRepPC t m r) where
    -- create in CRTC basis if possible, otherwise in powerful
    random = let cons = case crtSentinel of
                   Left  _ -> Left  . Pow
                   Right s -> Right . CRTC s
             in \g -> let (v,g') = random g
                      in (cons v, g')
    randomR _ = error "randomR non-sensical for CycRep"
  
  instance (Show (t m r)) => Show (CycRep t P m r) where
    show (Pow x) = "CycRep.Pow " ++ show x
  
  instance (Show (t m r)) => Show (CycRep t D m r) where
    show (Dec x) = "CycRep.Dec " ++ show x
  
  instance (Show (t m r)) => Show (CycRep t C m r) where
    show (CRTC _ x) = "CycRep.CRTC " ++ show x
  
  instance (Show (t m (CRTExt r))) => Show (CycRep t E m r) where
    show (CRTE _ x) = "CycRep.CRTE " ++ show x
  
  
  instance (NFData (t m r)) => NFData (CycRep t P m r) where
    rnf (Pow x) = rnf x
  
  instance (NFData (t m r)) => NFData (CycRep t D m r) where
    rnf (Dec x) = rnf x
  
  instance (NFData (t m r)) => NFData (CycRep t C m r) where
    rnf (CRTC _ x) = rnf x
  
  instance (NFData (t m (CRTExt r))) => NFData (CycRep t E m r) where
    rnf (CRTE _ x) = rnf x
  
  
  instance (Protoable (t m r)) => Protoable (CycRep t D m r) where
    type ProtoType (CycRep t D m r) = ProtoType (t m r)
    toProto (Dec t) = toProto t
    fromProto t = Dec <$> fromProto t
  