module SME.Trustworthy 
       (
        -- Lattices in general  
        Lattice (meet, join), 
        FiniteLattice (universe, upset), 
        less, 
        sless, 
        -- Two point lattice (low and high) 
        Level (L, H),
        -- Security policy 
        Policy (level, defvalue),
        -- Secure Multi-Execution monad
        ME (), 
        readFile, 
        writeFile, 
        sme,
        -- Secure Multi-Execution for the two point lattice (low and high) 
        sme'
       )
where

import Prelude hiding (readFile, writeFile)
import SME.Lattice
import SME.LatticeLH
import SME.ME 

-- | Function to perform secure multi-execution considering the two-point security lattice encoded by 'Level'.
sme' :: Policy Level FilePath String => ME a -> IO ()
sme' t = sme (undefined :: Level) t