diff --git a/CHANGES.md b/CHANGES.md
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,6 +1,11 @@
 Changelog for lol project
 ================================
 
+0.1.0.0
+-----
+ * Updated for lol-0.3.*
+ * Added simple example.
+
 0.0.0.1
 -----
  * Initial split from lol.
diff --git a/Crypto/Lol/Applications/SymmSHE.hs b/Crypto/Lol/Applications/SymmSHE.hs
--- a/Crypto/Lol/Applications/SymmSHE.hs
+++ b/Crypto/Lol/Applications/SymmSHE.hs
@@ -1,7 +1,7 @@
-{-# LANGUAGE ConstraintKinds, DataKinds,
-             FlexibleContexts, FlexibleInstances, GADTs,
-             MultiParamTypeClasses, NoImplicitPrelude, ScopedTypeVariables,
-             TypeFamilies, TypeOperators, UndecidableInstances #-}
+{-# LANGUAGE ConstraintKinds, DataKinds, FlexibleContexts,
+             FlexibleInstances, GADTs, MultiParamTypeClasses,
+             NoImplicitPrelude, ScopedTypeVariables, TypeFamilies,
+             TypeOperators, UndecidableInstances #-}
 
 -- | Symmetric-key somewhat homomorphic encryption.
 
@@ -26,7 +26,7 @@
 , GenSKCtx, EncryptCtx, ToSDCtx, ErrorTermCtx
 , DecryptCtx, DecryptUCtx
 , AddScalarCtx, AddPublicCtx, MulPublicCtx, ModSwitchPTCtx
-, SwitchCtx, KeySwitchCtx, KSHintCtx
+, KeySwitchCtx, KSHintCtx
 , TunnelCtx
 ) where
 
@@ -34,10 +34,10 @@
 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.Cyclotomic.UCyc   (D, UCyc)
 import Crypto.Lol.Gadget
-import Crypto.Lol.LatticePrelude    as LP hiding (sin)
+import Crypto.Lol.Prelude           as LP hiding (sin)
 
 import Control.Applicative  hiding ((*>))
 import Control.DeepSeq
@@ -117,12 +117,12 @@
          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' :: (Fact m, CElt t r, IntegralDomain 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,
+  (ErrorTermCtx t m' z zp zq, Reduce (LiftOf zq) zp, IntegralDomain zp,
    m `Divides` m', CElt t zp)
 
 -- | Decrypt a ciphertext.
@@ -134,15 +134,15 @@
      in (scalarCyc l) * twace (iterate divG' e !! k)
 
 --- unrestricted versions ---
-
+-- | Constraint synonym for unrestricted decryption.
 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)
+   Reduce z zq, Lift' zq, CElt t z,
+   ToSDCtx t m' zp zq, Reduce (LiftOf zq) zp, IntegralDomain zp)
 
 -- | More general form of 'errorTerm' that works for unrestricted
 -- output coefficient types.
-errorTermUnrestricted :: 
+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
@@ -228,15 +228,15 @@
 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 
+  -- 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 = 
+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))
 
@@ -264,7 +264,7 @@
 -- adviseCRT here because we map (x *) onto each polynomial coeff
 knapsack hint xs = sum $ zipWith (*>>) (adviseCRT <$> xs) hint
 
-type SwitchCtx gad t m' zq = 
+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.
@@ -277,7 +277,7 @@
   (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_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
@@ -306,7 +306,7 @@
     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)
 
@@ -322,7 +322,7 @@
       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
+-- | 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)
@@ -337,7 +337,7 @@
       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
+-- | 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)
@@ -394,8 +394,8 @@
 ---------- 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)
