{-# LANGUAGE DataKinds             #-}
# LANGUAGE MultiParamTypeClasses #
# LANGUAGE TypeFamilies           #
{-# LANGUAGE TypeOperators         #-}

module Crypto.Alchemy.Language.BGV where

import Crypto.Lol                      (Factored)
import Crypto.Lol.Applications.SymmBGV 
import GHC.Exts
import GHC.TypeLits

-- | Symantics for somewhat-homomorphic encryption operations (not
-- including those defined in 'Crypto.Alchemy.Language.Arithmetic').

class BGV_ expr where

  type ModSwitchPTCtx_   expr (c :: Factored -> * -> *)
    (m :: Factored) (m' :: Factored) zp zp' zq :: Constraint
  type ModSwitchCtx_     expr (c :: Factored -> * -> *)
    (m :: Factored) (m' :: Factored) zp zq zq' :: Constraint
  type AddPublicCtx_     expr (c :: Factored -> * -> *)
    (m :: Factored) (m' :: Factored) zp zq :: Constraint
  type MulPublicCtx_     expr (c :: Factored -> * -> *)
    (m :: Factored) (m' :: Factored) zp zq :: Constraint
  type KeySwitchQuadCtx_ expr (c :: Factored -> * -> *)
    (m :: Factored) (m' :: Factored) zp zq gad :: Constraint
  type AddCTCtx_         expr (c :: Factored -> * -> *)
    (m :: Factored) (m' :: Factored) zp zq :: Constraint
  type NegateCTCtx_      expr (c :: Factored -> * -> *) 
    (m :: Factored) (m' :: Factored) zp zq :: Constraint
  type MulCTCtx_         expr (c :: Factored -> * -> *)
    (m :: Factored) (m' :: Factored) zp zq :: Constraint
  type TunnelCtx_        expr (c  :: Factored -> * -> *)
    (e  :: Factored) (r  :: Factored) (s  :: Factored)
    (e' :: Factored) (r' :: Factored) (s' :: Factored) zp zq gad :: Constraint


  modSwitchPT_ :: (ModSwitchPTCtx_ expr c m m' zp zp' zq)
    => expr env (CT d m zp (c m' zq) -> CT d m zp' (c m' zq))

  modSwitch_ :: (ModSwitchCtx_ expr c m m' zp zq zq')
    => expr env (CT d m zp (c m' zq) -> CT d m zp (c m' zq'))

  addPublic_ :: (AddPublicCtx_ expr c m m' zp zq)
    => c m zp -> expr env (CT d m zp (c m' zq) -> CT d m zp (c m' zq))

  mulPublic_ :: (MulPublicCtx_ expr c m m' zp zq)
    => c m zp -> expr env (CT d m zp (c m' zq) -> CT d m zp (c m' zq))

  keySwitchQuad_ :: (KeySwitchQuadCtx_ expr c m m' zp zq gad)
    => KSHint gad (c m' zq) -> expr env (CT 2 m zp (c m' zq) -> CT 1 m zp (c m' zq))

  addCT_ :: AddCTCtx_ expr c m m' zp zq
    => expr env (CT d1 m zp (c m' zq) -> CT d2 m zp (c m' zq) -> CT (Max d1 d2) m zp (c m' zq))

  negateCT_ :: NegateCTCtx_ expr c m m' zp zq
    => expr env (CT d m zp (c m' zq) -> CT d m zp (c m' zq))

  mulCT_ :: MulCTCtx_ expr c m m' zp zq 
    => expr env (CT d1 m zp (c m' zq) -> CT d2 m zp (c m' zq) -> CT (d1 + d2) m zp (c m' zq))

  tunnel_ :: (TunnelCtx_ expr c e r s e' r' s' zp zq gad)
    => TunnelHint gad c e r s e' r' s' zp zq
    -> expr env (CT d r zp (c r' zq) -> CT d s zp (c s' zq))



-- | Symantics for obtaining the error rate of a ciphertext.

class ErrorRate_ expr where

  type ErrorRateCtx_ expr (c :: Factored -> * -> *)
    (m :: Factored) (m' :: Factored) zp zq z :: Constraint

  -- | Error rate of a ciphertext.  (Note that the secret key lives
  -- "outside" the object language.)
  errorRate_ :: (ErrorRateCtx_ expr c m m' zp zq z)
             => SK (c m' z) -> expr e (CT d m zp (c m' zq) -> Double)

# LANGUAGE DataKinds             #
# LANGUAGE TypeOperators         #
 | Symantics for somewhat-homomorphic encryption operations (not
 including those defined in 'Crypto.Alchemy.Language.Arithmetic').
 | Symantics for obtaining the error rate of a ciphertext.
 | Error rate of a ciphertext.  (Note that the secret key lives
 "outside" the object language.)
# LANGUAGE MultiParamTypeClasses #
# LANGUAGE TypeFamilies           #

module Crypto.Alchemy.Language.BGV where

import Crypto.Lol                      (Factored)
import Crypto.Lol.Applications.SymmBGV 
import GHC.Exts
import GHC.TypeLits


class BGV_ expr where

  type ModSwitchPTCtx_   expr (c :: Factored -> * -> *)
    (m :: Factored) (m' :: Factored) zp zp' zq :: Constraint
  type ModSwitchCtx_     expr (c :: Factored -> * -> *)
    (m :: Factored) (m' :: Factored) zp zq zq' :: Constraint
  type AddPublicCtx_     expr (c :: Factored -> * -> *)
    (m :: Factored) (m' :: Factored) zp zq :: Constraint
  type MulPublicCtx_     expr (c :: Factored -> * -> *)
    (m :: Factored) (m' :: Factored) zp zq :: Constraint
  type KeySwitchQuadCtx_ expr (c :: Factored -> * -> *)
    (m :: Factored) (m' :: Factored) zp zq gad :: Constraint
  type AddCTCtx_         expr (c :: Factored -> * -> *)
    (m :: Factored) (m' :: Factored) zp zq :: Constraint
  type NegateCTCtx_      expr (c :: Factored -> * -> *) 
    (m :: Factored) (m' :: Factored) zp zq :: Constraint
  type MulCTCtx_         expr (c :: Factored -> * -> *)
    (m :: Factored) (m' :: Factored) zp zq :: Constraint
  type TunnelCtx_        expr (c  :: Factored -> * -> *)
    (e  :: Factored) (r  :: Factored) (s  :: Factored)
    (e' :: Factored) (r' :: Factored) (s' :: Factored) zp zq gad :: Constraint


  modSwitchPT_ :: (ModSwitchPTCtx_ expr c m m' zp zp' zq)
    => expr env (CT d m zp (c m' zq) -> CT d m zp' (c m' zq))

  modSwitch_ :: (ModSwitchCtx_ expr c m m' zp zq zq')
    => expr env (CT d m zp (c m' zq) -> CT d m zp (c m' zq'))

  addPublic_ :: (AddPublicCtx_ expr c m m' zp zq)
    => c m zp -> expr env (CT d m zp (c m' zq) -> CT d m zp (c m' zq))

  mulPublic_ :: (MulPublicCtx_ expr c m m' zp zq)
    => c m zp -> expr env (CT d m zp (c m' zq) -> CT d m zp (c m' zq))

  keySwitchQuad_ :: (KeySwitchQuadCtx_ expr c m m' zp zq gad)
    => KSHint gad (c m' zq) -> expr env (CT 2 m zp (c m' zq) -> CT 1 m zp (c m' zq))

  addCT_ :: AddCTCtx_ expr c m m' zp zq
    => expr env (CT d1 m zp (c m' zq) -> CT d2 m zp (c m' zq) -> CT (Max d1 d2) m zp (c m' zq))

  negateCT_ :: NegateCTCtx_ expr c m m' zp zq
    => expr env (CT d m zp (c m' zq) -> CT d m zp (c m' zq))

  mulCT_ :: MulCTCtx_ expr c m m' zp zq 
    => expr env (CT d1 m zp (c m' zq) -> CT d2 m zp (c m' zq) -> CT (d1 + d2) m zp (c m' zq))

  tunnel_ :: (TunnelCtx_ expr c e r s e' r' s' zp zq gad)
    => TunnelHint gad c e r s e' r' s' zp zq
    -> expr env (CT d r zp (c r' zq) -> CT d s zp (c s' zq))




class ErrorRate_ expr where

  type ErrorRateCtx_ expr (c :: Factored -> * -> *)
    (m :: Factored) (m' :: Factored) zp zq z :: Constraint

  errorRate_ :: (ErrorRateCtx_ expr c m m' zp zq z)
             => SK (c m' z) -> expr e (CT d m zp (c m' zq) -> Double)
