DCLabel.NanoEDSL

Operators

(.\/.) :: DisjunctionOf a b => a -> b -> Label

(./\.) :: ConjunctionOf a b => a -> b -> Label

(<>) :: Label

Empty label.

(><) :: Label

All label.

DCLabel creation

newDC

Arguments

:: NewDC a b

=> a

-> b

-> DCLabel

Given two elements create label.

Privilege object creation

newPriv :: NewPriv a => a -> Priv

Given element create privilege.

Given element create (maybe) trusted privileged object.

newTCBPriv :: NewPriv a => TCBPriv -> a -> Maybe TCBPriv