{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}

{-# LANGUAGE Trustworthy #-}

-- | 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 :: L
           s = unLoc m

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