diff --git a/LIO.hs b/LIO.hs
--- a/LIO.hs
+++ b/LIO.hs
@@ -3,41 +3,36 @@
 
 This is the main module to be included by code using the Labeled IO
 (LIO) library. This module exports the core library (documented in
-"LIO.Core"), with support for labeled values (documented in
-"LIO.Labeled") and privileges (documented in "LIO.Privs").
+"LIO.Core"), with support for labels and privileges (documented in
+"LIO.Label") and labeled values (documented in "LIO.Labeled").
 
-Certain symbols in the lio library, particularly those in
+Certain symbols in the LIO library, particularly those in
 "LIO.Exception", use the same names as their 'IO' equivalents in the
-system libraries.  Hence main modules that mostly include 'IO' code
-and only need to invoke 'LIO' code should import "LIO.Run" (or
+system libraries.  Hence main modules consisting mostly of 'IO' code
+that simply need to run 'LIO' code should import "LIO.Run" (or
 "LIO.DCLabel") to avoid polluting their namespaces.
 
 Most code will need to use a particular label format, which needs to
-be imported separately.  For instance:
+be imported separately.  Hence, a typical set of imports for an
+untrusted LIO module is:
 
 @
  import "LIO"
- -- Import your favorite label format:
  import "LIO.DCLabel"
 @
 
-WARNING:  For security, untrusted code must always be compiled with
-the @-XSafe@ and @-fpackage-trust@ /SafeHaskell/ flags. See
-<http://hackage.haskell.org/trac/ghc/wiki/SafeHaskell> for more
-details on the guarantees provided by SafeHaskell.
-
 -}
 
 module LIO ( 
-    module LIO.Label
+    module LIO.Core
+  , module LIO.Delegate
   , module LIO.Exception
-  , module LIO.Core
+  , module LIO.Label
   , module LIO.Labeled
-  , module LIO.Privs
   ) where
 
-import LIO.Core
-import LIO.Exception
-import LIO.Label
-import LIO.Labeled
-import LIO.Privs
+import safe LIO.Core
+import safe LIO.Delegate
+import safe LIO.Exception
+import safe LIO.Label
+import safe LIO.Labeled
diff --git a/LIO/Concurrent.hs b/LIO/Concurrent.hs
--- a/LIO/Concurrent.hs
+++ b/LIO/Concurrent.hs
@@ -1,52 +1,54 @@
 {-# LANGUAGE Trustworthy #-}
 {- |
 
-This module exposes useful concurrency abstrations for 'LIO'. This
-module is, in part, analogous to "Control.Concurrent". Specifically,
-LIO provides a means for spawning 'LIO' computations in a new thread
-with 'forkLIO'.  LIO relies on the lightweight threads managed by
-Haskell's runtime system; we do not provide a way to fork OS-level
-threads.
+This module provides concurrency abstractions for 'LIO'.  The most
+basic function, 'forkLIO', spawns a computation in a new light-weight
+thread (analogous to 'forkIO').
 
-In addition to this, LIO also provides 'lFork' and 'lWait' which allow
-forking of a computation that is restricted from reading data more
-sensitive than a given upper bound. This limit is different from
-clearance in that it allows the computation to spawn additional
-threads with an upper bound above said upper bound label, but below
-the clearance. The 'lFork' function should be used whenever an LIO
-computation wishes to execute a sub-computation that may raise the
-current label (up to the supplied upper bound).  To this end, the
-current label only needs to be raised when the computation is
-interested in reading the result of the sub-computation. The role of
-'lWait' is precisely this: raise the current label and return the
-result of such a sub-computation.
+'lFork' spawns a forked thread that returns a result other threads can
+wait for (using 'lWait').  The label of such a thread's result must be
+specified at the time the thread is spawned with 'lFork'.  Should the
+'lFork'ed thread terminate with its current label be above the
+specified result label, 'lWait' will throw an exception of type
+'ResultExceedsLabel' in any thread waiting for the result.
 
+Learing that a spawned thread has terminated by catching a
+'ResultExceedsLabel' may cause the label of the waiting thread to
+rise, possibly above the current clearance (in which case the
+exception cannot be caught).  As an alternative, 'timedlWait'
+unconditionally kills a spawned thread if it has not terminated at an
+observable label within a certain time period.  'timedlWait' is
+guaranteed both to terminate and not to throw exceptions that cannot
+be caught at the current label.
+
 -}
 module LIO.Concurrent (
-    LabeledResult
-  -- * Forking new threads
-  , lForkP, lFork, forkLIO
+  -- * Forking simple threads
+    forkLIO
+  -- * Forking threads that return results
+  , LabeledResult
+  , lFork, lForkP
   -- * Waiting on threads
-  , lWaitP, lWait
-  , trylWaitP, trylWait
-  , timedlWaitP, timedlWait
+  , ResultExceedsLabel(..)
+  , lWait, lWaitP
+  , trylWait, trylWaitP
+  , timedlWait, timedlWaitP
   -- * Labeled MVars
   , module LIO.Concurrent.LMVar
   ) where
 
 
-import qualified Control.Concurrent as IO
-import qualified Control.Exception as IO
-import Control.Monad
-import Data.IORef
+import safe qualified Control.Concurrent as IO
+import safe qualified Control.Exception as IO
+import safe Control.Monad
+import safe Data.IORef
 
-import LIO.Concurrent.LMVar
-import LIO.Core
-import LIO.Exception
-import LIO.Label
-import LIO.Privs
+import safe LIO.Concurrent.LMVar
+import safe LIO.Core
+import safe LIO.Exception
+import safe LIO.Error
+import safe LIO.Label
 import LIO.TCB
-import LIO.TCB.Concurrent
 
 
 --
@@ -73,12 +75,7 @@
 -- label and clearance as enforced by a call to 'guardAlloc'.
 -- Moreover, the supplied computation must not terminate with its
 -- label above the result label; doing so will result in an exception
--- (whose label will reflect this observation) being thrown in the
--- thread reading the result.
---
--- If an exception is thrown in the inner computation, the exception
--- label will be raised to the join of the result label and original
--- exception label.
+-- being thrown in the thread reading the result.
 -- 
 -- Note that @lFork@ immediately returns a 'LabeledResult', which is
 -- essentially a \"future\", or \"promise\". This prevents
@@ -97,14 +94,14 @@
 -- for when performing label comparisons.
 lForkP :: PrivDesc l p =>
           Priv p -> l -> LIO l a -> LIO l (LabeledResult l a)
-lForkP p l lio = do
-  guardAllocP p l
+lForkP p l (LIOTCB action) = do
+  withContext "lForkP" $ guardAllocP p l
   mv <- ioTCB IO.newEmptyMVar
   st <- ioTCB $ newIORef LResEmpty
   s0 <- getLIOStateTCB
   tid <- ioTCB $ IO.mask $ \unmask -> IO.forkIO $ do
     sp <- newIORef s0
-    ea <- IO.try $ unmask $ unLIOTCB lio sp
+    ea <- IO.try $ unmask $ action sp
     LIOState lEnd _ <- readIORef sp
     writeIORef st $ case ea of
       _ | not (lEnd `canFlowTo` l) -> LResLabelTooHigh lEnd
@@ -124,7 +121,7 @@
 -- the result must be above the current label and below the current
 -- clearance. Moreover, before block-reading, @lWait@ raises the current
 -- label to the join of the current label and label of result.  An
--- exception is thrown by the underlying 'guardWrite' if this is not the
+-- exception is thrown by the underlying 'taint' if this is not the
 -- case.  Additionally, if the thread terminates with an exception (for
 -- example if it violates clearance), the exception is rethrown by
 -- @lWait@. Similarly, if the thread reads values above the result label,
@@ -134,14 +131,19 @@
 
 -- | Same as 'lWait', but uses priviliges in label checks and raises.
 lWaitP :: PrivDesc l p => Priv p -> LabeledResult l a -> LIO l a
-lWaitP p (LabeledResultTCB _ l mv st) = taintP p l >> go
+lWaitP p (LabeledResultTCB _ l mv st) =
+  withContext "lWaitP" (taintP p l) >> go
   where go = ioTCB (readIORef st) >>= check
         check LResEmpty = ioTCB (IO.readMVar mv) >> go
         check (LResResult a) = return $! a
         check (LResLabelTooHigh lnew) = do
           modifyLIOStateTCB $ \s -> s {
-            lioLabel = partDowngradeP p lnew (lioLabel s) }
-          throwLIO ResultExceedsLabel
+            lioLabel = downgradeP p lnew `lub` lioLabel s }
+          throwLIO ResultExceedsLabel {
+              relContext = []
+            , relLocation = "lWaitP"
+            , relDeclaredLabel = l
+            , relActualLabel = Just lnew }
 
 
 -- | Same as 'lWait', but does not block waiting for result.
@@ -151,13 +153,17 @@
 -- | Same as 'trylWait', but uses priviliges in label checks and raises.
 trylWaitP :: PrivDesc l p => Priv p -> LabeledResult l a -> LIO l (Maybe a)
 trylWaitP p (LabeledResultTCB _ rl _ st) =
-  taintP p rl >> ioTCB (readIORef st) >>= check
+  withContext "trylWaitP" (taintP p rl) >> ioTCB (readIORef st) >>= check
   where check LResEmpty = return Nothing
         check (LResResult a) = return . Just $! a
         check (LResLabelTooHigh lnew) = do
           curl <- getLabel
           if canFlowToP p lnew curl
-            then throwLIO ResultExceedsLabel
+            then throwLIO ResultExceedsLabel {
+                     relContext = []
+                   , relLocation = "trylWaitP"
+                   , relDeclaredLabel = rl
+                   , relActualLabel = Just lnew }
             else return Nothing
 
 
@@ -165,10 +171,14 @@
 -- | Like 'lWait', with two differences.  First, a timeout is
 -- specified and the thread is unconditionally killed after this
 -- timeout (if it has not yet returned a value).  Second, if the
--- thread's result exceeds its label @timedWait@ and exceeds what the
--- calling thread can observe, consumes the whole timeout and throws a
+-- thread's result exceeds what the calling thread can observe,
+-- @timedlWait@ consumes the whole timeout and throws a
 -- 'ResultExceedsLabel' exception you can catch (i.e., it never raises
 -- the label above the clearance).
+--
+-- Because this function can alter the result by killing a thread, it
+-- requires the label of the 'LabeledResult' to be both readable and
+-- writable at the current label.
 timedlWait :: Label l => LabeledResult l a -> Int -> LIO l a
 timedlWait = timedlWaitP noPrivs
 
@@ -177,7 +187,9 @@
 -- catching any 'ResultExceedsLabel' before the timeout period (if
 -- possible).
 timedlWaitP :: PrivDesc l p => Priv p -> LabeledResult l a -> Int -> LIO l a
-timedlWaitP p lr@(LabeledResultTCB t _ mvb _) to = trylWaitP p lr >>= go
+timedlWaitP p lr@(LabeledResultTCB t rl mvb _) to =
+  withContext "timedlWaitP" $ do guardWriteP p rl
+                                 trylWaitP p lr >>= go
   where go (Just a) = return a
         go Nothing = do
           mvk <- ioTCB $ IO.newEmptyMVar
@@ -186,5 +198,9 @@
             IO.throwTo t (UncatchableTCB IO.ThreadKilled)
           ioTCB $ IO.readMVar mvb
           trylWaitP p lr >>= maybe
-            (ioTCB (IO.takeMVar mvk) >> throwLIO ResultExceedsLabel)
+            (ioTCB (IO.takeMVar mvk) >> throwLIO failure)
             (\a -> ioTCB (IO.killThread tk) >> return a)
+        failure = ResultExceedsLabel { relContext = []
+                                     , relLocation = "timedWaitP"
+                                     , relDeclaredLabel = rl
+                                     , relActualLabel = Nothing }
diff --git a/LIO/Concurrent/LMVar.hs b/LIO/Concurrent/LMVar.hs
--- a/LIO/Concurrent/LMVar.hs
+++ b/LIO/Concurrent/LMVar.hs
@@ -7,7 +7,7 @@
 "Control.Concurrent.MVar", but the operations take place in the 'LIO'
 monad.  A labeled MVar, of type @'LMVar' l a@, is a mutable location
 that can be in of of two states; an 'LMVar' can be empty, or it can be
-full (with a value of tye @a@). The location is protected by a label
+full (with a value of type @a@). The location is protected by a label
 of type 'l'.  As in the case of @LIORef@s (see "LIO.LIORef"), this
 label is fixed and does not change according to the content placed
 into the location.  Different from @LIORef@s, taking and putting
@@ -40,11 +40,11 @@
   , isEmptyLMVar, isEmptyLMVarP
   ) where
 
-import Control.Concurrent.MVar
+import safe Control.Concurrent.MVar
 
-import LIO.Label
-import LIO.Core
-import LIO.Privs
+import safe LIO.Core
+import safe LIO.Error
+import safe LIO.Label
 import LIO.TCB
 import LIO.TCB.LObj
 
@@ -63,14 +63,16 @@
 newEmptyLMVar :: Label l
               => l                -- ^ Label of @LMVar@
               -> LIO l (LMVar l a)    -- ^ New mutable location
-newEmptyLMVar l = guardAlloc l >> ioTCB (LObjTCB l `fmap` newEmptyMVar)
+newEmptyLMVar l = do
+  withContext "newEmptyLMVar" $ guardAlloc l
+  ioTCB (LObjTCB l `fmap` newEmptyMVar)
 
 -- | Same as 'newEmptyLMVar' except it takes a set of privileges which
 -- are accounted for in comparing the label of the MVar to the current
 -- label and clearance.
 newEmptyLMVarP :: PrivDesc l p => Priv p -> l -> LIO l (LMVar l a)
 newEmptyLMVarP p l = do
-  guardAllocP p l
+  withContext "newEmptyLMVarP" $ guardAllocP p l
   ioTCB $ LObjTCB l `fmap` newEmptyMVar
 
 -- | Create a new labeled MVar, in an filled state with the supplied
@@ -80,14 +82,16 @@
          => l                       -- ^ Label of @LMVar@
          -> a                       -- ^ Initial value of @LMVar@
          -> LIO l (LMVar l a)       -- ^ New mutable location
-newLMVar l a = guardAlloc l >> ioTCB (LObjTCB l `fmap` newMVar a)
+newLMVar l a = do
+  withContext "newLMVar" $ guardAlloc l
+  ioTCB (LObjTCB l `fmap` newMVar a)
 
 -- | Same as 'newLMVar' except it takes a set of privileges which are
 -- accounted for in comparing the label of the MVar to the current label
 -- and clearance.
 newLMVarP :: PrivDesc l p => Priv p -> l -> a -> LIO l (LMVar l a)
 newLMVarP p l a = do
-  guardAllocP p l
+  withContext "newLMVarP" $ guardAllocP p l
   ioTCB $ LObjTCB l `fmap` newMVar a
 
 --
@@ -102,26 +106,26 @@
 -- current label to the join of the current label and the label of the
 -- MVar and read the contents of the @MVar@. The underlying guard
 -- 'guardWrite' will throw an exception if any of the IFC checks fail.
--- If the Finally, like 'MVars' if the 'LMVar' is empty, @takeLMVar@
+-- Finally, like 'MVars' if the 'LMVar' is empty, @takeLMVar@
 -- blocks.
 takeLMVar :: Label l => LMVar l a -> LIO l a
-takeLMVar = blessTCB takeMVar
+takeLMVar = blessTCB "takeLMVar" takeMVar
 
 -- | Same as 'takeLMVar' except @takeLMVarP@ takes a privilege object
 -- which is used when the current label is raised.
 takeLMVarP :: PrivDesc l p => Priv p -> LMVar l a -> LIO l a
-takeLMVarP = blessPTCB takeMVar
+takeLMVarP = blessPTCB "takeLMVarP" takeMVar
 
 -- | Non-blocking version of 'takeLMVar'. It returns @Nothing@ if the
 -- 'LMVar' is empty, otherwise it returns @Just@ value, emptying the
 -- 'LMVar'.
 tryTakeLMVar :: Label l => LMVar l a -> LIO l (Maybe a)
-tryTakeLMVar = blessTCB tryTakeMVar
+tryTakeLMVar = blessTCB "tryTakeLMVar" tryTakeMVar
 
 -- | Same as 'tryTakeLMVar', but uses priviliges when raising current
 -- label.
 tryTakeLMVarP :: PrivDesc l p => Priv p -> LMVar l a -> LIO l (Maybe a)
-tryTakeLMVarP = blessPTCB tryTakeMVar
+tryTakeLMVarP = blessPTCB "tryTakeLMVar" tryTakeMVar
 
 --
 -- Put 'LMVar'
@@ -140,21 +144,21 @@
          => LMVar l a   -- ^ Source 'LMVar'
          -> a           -- ^ New value
          -> LIO l ()
-putLMVar = blessTCB putMVar
+putLMVar = blessTCB "putLMVar" putMVar
 
 -- | Same as 'putLMVar' except @putLMVarP@ takes a privilege object
 -- which is used when the current label is raised.
 putLMVarP :: PrivDesc l p => Priv p -> LMVar l a -> a -> LIO l ()
-putLMVarP = blessPTCB putMVar
+putLMVarP = blessPTCB "putLMVarP" putMVar
 
 -- | Non-blocking version of 'putLMVar'. It returns @True@ if the
 -- 'LMVar' was empty and the put succeeded, otherwise it returns @False@.
 tryPutLMVar :: Label l => LMVar l a -> a -> LIO l Bool
-tryPutLMVar = blessTCB tryPutMVar
+tryPutLMVar = blessTCB "tryPutLMVar" tryPutMVar
 
 -- | Same as 'tryPutLMVar', but uses privileges when raising current label.
 tryPutLMVarP :: PrivDesc l p => Priv p -> LMVar l a -> a -> LIO l Bool
-tryPutLMVarP = blessPTCB tryPutMVar
+tryPutLMVarP = blessPTCB "tryPutLMVarP" tryPutMVar
 
 --
 -- Read 'LMVar'
@@ -166,12 +170,12 @@
 -- a function such as 'putLMVar', 'tryTakeLMVarP', or 'isEmptyLMVar'
 -- for this 'LMVar'.
 readLMVar :: Label l => LMVar l a -> LIO l a
-readLMVar = blessTCB readMVar
+readLMVar = blessTCB "readLMVar" readMVar
 
 -- | Same as 'readLMVar' except @readLMVarP@ takes a privilege object
 -- which is used when the current label is raised.
 readLMVarP :: PrivDesc l p => Priv p -> LMVar l a -> LIO l a
-readLMVarP = blessPTCB readMVar
+readLMVarP = blessPTCB "readLMVarP" readMVar
 
 --
 -- Swap 'LMVar'
@@ -188,12 +192,12 @@
           => LMVar l a          -- ^ Source @LMVar@
           -> a                  -- ^ New value
           -> LIO l a            -- ^ Taken value
-swapLMVar = blessTCB swapMVar
+swapLMVar = blessTCB "swapLMVar" swapMVar
 
 -- | Same as 'swapLMVar' except @swapLMVarP@ takes a privilege object
 -- which is used when the current label is raised.
 swapLMVarP :: PrivDesc l p => Priv p -> LMVar l a -> a -> LIO l a
-swapLMVarP = blessPTCB swapMVar
+swapLMVarP = blessPTCB "swapLMVarP" swapMVar
 
 --
 -- Check state of 'LMVar'
@@ -202,12 +206,10 @@
 -- | Check the status of an 'LMVar', i.e., whether it is empty. The
 -- function succeeds if the label of the 'LMVar' is below the current
 -- clearance -- the current label is raised to the join of the 'LMVar'
--- label and the current label. Note that this function only returns a
--- snapshot of the state and does not modify it -- hence the
--- underlying guard is 'taint' and not 'guardWrite'.
+-- label and the current label.
 isEmptyLMVar :: Label l => LMVar l a -> LIO l Bool
-isEmptyLMVar = blessTCB isEmptyMVar
+isEmptyLMVar = blessTCB "isEmptyLMVar" isEmptyMVar
 
 -- | Same as 'isEmptyLMVar', but uses privileges when raising current label.
 isEmptyLMVarP :: PrivDesc l p => Priv p -> LMVar l a -> LIO l Bool
