lol-apps 0.1.0.0 → 0.1.1.0

raw patch · 10 files changed

+121/−117 lines, 10 filesdep ~basedep ~lolsetup-changedPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependency ranges changed: base, lol

API changes (from Hackage documentation)

Files

• CHANGES.md +4/−0
• Crypto/Lol/Applications/SymmSHE.hs +57/−54
• Setup.hs +2/−0
• benchmarks/SHEBenches.hs +4/−4
• examples/SymmSHE/SimpleSHE.hs +28/−29
• lol-apps.cabal +7/−4
• tests/SHETests.hs +7/−13
• utils/Apply/SHE.hs +6/−7
• utils/GenArgs/SHE.hs +1/−2
• utils/Utils.hs +5/−4

@@ -1,6 +1,10 @@ Changelog for lol project ================================ +0.2.0.0+----+ * Updated documentation with MathJax+ 0.1.0.0 -----  * Updated for lol-0.3.*

@@ -3,12 +3,13 @@              NoImplicitPrelude, ScopedTypeVariables, TypeFamilies,              TypeOperators, UndecidableInstances #-} --- | Symmetric-key somewhat homomorphic encryption.+-- | Symmetric-key somewhat homomorphic encryption.  See Section 4 of+-- http://eprint.iacr.org/2015/1134 for mathematical description.  module Crypto.Lol.Applications.SymmSHE ( -- * Data types-SK, PT, CT                    -- don't export constructors!+SK, PT, CT -- don't export constructors! -- * Keygen, encryption, decryption , genSK , encrypt@@ -28,16 +29,14 @@ , AddScalarCtx, AddPublicCtx, MulPublicCtx, ModSwitchPTCtx , KeySwitchCtx, KSHintCtx , TunnelCtx+, SwitchCtx, LWECtx -- these are internal, but exported for better docs ) where  import qualified Algebra.Additive as Additive (C) import qualified Algebra.Ring     as Ring (C) -import Crypto.Lol.Cyclotomic.Cyc-import Crypto.Lol.Cyclotomic.Linear+import Crypto.Lol as LP hiding (sin) import Crypto.Lol.Cyclotomic.UCyc   (D, UCyc)-import Crypto.Lol.Gadget-import Crypto.Lol.Prelude           as LP hiding (sin)  import Control.Applicative  hiding ((*>)) import Control.DeepSeq@@ -58,7 +57,8 @@ -- | Ciphertext encoding type data Encoding = MSD | LSD deriving (Show, Eq) --- | Ciphertext over @R'_q@, encrypting a plaintext in @R_p (R=O_m)@.+-- | Ciphertext over \( R'_q \) encrypting a plaintext in \( R_p \)\,+-- where \( R=\mathcal{O}_m \). data CT (m :: Factored) zp r'q =   CT   !Encoding                     -- MSD/LSD encoding@@ -83,7 +83,7 @@   (ToInteger z, Fact m, CElt t z, ToRational v, NFData v)  -- | Generates a secret key with (index-independent) scaled variance--- parameter @v@; see 'errorRounded'.+-- parameter \( v \); see 'errorRounded'. genSK :: (GenSKCtx t m z v, MonadRandom rnd)          => v -> rnd (SK (Cyc t m z)) genSK v = liftM (SK v) $ errorRounded v@@ -96,8 +96,9 @@    m `Divides` m')  -- | Encrypt a plaintext under a secret key.-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 :: 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 = adviseCRT $ reduce s   in \pt -> do@@ -187,15 +188,14 @@  ---------- Modulus switching ---------- --- | Rescale a linear polynomial in MSD encoding, for best noise--- behavior.+-- | Rescale a linear polynomial in MSD encoding, for best noise behavior. rescaleLinearMSD :: (RescaleCyc (Cyc t) zq zq', Fact m')                     => Polynomial (Cyc t m' zq) -> Polynomial (Cyc t m' zq') rescaleLinearMSD c = case coeffs c of   [] -> fromCoeffs []-  [c0] -> fromCoeffs [rescaleCyc Dec c0]-  [c0,c1] -> let c0' = rescaleCyc Dec c0-                 c1' = rescaleCyc Pow c1+  [c0] -> fromCoeffs [rescaleDec c0]+  [c0,c1] -> let c0' = rescaleDec c0+                 c1' = rescalePow c1              in fromCoeffs [c0', c1']   _ -> error $ "rescaleLinearMSD: list too long (not linear): " ++        show (length $ coeffs c)@@ -211,8 +211,8 @@   (Lift' zp, Reduce (LiftOf zp) zp', ToSDCtx t m' zp zq)  -- | 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\'@.+-- of \( (p/p') \) by that factor, thereby scaling the plaintext modulus+-- from \( p \) to \( p' \). modSwitchPT :: (ModSwitchPTCtx t m' zp zp' zq)             => CT m zp (Cyc t m' zq) -> CT m zp' (Cyc t m' zq) modSwitchPT ct = let CT MSD k l c = toMSD ct in@@ -220,10 +220,11 @@  ---------- Key switching ---------- +-- | Constraint synonym for generating an LWE sample. type LWECtx t m' z zq =   (ToInteger z, Reduce z zq, Ring zq, Random zq, Fact m', CElt t z, CElt t zq) --- | An LWE sample for a given secret (corresponding to a linear+-- An LWE sample for a given secret (corresponding to a linear -- ciphertext encrypting 0 in MSD form) lweSample :: (LWECtx t m' z zq, MonadRandom rnd)              => SK (Cyc t m' z) -> rnd (Polynomial (Cyc t m' zq))@@ -264,6 +265,7 @@ -- adviseCRT here because we map (x *) onto each polynomial coeff knapsack hint xs = sum $ zipWith (*>>) (adviseCRT <$> xs) hint +-- | Constraint synonym for applying a key-switch hint. type SwitchCtx gad t m' zq =   (Decompose gad zq, Fact m', CElt t zq, CElt t (DecompOf zq)) @@ -277,7 +279,8 @@   (RescaleCyc (Cyc t) zq' zq, RescaleCyc (Cyc t) zq zq',    ToSDCtx t m' zp zq, SwitchCtx gad t m' zq') --- | Switch a linear ciphertext under @s_in@ to a linear one under @s_out@.+-- | Switch a linear ciphertext under \( s_{\text{in}} \) to a linear+-- one under \( s_{\text{out}} \). keySwitchLinear :: forall gad t m' zp zq zq' z rnd m .   (KeySwitchCtx gad t m' zp zq zq', KSHintCtx gad t m' z zq', MonadRandom rnd)   => SK (Cyc t m' z)                -- sout@@ -288,7 +291,7 @@   return $! hint `seq`     (\ct -> let CT MSD k l c = toMSD ct                 [c0,c1] = coeffs c-                c1' = rescaleCyc Pow c1+                c1' = rescalePow c1             in CT MSD k l $ P.const c0 + rescaleLinearMSD (switch hint c1'))  -- | Switch a quadratic ciphertext (i.e., one with three components)@@ -302,39 +305,37 @@   return $ hint `seq` (\ct ->     let CT MSD k l c = toMSD ct         [c0,c1,c2] = coeffs c-        c2' = rescaleCyc Pow c2+        c2' = rescalePow c2     in CT MSD k l $ P.fromCoeffs [c0,c1] + rescaleLinearMSD (switch hint c2'))  ---------- Misc homomorphic operations ---------- -- | Constraint synonym for adding a public scalar to a ciphertext. type AddScalarCtx t m' zp zq =-  (Lift' zp, Reduce (LiftOf zp) zq, ToSDCtx t m' zp zq)+  (Lift' zp, Reduce (LiftOf zp) zq,+   CElt t zp, CElt t (LiftOf zp), ToSDCtx t m' zp zq) --- | Homomorphically add a public @Z_p@ value to an encrypted value.  The--- ciphertext must not carry any @g@ factors.-addScalar :: (AddScalarCtx t m' zp zq)-             => zp -> CT m zp (Cyc t m' zq) -> CT m zp (Cyc t m' zq)+-- | Homomorphically add a public \(\mathbb{Z}_p\) value to an encrypted value.+addScalar :: forall t m m' zp zq . (AddScalarCtx t m' zp zq)+          => zp -> CT m zp (Cyc t m' zq) -> CT m zp (Cyc t m' zq) addScalar b ct =-  let (l,c) = case toLSD ct of-        CT LSD 0 l c -> (l,c)-        CT LSD _ _ _ -> error "cannot add public scalar to ciphertext with 'g' factors"-        _ -> error "internal error: addScalar"-      b' = scalarCyc (reduce $ lift $ b * recip l)-  in CT LSD 0 l $ c + P.const b'+  let CT LSD k l c = toLSD ct+      b' = iterate mulG (scalarCyc $ b * recip l) !! k :: Cyc t m' zp+  in CT LSD k l $ c + (P.const $ reduce $ liftPow b')  -- | Constraint synonym for adding a public value to an encrypted value. type AddPublicCtx t m m' zp zq =   (Lift' zp, Reduce (LiftOf zp) zq, m `Divides` m',    CElt t zp, CElt t (LiftOf zp), ToSDCtx t m' zp zq) --- | Homomorphically add a public @R_p@ value to an encrypted value.+-- | Homomorphically add a public \( R_p \) value to an encrypted+-- value. addPublic :: forall t m m' zp zq . (AddPublicCtx t m m' zp zq)           => Cyc t m zp -> CT m zp (Cyc t m' zq) -> CT m zp (Cyc t m' zq) addPublic b ct = let CT LSD k l c = toLSD ct in   let linv = scalarCyc $ recip l       -- multiply public value by appropriate power of g and divide by the       -- scale, to match the form of the ciphertext-      b' :: Cyc t m zq = reduce $ liftCyc Pow $ linv * (iterate mulG b !! k)+      b' :: Cyc t m zq = reduce $ liftPow $ linv * (iterate mulG b !! k)   in CT LSD k l $ c + P.const (embed b')  -- | Constraint synonym for multiplying a public value with an encrypted value.@@ -342,15 +343,16 @@   (Lift' zp, Reduce (LiftOf zp) zq, Ring zq, m `Divides` m',    CElt t zp, CElt t (LiftOf zp), CElt t zq) --- | Homomorphically multiply an encrypted value by a public @R_p@ value.+-- | Homomorphically multiply an encrypted value by a public \( R_p \)+-- value. mulPublic :: forall t m m' zp zq . (MulPublicCtx t m m' zp zq)              => Cyc t m zp -> CT m zp (Cyc t m' zq) -> CT m zp (Cyc t m' zq) mulPublic a (CT enc k l c) =-  let a' = embed (reduce $ liftCyc Pow a :: Cyc t m zq)+  let a' = embed (reduce $ liftPow a :: Cyc t m zq)   in CT enc k l $ (a' *) <$> c --- | Increment the internal g exponent without changing the encrypted--- message.+-- | Increment the internal \( g \) exponent without changing the+-- encrypted message. mulGCT :: (Fact m', CElt t zq)           => CT m zp (Cyc t m' zq) -> CT m zp (Cyc t m' zq) mulGCT (CT enc k l c) = CT enc (k+1) l $ mulG <$> c@@ -397,22 +399,22 @@   (Lift' zp, IntegralDomain zp, Reduce (LiftOf zp) zq, Ring zq,    Fact m', CElt t (LiftOf zp), CElt t zp, CElt t zq) --- | "Absorb" the powers of g associated with the ciphertext, at the--- cost of some increase in noise. This is usually needed before+-- | "Absorb" the powers of \( g \) associated with the ciphertext, at+-- the cost of some increase in noise. This is usually needed before -- changing the index of the ciphertext ring. absorbGFactors :: forall t zp zq m m' . (AbsorbGCtx t m' zp zq)                   => CT m zp (Cyc t m' zq) -> CT m zp (Cyc t m' zq) absorbGFactors ct@(CT enc k l c)   | k == 0 = ct   | k > 0 = let d :: Cyc t m' zp = iterate divG' one !! k-                rep = adviseCRT $ reduce $ liftCyc Pow d+                rep = adviseCRT $ reduce $ liftPow d             in CT enc 0 l $ (rep *) <$> c   | otherwise = error "k < 0 in absorbGFactors" --- | 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.+-- | 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 \). embedCT :: (CElt t zq,             r `Divides` r', s `Divides` s', r `Divides` s, r' `Divides` s')            => CT r zp (Cyc t r' zq) -> CT s zp (Cyc t s' zq)@@ -426,13 +428,14 @@ embedCT _ = error "embedCT requires 0 factors of g; call aborbGFactors first"  -- | Embed a secret key from a subring into a superring.-embedSK :: (CElt t z, m `Divides` m') => SK (Cyc t m z) -> SK (Cyc t m' z)+embedSK :: (m `Divides` m') => SK (Cyc t m z) -> SK (Cyc t m' z) embedSK (SK v s) = SK v $ embed s  -- | "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)@.+-- 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)+-- \). twaceCT :: (CElt t zq, r `Divides` r', s' `Divides` r',             s ~ (FGCD s' r))            => CT r zp (Cyc t r' zq) -> CT s zp (Cyc t s' zq)@@ -453,9 +456,9 @@    CElt t zp,                       -- liftLin    SwitchCtx gad t s' zq)           -- switch --- | 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.+-- | 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. tunnelCT :: forall gad t e r s e' r' s' z zp zq rnd .   (TunnelCtx t e r s e' r' s' z zp zq gad,    MonadRandom rnd)@@ -467,7 +470,7 @@   -- 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+      -- choice of basis here must match coeffs* basis below       ps = proxy powBasis (Proxy::Proxy e')       comps = (evalLin f' . (adviseCRT sin *)) <$> ps   hints :: [Tagged gad [Polynomial (Cyc t s' zq)]] <- CM.mapM (ksHint skout) comps@@ -478,7 +481,7 @@         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]+        c1s = coeffsPow c1 :: [Cyc t e' zq]         -- CJP: don't embed the c1s before decomposing them (inside         -- switch); instead decompose in smaller ring before         -- embedding (it matters).

