{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE EmptyDataDecls #-}

{-# LANGUAGE Trustworthy #-}

{- |
   Define the two-point standard security lattice that refers to public and
   secret information.
-}
module SecLib.LowHigh
       (
        -- * Security level for public data
           L
        -- * Security level for sensitive data
         , H
        -- * Abandoning the Sec monad
         , public
       )

where

import SecLib.TCB.Sec
import SecLib.TCB.Lattice

-- | Security level associated to public information.
data L

-- | Security level associated to secret information.
data H

instance CanFlowTo L L where

-- | Two-point lattice (information can flow between public entities)
instance Less L L where

instance CanFlowTo H H where

-- | Two-point lattice (information can flow between secret entities)
instance Less H H where

instance CanFlowTo L H where

-- | Two-point lattice (information can flow from public to secret entities)
instance Less L H where


-- | Only public values can be removed from the 'Sec' monad.
public :: Sec L a -> a
public (MkSec a) = a