+  (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
@@ -449,6 +449,7 @@
    KSHintCtx gad t r' z zq,         -- ksHint
    Reduce z zq,                     -- Reduce on Linear
    Lift zp z,                       -- liftLin
+   IntegralDomain zp,               -- absorbGFactors
    CElt t zp,                       -- liftLin
    SwitchCtx gad t s' zq)           -- switch
 
diff --git a/Setup.hs b/Setup.hs
deleted file mode 100644
--- a/Setup.hs
+++ /dev/null
@@ -1,2 +0,0 @@
-import Distribution.Simple
-main = defaultMain
diff --git a/benchmarks/Main.hs b/benchmarks/Main.hs
--- a/benchmarks/Main.hs
+++ b/benchmarks/Main.hs
@@ -2,9 +2,8 @@
 import SHEBenches
 
 import Criterion.Main
-import Control.Monad
 
 main :: IO ()
-main = defaultMain =<< (sequence [
+main = defaultMain =<< sequence [
   sheBenches
-  ])
+  ]
diff --git a/benchmarks/SHEBenches.hs b/benchmarks/SHEBenches.hs
--- a/benchmarks/SHEBenches.hs
+++ b/benchmarks/SHEBenches.hs
@@ -1,14 +1,15 @@
-{-# LANGUAGE DataKinds, FlexibleContexts, 
-             NoImplicitPrelude, PolyKinds, RebindableSyntax, 
-             ScopedTypeVariables, TypeFamilies, 
+{-# LANGUAGE DataKinds, FlexibleContexts,
+             NoImplicitPrelude, PolyKinds, RebindableSyntax,
+             ScopedTypeVariables, TypeFamilies,
              TypeOperators #-}
 
 module SHEBenches (sheBenches) where
 
-import Gen
-import Utils
-import Harness.SHE
+import Apply.SHE
 import Benchmarks hiding (hideArgs)
+import GenArgs
+import GenArgs.SHE
+import Utils
 
 import Control.Applicative
 import Control.Monad.Random
@@ -22,24 +23,24 @@
 
 import qualified Criterion as C
 
-hideArgs :: forall a rnd bnch . 
+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) <$> 
+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
+  benchGroup "encrypt"   $ applyEnc encParams         $ hideArgs bench_enc,
+  benchGroup "decrypt"   $ applyDec decParams         $ hideArgs bench_dec,
+  benchGroup "*"         $ applyCTFunc ctParams       $ hideArgs bench_mul,
+  benchGroup "addPublic" $ applyCTFunc ctParams       $ hideArgs bench_addPublic,
+  benchGroup "mulPublic" $ applyCTFunc ctParams       $ hideArgs bench_mulPublic,
+  benchGroup "dec"       $ applyDec decParams         $ hideArgs bench_dec,
+  benchGroup "rescaleCT" $ applyRescale rescaleParams $ hideArgs bench_rescaleCT,
+  benchGroup "keySwitch" $ applyKSQ ksqParams         $ hideArgs bench_keySwQ,
+  benchGroup "tunnel"    $ applyTunn tunnelParams     $ 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)
@@ -59,27 +60,27 @@
 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, 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' . 
+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))) 
+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))) 
+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 = 
+type MM'PQCombos =
   '[ '(F4, F128, Zq 64, Zq 257),
      '(F4, F128, Zq 64, Zq (257 ** 641)),
      '(F12, F32 * F9, Zq 64, Zq 577),
@@ -95,17 +96,32 @@
     ]
 
 type CTParams  = ( '(,) <$> Tensors) <*> MM'PQCombos
+ctParams :: Proxy CTParams
+ctParams = Proxy
+
 type DecParams = ( '(,) <$> Tensors) <*> (Nub (Filter Liftable MM'PQCombos))
+decParams :: Proxy DecParams
+decParams = Proxy
+
 type RescaleParams = ( '(,) <$> Tensors) <*> (Map AddZq (Filter NonLiftable MM'PQCombos))
