Documentation

Internal state of an LIO computation.

Execute an LIO action, returning its result and the final label state as a pair. Note that it returns a pair whether or not the LIO action throws an exception. Forcing the result value will re-throw the exception, but the label state will always be valid.

See also evalLIO.

A variant of runLIO that returns results in Right and exceptions in Left, much like the standard library try function.

Given an LIO computation and some initial state, return an IO action which, when executed, will perform the IFC-safe LIO computation.

Because untrusted code cannot execute IO computations, this function should only be useful within trusted code. No harm is done from exposing the evalLIO symbol to untrusted code. (In general, untrusted code is free to produce IO computations, but it cannot execute them.)

Unlike runLIO, this function throws an exception if the underlying LIO action terminates with an exception.

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.