-isEmptyLMVarP = blessPTCB isEmptyMVar
+isEmptyLMVarP = blessPTCB "isEmptyLMVarP" isEmptyMVar
diff --git a/LIO/Core.hs b/LIO/Core.hs
--- a/LIO/Core.hs
+++ b/LIO/Core.hs
@@ -2,70 +2,60 @@
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE FunctionalDependencies #-}
 {-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE DeriveDataTypeable #-}
 
 {- | 
 
-This module implements the core of the Labeled IO (LIO) library for
-information flow control (IFC) in Haskell.  It provides a monad,
-'LIO', that is intended to be used as a replacement for the 'IO' monad
-in untrusted code.  The idea is for untrusted code to provide a
-computation in the 'LIO' monad, which trusted code can then safely
-execute through using 'evalLIO'-like functions. Though, usually a
-wrapper function is employed depending on the type of /labels/ used by
-an application.  For example, with "LIO.DCLabel" trusted code would
-'evalDC' to execute an untrusted computation.
+This module implements the core of the Labeled IO (LIO) information
+flow control (IFC) library.  It provides a monad, 'LIO', that is
+intended to be used as a replacement for the 'IO' monad in untrusted
+code.  The idea is for untrusted code to provide a computation in the
+'LIO' monad, which trusted code can then safely execute through
+'evalLIO' and similar functions (e.g., 'evalDC' in
+"LIO.DCLabel#v:evalDC").
 
-Labels are a way of describing who can observe and modify data. (A
-detailed consideration of labels is given in "LIO.Label".) LIO
-associates a /current label/ with every 'LIO' computation. The current
-label effectively tracks the sensitivity of all the data that the
-computation has observed.  For example, if the computation has read a
-\"secret\" mutable refernce (see "LIO.LIORef") and then the result of
-a \"top-secret\" thread (see "LIO.Concurrent") then the current label
-will be at least \"top-secret\". The role of the current label is
-two-fold. First, the current label protects all the data in scope --
-it is the label associated with any /unlabeled/ data. For example, the
-current label is the label on constants such as @3@ or @\"tis a
-string\"@. More interestingly, consider reading a \"secret\" file:
+Unlike 'IO', the 'LIO' monad keeps track of a /current label/
+(accessible via the 'getLabel' function) during each computation. The
+current label effectively tracks the sensitivity of all the data that
+the computation has observed.  For example, if the computation has
+read a \"secret\" mutable reference (see "LIO.LIORef") and then the
+result of a \"top-secret\" thread (see "LIO.Concurrent") then the
+current label will be at least \"top-secret\".  Labels are described
+in more detail in the documentation for "LIO.Label", as well as the
+documentation for particular label formats (such as "LIO.DCLabel").
 
-> bs <- readFile "/secret/file.txt"
+The role of the current label is two-fold:  First, the current label
+protects all pure values currently in scope.  For example, the current
+label is the label on constants (such as @3@ and @\"tis a string\"@)
+as well as function arguments.  More interestingly, consider reading a
+secret reference:
 
-Though the label in the file store may be \"secret\", @bs@ has type
-@ByteString@, which is not explicitly labeled. Hence, to protect the
-contents (@bs@) the current label must be at least \"secret\" before
-executing @readFile@.  More generally, if the current label is
-@L_cur@, then it is only permissible to read data labeled @L_r@ if
-@L_r ``canFlowTo`` L_cur@.  Note that, rather than throw an exception,
-reading data will often just increase the current label to ensure that
-@L_r ``canFlowTo`` L_cur@ using 'taint'.
+> val <- readLIORef secret
 
-Second, the current label prevents inforation leaks into public
-channels. Specifically, it is only permissible to modify, or write
-to, data labeled @L_w@ when @L_cur``canFlowTo`` L_w@. Thus, it the
-following attempt to leak the secret @bs@ would fail:
+Though the label of @secret@ may be \"secret\", @val@ is not
+explicitly labeled.  Hence, to protect the contents of the 'LIORef'
+that has been read into @val@, the current label must be at least
+\"secret\" before returning from @readLIORef@.  More generally, if the
+current label is @l_cur@, then it is only permissible to read data
+labeled @l_r@ if @l_r ``canFlowTo`` l_cur@.  Note that, instead of
+throwing an exception, reading data often just increases the current
+label to ensure that @l_r ``canFlowTo`` l_cur@.  This is acomplished
+using a function such as 'taint'.
 
-> writeFile "/public/file.txt" bs
+The second purpose of the current label is to prevent inforation leaks
+into public channels. Specifically, it is only permissible to modify
+or write to data labeled @l_w@ when @l_cur``canFlowTo`` l_w@. Thus,
+the following attempt to leak the @val@ after reading it from a secret
+'LIORef' would fail:
 
+> writeLIORef public val
+
 In addition to the current label, the LIO monad keeps a second label,
-the current /clearance/ (accessible via the 'getClearance' function).
-The clearance can be used to enforce a \"need-to-know\" policy since
+the /current clearance/ (accessible via the 'getClearance' function).
+The clearance can be used to enforce a \"need-to-know\" policy, since
 it represents the highest value the current label can be raised to.
-In other words, if the current clearance is @L_clear@ then the
-computation cannot create, read or write to objects labeled @L@ such
-that @L ``canFlowTo`` L_clear@ does not hold.
-
-This module exports the 'LIO' monad, functions to access the internal
-state (e.g., 'getLabel' and 'getClearance'), functions for raising and
-catching exceptions, and IFC guards.  Exceptions are core to LIO since
-they provide a way to deal with potentially-misbehaving untrusted
-code. Specifically, when a computation is about to violate IFC (as
-@writeFile@ above), an exception is raised. Guards provide a useful
-abstraction for dealing with labeled objects; they should be used
-before performing a read-only, write-only, or read-write operation on
-a labeled object. The remaining core, but not all, abstractions are
-exported by "LIO".
+In other words, if the current clearance is @l_clear@ then the
+computation cannot create, read or write to objects labeled @l@ such
+that @(l ``canFlowTo`` l_clear) == False@.
 
 -}
 
@@ -81,78 +71,89 @@
   , getClearance, setClearance, setClearanceP
   , scopeClearance, withClearance, withClearanceP
   -- * Exceptions thrown by LIO
-  -- $lioExceptions
-  , MonitorFailure(..)
-  , VMonitorFailure(..)
+  , AnyLabelError(..), LabelError(..), InsufficientPrivs(..)
   -- * Guards
   -- $guards
-  -- ** Allocate/write-only
+
+  -- ** Allocate/write-only guards
   , guardAlloc, guardAllocP
-  -- ** Read-only
+  -- ** Read-only guards
   , taint, taintP
-  -- ** Write
+  -- ** Read-write guards
   , guardWrite, guardWriteP
   ) where
 
 
-import qualified Control.Exception as IO
-import Control.Monad
-import Data.IORef
-import Data.Typeable
+import safe qualified Control.Exception as IO
+import safe Control.Monad
+import safe Data.IORef
 
-import LIO.Exception
+import safe LIO.Error
+import safe LIO.Exception
+import safe LIO.Label
+import safe LIO.Run
 import LIO.TCB
-import LIO.Label
-import LIO.Privs
-import LIO.Run
 
 
 --
 -- Internal state
 --
 
--- | Returns the current value of the thread's label.
+-- | Returns the value of the thread's current label.
 getLabel :: Label l => LIO l l
 getLabel = lioLabel `liftM` getLIOStateTCB
 
 
--- | Raise the current label to the provided label, which must be
+-- | Raises the current label to the provided label, which must be
 -- between the current label and clearance. See 'taint'.
 setLabel :: Label l => l -> LIO l ()
-setLabel = setLabelP noPrivs
+setLabel l = withContext "setLabel" $ do
+  guardAlloc l
+  modifyLIOStateTCB $ \s -> s { lioLabel = l }
 
 -- | If the current label is @oldLabel@ and the current clearance is
--- @clearance@, this function allows code to raise the current label to
--- any value @newLabel@ such that @oldLabel ``canFlowTo`` newLabel &&
--- newLabel ``canFlowTo`` clearance@.
+-- @clearance@, this function allows code to raise the current label
+-- to any value @newLabel@ such that @'canFlowToP' priv oldLabel
+-- newLabel && 'canFlowTo' newLabel clearance@.  (Note the privilege
+-- argument affects the label check, not the clearance check; call
+-- 'setClearanceP' first to raise the clearance.)
 setLabelP :: PrivDesc l p => Priv p -> l -> LIO l ()
-setLabelP p l = do
-  guardAllocP p l `catch`
-      \(_ :: MonitorFailure) -> throwLIO InsufficientPrivs
+setLabelP p l = withContext "setLabelP" $ do
+  guardAllocP p l
   modifyLIOStateTCB $ \s -> s { lioLabel = l }
 
--- | Returns the current value of the thread's clearance.
+-- | Returns the thread's current clearance.
 getClearance :: Label l => LIO l l
 getClearance = lioClearance `liftM` getLIOStateTCB
 
--- | Lower the current clearance. The new clerance must be between
--- the current label and clerance. One cannot raise the current label
--- or create object with labels higher than the current clearance.
+-- | Lowers the current clearance.  The new clerance must be between
+-- the current label and previous current clerance.  One cannot raise
+-- the current label or create object with labels higher than the
+-- current clearance.
 setClearance :: Label l => l -> LIO l ()
-setClearance = setClearanceP noPrivs
+setClearance cnew = do
+  LIOState { lioLabel = l, lioClearance = c } <- getLIOStateTCB
+  unless (canFlowTo l cnew && canFlowTo cnew c) $
+    labelError "setClearance" [cnew]
+  putLIOStateTCB $ LIOState l cnew
 
--- | Raise the current clearance (undoing the effects of
--- 'setClearance') by exercising privileges. If the current label is
+-- | Raises the current clearance (undoing the effects of
+-- 'setClearance') by exercising privileges.  If the current label is
 -- @l@ and current clearance is @c@, then @setClearanceP p cnew@
 -- succeeds only if the new clearance is can flow to the current
--- clearance (modulo privileges), i.e., @'canFlowToP' p cnew c@ must
--- hold. Additionally, the current label must flow to the new
--- clearance, i.e., @l ``canFlowTo`` cnew@ must hold.
+-- clearance (modulo privileges), i.e., @'canFlowToP' p cnew c ==
+-- True@.  Additionally, the current label must flow to the new
+-- clearance, i.e., @l ``canFlowTo`` cnew@ == True.
+-- 
+-- Since LIO guards that are used when reading/writing data (e.g.,
+-- 'guardAllocP') do not use privileges when comparing labels with the
+-- current clearance, code must always raise the current clearance, to
+-- read/write data above the current clearance.
 setClearanceP :: PrivDesc l p => Priv p -> l -> LIO l ()
 setClearanceP p cnew = do
-  LIOState l c <- getLIOStateTCB
-  unless (canFlowToP p cnew c) $! throwLIO InsufficientPrivs
-  unless (l `canFlowTo` cnew)  $! throwLIO CurrentLabelViolation
+  LIOState { lioLabel = l, lioClearance = c } <- getLIOStateTCB
+  unless (canFlowTo l cnew && canFlowToP p cnew c) $
+    labelErrorP "setClearanceP" p [cnew]
   putLIOStateTCB $ LIOState l cnew
 
 -- | Runs an 'LIO' action and re-sets the current clearance to its
@@ -166,21 +167,26 @@
 -- be caught outside a second @scopeClearance@ that restores the
 -- clearance to higher than the current label.
 scopeClearance :: Label l => LIO l a -> LIO l a
-scopeClearance lio = LIOTCB $ \sp -> do
+scopeClearance (LIOTCB action) = LIOTCB $ \sp -> do
   LIOState _ c <- readIORef sp
-  ea <- IO.try $ unLIOTCB lio sp
+  ea <- IO.try $ action sp
   LIOState l _ <- readIORef sp
   writeIORef sp (LIOState l c)
   if l `canFlowTo` c
     then either (IO.throwIO :: SomeException -> IO a) return ea
-    else IO.throwIO ClearanceViolation
+    else IO.throwIO LabelError { lerrContext = []
+                               , lerrFailure = "scopeClearance"
+                               , lerrCurLabel = l
+                               , lerrCurClearance = c
+                               , lerrPrivs = []
+                               , lerrLabels = [] }
 
--- | Lowers the clearance of a computation, then restores the
--- clearance to its previous value (actually, to the upper bound of
--- the current label and previous value).  Useful to wrap around a
--- computation if you want to be sure you can catch exceptions thrown
--- by it. The supplied clearance label must be bounded by the current
--- label and clearance as enforced by 'guardAlloc'.
+-- | Temporarily lowers the clearance for a computation, then restores
+-- it.  Equivalent to:
+--
+-- @
+-- withClearance c lio = 'scopeClearance' $ 'setClearance' c >> lio
+-- @
 -- 
 -- Note that if the computation inside @withClearance@ acquires any
 -- 'Priv's, it may still be able to raise its clearance above the
@@ -188,63 +194,17 @@
 withClearance :: Label l => l -> LIO l a -> LIO l a
 withClearance c lio = scopeClearance $ setClearance c >> lio
 
--- | Same as 'withClearance', but uses privileges when applying
--- 'guardAllocP' to the supplied label.
+-- | A variant of 'withClearance' that takes privileges.  Equivalent
+-- to:
+--
+-- @
+-- withClearanceP p c lio = 'scopeClearance' $ 'setClearanceP' p c >> lio
+-- @
 withClearanceP :: PrivDesc l p => Priv p -> l -> LIO l a -> LIO l a
 withClearanceP p c lio = scopeClearance $ setClearanceP p c >> lio
 
 
 --
--- Exceptions thrown by LIO
---
-
-{- $lioExceptions
-
-Library functions throw an exceptions before an IFC violation can take
-place. 'MonitorFailure' should be used when the reason for failure is
-sufficiently described by the type. Otherwise, 'VMonitorFailure'
-(i.e., \"Verbose\"-'MonitorFailure') should be used to further
-describe the error.
-
--}
-
--- | Exceptions thrown when some IFC restriction is about to be
--- violated.
-data MonitorFailure = ClearanceViolation
-                    -- ^ Current label would exceed clearance, or
-                    -- object label is above clearance.
-                    | CurrentLabelViolation
-                    -- ^ Clearance would be below current label, or
-                    -- object label is not above current label.
-                    | InsufficientPrivs
-                    -- ^ Insufficient privileges. Thrown when lowering
-                    -- the current label or raising the clearance
-                    -- cannot be accomplished with the supplied
-                    -- privileges.
-                    | CanFlowToViolation
-                    -- ^ Generic can-flow-to failure, use with
-                    -- 'VMonitorFailure'
-                    | ResultExceedsLabel
-                    deriving (Show, Typeable)
-
-instance Exception MonitorFailure
-
--- | Verbose version of 'MonitorFailure' also carrying around a
--- detailed message.
-data VMonitorFailure = VMonitorFailure { monitorFailure :: MonitorFailure
-                                       -- ^ Generic monitor failure.
-                                       , monitorMessage :: String
-                                       -- ^ Detailed message of failure.
-                                       }
-                    deriving Typeable
-
-instance Show VMonitorFailure where
-  show m = (show $ monitorFailure m) ++ ": " ++ (monitorMessage m)
-
-instance Exception VMonitorFailure
-
-
---
 -- Guards
 --
 
@@ -260,9 +220,9 @@
      that @ldata ``canFlowTo`` lcurrent@.  This check is performed by
      the 'taint' function, so named because it \"taints\" the current
      'LIO' context by raising @lcurrent@ until @ldata ``canFlowTo``
-     lcurrent@.  (Specifically, it does this by computing the
-     least 'upperBound' of the two labels.) However, this is done
-     only if the new @lcurrent ``canFlowTo`` ccurrent@.
+     lcurrent@.  Specifically, it does this by computing the least
+     upper bound or 'lub' of the two labels.  (Note 'taint' will fail
+     if the new label cannot flow to the current clearance.)
 
    * When /creating/ or /allocating/ objects, it is permissible for
      them to be higher than the current label, so long as they are
@@ -279,13 +239,12 @@
      can flow to the current label, then throws an exception if
      @lcurrent@ cannot flow back to the target label.
 
-     Note that in this case a write /always/ implies a read. Hence,
-     when writing to an object for which you can observe the result,
-     you must use 'guardWrite'. However, when performing a write for
-     which there is no observable side-effects to the writer, i.e.,
-     you cannot observe the success or failure of the write, then it
-     is safe to solely use 'guardAlloc'.
-
+Note that a write /always/ implies a read.  Hence, when writing to an
+object for which you can observe the result (which is frequently the
+case), you must use 'guardWrite'.  However, when performing a write
+for which there are no observable side-effects to the writer, i.e.,
+you cannot observe the success or failure of the write, then it is
+safe to use 'guardAlloc'.
 
 The 'taintP', 'guardAllocP',  and 'guardWriteP' functions are variants
 of the above that take privilege to be more permissive and raise the
@@ -304,22 +263,20 @@
 -- Similarly use this guard in any code that writes to an
 -- object labeled @l@ for which the write has no observable
 -- side-effects.
---
--- If the label does not flow to clearance 'ClearanceViolation' is
--- thrown; if the current label does not flow to the argument label
--- 'CurrentLabelViolation' is thrown.
 guardAlloc :: Label l => l -> LIO l ()
-guardAlloc = guardAllocP noPrivs
+guardAlloc newl = do
+  LIOState { lioLabel = l, lioClearance = c } <- getLIOStateTCB
+  unless (canFlowTo l newl && canFlowTo newl c) $
+    labelError "guardAllocP" [newl]
 
 -- | Like 'guardAlloc', but takes privilege argument to be more
 -- permissive.  Note: privileges are /only/ used when checking that
 -- the current label can flow to the given label.
 guardAllocP :: PrivDesc l p => Priv p -> l -> LIO l ()
 guardAllocP p newl = do
-  c <- getClearance
-  l <- getLabel
-  unless (canFlowToP p l newl) $! throwLIO CurrentLabelViolation
-  unless (newl `canFlowTo` c)  $! throwLIO ClearanceViolation
+  LIOState { lioLabel = l, lioClearance = c } <- getLIOStateTCB
+  unless (canFlowToP p l newl && canFlowTo newl c) $
+    labelErrorP "guardAllocP" p [newl]
 
 --
 -- Read
@@ -327,10 +284,15 @@
 
 -- | Use @taint l@ in trusted code before observing an object labeled
 -- @l@.  This will raise the current label to a value @l'@ such that
--- @l ``canFlowTo`` l'@, or throw 'ClearanceViolation' if @l'@ would
--- have to be higher than the current clearance.
+-- @l ``canFlowTo`` l'@, or throw a 'LabelError' exception if @l'@
+-- would have to be higher than the current clearance.
 taint :: Label l => l -> LIO l ()
-taint = taintP noPrivs
+taint newl = do
+  LIOState { lioLabel = l, lioClearance = c } <- getLIOStateTCB
+  let l' = l `lub` newl
+  unless (l' `canFlowTo` c) $ labelError "taint" [newl]
+  modifyLIOStateTCB $ \s -> s { lioLabel = l' }
+  
 
 -- | Like 'taint', but use privileges to reduce the amount of taint
 -- required.  Note that @taintP@ will never lower the current label.
@@ -338,40 +300,41 @@
 -- 'taint' would raise it.
 taintP :: PrivDesc l p => Priv p -> l -> LIO l ()
 taintP p newl = do
-  c <- getClearance
-  l <- getLabel
-  let l' = partDowngradeP p newl l
-  unless (l' `canFlowTo` c) $! throwLIO ClearanceViolation
+  LIOState { lioLabel = l, lioClearance = c } <- getLIOStateTCB
+  let l' = l `lub` downgradeP p newl
+  unless (l' `canFlowTo` c) $ labelErrorP "taintP" p [newl]
   modifyLIOStateTCB $ \s -> s { lioLabel = l' }
 
 
 -- | Use @guardWrite l@ in any (trusted) code before modifying an
--- object labeled @l@, for which a the modification can be observed,
+-- object labeled @l@, for which the modification can be observed,
 -- i.e., the write implies a read.
 --
 -- The implementation of @guardWrite@ is straight forward:
 --
--- > guardWrite l = taint l >> guardAlloc l
+-- > guardWrite l = guardAlloc l >> taint l
 --
 -- This guarantees that @l@ ``canFlowTo`` the current label (and
 -- clearance), and that the current label ``canFlowTo`` @l@.
 --
 guardWrite :: Label l => l -> LIO l ()
-guardWrite = guardWriteP noPrivs
+guardWrite newl = withContext "guardWrite" $ do
+  guardAlloc newl
+  taint newl
 
--- | Like 'guardWrite', but takes privilege argument to be more
+-- | Like 'guardWrite', but takes a privilege argument to be more
 -- permissive.
 guardWriteP :: PrivDesc l p => Priv p -> l -> LIO l ()
-guardWriteP p newl = do
-  taintP      p newl
+guardWriteP p newl = withContext "guardWriteP" $ do
   guardAllocP p newl
+  taintP p newl
 
 --
 -- Monad base
 --
 
 -- | Synonym for monad in which 'LIO' is the base monad.
-class (Monad m, Label l) => MonadLIO l m | m -> l where
+class (Label l, Monad m) => MonadLIO l m | m -> l where
   -- | Lift an 'LIO' computation.
   liftLIO :: LIO l a -> m a
 
diff --git a/LIO/DCLabel.hs b/LIO/DCLabel.hs
--- a/LIO/DCLabel.hs
+++ b/LIO/DCLabel.hs
@@ -1,116 +1,504 @@
 {-# LANGUAGE Trustworthy #-}
-{-# LANGUAGE MultiParamTypeClasses,
-             ConstraintKinds,
-             TypeSynonymInstances #-}
+{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
 
 {-|
 
 /Disjunction Category Labels/ ('DCLabel's) are a label format that
-encode secrecy and integrity using propositional logic.  This exports
-label operators and instances for the "LIO". The label format is
-documented in "LIO.DCLabel.Core", privileges are described in
-"LIO.DCLabel.Privs", and a domain specific language for constructing
-labels is presented in "LIO.DCLabel.DSL".
+encodes authority, secrecy restrictions, and integrity properties
+using propositional logic.
 
+A 'DCLabel' consists of two boolean formulas over 'Principal's.  Each
+formula is in conjunctive normal form, represented by type 'CNF'.  The
+first 'CNF' ('dcSecrecy') specifies what combinations of principals
+are allowed to make data public.  The second 'CNF' ('dcIntegrity')
+specifies which combinations of principals have endorsed the integrity
+of the data.
+
+The '%%' operator allows one to construct a 'DCLabel' by joining a
+secrecy 'CNF' on the left with an integrity 'CNF' on the right.  A
+'DCLabel' can also be directly constructed with the constructor
+'DCLabel'.  However, '%%' has the added convenience of accepting any
+argument types that are instances of 'ToCNF'.
+
+For example, the following expresses data that can be exported by the
+principal \"Alice\" and may have been written by anybody:  @\"Alice\"
+'%%' 'True'@.  (@'toCNF' 'True'@ indicates a trivially satisfiable
+label component, which in this case means a label conveying no
+integrity properties.)
+
+A 'CNF' is created using the ('\/') and ('/\') operators.  The
+disjunction operator ('\/') is used to compute a 'CNF' equivalent to
+the disjunciton of two 'Principal's, 'Strings', or 'CNF's. For
+example:
+
+  @
+p1 = 'principal' \"p1\"
+p2 = 'principal' \"p2\"
+p3 = 'principal' \"p3\"
+e1 = p1 '\/' p2
+e2 = e1 '\/' \"p4\"
+  @
+
+Similarly, the conjunction operator ('/\') creates 'CNF' as a
+conjunction of 'Principal's, 'String's, 'Disjunction's, or 'CNF's.
+
+  @
+e3 = p1 '\/' p2
+e4 = e1 '/\' \"p4\" '/\' p3
+  @
+
+Note that because a 'CNF' formula is stored as a conjunction of
+'Disjunction's, it is much more efficient to apply '/\' to the result
+of '\/' than vice versa.  It would be logical for '/\' to have higher
+fixity than '\/'.  Unfortunately, this makes formulas harder to read
+(given the convention of AND binding more tightly than OR).  Hence
+'\/' and '/\' have been given the same fixity but different
+associativities, preventing the two from being mixed in the same
+expression without explicit parentheses.
+
+Consider the following, example:
+
+  @
+cnf1 = (\"Alice\" '\/' \"Bob\") '/\' \"Carla\"
+cnf2 = \"Alice\" '/\' \"Carla\"
+dc1 = cnf1 '%%' cnf2
+dc2 = \"Djon\" '%%' \"Alice\"
+pr = PrivTCB $ \"Alice\" '/\' \"Carla\"
+  @
+
+This will result in the following:
+
+>>> dc1
+"Carla" /\ ("Alice" \/ "Bob") %% "Alice" /\ "Carla"
+>>> dc2
+"Djon" %% "Alice"
+>>> canFlowTo dc1 dc2
+False
+>>> canFlowToP pr dc1 dc2
+True
+
 -}
 
 module LIO.DCLabel (
-  -- ** Principals
-    Principal(..), principal
-  -- ** Clauses
-  , Clause, clause
-  -- ** Components
-  , Component, dcTrue, dcFalse, dcFormula
-  , isTrue, isFalse
-  -- ** Labels
-  , DCLabel, dcSecrecy, dcIntegrity, dcLabel
-  , dcPub, dcTop, dcBottom
-  -- ** Privileges
-  , module LIO.DCLabel.Privs
-  -- ** DSL
-  , module LIO.DCLabel.DSL
-  -- * Synonyms for "LIO"
-  -- $dcMonad
-  , DCState, defaultState
-  , DC, evalDC, runDC, tryDC
-  , MonadDC
-  -- ** Labeled values
-  , DCLabeled
-  -- ** Labeled references
-  , DCRef
-  -- ** Gates
-  , DCGate
+  -- * Top-level aliases and functions
+    DC, DCPriv, DCLabeled, dcDefaultState, evalDC, tryDC
+  -- * Main types and functions
+  , Principal, principalBS, principal
+  , DCLabel(..), dcPublic, (%%), (/\), (\/)
+  , CNF, ToCNF(..)
+  -- * Lower-level functions
+  , principalName
+  , Disjunction, dToSet, dFromList
+  , cTrue, cFalse, cToSet, cFromList
   ) where
 
-import qualified Control.Exception as IO
+import safe Control.Applicative
+import safe Data.Bits
+import safe qualified Data.ByteString as S
+import Data.Hashable
+import safe Data.List
+import safe Data.Monoid
+import safe Data.Set (Set)
+import safe qualified Data.Set as Set
+import safe Data.String
+import safe Data.Typeable
+import safe Data.Word
+import safe Text.Read
 
-import LIO.Core
-import LIO.Labeled
-import LIO.Privs
-import LIO.LIORef
-import LIO.DCLabel.Core
-import LIO.DCLabel.Privs
-import LIO.DCLabel.DSL
+import safe LIO.Exception (SomeException)
+import safe LIO.Core
+import safe LIO.Label
+import safe LIO.Labeled
+import safe LIO.Run
 
+type SetTag = Word64
+
 --
--- LIO synonyms
+-- Principals
 --
 
+-- | A @Principal@ is a primitive source of authority, represented as
+-- a string.  The interpretation of principal strings is up to the
+-- application.  Reasonable schemes include encoding user names,
+-- domain names, and/or URLs in the 'Principal' type.
+data Principal = Principal !S.ByteString {-# UNPACK #-} !SetTag
+                 deriving (Ord, Typeable)
 
--- | DC 'Labeled' values.
-type DCLabeled = Labeled DCLabel
+instance Show Principal where
+  showsPrec _ (Principal n _) = shows n
 
--- | DC Labeled 'LIORef's.
-type DCRef a = LIORef DCLabel a
+instance Read Principal where
+  readsPrec d s = do
+    (name, rest) <- readsPrec d s
+    return (principalBS name, rest)
 
+instance Eq Principal where
+  (Principal n1 t1) == (Principal n2 t2) = t1 == t2 && n1 == n2
 
--- | DC 'Gate'.
-type DCGate = Gate DCPrivDesc
+-- | Extract the name of a principal as a strict 'S.ByteString'.
+-- (Use 'show' to get it as a regular 'String'.)
+principalName :: Principal -> S.ByteString
+{-# INLINE principalName #-}
+principalName (Principal n _) = n
 
+-- | Create a principal from a strict 'S.ByteString'.
+principalBS :: S.ByteString -> Principal
+principalBS bs = Principal bs bloom
+  where hv = hash bs
+        bloom = bit (hv .&. 0x3f)
+                .|. (bit $ shiftR hv 6 .&. 0x3f)
+                .|. (bit $ shiftR hv 12 .&. 0x3f)
+
+-- | Create a principal from a 'String'.  The 'String' is packed into
+-- a 'S.ByteString' using 'fromString', which will almost certainly
+-- give unexpected results for non-ASCII unicode code points.
+principal :: String -> Principal
+principal = principalBS . fromString
+
 --
--- DC monad
+-- Disjunctive clauses (a.k.a. "disjunction categories")
 --
 
-{- $dcMonad
+-- | Represents a disjunction of 'Principal's, or one clause of a
+-- 'CNF'.  There is generally not much need to work directly with
+-- @Disjunction@s unless you need to serialize and de-serialize them
+-- (by means of 'dToSet' and 'dFromList').
+data Disjunction = Disjunction !(Set Principal) {-# UNPACK #-} !SetTag
+                   deriving (Typeable)
 
-The 'DC' monad is 'LIO' with using 'DCLabel's as the label format.
-Most application should be written in terms of this monad, while most
-libraries should remain polymorphic in the label type. It is important
-that any *real* application set the initial current label and
-clearance to values other than 'bottom' and 'top' as set by
-'defaultState', respectively. In most cases the initial current label
-should be public, i.e., 'dcPub'.
+-- | Expose the set of 'Principal's being ORed together in a
+-- 'Disjunction'.
+dToSet :: Disjunction -> Set Principal
+dToSet (Disjunction ps _) = ps
 
--}
+instance Eq Disjunction where
+  (Disjunction ps1 t1) == (Disjunction ps2 t2) = t1 == t2 && ps1 == ps2
 
--- | Type synonym for 'MonadLIO'.
-type MonadDC m = MonadLIO DCLabel m
+instance Ord Disjunction where
+  compare (Disjunction ps1 _) (Disjunction ps2 _) =
+    case compare (Set.size ps1) (Set.size ps2) of
+      EQ -> compare ps1 ps2
+      o  -> o
 
--- | 'LIOState' with underlying label being 'DCLabel'
-type DCState = LIOState DCLabel
+instance Show Disjunction where
+  showsPrec _ (Disjunction ps _)
+    | Set.size ps == 0 = ("False" ++)
+    | Set.size ps == 1 = shows $ Set.findMin ps
+    | otherwise = showParen True $
+        foldr1 (\l r -> l . (" \\/ " ++) . r) $ map shows $ Set.toList ps
 
--- | Default, starting state for a 'DC' computation. The current label
--- is public (i.e., 'dcPub') and the current clearance is 'top'.
-defaultState :: DCState
-defaultState = LIOState { lioLabel = dcPub
-                        , lioClearance = dcTop }
+-- | Note that a disjunction containing more than one element /must/
+-- be surrounded by parentheses to parse correctly.
+instance Read Disjunction where
+  readPrec = false <++ clause <++ single
+    where false = do False <- readPrec; return dFalse
+          single = dSingleton <$> readPrec
+          clause = parens $ prec minPrec $ do
+            let next = do Symbol "\\/" <- lexP
+                          liftA2 (:) readPrec next
+                       <++ pure []
+            dFromList <$> liftA2 (:) readPrec next
 
--- | The monad for LIO computations using 'DCLabel' as the label.
+instance Monoid Disjunction where
+  mempty = dFalse
+  mappend = dUnion
+
+dFalse :: Disjunction
+dFalse = Disjunction Set.empty 0
+
+dSingleton :: Principal -> Disjunction
+dSingleton p@(Principal _ t) = Disjunction (Set.singleton p) t
+
+dUnion :: Disjunction -> Disjunction -> Disjunction
+dUnion (Disjunction ps1 t1) (Disjunction ps2 t2) =
+  Disjunction (Set.union ps1 ps2) (t1 .|. t2)
+
+-- | Convert a list of 'Principal's into a 'Disjunction'.
+dFromList :: [Principal] -> Disjunction
+dFromList pl = Disjunction (Set.fromList pl) tres
+  where tres = foldl' (\tl (Principal _ tr) -> tl .|. tr) 0 pl
+
+-- | Returns 'True' iff the first disjunction is a subset of the second.
+dImplies :: Disjunction -> Disjunction -> Bool
+dImplies (Disjunction ps1 t1) (Disjunction ps2 t2)
+  | t1 .&. t2 /= t1 = False
+  | otherwise       = ps1 `Set.isSubsetOf` ps2
+
+--
+-- Conjunctive Normal Form (CNF) Formulas
+--
+
+-- | A boolean formula in Conjunctive Normal Form.  @CNF@ is used to
+-- describe 'DCLabel' privileges, as well to provide each of the two
+-- halves of a 'DCLabel'.
+newtype CNF = CNF (Set Disjunction) deriving (Eq, Ord, Typeable)
+
+-- | Convert a 'CNF' to a 'Set' of 'Disjunction's.  Mostly useful if
+-- you wish to serialize a 'DCLabel'.
+cToSet :: CNF -> Set Disjunction
+{-# INLINE cToSet #-}
+cToSet (CNF ds) = ds
+
+instance Show CNF where
+  showsPrec d (CNF ds)
+    | Set.size ds == 0 = ("True" ++)
+    | Set.size ds == 1 = shows $ Set.findMin ds
+    | otherwise = showParen (d > 7) $
+        foldr1 (\l r -> l . (" /\\ " ++) . r) $ map shows $ Set.toList ds
+
+instance Read CNF where
+  readPrec = true <++ formula <++ single
+    where true = do True <- readPrec; return cTrue
+          single = cSingleton <$> readPrec
+          formula = parens $ prec 7 $ do
+            let next = do Symbol "/\\" <- lexP
+                          liftA2 (:) readPrec next
+                       <++ pure []
+            cFromList <$> liftA2 (:) readPrec next
+
+instance Monoid CNF where
+  mempty = cTrue
+  mappend = cUnion
+  
+-- | A 'CNF' that is always @True@--i.e., trivially satisfiable.  When
+-- @'dcSecrecy' = cTrue@, it means data is public.  When
+-- @'dcIntegrity' = cTrue@, it means data carries no integrity
+-- guarantees.  As a description of privileges, @cTrue@ conveys no
+-- privileges; @'canFlowToPrivDesc' cTrue l1 l2@ is equivalent to
+-- @'canFlowTo' l1 l2@.
+--
+-- Note that @'toCNF' 'True' = cTrue@.  Hence @'dcPublic' = 'DCLabel'
+-- cTrue cTrue@.
+cTrue :: CNF
+cTrue = CNF $ Set.empty
+
+-- | A 'CNF' that is always @False@.  If @'dcSecrecy' = cFalse@, then
+-- no combination of principals is powerful enough to make the data
+-- public.  For that reason, @cFalse@ generally shouldn't appear in a
+-- data label.  However, it is convenient to include as the
+-- 'dcSecrecy' component of 'lioClearance' to indicate a thread may
+-- arbitrarily raise its label.
+--
+-- @'dcIntegrity' = cFalse@ indicates impossibly much integrity--i.e.,
+-- data that no combination of principals is powerful enough to modify
+-- or have created.  Generally this is not a useful concept.
+--
+-- As a privilege description, @cFalse@ indicates impossibly high
+-- privileges (i.e., higher than could be achieved through any
+-- combination of 'Principal's).  @cFalse ``speaksFor`` p@ for any
+-- 'CNF' @p@.  This can be a useful concept for bootstrapping
+-- privileges within the 'DC' monad itself.  For instance, the result
+-- of @'privInit' cFalse@ can be passed to fully-trusted 'DC' code,
+-- which can in turn use 'delegate' to create arbitrary finite
+-- privileges to pass to less privileged code.
+cFalse :: CNF
+cFalse = CNF $ Set.singleton dFalse
+
+cSingleton :: Disjunction -> CNF
+cSingleton = CNF . Set.singleton
+
+setAny :: (a -> Bool) -> Set a -> Bool
+setAny prd = Set.foldr' (\a -> (prd a ||)) False
+
+setAll :: (a -> Bool) -> Set a -> Bool
+setAll prd = Set.foldr' (\a -> (prd a &&)) True
+
+cInsert :: Disjunction -> CNF -> CNF
+cInsert dnew c@(CNF ds)
+  | setAny (`dImplies` dnew) ds = c
+  | otherwise = CNF $ Set.insert dnew $ Set.filter (not . (dnew `dImplies`)) ds
+
+cUnion :: CNF -> CNF -> CNF
+cUnion c (CNF ds) = Set.foldr cInsert c ds
+
+cOr :: CNF -> CNF -> CNF
+cOr (CNF ds1) (CNF ds2) =
+  cFromList $ [dUnion d1 d2 | d1 <- Set.toList ds1, d2 <- Set.toList ds2]
+
+-- | Convert a list of 'Disjunction's into a 'CNF'.  Mostly useful if
+-- you wish to de-serialize a 'CNF'.
+cFromList :: [Disjunction] -> CNF
+cFromList = Set.foldr cInsert cTrue . Set.fromList
+
+cImplies1 :: CNF -> Disjunction -> Bool
+cImplies1 (CNF ds) d = setAny (`dImplies` d) ds
+
+cImplies :: CNF -> CNF -> Bool
+cImplies c (CNF ds) = setAll (c `cImplies1`) ds
+
+--
+-- DCLabel
+--
+
+-- | Main DCLabel type.  @DCLabel@s use 'CNF' boolean formulas over
+-- principals to express authority exercised by a combination of
+-- principals.  A @DCLabel@ contains two 'CNF's.  One, 'dcSecrecy',
+-- specifies the minimum authority required to make data with the
+-- label completely public.  The second, 'dcIntegrity', expresses the
+-- minimum authority that was used to endorse data with the label, or,
+-- for mutable objects, the minimum authority required to modify the
+-- object.
+--
+-- @DCLabel@s are more conveniently expressed using the '%%' operator,
+-- with 'dcSecrecy' on the left and 'dcIntegrity' on the right, i.e.:
+-- @(@/dcSecrecyValue/ '%%' /dcIntegrityValue/@)@.
+--
+-- @DCLabel@s enforce the following relations:
+--
+--   * If @cnf1@ and @cnf2@ are 'CNF's describing authority, then
+--   @cnf1 ``speaksFor`` cnf2@ if and only if @cnf1@ logically implies
+--   @cnf2@ (often written @cnf1 &#x27f9; cnf2@).  For example,
+--   @(\"A\" '/\' \"B\") ``speaksFor`` 'toCNF' \"A\"@, while @'toCNF'
+--   \"A\" ``speaksFor`` (\"A\" '\/' \"C\")@.
+--
+--   * Given two @DCLabel@s @dc1 = (s1 '%%' i1)@ and @dc2 = (s2 '%%'
+--   i2)@, @dc1 ``canFlowTo`` dc2@ (often written @dc1@ &#8849; @dc2@)
+--   if and only if @s2 ``speaksFor`` s1 && i1 ``speaksFor`` i2@.  In
+--   other words, data can flow in the direction of requiring more
+--   authority to make it public or removing integrity endorsements.
+--
+--   * Given two @DCLabel@s @dc1 = (s1 '%%' i1)@ and @dc 2 = (s2 '%%'
+--   i2)@, and a @p::'CNF'@ representing privileges,
+--   @'canFlowToPrivDesc' p dc1 dc2@ (often written @dc1@
+--   &#8849;&#8346; @dc2@) if and only if @(p '/\' s2) ``speaksFor``
+--   s2 && (p '/\' i1) ``speaksFor`` i2@.
+data DCLabel = DCLabel { dcSecrecy :: !CNF
+                         -- ^ Describes the authority required to make
+                         -- the data public.
+                       , dcIntegrity :: !CNF
+                         -- ^ Describes the authority with which
+                         -- immutable data was endorsed, or the
+                         -- authority required to modify mutable data.
+                       } deriving (Eq, Ord, Typeable)
+
+instance Show DCLabel where
+  showsPrec d (DCLabel sec int) =
+    showParen (d > 5) $ shows sec . (" %% " ++) . shows int
+
+instance Read DCLabel where
+  readPrec = parens $ prec 5 $ do
+    sec <- readPrec
+    Symbol "%%" <- lexP
+    int <- readPrec
+    return $ DCLabel sec int
+
+-- |
+-- > dcPublic = True %% True
+--
+-- This label corresponds to public data with no integrity guarantees.
+-- For instance, an unrestricted Internet socket should be labeled
+-- @dcPublic@.  The significance of @dcPublic@ is that given data
+-- labeled @(s %% i)@, @s@ is the exact minimum authority required to
+-- transition the data to @dcPublic@.  Conversely, given data labeled
+-- @dcPublic@, @i@ is the exact authority required to transition the
+-- data to @(s %% i)@ (assuming sufficient clearance).
+dcPublic :: DCLabel
+dcPublic = True %% True
+
+-- | As a type, a 'CNF' is always a conjunction of 'Disjunction's of
+-- 'Principal's.  However, mathematically speaking, a single
+-- 'Principal' or single 'Disjunction' is also a degenerate example of
+-- conjunctive normal form.  Class 'ToCNF' abstracts over the
+-- differences between these types, promoting them all to 'CNF'.
+class ToCNF c where toCNF :: c -> CNF
+instance ToCNF CNF where toCNF = id
+instance ToCNF (Priv CNF) where toCNF = privDesc
+instance ToCNF Disjunction where toCNF = cSingleton
+instance ToCNF Principal where toCNF = toCNF . dSingleton
+instance ToCNF [Char] where toCNF = toCNF . principal
+instance ToCNF Bool where
+  toCNF True = cTrue
+  toCNF False = cFalse
+
+-- | The primary way of creating a 'DCLabel'.  The secrecy component
+-- goes on the left, while the integrity component goes on the right,
+-- e.g.:
+--
+-- > label = secrecyCNF %% integrityCNF
+--
+-- Unlike the 'DCLabel' constructor, the arguments can be any instance
+-- of 'ToCNF'.  @%%@ has fixity:
+--
+-- > infix 6 %%
+(%%) :: (ToCNF a, ToCNF b) => a -> b -> DCLabel
+a %% b = toCNF a `DCLabel` toCNF b
+infix 6 %%
+
+-- | Compute a conjunction of two 'CNF's or 'ToCNF' instances.
+--
+-- Has fixity:
+--
+-- > infixr 7 /\
+(/\) :: (ToCNF a, ToCNF b) => a -> b -> CNF
+a /\ b = toCNF a `cUnion` toCNF b
+infixr 7 /\
+
+-- | Compute a disjunction of two 'CNF's or 'ToCNF' instances.  Note
+-- that this can be an expensive operation if the inputs have many
+-- conjunctions.
+--
+-- The fixity is specifically chosen so that @&#92;&#47;@ and '/\'
+-- cannot be mixed in the same expression without parentheses:
+--
+-- > infixl 7 \/
+(\/) :: (ToCNF a, ToCNF b) => a -> b -> CNF
+a \/ b = toCNF a `cOr` toCNF b
+infixl 7 \/
+
+instance Label DCLabel where
+  lub (DCLabel s1 i1) (DCLabel s2 i2) = DCLabel (cUnion s1 s2) (cOr i1 i2)
+  glb (DCLabel s1 i1) (DCLabel s2 i2) = DCLabel (cOr s1 s2) (cUnion i1 i2)
+  canFlowTo (DCLabel s1 i1) (DCLabel s2 i2) = cImplies s2 s1 && cImplies i1 i2
+
+instance SpeaksFor CNF where
+  {-# INLINE speaksFor #-}
+  speaksFor = cImplies
+
+dcMaxDowngrade :: CNF -> DCLabel -> DCLabel
+dcMaxDowngrade p (DCLabel (CNF ds) int) = DCLabel sec (cUnion p int)
+  where sec = CNF $ Set.filter (not . cImplies1 p) ds
+
+instance PrivDesc DCLabel CNF where
+  downgradeP = dcMaxDowngrade
+  canFlowToP p (DCLabel s1 i1) (DCLabel s2 i2) =
+    cImplies (cUnion p s2) s1 && cImplies (cUnion p i1) i2
+
+--
+-- Type aliases
+--
+
+-- | A common default starting state, where @'lioLabel' = 'dcPublic'@
+-- and @'lioClearance' = False '%%' True@ (i.e., the highest
+-- possible clearance).
+dcDefaultState :: LIOState DCLabel
+dcDefaultState = LIOState { lioLabel = dcPublic
+                          , lioClearance = False %% True }
+
+-- | The main monad type alias to use for 'LIO' computations that are
+-- specific to 'DCLabel's.
 type DC = LIO DCLabel
 
+-- | 'DCLabel' privileges are expressed as a 'CNF' of the principals
+-- whose authority is being exercised.
+type DCPriv = Priv CNF
 
--- | Evaluate computation in the 'DC' monad.
-evalDC :: DC a -> IO a
-evalDC act = evalLIO act defaultState
+-- | An alias for 'Labeled' values labeled with a 'DCLabel'.
+type DCLabeled = Labeled DCLabel
 
--- | Evaluate computation in the 'DC' monad.
-runDC :: DC a -> IO (a, DCState)
-runDC act = runLIO act defaultState
+-- | Wrapper function for running @'LIO' 'DCLabel'@ computations.
+--
+-- @
+-- evalDC dc = 'evalLIO' dc 'dcDefaultState'
+-- @
+evalDC :: DC a -> IO a
+evalDC dc = evalLIO dc dcDefaultState
 
--- | Similar to 'evalLIO', but catches any exceptions thrown by
--- untrusted code with 'throwLIO'.
-tryDC :: DC a -> IO (Either IO.SomeException a, DCState)
-tryDC act = runDC act >>= tryit
-  where tryit (a, s) = do
-          ea <- IO.try (IO.evaluate a)
-          return (ea, s)
+-- | 'DCLabel' wrapper for 'tryLIO':
+--
+-- @
+-- tryDC dc = 'tryLIO' dc 'dcDefaultState'
+-- @
+tryDC :: DC a -> IO (Either SomeException a, LIOState DCLabel)
+tryDC dc = tryLIO dc dcDefaultState
diff --git a/LIO/DCLabel/Core.hs b/LIO/DCLabel/Core.hs
deleted file mode 100644
--- a/LIO/DCLabel/Core.hs
+++ /dev/null
@@ -1,318 +0,0 @@
-{-# LANGUAGE Safe #-}
-{-# LANGUAGE DeriveDataTypeable #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-|
-
-This module implements Disjunction Category Labels (DCLabels).
-DCLabels is a label format for information flow control (IFC) systems.
-This library exports relevant data types and operations that may be
-used by dynamic IFC systems such as the "LIO" library.
-
-A 'DCLabel' is a pair of /secrecy/ and /integrity/ 'Component's
-(sometimes called category sets).  Each 'Component' (or formula) is a
-conjunction (implemented in terms of 'Set's) of 'Clause's (or
-category) in propositional logic (without negation) specifying a
-restriction on the flow of information labeled as such. Alternatively,
-a 'Component' can take on the value 'DCFalse' corresponding to
-falsehood.  Each 'Clause', in turn, is a disjunction of 'Principal's,
-, where a 'Principal' is a source of authority of type 'ByteString',
-whose meaning is application-specific (e.g., a 'Principal' can be a
-user name, a URL, etc.).
-
-A clause imposes an information flow restriction. In the case of
-secrecy, a clause restricts who can read, receive, or propagate the
-information, while in the case of integrity it restricts who can
-modify a piece of data. The principals composing a clause are said to
-/own/ the clause or category.
-
-For information to flow from a source labeled @L_1@ to a sink @L_2@, the
-restrictions imposed by the clauses of @L_2@ must at least as restrictive as
-all the restrictions imposed by the clauses of @L_1@ (hence the conjunction)
-in the case of secrecy, and at least as permissive in the case of integrity.
-More specifically, for information to flow from @L_1@ to @L_2@, the labels
-must satisfy the \"can-flow-to\" relation: @L_1 &#8849; L_2@.  The &#8849;
-label check is implemented by the 'canFlowTo' function.  For labels
-@L_1=\<S_1, I_1\>@, @L_2=\<S_2, I_2\>@ the can-flow-to relation is satisfied
-if the secrecy component @S_2@ /implies/ @S_1@ and @I_1@ /implies/ @I_2@
-(recall that a category set is a conjunction of disjunctions of principals).
-For example, @\<P_1 &#8897; P_2, True\> &#8849; \<P_1, True\>@ because data
-that can be read by @P_1@ is more restricting than that readable by @P_1@
-or @P_2@. Conversely, @\<True,P_1\> &#8849; \<True,P_1 &#8897; P_2\>@
-because data vouched for by @P_1@ or @P_2@ is more permissive than just @P_1@
-(note the same principle holds when writing to sinks with such labeling).
-
--}
-
-module LIO.DCLabel.Core ( 
-  -- * Principals
-    Principal(..), principal
-  -- * Clauses
-  , Clause(..), clause
-  -- * Components
-  -- $component
-  , Component(..)
-  , dcTrue, dcFalse, dcFormula 
-  , isTrue, isFalse
-  -- * Labels
-  , DCLabel(..), dcLabel, dcLabelNoReduce
-  , dcPub, dcTop, dcBottom
-  -- * Internal
-  , dcReduce, dcImplies
-  , dcAnd, dcOr
-  ) where
-
-import qualified Data.ByteString.Char8 as S8
-import Data.List (intercalate)
-import Data.Monoid
-import Data.Set (Set)
-import qualified Data.Set as Set
-import Data.Typeable
-
-import LIO.Label
-import LIO.Privs
-
---
--- Principals
---
-
--- | A @Principal@ is a simple string representing a source of
--- authority. Any piece of code can create principals, regardless of how
--- untrusted it is.
-newtype Principal = Principal { principalName :: S8.ByteString
-                                -- ^ Get the principal name.
-                              } deriving (Eq, Ord, Typeable)
-
-instance Show Principal where
-  showsPrec _ = shows . principalName
-
--- | Generate a principal from a 'String'.  (To create one from a
--- 'S8.ByteString', just use the 'Principal' constructor directly.)
-principal :: String -> Principal
-principal = Principal . S8.pack
-
---
--- Category - disjunction clauses
---
-
--- | A clause or disjunction category is a set of 'Principal's.
--- Logically the set corresponds to a disjunction of the principals.
-newtype Clause = Clause { unClause :: Set Principal
-                          -- ^ Get underlying principal-set.
-                        } deriving (Eq, Typeable)
-
-instance Ord Clause where
-  (Clause c1) <= (Clause c2) =
-    case () of
-      _ | Set.size c1 == Set.size c2 -> c1 <= c2
-      _ -> Set.size c1 < Set.size c2
-
-instance Show Clause where
-  show c@(Clause uc)
-         | Set.size uc == 1 = show . head . Set.toList $ uc
-         | otherwise =
-              let ps = map show . Set.toList $! unClause c
-              in parens . intercalate " \\/ " $! ps
-    where parens x = "(" ++ x ++ ")"
-
--- | Clause constructor
-clause :: Set Principal -> Clause
-clause = Clause
-
--- | A component is a set of clauses, i.e., a formula (conjunction of
--- disjunction of 'Principal's). @DCFalse@ corresponds to logical
--- @False@, while @DCFormula Set.empty@ corresponds to logical @True@.
-data Component = DCFalse
-                 -- ^ Logical @False@
-               | DCFormula { unDCFormula :: !(Set Clause) 
-                              -- ^ Get underlying clause-set.
-                           }
-                 -- ^ Conjunction of disjunction categories
-  deriving (Eq, Typeable)
-
-instance Show Component where
-  show c | isFalse c = show False
-         | isTrue c  = show True
-         | otherwise = let cs = map show . Set.toList $! unDCFormula c
-                       in intercalate " /\\ " $! cs
-
--- | Privileges can be combined using 'mappend'
-instance Monoid Component where
-  mempty = dcTrue
-  mappend p1 p2 = dcReduce $! p1 `dcAnd` p2
-
-instance PrivDesc DCLabel Component where
-  canFlowToPrivDesc pd l1 l2
-           | pd == dcTrue = canFlowTo l1 l2
-           | otherwise =
-    let i1 = dcReduce $ dcIntegrity l1 `dcAnd` pd
-        s2 = dcReduce $ dcSecrecy l2   `dcAnd` pd
-    in l1 { dcIntegrity = i1 } `canFlowTo` l2 { dcSecrecy = s2 }
-
-  partDowngradePrivDesc pd la lg
-               | pd == mempty  = la `lub` lg
-               | pd == dcFalse = lg
-               | otherwise = 
-    let sec_a  = dcSecrecy la
-        int_a  = dcIntegrity la
-        sec_g  = dcSecrecy   lg
-        int_g  = dcIntegrity lg
-        sec_a' = dcFormula . Set.filter f $ unDCFormula sec_a
-        sec_res  = if isFalse sec_a
-                then sec_a
-                else sec_a' `dcAnd` sec_g
-        int_res  = (pd `dcAnd` int_a) `dcOr` int_g
-    in dcLabel sec_res int_res
-      where f c = not $ pd `dcImplies` (dcFormula . Set.singleton $ c)
-
-
-
--- | Logical @True@.
-dcTrue :: Component
-dcTrue = DCFormula Set.empty
-
--- | Logical @False@.
-dcFalse :: Component
-dcFalse = DCFalse
-
--- | Arbitrary formula from a clause.
-dcFormula :: Set Clause -> Component
-dcFormula = DCFormula
-
--- | Is the component @True@.
-isTrue :: Component -> Bool
-isTrue = (== dcTrue)
-
--- | Is the component @False@.
-isFalse :: Component -> Bool
-isFalse = (== dcFalse)
-
---
--- Labels
---
-
-{- $component
-   A 'Component' is a conjunction of disjunctions of 'Principal's. A
-   'DCLabel' is simply a pair of such 'Component's. Hence, we define
-   almost all operations in terms of this construct, from which the
-   'DCLabel' implementation follows almost trivially.
--}
-
--- | A @DCLabel@ is a pair of secrecy and integrity 'Component's.
-data DCLabel = DCLabel { dcSecrecy   :: !Component
-                         -- ^ Extract secrecy component of a label
-                       , dcIntegrity :: !Component
-                         -- ^ Extract integrity component of a label
-                       } deriving (Eq, Typeable)
-
-instance Show DCLabel where 
-  showsPrec d l = showParen (d > 5) $
-    let s = dcSecrecy l
-        i = dcIntegrity l
-    in showsPrec (d + 1) s . showString " %% " . showsPrec (d + 1) i
-
--- | @dcLabel secrecyComponent integrityComponent@ creates a label,
--- reducing each component to CNF.
-dcLabel :: Component -> Component -> DCLabel
-dcLabel c1 c2 = DCLabel (dcReduce c1) (dcReduce c2)
-
--- | Label contstructor. Note: the components should already be reduced.
-dcLabelNoReduce :: Component -> Component -> DCLabel
-dcLabelNoReduce = DCLabel
-
-
-
--- | Element in the DCLabel lattice corresponding to the most secret
--- and least trustworthy data.
--- @dcTop = \< False, True \> @.
-dcTop :: DCLabel
-dcTop = dcLabel dcFalse dcTrue
-
--- | Element in the DCLabel lattice corresponding to the least secret
--- and most trustworthy data.
--- @dcTop = \< True, False \> @.
-dcBottom :: DCLabel
-dcBottom = dcLabel dcTrue dcFalse
-
--- | Element in the DCLabel lattice corresponding to public data.
--- @dcPub = \< True, True \> @. This corresponds to data that is not
--- secret nor trustworthy.
-dcPub :: DCLabel
-dcPub = DCLabel { dcSecrecy = dcTrue, dcIntegrity = dcTrue }
-
---
--- Bounded by \< True, False \> and \< False, True \>
---
-instance Bounded DCLabel where
-  minBound = dcBottom
-  maxBound = dcTop
-
---
--- Lattice operations
---
-
-instance Label DCLabel where
-  -- | Partial /can-flow-to/ relation on labels.
-  canFlowTo l1 l2 = (dcSecrecy l2   `dcImplies` dcSecrecy l1) &&
-                    (dcIntegrity l1 `dcImplies` dcIntegrity l2)
-
-
-  -- | The least upper bound of two labels, i.e., the join.
-  lub l1 l2 = DCLabel
-    { dcSecrecy   = dcReduce $ dcSecrecy l1   `dcAnd` dcSecrecy l2
-    , dcIntegrity = dcReduce $ dcIntegrity l1 `dcOr`  dcIntegrity l2 }
-
-  -- | The greatest lower bound of two labels, i.e., the meet.
-  glb l1 l2 = DCLabel
-    { dcSecrecy   = dcReduce $ dcSecrecy l1   `dcOr`  dcSecrecy l2
-    , dcIntegrity = dcReduce $ dcIntegrity l1 `dcAnd` dcIntegrity l2 }
-
---
--- Helpers
---
-
--- | Logical implication.
-dcImplies :: Component -> Component -> Bool
-dcImplies DCFalse _ = True
-dcImplies _ DCFalse = False
-dcImplies f1@(DCFormula cs1) f2@(DCFormula cs2)
-   | isTrue f2 = True
-   | isTrue f1 = False
-   | otherwise = Set.foldl' dcImpliesDisj True cs2
-  where dcImpliesDisj :: Bool -> Clause -> Bool
-        dcImpliesDisj False _ = False
-        dcImpliesDisj _ (Clause c2) = Set.foldl' f False cs1
-          where f True _  = True
-                f _     c1 = unClause c1 `Set.isSubsetOf` c2 
-
--- | Logical conjunction
-dcAnd :: Component -> Component -> Component 
-dcAnd x y | isFalse x || isFalse y = dcFalse
-          | otherwise = DCFormula $! unDCFormula x `Set.union` unDCFormula y
-
--- | Logical disjunction
-dcOr :: Component -> Component -> Component 
-dcOr x y | isTrue x || isTrue y = dcTrue
-dcOr x y | isFalse x = y
-         | isFalse y = x
-         | otherwise = let cs1 = unDCFormula x
-                           cs2 = unDCFormula y
-                       in DCFormula $! doOr cs1 cs2
-  where -- | Perform disjunction of two components.
-        doOr :: Set Clause -> Set Clause -> Set Clause
-        doOr cs1 cs2 = Set.foldl' disjFunc Set.empty cs2
-          where disjFunc acc c = acc `Set.union` singleOr c cs1
-        -- | Given a clause and a formula, perform logical or of
-        -- clause with every clause in formula.
-        singleOr :: Clause -> Set Clause -> Set Clause
-        singleOr (Clause c1) = Set.map (Clause . Set.union c1 . unClause)
-
--- | Reduce component to conjunction normal form by removing clauses
--- implied by other.
-dcReduce :: Component -> Component
-dcReduce f | isFalse f || isTrue f = f
-           | otherwise = DCFormula . doReduce . unDCFormula $ f
-  where doReduce cs | Set.null cs = cs
-        doReduce cs =
-          let (x@(Clause x'), xs) = Set.deleteFindMin cs 
-              ys = doReduce $ Set.filter (not . Set.isSubsetOf x' . unClause) xs
-          in Set.singleton x `Set.union` ys
diff --git a/LIO/DCLabel/DSL.hs b/LIO/DCLabel/DSL.hs
deleted file mode 100644
--- a/LIO/DCLabel/DSL.hs
+++ /dev/null
@@ -1,182 +0,0 @@
-{-# LANGUAGE Safe #-}
-{-# LANGUAGE FlexibleInstances #-}
-
-{-|
-  This module implements a simple, embedded domain specific language
-  to create 'Component's, privilage descriptions and labels from
-  conjunctions of principal disjunctions.
-
-  A 'DCLabel' consists of a secrecy 'Component' and an integrity
-  'Component'.  The '%%' operator allows one to construct a 'DCLabel'
-  by joining a secrecy 'Component' (on the left) with an integrity
-  'Component' on the right.  This is similar to 'dcLabel', except that
-  the arguments can also be instances of 'ToComponent'.  For example,
-  the following expresses data that can be exported by the principal
-  \"Alice\" and written by anybody:  @\"Alice\" '%%' 'True'@.  (The
-  component 'True' or 'dcTrue' indicates a trivially satisfiable label
-  component, which in this case means a label with no integrity
-  guarantees.)
-
-  A 'Component' or 'DCPrivDesc' is created using the ('\/') and ('/\')
-  operators.  The disjunction operator ('\/') is used to create a
-  'Clause' from 'Principal's, ByteStrings, or a disjunctive
-  sub-expression. For example:
-
-  @
-     p1 = 'principal' \"p1\"
-     p2 = 'principal' \"p2\"
-     p3 = 'principal' \"p3\"
-     e1 = p1 '\/' p2
-     e2 = e1 '\/' \"p4\"
-  @
-
-  Similarly, the conjunction operator ('/\') is used to create category-sets
-  from 'Principal's, ByteStrings, and conjunctive or disjunctive sub-expressions.
-  For example:
-
-  @
-     e3 = p1 '\/' p2
-     e4 = e1 '/\' \"p4\" '/\' p3
-  @
-
-  /Note/ that because a clause consists of a disjunction of principals, and a
-  component is composed of the conjunction of categories, ('\/') binds
-  more tightly than ('/\').
-
-  Given two 'Component's, one for secrecy and one for integrity, you
-  can create a 'DCLabel' with 'dcLabel'.  Given a 'DCPriv' and
-  'DCPrivDesc' you can create a new minted privilege with
-  'dcDelegatePriv'.
-  
-  
-  Consider the following, example:
-
-  @
-l1 = \"Alice\" '\/' \"Bob\" '/\' \"Carla\"
-l2 = \"Alice\" '/\' \"Carla\"
-dc1 = 'dcLabel' l1 l2
-dc2 = 'dcLabel' ('toComponent' \"Djon\") ('toComponent' \"Alice\")
-pr = PrivTCB $ toComponent $ \"Alice\" '/\' \"Carla\"
-  @
-
-  This will result in the following:
-
->>> dc1
-"Carla" /\ ("Alice" \/ "Bob") %% "Alice" /\ "Carla"
->>> dc2
-"Djon" %% "Alice"
->>> canFlowTo dc1 dc2
-False
->>> canFlowToP pr dc1 dc2
-True
-
--}
-
-module LIO.DCLabel.DSL (
-  -- * Operators
-    (%%), (\/), (/\), ToComponent(..)
-  , fromList, toList
-  -- * Aliases
-  , impossible, unrestricted
-  ) where
-
-import qualified Data.Set as Set
-
-import LIO.Privs
-import LIO.DCLabel.Core
-
--- | Convert a type (e.g., 'Clause', 'Principal') to a label component.
-class ToComponent a where
-  -- | Convert to 'Component'
-  toComponent :: a -> Component
-
-infix 5 %%
-
--- | Create a `DCLabel` from a secrecy `ToComponent` and integrity
--- `ToComponent`. E.g.:
---
--- @
---   \"secrecy\" %% \"integrity\"
--- @
---
--- @
--- infix 5 %%
--- @
-(%%) :: (ToComponent a, ToComponent b) => a -> b -> DCLabel
-(%%) sec int = dcLabel (toComponent sec) (toComponent int)
-
--- | Identity of 'Component'.
-instance ToComponent Component where
-  {-# INLINE toComponent #-}
-  toComponent = id
-instance ToComponent (Priv Component) where
-  {-# INLINE toComponent #-}
-  toComponent = privDesc
--- | Convert singleton 'Clause' to 'Component'.
-instance ToComponent Clause    where
-  toComponent c = DCFormula $! Set.singleton c
--- | Convert singleton 'Principal' to 'Component'.
-instance ToComponent Principal where
-  toComponent p = toComponent . Clause $! Set.singleton p
-
--- | Convert singleton 'Principal' (in the form of a 'String')to 'Component'.
-instance ToComponent String where
-  toComponent = toComponent . principal
-
-instance ToComponent Bool where
-  {-# INLINE toComponent #-}
-  toComponent True = DCFormula Set.empty
-  toComponent False = DCFalse
-
-infixl 7 \/
-infixl 6 /\
-
--- | Conjunction of two 'Principal'-based elements.
--- 
--- @
--- infixl 6 /&#92;
--- @
---
-(/\) :: (ToComponent a, ToComponent b) => a -> b -> Component
-a /\ b = dcReduce $! toComponent a `dcAnd` toComponent b
-
--- | Disjunction of two 'Principal'-based elements.
--- 
--- @
--- infixl 7 \\/
--- @
---
-(\/) :: (ToComponent a, ToComponent b) => a -> b -> Component
-a \/ b = dcReduce $! toComponent a `dcOr` toComponent b
-
---
--- Aliases
---
-
--- | Logical falsehood can be thought of as the component containing
--- every possible principal, hence impossible to express:
---
--- > impossible = dcFalse
---
-impossible :: Component
-impossible = dcFalse
-
--- | Logical truth can be thought of as the component containing
--- no specific principal, hence imposing no restrictions:
---
--- > unrestricted = dcTrue
---
-unrestricted :: Component
-unrestricted = dcTrue
-
--- | Convert a 'Component' to a list of list of 'Principal's if the
--- 'Component' does not have the value 'DCFalse'. In the latter case
--- the function returns an exception.
-toList :: Component -> [[Principal]]
-toList DCFalse        = error "toList: Invalid use, expected DCFormula"
-toList (DCFormula cs) = map (Set.toList . unClause) $! Set.toList cs
-
--- | Convert a list of list of 'Principal's to a 'Component'. Each
--- inner list is considered to correspond to a 'Clause'.
-fromList :: [[Principal]] -> Component
-fromList ps = DCFormula . Set.fromList $! map (Clause . Set.fromList) ps
diff --git a/LIO/DCLabel/Privs.hs b/LIO/DCLabel/Privs.hs
deleted file mode 100644
--- a/LIO/DCLabel/Privs.hs
+++ /dev/null
@@ -1,78 +0,0 @@
-{-# LANGUAGE Trustworthy #-}
-{- |
-
-Privileges allow a piece of code to bypass certain information flow
-restrictions imposed by labels.  A privilege is simply a conjunction
-of disjunctions of 'Principal's, i.e., a 'Component'. We say that a
-piece of code containing a singleton 'Clause' owns the 'Principal'
-composing the 'Clause'.  However, we allow for the more general notion
-of ownership of a clause, or category, as to create a
-privilege-hierarchy. Specifically, a piece of code exercising a
-privilege @P@ can always exercise privilege @P'@ (instead), if @P' => P@.
-(This is similar to the DLM notion of \"can act for\".) Hence, if a
-piece of code with certain privileges implies a clause, then it is
-said to own the clause. Consequently it can bypass the restrictions of
-the clause in any label.
-
-Note that the privileges form a partial order over logicla implication
-(@=>@), such that @'allPrivTCB' => P@ and @P => 'noPriv'@ for any
-privilege @P@.  Hence, a privilege hierarchy which can be concretely
-built through delegation, with 'allPrivTCB' corresponding to the
-/root/, or all, privileges from which all others may be created. More
-specifically, given a privilege @P'@ of type 'DCPriv', and a privilege
-description @P@ of type 'DCPrivDesc', any piece of code can use
-'delegatePriv' to \"mint\" @P@, assuming @P' => P@.
-
--}
-
-module LIO.DCLabel.Privs (
-    DCPrivDesc
-  , DCPriv
-  -- ** Helpers
-  , noPriv
-  , dcDelegatePriv
-  , dcOwns
-  ) where
-
-import qualified Data.Set as Set
-
-import LIO
-import LIO.DCLabel.Core
-import LIO.TCB
-
--- | A privilege description is simply a conjunction of disjunctions.
--- Unlike (actually minted) privileges (see 'DCPriv'), privilege
--- descriptions may be created by untrusted code.
-type DCPrivDesc = Component
-
--- | A privilege is a minted and protected privilege description
--- ('DCPrivDesc') that may only be created by trusted code or
--- delegated from an existing @DCPriv@.
-type DCPriv = Priv DCPrivDesc
-
---
--- Helpers
---
-
--- | The empty privilege, or no privileges, corresponds to logical
--- @True@.
-noPriv :: DCPriv
-noPriv = PrivTCB dcTrue
-
--- | Given a privilege and a privilege description turn the privilege
--- description into a privilege (i.e., mint). Such delegation succeeds
--- only if the supplied privilege implies the privilege description.
-dcDelegatePriv :: DCPriv -> DCPrivDesc -> Maybe DCPriv
-dcDelegatePriv p pd = let c  = privDesc $! p
-                      in if c `dcImplies` pd
-                           then Just $! PrivTCB pd
-                           else Nothing
-
--- | We say a piece of code having a privilege object (of type 'DCPriv')
--- owns a clause when the privileges allow code to bypass restrictions
--- imposed by the clause. This is the case if and only if the 'DCPriv'
--- object contains one of the 'Principal's in the 'Clause'.  This
--- function can be used to make such checks.
-dcOwns :: DCPrivDesc -> Clause -> Bool
-dcOwns pd c = pd `dcImplies` dcFormula (Set.singleton c)
-
diff --git a/LIO/Delegate.hs b/LIO/Delegate.hs
new file mode 100644
--- /dev/null
+++ b/LIO/Delegate.hs
@@ -0,0 +1,130 @@
+{-# LANGUAGE Trustworthy #-}
+{-# LANGUAGE DeriveDataTypeable #-}
+
+-- | This module provides two functions useful for delegating
+-- privileges.  The 'delegate' function creates a 'Priv' value less
+-- powerful than an existing one.  'Gate's provide a mechanism for
+-- authenticating calls to closures that embed privileges.
+module LIO.Delegate (
+    -- * Delegating privileges
+    delegate
+    -- * Gates
+    -- $gateIntro
+  , Gate, gate, callGate
+    -- ** Gate example
+    -- $gateExample
+  ) where
+
+import safe Data.Typeable
+
+import safe LIO.Error
+import safe LIO.Label
+import LIO.TCB
+
+-- | @delegate@ allows you to create a new privilege object that is
+-- less powerful than an existing privilege object.  The first
+-- argument supplies actual privileges.  The second argument is a
+-- 'PrivDesc' describing the desired new privileges.  The call throws
+-- an exception unless the privileges supplied 'speaksFor' the
+-- privileges requested.
+--
+-- Note:  If you are looking for a way to create privileges /more/
+-- powerful than ones you already have, you can use the 'mappend'
+-- function to combine existing privileges.
+delegate :: (SpeaksFor p) => Priv p -> p -> Priv p
+delegate p1 p2
+  | privDesc p1 `speaksFor` p2 = PrivTCB p2
+  | otherwise                  = insufficientPrivs "delegate" p1 p2
+
+{- $gateIntro
+
+LIO provides a basic implementation of /gates/, useful in providing
+controlled RPC-like services where the client and service provider are
+in mutual distrust. 
+
+A service provider uses 'gate' to create a gate data type @'Gate' p a@
+given a computation of type @p -> a@. Here, @p@ is a privilege
+description (type variable for an instance of 'PrivDesc').  Gates are
+invoked with 'callGate', and as such the service provider has the
+guarantee that the client (the caller) owns the privileges
+corresponding to the privilege description @p@.  In effect, this
+allows a client to \"prove\" to the service provider that they own
+certain privileges without entrusting the service with its privileges.
+The gate computation can analyze this privilege description before
+performing the \"actual\" computation.  The client and server solely
+need to trust the implementation of 'callGate'.
+
+-}
+
+
+-- | A Gate is a lambda abstraction from a privilege description to an
+-- arbitrary type @a@. Applying the gate is accomplished with 'callGate'
+-- which takes a privilege argument that is converted to a description
+-- before invoking the gate computation.
+newtype Gate p a = GateTCB (p -> a) deriving Typeable
+-- Note GateTCB is trusted by convention.  Anyone with access to the
+-- symbol can call any gate while claiming arbitrary privileges.  In
+-- the absence of gates, however, GateTCB doesn't provide any
+-- particular privileges.
+
+-- | Create a gate given a computation from a privilege description.
+-- Note that because of currying type 'a' may itself be a function
+-- type and thus gates can take arguments in addition to the privilege
+-- descriptoin.
+gate :: (p -> a)  -- ^ Gate computation
+     -> Gate p a
+{-# INLINE gate #-}
+gate = GateTCB
+
+-- | Given a gate and privilege, execute the gate computation.  It is
+-- important to note that @callGate@ invokes the gate computation with
+-- the privilege description and /NOT/ the privilege itself.
+--
+-- Note that, in general, code should /not/ provide privileges to
+-- functions other than @callGate@ when wishing to call a gate. This
+-- function is provided by LIO since it can be easily inspected by
+-- both the gate creator and caller to be doing the \"right\" thing:
+-- provide the privilege description corresponding to the supplied
+-- privilege as \"proof\" without explicitly passing in the privilege.
+-- 
+callGate :: Gate p a -- ^ Gate
+         -> Priv p   -- ^ Privilege used as proof-of-ownership
+         -> a
+{-# INLINE callGate #-}
+callGate (GateTCB g) = g . privDesc
+
+{- $gateExample
+
+This example uses "LIO.DCLabel" to demonstrate the use of gates.  The
+service provider provides @addGate@ which adds two integers if the
+gate is called by a piece of code that owns the \"Alice\" or \"Bob\"
+principals. Otherwise, it simply returns @Nothing@.  Though 'privInit'
+(in "LIO.Run#v:privInit") allows us to create arbitrary privileges in
+the 'IO' monad, the gate restricts access to @addGate@ from within the
+'LIO' monad where code cannot create arbitrary privileges.
+
+> import LIO
+> import LIO.DCLabel
+> import LIO.Run
+> 
+> -- | Add two numbers if the computation is invoked by Alice or Bob.
+> addGate :: Gate CNF (Int -> Int -> Maybe Int)
+> addGate = gate $ \pd a b ->
+>   if pd `speaksFor` "Alice" \/ "Bob"
+>   then Just $ a + b
+>   else Nothing
+> 
+> main :: IO ()
+> main = do
+>   alice <- privInit $ toCNF $ "Alice"
+>   bob <- privInit $ toCNF $ "Bob"
+>   clark <- privInit $ toCNF $ "Clark"
+>   putStrLn . show $ [
+>       callGate addGate alice 1 2 -- Just 3
+>     , callGate addGate bob   3 4 -- Just 7
+>     , callGate addGate clark 5 6 -- Nothing
+>     ]
+> 
+
+-}
+
diff --git a/LIO/Error.hs b/LIO/Error.hs
new file mode 100644
--- /dev/null
+++ b/LIO/Error.hs
@@ -0,0 +1,173 @@
+{-# LANGUAGE Trustworthy #-}
+{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE ExistentialQuantification #-}
+
+{- |
+
+This module exports exception types thrown in response to label
+failures.  In addition, it provides 'withContext', a function that
+annotates any exceptions in the 'AnyLabelError' hierarchy that are
+thrown within a given scope.  These annotations should be used to add
+function names to exceptions, so as to make it easier to pinpoint the
+cause of a label error.
+
+-}
+
+module LIO.Error (
+    Annotatable(..), withContext
+  , AnyLabelError(..), lerrToException, lerrFromException
+  , GenericPrivDesc(..), LabelError(..),  labelError, labelErrorP
+  , InsufficientPrivs(..), insufficientPrivs
+  , ResultExceedsLabel(..)
+  ) where
+
+import safe qualified Control.Exception as IO
+import safe Data.Typeable
+
+import safe LIO.Exception
+import safe LIO.Label
+import LIO.TCB
+
+-- | Class of error messages that can be annotated with context.
+class Annotatable e where
+  annotate :: String -> e -> e
+
+-- | Parent of all label-related exceptions.
+data AnyLabelError = forall e. (Exception e, Annotatable e) =>
+                     AnyLabelError e deriving Typeable
+
+instance Show AnyLabelError where
+  showsPrec d (AnyLabelError e) = showsPrec d e
+
+instance Annotatable AnyLabelError where
+  annotate s (AnyLabelError e) = AnyLabelError $ annotate s e
+
+instance Exception AnyLabelError
+
+-- | Executes an action with a context string which will be added to
+-- any label exception thrown.
+-- 
+-- Note: this function wraps an action with a 'catch', and thus may
+-- incur a small runtime cost (though it is well under 100 ns on
+-- machines we benchmarked).
+withContext :: String -> LIO l a -> LIO l a
+withContext ctx (LIOTCB act) =
+  LIOTCB $ \st -> act st `IO.catch` \e ->
+  IO.throwIO $ annotate ctx (e :: AnyLabelError)
+
+-- | Definition of 'toException' for children of 'AnyLabelError' in
+-- the exception hierarchy.
+lerrToException :: (Exception e, Annotatable e) => e -> SomeException
+lerrToException = toException . AnyLabelError
+
+-- | Definition of 'fromException' for children of 'AnyLabelError' in
+-- the exception hierarchy.
+lerrFromException :: (Exception e) => SomeException -> Maybe e
+lerrFromException se = do
+  AnyLabelError e <- fromException se
+  cast e
+
+
+-- | A generic privilege description for recording relevant privileges
+-- in exceptions.
+data GenericPrivDesc l = forall p. (PrivDesc l p) => GenericPrivDesc p
+instance Show (GenericPrivDesc l) where
+  showsPrec d (GenericPrivDesc p) = showsPrec d p
+
+
+-- | Main error type thrown by label failures in the 'LIO' monad.
+data LabelError l = LabelError {
+    lerrContext :: [String] -- ^ Annotation of where the failure happened.
+  , lerrFailure :: String   -- ^ Actual function that failed.
+  , lerrCurLabel :: l       -- ^ Current label at time of error.
+  , lerrCurClearance :: l   -- ^ Current clearance at time of error.
+  , lerrPrivs :: [GenericPrivDesc l] -- ^ Any privileges involved in error.
+  , lerrLabels :: [l]       -- ^ Any labels involved in error.
+  } deriving (Show, Typeable)
+
+instance Annotatable (LabelError l) where
+  annotate a e = e { lerrContext = a : lerrContext e }
+
+instance Label l => Exception (LabelError l) where
+  toException = lerrToException
+  fromException = lerrFromException
+
+-- | Throw a label-error exception.
+labelError :: (Label l) => String -- ^ Function that failed.
+                        -> [l]    -- ^ Labels involved in error.
+                        -> LIO l a
+labelError fl ls = do
+  st <- getLIOStateTCB
+  throwLIO LabelError {
+      lerrContext = []
+    , lerrFailure = fl
+    , lerrCurLabel = lioLabel st
+    , lerrCurClearance = lioClearance st
+    , lerrPrivs = []
+    , lerrLabels = ls
+    }
+
+-- | Throw a label-error exception.
+labelErrorP :: (Label l, PrivDesc l p) => String  -- ^ Function that failed.
+                                       -> Priv p  -- ^ Privileges involved.
+                                       -> [l]     -- ^ Labels involved.
+                                       -> LIO l a
+labelErrorP fl p ls = do
+  st <- getLIOStateTCB
+  throwLIO LabelError {
+      lerrContext = []
+    , lerrFailure = fl
+    , lerrCurLabel = lioLabel st
+    , lerrCurClearance = lioClearance st
+    , lerrPrivs = [GenericPrivDesc $ privDesc p]
+    , lerrLabels = ls
+    }
+
+
+-- | Error indicating insufficient privileges (independent of the
+-- current label).  This exception is thrown by 'delegate', and
+-- should also be thrown by gates that receive insufficient privilege
+-- descriptions (see "LIO.Delegate").
+data InsufficientPrivs = forall p. (SpeaksFor p) => InsufficientPrivs {
+    inspContext :: [String]
+  , inspFailure :: String
+  , inspSupplied :: p
+  , inspNeeded :: p
+  } deriving (Typeable)
+
+instance Show InsufficientPrivs where
+  showsPrec _ (InsufficientPrivs c l s n) =
+    ("InsufficientPrivs { inspContext = " ++) . shows c .
+    (", inspLocation = " ++) . shows l .
+    (", inspSupplied = " ++) . shows s .
+    (", inspNeeded = " ++) . shows n .
+    (" }" ++)
+
+instance Annotatable InsufficientPrivs where
+  annotate a e = e { inspContext = a : inspContext e }
+
+instance Exception InsufficientPrivs where
+  toException = lerrToException
+  fromException = lerrFromException
+
+-- | Raise 'InsufficientPrivs' error.
+insufficientPrivs :: (SpeaksFor p) => String -> Priv p -> p -> a
+insufficientPrivs fl supplied needed =
+  IO.throw $ InsufficientPrivs [] fl (privDesc supplied) needed
+
+
+-- | Error raised when a computation spawned by 'lFork' terminates
+-- with its current label above the label of the result.
+data ResultExceedsLabel l = ResultExceedsLabel {
+    relContext :: [String]
+  , relLocation :: String
+  , relDeclaredLabel :: l
+  , relActualLabel :: Maybe l
+  } deriving (Show, Typeable)
+
+instance Annotatable (ResultExceedsLabel l) where
+  annotate a e = e { relContext = a : relContext e }
+
+instance (Label l) => Exception (ResultExceedsLabel l) where
+  toException = lerrToException
+  fromException = lerrFromException
diff --git a/LIO/Exception.hs b/LIO/Exception.hs
--- a/LIO/Exception.hs
+++ b/LIO/Exception.hs
@@ -21,14 +21,15 @@
   , onException, finally, bracket, evaluate
   ) where
 
-import Control.Exception (Exception(..), SomeException(..))
-import qualified Control.Exception as IO
-import Control.Monad
-import Data.Typeable
+import safe Control.Exception (Exception(..), SomeException(..))
+import safe qualified Control.Exception as IO
+import safe Control.Monad
+import safe Data.Typeable
 
 import LIO.TCB
-import LIO.Label
+import safe LIO.Label
 
+-- | Throw an exception.
 throwLIO :: Exception e => e -> LIO l a
 throwLIO = ioTCB . IO.throwIO
 
@@ -40,8 +41,8 @@
 -- exceeding the clarance, and an exception is always thrown at the
 -- time this happens.)
 catch :: (Label l, Exception e) => LIO l a -> (e -> LIO l a) -> LIO l a
-catch io h =
-  LIOTCB $ \s -> unLIOTCB io s `IO.catch` \e -> unLIOTCB (safeh e) s
+catch (LIOTCB io) h =
+  LIOTCB $ \s -> io s `IO.catch` \e -> case safeh e of LIOTCB ioe -> ioe s
   where uncatchableType = typeOf (undefined :: UncatchableTCB)
         safeh e@(SomeException einner) = do
           when (typeOf einner == uncatchableType) $ throwLIO e
diff --git a/LIO/LIORef.hs b/LIO/LIORef.hs
--- a/LIO/LIORef.hs
+++ b/LIO/LIORef.hs
@@ -28,10 +28,11 @@
   , atomicModifyLIORef, atomicModifyLIORefP
   ) where
 
-import Data.IORef
-import LIO.Core
-import LIO.Label
-import LIO.Privs
+import safe Data.IORef
+
+import safe LIO.Core
+import safe LIO.Error
+import safe LIO.Label
 import LIO.TCB
 import LIO.TCB.LObj
 
@@ -55,13 +56,17 @@
           => l                  -- ^ Label of reference
           -> a                  -- ^ Initial value
           -> LIO l (LIORef l a) -- ^ Mutable reference
-newLIORef = newLIORefP noPrivs
+newLIORef l a = do
+  withContext "newLIORef" $ guardAlloc l
+  ioTCB (LObjTCB l `fmap` newIORef a)
 
 -- | Same as 'newLIORef' except @newLIORefP@ takes a set of
 -- privileges which are accounted for in comparing the label of
 -- the reference to the current label and clearance.
 newLIORefP :: PrivDesc l p => Priv p -> l -> a -> LIO l (LIORef l a)
-newLIORefP p l a = guardAllocP p l >> ioTCB (LObjTCB l `fmap` newIORef a)
+newLIORefP p l a = do
+  withContext "newLIORefP" $ guardAllocP p l
+  ioTCB (LObjTCB l `fmap` newIORef a)
 
 --
 -- Read 'LIORef's
@@ -71,14 +76,18 @@
 -- label of the reference is below the current clearance. Moreover,
 -- the current label is raised to the join of the current label and
 -- the reference label. To avoid failures (introduced by the 'taint'
----guard) use 'labelOf' to check that a read will succeed.
+-- guard) use 'labelOf' to check that a read will succeed.
 readLIORef :: Label l => LIORef l a -> LIO l a
-readLIORef (LObjTCB l r) = taint l >> ioTCB (readIORef r)
+readLIORef (LObjTCB l r) = do
+  withContext "readLIORef" $ taint l
+  ioTCB (readIORef r)
 
 -- | Same as 'readLIORef' except @readLIORefP@ takes a privilege object
 -- which is used when the current label is raised.
 readLIORefP :: PrivDesc l p => Priv p -> LIORef l a -> LIO l a
-readLIORefP p (LObjTCB l r) = taintP p l >> ioTCB (readIORef r)
+readLIORefP p (LObjTCB l r) = do
+  withContext "readLIORefP" $ taintP p l
+  ioTCB (readIORef r)
 
 --
 -- Write 'LIORef's
@@ -89,13 +98,17 @@
 -- label of the reference can-flow-to the current clearance. Otherwise,
 -- an exception is raised by the underlying 'guardAlloc' guard.
 writeLIORef :: Label l => LIORef l a -> a -> LIO l ()
-writeLIORef (LObjTCB l r) a = guardAlloc l >> ioTCB (writeIORef r a)
+writeLIORef (LObjTCB l r) a = do
+  withContext "writeLIORef" $ guardAlloc l
+  ioTCB (writeIORef r a)
 
 -- | Same as 'writeLIORef' except @writeLIORefP@ takes a set of
 -- privileges which are accounted for in comparing the label of
 -- the reference to the current label and clearance.
 writeLIORefP :: PrivDesc l p => Priv p -> LIORef l a -> a -> LIO l ()
-writeLIORefP p (LObjTCB l r) a = guardAllocP p l >> ioTCB (writeIORef r a)
+writeLIORefP p (LObjTCB l r) a = do
+  withContext "writeLIORefP" $ guardAllocP p l
+  ioTCB (writeIORef r a)
 
 --
 -- Modify 'LIORef's
@@ -113,14 +126,18 @@
              =>  LIORef l a            -- ^ Labeled reference
              -> (a -> a)               -- ^ Modifier
              -> LIO l ()
-modifyLIORef (LObjTCB l r) f = guardAlloc l >> ioTCB (modifyIORef r f)
+modifyLIORef (LObjTCB l r) f = do
+  withContext "modifyLIORef" $ guardAlloc l
+  ioTCB (modifyIORef r f)
 
 -- | Same as 'modifyLIORef' except @modifyLIORefP@ takes a set of
 -- privileges which are accounted for in comparing the label of
 -- the reference to the current label and clearance.
 modifyLIORefP :: PrivDesc l p
               =>  Priv p -> LIORef l a -> (a -> a) -> LIO l ()
-modifyLIORefP p (LObjTCB l r) f = guardAllocP p l >> ioTCB (modifyIORef r f)
+modifyLIORefP p (LObjTCB l r) f = do
+  withContext "modifyLIORefP" $ guardAllocP p l
+  ioTCB (modifyIORef r f)
 
 -- | Atomically modifies the contents of an 'LIORef'. It is required
 -- that the label of the reference be above the current label, but
@@ -132,11 +149,11 @@
 -- which will raise an exception if any of the IFC conditions cannot
 -- be satisfied.
 atomicModifyLIORef :: Label l => LIORef l a -> (a -> (a, b)) -> LIO l b
-atomicModifyLIORef = blessTCB atomicModifyIORef
+atomicModifyLIORef = blessTCB "atomicModifyIORef" atomicModifyIORef
 
 -- | Same as 'atomicModifyLIORef' except @atomicModifyLIORefP@ takes
 -- a set of privileges which are accounted for in label comparisons.
 atomicModifyLIORefP :: PrivDesc l p
                     => Priv p -> LIORef l a -> (a -> (a, b)) -> LIO l b
-atomicModifyLIORefP = blessPTCB atomicModifyIORef
+atomicModifyLIORefP = blessPTCB "atomicModifyLIORefP" atomicModifyIORef
 
diff --git a/LIO/Label.hs b/LIO/Label.hs
--- a/LIO/Label.hs
+++ b/LIO/Label.hs
@@ -1,141 +1,264 @@
-{-# LANGUAGE Safe #-}
-{- | 
+{-# LANGUAGE Trustworthy #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE DeriveDataTypeable #-}
 
-Labels are a way of describing who can observe and modify data.  There
-is a partial order, generally pronounced \"can flow to\" on labels.
-In LIO we write this partial order ``canFlowTo`` (in the literature it
-is usually written as &#8849;).
 
-The idea is that data labeled @L_1@ may affect data labeled @L_2@
-only if @L_1@ ``canFlowTo`` @L_2@.  The 'LIO' monad (see "LIO.Core")
-keeps track of the current label of the executing code (accessible via
-the 'getLabel' function).  Code may attempt to perform various IO or
-memory operations on labeled data.  Hence, touching data may change
-the current label (or throw an exception if an operation would violate
-flow restrictions).
-
-If the current label is @L_cur@, then it is only permissible to read
-data labeled @L_r@ if @L_r ``canFlowTo`` L_cur@.  This is sometimes
-termed \"no read up\" in the literature; however, because the partial
-order allows for incomparable labels (i.e., two labels @L_1@ and @L_2@
-such that @not (L_1 ``canFlowTo`` L_2) && not (L_2 ``canFlowTo``
-L_1)@), a more appropriate phrasing would be \"read only what can flow
-to your label\".  Note that, rather than throw an exception, reading
-data will often just increase the current label to ensure that @L_r
-``canFlowTo`` L_cur@.  The LIO monad keeps a second label, called the
-/clearance/ (accessible via the @getClearance@ function), that
-represents the highest value the current thread can raise its label
-to. The purpose of clearance is to enforce discretionary access
-control: you can set the clearance to a label @L_clear@ so as to prevent
-a piece of LIO code from accessing anything above @L_clear@.
+module LIO.Label (
+  -- * Labels
+  -- $Labels
+    Label(..)
+  -- * Privileges
+  -- $Privileges
+  , SpeaksFor(..), PrivDesc(..)
+  , Priv, privDesc
+  -- * Empty privileges
+  , NoPrivs(..), noPrivs
+  ) where
 
-Conversely, it is only permissible to modify data labeled @L_w@ when
-@L_cur``canFlowTo`` L_w@, a property often cited as \"no write down\",
-but more accurately characterized as \"write only what you can flow
-to\".  In practice, there are very few IO abstractions (namely,
-mutable references) in which it is possible to do a pure write that
-doesn't also involve observing some state.  For instance, writing to a
-file handle and not getting an exception tells you that the handle is
-not closed.  Thus, in practice, the requirement for modifying data
-labeled @L_w@ is almost always that @L_cur ``canFlowTo`` L_w@ and @L_w
-``canFlowTo`` L_cur@, i.e., @L_cur == L_w@.
+import safe Data.Monoid
+import safe Data.Typeable
 
-Note that higher labels are neither more nor less privileged than
-lower ones.  Simply, the higher one's label is, the more things one
-can read.  Conversely, the lower one's label, the more things one can
-write.  But, because labels are a partial and not a total order, some
-data may be completely inaccessible to a particular computation; for
-instance, if the current label is @L_cur@, the current clearance is
-@C_cur@, and some data is labeled @L_d@, such that @not (L_cur
-``canFlowTo`` L_d || L_d ``canFlowTo`` C_cur)@, then the current
-thread can neither read nor write the data, at least without invoking
-some privilege.
+import LIO.TCB
 
-LIO is polymorphic in the label type. It is solely required that every
-implementation of a label (usually called a "label format") be an
-instance of the 'Label' class. This class provides a generic interface
-to labels: they must define the 'canFlowTo' relation, some minimal
-element 'bottom', some maximum element 'top', and two binary operators
-on how to combine labels: the least upper bound ('lub') and greatest
-lower bound ('glb').
+{- $Labels
 
-Since LIO associates labels with different data types, it is useful to
-be able to access the label of such objects (when the label is solely
-protected by the current label). To this end, LIO provides the
-'LabelOf' type class for which different labeled objects
-implementations provide an instance.
+Labels are a way of describing who can observe and modify data.
+Labels are governed by a partial order, generally pronounced \"can
+flow to.\"  In LIO, we write this relation ``canFlowTo``.  In the
+literature, it is usually written &#8849;.
 
--}
+At a high level, the purpose of this whole library is to ensure that
+data labeled @l1@ may affect data labeled @l2@ only if @l1
+``canFlowTo`` l2@.  The 'LIO' monad (see "LIO.Core") ensures this by
+keeping track of a /current label/ of the executing thread (accessible
+via the 'getLabel' function).  Code may attempt to perform various IO
+or memory operations on labeled data.  Touching data may change the
+current label and will throw an exception in the event that an
+operation would violate information flow restrictions.
 
-module LIO.Label (
-  -- * Labels
-    Label(..)
-  -- * Accessing label of labeled values
- , LabelOf(..) 
- ) where
+The specific invariant maintained by 'LIO' is, first, that labels on
+all previously observed data must flow to a thread's current label.
+Second, the current label must flow to the labels of any future
+objects the thread will be allowed to modify.  Hence, after a thread
+with current label @lcur@ observes data labeled @l1@, it must hold
+that @l1 ``canFlowTo`` lcur@.  If the thread is later permitted to
+modify an object labeled @l2@, it must hold that @lcur ``canFlowTo``
+l2@.  By transitifity of the ``canFlowTo`` relation, it holds that @l1
+``canFlowTo` l2@.
 
+-}
 
--- | This class defines a label format, corresponding to a bounded
--- lattice (see <https://en.wikipedia.org/wiki/Bounded_lattice>).
--- Specifically, it is necessary to define a bottom element
--- 'bottom' (in literature, written as &#8869;), a top element 'top' (in
--- literature, written as &#8868;), a join, or least upper bound, 'lub'
--- (in literature, written as &#8852;), a meet, or greatest lower bound,
--- 'glb' (in literature, written as &#8851;), and of course the
--- can-flow-to partial-order 'canFlowTo' (in literature, written as
--- &#8849;).
-class (Eq l, Show l) => Label l where
-  -- | /Least/ upper bound, or join, of two labels. For any two labels
-  -- @L_1@ and @L_2@, if @L_3 = L_1 \`lub` L_2@, it must be that:
+-- | This class defines the operations necessary to make a label into
+-- a lattice (see <http://en.wikipedia.org/wiki/Lattice_(order)>).
+-- 'canFlowTo' partially orders labels.
+-- 'lub' and 'glb' compute the least upper bound and greatest lower
+-- bound of two labels, respectively.
+class (Eq l, Show l, Typeable l) => Label l where
+  -- | Compute the /least upper bound/, or join, of two labels.  When
+  -- data carrying two different labels is mixed together in a
+  -- document, the @lub@ of the two labels is the lowest safe value
+  -- with which to label the result.
   --
-  -- * @L_1 ``canFlowTo`` L_3@,
+  -- More formally, for any two labels @l1@ and @l2@, if @ljoin = l1
+  -- \`lub` l2@, it must be that:
   --
-  -- * @L_2 ``canFlowTo`` L_3@, and
+  -- * @L_1 ``canFlowTo`` ljoin@,
   --
-  -- * There is no label @L_4 /= L_3 @ such that
-  --   @L_1 ``canFlowTo`` L_4@, @L_2 ``canFlowTo`` L_4@, and
-  --   @L_4 ``canFlowTo`` L_3@.  In other words @L_3@ is the least
-  --   such element.
+  -- * @L_2 ``canFlowTo`` ljoin@, and
+  --
+  -- * There is no label @l /= ljoin@ such that @l1 ``canFlowTo`` l@,
+  --   @l2 ``canFlowTo`` l@, and @l ``canFlowTo`` ljoin@.  In other
+  --   words @ljoin@ is the least element to which both @l1@ and @l2@
+  --   can flow.
+  --
+  -- When used infix, has fixity:
+  --
+  -- > infixl 5 `lub`
   lub :: l -> l -> l
-  -- | /Greatest/ lower bound, or meet, of two labels. For any two labels
-  -- @L_1@ and @L_2@, if @L_3 = L_1 \`glb` L_2@, it must be that:
+
+  -- | /Greatest lower bound/, or meet, of two labels. For any two
+  -- labels @l1@ and @l2@, if @lmeet = l1 \`glb` l2@, it must be
+  -- that:
   --
-  -- * @L_3 ``canFlowTo`` L_1@,
+  -- * @lmeet ``canFlowTo`` l1@,
   --
-  -- * @L_3 ``canFlowTo`` L_2@, and
+  -- * @lmeet ``canFlowTo`` l2@, and
   --
-  -- * There is no label @L_4 /= L_3@ such that
-  --   @L_4 ``canFlowTo`` L_1@, @L_4 ``canFlowTo`` L_1@, and
-  --   @L_3 ``canFlowTo`` L_4@.  In other words @L_3@ is the greatest
-  --   such element.
+  -- * There is no label @l /= lmeet@ such that @l ``canFlowTo`` l1@,
+  --   @l ``canFlowTo`` l2@, and @lmeet ``canFlowTo`` l@.  In other
+  --   words @lmeet@ is the greatest element flowing to both @l1@ and
+  --   @l2@.
+  --
+  -- When used infix, has fixity:
+  --
+  -- > infixl 5 `glb`
   glb :: l -> l -> l
-  -- | Can-flow-to relation. An entity labeled @L_1@ should be allowed
-  -- to affect an entity @L_2@ only if @L_1 \`canFlowTo` L_2@. This
-  -- relation on labels is at least a partial order (see
+
+  -- | /Can-flow-to/ relation (&#8849;). An entity labeled @l1@ should
+  -- be allowed to affect an entity @l2@ only if @l1 \`canFlowTo`
+  -- l2@. This relation on labels is at least a partial order (see
   -- <https://en.wikipedia.org/wiki/Partially_ordered_set>), and must
-  -- satisfy the following rules:
+  -- satisfy the following laws:
   --
-  -- * Reflexivity: @L_1 \`canFlowTo` L_1@ for any @L_1@.
+  -- * Reflexivity: @l1 \`canFlowTo` l1@ for any @l1@.
   --
-  -- * Antisymmetry: If @L_1 \`canFlowTo` L_2@ and
-  --   @L_2 \`canFlowTo` L_1@ then @L_1 = L_2@.
+  -- * Antisymmetry: If @l1 \`canFlowTo` l2@ and
+  --   @l2 \`canFlowTo` l1@ then @l1 = l2@.
   --
-  -- * Transitivity: If @L_1 \`canFlowTo` L_2@ and
-  --   @L_2 \`canFlowTo` L_3@ then @L_1 \`canFlowTo` L_3@.
+  -- * Transitivity: If @l1 \`canFlowTo` l2@ and
+  --   @l2 \`canFlowTo` l3@ then @l1 \`canFlowTo` l3@.
+  --
+  -- When used infix, has fixity:
+  --
+  -- > infix 4 `canFlowTo`
   canFlowTo :: l -> l -> Bool
 
--- | Generic class used to get the type of labeled objects. For,
--- instance, if you wish to associate a label with a pure value (as in
--- "LIO.Labeled"), you may create a data type:
--- 
--- > newtype LVal l a = LValTCB (l, a)
--- 
--- Then, you may wish to allow untrusted code to read the label of any
--- @LVal@s but not necessarily the actual value. To do so, simply
--- provide an instance for @LabelOf@:
--- 
--- > instance LabelOf LVal where
--- >   labelOf (LValTCB lv) = fst lv
-class LabelOf t where
-  -- | Get the label of a type kinded @* -> *@
-  labelOf :: t l a -> l
+infixl 5 `lub`, `glb`
+infix 4 `canFlowTo`
+
+{- $Privileges 
+
+Privileges are objects the possesion of which allows code to bypass
+certain label protections.  An instance of class 'PrivDesc' describes
+a pre-order (see <http://en.wikipedia.org/wiki/Preorder>) among labels
+in which certain unequal labels become equivalent.  A 'Priv' object
+containing a 'PrivDesc' instance allows code to make those unequal
+labels equivalent for the purposes of many library functions.
+Effectively, a 'PrivDesc' instance /describes/ privileges, while a
+'Priv' object /embodies/ them.
+
+Any code is free to construct 'PrivDesc' values describing arbitrarily
+powerful privileges.  Security is enforced by preventing safe code
+from accessing the constructor for 'Priv' (called 'PrivTCB').  Safe
+code can construct arbitrary privileges from the 'IO' monad (using
+'privInit' in "LIO.Run#v:privInit"), but cannot do so from the 'LIO'
+monad.  Starting from existing privileges, safe code can also
+'delegate' lesser privileges (see "LIO.Delegate#v:delegate").
+
+Privileges allow you to behave as if @l1 ``canFlowTo`` l2@ even when
+that is not the case, but only for certain pairs of labels @l1@ and
+@l2@; which pairs depends on the specific privileges.  The process of
+allowing data labeled @l1@ to infulence data labeled @l2@ when @(l1
+``canFlowTo`` l2) == False@ is known as /downgrading/.
+
+The core privilege function is 'canFlowToP', which performs a
+more permissive can-flow-to check by exercising particular privileges
+(in literature this relation is commonly written @&#8849;&#8346;@ for
+privileges @p@).  Most core 'LIO' function have variants ending @...P@
+that take a privilege argument to act in a more permissive way.
+
+By convention, all 'PrivDesc' instances should also be instances of
+'Monoid', allowing privileges to be combined with 'mappend', though
+this is not enforced with superclasses.
+
+-}
+
+
+-- | Turns privileges into a powerless description of the privileges
+-- by unwrapping the 'Priv' newtype.
+privDesc :: Priv a -> a
+{-# INLINE privDesc #-}
+privDesc (PrivTCB a) = a
+
+-- | Every privilege type must be an instance of 'SpeaksFor', which
+-- specifies when one privilege value is more powerful than another.
+-- If you do not wish to allow delegation, you can simply define
+-- @'speaksFor' _ _ = False@.
+class (Typeable p, Show p) => SpeaksFor p where
+  -- | @speaksFor p1 p2@ returns 'True' iff @p1@ subsumes all the
+  -- privileges of @p2@.  In other words, it is safe for 'delegate' to
+  -- hand out @p2@ to a caller who already has @p1@.
+  --
+  -- Has fixity:
+  --
+  -- > infix 4 `speaksFor`
+  speaksFor :: p -> p -> Bool
+
+infix 4 `speaksFor`
+
+-- | This class represents privilege descriptions, which define a
+-- pre-order on labels in which distinct labels become equivalent.
+-- The pre-oder implied by a privilege description is specified by the
+-- method 'canFlowToP'.  In addition, this this class defines a method
+-- 'downgradeP', which is important for finding least labels
+-- satisfying a privilege equivalence.
+--
+-- Minimal complete definition: 'downgradeP'.
+--
+-- (The 'downgradeP' requirement represents the fact that a generic
+-- 'canFlowToP' can be implemented efficiently in terms of
+-- 'downgradeP', but not vice-versa.)
+class (Label l, SpeaksFor p) => PrivDesc l p where
+-- Note: SpeaksFor is a superclass for security reasons.  Were it not
+-- a superclass, then if a label format ever failed to define
+-- SpeaksFor, or defined it in a different module from the PrivDesc
+-- instance, then an attacker could produce an vacuous instance that
+-- allows all delegation.
+
+    -- | Privileges are described in terms of a pre-order on labels in
+    -- which sets of distinct labels become equivalent.  @downgradeP p
+    -- l@ returns the lowest of all labels equivalent to @l@ under
+    -- privilege description @p@.
+    --
+    -- Less formally, @downgradeP p l@ returns a label representing
+    -- the furthest you can downgrade data labeled @l@ given
+    -- privileges described by @p@.
+    --
+    -- Yet another way to view this function is that @downgradeP p l@
+    -- returns the greatest lower bound (under 'canFlowTo') of the set
+    -- of all labels @l'@ such that @'canFlowToP' p l' l@.
+    downgradeP :: p     -- ^ Privilege description
+                  -> l  -- ^ Label to downgrade
+                  -> l  -- ^ Lowest label equivelent to input
+
+    -- | @canFlowToP p l1 l2@ determines whether @p@ describes
+    -- sufficient privileges to observe data labeled @l1@ and
+    -- subsequently write it to an object labeled @l2@.  The function
+    -- returns 'True' if and only if either @canFlowTo l1 l2@ or @l1
+    -- and l2@ are equivalent under @p@.
+    --
+    -- The default definition is:
+    --
+    -- > canFlowToP p l1 l2 = downgradeP p l1 `canFlowTo` l2
+    -- 
+    -- @canFlowToP@ is a method rather than a function so that it can
+    -- be optimized in label-specific ways.  However, custom
+    -- definitions should behave identically to the default.
+    canFlowToP :: p -> l -> l -> Bool
+    canFlowToP p l1 l2 = downgradeP p l1 `canFlowTo` l2
+
+instance (SpeaksFor p) => SpeaksFor (Priv p) where
+  {-# INLINE speaksFor #-}
+  speaksFor p1 p2 = privDesc p1 `speaksFor` privDesc p2
+
+instance (PrivDesc l p) => PrivDesc l (Priv p) where
+  {-# INLINE downgradeP #-}
+  downgradeP = downgradeP . privDesc
+  {-# INLINE canFlowToP #-}
+  canFlowToP = canFlowToP . privDesc
+
+--
+-- NoPrivs
+--
+
+-- | Generic 'PrivDesc' used to denote the lack of privileges.  Works
+-- with any 'Label' type.  This is only a privilege description; a
+-- more useful symbol is 'noPrivs', which actually embodies the
+-- @NoPrivs@ privilege.
+data NoPrivs = NoPrivs deriving (Show, Read, Typeable)
+
+instance SpeaksFor NoPrivs where speaksFor _ _ = True
+
+-- | 'downgradeP' 'NoPrivs' is the identify function.  Hence
+-- 'canFlowToP' 'NoPrivs' is the same as 'canFlowTo'.
+instance Label l => PrivDesc l NoPrivs where downgradeP _ l = l
+
+instance Monoid NoPrivs where
+  mempty      = NoPrivs
+  mappend _ _ = NoPrivs
+
+-- | 'Priv' object corresponding to 'NoPrivs'.
+noPrivs :: Priv NoPrivs
+noPrivs = PrivTCB NoPrivs
+
diff --git a/LIO/Labeled.hs b/LIO/Labeled.hs
--- a/LIO/Labeled.hs
+++ b/LIO/Labeled.hs
@@ -1,7 +1,4 @@
 {-# LANGUAGE Trustworthy #-}
-{-# LANGUAGE CPP,
-             ConstraintKinds,
-             FlexibleContexts #-}
 
 {- |
 
@@ -20,31 +17,30 @@
 data.  This module exports functions for creating labeled values
 ('label'), using the values protected by 'Labeled' by unlabeling them
 ('unlabel'), and changing the value of a labeled value without
-inspection ('relabelLabeledP', 'taintLabeled', 'untaintLabeled').  A
+inspection ('relabelLabeledP', 'taintLabeled').  A
 'Functor'-like class ('LabeledFunctor') on 'Labeled' is also defined
 in this module.
 
 -}
 
 module LIO.Labeled (
-    Labeled
+    Labeled, LabelOf(..)
   -- * Label values
   , label, labelP
   -- * Unlabel values
   , unlabel, unlabelP
   -- * Relabel values
   , relabelLabeledP
-  , taintLabeled, taintLabeledP , untaintLabeledP
+  , taintLabeled, taintLabeledP 
   , lFmap, lAp
   ) where
 
-import Control.Monad
+import safe Control.Monad
 
-import LIO.Exception
+import safe LIO.Error
+import safe LIO.Label
+import safe LIO.Core
 import LIO.TCB
-import LIO.Label
-import LIO.Core
-import LIO.Privs
 
 --
 -- Label values
@@ -56,7 +52,9 @@
 -- ``canFlowTo`` l && l ``canFlowTo`` ccurrent@. Otherwise an
 -- exception is thrown (see 'guardAlloc').
 label :: Label l => l -> a -> LIO l (Labeled l a)
-label = labelP noPrivs
+label l a = do
+  withContext "label" $ guardAlloc l
+  return $ LabeledTCB l a
 
 -- | Constructs a 'Labeled' using privilege to allow the `Labeled`'s
 -- label to be below the current label.  If the current label is
@@ -68,7 +66,7 @@
 -- current clearance.
 labelP :: PrivDesc l p => Priv p -> l -> a -> LIO l (Labeled l a)
 labelP p l a = do
-  guardAllocP p l
+  withContext "labelP" $ guardAllocP p l
   return $ LabeledTCB l a
 
 --
@@ -87,14 +85,14 @@
 -- However, you can use 'labelOf' to check if 'unlabel' will succeed
 -- without throwing an exception.
 unlabel :: Label l => Labeled l a -> LIO l a
-unlabel = unlabelP noPrivs
+unlabel (LabeledTCB l v) = withContext "unlabel" (taint l) >> return v
 
 -- | Extracts the value of an 'Labeled' just like 'unlabel', but takes a
 -- privilege argument to minimize the amount the current label must be
 -- raised.  Function will throw 'ClearanceViolation' under the same
 -- circumstances as 'unlabel'.
 unlabelP :: PrivDesc l p => Priv p -> Labeled l a -> LIO l a
-unlabelP p (LabeledTCB l v) = taintP p l >> return v
+unlabelP p (LabeledTCB l v) = withContext "unlabelP" (taintP p l) >> return v
 
 --
 -- Relabel values
@@ -113,8 +111,9 @@
 relabelLabeledP :: PrivDesc l p
                 => Priv p -> l -> Labeled l a -> LIO l (Labeled l a)
 relabelLabeledP p newl (LabeledTCB oldl v) = do
-  guardAllocP p newl
-  unless (canFlowToP p oldl newl) $ throwLIO InsufficientPrivs
+  withContext "relabelLabeledP" $ guardAllocP p newl
+  unless (canFlowToP p oldl newl) $
+    labelErrorP "relabelLabeledP" p [oldl, newl]
   return $ LabeledTCB newl v
 
 -- | Raises the label of a 'Labeled' to the 'upperBound' of it's current
@@ -124,7 +123,10 @@
 -- the supplied label is not bounded then @taintLabeled@ will throw an
 -- exception (see 'guardAlloc').
 taintLabeled :: Label l => l -> Labeled l a -> LIO l (Labeled l a)
-taintLabeled = taintLabeledP noPrivs
+taintLabeled l (LabeledTCB lold v) = do
+  let lnew = lold `lub` l
+  withContext "taintLabeled" $ guardAlloc lnew
+  return $ LabeledTCB lnew v
 
 -- | Same as 'taintLabeled', but uses privileges when comparing the
 -- current label to the supplied label. In other words, this function
@@ -134,16 +136,9 @@
               => Priv p -> l -> Labeled l a -> LIO l (Labeled l a)
 taintLabeledP p l (LabeledTCB lold v) = do
   let lnew = lold `lub` l
-  guardAllocP p lnew
+  withContext "taintLabeledP" $ guardAllocP p lnew
   return $ LabeledTCB lnew v
 
--- | Downgrades a label.
-untaintLabeledP :: PrivDesc l p
-                => Priv p -> l -> Labeled l a -> LIO l (Labeled l a)
-untaintLabeledP p target lv =
-  relabelLabeledP p (partDowngradeP p (labelOf lv) target) lv
-
-
 {- $functor
 
 Making 'Labeled' an instance of 'Functor' is problematic because:
@@ -174,7 +169,7 @@
   -- Result label is joined with current label
   let lnew = lold `lub` l
   -- `label` checks for clearance violation then labels
-  label lnew $ f v
+  withContext "lFmap" $ label lnew $ f v
 
 
 -- | Similar to 'ap', apply function (wrapped by 'Labeled') to the
@@ -185,4 +180,4 @@
 lAp (LabeledTCB lf f) (LabeledTCB la a) = do
   l <- getLabel
   let lnew = l `lub` lf `lub` la
-  label lnew $ f a
+  withContext "lAp" $ label lnew $ f a
diff --git a/LIO/Privs.hs b/LIO/Privs.hs
deleted file mode 100644
--- a/LIO/Privs.hs
+++ /dev/null
@@ -1,213 +0,0 @@
-{-# LANGUAGE Trustworthy #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE FlexibleInstances #-}
-
-{- | 
-
-Privileges are objects the possesion of which allows code to bypass
-some label protections.  An in instance of class 'PrivDesc' describes
-a pre-order among labels in which certain unequal labels become
-equivalent.  When wrapped in a 'Priv' type (whose constructor is
-private) a 'PrivDesc' allows code to treat those labels as equivalent.
-
-Put another way, privileges represent the ability to bypass the
-protection of certain labels.  Specifically, privilege allows you to
-behave as if @L_1 ``canFlowTo`` L_2@ even when that is not the case.
-The process of making data labeled @L_1@ affect data labeled @L_2@
-when @not (L_1 ``canFlowTo`` L_2)@ is called /downgrading/.
-
-The basic method of the 'PrivDesc' class is 'canFlowToP', which
-performs a more permissive can-flow-to check by exercising particular
-privileges (in literature this relation is a pre-order, commonly
-written as &#8849;&#8346;).  Almost all 'LIO' operations have variants
-ending @...P@ that take a privilege argument to act in a more
-permissive way.
-
-By convention, all 'PrivDesc' instances are also be instances of
-'Monoid', allowing privileges to be combined with 'mappend'.  The
-creation of 'PrivDesc' values is specific to the particular label type
-in use; the method used is 'mintTCB', but the arguments depend on the
-particular label type.
-
--}
-
-module LIO.Privs (
-  -- * Privilege descriptions
-    PrivDesc(..), canFlowToP, partDowngradeP
-  -- * Privileges
-  , Priv, privDesc
-  , NoPrivs, noPrivs
-  -- * Gates
-  -- $gateIntro
-  , Gate, gate, callGate
-  -- ** Gate example
-  -- $gateExample
-  ) where
-
-import Data.Monoid
-import LIO.Label
-import LIO.TCB
-
---
--- No privileges
---
-
-privDesc :: Priv a -> a
-privDesc (PrivTCB a) = a
-
--- | This class defines privileges and the more-permissive relation
--- ('canFlowToP') on labels using privileges. Additionally, it defines
--- 'partDowngradeP' which is used to downgrage a label up to a limit,
--- given a set of privilege.
-class (Label l) => PrivDesc l p where
-    -- | The \"can-flow-to given privileges\" pre-order used to compare
-    -- two labels in the presence of privileges.  If @'canFlowToP' p L_1
-    -- L_2@ holds, then privileges @p@ are sufficient to downgrade data
-    -- from @L_1@ to @L_2@.  Note that @'canFlowTo' L_1 L_2@ implies
-    -- @'canFlowToP' p L_1 L_2@ for all @p@, but for some labels and
-    -- privileges, 'canFlowToP' will hold even where 'canFlowTo' does
-    -- not.
-    canFlowToPrivDesc :: p -> l -> l -> Bool
-    canFlowToPrivDesc p a b = partDowngradePrivDesc p a b `canFlowTo` b
-
-    -- | Roughly speaking, @L_r = partDowngradeP p L L_g@ computes how
-    -- close one can come to downgrading data labeled @L@ to the goal
-    -- label @L_g@, given privileges @p@.  When @p == 'NoPrivs'@, the
-    -- resulting label @L_r == L ``lub`` L_g@.  If @p@ contains /all/
-    -- possible privileges, then @L_r == L_g@.
-    --
-    -- More specifically, @L_r@ is the greatest lower bound of the
-    -- set of all labels @L_l@ satisfying:
-    --
-    --   1. @ L_g &#8849; L_l@, and
-    --
-    --   2. @ L &#8849;&#8346; L_l@.
-    --
-    -- Operationally, @partDowngradeP@ captures the minimum change required
-    -- to the current label when viewing data labeled @L_l@.  A common
-    -- pattern is to use the result of 'getLabel' as @L_g@ (i.e., the
-    -- goal is to use privileges @p@ to avoid changing the label at all),
-    -- and then compute @L_r@ based on the label of data the code is
-    -- about to observe. 
-    partDowngradePrivDesc :: p  -- ^ Privileges
-                   -> l  -- ^ Label from which data must flow
-                   -> l  -- ^ Goal label
-                   -> l  -- ^ Result
-
--- | TODO(dm): document
-canFlowToP :: PrivDesc l p => Priv p -> l -> l -> Bool
-canFlowToP priv = canFlowToPrivDesc (privDesc priv)
-
--- | TODO(dm): document
-partDowngradeP :: PrivDesc l p => Priv p -> l -> l -> l
-partDowngradeP priv = partDowngradePrivDesc (privDesc priv)
-
-
--- | Generic privilege type used to denote the lack of privileges.
-data NoPrivs = NoPrivs deriving (Show, Read)
-
-noPrivs :: Priv NoPrivs
-noPrivs = PrivTCB NoPrivs
-
-instance Monoid NoPrivs where
-  mempty      = NoPrivs
-  mappend _ _ = NoPrivs
-
--- | With lack of privileges, 'canFlowToP' is simply 'canFlowTo', and
--- 'partDowngradeP' is the least 'upperBound'.
-instance Label l => PrivDesc l NoPrivs where
-  canFlowToPrivDesc _ l1 l2    = l1 `canFlowTo` l2
-  partDowngradePrivDesc _ l lg = l `lub` lg
-
-
-{- $gateIntro
-
-LIO provides a basic implementation of /gates/, useful in providing
-controlled RPC-like services where the client and service provider are
-in mutual distrust. 
-
-A service provider uses 'gate' to create a gate data type @'Gate' d a@
-given a computation of type @d -> a@. Here, @d@ is a privilege
-description (type variable for an instance of 'PrivDesc').  Gates are
-invoked with 'callGate', and as such the service provider has the
-guarantee that the client (the caller) owns the privileges
-corresponding to the privilege description @d@.  In effect, this
-allows a client to \"prove\" to the service provider that they own
-certain privileges without entrusting the service with its privileges.
-The gate computation can analyze this privilege description before
-performing the \"actual\" computation.  The client and server solely
-need to trust the implementation of 'callGate'.
-
--}
-
-
--- | A Gate is a lambda abstraction from a privilege description to an
--- arbitrary type @a@. Applying the gate is accomplished with 'callGate'
--- which takes a privilege argument that is converted to a description
--- before invoking the gate computation.
-newtype Gate d a = GateTCB (d -> a)
--- Note GateTCB is trusted by convention.  Anyone with access to the
--- symbol can call any gate while claiming arbitrary privileges.  In
--- the absence of gates, however, GateTCB doesn't provide any
--- particular privileges.
-
--- | Create a gate given a computation from a privilege description.
--- Note that because of currying type 'a' may itself be a function
--- type and thus gates can take arguments in addition to the privilege
--- descriptoin.
-gate :: (d -> a)  -- ^ Gate computation
-     -> Gate d a
-{-# INLINE gate #-}
-gate = GateTCB
-
--- | Given a gate and privilege, execute the gate computation.  It is
--- important to note that @callGate@ invokes the gate computation with
--- the privilege description and /NOT/ the privilege itself.
---
--- Note that, in general, code should /not/ provide privileges to
--- functions other than @callGate@ when wishing to call a gate. This
--- function is provided by LIO since it can be easily inspected by
--- both the gate creator and caller to be doing the \"right\" thing:
--- provide the privilege description corresponding to the supplied
--- privilege as \"proof\" without explicitly passing in the privilege.
--- 
-callGate :: Gate p a -- ^ Gate
-         -> Priv p   -- ^ Privilege used as proof-of-ownership
-         -> a
-{-# INLINE callGate #-}
-callGate (GateTCB g) = g . privDesc
-
-{- $gateExample
-
-This example uses "LIO.DCLabel" to demonstrate the use of gates.  The
-service provider provides @addGate@ which adds two integers if the
-gate is called by a piece of code that owns the \"Alice\" or \"Bob\"
-principals. Otherwise, it simply returns @Nothing@.
-
-> import LIO
-> import LIO.DCLabel
-> 
-> import LIO.Privs.TCB (mintTCB)
-> 
-> 
-> -- | Add two numbers if the computation is invoked by Alice or Bob.
-> addGate :: DCGate (Int -> Int -> Maybe Int)
-> addGate = gate $ \pd a b ->
->   if pd `elem` (dcPrivDesc `map` ["Alice", "Bob"])
->     then Just $ a + b
->     else Nothing
-> 
-> 
-> alice, bob, clark :: DCPriv
-> alice = PrivTCB . dcPrivDesc $ "Alice"
-> bob   = PrivTCB . dcPrivDesc $ "Bob"
-> clark = PrivTCB . dcPrivDesc $ "Clark"
-> 
-> main = putStrLn . show $ 
->   [ callGate addGate alice 1 2 -- Just 3
->   , callGate addGate bob   3 4 -- Just 7
->   , callGate addGate clark 5 6 -- Nothing
->   ]
-
-
--}
diff --git a/LIO/Run.hs b/LIO/Run.hs
--- a/LIO/Run.hs
+++ b/LIO/Run.hs
@@ -9,10 +9,13 @@
 -- use in invoking 'LIO' code.  The functions are also available via
 -- "LIO" and "LIO.Core", but those modules will clutter your namespace
 -- with symbols you don't need in the 'IO' monad.
-module LIO.Run (LIOState(..), runLIO, evalLIO) where
+module LIO.Run (LIOState(..), runLIO, tryLIO, evalLIO, privInit) where
 
-import Control.Exception
-import Data.IORef
+import safe Control.Exception
+import safe Data.IORef
+import safe Data.Typeable
+
+import safe LIO.Label
 import LIO.TCB
 
 -- | Execute an 'LIO' action, returning its result and the final label
@@ -28,8 +31,18 @@
   s1 <- readIORef sp
   return (a, s1)
 
+-- | A variant of 'runLIO' that returns results in 'Right' and
+-- exceptions in 'Left', much like the standard library 'try'
+-- function.
+tryLIO :: LIO l a -> LIOState l -> IO (Either SomeException a, LIOState l)
+tryLIO lio s0 = runLIO lio s0 >>= tryit
+  where tryit (a, s) = do
+          ea <- try (evaluate a)
+          return (ea, s)
+
+
 -- | Given an 'LIO' computation and some initial state, return an IO
--- action which when executed will perform the IFC-safe LIO
+-- action which, when executed, will perform the IFC-safe LIO
 -- computation.
 --
 -- Because untrusted code cannot execute 'IO' computations, this function
@@ -45,3 +58,21 @@
   (a, _) <- runLIO lio s
   return $! a
 
+-- | Initialize some privileges (within the 'IO' monad) that can be
+-- passed to 'LIO' computations run with 'runLIO' or 'evalLIO'.  This
+-- is a pure function, but the result is encapsulated in 'IO' to
+-- make the return value inaccessible from 'LIO' computations.
+--
+-- Note the same effect can be achieved using the 'PrivTCB'
+-- constructor, but 'PrivTCB' is easier to misuse and is only available by
+-- importing "LIO.TCB".
+privInit :: (SpeaksFor p) => p -> IO (Priv p)
+privInit p | isPriv p  = fail "privInit called on Priv object"
+           | otherwise = return $ PrivTCB p
+
+-- | Uses dynamic typing to return 'True' iff the type of the argument
+-- is @'Priv' a@ (for any @a@).  Mostly useful to prevent users from
+-- accidentally wrapping 'Priv' objects inside other 'Priv' objects.
+isPriv :: (Typeable p) => p -> Bool
+isPriv p = typeRepTyCon (typeOf p) == privcon
+  where privcon = typeRepTyCon $ typeOf noPrivs
diff --git a/LIO/TCB.hs b/LIO/TCB.hs
--- a/LIO/TCB.hs
+++ b/LIO/TCB.hs
@@ -4,21 +4,16 @@
 
 {- | 
 
-This module exports 
-
-* The definition of the 'LIO' monad and relevant trusted state
-  access/modifying functions.
-
-* Various other types whose constructors are privileged and must be
-  hidden from untrusted code.
-
-* Uncatchable exceptions used to pop threads out of the 'LIO' monad
-  unconditionally.
-
-* Combinators for executing 'IO' actions within the 'LIO' monad.
+This module exports symbols that must be accessible only to trusted
+code.  By convention, the names of such symbols always end
+\"@...TCB@\" (short for \"trusted computing base\").  In many cases, a
+type is safe to export while its constructor is not.  Hence, only the
+constructor ends \"@TCB@\", while the type is re-exported to safe code
+(without constructors) to from "LIO.Core".
 
-The documentation and external, safe 'LIO' interface is provided in
-"LIO.Core".
+Security rests on the fact that untrusted code must be compiled with
+@-XSafe@.  Because this module is flagged unsafe, it cannot be
+imported from safe modules.
 
 -}
 
@@ -26,26 +21,26 @@
   -- * LIO monad
     LIOState(..), LIO(..)
   -- ** Accessing internal state
-  , getLIOStateTCB, putLIOStateTCB, modifyLIOStateTCB, updateLIOStateTCB 
+  , getLIOStateTCB, putLIOStateTCB, modifyLIOStateTCB
   -- * Executing IO actions
   , ioTCB
   -- * Privileged constructors
-  , Priv(..), Labeled(..)
+  , Priv(..), Labeled(..), LabelOf(..)
   -- * Uncatchable exception type
   , UncatchableTCB(..), makeCatchable
-  -- * Trusted 'Show' and 'Read'
-  , ShowTCB(..), ReadTCB(..)
+  -- * Trusted 'Show'
+  , ShowTCB(..)
+  -- * 'LabeledResult's
+  , LabeledResult(..), LResStatus(..)
   ) where
 
-import Control.Applicative
-import Control.Exception (Exception(..), SomeException(..))
-import Control.Monad
-import Data.Monoid
-import Data.IORef
-import Data.Typeable
-import Text.Read (minPrec)
-
-import LIO.Label
+import safe Control.Applicative
+import safe Control.Exception (Exception(..), SomeException(..))
+import safe qualified Control.Concurrent as IO
+import safe Control.Monad
+import safe Data.Monoid
+import safe Data.IORef
+import safe Data.Typeable
 
 --
 -- LIO Monad
@@ -56,31 +51,26 @@
                            , lioClearance :: !l -- ^ Current clearance.
                            } deriving (Eq, Show, Read)
 
--- | The @LIO@ monad is a state monad, with 'IO' as the underlying monad,
--- that carries along a /current label/ ('lioLabel') and /current clearance/
--- ('lioClearance'). The current label imposes restrictions on
--- what the current computation may read and write (e.g., no writes to
--- public channels after reading sensitive data).  Since the current
--- label can be raised to be permissive in what a computation observes,
--- we need a way to prevent certain computations from reading overly
--- sensitive data. This is the role of the current clearance: it imposes
--- an upper bound on the current label.
-newtype LIO l a = LIOTCB {
-    unLIOTCB :: IORef (LIOState l) -> IO a
-  } deriving (Typeable)
+-- | The @LIO@ monad is a wrapper around 'IO' that keeps track of a
+-- /current label/ and /current clearance/.  Safe code cannot execute
+-- arbitrary 'IO' actions from the 'LIO' monad.  However, trusted
+-- runtime functions can use 'ioTCB' to perform 'IO' actions (which
+-- they should only do after appropriately checking labels).
+newtype LIO l a = LIOTCB (IORef (LIOState l) -> IO a) deriving (Typeable)
 
 instance Monad (LIO l) where
   {-# INLINE return #-}
   return = LIOTCB . const . return
   {-# INLINE (>>=) #-}
-  m >>= k = LIOTCB $ \s -> do
-    a <- unLIOTCB m s
-    unLIOTCB (k a) s
+  (LIOTCB ma) >>= k = LIOTCB $ \s -> do
+    a <- ma s
+    case k a of LIOTCB mb -> mb s
   fail = LIOTCB . const . fail
 
 instance Functor (LIO l) where
-  {-# INLINE fmap #-}
-  fmap f ma = LIOTCB $ \s -> unLIOTCB ma s >>= return . f
+  fmap f (LIOTCB a) = LIOTCB $ \s -> a s >>= return . f
+-- fmap typically isn't inlined, so we don't inline our definition,
+-- but we do define it in terms of >>= and return (which are inlined)
 
 instance Applicative (LIO l) where
   {-# INLINE pure #-}
@@ -105,24 +95,19 @@
 putLIOStateTCB s = LIOTCB $ \sp -> writeIORef sp $! s
 
 -- | Update the internal state given some function.
-modifyLIOStateTCB :: Label l => (LIOState l -> LIOState l) -> LIO l ()
+modifyLIOStateTCB :: (LIOState l -> LIOState l) -> LIO l ()
 {-# INLINE modifyLIOStateTCB #-}
 modifyLIOStateTCB f = do
   s <- getLIOStateTCB
   putLIOStateTCB (f s)
 
-{-# DEPRECATED updateLIOStateTCB "Use modifyLIOStateTCB instead" #-}
-updateLIOStateTCB :: Label l => (LIOState l -> LIOState l) -> LIO l ()
-updateLIOStateTCB = modifyLIOStateTCB
-
 --
 -- Executing IO actions
 --
 
--- | Lifts an 'IO' computation into the 'LIO' monad.  Note that
--- exceptions thrown within the 'IO' computation cannot directly be
--- caught within the 'LIO' computation.  Thus, you will generally want to
--- use 'rethrowIoTCB'.
+-- | Lifts an 'IO' computation into the 'LIO' monad.  This function is
+-- dangerous and should only be called after appropriate checks ensure
+-- the 'IO' computation will not violate IFC policy.
 ioTCB :: IO a -> LIO l a
 {-# INLINE ioTCB #-}
 ioTCB = LIOTCB . const
@@ -131,13 +116,14 @@
 -- Exception handling
 --
 
--- | An uncatchable exception hierarchy use to terminate an untrusted
--- thread.  Wrap the uncatchable exception in 'UncatchableTCB' before
--- throwing it to the thread.  'runLIO' will subsequently unwrap the
--- 'UncatchableTCB' constructor.
+-- | An uncatchable exception hierarchy is used to terminate an
+-- untrusted thread.  Wrap the uncatchable exception in
+-- 'UncatchableTCB' before throwing it to the thread.  'runLIO' will
+-- subsequently unwrap the 'UncatchableTCB' constructor.
 --
 -- Note this can be circumvented by 'IO.mapException', which should be
--- made unsafe.
+-- made unsafe. In the interim, auditing untrusted code for this is
+-- necessary.
 data UncatchableTCB = forall e. (Exception e) =>
                       UncatchableTCB e deriving (Typeable)
 
@@ -159,10 +145,13 @@
 -- Privileges
 --
 
--- | A newtype wrapper that can be used by trusted code to bless
--- privileges.  Privilege-related functions are defined in
--- "LIO.Privs", but the constructor, 'PrivTCB', allows one to mint
--- arbitrary privileges and hence must be located in this file.
+-- | A newtype wrapper that can be used by trusted code to transform a
+-- powerless description of privileges into actual privileges.  The
+-- constructor, 'PrivTCB', is dangerous as it allows creation of
+-- arbitrary privileges.  Hence it is only exported by the unsafe
+-- module "LIO.TCB".  A safe way to create arbitrary privileges is to
+-- call 'privInit' (see "LIO.Run#v:privInit") from the 'IO' monad
+-- before running your 'LIO' computation.
 newtype Priv a = PrivTCB a deriving (Show, Eq, Typeable)
 
 instance Monoid p => Monoid (Priv p) where
@@ -177,53 +166,75 @@
 --
 
 -- | @Labeled l a@ is a value that associates a label of type @l@ with
--- a value of type @a@. Labeled values allow users to label data with
--- a label other than the current label. In an embedded setting this
--- is akin to having first class labeled values. Note that 'Labeled'
--- is an instance of 'LabelOf', which effectively means that the label
--- of a 'Labeled' value is usually just protected by the current
--- label. (Of course if you have a nested labeled value then the label
--- on the inner labeled value's label is the outer label.)
+-- a pure value of type @a@. Labeled values allow users to label data
+-- with a label other than the current label.  Note that 'Labeled' is
+-- an instance of 'LabelOf', which means that only the /contents/ of a
+-- labeled value (the type @t@) is kept secret, not the label.  Of
+-- course, if you have a @Labeled@ within a @Labeled@, then the label
+-- on the inner value will be protected by the outer label.
 data Labeled l t = LabeledTCB !l t deriving Typeable
 -- Note: t cannot be strict if we want things like lFmap.
 
+-- | Trusted 'Show' instance.
+instance (Show l, Show a) => ShowTCB (Labeled l a) where
+    showTCB (LabeledTCB l a) = show a ++ " {" ++ show l ++ "}"
+
+-- | Generic class used to get the type of labeled objects. For,
+-- instance, if you wish to associate a label with a pure value (as in
+-- "LIO.Labeled"), you may create a data type:
+-- 
+-- > newtype LVal l a = LValTCB (l, a)
+-- 
+-- Then, you may wish to allow untrusted code to read the label of any
+-- @LVal@s but not necessarily the actual value. To do so, simply
+-- provide an instance for @LabelOf@:
+-- 
+-- > instance LabelOf LVal where
+-- >   labelOf (LValTCB lv) = fst lv
+class LabelOf t where
+  -- | Get the label of a labeled value or object.  Note the label
+  -- must be the second to last type constructor argument.
+  labelOf :: t l a -> l
+
 instance LabelOf Labeled where
+  {-# INLINE labelOf #-}
   labelOf (LabeledTCB l _) = l
 
--- | Trusted 'Show' instance.
-instance (Label l, Show a) => ShowTCB (Labeled l a) where
-    showTCB (LabeledTCB l t) = show t ++ " {" ++ show l ++ "}"
+--
+-- Trusted 'Show'
+--
 
--- | Trusted 'Read' instance.
-instance (Label l, Read l, Read a) => ReadTCB (Labeled l a) where
-  readsPrecTCB _ str = do (val, str1) <- reads str
-                          ("{", str2) <- lex str1
-                          (lab, str3) <- reads str2
-                          ("}", rest) <- lex str3
-                          return (LabeledTCB lab val, rest)
+-- | It would be a security issue to make certain objects members of
+-- the 'Show' class.  Nonetheless it is useful to be able to examine
+-- such objects when debugging.  The 'showTCB' method can be used to
+-- examine such objects.
+class ShowTCB a where
+  showTCB :: a -> String
 
+
 --
--- Trusted 'Show' and 'Read'
+-- LabeledResult
 --
 
--- | It would be a security issue to make certain objects a member of
--- the 'Show' class, but nonetheless it is useful to be able to
--- examine such objects when debugging.  The 'showTCB' method can be used
--- to examine such objects.
-class ShowTCB a where
-    showTCB :: a -> String
+-- | Status of a 'LabeledResult'.
+data LResStatus l a = LResEmpty
+                    | LResLabelTooHigh !l
+                    | LResResult a
+                      deriving (Show)
 
--- | It is useful to have the dual of 'ShowTCB', @ReadTCB@, that allows
--- for the reading of strings that were created using 'showTCB'. Only
--- @readTCB@ (corresponding to 'read') and @readsPrecTCB@ (corresponding
--- to 'readsPrec') are implemented.
-class ReadTCB a where
-  -- | Trusted 'readsPrec'
-  readsPrecTCB :: Int -> ReadS a
-  -- | Trusted 'read'
-  readTCB :: String -> a
-  readTCB str = check $ readsPrecTCB minPrec str
-    where check []                          = error "readTCB: no parse"
-          check [(x,rst)] | all (==' ') rst = x
-                         | otherwise        = error "readTCB: no parse"
-          check _                           = error "readTCB: ambiguous parse"
+-- | A @LabeledResult@ encapsulates a future result from a computation
+-- spawned by 'lFork' or 'lForkP'.  See "LIO.Concurrent" for a
+-- description of the concurrency abstractions of LIO.
+data LabeledResult l a = LabeledResultTCB {
+    lresThreadIdTCB :: !IO.ThreadId
+    -- ^ Thread executing the computation
+  , lresLabelTCB :: !l
+    -- ^ Label of the tresult
+  , lresBlockTCB :: !(IO.MVar ())
+  , lresStatusTCB :: !(IORef (LResStatus l a))
+    -- ^ Result (when it is ready), or the label at which the thread
+    -- terminated, if that label could not flow to 'lresLabelTCB'.
+  }
+
+instance LabelOf LabeledResult where
+  labelOf = lresLabelTCB
diff --git a/LIO/TCB/Concurrent.hs b/LIO/TCB/Concurrent.hs
deleted file mode 100644
--- a/LIO/TCB/Concurrent.hs
+++ /dev/null
@@ -1,44 +0,0 @@
-{-# LANGUAGE Unsafe #-}
-
-{- |
-
-This module exports 'LabeledResult's which are effectively thread exit
-results protected by a label. See "LIO.Concurrent" for a description
-of the concurrency abstractions of LIO.
-
--}
-
-module LIO.TCB.Concurrent (
-    LabeledResult(..), LResStatus(..)
-  ) where
-
-import qualified Control.Concurrent as IO
-import Data.IORef
-
-import LIO.Label
-
-data LResStatus l a = LResEmpty
-                    | LResLabelTooHigh !l
-                    | LResResult a
-                      deriving (Show)
-
--- | A LabeledResult encapsulates a future result from a computation running
--- in a thread. It holds the 'ThreadId' and an 'LMVar' where the result is
--- stored. The thread referenced in 'lresThreadIdTCB' should fill in
--- 'lresResultTCB' (either with a value or exception), so waiting on the thread
--- should ensure that a result is ready.
-data LabeledResult l a = LabeledResultTCB {
-    lresThreadIdTCB :: !IO.ThreadId
-    -- ^ Thread executing the computation
-  , lresLabelTCB :: !l
-    -- ^ Label of the tresult
-  , lresBlockTCB :: !(IO.MVar ())
-  , lresStatusTCB :: !(IORef (LResStatus l a))
-    -- ^ Result (when it is ready), or the label at which the thread
-    -- terminated, if that label could not flow to 'lresLabelTCB'.
-  }
-
-instance LabelOf LabeledResult where
-  labelOf = lresLabelTCB
-
-
diff --git a/LIO/TCB/DCLabel.hs b/LIO/TCB/DCLabel.hs
deleted file mode 100644
--- a/LIO/TCB/DCLabel.hs
+++ /dev/null
@@ -1,22 +0,0 @@
-{-# LANGUAGE Unsafe #-}
-
-{-|
-
-This module implements the trusted compoenet of DCLabel privileges,
-documented in "LIO.DCLabel.Privs".
-Since privilege objects may be used unsafely, this module is marked
-@-XUnsafe@. Untrusted code may access privileges using the interface
-provided by "LIO.DCLabel.Privs".
-
--}
-
-module LIO.TCB.DCLabel (allPrivTCB) where
-
-import LIO.DCLabel.Core
-import LIO.DCLabel.Privs
-import LIO.TCB
-
--- | The all privilege corresponds to logical @False@
-allPrivTCB :: DCPriv
-allPrivTCB = PrivTCB dcFalse
-
diff --git a/LIO/TCB/LObj.hs b/LIO/TCB/LObj.hs
--- a/LIO/TCB/LObj.hs
+++ b/LIO/TCB/LObj.hs
@@ -27,25 +27,26 @@
 -- around each 'Handle' using the 'LObjTCB' constructor.
 module LIO.TCB.LObj (LObj(..), blessTCB, blessPTCB, GuardIO(..)) where
 
-import Data.Typeable
+import safe Data.Typeable
 
 import safe LIO.Core
+import safe LIO.Error
 import safe LIO.Label
-import safe LIO.Privs
 import LIO.TCB
 
--- | A "@LObj label object@" is a wrapper around an IO abstraction of
--- type @object@ (such as a file handle or socket) on which it is safe
--- to do @IO@ operations in the 'LIO' monad when the caller can read
--- and write a particular label.  It is the job of the trusted code
--- constructing such a @LObj@ object to ensure both that the same IO
--- object is only ever blessed with one label, and that the
+-- | A \"@LObj label object@\" is a wrapper around an IO abstraction
+-- of type @object@ (such as a file handle or socket) on which it is
+-- safe to do @IO@ operations in the 'LIO' monad when the caller can
+-- read and write a particular label.  It is the job of the trusted
+-- code constructing such a @LObj@ object to ensure both that the same
+-- IO object is only ever blessed with one label, and that the
 -- abstraction combined with its blessed IO operations (see
 -- 'blessTCB') cannot be used to communicate with code running at
 -- different labels.
 data LObj label object = LObjTCB !label !object deriving (Typeable)
 
 instance LabelOf LObj where
+  {-# INLINE labelOf #-}
   labelOf (LObjTCB l _) = l
 
 instance (Label l, Show t) => ShowTCB (LObj l t) where
@@ -83,6 +84,7 @@
   macro(a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> a9 -> a10, \
         a1 a2 a3 a4 a5 a6 a7 a8 a9 a10)
 
+-- | Class for lifting 'IO' actions.
 class GuardIO l io lio | l io -> lio where
   -- | Lifts an 'IO' action in the 'LIO' monad, executing a guard
   -- before calling the function.
@@ -101,17 +103,23 @@
 -- one.  The 'LIO' version expects a 'LObj' argument, and before
 -- performing any IO uses 'guardWrite' to check that the current label
 -- can write the label in the 'LObj' object.
+-- 
+-- The first argument should be the name of the function being defined
+-- with @blessTCB@.  Its purpose is to enhance error reporting.
 --
 -- Note that @io@ and @lio@ are function types (of up to nine
 -- arguments), which must be the same in all types except the monad.
 -- For example, if @io@ is @Int -> String -> IO ()@, then @lio@ must
 -- be @Int -> String -> LIO l ()@.
-blessTCB :: (GuardIO l io lio, Label l) => (a -> io) -> (LObj l a) -> lio
+blessTCB :: (GuardIO l io lio, Label l) =>
+            String -> (a -> io) -> (LObj l a) -> lio
 {-# INLINE blessTCB #-}
-blessTCB io (LObjTCB l a) = guardIOTCB (guardWrite l) (io a)
+blessTCB name io (LObjTCB l a) =
+  guardIOTCB (withContext name $ guardWrite l) (io a)
 
 -- | A variant of 'blessTCB' that takes a privilege argument.
 blessPTCB :: (GuardIO l io lio, PrivDesc l p) =>
-             (a -> io) -> Priv p -> (LObj l a) -> lio
+             String -> (a -> io) -> Priv p -> (LObj l a) -> lio
 {-# INLINE blessPTCB #-}
-blessPTCB io p (LObjTCB l a) = guardIOTCB (guardWriteP p l) (io a)
+blessPTCB name io p (LObjTCB l a) =
+  guardIOTCB (withContext name $ guardWriteP p l) (io a)
diff --git a/lio.cabal b/lio.cabal
--- a/lio.cabal
+++ b/lio.cabal
@@ -1,5 +1,5 @@
 Name:           lio
-Version:        0.10.0.0
+Version:        0.11.0.0
 Cabal-Version:  >= 1.8
 Build-type:     Simple
 License:        GPL
@@ -9,38 +9,49 @@
 Synopsis:       Labeled IO Information Flow Control Library
 Category:       Security
 Description:
+
   The /Labeled IO/ (LIO) library is an information flow control (IFC)
   library. IFC is a mechanism that enforces security policies by
   tracking and controlling the flow of information within a system.
-  Different from discretionary access control (think UNIX file
-  permissions), with IFC you can execute an untrusted computation on
-  your secret data and be sure that it does not leak it or overwrite
-  it.
+  Unlike discretionary access control (such as UNIX file permissions),
+  IFC permits scenarios in which untrusted computation may have the
+  ability to manipulate secret data without having the ability to
+  further disclose that data.
 
   .
+
   LIO is an IFC library that can be used to implement such untrusted
-  computations. LIO provides combinators similar to those of 'IO' for
-  performing side-effecting computations (e.g., accessing the
-  filesystem, modifying mutable references, throwing exceptions, etc.)
+  computations.  LIO provides combinators similar to those of 'IO' for
+  performing side-effecting computations (e.g., modifying mutable
+  references, forking threads, throwing and catching exceptions, etc.)
   To track and control the flow of information, LIO associates a
-  security policy, usually called a /label/, with every piece of data.
-  A label may, for example, impose a restriction on who can observe,
-  propagate, or modify the data labeled as such.  Different from
-  standard IO operations, the LIO counterparts usually take an
-  additional parameter for the label which they inspect before
-  actually performing the (underlying IO) side-effecting computation.
-  So, before writing to a file LIO asserts that the write will not
-  violate any security policies associated with the file or the data
-  to be written.
+  security policy, called a /label/, with every piece of data.  A
+  label may, for example, impose a restriction on who can observe,
+  propagate, or modify the data to which it applies.  Unlike standard
+  IO operations, the LIO counterparts check the vailidity of labels
+  before performing the (underlying IO) side-effecting computation.
+  For example, before writing to a labeled variable, LIO asserts that
+  the write will not violate any security policies associated with the
+  data to be written.
 
   .
 
   Most code should import module "LIO" and whichever label format the
-  application is using (e.g., "LIO.DCLabel"). All untrusted code
-  should have type 'LIO', which trusted code can safely execute with
-  'evalLIO'. See "LIO" for a description of the core library API.
+  application is using (e.g., "LIO.DCLabel" to use the format that
+  ships with the library).  Side-effecting code should be specified as
+  actions in the 'LIO' monad.  See "LIO.Core" for a description of the
+  core library API, "LIO.Label" for a discussion of labels, and
+  "LIO.Run" for functions allowing one to run an 'LIO' computation
+  from the 'IO' monad.
 
+  .
 
+  WARNING:  For security, untrusted code must always be compiled with
+  the @-XSafe@ and @-fpackage-trust@ /SafeHaskell/ flags. See
+  <http://www.haskell.org/ghc/docs/latest/html/users_guide/safe-haskell.html>
+  for more details on the guarantees provided by SafeHaskell.
+
+
 Extra-source-files:
   examples/dclabel.hs
   examples/gate.hs
@@ -56,6 +67,7 @@
     base          >= 4.5     && < 5.0
    ,containers
    ,bytestring
+   ,hashable      >= 1.2
 
   GHC-options: -Wall -fno-warn-orphans
 
@@ -67,23 +79,19 @@
     LIO.Label
     -- * Core library
     LIO.Core
+    LIO.Error
     LIO.Exception
     -- * Labeled values
     LIO.Labeled
     -- * Labeled IORefs
     LIO.LIORef
     -- * LIO privileges
-    LIO.Privs
+    LIO.Delegate
     -- * Concurrency
     LIO.Concurrent
     LIO.Concurrent.LMVar
     -- * DCLabels
     LIO.DCLabel
-    LIO.DCLabel.Core
-    LIO.DCLabel.Privs
-    LIO.DCLabel.DSL
     -- * Privileged internals
     LIO.TCB
     LIO.TCB.LObj
-    LIO.TCB.Concurrent
-    LIO.TCB.DCLabel