@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain

@@ -16,10 +16,10 @@ import Control.Monad.State import Crypto.Random.DRBG -import Crypto.Lol hiding (CT)+import Crypto.Lol import Crypto.Lol.Applications.SymmSHE-import qualified Crypto.Lol.Cyclotomic.Tensor.CTensor as CT-import Crypto.Lol.Types.Random+import Crypto.Lol.Types hiding (CT)+import qualified Crypto.Lol.Types as CT  import qualified Criterion as C @@ -60,7 +60,7 @@ bench_mulPublic a ct = bench (mulPublic a) ct  -- requires zq to be Liftable-bench_dec :: (DecryptCtx t m m' z zp zq, z ~ LiftOf zp, NFElt zp)+bench_dec :: (DecryptCtx t m m' z zp zq, NFElt zp)   => SK (Cyc t m' z) -> CT m zp (Cyc t m' zq) -> Bench '(t,m,m',zp,zq) bench_dec sk ct = bench (decrypt sk) ct 

@@ -1,48 +1,47 @@-{-# LANGUAGE-     DataKinds,         -- so we can use GHC.TypeLits-     NoImplicitPrelude, -- an alternate Prelude is imported from Crypto.Lol-     PolyKinds,-     RebindableSyntax,  -- since we use an alternate Prelude, this lets GHC read literals, etc-     ScopedTypeVariables,-     TemplateHaskell    -- provides a simple way to construct cyclotomic indices and prime-power moduli-     #-}+{-# LANGUAGE DataKinds           #-}+{-# LANGUAGE NoImplicitPrelude   #-}+{-# LANGUAGE PolyKinds           #-}+{-# LANGUAGE RebindableSyntax    #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskell     #-} -import Crypto.Lol hiding ((^),CT)-import qualified Crypto.Lol as Lol-import Crypto.Lol.Applications.SymmSHE-import Algebra.Ring ((^)) -- easier to use with the TH commands below-import Math.NumberTheory.Primes.Testing (isPrime) -- used to generate "good" moduli-import Control.Monad.Random (getRandom)+import           Crypto.Lol hiding ((^))+import           Crypto.Lol.Applications.SymmSHE -- exports *ciphertext* 'CT'+import           Crypto.Lol.Types hiding (CT)+import qualified Crypto.Lol.Types as C -- the *tensor* 'CT' --- an infinite list of primes greater than `lower` and congruent to 1 mod m--- useful for generating moduli for CTZq below-goodQs :: (IntegralDomain i, ToInteger i) => i -> i -> [i]-goodQs m lower = checkVal (lower + ((m-lower) `mod` m) + 1)-  where checkVal v = if (isPrime (fromIntegral v :: Integer))-                     then v : checkVal (v+m)-                    else checkVal (v+m)+import Algebra.Ring ((^)) +import Control.Monad.Random (getRandom)+ -- PTIndex must divide CTIndex type PTIndex = F128+ -- Crypto.Lol includes Factored types F1..F512 -- for cyclotomic indices outside this range, -- we provide a TH wrapper. -- TH to constuct the cyclotomic index 11648 type CTIndex = $(fType $ 2^7 * 7 * 13)--- to use crtSet (for example, when ring switching), the plaintext modulus must be a PrimePower (ZPP constraint)--- Crypto.Lol exports PP2,PP4,...,PP128 as well as some prime powers for 3,5,7, and 11.--- See Crypto.Lol.Factored. Alternately, an arbitrary prime power p^e can be constructed with--- the TH $(ppType (p,e))--- for applications that don't use crtSet, PT modulus can be a TypeLit.++-- To use crtSet (for example, when ring switching), the plaintext+-- modulus must be a PrimePower (ZPP constraint).  Crypto.Lol exports+-- (via Crypto.Lol.Factored) PP2,PP4,...,PP128, as well as some prime+-- powers for 3,5,7, and 11.  Alternately, an arbitrary prime power+-- p^e can be constructed with the Template Haskell splice $(ppType+-- (p,e)).  For applications that don't use crtSet, the PT modulus can+-- be a TypeLit. type PTZq = ZqBasic PP8 Int64--- uses GHC.TypeLits as modulus, and Int64 as repr (needed to use with CT backend)--- modulus doesn't have to be "good", but "good" moduli are much faster++-- uses GHC.TypeLits as modulus, and Int64 as underyling+-- representation (needed to use with CT backend).  The modulus+-- doesn't have to be "good", but "good" moduli are faster. type Zq q = ZqBasic q Int64 -- uses PolyKinds type CTZq1 = Zq 536937857 type CTZq2 = (CTZq1, Zq 536972801) type CTZq3 = (CTZq2, Zq 537054337)+ -- Tensor backend, either Repa (RT) or C (CT)-type T = Lol.CT -- can also use RT+type T = C.CT -- can also use RT  type KSGad = TrivGad -- can also use (BaseBGad 2), for example 

@@ -5,7 +5,7 @@ -- PVP summary:      +-+------- breaking API changes --                   | | +----- non-breaking API additions --                   | | | +--- code changes with no API change-version:             0.1.0.0+version:             0.1.1.0 synopsis:            Lattice-based cryptographic applications using Lol. homepage:            https://github.com/cpeikert/Lol Bug-Reports:         https://github.com/cpeikert/Lol/issues@@ -64,9 +64,9 @@     Crypto.Lol.Applications.SymmSHE    build-depends:-    base==4.8.*,+    base>=4.8 && <5,     deepseq >= 1.4.1.1 && <1.5,-    lol == 0.3.*,+    lol >= 0.3 && < 0.5,     MonadRandom >= 0.2 && < 0.5,     numeric-prelude >= 0.4.2 && < 0.5 @@ -79,6 +79,7 @@   ghc-options: -threaded -rtsopts    build-depends:+    arithmoi,     base,     constraints,     deepseq,@@ -108,6 +109,7 @@ --  ghc-options: -fno-liberate-case -funfolding-use-threshold1000 -funfolding-keeness-factor1000    build-depends:+    arithmoi,     base,     criterion,     deepseq,@@ -122,7 +124,7 @@     repa  executable simpleSHE-  hs-source-dirs:   examples/SymmSHE+  hs-source-dirs:   examples/SymmSHE, utils   default-language: Haskell2010   main-is:          SimpleSHE.hs @@ -130,6 +132,7 @@    build-depends:     arithmoi,+    base,     lol,     lol-apps,     MonadRandom,

@@ -15,10 +15,10 @@ import Control.Monad.Random import Control.Monad.State -import Crypto.Lol hiding (CT)+import Crypto.Lol import Crypto.Lol.Applications.SymmSHE-import Crypto.Lol.Cyclotomic.Linear import qualified Crypto.Lol.Cyclotomic.Tensor.CTensor as CT+import qualified Crypto.Lol.Cyclotomic.Tensor.RepaTensor as RT  import qualified Test.Framework as TF import Test.Framework.Providers.QuickCheck2@@ -75,7 +75,7 @@   ]  type Gadgets = '[TrivGad, BaseBGad 2]-type Tensors = '[CT.CT,RT]+type Tensors = '[CT.CT,RT.RT] type MM'PQCombos =   '[ '(F1, F7, Zq 2, Zq (19393921 ** 18869761)),      '(F2, F4, Zq 8, Zq (2148854401 ** 2148249601)),@@ -207,8 +207,6 @@ prop_ctembed :: forall t r r' s s' z zp zq .   (DecryptUCtx t r r' z zp zq,    DecryptUCtx t s s' z zp zq,-   r `Divides` r',-   s `Divides` s',    r `Divides` s,    r' `Divides` s',    Eq (Cyc t s zp))@@ -225,7 +223,6 @@    DecryptUCtx t r r' z zp zq,    r `Divides` s,    r' `Divides` s',-   s `Divides` s',    r ~ (FGCD r' s))   => SK (Cyc t r' z) -> Cyc t s zp -> Test '(t,r,r',s,s',zp,zq) prop_cttwace sk x = testIO $ do@@ -235,8 +232,7 @@   return $ (twace x :: Cyc t r zp) == x'  prop_encDecU :: forall t m m' z zp zq .-  (GenSKCtx t m' z Double,-   EncryptCtx t m m' z zp zq,+  (EncryptCtx t m m' z zp zq,    DecryptUCtx t m m' z zp zq,    Eq (Cyc t m zp))   => SK (Cyc t m' z) -> Cyc t m zp -> Test '(t,m,m',zp,zq)@@ -246,8 +242,7 @@   return $ x == x'  prop_encDec :: forall t m m' z zp zq .-  (GenSKCtx t m' z Double,-   EncryptCtx t m m' z zp zq,+  (EncryptCtx t m m' z zp zq,    DecryptCtx t m m' z zp zq,    Eq (Cyc t m zp))   => SK (Cyc t m' z) -> Cyc t m zp -> Test '(t,m,m',zp,zq)@@ -266,7 +261,6 @@    DecryptUCtx t m m' z zp' zq,    ModSwitchPTCtx t m' zp zp' zq,    RescaleCyc (Cyc t) zp zp',-   Ring (Cyc t m zp),    Mod zp, Mod zp',    ModRep zp ~ ModRep zp')   => SK (Cyc t m' z) -> CT m zp (Cyc t m' zq) -> Test '(t, '(m,m',zp',zp,zq))@@ -280,13 +274,13 @@   in test $ x'' == rescaleCyc Dec x  modSwPTTests :: [IO TF.Test]-modSwPTTests = (modSwPTTests' (Proxy::Proxy CT.CT)) ++ (modSwPTTests' (Proxy::Proxy RT))+modSwPTTests = (modSwPTTests' (Proxy::Proxy CT.CT)) ++ (modSwPTTests' (Proxy::Proxy RT.RT))  where modSwPTTests' p =         [helper (hideArgs prop_modSwPT) p (Proxy::Proxy '(F7,F21,Zq 4,Zq 8,Zq 18869761)),          helper (hideArgs prop_modSwPT) p (Proxy::Proxy '(F7,F42,Zq 2,Zq 4,Zq (18869761 ** 19393921)))]  tunnelTests :: [IO TF.Test]-tunnelTests = (tunnelTests' (Proxy::Proxy CT.CT)) ++ (tunnelTests' (Proxy::Proxy RT))+tunnelTests = (tunnelTests' (Proxy::Proxy CT.CT)) ++ (tunnelTests' (Proxy::Proxy RT.RT))   where tunnelTests' p =          [helper (hideArgs prop_ringTunnel) p           (Proxy::Proxy '(F8,F40,F20,F60,Zq 4,Zq (18869761 ** 19393921),TrivGad))]

@@ -35,7 +35,7 @@ import Control.Monad.Random import Control.Monad.State -import Crypto.Lol                      hiding (CT)+import Crypto.Lol import Crypto.Lol.Applications.SymmSHE import Crypto.Lol.Types.ZPP @@ -124,7 +124,7 @@   => ( '(t, '(r,r',s,s',zp,zq)) ': params) `Satisfy` CTEmCtxD where   run _ f = f (TwEmD (Proxy::Proxy '(t,r,r',s,s',zp,zq))) : run (Proxy::Proxy params) f -applyCTTwEm :: (params `Satisfy` CTEmCtxD, MonadRandom rnd) =>+applyCTTwEm :: (params `Satisfy` CTEmCtxD) =>   Proxy params ->   (forall t r r' s s' zp zq . (CTEmCtx t r r' s s' zp zq)        => Proxy '(t,r,r',s,s',zp,zq) -> rnd res)@@ -136,8 +136,7 @@ data KSQCtxD -- it'd be nice to make this associated to `Satsify`, -- but we have to use a *ton* of kind signatures if we do-type family KSQCtx a where-  KSQCtx '(gad, '(t, '(m,m',zp,zq,zq'))) =+type KSQCtx gad t m m' zp zq zq' =     (Random zp, Eq zp,          -- CJP: added b/c CElt doesn't have them      EncryptCtx t m m' (LiftOf zp) zp zq,      DecryptUCtx t m m' (LiftOf zp) zp zq,@@ -153,15 +152,15 @@      ShowType '(t,m,m',zp,zq,zq',gad))      -- ^ these provide the context for benchmarks data instance ArgsCtx KSQCtxD where-    KSQD :: (KSQCtx '(gad, '(t, '(m,m',zp,zq,zq'))))+    KSQD :: (KSQCtx gad t m m' zp zq zq')       => Proxy '(t,m,m',zp,zq,zq',gad) -> ArgsCtx KSQCtxD-instance (params `Satisfy` KSQCtxD, KSQCtx '(gad, '(t, '(m,m',zp,zq,zq'))))+instance (params `Satisfy` KSQCtxD, KSQCtx gad t m m' zp zq zq')   => ( '(gad , '(t, '(m, m', zp, zq, zq'))) ': params) `Satisfy` KSQCtxD where   run _ f = f (KSQD (Proxy::Proxy '(t,m,m',zp,zq,zq',gad))) : run (Proxy::Proxy params) f  applyKSQ :: (params `Satisfy` KSQCtxD) =>   Proxy params ->-  (forall t m m' zp zq zq' gad . (KSQCtx '(gad, '(t, '(m,m',zp,zq,zq'))))+  (forall t m m' zp zq zq' gad . (KSQCtx gad t m m' zp zq zq')      => Proxy '(t,m,m',zp,zq,zq',gad) -> rnd res)   -> [rnd res] applyKSQ params g = run params $ \(KSQD p) -> g p

@@ -11,9 +11,8 @@ import Control.Monad.Random import Control.Monad.State -import Crypto.Lol hiding (CT)+import Crypto.Lol import Crypto.Lol.Applications.SymmSHE-import Crypto.Lol.Cyclotomic.Linear import Crypto.Lol.Types.ZPP  --extract an SK type from a tuple of params

@@ -10,17 +10,19 @@ ,type (<*>)  ,module Data.Promotion.Prelude.List-+,goodQs ,showType ,ShowType) where -import Crypto.Lol (Int64,Fact,valueFact,Mod(..), Proxy(..), proxy, RT, CT, TrivGad, BaseBGad)+import Crypto.Lol (Int64,Fact,valueFact,Mod(..), Proxy(..), proxy, TrivGad, BaseBGad) import Crypto.Lol.Reflects+import Crypto.Lol.Cyclotomic.Tensor.RepaTensor+import Crypto.Lol.Cyclotomic.Tensor.CTensor import Crypto.Lol.Types.ZqBasic import Crypto.Random.DRBG  import Data.Promotion.Prelude.List-{-+ import Math.NumberTheory.Primes.Testing (isPrime)  -- an infinite list of primes greater than the input and congruent to@@ -30,7 +32,6 @@   where checkVal v = if (isPrime (fromIntegral v :: Integer))                      then v : checkVal (v+m)                     else checkVal (v+m)--}  infixr 9 ** data a ** b