{-# LANGUAGE ExistentialQuantification #-}

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

where

import SecLib.Sec ( Sec (), reveal, unSecType )
import SecLib.SecIO
import Data.IORef
import SecLib.Lattice ( Less (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 sh sl a b = Sec sh a -> SecIO sl b

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

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


-- | Create an escape hatch. 
hatch :: Less sl sh => (a -> b) -> Sec sh a -> SecIO s (Sec sl b)   
hatch f sec_sh = less sl sh `seq` return sec_sl 
                 where 
                       sec_sl = return $ f $ reveal sec_sh
                       sh = unSecType sec_sh
                       sl = unSecType sec_sl 


{- | Limit the number of times that an escape hatch can be applied by 
      a single run of the program.
-}
ntimes :: Int -> (Sec sh a -> SecIO s (Sec sl b)) 
              -> IO (Sec sh a -> SecIO s (Sec sl b))  
ntimes n f = do ref <- newIORef n
                return $ \sa -> 
                        MkSecIO $
                                  do k <- readIORef ref
                                     let MkSecIO m = f sa
                                     if k <= 0
                                        then error "ntimes failed!"
                                        else do writeIORef ref (k-1)
                                                m 


{- | 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 :: (Sec sh a -> SecIO s (Sec sl b)) 
         -> IO (Sec sh a -> SecIO s (Sec sl b), Open s, Close s)  
flock f = do ref <- newIORef False 
             return (\sa -> MkSecIO $ 
                             do b <- readIORef ref
                                let MkSecIO m = f sa 
                                if b then m  
                                     else error "flock fails!"  
                     , MkSecIO $ writeIORef ref True >> return (return ()) 
                     , MkSecIO $ writeIORef ref False >> return (return ())
                    )

 

{- | 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 @sh@.
-}
dlm :: (Sec sh a -> SecIO s (Sec sl b)) 
       -> IO (Sec sh a -> SecIO s (Sec sl b), Authority sh)  
dlm f = do (whof, open, close) <- flock f
           return (whof, Authority open close) 

{- | Certify that a piece of code have certain authority. -}
certify :: sh -> Authority sh -> SecIO s a -> SecIO s a 
certify sh (Authority open close) sec_io = 
   sh `seq` do MkSecIO $ run open >> return (return ())
               a <- sec_io 
               MkSecIO $ run close >> return (return ())
               return a