-- | Provide declassification combinators.
module SecLib.Declassification
( 
    Hatch
  , Open
  , Close
  , Authority 
  , hatch
  , ntimes
  , flock 
  , dlm
  , certify 
)

where

import SecLib.Sec ( Sec (), reveal )
import Data.IORef
import SecLib.Lattice ( Less )


{- | 
    Type for escape hatches. Observe that @s@ and @s'@ can be arbitrarily chosen. 
    However, they are restricted when escape hatches are created using the declassification 
    combinators 'ntimes', 'flock', and 'dlm'.
-} 
type Hatch s s' a b = Sec s a -> IO (Maybe (Sec s' b))

-- | Used by 'flock'. It represents computations that open flow locks.
type Open  = IO ()
-- | Used by 'flock'. It represents computations that close flow locks.
type Close = IO ()

-- | Used by 'dlm'. 
data Authority s = Authority Open Close 


-- | Create an escape hatch. 
hatch :: Less s' s => (a -> b) -> Hatch s s' a b  
hatch f = \sa -> return ( Just ( return ( f (reveal sa) ) ) )

{- | Limit the number of times that an escape hatch can be applied by 
     a single run of the program.
-}
ntimes :: Int -> Hatch s s' a b -> IO (Hatch s s' a b)  
ntimes n f = do ref <- newIORef n
                return $ \sa ->
                              do k <- readIORef ref
                                 if k <= 0
                                    then do return Nothing
                                    else do writeIORef ref (k-1)
                                            f sa 


{- | This function associates a flow lock to an escape hatch. 
     Then, the escape hatch 
     can be successfully applied when the flow lock is open. 
     The escape hatch cannot by applied after closing the flock lock.
-}
flock :: Hatch s s' a b -> IO (Hatch s s' a b, Open, Close)  
flock f = do ref <- newIORef False 
             return (\sa -> do b <- readIORef ref
                               if b then f sa 
                                    else return Nothing 
                     , writeIORef ref True 
                     , writeIORef ref False
                    )
 

{- | This function allows to an escape hatch to be applied only when 
     the running code can be certified with some authority. The certification process is just to show that 
     the code has access to a constructor of type @s@.
-}
dlm :: Hatch s s' a b -> IO (Hatch s s' a b, Authority s )  
dlm f = do (whof, open, close) <- flock f
           return (whof, Authority open close) 

-- | Certify that a piece of code have certain authority.
certify :: s -> Authority s -> IO a -> IO a 
certify s (Authority open close) io = 
  s `seq` ( do open ; a <- io ; close ; return a )