{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE Unsafe #-}

-- | Provide security for computations involving pure values.
module SecLib.Sec where

import SecLib.Lattice

-- Sec

-- | This type represents pure values of type @a@ at confidentiality level @s@.
newtype Sec s a = MkSec a


instance Functor (Sec s) where
  h `fmap` (MkSec x) = MkSec (h x)


instance Monad (Sec s) where
  return x = sec x

  MkSec a >>= k =
    MkSec (let MkSec b = k a in b)


-- | Assign the confidentiality level @s@ to a value of type @a@.
sec :: a -> Sec s a
sec x = MkSec x

{- Legacy code

{-| Open the abstraction provided by 'Sec'.
    However, it is only possible to obtain a when  providing the key s.
-}
open :: Sec s a -> s -> a
open (MkSec a) s = s `seq` a

-}

-- | Raise the confidentiality level of values.
up :: forall a s s'. Less s s' => Sec s a -> Sec s' a
up sec_s@(MkSec a) = less s s' `seq` sec_s'
                     where sec_s' = sec a :: Sec s' a
                           s      = unSecType sec_s
                           s'     = unSecType sec_s'

-- | Break the abstraction provide by 'Sec'. /It is used only in trustworthy code/.
reveal :: Sec s a -> a
reveal (MkSec a) = a

-- | Internal function, not exported. For type-checking purposes.
unSecType :: Sec s a -> s
unSecType _ = undefined


-- | Reveal values that the attacker can observe.
public :: Attacker s => Sec s a -> a
public sec_s@(MkSec a) = observe s `seq` a
                         where s = unSecType sec_s