module CopyT where 

import SecLib.LatticeLH
import SecLib.Trustworthy

import CopyU (copy)  -- Import the untrustworthy code that will 
                     -- use secret_file and public_file 

secret_file :: File H 
secret_file = mkFile "SecretFile" 

public_file :: File L 
public_file = mkFile "PublicFile"


trusted_copy :: Less s s' => (File s -> File s' -> SecIO s' ()) 
                             -> File s -> File s' -> IO ()  
trusted_copy copy_func fs fs' = do sec <- revealIO $ copy_func fs fs' 
                                   return $ reveal sec

execute :: IO () 
execute = trusted_copy copy public_file secret_file