+rescaleParams :: Proxy RescaleParams
+rescaleParams = Proxy
+
 type KSQParams = ( '(,) <$> Gadgets) <*> RescaleParams
+ksqParams :: Proxy KSQParams
+ksqParams = Proxy
+
 type EncParams = ( '(,) <$> Gens) <*> CTParams
+encParams :: Proxy EncParams
+encParams = Proxy
 
 -- 3144961,5241601,7338241,9959041,10483201,11531521,12579841,15200641,18869761,19393921
-type TunnParams = 
-  ( '(,) <$> Gadgets) <*> 
-  (( '(,) <$> Tensors) <*> 
+type TunnParams =
+  ( '(,) <$> Gadgets) <*>
+  (( '(,) <$> Tensors) <*>
   (( '(,) <$> TunnRings) <*> TunnMods))
-
+tunnelParams :: Proxy TunnParams
+tunnelParams = Proxy
 
 type TunnRings = '[
   {- H0 -> H1 -} '(F128, F128 * F7 * F13, F64 * F7, F64 * F7 * F13),
diff --git a/examples/SymmSHE/SimpleSHE.hs b/examples/SymmSHE/SimpleSHE.hs
new file mode 100644
--- /dev/null
+++ b/examples/SymmSHE/SimpleSHE.hs
@@ -0,0 +1,82 @@
+{-# 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
+     #-}
+
+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)
+
+-- 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)
+
+-- 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.
+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
+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 KSGad = TrivGad -- can also use (BaseBGad 2), for example
+
+type PTRing = Cyc T PTIndex PTZq
+type CTRing1 = CT PTIndex PTZq (Cyc T CTIndex CTZq1)
+type CTRing2 = CT PTIndex PTZq (Cyc T CTIndex CTZq2)
+type SKRing = Cyc T CTIndex (LiftOf PTZq)
+
+main :: IO ()
+main = do
+  plaintext <- getRandom
+  sk :: SK SKRing <- genSK (1 :: Double)
+  -- encrypt with a single modulus
+  ciphertext :: CTRing1 <- encrypt sk plaintext
+
+  let ct1 = 2*ciphertext
+      pt1 = decrypt sk ct1
+  print $ "Test1: " ++ (show $ 2*plaintext == pt1)
+
+  kswq <- proxyT (keySwitchQuadCirc sk) (Proxy::Proxy (KSGad, CTZq2))
+  let ct2 = kswq $ ciphertext*ciphertext
+      pt2 = decrypt sk ct2
+  -- note: this requires a *LARGE* CT modulus to succeed
+  print $ "Test2: " ++ (show $ plaintext*plaintext == pt2)
+
+  -- so we support using *several* small moduli:
+  kswq' <- proxyT (keySwitchQuadCirc sk) (Proxy::Proxy (KSGad, CTZq3))
+  ciphertext' :: CTRing2 <- encrypt sk plaintext
+  let ct3 = kswq' $ ciphertext' * ciphertext'
+      -- the CT modulus of ct3 is a ring product, which can't be lifted to a fixed size repr
+      -- so use decryptUnrestricted instead
+      pt3 = decryptUnrestricted sk ct3
+      ct3' = rescaleLinearCT ct3 :: CTRing1
+      -- after rescaling, ct3' has a single modulus, so we can use normal decrypt
+      pt3' = decrypt sk ct3'
+  print $ "Test3: " ++ (show $ (plaintext*plaintext == pt3) && (pt3' == pt3))
+
diff --git a/lol-apps.cabal b/lol-apps.cabal
--- a/lol-apps.cabal
+++ b/lol-apps.cabal
@@ -1,12 +1,12 @@
 name:                lol-apps
--- The package version.  See the Haskell package versioning policy (PVP) 
+-- 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 Λ ○ λ>.
+version:             0.1.0.0
+synopsis:            Lattice-based cryptographic applications using Lol.
 homepage:            https://github.com/cpeikert/Lol
 Bug-Reports:         https://github.com/cpeikert/Lol/issues
 license:             GPL-2
@@ -21,16 +21,17 @@
                      benchmarks/SHEBenches.hs,
                      tests/SHETests.hs,
                      utils/Apply.hs,
+                     utils/Apply/SHE.hs
                      utils/Benchmarks.hs,
-                     utils/Gen.hs,
+                     utils/GenArgs.hs,
+                     utils/GenArgs/SHE.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), 
+    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
@@ -41,7 +42,7 @@
   Description:  Compile via LLVM. This produces much better object code,
                 but you need to have the LLVM compiler installed.
 
-  Default:      True
+  Default:      False
 
 Flag opt
   Description: Turn on library optimizations
@@ -56,24 +57,24 @@
 
   -- ghc optimizations
   if flag(opt)
-    ghc-options: -O3 -Odph -funbox-strict-fields -fwarn-dodgy-imports -rtsopts
+    ghc-options: -O3 -Odph -funbox-strict-fields -fwarn-dodgy-imports
     ghc-options: -fno-liberate-case -funfolding-use-threshold1000 -funfolding-keeness-factor1000
 
-  exposed-modules: 
+  exposed-modules:
     Crypto.Lol.Applications.SymmSHE
 
   build-depends:
     base==4.8.*,
     deepseq >= 1.4.1.1 && <1.5,
-    lol == 0.2.0.0,
+    lol == 0.3.*,
     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
+  type:             exitcode-stdio-1.0
+  hs-source-dirs:   tests,utils
+  default-language: Haskell2010
+  main-is:          Main.hs
 
   ghc-options: -threaded -rtsopts
 
@@ -95,10 +96,10 @@
     vector
 
 Benchmark bench-apps
-  type:               exitcode-stdio-1.0
-  hs-source-dirs:     benchmarks,utils
-  default-language:   Haskell2010
-  main-is:            Main.hs
+  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
@@ -118,5 +119,18 @@
     singletons,
     transformers,
     vector,
-    repa                        
+    repa
 
+executable simpleSHE
+  hs-source-dirs:   examples/SymmSHE
+  default-language: Haskell2010
+  main-is:          SimpleSHE.hs
+
+  ghc-options: -threaded -rtsopts
+
+  build-depends:
+    arithmoi,
+    lol,
+    lol-apps,
+    MonadRandom,
+    numeric-prelude
diff --git a/tests/SHETests.hs b/tests/SHETests.hs
--- a/tests/SHETests.hs
+++ b/tests/SHETests.hs
@@ -4,8 +4,9 @@
 
 module SHETests (sheTests) where
 
-import Gen
-import Harness.SHE
+import Apply.SHE
+import GenArgs
+import GenArgs.SHE
 import Tests hiding (hideArgs)
 import Utils
 
@@ -21,12 +22,12 @@
 
 import qualified Test.Framework as TF
 import Test.Framework.Providers.QuickCheck2
-import Test.QuickCheck
 
-v = 1 :: Double
+v :: Double
+v = 1
 
-hideArgs :: forall a rnd bnch. 
-  (GenArgs (StateT (Maybe (SKOf a)) rnd) bnch, MonadRandom rnd, 
+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
@@ -35,22 +36,23 @@
     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,
+sheTests :: [TF.Test]
+sheTests =
+  [testGroupM "Dec . Enc"  $ applyDec decParams $ hideArgs prop_encDec,
+   testGroupM "DecU . Enc" $ applyCTFunc ctParams $ hideArgs prop_encDecU,
+   testGroupM "AddPub"     $ applyCTFunc ctParams $ hideArgs prop_addPub,
+   testGroupM "MulPub"     $ applyCTFunc ctParams $ hideArgs prop_mulPub,
+   testGroupM "ScalarPub"  $ applyCTFunc ctParams $ hideArgs prop_addScalar,
+   testGroupM "CTAdd"      $ applyCTFunc ctParams $ hideArgs prop_ctadd,
+   testGroupM "CTMul"      $ applyCTFunc ctParams $ hideArgs prop_ctmul,
+   testGroupM "CT zero"    $ applyCTFunc ctParams $ hideArgs prop_ctzero,
+   testGroupM "CT one"     $ applyCTFunc 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
+   testGroupM "Twace"      $ applyCTTwEm twoIdxParams $ hideArgs prop_cttwace,
+   testGroupM "Embed"      $ applyCTTwEm twoIdxParams $ hideArgs prop_ctembed,
+   testGroupM "KSLin"      $ applyKSQ ksqParams $ hideArgs prop_ksLin,
+   testGroupM "keySwitch"  $ applyKSQ ksqParams $ hideArgs prop_ksQuad
   ]
 
 type CTCombos = '[
@@ -74,7 +76,7 @@
 
 type Gadgets = '[TrivGad, BaseBGad 2]
 type Tensors = '[CT.CT,RT]
-type MM'PQCombos = 
+type MM'PQCombos =
   '[ '(F1, F7, Zq 2, Zq (19393921 ** 18869761)),
      '(F2, F4, Zq 8, Zq (2148854401 ** 2148249601)),
      '(F4, F12, Zq 2, Zq (2148854401 ** 2148249601)),
@@ -87,44 +89,54 @@
 
 
 type CTParams  = ( '(,) <$> Tensors) <*> CTCombos
+ctParams :: Proxy CTParams
+ctParams = Proxy
+
 type DecParams = ( '(,) <$> Tensors) <*> (Nub (Filter Liftable CTCombos))
+decParams :: Proxy DecParams
+decParams = Proxy
+
 type Zq'Params = ( '(,) <$> Tensors) <*> (Map AddZq (Filter NonLiftable MM'PQCombos))
 type KSQParams = ( '(,) <$> Gadgets) <*> Zq'Params
+ksqParams :: Proxy KSQParams
+ksqParams = Proxy
+
 type TwoIdxParams = ( '(,) <$> Tensors) <*> '[ '(F1, F7, F3, F21, Zq 2, Zq 18869761)]
+twoIdxParams :: Proxy TwoIdxParams
+twoIdxParams = Proxy
 
 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) 
+  => 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) =
+prop_ksLin (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, 
+                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' 
+  => 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) = 
+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 . 
+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) 
+  => 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) = 
+prop_addPub sk x (PTCT y' y) =
   let xy = addPublic x y
       xy' = decryptUnrestricted sk xy
   in test $ xy' == (x+y')
@@ -132,11 +144,11 @@
 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 
+  => 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) = 
+prop_mulPub sk x (PTCT y' y) =
   let xy = mulPublic x y
       xy' = decryptUnrestricted sk xy
   in test $ xy' == (x*y')
@@ -153,11 +165,11 @@
 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) 
+  => 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) = 
+prop_ctadd sk (PTCT x1' x1) (PTCT x2' x2) =
   let y = x1+x2
       y' = decryptUnrestricted sk y
   in test $ x1'+x2' == y'
@@ -165,11 +177,11 @@
 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) 
+  => 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) = 
+prop_ctmul sk (PTCT x1' x1) (PTCT x2' x2) =
   let y = x1*x2
       y' = decryptUnrestricted sk y
   in test $ x1'*x2' == y'
@@ -177,7 +189,7 @@
 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)) 
+  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))
@@ -188,28 +200,28 @@
    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 = 
+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 . 
+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` 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) = 
+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 . 
+prop_cttwace :: forall t r r' s s' z zp zq .
   (Eq zp,
-   EncryptCtx t s s' z zp zq, 
+   EncryptCtx t s s' z zp zq,
    DecryptUCtx t r r' z zp zq,
    r `Divides` s,
    r' `Divides` s',
@@ -222,9 +234,9 @@
       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, 
+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)
@@ -233,9 +245,9 @@
   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, 
+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)
@@ -256,7 +268,7 @@
    RescaleCyc (Cyc t) zp zp',
    Ring (Cyc t m zp),
    Mod zp, Mod zp',
-   ModRep zp ~ ModRep 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)
@@ -267,27 +279,26 @@
       x'' = decryptUnrestricted sk y'
   in test $ x'' == rescaleCyc Dec x
 
+modSwPTTests :: [IO TF.Test]
 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)))]
-
+ 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' p = 
-  [helper (hideArgs prop_ringTunnel) p 
-    (Proxy::Proxy '(F8,F40,F20,F60,Zq 4,Zq (18869761 ** 19393921),TrivGad))]
+  where 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 . 
+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) 
+   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)
@@ -295,7 +306,7 @@
       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 
+  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
diff --git a/utils/Apply.hs b/utils/Apply.hs
--- a/utils/Apply.hs
+++ b/utils/Apply.hs
@@ -1,17 +1,17 @@
-{-# LANGUAGE DataKinds, FlexibleInstances, MultiParamTypeClasses, PolyKinds, 
+{-# LANGUAGE DataKinds, FlexibleInstances, MultiParamTypeClasses, PolyKinds,
              TypeFamilies, TypeOperators #-}
 
 -- applies functions to proxy arguments
 module Apply where
 
-class (params :: [k]) `Satisfy` (ctx :: *)  where
-  data ArgsCtx ctx
+-- not associated due to the generic instance below:
+-- any definition of ArgsCtx would conflict with specific instances
+data family ArgsCtx ctx
 
+class (params :: [k]) `Satisfy` (ctx :: *)  where
   run :: proxy params
-            -> (ArgsCtx ctx -> rnd res) 
+            -> (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/Apply/SHE.hs b/utils/Apply/SHE.hs
new file mode 100644
--- /dev/null
+++ b/utils/Apply/SHE.hs
@@ -0,0 +1,236 @@
+{-# LANGUAGE ConstraintKinds       #-}
+{-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE NoImplicitPrelude     #-}
+{-# LANGUAGE PolyKinds             #-}
+{-# LANGUAGE RankNTypes            #-}
+{-# LANGUAGE RebindableSyntax      #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE TypeFamilies          #-}
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE UndecidableInstances  #-}
+
+module Apply.SHE
+(AddZq
+,Liftable
+,NonLiftable
+,RoundDown
+,applyKSQ
+,applyRescale
+,applyDec
+,applyCTFunc
+,applyEnc
+,applyTunn
+,applyCTTwEm
+) where
+
+import Apply
+import GenArgs
+import Utils
+
+import Control.DeepSeq
+import Control.Monad.Random
+import Control.Monad.State
+
+import Crypto.Lol                      hiding (CT)
+import Crypto.Lol.Applications.SymmSHE
+import Crypto.Lol.Types.ZPP
+
+import Crypto.Random.DRBG
+
+import Data.Promotion.Prelude.Eq
+import Data.Singletons
+import Data.Singletons.TypeRepStar ()
+
+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))
+data instance ArgsCtx DecCtxD where
+    DecD :: (DecCtx t m m' zp zq) => Proxy '(t,m,m',zp,zq) -> ArgsCtx DecCtxD
+instance (params `Satisfy` DecCtxD, DecCtx t m m' zp zq)
+  => ( '(t, '(m,m',zp,zq)) ': params) `Satisfy` DecCtxD where
+  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))
+data instance 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
+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
+  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))
+data instance ArgsCtx CTEmCtxD where
+    TwEmD :: (CTEmCtx t r r' s s' zp zq)
+      => Proxy '(t,r,r',s,s',zp,zq) -> ArgsCtx CTEmCtxD
+instance (params `Satisfy` CTEmCtxD, CTEmCtx t r r' s s' zp zq)
+  => ( '(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) =>
+  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,
+     DecryptUCtx 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
+data instance ArgsCtx KSQCtxD where
+    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'))))
+  => ( '(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'))))
+     => 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')
+data instance ArgsCtx RescaleCtxD where
+    RD :: (RescaleCtx t m m' zp zq zq')
+      => Proxy '(t,m,m',zp,zq,zq') -> ArgsCtx RescaleCtxD
+instance (params `Satisfy` RescaleCtxD, RescaleCtx t m m' zp zq zq')
+  => ( '(t, '(m,m',zp,zq,zq')) ': params) `Satisfy` RescaleCtxD where
+  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))
+data instance ArgsCtx CTCtxD where
+    CTD :: (CTCtx t m m' zp zq)
+      => Proxy '(t,m,m',zp,zq) -> ArgsCtx CTCtxD
+instance (params `Satisfy` CTCtxD, CTCtx t m m' zp zq)
+  => ( '(t, '(m,m',zp,zq)) ': params) `Satisfy` CTCtxD where
+  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)
+data instance ArgsCtx EncCtxD where
+    EncD :: (EncCtx t m m' zp zq gen)
+      => Proxy '(t,m,m',zp,zq,gen) -> ArgsCtx EncCtxD
+instance (params `Satisfy` EncCtxD, EncCtx t m m' zp zq gen)
+  => ( '(gen, '(t, '(m,m',zp,zq))) ': params) `Satisfy` EncCtxD where
+  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
diff --git a/utils/Benchmarks.hs b/utils/Benchmarks.hs
--- a/utils/Benchmarks.hs
+++ b/utils/Benchmarks.hs
@@ -1,7 +1,7 @@
-{-# LANGUAGE FlexibleContexts, FlexibleInstances, MultiParamTypeClasses, 
+{-# LANGUAGE FlexibleContexts, FlexibleInstances, MultiParamTypeClasses,
              PolyKinds, RankNTypes, ScopedTypeVariables, TypeFamilies #-}
 
-module Benchmarks 
+module Benchmarks
 (Benchmarks.bench
 ,benchIO
 ,benchGroup
@@ -10,12 +10,10 @@
 ,Benchmark
 ,NFData) where
 
-import Gen
+import GenArgs
 import Utils
 
 import Control.DeepSeq
-import Control.Monad.Random
-import Control.Monad.State
 import Criterion as C
 
 import Data.Proxy
@@ -28,11 +26,11 @@
 benchIO :: NFData b => IO b -> Bench params
 benchIO = Bench . nfIO
 
--- wrapper for Criterion's 
+-- 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 
+-- 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)
diff --git a/utils/Gen.hs b/utils/Gen.hs
deleted file mode 100644
--- a/utils/Gen.hs
+++ /dev/null
@@ -1,27 +0,0 @@
-{-# 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/GenArgs.hs b/utils/GenArgs.hs
new file mode 100644
--- /dev/null
+++ b/utils/GenArgs.hs
@@ -0,0 +1,31 @@
+{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, TypeFamilies #-}
+
+-- generates arguments to functions
+module GenArgs where
+
+import Control.Monad.Random
+import Data.Proxy
+
+-- 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
+
+instance (Monad rnd) => Generatable rnd (Proxy a) where
+  genArg = return Proxy
diff --git a/utils/GenArgs/SHE.hs b/utils/GenArgs/SHE.hs
new file mode 100644
--- /dev/null
+++ b/utils/GenArgs/SHE.hs
@@ -0,0 +1,111 @@
+{-# LANGUAGE DataKinds, FlexibleContexts, FlexibleInstances, GADTs,
+             MultiParamTypeClasses, NoImplicitPrelude, PolyKinds,
+             RebindableSyntax, ScopedTypeVariables, TypeFamilies,
+             UndecidableInstances #-}
+
+module GenArgs.SHE where
+
+import GenArgs
+
+import Control.Applicative
+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
+
+--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))
+
+-- 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
+    case msk of
+      Just sk -> return sk
+      Nothing -> do
+        sk <- genSK (1 :: Double)
+        put $ Just 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)
+    Tunnel <$> proxyT (tunnelCT linf skout skin) (Proxy::Proxy gad)
+
+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/Harness/SHE.hs b/utils/Harness/SHE.hs
deleted file mode 100644
--- a/utils/Harness/SHE.hs
+++ /dev/null
@@ -1,353 +0,0 @@
-{-# 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
--- a/utils/TestTypes.hs
+++ b/utils/TestTypes.hs
@@ -1,18 +1,17 @@
 {-# LANGUAGE ConstraintKinds, DataKinds, FlexibleContexts,
-             FlexibleInstances, KindSignatures, MultiParamTypeClasses,
+             FlexibleInstances, MultiParamTypeClasses,
              NoImplicitPrelude, PolyKinds, RankNTypes, RebindableSyntax,
              ScopedTypeVariables, TypeFamilies, TypeOperators #-}
 
-module TestTypes (
-
-SmoothZQ1, SmoothZQ2, SmoothZQ3
-, Zq, ZQ1, ZQ2, ZQ3) where
+module TestTypes
+(SmoothQ1, SmoothQ2, SmoothQ3
+,SmoothZQ1, SmoothZQ2, SmoothZQ3
+,Zq
+,ZQ1,ZQ2,ZQ3) where
 
-import Control.Monad
 import Control.Monad.Random
 
 import Crypto.Lol
-import Crypto.Lol.Reflects
 
 import Utils
 
diff --git a/utils/Tests.hs b/utils/Tests.hs
--- a/utils/Tests.hs
+++ b/utils/Tests.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE FlexibleContexts, FlexibleInstances, GADTs, MultiParamTypeClasses, 
+{-# LANGUAGE FlexibleContexts, FlexibleInstances, GADTs, MultiParamTypeClasses,
              PolyKinds, RankNTypes, ScopedTypeVariables, TypeFamilies #-}
 module Tests
 (test
@@ -8,17 +8,15 @@
 ,hideArgs
 ,Test(..)) where
 
-import Gen
+import GenArgs
 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
@@ -29,7 +27,7 @@
 testGroupM :: String -> [IO TF.Test] -> TF.Test
 testGroupM str = TF.buildTest . (TF.testGroup str <$>) . sequence
 
--- normalizes any function resulting in a Benchmark to 
+-- 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)
diff --git a/utils/Utils.hs b/utils/Utils.hs
--- a/utils/Utils.hs
+++ b/utils/Utils.hs
@@ -1,10 +1,9 @@
-{-# LANGUAGE DataKinds, FlexibleContexts, FlexibleInstances, GADTs,
-             GeneralizedNewtypeDeriving, MultiParamTypeClasses, 
-             PolyKinds, RankNTypes, ConstraintKinds, ScopedTypeVariables, 
-             KindSignatures,
-             TypeFamilies, TypeOperators, UndecidableInstances #-}
+{-# LANGUAGE ConstraintKinds, DataKinds, FlexibleContexts, FlexibleInstances,
+             GADTs, KindSignatures, MultiParamTypeClasses, PolyKinds,
+             RankNTypes, ScopedTypeVariables, TypeFamilies, TypeOperators,
+             UndecidableInstances #-}
 
-module Utils 
+module Utils
 (Zq
 ,type (**)
 ,type (<$>)
@@ -15,13 +14,7 @@
 ,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 (Int64,Fact,valueFact,Mod(..), Proxy(..), proxy, RT, CT, TrivGad, BaseBGad)
 import Crypto.Lol.Reflects
 import Crypto.Lol.Types.ZqBasic
 import Crypto.Random.DRBG
@@ -78,10 +71,10 @@
   show _ = "HashDRBG"
 
 instance (Fact m) => Show (ArgType m) where
-  show _ = "F" ++ (show $ proxy valueFact (Proxy::Proxy m))
+  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)))
+  show _ = "Q" ++ show (proxy modulus (Proxy::Proxy (ZqBasic q i)))
 
 instance Show (ArgType RT) where
   show _ = "RT"
@@ -96,38 +89,38 @@
   show _ = "TrivGad"
 
 instance (Reflects b Integer) => Show (ArgType (BaseBGad (b :: k))) where
-  show _ = "Base" ++ (show $ (proxy value (Proxy::Proxy b) :: Integer)) ++ "Gad"
+  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))
+  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)) 
+instance (Show (ArgType a), Show (ArgType b))
   => Show (ArgType '(a,b)) where
-  show _ = (show (AT :: ArgType a)) ++ " " ++ (show (AT :: ArgType b))
+  show _ = show (AT :: ArgType a) ++ " " ++ show (AT :: ArgType b)
 
-instance (Show (ArgType a), Show (ArgType '(b,c))) 
+instance (Show (ArgType a), Show (ArgType '(b,c)))
   => Show (ArgType '(a,b,c)) where
-  show _ = (show (AT :: ArgType a)) ++ " " ++ (show (AT :: ArgType '(b,c)))
+  show _ = show (AT :: ArgType a) ++ " " ++ show (AT :: ArgType '(b,c))
 
-instance (Show (ArgType a), Show (ArgType '(b,c,d))) 
+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)))
+  show _ = show (AT :: ArgType a) ++ " " ++ show (AT :: ArgType '(b,c,d))
 
-instance (Show (ArgType a), Show (ArgType '(b,c,d,e))) 
+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)))
+  show _ = show (AT :: ArgType a) ++ " " ++ show (AT :: ArgType '(b,c,d,e))
 
-instance (Show (ArgType a), Show (ArgType '(b,c,d,e,f))) 
+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)))
+  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))) 
+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)))
+  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))) 
+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)))
+  show _ = show (AT :: ArgType a) ++ " " ++ show (AT :: ArgType '(b,c,d,e,f,g,h))