Copyright	(c) Eric Crockett 2011-2017 Chris Peikert 2011-2017
License	GPL-3
Maintainer	ecrockett0@email.com
Stability	experimental
Portability	POSIX \( \def\O{\mathcal{O}} \)
Safe Haskell	None
Language	Haskell2010

Crypto.Lol.Applications.SymmBGV

Contents

Data types
Keygen, encryption, decryption
Arithmetic with public values
Modulus switching
Key switching
Ring switching
Arithmetic
Constraint synonyms
Orphan instances

Description

Symmetric-key somewhat homomorphic encryption. See Section 4 of http://eprint.iacr.org/2015/1134 for mathematical description.

Synopsis

data SK r
type PT rp = rp
data CT (d :: Nat) m zp r'q
genSK :: (GenSKCtx c m z v, MonadRandom rnd) => v -> rnd (SK (c m z))
genAnotherSK :: (GenSKCtx c m z a, MonadRandom rnd) => SK a -> rnd (SK (c m z))
encrypt :: forall c m m' z zp zq rnd. (EncryptCtx c m m' z zp zq, MonadRandom rnd) => SK (c m' z) -> PT (c m zp) -> rnd (CT 1 m zp (c m' zq))
errorTerm :: ErrorTermCtx c m' z zp zq => SK (c m' z) -> CT d m zp (c m' zq) -> LiftOf (c m' zq)
decrypt :: forall c m m' z zp zq d. DecryptCtx c m m' z zp zq => SK (c m' z) -> CT d m zp (c m' zq) -> PT (c m zp)
addPublic :: forall c m m' zp zq d. AddPublicCtx c m m' zp zq => c m zp -> CT d m zp (c m' zq) -> CT d m zp (c m' zq)
mulPublic :: forall c m m' zp zq d. MulPublicCtx c m m' zp zq => c m zp -> CT d m zp (c m' zq) -> CT d m zp (c m' zq)
modSwitch :: ModSwitchCtx c m' zp zq zq' => CT d m zp (c m' zq) -> CT d m zp (c m' zq')
modSwitchPT :: ModSwitchPTCtx c m' zp zp' zq => CT d m zp (c m' zq) -> CT d m zp' (c m' zq)
data KSHint gad r'q'
ksLinearHint :: forall gad c m' z zq' rnd. (KSHintCtx gad c m' z zq', MonadRandom rnd) => SK (c m' z) -> SK (c m' z) -> rnd (KSHint gad (c m' zq'))
ksQuadCircHint :: forall gad c m' z zq' rnd. (KSHintCtx gad c m' z zq', Ring (c m' z), MonadRandom rnd) => SK (c m' z) -> rnd (KSHint gad (c m' zq'))
keySwitchLinear :: forall gad c m m' zp zq'. KeySwitchCtx gad c m' zp zq' => KSHint gad (c m' zq') -> CT 1 m zp (c m' zq') -> CT 1 m zp (c m' zq')
keySwitchQuadCirc :: forall gad c m m' zp zq'. KeySwitchCtx gad c m' zp zq' => KSHint gad (c m' zq') -> CT 2 m zp (c m' zq') -> CT 1 m zp (c m' zq')
embedSK :: (m `Divides` m', ExtensionCyc c z) => SK (c m z) -> SK (c m' z)
embedCT :: (r `Divides` r', s `Divides` s', r `Divides` s, r' `Divides` s', ExtensionCyc c zq, AbsorbGCtx c r' zp zq) => CT d r zp (c r' zq) -> CT d s zp (c s' zq)
twaceCT :: (r `Divides` r', s' `Divides` r', s ~ FGCD s' r, ExtensionCyc c zq, AbsorbGCtx c r' zp zq) => CT d r zp (c r' zq) -> CT d s zp (c s' zq)
data TunnelHint gad c e r s e' r' s' zp zq
tunnelHint :: forall gad c e r s e' r' s' z zp zq' rnd. (MonadRandom rnd, TunnelHintCtx c e r s e' r' s' z zp zq' gad) => Linear c e r s zp -> SK (c s' z) -> SK (c r' z) -> rnd (TunnelHint gad c e r s e' r' s' zp zq')
tunnel :: forall gad c e r s e' r' s' zp zq' d. TunnelCtx c r s e' r' s' zp zq' gad => TunnelHint gad c e r s e' r' s' zp zq' -> CT d r zp (c r' zq') -> CT d s zp (c s' zq')
addCT :: forall c m m' zp zq d1 d2. AddCTCtx c m m' zp zq => CT d1 m zp (c m' zq) -> CT d2 m zp (c m' zq) -> CT (Max d1 d2) m zp (c m' zq)
mulCT :: forall c m m' zp zq d1 d2. MulCTCtx c m' zp zq => CT d1 m zp (c m' zq) -> CT d2 m zp (c m' zq) -> CT (d1 + d2) m zp (c m' zq)
negateCT :: NegateCTCtx c m' zq => CT d m zp (c m' zq) -> CT d m zp (c m' zq)
type AddCTCtx c m m' zp zq = (Lift' zp, Reduce (LiftOf zp) zq, ToSDCtx c m' zp zq, Eq zp, m `Divides` m')
type MulCTCtx c m' zp zq = ToSDCtx c m' zp zq
type NegateCTCtx c m' zq = Additive (c m' zq)
type family Max (arg :: a) (arg1 :: a) :: a
type family (a :: Nat) + (b :: Nat) :: Nat where ...
type GenSKCtx c m z v = (ToInteger z, RoundedGaussianCyc (c m z), ToRational v, NFData v)
type EncryptCtx c m m' z zp zq = (Ring zp, Cyclotomic (c m' zq), Ring (c m' zq), Random (c m' zq), Reduce (c m' z) (c m' zq), Reduce (LiftOf (c m' zp)) (c m' zq), CosetGaussianCyc (c m' zp), ExtensionCyc c zp, m `Divides` m')
type ToSDCtx c m' zp zq = (Encode zp zq, Cyclotomic (c m' zq), Ring (c m' zq), Module zq (c m' zq))
type ErrorTermCtx c m' z zp zq = (ToSDCtx c m' zp zq, Ring (c m' zq), Reduce (c m' z) (c m' zq), LiftCyc (c m' zq))
type DecryptCtx c m m' z zp zq = (ErrorTermCtx c m' z zp zq, Cyclotomic (c m' zp), Module zp (c m zp), Reduce (LiftOf (c m' zq)) (c m' zp), ExtensionCyc c zp, m `Divides` m')
type AddPublicCtx c m m' zp zq = (ToSDCtx c m' zp zq, Cyclotomic (c m zp), Module zp (c m zp), LiftCyc (c m zp), Reduce (LiftOf (c m zp)) (c m zq), ExtensionCyc c zq, m `Divides` m')
type MulPublicCtx c m m' zp zq = (LiftCyc (c m zp), Reduce (LiftOf (c m zp)) (c m zq), ExtensionCyc c zq, m `Divides` m', Ring (c m' zq))
type ModSwitchCtx c m' zp zq zq' = (RescaleCyc (c m') zq zq', ToSDCtx c m' zp zq)
type ModSwitchPTCtx c m' zp zp' zq = (Lift' zp, Reduce (LiftOf zp) zp', ToSDCtx c m' zp zq)
type KSHintCtx gad c m' z zq = (LWECtx c m' z zq, Gadget gad (c m' zq))
type KeySwitchCtx gad c m' zp zq' = (ToSDCtx c m' zp zq', SwitchCtx gad c m' zq')
type TunnelHintCtx c e r s e' r' s' z zp zq' gad = (ExtendLinCtx c e r s e' r' s' zp, e' ~ (e * (r' / r)), Fact r, z ~ LiftOf zp, KSHintCtx gad c s' z zq', LiftCyc (c s zp), LiftOf (c s zp) ~ c s z, ExtensionCyc c z, e' `Divides` r', Reduce (c s' z) (c s' zq'), Cyclotomic (c r' z), Ring (c r' z), Ring (c s' z), Random (c s' zq'), Gadget gad (c s' zq'))
type TunnelCtx c r s e' r' s' zp zq' gad = (Fact r, Fact s, e' `Divides` r', e' `Divides` s', ExtensionCyc c zq', ToSDCtx c r' zp zq', AbsorbGCtx c r' zp zq', SwitchCtx gad c s' zq')
type SwitchCtx gad c m' zq = (Cyclotomic (c m' zq), Ring (c m' zq), Decompose gad (c m' zq), Reduce (DecompOf (c m' zq)) (c m' zq))
type LWECtx c m' z zq = (Cyclotomic (c m' zq), RoundedGaussianCyc (c m' z), Reduce (c m' z) (c m' zq), Random (c m' zq), Ring (c m' zq))

Data types

data SK r Source #

secret key

Instances

Show r => Show (SK r) Source #
Instance details Defined in Crypto.Lol.Applications.SymmBGV Methods showsPrec :: Int -> SK r -> ShowS # show :: SK r -> String # showList :: [SK r] -> ShowS #
GenSKCtx c m' z Double => Random (SK (c m' z)) Source #
Instance details Defined in Crypto.Lol.Applications.Tests.BGVTests Methods randomR :: RandomGen g => (SK (c m' z), SK (c m' z)) -> g -> (SK (c m' z), g) # random :: RandomGen g => g -> (SK (c m' z), g) # randomRs :: RandomGen g => (SK (c m' z), SK (c m' z)) -> g -> [SK (c m' z)] # randoms :: RandomGen g => g -> [SK (c m' z)] # randomRIO :: (SK (c m' z), SK (c m' z)) -> IO (SK (c m' z)) # randomIO :: IO (SK (c m' z)) #
NFData r => NFData (SK r) Source #
Instance details Defined in Crypto.Lol.Applications.SymmBGV Methods rnf :: SK r -> () #
(Protoable r, ProtoType r ~ R) => Protoable (SK r) Source #
Instance details Defined in Crypto.Lol.Applications.SymmBGV Associated Types type ProtoType (SK r) :: Type # Methods toProto :: SK r -> ProtoType (SK r) # fromProto :: MonadError String m => ProtoType (SK r) -> m (SK r) #
type ProtoType (SK r) Source #
Instance details Defined in Crypto.Lol.Applications.SymmBGV type ProtoType (SK r) = SecretKey

type PT rp = rp Source #

plaintext

data CT (d :: Nat) m zp r'q Source #

Ciphertext of degree (at most) \(d\) over \( R'_q \) encrypting a plaintext in \( R_p \), where \( R=\mathcal{O}_m \).

Instances

(Show zp, Show r'q) => Show (CT d m zp r'q) Source #
Instance details Defined in Crypto.Lol.Applications.SymmBGV Methods showsPrec :: Int -> CT d m zp r'q -> ShowS # show :: CT d m zp r'q -> String # showList :: [CT d m zp r'q] -> ShowS #
Generic (CT d m zp r'q) Source #
Instance details Defined in Crypto.Lol.Applications.SymmBGV Associated Types type Rep (CT d m zp r'q) :: Type -> Type # Methods from :: CT d m zp r'q -> Rep (CT d m zp r'q) x # to :: Rep (CT d m zp r'q) x -> CT d m zp r'q #
(NFData zp, NFData r'q) => NFData (CT d m zp r'q) Source #
Instance details Defined in Crypto.Lol.Applications.SymmBGV Methods rnf :: CT d m zp r'q -> () #
type Rep (CT d m zp r'q) Source #
Instance details Defined in Crypto.Lol.Applications.SymmBGV type Rep (CT d m zp r'q)

Keygen, encryption, decryption

genSK :: (GenSKCtx c m z v, MonadRandom rnd) => v -> rnd (SK (c m z)) Source #

Generates a secret key with (index-independent) scaled variance parameter \( v \); see roundedGaussian.

genAnotherSK :: (GenSKCtx c m z a, MonadRandom rnd) => SK a -> rnd (SK (c m z)) Source #

Generates a secret key with the same scaled variance as the given secret key.

encrypt :: forall c m m' z zp zq rnd. (EncryptCtx c m m' z zp zq, MonadRandom rnd) => SK (c m' z) -> PT (c m zp) -> rnd (CT 1 m zp (c m' zq)) Source #

Encrypt a plaintext under a secret key.

errorTerm :: ErrorTermCtx c m' z zp zq => SK (c m' z) -> CT d m zp (c m' zq) -> LiftOf (c m' zq) Source #

Extract the error term of a ciphertext.

decrypt :: forall c m m' z zp zq d. DecryptCtx c m m' z zp zq => SK (c m' z) -> CT d m zp (c m' zq) -> PT (c m zp) Source #

Decrypt a ciphertext.

Arithmetic with public values

addPublic :: forall c m m' zp zq d. AddPublicCtx c m m' zp zq => c m zp -> CT d m zp (c m' zq) -> CT d m zp (c m' zq) Source #

Homomorphically add a public \( R_p \) value to an encrypted value.

mulPublic :: forall c m m' zp zq d. MulPublicCtx c m m' zp zq => c m zp -> CT d m zp (c m' zq) -> CT d m zp (c m' zq) Source #

Homomorphically multiply an encrypted value by a public \( R_p \) value.

Modulus switching

modSwitch :: ModSwitchCtx c m' zp zq zq' => CT d m zp (c m' zq) -> CT d m zp (c m' zq') Source #

Rescale a ciphertext to a new modulus.

modSwitchPT :: ModSwitchPTCtx c m' zp zp' zq => CT d m zp (c m' zq) -> CT d m zp' (c m' zq) Source #

Homomorphically divide a plaintext that is known to be a multiple of \( (p/p') \) by that factor, thereby scaling the plaintext modulus from \( p \) to \( p' \).

Key switching

data KSHint gad r'q' Source #

Key-switch hint.

Instances

Generic (KSHint gad r'q') Source #
Instance details Defined in Crypto.Lol.Applications.SymmBGV Associated Types type Rep (KSHint gad r'q') :: Type -> Type # Methods from :: KSHint gad r'q' -> Rep (KSHint gad r'q') x # to :: Rep (KSHint gad r'q') x -> KSHint gad r'q' #
NFData r'q' => NFData (KSHint gad r'q') Source #
Instance details Defined in Crypto.Lol.Applications.SymmBGV Methods rnf :: KSHint gad r'q' -> () #
(Typeable gad, Protoable r'q', ProtoType r'q' ~ RqProduct) => Protoable (KSHint gad r'q') Source #
Instance details Defined in Crypto.Lol.Applications.SymmBGV Associated Types type ProtoType (KSHint gad r'q') :: Type # Methods toProto :: KSHint gad r'q' -> ProtoType (KSHint gad r'q') # fromProto :: MonadError String m => ProtoType (KSHint gad r'q') -> m (KSHint gad r'q') #
type Rep (KSHint gad r'q') Source #
Instance details Defined in Crypto.Lol.Applications.SymmBGV type Rep (KSHint gad r'q') = D1 (MetaData "KSHint" "Crypto.Lol.Applications.SymmBGV" "lol-apps-0.3.0.0-Khey1psotef4oHNynjEogf" True) (C1 (MetaCons "KSHint" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Polynomial r'q'])))
type ProtoType (KSHint gad r'q') Source #
Instance details Defined in Crypto.Lol.Applications.SymmBGV type ProtoType (KSHint gad r'q') = KSHint

ksLinearHint :: forall gad c m' z zq' rnd. (KSHintCtx gad c m' z zq', MonadRandom rnd) => SK (c m' z) -> SK (c m' z) -> rnd (KSHint gad (c m' zq')) Source #

A hint to switch a linear ciphertext under \( s_{\text{in}} \) to a linear one under \( s_{\text{out}} \).

ksQuadCircHint :: forall gad c m' z zq' rnd. (KSHintCtx gad c m' z zq', Ring (c m' z), MonadRandom rnd) => SK (c m' z) -> rnd (KSHint gad (c m' zq')) Source #

A hint to switch a quadratic ciphertext to a linear one under the same key.

keySwitchLinear :: forall gad c m m' zp zq'. KeySwitchCtx gad c m' zp zq' => KSHint gad (c m' zq') -> CT 1 m zp (c m' zq') -> CT 1 m zp (c m' zq') Source #

Switch a linear ciphertext using the supplied hint. (The input ciphertext may first need to be rescaled so that its modulus matches that of the hint.)

keySwitchQuadCirc :: forall gad c m m' zp zq'. KeySwitchCtx gad c m' zp zq' => KSHint gad (c m' zq') -> CT 2 m zp (c m' zq') -> CT 1 m zp (c m' zq') Source #

Switch a ciphertext of degree two or less (i.e., one with no more than three components) to a ciphertext of degree one (or less) under the same key, using the supplied hint. (The input ciphertext may first need to be rescaled so that its modulus matches that of the hint.)

Ring switching

embedSK :: (m `Divides` m', ExtensionCyc c z) => SK (c m z) -> SK (c m' z) Source #

Embed a secret key from a subring into a superring.

embedCT :: (r `Divides` r', s `Divides` s', r `Divides` s, r' `Divides` s', ExtensionCyc c zq, AbsorbGCtx c r' zp zq) => CT d r zp (c r' zq) -> CT d s zp (c s' zq) Source #

Embed a ciphertext in \( R' \) encrypting a plaintext in \( R \) to a ciphertext in \( T' \) encrypting a plaintext in \( T \). The target ciphertext ring \( T' \) must contain both the the source ciphertext ring \( R' \) and the target plaintext ring \( T \).

twaceCT :: (r `Divides` r', s' `Divides` r', s ~ FGCD s' r, ExtensionCyc c zq, AbsorbGCtx c r' zp zq) => CT d r zp (c r' zq) -> CT d s zp (c s' zq) Source #

"Tweaked trace" function for ciphertexts. Mathematically, the target plaintext ring \( S \) must contain the intersection of the source plaintext ring \( T \) and the target ciphertext ring ( S' ). Here we make the stricter requirement that ( s = gcd(s', t) ).

data TunnelHint gad c e r s e' r' s' zp zq Source #

Auxilliary data needed to tunnel from \(\O_{r'}\) to \(\O_{s'}\).

Instances

(Show (c s' zq), Show (KSHint gad (c s' zq))) => Show (TunnelHint gad c e r s e' r' s' zp zq) Source #
Instance details Defined in Crypto.Lol.Applications.SymmBGV Methods showsPrec :: Int -> TunnelHint gad c e r s e' r' s' zp zq -> ShowS # show :: TunnelHint gad c e r s e' r' s' zp zq -> String # showList :: [TunnelHint gad c e r s e' r' s' zp zq] -> ShowS #
Generic (TunnelHint gad c e r s e' r' s' zp zq) Source #
Instance details Defined in Crypto.Lol.Applications.SymmBGV Associated Types type Rep (TunnelHint gad c e r s e' r' s' zp zq) :: Type -> Type # Methods from :: TunnelHint gad c e r s e' r' s' zp zq -> Rep (TunnelHint gad c e r s e' r' s' zp zq) x # to :: Rep (TunnelHint gad c e r s e' r' s' zp zq) x -> TunnelHint gad c e r s e' r' s' zp zq #
NFData (c s' zq) => NFData (TunnelHint gad c e r s e' r' s' zp zq) Source #
Instance details Defined in Crypto.Lol.Applications.SymmBGV Methods rnf :: TunnelHint gad c e r s e' r' s' zp zq -> () #
(Mod zp, Typeable gad, Protoable (Linear c e' r' s' zq), Protoable (KSHint gad (c s' zq)), Reflects s Int, Reflects r Int, Reflects e Int) => Protoable (TunnelHint gad c e r s e' r' s' zp zq) Source #
Instance details Defined in Crypto.Lol.Applications.SymmBGV Associated Types type ProtoType (TunnelHint gad c e r s e' r' s' zp zq) :: Type # Methods toProto :: TunnelHint gad c e r s e' r' s' zp zq -> ProtoType (TunnelHint gad c e r s e' r' s' zp zq) # fromProto :: MonadError String m => ProtoType (TunnelHint gad c e r s e' r' s' zp zq) -> m (TunnelHint gad c e r s e' r' s' zp zq) #
type Rep (TunnelHint gad c e r s e' r' s' zp zq) Source #
Instance details Defined in Crypto.Lol.Applications.SymmBGV type Rep (TunnelHint gad c e r s e' r' s' zp zq) = D1 (MetaData "TunnelHint" "Crypto.Lol.Applications.SymmBGV" "lol-apps-0.3.0.0-Khey1psotef4oHNynjEogf" False) (C1 (MetaCons "THint" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Linear c e' r' s' zq)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [KSHint gad (c s' zq)])))
type ProtoType (TunnelHint gad c e r s e' r' s' zp zq) Source #
Instance details Defined in Crypto.Lol.Applications.SymmBGV type ProtoType (TunnelHint gad c e r s e' r' s' zp zq) = TunnelHint

tunnelHint :: forall gad c e r s e' r' s' z zp zq' rnd. (MonadRandom rnd, TunnelHintCtx c e r s e' r' s' z zp zq' gad) => Linear c e r s zp -> SK (c s' z) -> SK (c r' z) -> rnd (TunnelHint gad c e r s e' r' s' zp zq') Source #

Generates auxilliary data needed to tunnel from \( \O_{r'} \) to \( \O_{s'} \).

tunnel :: forall gad c e r s e' r' s' zp zq' d. TunnelCtx c r s e' r' s' zp zq' gad => TunnelHint gad c e r s e' r' s' zp zq' -> CT d r zp (c r' zq') -> CT d s zp (c s' zq') Source #

Homomorphically apply the \( E \)-linear function that maps the elements of the decoding basis of \( R/E \) to the corresponding \( S \)-elements in the input array.

Arithmetic

addCT :: forall c m m' zp zq d1 d2. AddCTCtx c m m' zp zq => CT d1 m zp (c m' zq) -> CT d2 m zp (c m' zq) -> CT (Max d1 d2) m zp (c m' zq) Source #

mulCT :: forall c m m' zp zq d1 d2. MulCTCtx c m' zp zq => CT d1 m zp (c m' zq) -> CT d2 m zp (c m' zq) -> CT (d1 + d2) m zp (c m' zq) Source #

negateCT :: NegateCTCtx c m' zq => CT d m zp (c m' zq) -> CT d m zp (c m' zq) Source #

type AddCTCtx c m m' zp zq = (Lift' zp, Reduce (LiftOf zp) zq, ToSDCtx c m' zp zq, Eq zp, m `Divides` m') Source #

type MulCTCtx c m' zp zq = ToSDCtx c m' zp zq Source #

type NegateCTCtx c m' zq = Additive (c m' zq) Source #

type family Max (arg :: a) (arg1 :: a) :: a #

Instances

type Max (arg1 :: Bool) (arg2 :: Bool)
Instance details Defined in Data.Singletons.Prelude.Ord type Max (arg1 :: Bool) (arg2 :: Bool) = Apply (Apply (Max_6989586621679380204Sym0 :: TyFun Bool (Bool ~> Bool) -> Type) arg1) arg2
type Max (arg1 :: Ordering) (arg2 :: Ordering)
Instance details Defined in Data.Singletons.Prelude.Ord type Max (arg1 :: Ordering) (arg2 :: Ordering) = Apply (Apply (Max_6989586621679380204Sym0 :: TyFun Ordering (Ordering ~> Ordering) -> Type) arg1) arg2
type Max (arg1 :: Nat) (arg2 :: Nat)
Instance details Defined in Data.Singletons.TypeLits.Internal type Max (arg1 :: Nat) (arg2 :: Nat) = Apply (Apply (Max_6989586621679380204Sym0 :: TyFun Nat (Nat ~> Nat) -> Type) arg1) arg2
type Max (arg1 :: Symbol) (arg2 :: Symbol)
Instance details Defined in Data.Singletons.TypeLits.Internal type Max (arg1 :: Symbol) (arg2 :: Symbol) = Apply (Apply (Max_6989586621679380204Sym0 :: TyFun Symbol (Symbol ~> Symbol) -> Type) arg1) arg2
type Max (arg1 :: ()) (arg2 :: ())
Instance details Defined in Data.Singletons.Prelude.Ord type Max (arg1 :: ()) (arg2 :: ()) = Apply (Apply (Max_6989586621679380204Sym0 :: TyFun () (() ~> ()) -> Type) arg1) arg2
type Max (arg1 :: Void) (arg2 :: Void)
Instance details Defined in Data.Singletons.Prelude.Ord type Max (arg1 :: Void) (arg2 :: Void) = Apply (Apply (Max_6989586621679380204Sym0 :: TyFun Void (Void ~> Void) -> Type) arg1) arg2
type Max (arg1 :: All) (arg2 :: All)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Max (arg1 :: All) (arg2 :: All) = Apply (Apply (Max_6989586621679380204Sym0 :: TyFun All (All ~> All) -> Type) arg1) arg2
type Max (arg1 :: Any) (arg2 :: Any)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Max (arg1 :: Any) (arg2 :: Any) = Apply (Apply (Max_6989586621679380204Sym0 :: TyFun Any (Any ~> Any) -> Type) arg1) arg2
type Max (arg :: PrimeBin) (arg1 :: PrimeBin)
Instance details Defined in Crypto.Lol.FactoredDefs type Max (arg :: PrimeBin) (arg1 :: PrimeBin) = Apply (Apply (Max_6989586621679380204Sym0 :: TyFun PrimeBin (PrimeBin ~> PrimeBin) -> Type) arg) arg1
type Max (arg :: Bin) (arg1 :: Bin)
Instance details Defined in Crypto.Lol.PosBinDefs type Max (arg :: Bin) (arg1 :: Bin) = Apply (Apply (Max_6989586621679380204Sym0 :: TyFun Bin (Bin ~> Bin) -> Type) arg) arg1
type Max (arg :: Pos) (arg1 :: Pos)
Instance details Defined in Crypto.Lol.PosBinDefs type Max (arg :: Pos) (arg1 :: Pos) = Apply (Apply (Max_6989586621679380204Sym0 :: TyFun Pos (Pos ~> Pos) -> Type) arg) arg1
type Max (arg1 :: [a]) (arg2 :: [a])
Instance details Defined in Data.Singletons.Prelude.Ord type Max (arg1 :: [a]) (arg2 :: [a]) = Apply (Apply (Max_6989586621679380204Sym0 :: TyFun [a] ([a] ~> [a]) -> Type) arg1) arg2
type Max (arg1 :: Maybe a) (arg2 :: Maybe a)
Instance details Defined in Data.Singletons.Prelude.Ord type Max (arg1 :: Maybe a) (arg2 :: Maybe a) = Apply (Apply (Max_6989586621679380204Sym0 :: TyFun (Maybe a) (Maybe a ~> Maybe a) -> Type) arg1) arg2
type Max (arg1 :: Min a) (arg2 :: Min a)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Max (arg1 :: Min a) (arg2 :: Min a) = Apply (Apply (Max_6989586621679380204Sym0 :: TyFun (Min a) (Min a ~> Min a) -> Type) arg1) arg2
type Max (arg1 :: Max a) (arg2 :: Max a)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Max (arg1 :: Max a) (arg2 :: Max a) = Apply (Apply (Max_6989586621679380204Sym0 :: TyFun (Max a) (Max a ~> Max a) -> Type) arg1) arg2
type Max (arg1 :: First a) (arg2 :: First a)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Max (arg1 :: First a) (arg2 :: First a) = Apply (Apply (Max_6989586621679380204Sym0 :: TyFun (First a) (First a ~> First a) -> Type) arg1) arg2
type Max (arg1 :: Last a) (arg2 :: Last a)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Max (arg1 :: Last a) (arg2 :: Last a) = Apply (Apply (Max_6989586621679380204Sym0 :: TyFun (Last a) (Last a ~> Last a) -> Type) arg1) arg2
type Max (arg1 :: WrappedMonoid m) (arg2 :: WrappedMonoid m)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Max (arg1 :: WrappedMonoid m) (arg2 :: WrappedMonoid m) = Apply (Apply (Max_6989586621679380204Sym0 :: TyFun (WrappedMonoid m) (WrappedMonoid m ~> WrappedMonoid m) -> Type) arg1) arg2
type Max (arg1 :: Option a) (arg2 :: Option a)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Max (arg1 :: Option a) (arg2 :: Option a) = Apply (Apply (Max_6989586621679380204Sym0 :: TyFun (Option a) (Option a ~> Option a) -> Type) arg1) arg2
type Max (arg1 :: Identity a) (arg2 :: Identity a)
Instance details Defined in Data.Singletons.Prelude.Ord type Max (arg1 :: Identity a) (arg2 :: Identity a) = Apply (Apply (Max_6989586621679380204Sym0 :: TyFun (Identity a) (Identity a ~> Identity a) -> Type) arg1) arg2
type Max (arg1 :: First a) (arg2 :: First a)
Instance details Defined in Data.Singletons.Prelude.Monoid type Max (arg1 :: First a) (arg2 :: First a) = Apply (Apply (Max_6989586621679380204Sym0 :: TyFun (First a) (First a ~> First a) -> Type) arg1) arg2
type Max (arg1 :: Last a) (arg2 :: Last a)
Instance details Defined in Data.Singletons.Prelude.Monoid type Max (arg1 :: Last a) (arg2 :: Last a) = Apply (Apply (Max_6989586621679380204Sym0 :: TyFun (Last a) (Last a ~> Last a) -> Type) arg1) arg2
type Max (arg1 :: Dual a) (arg2 :: Dual a)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Max (arg1 :: Dual a) (arg2 :: Dual a) = Apply (Apply (Max_6989586621679380204Sym0 :: TyFun (Dual a) (Dual a ~> Dual a) -> Type) arg1) arg2
type Max (arg1 :: Sum a) (arg2 :: Sum a)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Max (arg1 :: Sum a) (arg2 :: Sum a) = Apply (Apply (Max_6989586621679380204Sym0 :: TyFun (Sum a) (Sum a ~> Sum a) -> Type) arg1) arg2
type Max (arg1 :: Product a) (arg2 :: Product a)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Max (arg1 :: Product a) (arg2 :: Product a) = Apply (Apply (Max_6989586621679380204Sym0 :: TyFun (Product a) (Product a ~> Product a) -> Type) arg1) arg2
type Max (arg1 :: Down a) (arg2 :: Down a)
Instance details Defined in Data.Singletons.Prelude.Ord type Max (arg1 :: Down a) (arg2 :: Down a) = Apply (Apply (Max_6989586621679380204Sym0 :: TyFun (Down a) (Down a ~> Down a) -> Type) arg1) arg2
type Max (arg1 :: NonEmpty a) (arg2 :: NonEmpty a)
Instance details Defined in Data.Singletons.Prelude.Ord type Max (arg1 :: NonEmpty a) (arg2 :: NonEmpty a) = Apply (Apply (Max_6989586621679380204Sym0 :: TyFun (NonEmpty a) (NonEmpty a ~> NonEmpty a) -> Type) arg1) arg2
type Max (arg1 :: Either a b) (arg2 :: Either a b)
Instance details Defined in Data.Singletons.Prelude.Ord type Max (arg1 :: Either a b) (arg2 :: Either a b) = Apply (Apply (Max_6989586621679380204Sym0 :: TyFun (Either a b) (Either a b ~> Either a b) -> Type) arg1) arg2
type Max (arg1 :: (a, b)) (arg2 :: (a, b))
Instance details Defined in Data.Singletons.Prelude.Ord type Max (arg1 :: (a, b)) (arg2 :: (a, b)) = Apply (Apply (Max_6989586621679380204Sym0 :: TyFun (a, b) ((a, b) ~> (a, b)) -> Type) arg1) arg2
type Max (a2 :: Arg a1 b) (a3 :: Arg a1 b)
Instance details Defined in Data.Singletons.Prelude.Semigroup type Max (a2 :: Arg a1 b) (a3 :: Arg a1 b) = Apply (Apply (Max_6989586621680882985Sym0 :: TyFun (Arg a1 b) (Arg a1 b ~> Arg a1 b) -> Type) a2) a3
type Max (arg1 :: (a, b, c)) (arg2 :: (a, b, c))
Instance details Defined in Data.Singletons.Prelude.Ord type Max (arg1 :: (a, b, c)) (arg2 :: (a, b, c)) = Apply (Apply (Max_6989586621679380204Sym0 :: TyFun (a, b, c) ((a, b, c) ~> (a, b, c)) -> Type) arg1) arg2
type Max (arg1 :: Const a b) (arg2 :: Const a b)
Instance details Defined in Data.Singletons.Prelude.Const type Max (arg1 :: Const a b) (arg2 :: Const a b) = Apply (Apply (Max_6989586621679380204Sym0 :: TyFun (Const a b) (Const a b ~> Const a b) -> Type) arg1) arg2
type Max (arg1 :: (a, b, c, d)) (arg2 :: (a, b, c, d))
Instance details Defined in Data.Singletons.Prelude.Ord type Max (arg1 :: (a, b, c, d)) (arg2 :: (a, b, c, d)) = Apply (Apply (Max_6989586621679380204Sym0 :: TyFun (a, b, c, d) ((a, b, c, d) ~> (a, b, c, d)) -> Type) arg1) arg2
type Max (arg1 :: (a, b, c, d, e)) (arg2 :: (a, b, c, d, e))
Instance details Defined in Data.Singletons.Prelude.Ord type Max (arg1 :: (a, b, c, d, e)) (arg2 :: (a, b, c, d, e)) = Apply (Apply (Max_6989586621679380204Sym0 :: TyFun (a, b, c, d, e) ((a, b, c, d, e) ~> (a, b, c, d, e)) -> Type) arg1) arg2
type Max (arg1 :: (a, b, c, d, e, f)) (arg2 :: (a, b, c, d, e, f))
Instance details Defined in Data.Singletons.Prelude.Ord type Max (arg1 :: (a, b, c, d, e, f)) (arg2 :: (a, b, c, d, e, f)) = Apply (Apply (Max_6989586621679380204Sym0 :: TyFun (a, b, c, d, e, f) ((a, b, c, d, e, f) ~> (a, b, c, d, e, f)) -> Type) arg1) arg2
type Max (arg1 :: (a, b, c, d, e, f, g)) (arg2 :: (a, b, c, d, e, f, g))
Instance details Defined in Data.Singletons.Prelude.Ord type Max (arg1 :: (a, b, c, d, e, f, g)) (arg2 :: (a, b, c, d, e, f, g)) = Apply (Apply (Max_6989586621679380204Sym0 :: TyFun (a, b, c, d, e, f, g) ((a, b, c, d, e, f, g) ~> (a, b, c, d, e, f, g)) -> Type) arg1) arg2

type family (a :: Nat) + (b :: Nat) :: Nat where ... infixl 6 #

Addition of type-level naturals.

Since: base-4.7.0.0

Constraint synonyms

type GenSKCtx c m z v = (ToInteger z, RoundedGaussianCyc (c m z), ToRational v, NFData v) Source #

Constraint synonym for generating a secret key.

type EncryptCtx c m m' z zp zq = (Ring zp, Cyclotomic (c m' zq), Ring (c m' zq), Random (c m' zq), Reduce (c m' z) (c m' zq), Reduce (LiftOf (c m' zp)) (c m' zq), CosetGaussianCyc (c m' zp), ExtensionCyc c zp, m `Divides` m') Source #

Constraint synonym for encryption.

type ToSDCtx c m' zp zq = (Encode zp zq, Cyclotomic (c m' zq), Ring (c m' zq), Module zq (c m' zq)) Source #

Constraint synonym for converting between ciphertext encodings.

type ErrorTermCtx c m' z zp zq = (ToSDCtx c m' zp zq, Ring (c m' zq), Reduce (c m' z) (c m' zq), LiftCyc (c m' zq)) Source #

Constraint synonym for extracting the error term of a ciphertext.

type DecryptCtx c m m' z zp zq = (ErrorTermCtx c m' z zp zq, Cyclotomic (c m' zp), Module zp (c m zp), Reduce (LiftOf (c m' zq)) (c m' zp), ExtensionCyc c zp, m `Divides` m') Source #

Constraint synonym for decryption.

type AddPublicCtx c m m' zp zq = (ToSDCtx c m' zp zq, Cyclotomic (c m zp), Module zp (c m zp), LiftCyc (c m zp), Reduce (LiftOf (c m zp)) (c m zq), ExtensionCyc c zq, m `Divides` m') Source #

Constraint synonym for adding a public value to an encrypted value.

type MulPublicCtx c m m' zp zq = (LiftCyc (c m zp), Reduce (LiftOf (c m zp)) (c m zq), ExtensionCyc c zq, m `Divides` m', Ring (c m' zq)) Source #

Constraint synonym for multiplying a public value with an encrypted value.

type ModSwitchCtx c m' zp zq zq' = (RescaleCyc (c m') zq zq', ToSDCtx c m' zp zq) Source #

type ModSwitchPTCtx c m' zp zp' zq = (Lift' zp, Reduce (LiftOf zp) zp', ToSDCtx c m' zp zq) Source #

Constraint synonym for modulus switching.

type KSHintCtx gad c m' z zq = (LWECtx c m' z zq, Gadget gad (c m' zq)) Source #

Constraint synonym for generating key-switch hints.

type KeySwitchCtx gad c m' zp zq' = (ToSDCtx c m' zp zq', SwitchCtx gad c m' zq') Source #

Constraint synonym for key switching.

type TunnelHintCtx c e r s e' r' s' z zp zq' gad = (ExtendLinCtx c e r s e' r' s' zp, e' ~ (e * (r' / r)), Fact r, z ~ LiftOf zp, KSHintCtx gad c s' z zq', LiftCyc (c s zp), LiftOf (c s zp) ~ c s z, ExtensionCyc c z, e' `Divides` r', Reduce (c s' z) (c s' zq'), Cyclotomic (c r' z), Ring (c r' z), Ring (c s' z), Random (c s' zq'), Gadget gad (c s' zq')) Source #

Constraint synonym for generating TunnelHint.

type TunnelCtx c r s e' r' s' zp zq' gad = (Fact r, Fact s, e' `Divides` r', e' `Divides` s', ExtensionCyc c zq', ToSDCtx c r' zp zq', AbsorbGCtx c r' zp zq', SwitchCtx gad c s' zq') Source #

Constraint synonym for ring tunneling.

type SwitchCtx gad c m' zq = (Cyclotomic (c m' zq), Ring (c m' zq), Decompose gad (c m' zq), Reduce (DecompOf (c m' zq)) (c m' zq)) Source #

Constraint synonym for applying a key-switch hint.

type LWECtx c m' z zq = (Cyclotomic (c m' zq), RoundedGaussianCyc (c m' z), Reduce (c m' z) (c m' zq), Random (c m' zq), Ring (c m' zq)) Source #

Constraint synonym for generating a ring-LWE sample.

Orphan instances

(Protoable rq, ProtoType rq ~ RqProduct) => Protoable (Polynomial rq) Source #
Instance details Associated Types type ProtoType (Polynomial rq) :: Type # Methods toProto :: Polynomial rq -> ProtoType (Polynomial rq) # fromProto :: MonadError String m => ProtoType (Polynomial rq) -> m (Polynomial rq) #