{-# LANGUAGE Unsafe #-}

{- |
   It provides a secure interface for manipulation of references.
-}
module SecLib.TCB.Ref
    (
       -- * Secure references
       Ref
       -- * Operations
     , tcbRef
     , newRefSecIO
     , readRefSecIO
     , writeRefSecIO
    )

where

import Data.IORef
import SecLib.Sec
import SecLib.TCB.SecIO

---
--- Secure references
---

-- | Secure references
data Ref l a = MkRef (IORef a)

---
--- Operations
---

-- | Only use by trusted code
tcbRef = MkRef

{- | It creates a new reference. There is no relation between
@l@ and @l'@ since creating a reference
is not an /observable/ event inside the 'SecIO' monad.
-}
newRefSecIO :: a -> SecIO l (Ref l' a)
newRefSecIO a = do ref <- ioTCB $ newIORef a
                   return (MkRef ref)

{- | As above, there is no relation between
@l@ and @l'@. Bare in mind that reading a reference
is not an /observable/ event inside the `SecIO` monad.
-}
readRefSecIO :: Ref l a -> SecIO l' (Sec l a)
readRefSecIO (MkRef ref) = do a <- ioTCB $ readIORef ref
                              return (return a)
{- | It writes references only at the security level indicated by the argument
of the 'SecIO' monad.
-}
writeRefSecIO :: Ref l a -> a -> SecIO l ()
writeRefSecIO (MkRef ref) a = ioTCB $ writeIORef ref a