{-| This module provides bindings for the "DCLabel" module, with some 
renaming to resolve name clashes. The delegation of privilege and 
other trusted code is not exported by this module and code wishing to
use this should import "DCLabel.TCB".
-}

{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE DeriveDataTypeable #-}
module LIO.DCLabel ( -- * DCLabel export
  		     module DCLabel.Safe
                   , DCCatSet
                     -- * Renamed privileges
                   , DCPriv, DCPrivTCB
                     -- * Useful aliases for the LIO Monad
                   , DC, evalDC
                   )where

import LIO.TCB
import Data.Typeable

import DCLabel.Safe hiding ( Label
                           , Priv
                           , bottom
                           , top
                           , join
                           , meet)
import qualified DCLabel.Core as DCL


deriving instance Typeable DCL.Disj
deriving instance Typeable DCL.Conj
deriving instance Typeable DCL.Label
deriving instance Typeable DCL.DCLabel

instance POrd DCLabel where
	leq = DCL.canflowto

instance Label DCLabel where
	lbot = DCL.bottom
	ltop = DCL.top
	lub  = DCL.join
	glb  = DCL.meet

instance PrivTCB DCL.TCBPriv

instance MintTCB DCL.TCBPriv DCL.Priv where
	mintTCB = DCL.createPrivTCB

instance MintTCB DCL.TCBPriv DCL.Principal where
	mintTCB p = DCL.createPrivTCB (newPriv p)

instance Priv DCLabel DCL.TCBPriv where
  	leqp = DCL.canflowto_p
        {-
        The implementation of lostar deserves an explanation. Firstly note
        that the properties, for @r = lostar p l g@ that must be satisfied
        are [the suffix \'s\' (\'i\')is used for seecrecy (resp. integrity):
        1.) @leq g r    : (rs => gs)      and  (gi => ri)@
        2.) @leqp p l r : (rs /\ p => ls) and  (li /\ p => ri)@
        Finding the integrity component of @r@ is trivial: it's
        simply the least upper bound of @gi@ and @li /\ p@.
        Finding the secrecy component is a bit trickier. To do so, we first
        find all the categories of @ls@ that are not implied by @p@ (this
        gives us @rs'@), such that @rs' /\ p => ls@. Then, we need to find
        the remaining categories in @gs@ that are not implied by @rs'@ (this
        gives us @rs''@). Directly, @rs = rs' /\ rs''@.
        -}
        lostar p l g = 
          let (ls, li) = (secrecy l, integrity l)
              (gs, gi) = (secrecy g, integrity g)
              lp       = DCL.priv p
              rs'      = c2l [c | c <- getCats ls
                                , not (lp `DCL.implies` (c2l [c]))]
              rs''     = c2l [c | c <- getCats gs
                                , not (rs' `DCL.implies` (c2l [c]))]
              rs       = rs' `DCL.and_label` rs''
              ri       = (li `DCL.and_label` lp) `DCL.or_label` gi
         in DCL.toLNF $ newDC rs ri
              where getCats = DCL.conj . DCL.label
                    c2l = DCL.MkLabel . DCL.MkConj
        {- OLD, BROKEN (was more elegant than above, so maybe use some ideas
           when rewriting  the above):
  	lostar p li lg = 
          let lip = newDC (DCL.secrecy li) ((DCL.integrity li) ./\. lp)
              lgp = newDC ((DCL.secrecy lg) ./\. lp) (DCL.integrity lg)
	      lp  = DCL.priv p
	  in DCL.join lip lgp
        -}

--
-- Renaming
--

-- | A "DCLabel" category set.
type DCCatSet = DCL.Label
-- | A "DCLabel" (untrusted) privilege.
type DCPriv = DCL.Priv
-- | A "DCLabel" privilege.
type DCPrivTCB = DCL.TCBPriv


--
-- LIO aliases
--

-- | The monad for LIO computations using 'DCLabel' as the label.
type DC = LIO DCLabel ()

-- | Runs a computation in the LIO Monad, returning both the
-- computation's result and the label of the result.
evalDC :: DC a -> IO (a, DCLabel)
evalDC m = evalLIO m ()