diff --git a/CHANGES.md b/CHANGES.md
new file mode 100644
--- /dev/null
+++ b/CHANGES.md
@@ -0,0 +1,6 @@
+Changelog for lol project
+================================
+
+0.0.0.1
+-----
+ * Initial split from lol.
diff --git a/Crypto/Lol/Applications/SymmSHE.hs b/Crypto/Lol/Applications/SymmSHE.hs
new file mode 100644
--- /dev/null
+++ b/Crypto/Lol/Applications/SymmSHE.hs
@@ -0,0 +1,489 @@
+{-# LANGUAGE ConstraintKinds, DataKinds,
+             FlexibleContexts, FlexibleInstances, GADTs,
+             MultiParamTypeClasses, NoImplicitPrelude, ScopedTypeVariables,
+             TypeFamilies, TypeOperators, UndecidableInstances #-}
+
+-- | Symmetric-key somewhat homomorphic encryption.
+
+module Crypto.Lol.Applications.SymmSHE
+(
+-- * Data types
+SK, PT, CT                    -- don't export constructors!
+-- * Keygen, encryption, decryption
+, genSK
+, encrypt
+, errorTerm, errorTermUnrestricted, decrypt, decryptUnrestricted
+-- * Arithmetic with public values
+, addScalar, addPublic, mulPublic
+-- * Modulus switching
+, rescaleLinearCT, modSwitchPT
+-- * Key switching
+, keySwitchLinear, keySwitchQuadCirc
+-- * Ring switching
+, embedSK, embedCT, twaceCT
+, tunnelCT
+-- * Constraint synonyms
+, GenSKCtx, EncryptCtx, ToSDCtx, ErrorTermCtx
+, DecryptCtx, DecryptUCtx
+, AddScalarCtx, AddPublicCtx, MulPublicCtx, ModSwitchPTCtx
+, SwitchCtx, KeySwitchCtx, KSHintCtx
+, TunnelCtx
+) where
+
+import qualified Algebra.Additive as Additive (C)
+import qualified Algebra.Ring     as Ring (C)
+
+import Crypto.Lol.Cyclotomic.Cyc
+import Crypto.Lol.Cyclotomic.UCyc (UCyc, D)
+import Crypto.Lol.Cyclotomic.Linear
+import Crypto.Lol.Gadget
+import Crypto.Lol.LatticePrelude    as LP hiding (sin)
+
+import Control.Applicative  hiding ((*>))
+import Control.DeepSeq
+import Control.Monad        as CM
+import Control.Monad.Random
+import Data.Maybe
+import Data.Traversable     as DT
+
+import MathObj.Polynomial as P
+
+-- | secret key
+data SK r where
+  SK  :: (ToRational v, NFData v) => v -> r -> SK r
+
+-- | plaintext
+type PT rp = rp
+
+-- | Ciphertext encoding type
+data Encoding = MSD | LSD deriving (Show, Eq)
+
+-- | Ciphertext over @R'_q@, encrypting a plaintext in @R_p (R=O_m)@.
+data CT (m :: Factored) zp r'q =
+  CT
+  !Encoding                     -- MSD/LSD encoding
+  !Int                          -- accumulated power of g_m' in c(s)
+  !zp                           -- factor to mul by upon decryption
+  !(Polynomial r'q)             -- the polynomial c(s)
+  deriving (Show)
+
+-- Note: do *not* give an Eq instance for CT, because it's not
+-- meaningful to compare ciphertexts for equality
+
+instance (NFData zp, NFData r'q) => NFData (CT m zp r'q) where
+  rnf (CT _ k sc cs) = rnf k `seq` rnf sc `seq` rnf cs
+
+instance (NFData r) => NFData (SK r) where
+  rnf (SK v s) = rnf v `seq` rnf s
+
+---------- Basic functions: Gen, Enc, Dec ----------
+
+-- | Constraint synonym for generating a secret key.
+type GenSKCtx t m z v =
+  (ToInteger z, Fact m, CElt t z, ToRational v, NFData v)
+
+-- | Generates a secret key with (index-independent) scaled variance
+-- 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
+
+-- | Constraint synonym for encryption.
+type EncryptCtx t m m' z zp zq =
+  (Mod zp, Ring zp, Ring zq, Lift zp (ModRep zp), Random zq,
+   Reduce z zq, Reduce (LiftOf zp) zq,
+   CElt t zq, CElt t zp, CElt t z, CElt t (LiftOf zp),
+   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 (SK svar s) =
+  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 =
+  (Reduce z zq, Lift' zq, CElt t z, CElt t (LiftOf zq), ToSDCtx t m' zp zq)
+
+-- | Extract the error term of a ciphertext.
+errorTerm :: (ErrorTermCtx t m' z zp zq)
+             => SK (Cyc t m' z) -> CT m zp (Cyc t m' zq) -> Cyc t m' (LiftOf zq)
+errorTerm (SK _ s) = let sq = reduce s in
+  \ct -> let (CT LSD _ _ c) = toLSD ct
+         in liftCyc Dec $ evaluate c sq
+
+-- for when we know the division must succeed
+divG' :: (Fact m, CElt t r) => Cyc t m r -> Cyc t m r
+divG' = fromJust . divG
+
+-- | Constraint synonym for decryption.
+type DecryptCtx t m m' z zp zq =
+  (ErrorTermCtx t m' z zp zq, Reduce (LiftOf zq) zp,
+   m `Divides` m', CElt t zp)
+
+-- | Decrypt a ciphertext.
+decrypt :: forall t m m' z zp zq . (DecryptCtx t m m' z zp zq)
+           => SK (Cyc t m' z) -> CT m zp (Cyc t m' zq) -> PT (Cyc t m zp)
+decrypt sk ct =
+  let ct'@(CT LSD k l _) = toLSD ct
+  in let e :: Cyc t m' zp = reduce $ errorTerm sk ct'
+     in (scalarCyc l) * twace (iterate divG' e !! k)
+
+--- unrestricted versions ---
+
+type DecryptUCtx t m m' z zp zq =
+  (Fact m, Fact m', CElt t zp, m `Divides` m',
+   Reduce z zq, Lift' zq, CElt t z, 
+   ToSDCtx t m' zp zq, Reduce (LiftOf zq) zp)
+
+-- | More general form of 'errorTerm' that works for unrestricted
+-- output coefficient types.
+errorTermUnrestricted :: 
+  (Reduce z zq, Lift' zq, CElt t z, ToSDCtx t m' zp zq)
+  => SK (Cyc t m' z) -> CT m zp (Cyc t m' zq) -> UCyc t m' D (LiftOf zq)
+errorTermUnrestricted (SK _ s) = let sq = reduce s in
+  \ct -> let (CT LSD _ _ c) = toLSD ct
+             eval = evaluate c sq
+         in fmap lift $ uncycDec eval
+
+-- | More general form of 'decrypt' that works for unrestricted output
+-- coefficient types.
+decryptUnrestricted :: (DecryptUCtx t m m' z zp zq)
+  => SK (Cyc t m' z) -> CT m zp (Cyc t m' zq) -> PT (Cyc t m zp)
+decryptUnrestricted (SK _ s) = let sq = reduce s in
+  \ct -> let (CT LSD k l c) = toLSD ct
+         in let eval = evaluate c sq
+                e = cycDec $ fmap (reduce . lift) $ uncycDec eval
+                l' = scalarCyc l
+            in l' * twace (iterate divG' e !! k)
+
+---------- LSD/MSD switching ----------
+
+-- | Constraint synonym for converting between ciphertext encodings.
+type ToSDCtx t m' zp zq = (Encode zp zq, Fact m', CElt t zq)
+
+toLSD, toMSD :: ToSDCtx t m' zp zq
+ => CT m zp (Cyc t m' zq) -> CT m zp (Cyc t m' zq)
+
+-- CJP: reduce duplication in these functions?  They differ in only two places
+
+-- | Convert a ciphertext to MSD encoding.
+toMSD = let (zpScale, zqScale) = lsdToMSD
+            rqScale = scalarCyc zqScale
+        in \ct@(CT enc k l c) -> case enc of
+          MSD -> ct
+          LSD -> CT MSD k (zpScale * l) ((rqScale *) <$> c)
+
+-- | Convert a ciphertext to LSD encoding.
+toLSD = let (zpScale, zqScale) = msdToLSD
+            rqScale = scalarCyc zqScale
+        in \ct@(CT enc k l c) -> case enc of
+          LSD -> ct
+          MSD -> CT LSD k (zpScale * l) ((rqScale *) <$> c)
+
+---------- Modulus switching ----------
+
+-- | 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
+             in fromCoeffs [c0', c1']
+  _ -> error $ "rescaleLinearMSD: list too long (not linear): " ++
+       show (length $ coeffs c)
+
+-- | Rescale a linear ciphertext to a new modulus.
+rescaleLinearCT :: (RescaleCyc (Cyc t) zq zq', ToSDCtx t m' zp zq)
+           => CT m zp (Cyc t m' zq) -> CT m zp (Cyc t m' zq')
+rescaleLinearCT ct = let CT MSD k l c = toMSD ct
+                     in CT MSD k l $ rescaleLinearMSD c
+
+-- | Constraint synonym for modulus switching.
+type ModSwitchPTCtx t m' zp zp' zq =
+  (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\'@.
+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
+    CT MSD k (reduce (lift l)) c
+
+---------- Key switching ----------
+
+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
+-- 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))
+lweSample (SK svar 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 <- adviseCRT <$> getRandom -- want entire hint to be in CRT form
+    return $ fromCoeffs [c1 * sq + reduce (e `asTypeOf` s), c1]
+
+-- | Constraint synonym for generating key-switch hints.
+type KSHintCtx gad t m' z zq = 
+  (LWECtx t m' z zq, Reduce (DecompOf zq) zq, Gadget gad zq,
+   NFElt zq, CElt t (DecompOf zq))
+
+-- | Generate a hint that "encrypts" a value under a secret key, in
+-- the sense required for key-switching.  The hint works for any
+-- plaintext modulus, but must be applied on a ciphertext in MSD form.
+-- The output is 'force'd, i.e., evaluating it to whnf will actually
+-- cause it to be be evaluated to nf.
+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
+  let valq = reduce val
+      valgad = encode valq
+  -- CJP: clunky, but that's what we get without a MonadTagged
+  samples <- DT.mapM (\as -> replicateM (length as) (lweSample skout)) valgad
+  return $! force $ zipWith (+) <$> (map P.const <$> valgad) <*> samples
+
+-- poor man's module multiplication for knapsack
+(*>>) :: (Ring r, Functor f) => r -> f r -> f r
+(*>>) r = fmap (r *)
+
+knapsack :: (Fact m', CElt t zq, r'q ~ Cyc t m' zq)
+            => [Polynomial r'q] -> [r'q] -> Polynomial r'q
+-- adviseCRT here because we map (x *) onto each polynomial coeff
+knapsack hint xs = sum $ zipWith (*>>) (adviseCRT <$> xs) hint
+
+type SwitchCtx gad t m' zq = 
+  (Decompose gad zq, Fact m', CElt t zq, CElt t (DecompOf zq))
+
+-- Helper function: applies key-switch hint to a ring element.
+switch :: (SwitchCtx gad t m' zq, r'q ~ Cyc t m' zq)
+          => Tagged gad [Polynomial r'q] -> r'q -> Polynomial r'q
+switch hint c = untag $ knapsack <$> hint <*> (fmap reduce <$> decompose c)
+
+-- | Constraint synonym for key switching.
+type KeySwitchCtx gad t m' zp zq zq' =
+  (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@
+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
+  -> SK (Cyc t m' z)                -- sin
+  -> TaggedT (gad, zq') rnd (CT m zp (Cyc t m' zq) -> CT m zp (Cyc t m' zq))
+keySwitchLinear skout (SK _ sin) = tagT $ do
+  hint :: Tagged gad [Polynomial (Cyc t m' zq')] <- ksHint skout sin
+  return $! hint `seq`
+    (\ct -> let CT MSD k l c = toMSD ct
+                [c0,c1] = coeffs c
+                c1' = rescaleCyc Pow c1
+            in CT MSD k l $ P.const c0 + rescaleLinearMSD (switch hint c1'))
+
+-- | Switch a quadratic ciphertext (i.e., one with three components)
+-- to a linear one under the /same/ key.
+keySwitchQuadCirc :: forall gad t m' zp zq zq' z m rnd .
+  (KeySwitchCtx gad t m' zp zq zq', KSHintCtx gad t m' z zq', MonadRandom rnd)
+  => SK (Cyc t m' z)
+  -> TaggedT (gad, zq') rnd (CT m zp (Cyc t m' zq) -> CT m zp (Cyc t m' zq))
+keySwitchQuadCirc sk@(SK _ s) = tagT $ do
+  hint :: Tagged gad [Polynomial (Cyc t m' zq')] <- ksHint sk (s*s)
+  return $ hint `seq` (\ct ->
+    let CT MSD k l c = toMSD ct
+        [c0,c1,c2] = coeffs c
+        c2' = rescaleCyc Pow c2
+    in CT MSD k l $ P.fromCoeffs [c0,c1] + rescaleLinearMSD (switch hint c2'))
+
+---------- Misc homomorphic operations ----------
+
+type AddScalarCtx t m' zp zq =
+  (Lift' zp, Reduce (LiftOf zp) zq, 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)
+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'
+
+-- | 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.
+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)
+  in CT LSD k l $ c + P.const (embed b')
+
+-- | Constraint synonym for multiplying a public value with an encrypted value
+type MulPublicCtx t m m' zp zq =
+  (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.
+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)
+  in CT enc k l $ (a' *) <$> c
+
+-- | 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
+
+---------- NumericPrelude instances ----------
+
+instance (Eq zp, m `Divides` m', ToSDCtx t m' zp zq)
+         => Additive.C (CT m zp (Cyc t m' zq)) where
+
+  zero = CT LSD 0 one zero
+
+  -- the scales, g-exponents of ciphertexts, and MSD/LSD types must match.
+  ct1@(CT enc1 k1 l1 c1) + ct2@(CT enc2 k2 l2 c2)
+      -- for simplicity, we don't currently support this. Shouldn't be
+      -- too complicated though.
+      | l1 /= l2 = error "Cannot add ciphertexts with different scale values"
+      | k1 < k2 = iterate mulGCT ct1 !! (k2-k1) + ct2
+      | k1 > k2 = ct1 + iterate mulGCT ct2 !! (k1-k2)
+      | enc1 == LSD && enc2 == MSD = toMSD ct1 + ct2
+      | enc1 == MSD && enc2 == LSD = ct1 + toMSD ct2
+      | otherwise = CT enc1 k1 l1 $ c1 + c2
+
+  negate (CT enc k l c) = CT enc k l $ negate <$> c
+
+instance (ToSDCtx t m' zp zq, Additive (CT m zp (Cyc t m' zq)))
+  => Ring.C (CT m zp (Cyc t m' zq)) where
+
+  one = CT LSD 0 one one
+
+  -- need at least one ct to be in LSD form
+  ct1@(CT MSD _ _ _) * ct2@(CT MSD _ _ _) = toLSD ct1 * ct2
+
+  -- first is in LSD
+  (CT LSD k1 l1 c1) * (CT d2 k2 l2 c2) =
+    -- mul by g so error maintains invariant: error*g is "round"
+    CT d2 (k1+k2+1) (l1*l2) (mulG <$> c1 * c2)
+
+  -- else, second must be in LSD
+  ct1 * ct2 = ct2 * ct1
+
+---------- Ring switching ----------
+
+type AbsorbGCtx t m' zp zq =
+  (Lift' zp, Reduce (LiftOf zp) zq, Ring zp, 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
+-- 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
+            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.
+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)
+-- We could call absorbGFactors first, insead of error.  Embedding
+-- *essentially* maintains the invariant that noise*g is "round."
+-- While g'/g can be non-spherical, it only stretches by at most a
+-- factor of 2 per new odd prime.  We *cannot* multiply by g, then
+-- embed, then divide by g' because the result would not remain in R'.
+-- So this is the best we can do.
+embedCT (CT d 0 l c) = CT d 0 l (embed <$> c)
+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 (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)@.
+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)
+-- we could call absorbGFactors first, insead of error
+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 gad =
+  (ExtendLinIdx e r s e' r' s',     -- liftLin
+   e' ~ (e * (r' / r)),             -- convenience; implied by prev constraint
+   ToSDCtx t r' zp zq,              -- toMSD
+   KSHintCtx gad t r' z zq,         -- ksHint
+   Reduce z zq,                     -- Reduce on Linear
+   Lift zp z,                       -- liftLin
+   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.
+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)
+  => Linear t zp e r s
+  -> SK (Cyc t s' z)
+  -> SK (Cyc t r' z)
+  -> TaggedT gad rnd (CT r zp (Cyc t r' zq) -> CT s zp (Cyc t s' zq))
+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
+  hints :: [Tagged gad [Polynomial (Cyc t s' zq)]] <- CM.mapM (ksHint skout) comps
+  return $ hints `deepseq` \ct ->
+    let CT MSD 0 s c = toMSD $ absorbGFactors ct
+        [c0,c1] = coeffs c
+        -- apply E-linear function to constant term 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]
+        -- CJP: don't embed the c1s before decomposing them (inside
+        -- switch); instead decompose in smaller ring before
+        -- embedding (it matters).
+        -- We may need to generalize switch or define an
+        -- alternative.
+        c1s' = zipWith switch hints (embed <$> c1s)
+        c1' = sum c1s'
+    in CT MSD 0 s $ P.const c0' + c1')
+      \\ lcmDivides (Proxy::Proxy r) (Proxy::Proxy e')
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,339 @@
+             GNU GENERAL PUBLIC LICENSE
+                Version 2, June 1991
+
+ Copyright (C) 1989, 1991 Free Software Foundation, Inc.,
+ 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA
+ Everyone is permitted to copy and distribute verbatim copies
+ of this license document, but changing it is not allowed.
+
+                     Preamble
+
+  The licenses for most software are designed to take away your
+freedom to share and change it.  By contrast, the GNU General Public
+License is intended to guarantee your freedom to share and change free
+software--to make sure the software is free for all its users.  This
+General Public License applies to most of the Free Software
+Foundation's software and to any other program whose authors commit to
+using it.  (Some other Free Software Foundation software is covered by
+the GNU Lesser General Public License instead.)  You can apply it to
+your programs, too.
+
+  When we speak of free software, we are referring to freedom, not
+price.  Our General Public Licenses are designed to make sure that you
+have the freedom to distribute copies of free software (and charge for
+this service if you wish), that you receive source code or can get it
+if you want it, that you can change the software or use pieces of it
+in new free programs; and that you know you can do these things.
+
+  To protect your rights, we need to make restrictions that forbid
+anyone to deny you these rights or to ask you to surrender the rights.
+These restrictions translate to certain responsibilities for you if you
+distribute copies of the software, or if you modify it.
+
+  For example, if you distribute copies of such a program, whether
+gratis or for a fee, you must give the recipients all the rights that
+you have.  You must make sure that they, too, receive or can get the
+source code.  And you must show them these terms so they know their
+rights.
+
+  We protect your rights with two steps: (1) copyright the software, and
+(2) offer you this license which gives you legal permission to copy,
+distribute and/or modify the software.
+
+  Also, for each author's protection and ours, we want to make certain
+that everyone understands that there is no warranty for this free
+software.  If the software is modified by someone else and passed on, we
+want its recipients to know that what they have is not the original, so
+that any problems introduced by others will not reflect on the original
+authors' reputations.
+
+  Finally, any free program is threatened constantly by software
+patents.  We wish to avoid the danger that redistributors of a free
+program will individually obtain patent licenses, in effect making the
+program proprietary.  To prevent this, we have made it clear that any
+patent must be licensed for everyone's free use or not licensed at all.
+
+  The precise terms and conditions for copying, distribution and
+modification follow.
+
+             GNU GENERAL PUBLIC LICENSE
+   TERMS AND CONDITIONS FOR COPYING, DISTRIBUTION AND MODIFICATION
+
+  0. This License applies to any program or other work which contains
+a notice placed by the copyright holder saying it may be distributed
+under the terms of this General Public License.  The "Program", below,
+refers to any such program or work, and a "work based on the Program"
+means either the Program or any derivative work under copyright law:
+that is to say, a work containing the Program or a portion of it,
+either verbatim or with modifications and/or translated into another
+language.  (Hereinafter, translation is included without limitation in
+the term "modification".)  Each licensee is addressed as "you".
+
+Activities other than copying, distribution and modification are not
+covered by this License; they are outside its scope.  The act of
+running the Program is not restricted, and the output from the Program
+is covered only if its contents constitute a work based on the
+Program (independent of having been made by running the Program).
+Whether that is true depends on what the Program does.
+
+  1. You may copy and distribute verbatim copies of the Program's
+source code as you receive it, in any medium, provided that you
+conspicuously and appropriately publish on each copy an appropriate
+copyright notice and disclaimer of warranty; keep intact all the
+notices that refer to this License and to the absence of any warranty;
+and give any other recipients of the Program a copy of this License
+along with the Program.
+
+You may charge a fee for the physical act of transferring a copy, and
+you may at your option offer warranty protection in exchange for a fee.
+
+  2. You may modify your copy or copies of the Program or any portion
+of it, thus forming a work based on the Program, and copy and
+distribute such modifications or work under the terms of Section 1
+above, provided that you also meet all of these conditions:
+
+    a) You must cause the modified files to carry prominent notices
+    stating that you changed the files and the date of any change.
+
+    b) You must cause any work that you distribute or publish, that in
+    whole or in part contains or is derived from the Program or any
+    part thereof, to be licensed as a whole at no charge to all third
+    parties under the terms of this License.
+
+    c) If the modified program normally reads commands interactively
+    when run, you must cause it, when started running for such
+    interactive use in the most ordinary way, to print or display an
+    announcement including an appropriate copyright notice and a
+    notice that there is no warranty (or else, saying that you provide
+    a warranty) and that users may redistribute the program under
+    these conditions, and telling the user how to view a copy of this
+    License.  (Exception: if the Program itself is interactive but
+    does not normally print such an announcement, your work based on
+    the Program is not required to print an announcement.)
+
+These requirements apply to the modified work as a whole.  If
+identifiable sections of that work are not derived from the Program,
+and can be reasonably considered independent and separate works in
+themselves, then this License, and its terms, do not apply to those
+sections when you distribute them as separate works.  But when you
+distribute the same sections as part of a whole which is a work based
+on the Program, the distribution of the whole must be on the terms of
+this License, whose permissions for other licensees extend to the
+entire whole, and thus to each and every part regardless of who wrote it.
+
+Thus, it is not the intent of this section to claim rights or contest
+your rights to work written entirely by you; rather, the intent is to
+exercise the right to control the distribution of derivative or
+collective works based on the Program.
+
+In addition, mere aggregation of another work not based on the Program
+with the Program (or with a work based on the Program) on a volume of
+a storage or distribution medium does not bring the other work under
+the scope of this License.
+
+  3. You may copy and distribute the Program (or a work based on it,
+under Section 2) in object code or executable form under the terms of
+Sections 1 and 2 above provided that you also do one of the following:
+
+    a) Accompany it with the complete corresponding machine-readable
+    source code, which must be distributed under the terms of Sections
+    1 and 2 above on a medium customarily used for software interchange; or,
+
+    b) Accompany it with a written offer, valid for at least three
+    years, to give any third party, for a charge no more than your
+    cost of physically performing source distribution, a complete
+    machine-readable copy of the corresponding source code, to be
+    distributed under the terms of Sections 1 and 2 above on a medium
+    customarily used for software interchange; or,
+
+    c) Accompany it with the information you received as to the offer
+    to distribute corresponding source code.  (This alternative is
+    allowed only for noncommercial distribution and only if you
+    received the program in object code or executable form with such
+    an offer, in accord with Subsection b above.)
+
+The source code for a work means the preferred form of the work for
+making modifications to it.  For an executable work, complete source
+code means all the source code for all modules it contains, plus any
+associated interface definition files, plus the scripts used to
+control compilation and installation of the executable.  However, as a
+special exception, the source code distributed need not include
+anything that is normally distributed (in either source or binary
+form) with the major components (compiler, kernel, and so on) of the
+operating system on which the executable runs, unless that component
+itself accompanies the executable.
+
+If distribution of executable or object code is made by offering
+access to copy from a designated place, then offering equivalent
+access to copy the source code from the same place counts as
+distribution of the source code, even though third parties are not
+compelled to copy the source along with the object code.
+
+  4. You may not copy, modify, sublicense, or distribute the Program
+except as expressly provided under this License.  Any attempt
+otherwise to copy, modify, sublicense or distribute the Program is
+void, and will automatically terminate your rights under this License.
+However, parties who have received copies, or rights, from you under
+this License will not have their licenses terminated so long as such
+parties remain in full compliance.
+
+  5. You are not required to accept this License, since you have not
+signed it.  However, nothing else grants you permission to modify or
+distribute the Program or its derivative works.  These actions are
+prohibited by law if you do not accept this License.  Therefore, by
+modifying or distributing the Program (or any work based on the
+Program), you indicate your acceptance of this License to do so, and
+all its terms and conditions for copying, distributing or modifying
+the Program or works based on it.
+
+  6. Each time you redistribute the Program (or any work based on the
+Program), the recipient automatically receives a license from the
+original licensor to copy, distribute or modify the Program subject to
+these terms and conditions.  You may not impose any further
+restrictions on the recipients' exercise of the rights granted herein.
+You are not responsible for enforcing compliance by third parties to
+this License.
+
+  7. If, as a consequence of a court judgment or allegation of patent
+infringement or for any other reason (not limited to patent issues),
+conditions are imposed on you (whether by court order, agreement or
+otherwise) that contradict the conditions of this License, they do not
+excuse you from the conditions of this License.  If you cannot
+distribute so as to satisfy simultaneously your obligations under this
+License and any other pertinent obligations, then as a consequence you
+may not distribute the Program at all.  For example, if a patent
+license would not permit royalty-free redistribution of the Program by
+all those who receive copies directly or indirectly through you, then
+the only way you could satisfy both it and this License would be to
+refrain entirely from distribution of the Program.
+
+If any portion of this section is held invalid or unenforceable under
+any particular circumstance, the balance of the section is intended to
+apply and the section as a whole is intended to apply in other
+circumstances.
+
+It is not the purpose of this section to induce you to infringe any
+patents or other property right claims or to contest validity of any
+such claims; this section has the sole purpose of protecting the
+integrity of the free software distribution system, which is
+implemented by public license practices.  Many people have made
+generous contributions to the wide range of software distributed
+through that system in reliance on consistent application of that
+system; it is up to the author/donor to decide if he or she is willing
+to distribute software through any other system and a licensee cannot
+impose that choice.
+
+This section is intended to make thoroughly clear what is believed to
+be a consequence of the rest of this License.
+
+  8. If the distribution and/or use of the Program is restricted in
+certain countries either by patents or by copyrighted interfaces, the
+original copyright holder who places the Program under this License
+may add an explicit geographical distribution limitation excluding
+those countries, so that distribution is permitted only in or among
+countries not thus excluded.  In such case, this License incorporates
+the limitation as if written in the body of this License.
+
+  9. The Free Software Foundation may publish revised and/or new versions
+of the General Public License from time to time.  Such new versions will
+be similar in spirit to the present version, but may differ in detail to
+address new problems or concerns.
+
+Each version is given a distinguishing version number.  If the Program
+specifies a version number of this License which applies to it and "any
+later version", you have the option of following the terms and conditions
+either of that version or of any later version published by the Free
+Software Foundation.  If the Program does not specify a version number of
+this License, you may choose any version ever published by the Free Software
+Foundation.
+
+  10. If you wish to incorporate parts of the Program into other free
+programs whose distribution conditions are different, write to the author
+to ask for permission.  For software which is copyrighted by the Free
+Software Foundation, write to the Free Software Foundation; we sometimes
+make exceptions for this.  Our decision will be guided by the two goals
+of preserving the free status of all derivatives of our free software and
+of promoting the sharing and reuse of software generally.
+
+                     NO WARRANTY
+
+  11. BECAUSE THE PROGRAM IS LICENSED FREE OF CHARGE, THERE IS NO WARRANTY
+FOR THE PROGRAM, TO THE EXTENT PERMITTED BY APPLICABLE LAW.  EXCEPT WHEN
+OTHERWISE STATED IN WRITING THE COPYRIGHT HOLDERS AND/OR OTHER PARTIES
+PROVIDE THE PROGRAM "AS IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESSED
+OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF
+MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE.  THE ENTIRE RISK AS
+TO THE QUALITY AND PERFORMANCE OF THE PROGRAM IS WITH YOU.  SHOULD THE
+PROGRAM PROVE DEFECTIVE, YOU ASSUME THE COST OF ALL NECESSARY SERVICING,
+REPAIR OR CORRECTION.
+
+  12. IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN WRITING
+WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MAY MODIFY AND/OR
+REDISTRIBUTE THE PROGRAM AS PERMITTED ABOVE, BE LIABLE TO YOU FOR DAMAGES,
+INCLUDING ANY GENERAL, SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING
+OUT OF THE USE OR INABILITY TO USE THE PROGRAM (INCLUDING BUT NOT LIMITED
+TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY
+YOU OR THIRD PARTIES OR A FAILURE OF THE PROGRAM TO OPERATE WITH ANY OTHER
+PROGRAMS), EVEN IF SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE
+POSSIBILITY OF SUCH DAMAGES.
+
+              END OF TERMS AND CONDITIONS
+
+     How to Apply These Terms to Your New Programs
+
+  If you develop a new program, and you want it to be of the greatest
+possible use to the public, the best way to achieve this is to make it
+free software which everyone can redistribute and change under these terms.
+
+  To do so, attach the following notices to the program.  It is safest
+to attach them to the start of each source file to most effectively
+convey the exclusion of warranty; and each file should have at least
+the "copyright" line and a pointer to where the full notice is found.
+
+    <one line to give the program's name and a brief idea of what it does.>
+    Copyright (C) <year>  <name of author>
+
+    This program is free software; you can redistribute it and/or modify
+    it under the terms of the GNU General Public License as published by
+    the Free Software Foundation; either version 2 of the License, or
+    (at your option) any later version.
+
+    This program is distributed in the hope that it will be useful,
+    but WITHOUT ANY WARRANTY; without even the implied warranty of
+    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+    GNU General Public License for more details.
+
+    You should have received a copy of the GNU General Public License along
+    with this program; if not, write to the Free Software Foundation, Inc.,
+    51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
+
+Also add information on how to contact you by electronic and paper mail.
+
+If the program is interactive, make it output a short notice like this
+when it starts in an interactive mode:
+
+    Gnomovision version 69, Copyright (C) year name of author
+    Gnomovision comes with ABSOLUTELY NO WARRANTY; for details type `show w'.
+    This is free software, and you are welcome to redistribute it
+    under certain conditions; type `show c' for details.
+
+The hypothetical commands `show w' and `show c' should show the appropriate
+parts of the General Public License.  Of course, the commands you use may
+be called something other than `show w' and `show c'; they could even be
+mouse-clicks or menu items--whatever suits your program.
+
+You should also get your employer (if you work as a programmer) or your
+school, if any, to sign a "copyright disclaimer" for the program, if
+necessary.  Here is a sample; alter the names:
+
+  Yoyodyne, Inc., hereby disclaims all copyright interest in the program
+  `Gnomovision' (which makes passes at compilers) written by James Hacker.
+
+  <signature of Ty Coon>, 1 April 1989
+  Ty Coon, President of Vice
+
+This General Public License does not permit incorporating your program into
+proprietary programs.  If your program is a subroutine library, you may
+consider it more useful to permit linking proprietary applications with the
+library.  If this is what you want to do, use the GNU Lesser General
+Public License instead of this License.
diff --git a/README b/README
new file mode 100644
--- /dev/null
+++ b/README
@@ -0,0 +1,5 @@
+Overview of applications:
+
+* SymmSHE.hs gives an implementation of a symmetric-key,
+  somewhat-homomorphic encryption scheme that is essentially
+  equivalent to the one from the toolkit paper [LPR'13].
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/benchmarks/Main.hs b/benchmarks/Main.hs
new file mode 100644
--- /dev/null
+++ b/benchmarks/Main.hs
@@ -0,0 +1,10 @@
+
+import SHEBenches
+
+import Criterion.Main
+import Control.Monad
+
+main :: IO ()
+main = defaultMain =<< (sequence [
+  sheBenches
+  ])
diff --git a/benchmarks/SHEBenches.hs b/benchmarks/SHEBenches.hs
new file mode 100644
--- /dev/null
+++ b/benchmarks/SHEBenches.hs
@@ -0,0 +1,120 @@
+{-# LANGUAGE DataKinds, FlexibleContexts, 
+             NoImplicitPrelude, PolyKinds, RebindableSyntax, 
+             ScopedTypeVariables, TypeFamilies, 
+             TypeOperators #-}
+
+module SHEBenches (sheBenches) where
+
+import Gen
+import Utils
+import Harness.SHE
+import Benchmarks hiding (hideArgs)
+
+import Control.Applicative
+import Control.Monad.Random
+import Control.Monad.State
+import Crypto.Random.DRBG
+
+import Crypto.Lol hiding (CT)
+import Crypto.Lol.Applications.SymmSHE
+import qualified Crypto.Lol.Cyclotomic.Tensor.CTensor as CT
+import Crypto.Lol.Types.Random
+
+import qualified Criterion as C
+
+hideArgs :: forall a rnd bnch . 
+  (GenArgs (StateT (Maybe (SKOf a)) rnd) bnch, Monad rnd, ShowType a,
+   ResultOf bnch ~ Bench a)
+  => bnch -> Proxy a -> rnd Benchmark
+hideArgs f p = (C.bench (showType p) . unbench) <$> 
+  (evalStateT (genArgs f) (Nothing :: Maybe (SKOf a)))
+
+sheBenches :: (MonadRandom m) => m Benchmark
+sheBenches = benchGroup "SHE" [
+  benchGroup "encrypt"   $ applyEnc (Proxy::Proxy EncParams)         $ hideArgs bench_enc,
+  benchGroup "decrypt"   $ applyDec (Proxy::Proxy DecParams)         $ hideArgs bench_dec,
+  benchGroup "*"         $ applyCTFunc (Proxy::Proxy CTParams)       $ hideArgs bench_mul,
+  benchGroup "addPublic" $ applyCTFunc (Proxy::Proxy CTParams)       $ hideArgs bench_addPublic,
+  benchGroup "mulPublic" $ applyCTFunc (Proxy::Proxy CTParams)       $ hideArgs bench_mulPublic,
+  benchGroup "dec"       $ applyDec (Proxy::Proxy DecParams)         $ hideArgs bench_dec,
+  benchGroup "rescaleCT" $ applyRescale (Proxy::Proxy RescaleParams) $ hideArgs bench_rescaleCT,
+  benchGroup "keySwitch" $ applyKSQ (Proxy::Proxy KSQParams)         $ hideArgs bench_keySwQ,
+  benchGroup "tunnel"    $ applyTunn (Proxy::Proxy TunnParams)       $ hideArgs bench_tunnel
+  ]
+
+bench_enc :: forall t m m' z zp zq gen . (EncryptCtx t m m' z zp zq, CryptoRandomGen gen, z ~ LiftOf zp, NFElt zp, NFElt zq)
+  => SK (Cyc t m' z) -> PT (Cyc t m zp) -> Bench '(t,m,m',zp,zq,gen)
+bench_enc sk pt = benchIO $ do
+  gen <- newGenIO
+  return $ evalRand (encrypt sk pt :: Rand (CryptoRand gen) (CT m zp (Cyc t m' zq))) gen
+
+bench_mul :: (Ring (CT m zp (Cyc t m' zq)), NFData (CT m zp (Cyc t m' zq)))
+  => CT m zp (Cyc t m' zq) -> CT m zp (Cyc t m' zq) -> Bench '(t,m,m',zp,zq)
+bench_mul a = bench (*a)
+
+bench_addPublic :: (AddPublicCtx t m m' zp zq, NFElt zp, NFElt zq) => Cyc t m zp -> CT m zp (Cyc t m' zq) -> Bench '(t,m,m',zp,zq)
+bench_addPublic a ct = bench (addPublic a) ct
+
+bench_mulPublic :: (MulPublicCtx t m m' zp zq, NFElt zp, NFElt zq) => Cyc t m zp -> CT m zp (Cyc t m' zq) -> Bench '(t,m,m',zp,zq)
+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) 
+  => 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
+
+bench_rescaleCT :: forall t m m' zp zq zq' . 
+  (RescaleCyc (Cyc t) zq' zq, ToSDCtx t m' zp zq', NFData (CT m zp (Cyc t m' zq)))
+  => CT m zp (Cyc t m' zq') -> Bench '(t,m,m',zp,zq,zq')
+bench_rescaleCT = bench (rescaleLinearCT :: CT m zp (Cyc t m' zq') -> CT m zp (Cyc t m' zq))
+
+bench_keySwQ :: (Ring (CT m zp (Cyc t m' zq)), NFData (CT m zp (Cyc t m' zq))) 
+  => KSHint m zp t m' zq gad zq' -> CT m zp (Cyc t m' zq) -> Bench '(t,m,m',zp,zq,zq',gad)
+bench_keySwQ (KeySwitch kswq) x = bench kswq $ x*x
+
+bench_tunnel :: (NFData (CT s zp (Cyc t s' zq))) 
+  => Tunnel t r r' s s' zp zq gad -> CT r zp (Cyc t r' zq) -> Bench '(t,r,r',s,s',zp,zq,gad)
+bench_tunnel (Tunnel f) x = bench f x
+
+type Gens    = '[HashDRBG]
+type Gadgets = '[TrivGad, BaseBGad 2]
+type Tensors = '[CT.CT,RT]
+type MM'PQCombos = 
+  '[ '(F4, F128, Zq 64, Zq 257),
+     '(F4, F128, Zq 64, Zq (257 ** 641)),
+     '(F12, F32 * F9, Zq 64, Zq 577),
+     '(F12, F32 * F9, Zq 64, Zq (577 ** 1153)),
+     '(F12, F32 * F9, Zq 64, Zq (577 ** 1153 ** 2017)),
+     '(F12, F32 * F9, Zq 64, Zq (577 ** 1153 ** 2017 ** 2593)),
+     '(F12, F32 * F9, Zq 64, Zq (577 ** 1153 ** 2017 ** 2593 ** 3169)),
+     '(F12, F32 * F9, Zq 64, Zq (577 ** 1153 ** 2017 ** 2593 ** 3169 ** 3457)),
+     '(F12, F32 * F9, Zq 64, Zq (577 ** 1153 ** 2017 ** 2593 ** 3169 ** 3457 ** 6337)),
+     '(F12, F32 * F9, Zq 64, Zq (577 ** 1153 ** 2017 ** 2593 ** 3169 ** 3457 ** 6337 ** 7489)),
+     '(F12, F32 * F9 * F25, Zq 64, Zq 14401),
+     '(F12, F32 * F9 * F25, Zq 64, Zq (14401 ** 21601))
+    ]
+
+type CTParams  = ( '(,) <$> Tensors) <*> MM'PQCombos
+type DecParams = ( '(,) <$> Tensors) <*> (Nub (Filter Liftable MM'PQCombos))
+type RescaleParams = ( '(,) <$> Tensors) <*> (Map AddZq (Filter NonLiftable MM'PQCombos))
+type KSQParams = ( '(,) <$> Gadgets) <*> RescaleParams
+type EncParams = ( '(,) <$> Gens) <*> CTParams
+
+-- 3144961,5241601,7338241,9959041,10483201,11531521,12579841,15200641,18869761,19393921
+type TunnParams = 
+  ( '(,) <$> Gadgets) <*> 
+  (( '(,) <$> Tensors) <*> 
+  (( '(,) <$> TunnRings) <*> TunnMods))
+
+
+type TunnRings = '[
+  {- H0 -> H1 -} '(F128, F128 * F7 * F13, F64 * F7, F64 * F7 * F13),
+  {- H1 -> H2 -} '(F64 * F7, F64 * F7 * F13, F32 * F7 * F13, F32 * F7 * F13),
+  {- H2 -> H3 -} '(F32 * F7 * F13, F32 * F7 * F13, F8 * F5 * F7 * F13, F8 * F5 * F7 *F13),
+  {- H3 -> H4 -} '(F8 * F5 * F7 * F13, F8 * F5 * F7 *F13, F4 * F3 * F5 * F7 * F13, F4 * F3 * F5 * F7 * F13),
+  {- H4 -> H5 -} '(F4 * F3 * F5 * F7 * F13, F4 * F3 * F5 * F7 *F13, F9 * F5 * F7 * F13, F9 * F5 * F7 * F13)
+    ]
+
+type TunnMods = '[
+  '(Zq PP32, Zq 3144961)
+  ]
diff --git a/lol-apps.cabal b/lol-apps.cabal
new file mode 100644
--- /dev/null
+++ b/lol-apps.cabal
@@ -0,0 +1,122 @@
+name:                lol-apps
+-- The package version.  See the Haskell package versioning policy (PVP) 
+-- for standards guiding when and how versions should be incremented.
+-- http://www.haskell.org/haskellwiki/Package_versioning_policy
+-- PVP summary:      +-+------- breaking API changes
+--                   | | +----- non-breaking API additions
+--                   | | | +--- code changes with no API change
+version:             0.0.0.1
+synopsis:            Cryptographic applications using <https://hackage.haskell.org/package/lol Λ ○ λ>.
+homepage:            https://github.com/cpeikert/Lol
+Bug-Reports:         https://github.com/cpeikert/Lol/issues
+license:             GPL-2
+license-file:        LICENSE
+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, CHANGES.md,
+                     benchmarks/SHEBenches.hs,
+                     tests/SHETests.hs,
+                     utils/Apply.hs,
+                     utils/Benchmarks.hs,
+                     utils/Gen.hs,
+                     utils/Tests.hs,
+                     utils/TestTypes.hs,
+                     utils/Utils.hs
+                     utils/Harness/SHE.hs
+cabal-version:       >= 1.10
+description:
+    This library contains example cryptographic applications built using 
+    <https://hackage.haskell.org/package/lol Λ ○ λ>  (Lol), 
+    a general-purpose library for ring-based lattice cryptography.
+
+source-repository head
+  type: git
+  location: https://github.com/cpeikert/Lol
+
+Flag llvm
+  Description:  Compile via LLVM. This produces much better object code,
+                but you need to have the LLVM compiler installed.
+
+  Default:      True
+
+Flag opt
+  Description: Turn on library optimizations
+  Default:     True
+  Manual:      False
+
+library
+  default-language:   Haskell2010
+
+  if flag(llvm)
+    ghc-options: -fllvm -optlo-O3
+
+  -- ghc optimizations
+  if flag(opt)
+    ghc-options: -O3 -Odph -funbox-strict-fields -fwarn-dodgy-imports -rtsopts
+    ghc-options: -fno-liberate-case -funfolding-use-threshold1000 -funfolding-keeness-factor1000
+
+  exposed-modules: 
+    Crypto.Lol.Applications.SymmSHE
+
+  build-depends:
+    base==4.8.*,
+    deepseq >= 1.4.1.1 && <1.5,
+    lol == 0.2.0.0,
+    MonadRandom >= 0.2 && < 0.5,
+    numeric-prelude >= 0.4.2 && < 0.5
+
+test-suite test-apps
+  type:               exitcode-stdio-1.0
+  hs-source-dirs:     tests,utils
+  default-language:   Haskell2010
+  main-is:            Main.hs
+
+  ghc-options: -threaded -rtsopts
+
+  build-depends:
+    base,
+    constraints,
+    deepseq,
+    DRBG,
+    lol,
+    lol-apps,
+    MonadRandom,
+    mtl,
+    QuickCheck >= 2.8 && < 2.9,
+    random,
+    repa,
+    singletons,
+    test-framework >= 0.8 && < 0.9,
+    test-framework-quickcheck2 >= 0.3 && < 0.4,
+    vector
+
+Benchmark bench-apps
+  type:               exitcode-stdio-1.0
+  hs-source-dirs:     benchmarks,utils
+  default-language:   Haskell2010
+  main-is:            Main.hs
+
+--  if flag(llvm)
+--    ghc-options: -fllvm -optlo-O3
+  ghc-options: -threaded -rtsopts
+--  ghc-options: -O2 -Odph -funbox-strict-fields -fwarn-dodgy-imports -rtsopts
+--  ghc-options: -fno-liberate-case -funfolding-use-threshold1000 -funfolding-keeness-factor1000
+
+  build-depends:
+    base,
+    criterion,
+    deepseq,
+    DRBG,
+    lol,
+    lol-apps,
+    MonadRandom,
+    mtl,
+    singletons,
+    transformers,
+    vector,
+    repa                        
+
diff --git a/tests/Main.hs b/tests/Main.hs
new file mode 100644
--- /dev/null
+++ b/tests/Main.hs
@@ -0,0 +1,10 @@
+
+import SHETests
+
+import Test.Framework
+
+main :: IO ()
+main = do
+  flip defaultMainWithArgs ["--threads=1","--maximum-generated-tests=100"]
+    [ testGroup "SHE Tests" sheTests
+    ]
diff --git a/tests/SHETests.hs b/tests/SHETests.hs
new file mode 100644
--- /dev/null
+++ b/tests/SHETests.hs
@@ -0,0 +1,307 @@
+{-# LANGUAGE DataKinds, FlexibleContexts,
+             NoImplicitPrelude, PolyKinds, RebindableSyntax,
+             ScopedTypeVariables, TypeFamilies, TypeOperators #-}
+
+module SHETests (sheTests) where
+
+import Gen
+import Harness.SHE
+import Tests hiding (hideArgs)
+import Utils
+
+import Control.Applicative
+import Control.Monad
+import Control.Monad.Random
+import Control.Monad.State
+
+import Crypto.Lol hiding (CT)
+import Crypto.Lol.Applications.SymmSHE
+import Crypto.Lol.Cyclotomic.Linear
+import qualified Crypto.Lol.Cyclotomic.Tensor.CTensor as CT
+
+import qualified Test.Framework as TF
+import Test.Framework.Providers.QuickCheck2
+import Test.QuickCheck
+
+v = 1 :: Double
+
+hideArgs :: forall a rnd bnch. 
+  (GenArgs (StateT (Maybe (SKOf a)) rnd) bnch, MonadRandom rnd, 
+   ShowType a, ResultOf bnch ~ Test a)
+  => bnch -> Proxy a -> rnd TF.Test
+hideArgs f p = do
+  res <- evalStateT (genArgs f) (Nothing :: Maybe (SKOf a))
+  case res of
+    Test b -> return $ testProperty (showType p) b
+    TestM b -> testProperty (showType p) <$> b
+
+sheTests = 
+  [testGroupM "Dec . Enc"  $ applyDec (Proxy::Proxy DecParams) $ hideArgs prop_encDec,
+   testGroupM "DecU . Enc" $ applyCTFunc (Proxy::Proxy CTParams) $ hideArgs prop_encDecU,
+   testGroupM "AddPub"     $ applyCTFunc (Proxy::Proxy CTParams) $ hideArgs prop_addPub,
+   testGroupM "MulPub"     $ applyCTFunc (Proxy::Proxy CTParams) $ hideArgs prop_mulPub,
+   testGroupM "ScalarPub"  $ applyCTFunc (Proxy::Proxy CTParams) $ hideArgs prop_addScalar,
+   testGroupM "CTAdd"      $ applyCTFunc (Proxy::Proxy CTParams) $ hideArgs prop_ctadd,
+   testGroupM "CTMul"      $ applyCTFunc (Proxy::Proxy CTParams) $ hideArgs prop_ctmul,
+   testGroupM "CT zero"    $ applyCTFunc (Proxy::Proxy CTParams) $ hideArgs prop_ctzero,
+   testGroupM "CT one"     $ applyCTFunc (Proxy::Proxy CTParams) $ hideArgs prop_ctone,
+   testGroupM "ModSwitch PT" modSwPTTests,
+   testGroupM "Tunnel"       tunnelTests,
+   testGroupM "Twace"      $ applyCTTwEm (Proxy::Proxy TwoIdxParams) $ hideArgs prop_cttwace,
+   testGroupM "Embed"      $ applyCTTwEm (Proxy::Proxy TwoIdxParams) $ hideArgs prop_ctembed,
+   testGroupM "KSLin"      $ applyKSQ (Proxy::Proxy KSQParams) $ hideArgs prop_ksLin,
+   testGroupM "keySwitch"  $ applyKSQ (Proxy::Proxy KSQParams) $ hideArgs prop_ksQuad
+  ]
+
+type CTCombos = '[
+  '(F7, F7, Zq 2,Zq (19393921 ** 18869761)),
+  '(F7, F21,Zq 2,Zq (19393921 ** 18869761)),
+  '(F2, F8, Zq 2,Zq 536871001),
+  '(F1, F8, Zq 2,Zq 536871001),
+  '(F4, F12,Zq 2,Zq 2148249601),
+  '(F4, F8, Zq 3,Zq 2148249601),
+  '(F7, F7, Zq 4,Zq (19393921 ** 18869761)),
+  '(F7, F21,Zq 4,Zq (19393921 ** 18869761)),
+  '(F1, F4, Zq 4,Zq 18869761),
+  '(F4, F4, Zq 4,Zq 18869761),
+  '(F14,F14,Zq 4,Zq 18869761),
+  '(F28,F28,Zq 4,Zq 18869761),
+  '(F28,F28,Zq 4,Zq 80221),
+  '(F1, F8, Zq 4,Zq 536871001),
+  '(F2, F8, Zq 4,Zq 536871001),
+  '(F4, F12,Zq 8,Zq 2148249601)
+  ]
+
+type Gadgets = '[TrivGad, BaseBGad 2]
+type Tensors = '[CT.CT,RT]
+type MM'PQCombos = 
+  '[ '(F1, F7, Zq 2, Zq (19393921 ** 18869761)),
+     '(F2, F4, Zq 8, Zq (2148854401 ** 2148249601)),
+     '(F4, F12, Zq 2, Zq (2148854401 ** 2148249601)),
+     '(F8, F64, Zq 2, Zq (2148854401 ** 2148249601)),
+     '(F3, F27, Zq 2, Zq (2148854401 ** 2148249601)),
+     '(F2, F4, Zq 8, Zq (2148854401 ** 2148249601 ** 2150668801)),
+     '(F4, F12, Zq 2, Zq (2148854401 ** 2148249601 ** 2150668801)),
+     '(F8, F64, Zq 2, Zq (2148854401 ** 2148249601 ** 2150668801)),
+     '(F3, F27, Zq 2, Zq (2148854401 ** 2148249601 ** 2150668801))]
+
+
+type CTParams  = ( '(,) <$> Tensors) <*> CTCombos
+type DecParams = ( '(,) <$> Tensors) <*> (Nub (Filter Liftable CTCombos))
+type Zq'Params = ( '(,) <$> Tensors) <*> (Map AddZq (Filter NonLiftable MM'PQCombos))
+type KSQParams = ( '(,) <$> Gadgets) <*> Zq'Params
+type TwoIdxParams = ( '(,) <$> Tensors) <*> '[ '(F1, F7, F3, F21, Zq 2, Zq 18869761)]
+
+prop_ksLin :: (DecryptUCtx t m m' z zp zq, Eq (Cyc t m zp))
+  => SK (Cyc t m' z) 
+     -> KSLinear t m m' z zp zq zq' gad 
+     -> PTCT m zp (Cyc t m' zq) 
+     -> Test '(t,m,m',zp,zq,zq',gad)
+prop_ksLin skin (KSL kswlin skout) (PTCT x' x) =
+  let y = kswlin x
+      y' = decryptUnrestricted skout y
+  in test $ x' == y'
+
+prop_ksQuad :: (Ring (CT m zp (Cyc t m' zq)),
+                DecryptUCtx t m m' z zp zq, 
+                Eq (Cyc t m zp))
+  => SK (Cyc t m' z) 
+     -> KSHint m zp t m' zq gad zq' 
+     -> PTCT m zp (Cyc t m' zq)
+     -> PTCT m zp (Cyc t m' zq)
+     -> Test '(t,m,m',zp,zq,zq',gad)
+prop_ksQuad sk (KeySwitch kswq) (PTCT y1 x1) (PTCT y2 x2) = 
+  let x' = kswq $ x1*x2
+      y = y1*y2
+      x = decryptUnrestricted sk x'
+  in test $ y == x
+
+prop_addPub :: forall t m m' z zp zq . 
+  (DecryptUCtx t m m' z zp zq,
+   AddPublicCtx t m m' zp zq,
+   Eq (Cyc t m zp))
+  => SK (Cyc t m' z) 
+     -> Cyc t m zp 
+     -> PTCT m zp (Cyc t m' zq) 
+     -> Test '(t,m,m',zp,zq)
+prop_addPub sk x (PTCT y' y) = 
+  let xy = addPublic x y
+      xy' = decryptUnrestricted sk xy
+  in test $ xy' == (x+y')
+
+prop_mulPub :: (DecryptUCtx t m m' z zp zq,
+                MulPublicCtx t m m' zp zq,
+                Eq (Cyc t m zp))
+  => SK (Cyc t m' z) 
+     -> Cyc t m zp 
+     -> PTCT m zp (Cyc t m' zq)
+     -> Test '(t,m,m',zp,zq)
+prop_mulPub sk x (PTCT y' y) = 
+  let xy = mulPublic x y
+      xy' = decryptUnrestricted sk xy
+  in test $ xy' == (x*y')
+
+prop_addScalar :: (DecryptUCtx t m m' z zp zq,
+                   AddScalarCtx t m' zp zq,
+                   Eq (Cyc t m zp))
+  => SK (Cyc t m' z) -> zp -> PTCT m zp (Cyc t m' zq) -> Test '(t,m,m',zp,zq)
+prop_addScalar sk c (PTCT x' x) =
+  let cx = addScalar c x
+      cx' = decryptUnrestricted sk cx
+  in test $ cx' == ((scalarCyc c)+x')
+
+prop_ctadd :: (DecryptUCtx t m m' z zp zq,
+               Additive (CT m zp (Cyc t m' zq)),
+               Eq (Cyc t m zp))
+  => SK (Cyc t m' z) 
+     -> PTCT m zp (Cyc t m' zq)
+     -> PTCT m zp (Cyc t m' zq)
+     -> Test '(t,m,m',zp,zq)
+prop_ctadd sk (PTCT x1' x1) (PTCT x2' x2) = 
+  let y = x1+x2
+      y' = decryptUnrestricted sk y
+  in test $ x1'+x2' == y'
+
+prop_ctmul :: (DecryptUCtx t m m' z zp zq,
+               Ring (CT m zp (Cyc t m' zq)),
+               Eq (Cyc t m zp))
+  => SK (Cyc t m' z) 
+     -> PTCT m zp (Cyc t m' zq)
+     -> PTCT m zp (Cyc t m' zq)
+     -> Test '(t,m,m',zp,zq)
+prop_ctmul sk (PTCT x1' x1) (PTCT x2' x2) = 
+  let y = x1*x2
+      y' = decryptUnrestricted sk y
+  in test $ x1'*x2' == y'
+
+prop_ctzero :: forall t m m' z zp zq .
+ (DecryptUCtx t m m' z zp zq,
+  Additive (CT m zp (Cyc t m' zq)),
+  Eq (Cyc t m zp)) 
+  => SK (Cyc t m' z) -> Test '(t,m,m',zp,zq)
+prop_ctzero sk =
+  let z = decryptUnrestricted sk (zero :: CT m zp (Cyc t m' zq))
+  in test $ zero == z
+
+prop_ctone :: forall t m m' z zp zq .
+  (DecryptUCtx t m m' z zp zq,
+   Ring (CT m zp (Cyc t m' zq)),
+   Eq (Cyc t m zp))
+  => SK (Cyc t m' z) -> Test '(t,m,m',zp,zq)
+prop_ctone sk = 
+  let z = decryptUnrestricted sk (one :: CT m zp (Cyc t m' zq))
+  in test $ one == z
+
+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))
+  => SK (Cyc t r' z) -> PTCT r zp (Cyc t r' zq) -> Test '(t,r,r',s,s',zp,zq)
+prop_ctembed sk (PTCT x' x) = 
+  let y = embedCT x :: CT s zp (Cyc t s' zq)
+      y' = decryptUnrestricted (embedSK sk) y
+  in test $ (embed x' :: Cyc t s zp) == y'
+
+-- CT must be encrypted with key from small ring
+prop_cttwace :: forall t r r' s s' z zp zq . 
+  (Eq zp,
+   EncryptCtx t s s' z zp zq, 
+   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
+  y :: CT s zp (Cyc t s' zq) <- encrypt (embedSK sk) x
+  let y' = twaceCT y :: CT r zp (Cyc t r' zq)
+      x' = decryptUnrestricted sk y'
+  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, 
+   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)
+prop_encDecU sk x = testIO $ do
+  y :: CT m zp (Cyc t m' zq) <- encrypt sk x
+  let x' = decryptUnrestricted sk $ y
+  return $ x == x'
+
+prop_encDec :: forall t m m' z zp zq . 
+  (GenSKCtx t m' z Double, 
+   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)
+prop_encDec sk x = testIO $ do
+  y :: CT m zp (Cyc t m' zq) <- encrypt sk x
+  let x' = decrypt sk $ y
+  return $ x == x'
+
+helper :: (Proxy '(t,b) -> a) -> Proxy t -> Proxy b -> a
+helper f _ _ = f Proxy
+
+-- one-off tests, no hideArgsper
+prop_modSwPT :: forall t m m' z zp zp' zq .
+  (Eq zp, Eq zp',
+   DecryptUCtx t m m' z zp zq,
+   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))
+prop_modSwPT sk y =
+  let p = proxy modulus (Proxy::Proxy zp)
+      p' = proxy modulus (Proxy::Proxy zp')
+      z = (fromIntegral $ p `div` p')*y
+      x = decryptUnrestricted sk z
+      y' = modSwitchPT z :: CT m zp' (Cyc t m' zq)
+      x'' = decryptUnrestricted sk y'
+  in test $ x'' == rescaleCyc Dec x
+
+modSwPTTests = (modSwPTTests' (Proxy::Proxy CT.CT)) ++ (modSwPTTests' (Proxy::Proxy RT))
+
+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 = (tunnelTests' (Proxy::Proxy CT.CT)) ++ (tunnelTests' (Proxy::Proxy RT))
+
+tunnelTests' p = 
+  [helper (hideArgs prop_ringTunnel) p 
+    (Proxy::Proxy '(F8,F40,F20,F60,Zq 4,Zq (18869761 ** 19393921),TrivGad))]
+
+prop_ringTunnel :: forall t e r s e' r' s' z zp zq gad . 
+  (TunnelCtx t e r s e' r' s' z zp zq gad,
+   EncryptCtx t r r' z zp zq,
+   GenSKCtx t r' z Double,
+   GenSKCtx t s' z Double,
+   DecryptUCtx t s s' z zp zq,
+   Random zp, Eq zp,
+   e ~ FGCD r s, Fact e) 
+  => Cyc t r zp -> Test '(t,'(r,r',s,s',zp,zq,gad))
+prop_ringTunnel x = testIO $ do
+  let totr = proxy totientFact (Proxy::Proxy r)
+      tote = proxy totientFact (Proxy::Proxy e)
+      basisSize = totr `div` tote
+  -- choose a random linear function of the appropriate size
+  bs :: [Cyc t s zp] <- replicateM basisSize getRandom
+  let f = (linearDec bs) \\ (gcdDivides (Proxy::Proxy r) (Proxy::Proxy s)) :: Linear t zp e r s 
+      expected = evalLin f x \\ (gcdDivides (Proxy::Proxy r) (Proxy::Proxy s))
+  skin :: SK (Cyc t r' (LiftOf zp)) <- genSK v
+  skout :: SK (Cyc t s' (LiftOf zp)) <- genSK v
+  y :: CT r zp (Cyc t r' zq) <- encrypt skin x
+  tunn <- proxyT (tunnelCT f skout skin) (Proxy::Proxy gad)
+  let y' = tunn y :: CT s zp (Cyc t s' zq)
+      actual = decryptUnrestricted skout y' :: Cyc t s zp
+  return $ expected == actual
+
diff --git a/utils/Apply.hs b/utils/Apply.hs
new file mode 100644
--- /dev/null
+++ b/utils/Apply.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE DataKinds, FlexibleInstances, MultiParamTypeClasses, PolyKinds, 
+             TypeFamilies, TypeOperators #-}
+
+-- applies functions to proxy arguments
+module Apply where
+
+class (params :: [k]) `Satisfy` (ctx :: *)  where
+  data ArgsCtx ctx
+
+  run :: proxy params
+            -> (ArgsCtx ctx -> rnd res) 
+            -> [rnd res]
+
+instance '[] `Satisfy` ctx  where
+  -- any implementation of ArgsCtx would conflict with concrete instances,
+  -- so skip  
+  run _ _ = []
diff --git a/utils/Benchmarks.hs b/utils/Benchmarks.hs
new file mode 100644
--- /dev/null
+++ b/utils/Benchmarks.hs
@@ -0,0 +1,46 @@
+{-# LANGUAGE FlexibleContexts, FlexibleInstances, MultiParamTypeClasses, 
+             PolyKinds, RankNTypes, ScopedTypeVariables, TypeFamilies #-}
+
+module Benchmarks 
+(Benchmarks.bench
+,benchIO
+,benchGroup
+,hideArgs
+,Bench(..)
+,Benchmark
+,NFData) where
+
+import Gen
+import Utils
+
+import Control.DeepSeq
+import Control.Monad.Random
+import Control.Monad.State
+import Criterion as C
+
+import Data.Proxy
+
+-- wrapper for Criterion's `nf`
+bench :: NFData b => (a -> b) -> a -> Bench params
+bench f = Bench . nf f
+
+-- wrapper for Criterion's `nfIO`
+benchIO :: NFData b => IO b -> Bench params
+benchIO = Bench . nfIO
+
+-- wrapper for Criterion's 
+benchGroup :: (Monad rnd) => String -> [rnd Benchmark] -> rnd Benchmark
+benchGroup str = (bgroup str <$>) . sequence
+
+-- normalizes any function resulting in a Benchmark to 
+-- one that takes a proxy for its arguments
+hideArgs :: (GenArgs rnd bnch, Monad rnd, ShowType a,
+             ResultOf bnch ~ Bench a)
+  => bnch -> Proxy a -> rnd Benchmark
+hideArgs f p = (C.bench (showType p) . unbench) <$> genArgs f
+
+newtype Bench params = Bench {unbench :: Benchmarkable}
+
+instance (Monad rnd) => GenArgs rnd (Bench params) where
+  type ResultOf (Bench params) = Bench params
+  genArgs = return
diff --git a/utils/Gen.hs b/utils/Gen.hs
new file mode 100644
--- /dev/null
+++ b/utils/Gen.hs
@@ -0,0 +1,27 @@
+{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, TypeFamilies #-}
+
+-- generates arguments to functions
+module Gen where
+
+import Control.Monad.Random
+
+-- bnch represents a function whose arguments can be generated,
+-- resulting in a "NFValue"
+class GenArgs rnd bnch where
+  type ResultOf bnch
+  genArgs :: bnch -> rnd (ResultOf bnch)
+
+instance (Generatable rnd a, GenArgs rnd b, 
+          Monad rnd, ResultOf b ~ ResultOf (a -> b)) 
+  => GenArgs rnd (a -> b) where
+  type ResultOf (a -> b) = ResultOf b
+  genArgs f = do
+    x <- genArg
+    genArgs $ f x
+
+-- a parameter that can be generated using a particular monad
+class Generatable rnd arg where
+  genArg :: rnd arg
+
+instance {-# Overlappable #-} (Random a, MonadRandom rnd) => Generatable rnd a where
+  genArg = getRandom
diff --git a/utils/Harness/SHE.hs b/utils/Harness/SHE.hs
new file mode 100644
--- /dev/null
+++ b/utils/Harness/SHE.hs
@@ -0,0 +1,353 @@
+{-# LANGUAGE ConstraintKinds, DataKinds, FlexibleContexts, FlexibleInstances,
+             GADTs, MultiParamTypeClasses, NoImplicitPrelude, PolyKinds, RankNTypes,
+             RebindableSyntax, ScopedTypeVariables, 
+             TypeFamilies, TypeOperators, UndecidableInstances #-}
+
+module Harness.SHE 
+(KSHint(..)
+,Tunnel(..)
+,KSLinear(..)
+,PTCT(..)
+,SKOf
+,AddZq
+,Liftable
+,NonLiftable
+,RoundDown
+
+,applyKSQ
+,applyRescale
+,applyDec
+,applyCTFunc
+,applyEnc
+,applyTunn
+,applyCTTwEm
+)where
+
+import Utils
+import Gen
+import Apply
+
+import Control.Applicative
+import Control.DeepSeq
+import Control.Monad.Random
+import Control.Monad.State
+
+import Crypto.Lol hiding (CT)
+import Crypto.Lol.Applications.SymmSHE
+import Crypto.Lol.Cyclotomic.Linear
+import Crypto.Lol.Types.ZPP
+import qualified Crypto.Lol.Cyclotomic.Tensor.CTensor as CT
+
+import Crypto.Random.DRBG
+
+import Data.Singletons
+import Data.Promotion.Prelude.List
+import Data.Promotion.Prelude.Eq
+import Data.Singletons.TypeRepStar
+
+--extract an SK type from a tuple of params
+type family SKOf (a :: k) :: * where
+  SKOf '(t,m,m',zp,zq)         = SK (Cyc t m' (LiftOf zp))
+  SKOf '(t,m,m',zp,zq,zq')     = SK (Cyc t m' (LiftOf zp))
+  SKOf '(t,m,m',zp,zq,zq',gad) = SK (Cyc t m' (LiftOf zp))
+  SKOf '(t,r,r',s,s',zp,zq)    = SK (Cyc t r' (LiftOf zp))
+  SKOf '(t,r,r',s,s',zp,zq,gad) = SK (Cyc t r' (LiftOf zp))
+  SKOf '(t,'(m,m',zp,zp',zq)) = SK (Cyc t m' (LiftOf zp))
+
+data AddZq :: TyFun (Factored, Factored, *, *) (Factored, Factored, *, *, *) -> *
+type instance Apply AddZq '(m,m',zp,zq) = '(m,m',zp,RoundDown zq,zq)
+
+data Liftable :: TyFun (Factored, Factored, *, *) Bool -> *
+type instance Apply Liftable '(m,m',zp,zq) = Int64 :== (LiftOf zq)
+
+data NonLiftable :: TyFun (Factored, Factored, *, *) Bool -> *
+type instance Apply NonLiftable '(m,m',zp,zq) = Integer :== (LiftOf zq)
+
+type family RoundDown zq where
+  RoundDown (a,(b,c)) = (b,c)
+  RoundDown ((a,b),c) = (a,b)
+  RoundDown (a,b) = a
+
+data DecCtxD
+type DecCtx t m m' zp zq = 
+  (Random zp, NFElt zp,
+   EncryptCtx t m m' (LiftOf zp) zp zq,
+   -- ^ these provide the context to generate the parameters
+   DecryptCtx t m m' (LiftOf zp) zp zq, Eq zp,
+   ShowType '(t,m,m',zp,zq))
+instance (params `Satisfy` DecCtxD, DecCtx t m m' zp zq)
+  => ( '(t, '(m,m',zp,zq)) ': params) `Satisfy` DecCtxD where
+  data ArgsCtx DecCtxD where
+    DecD :: (DecCtx t m m' zp zq) 
+      => Proxy '(t,m,m',zp,zq) -> ArgsCtx DecCtxD
+  run _ f = (f $ DecD (Proxy::Proxy '(t,m,m',zp,zq))) : (run (Proxy::Proxy params) f)
+
+applyDec :: (params `Satisfy` DecCtxD) =>
+  Proxy params ->
+  (forall t m m' zp zq . (DecCtx t m m' zp zq) 
+        => Proxy '(t,m,m',zp,zq) -> rnd res)
+     -> [rnd res]
+applyDec params g = run params $ \(DecD p) -> g p
+
+
+
+
+data TunnCtxD
+-- union of compatible constraints in benchmarks
+type TunnCtx t r r' e e' s s' zp zq gad = 
+  (NFData (CT s zp (Cyc t s' zq)),
+   ShowType '(t,r,r',s,s',zp,zq,gad),
+   EncryptCtx t r r' (LiftOf zp) zp zq,
+   EncryptCtx t s s' (LiftOf zp) zp zq,
+   TunnelCtx t e r s e' r' s' (LiftOf zp) zp zq gad, 
+   e ~ FGCD r s,
+   ZPP zp, Random zp,
+   Fact e,
+   CElt t (ZpOf zp))
+instance (params `Satisfy` TunnCtxD, TunnCtx t r r' e e' s s' zp zq gad) 
+  => ( '(gad, '(t, '( '(r,r',s,s'), '(zp,zq)))) ': params) `Satisfy` TunnCtxD where
+  data ArgsCtx TunnCtxD where
+    TunnD :: (TunnCtx t r r' e e' s s' zp zq gad) 
+      => Proxy '(t,r,r',s,s',zp,zq,gad) -> ArgsCtx TunnCtxD
+  run _ f = (f $ TunnD (Proxy::Proxy '(t,r,r',s,s',zp,zq,gad))) : (run (Proxy::Proxy params) f)
+
+applyTunn :: (params `Satisfy` TunnCtxD) =>
+  Proxy params ->
+  (forall t r r' e e' s s' zp zq gad . (TunnCtx t r r' e e' s s' zp zq gad) 
+       => Proxy '(t,r,r',s,s',zp,zq,gad) -> rnd res)
+    -> [rnd res]
+applyTunn params g = run params $ \(TunnD p) -> g p
+
+
+
+data CTEmCtxD
+-- union of compatible constraints in benchmarks
+type CTEmCtx t r r' s s' zp zq = 
+  (Random zp, Eq zp,            -- CJP: added b/c CElt doesn't have them
+   DecryptUCtx t r r' (LiftOf zp) zp zq,
+   DecryptUCtx t s s' (LiftOf zp) zp zq,
+   ShowType '(t,r,r',s,s',zp,zq),
+   EncryptCtx t r r' (LiftOf zp) zp zq,
+   r `Divides` s,
+   r' `Divides` s',
+   s `Divides` s',
+   r ~ (FGCD r' s))
+instance (params `Satisfy` CTEmCtxD, CTEmCtx t r r' s s' zp zq) 
+  => ( '(t, '(r,r',s,s',zp,zq)) ': params) `Satisfy` CTEmCtxD where
+  data ArgsCtx CTEmCtxD where
+    TwEmD :: (CTEmCtx t r r' s s' zp zq) 
+      => Proxy '(t,r,r',s,s',zp,zq) -> ArgsCtx CTEmCtxD
+  run _ f = (f $ TwEmD (Proxy::Proxy '(t,r,r',s,s',zp,zq))) : (run (Proxy::Proxy params) f)
+
+applyCTTwEm :: (params `Satisfy` CTEmCtxD, MonadRandom rnd) =>
+  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)
+    -> [rnd res]
+applyCTTwEm params g = run params $ \(TwEmD p) -> g p
+
+
+-- allowed args: CT, KSHint, SK
+-- context for (*), (==), decryptUnrestricted
+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'))) = 
+    (Random zp, Eq zp,          -- CJP: added b/c CElt doesn't have them
+     EncryptCtx t m m' (LiftOf zp) zp zq,
+     KeySwitchCtx gad t m' zp zq zq',
+     KSHintCtx gad t m' (LiftOf zp) zq',
+     -- ^ these provide the context to generate the parameters
+     Ring (CT m zp (Cyc t m' zq)), 
+     -- Eq (Cyc t m zp), 
+     Fact m, Fact m', CElt t zp, m `Divides` m',
+     Reduce (LiftOf zp) zq, Lift' zq, CElt t (LiftOf zp), ToSDCtx t m' zp zq, Reduce (LiftOf zq) zp,
+     -- ^ these provide the context for tests
+     NFData (CT m zp (Cyc t m' zq)),
+     ShowType '(t,m,m',zp,zq,zq',gad))
+     -- ^ these provide the context for benchmarks
+
+instance (params `Satisfy` KSQCtxD, KSQCtx '(gad, '(t, '(m,m',zp,zq,zq'))))
+  => ( '(gad , '(t, '(m, m', zp, zq, zq'))) ': params) `Satisfy` KSQCtxD where
+  data ArgsCtx KSQCtxD where
+    KSQD :: (KSQCtx '(gad, '(t, '(m,m',zp,zq,zq'))))
+      => Proxy '(t,m,m',zp,zq,zq',gad) -> ArgsCtx KSQCtxD
+  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'))))
+     => Proxy '(t,m,m',zp,zq,zq',gad) -> rnd res)
+  -> [rnd res]
+applyKSQ params g = run params $ \(KSQD p) -> g p
+
+
+
+
+data RescaleCtxD
+type RescaleCtx t m m' zp zq zq' = 
+  (Random zp,
+   EncryptCtx t m m' (LiftOf zp) zp zq',
+   ShowType '(t,m,m',zp,zq,zq'),
+   RescaleCyc (Cyc t) zq' zq,
+   NFData (CT m zp (Cyc t m' zq)),
+   ToSDCtx t m' zp zq')
+instance (params `Satisfy` RescaleCtxD, RescaleCtx t m m' zp zq zq') 
+  => ( '(t, '(m,m',zp,zq,zq')) ': params) `Satisfy` RescaleCtxD where
+  data ArgsCtx RescaleCtxD where
+    RD :: (RescaleCtx t m m' zp zq zq') 
+      => Proxy '(t,m,m',zp,zq,zq') -> ArgsCtx RescaleCtxD
+  run _ f = (f $ RD (Proxy::Proxy '(t,m,m',zp,zq,zq'))) : (run (Proxy::Proxy params) f)
+
+applyRescale :: (params `Satisfy` RescaleCtxD) =>
+  Proxy params ->
+  (forall t m m' zp zq zq' . (RescaleCtx t m m' zp zq zq') 
+    => Proxy '(t,m,m',zp,zq,zq') -> rnd res)
+  -> [rnd res]
+applyRescale params g = run params $ \(RD p) -> g p
+
+
+
+data CTCtxD
+-- union of compatible constraints in benchmarks
+type CTCtx t m m' zp zq = 
+  (Random zp, Eq zp, NFElt zp, NFElt zq, -- CJP: CElt doesn't have these
+   EncryptCtx t m m' (LiftOf zp) zp zq,
+   Ring (CT m zp (Cyc t m' zq)),
+   AddPublicCtx t m m' zp zq,
+   DecryptUCtx t m m' (LiftOf zp) zp zq,
+   MulPublicCtx t m m' zp zq,
+   ShowType '(t,m,m',zp,zq))
+instance (params `Satisfy` CTCtxD, CTCtx t m m' zp zq) 
+  => ( '(t, '(m,m',zp,zq)) ': params) `Satisfy` CTCtxD where
+  data ArgsCtx CTCtxD where
+    CTD :: (CTCtx t m m' zp zq) 
+      => Proxy '(t,m,m',zp,zq) -> ArgsCtx CTCtxD
+  run _ f = (f $ CTD (Proxy::Proxy '(t,m,m',zp,zq))) : (run (Proxy::Proxy params) f)
+
+applyCTFunc :: (params `Satisfy` CTCtxD, MonadRandom rnd) =>
+  Proxy params 
+  -> (forall t m m' zp zq . (CTCtx t m m' zp zq, Generatable (StateT (Maybe (SK (Cyc t m' (LiftOf zp)))) rnd) zp) 
+      => Proxy '(t,m,m',zp,zq) -> rnd res)
+  -> [rnd res]
+applyCTFunc params g = run params $ \(CTD p) -> g p
+
+
+
+
+
+data EncCtxD
+type EncCtx t m m' zp zq gen = 
+  (Random zp, NFElt zp, NFElt zq,
+   EncryptCtx t m m' (LiftOf zp) zp zq,
+   Ring (CT m zp (Cyc t m' zq)),
+   AddPublicCtx t m m' zp zq,
+   MulPublicCtx t m m' zp zq,
+   ShowType '(t,m,m',zp,zq,gen),
+   CryptoRandomGen gen)
+instance (params `Satisfy` EncCtxD, EncCtx t m m' zp zq gen) 
+  => ( '(gen, '(t, '(m,m',zp,zq))) ': params) `Satisfy` EncCtxD where
+  data ArgsCtx EncCtxD where
+    EncD :: (EncCtx t m m' zp zq gen) 
+      => Proxy '(t,m,m',zp,zq,gen) -> ArgsCtx EncCtxD
+  run _ f = (f $ EncD (Proxy::Proxy '(t,m,m',zp,zq,gen))) : (run (Proxy::Proxy params) f)
+
+applyEnc :: (params `Satisfy` EncCtxD) =>
+  Proxy params
+  -> (forall t m m' zp zq gen . (EncCtx t m m' zp zq gen) 
+      => Proxy '(t,m,m',zp,zq,gen) -> rnd res)
+  -> [rnd res]
+applyEnc params g = run params $ \(EncD p) -> g p
+
+
+
+
+
+
+-- generates a secrete key with svar=1, using non-cryptographic randomness
+instance (GenSKCtx t m z Double, 
+          MonadRandom rnd, 
+          MonadState (Maybe (SK (Cyc t m z))) rnd)
+  => Generatable rnd (SK (Cyc t m z)) where
+  genArg = do
+    msk <- get
+    sk <- case msk of
+      Just sk -> return sk
+      Nothing -> do
+        sk <- genSK (1 :: Double)
+        put $ Just sk
+        return sk
+    return sk
+
+instance (Generatable rnd (PTCT m zp (Cyc t m' zq)), Monad rnd) 
+  => Generatable rnd (CT m zp (Cyc t m' zq)) where
+  genArg = do
+    (PTCT _ ct) :: PTCT m zp (Cyc t m' zq) <- genArg
+    return ct
+
+-- use this data type in functions that need a circular key switch hint
+newtype KSHint m zp t m' zq gad zq' = KeySwitch (CT m zp (Cyc t m' zq) -> CT m zp (Cyc t m' zq))
+instance (Generatable rnd (SK (Cyc t m' z)),
+          z ~ LiftOf zp,
+          KeySwitchCtx gad t m' zp zq zq',
+          KSHintCtx gad t m' z zq', 
+          MonadRandom rnd)
+  => Generatable rnd (KSHint m zp t m' zq gad zq') where
+  genArg = do
+    sk :: SK (Cyc t m' z) <- genArg
+    KeySwitch <$> proxyT (keySwitchQuadCirc sk) (Proxy::Proxy (gad,zq'))
+
+newtype Tunnel t r r' s s' zp zq gad = Tunnel (CT r zp (Cyc t r' zq) -> CT s zp (Cyc t s' zq))
+instance (Generatable rnd (SK (Cyc t r' z)),
+          z ~ LiftOf zp,
+          TunnelCtx t e r s e' r' s' z zp zq gad, 
+          e ~ FGCD r s,
+          ZPP zp,
+          Fact e,
+          CElt t (ZpOf zp),
+          MonadRandom rnd,
+          Generatable (StateT (Maybe (SK (Cyc t s' z))) rnd) (SK (Cyc t s' z)))
+  => Generatable rnd (Tunnel t r r' s s' zp zq gad) where
+  genArg = do
+    skin :: SK (Cyc t r' z) <- genArg
+    -- EAC: bit of a hack for now
+    skout <- evalStateT genArg (Nothing :: Maybe (SK (Cyc t s' z)))
+    let crts :: [Cyc t s zp] = proxy crtSet (Proxy::Proxy e)\\ gcdDivides (Proxy::Proxy r) (Proxy::Proxy s)
+        r = proxy totientFact (Proxy::Proxy r)
+        e = proxy totientFact (Proxy::Proxy e)
+        dim = r `div` e
+        -- only take as many crts as we need
+        -- otherwise linearDec fails
+        linf :: Linear t zp e r s = linearDec (take dim crts) \\ gcdDivides (Proxy::Proxy r) (Proxy::Proxy s)
+    f <- proxyT (tunnelCT linf skout skin) (Proxy::Proxy gad)
+    return $ Tunnel f
+
+data KSLinear t m m' z zp zq (zq' :: *) (gad :: *) = KSL (CT m zp (Cyc t m' zq) -> CT m zp (Cyc t m' zq)) (SK (Cyc t m' z))
+instance (KeySwitchCtx gad t m' zp zq zq', 
+          KSHintCtx gad t m' z zq', 
+          MonadRandom rnd,
+          Generatable rnd (SK (Cyc t m' z)), -- for skin
+          Generatable (StateT (Maybe (SK (Cyc t m' z))) rnd) (SK (Cyc t m' z))) -- for skout
+  => Generatable rnd (KSLinear t m m' z zp zq zq' gad) where
+  genArg = do
+    skin <- genArg
+    -- generate an independent key
+    skout <- evalStateT genArg (Nothing :: Maybe (SK (Cyc t m' z)))
+    ksl <- proxyT (keySwitchLinear skout skin) (Proxy::Proxy (gad,zq'))
+    return $ KSL ksl skout
+
+data PTCT m zp rq where
+  PTCT :: Cyc t m zp -> CT m zp (Cyc t m' zq) -> PTCT m zp (Cyc t m' zq)
+instance (EncryptCtx t m m' z zp zq,
+          z ~ LiftOf zp,
+          MonadRandom rnd,
+          Generatable rnd (SK (Cyc t m' z)),
+          Generatable rnd (Cyc t m zp),
+          rq ~ Cyc t m' zq) 
+  => Generatable rnd (PTCT m zp rq) where
+  genArg = do
+    sk :: SK (Cyc t m' z) <- genArg
+    pt <- genArg
+    ct <- encrypt sk pt
+    return $ PTCT pt ct
diff --git a/utils/TestTypes.hs b/utils/TestTypes.hs
new file mode 100644
--- /dev/null
+++ b/utils/TestTypes.hs
@@ -0,0 +1,39 @@
+{-# LANGUAGE ConstraintKinds, DataKinds, FlexibleContexts,
+             FlexibleInstances, KindSignatures, MultiParamTypeClasses,
+             NoImplicitPrelude, PolyKinds, RankNTypes, RebindableSyntax,
+             ScopedTypeVariables, TypeFamilies, TypeOperators #-}
+
+module TestTypes (
+
+SmoothZQ1, SmoothZQ2, SmoothZQ3
+, Zq, ZQ1, ZQ2, ZQ3) where
+
+import Control.Monad
+import Control.Monad.Random
+
+import Crypto.Lol
+import Crypto.Lol.Reflects
+
+import Utils
+
+import Test.QuickCheck.Monadic
+
+instance (MonadRandom m) => MonadRandom (PropertyM m) where
+  getRandom = run getRandom
+  getRandoms = run getRandoms
+  getRandomR r = run $ getRandomR r
+  getRandomRs r = run $ getRandomRs r
+
+-- three 24-bit moduli, enough to handle rounding for p=32 (depth-4 circuit at ~17 bits per mul)
+type ZQ1 = Zq 18869761
+type ZQ2 = Zq (19393921 ** 18869761)
+type ZQ3 = Zq (19918081 ** 19393921 ** 18869761)
+
+-- the next three moduli are "good" for any index dividing 128*27*25*7
+type SmoothQ1 = 2148249601
+type SmoothQ2 = 2148854401
+type SmoothQ3 = 2150668801
+
+type SmoothZQ1 = Zq 2148249601
+type SmoothZQ2 = Zq (2148854401 ** 2148249601)
+type SmoothZQ3 = Zq (2148854401 ** 2148249601 ** 2150668801)
diff --git a/utils/Tests.hs b/utils/Tests.hs
new file mode 100644
--- /dev/null
+++ b/utils/Tests.hs
@@ -0,0 +1,49 @@
+{-# LANGUAGE FlexibleContexts, FlexibleInstances, GADTs, MultiParamTypeClasses, 
+             PolyKinds, RankNTypes, ScopedTypeVariables, TypeFamilies #-}
+module Tests
+(test
+,testIO
+,TF.testGroup
+,testGroupM
+,hideArgs
+,Test(..)) where
+
+import Gen
+import Utils
+
+import Control.Monad.Random
+import Control.Monad.State
+
+import Data.Proxy
+
+import qualified Test.Framework as TF
+import Test.Framework.Providers.QuickCheck2
+import Test.QuickCheck
+
+test :: Bool -> Test params
+test = Test
+
+testIO :: (forall m . MonadRandom m => m Bool) -> Test params
+testIO = TestM
+
+testGroupM :: String -> [IO TF.Test] -> TF.Test
+testGroupM str = TF.buildTest . (TF.testGroup str <$>) . sequence
+
+-- normalizes any function resulting in a Benchmark to 
+-- one that takes a proxy for its arguments
+hideArgs :: (GenArgs rnd bnch, MonadRandom rnd, ShowType a,
+             ResultOf bnch ~ Test a)
+  => bnch -> Proxy a -> rnd TF.Test
+hideArgs f p = do
+  res <- genArgs f
+  case res of
+    Test b -> return $ testProperty (showType p) b
+    TestM b -> testProperty (showType p) <$> b
+
+data Test params where
+  Test :: Bool -> Test params
+  TestM :: (forall m . MonadRandom m => m Bool) -> Test params
+
+instance (MonadRandom rnd) => GenArgs rnd (Test params) where
+  type ResultOf (Test params) = Test params
+  genArgs = return
diff --git a/utils/Utils.hs b/utils/Utils.hs
new file mode 100644
--- /dev/null
+++ b/utils/Utils.hs
@@ -0,0 +1,133 @@
+{-# LANGUAGE DataKinds, FlexibleContexts, FlexibleInstances, GADTs,
+             GeneralizedNewtypeDeriving, MultiParamTypeClasses, 
+             PolyKinds, RankNTypes, ConstraintKinds, ScopedTypeVariables, 
+             KindSignatures,
+             TypeFamilies, TypeOperators, UndecidableInstances #-}
+
+module Utils 
+(Zq
+,type (**)
+,type (<$>)
+,type (<*>)
+
+,module Data.Promotion.Prelude.List
+
+,showType
+,ShowType) where
+
+import Control.Monad.Random
+import Control.Monad (liftM)
+import Control.Monad.State
+
+import Control.DeepSeq
+
+import Crypto.Lol (Int64,Fact,Factored,valueFact,Mod(..), Proxy(..), proxy, Cyc, RT, CT, LiftOf, TrivGad, BaseBGad)
+import Crypto.Lol.Reflects
+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
+-- 1 mod m
+goodQs :: (Integral 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)
+-}
+
+infixr 9 **
+data a ** b
+
+type family Zq (a :: k) :: * where
+  Zq (a ** b) = (Zq a, Zq b)
+  Zq q = (ZqBasic q Int64)
+
+
+type family (f :: (k1 -> k2)) <$>  (xs :: [k1]) where
+  f <$> '[] = '[]
+  f <$> (x ': xs) = (f x) ': (f <$> xs)
+
+type family (fs :: [k1 -> k2]) <*> (xs :: [k1]) where
+  fs <*> xs = Go fs xs xs
+
+type family Go (fs :: [k1 -> k2]) (xs :: [k1]) (ys :: [k1]) where
+  Go '[] xs ys = '[]
+  Go (f ': fs) '[] ys = Go fs ys ys
+  Go (f ': fs) (x ': xs) ys = (f x) ': (Go (f ': fs) xs ys)
+
+
+
+
+
+
+
+-- a wrapper type for printing test/benchmark names
+data ArgType (a :: k) = AT
+
+-- allows automatic printing of test parameters
+type ShowType a = Show (ArgType a)
+
+showType :: forall a . (Show (ArgType a)) => Proxy a -> String
+showType _ = show (AT :: ArgType a)
+
+instance Show (ArgType HashDRBG) where
+  show _ = "HashDRBG"
+
+instance (Fact m) => Show (ArgType m) where
+  show _ = "F" ++ (show $ proxy valueFact (Proxy::Proxy m))
+
+instance (Mod (ZqBasic q i), Show i) => Show (ArgType (ZqBasic q i)) where
+  show _ = "Q" ++ (show $ proxy modulus (Proxy::Proxy (ZqBasic q i)))
+
+instance Show (ArgType RT) where
+  show _ = "RT"
+
+instance Show (ArgType CT) where
+  show _ = "CT"
+
+instance Show (ArgType Int64) where
+  show _ = "Int64"
+
+instance Show (ArgType TrivGad) where
+  show _ = "TrivGad"
+
+instance (Reflects b Integer) => Show (ArgType (BaseBGad (b :: k))) where
+  show _ = "Base" ++ (show $ (proxy value (Proxy::Proxy b) :: Integer)) ++ "Gad"
+
+-- for RNS-style moduli
+instance (Show (ArgType a), Show (ArgType b)) => Show (ArgType (a,b)) where
+  show _ = (show (AT :: ArgType a)) ++ "*" ++ (show (AT :: ArgType b))
+
+-- we use tuples rather than lists because types in a list must have the same kind,
+-- but tuples permit different kinds
+instance (Show (ArgType a), Show (ArgType b)) 
+  => Show (ArgType '(a,b)) where
+  show _ = (show (AT :: ArgType a)) ++ " " ++ (show (AT :: ArgType b))
+
+instance (Show (ArgType a), Show (ArgType '(b,c))) 
+  => Show (ArgType '(a,b,c)) where
+  show _ = (show (AT :: ArgType a)) ++ " " ++ (show (AT :: ArgType '(b,c)))
+
+instance (Show (ArgType a), Show (ArgType '(b,c,d))) 
+  => Show (ArgType '(a,b,c,d)) where
+  show _ = (show (AT :: ArgType a)) ++ " " ++ (show (AT :: ArgType '(b,c,d)))
+
+instance (Show (ArgType a), Show (ArgType '(b,c,d,e))) 
+  => Show (ArgType '(a,b,c,d,e)) where
+  show _ = (show (AT :: ArgType a)) ++ " " ++ (show (AT :: ArgType '(b,c,d,e)))
+
+instance (Show (ArgType a), Show (ArgType '(b,c,d,e,f))) 
+  => Show (ArgType '(a,b,c,d,e,f)) where
+  show _ = (show (AT :: ArgType a)) ++ " " ++ (show (AT :: ArgType '(b,c,d,e,f)))
+
+instance (Show (ArgType a), Show (ArgType '(b,c,d,e,f,g))) 
+  => Show (ArgType '(a,b,c,d,e,f,g)) where
+  show _ = (show (AT :: ArgType a)) ++ " " ++ (show (AT :: ArgType '(b,c,d,e,f,g)))
+
+instance (Show (ArgType a), Show (ArgType '(b,c,d,e,f,g,h))) 
+  => Show (ArgType '(a,b,c,d,e,f,g,h)) where
+  show _ = (show (AT :: ArgType a)) ++ " " ++ (show (AT :: ArgType '(b,c,d,e,f,g,h)))