-- | 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 :: Less s s' => Sec s a -> Sec s' a
up sec_s@(MkSec a) = less s s' `seq` sec_s' 
                     where (sec_s') = MkSec 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