{-# LANGUAGE FlexibleContexts #-}

-- | Define the classic two-point lattice that refers to public and secret information. 
module SecLib.LatticeLH 
       (
           L 
         , H 
         , scr
       ) 

where

import SecLib.Trustworthy 

-- | Data type representing the security level associated to public information.
data L = L 

-- | Data type representing the security level associated to secret information.
data H = H 

-- | Information can flow among entities of the same level.
instance Less a a where
  less _ _ = ()

-- | Public information can become secret.
instance Less L H where 
  less _ _ = () 


-- | The attacker can observe public data.
instance Attacker L where 
  observe _ = ()

-- | The attacker is at the terminal.
scr :: Screen L
scr = observe s `seq` m
      where (m) = MkLoc ()
            s = unLoc m 

-- | For internal use. It is not exported. 
unLoc :: Loc () s a b -> s
unLoc _ = undefined