Yggdrasil.ExecutionModel

Defines the basic model of execution for Yggdrasil. This is modelled after, but not directly equal to, the Universal Composability framework by Ran Canetti.

Usage typically involves constructing a complex Action, and then running it.

Documentation

type Operation s c a b = Ref s -> a -> StateT c (Action s) b

Describes what a node with internal state of type c does when passed an input of type a by Ref s.

data RealRef s a

A reference to an actual node in the system.

data Ref s

A reference to a node, either RealRef, or external to the system.

Constructors

External

Instances

Eq (Ref s)

Defined in Yggdrasil.ExecutionModel

Methods

(==) :: Ref s -> Ref s -> Bool

(/=) :: Ref s -> Ref s -> Bool

data Action s b where

Yggdrasil's version of IO. Is self-contained, and can be opened with run.

Constructors

Abort :: Action s b

Fail. This should be used over actual errors!

SecParam :: Action s Int

Retrieves the security parameter of the running system.

Sample :: Distribution b -> Action s b

Samples from a distribution.

Create :: InterfaceMap s c ops => Functionality s c (ops :: [(*, *)]) -> Action s (HList (Interfaces s ops))

Creates a new node from a functionality specification.

Instances

Monad (Action s)

Defined in Yggdrasil.ExecutionModel

Methods

(>>=) :: Action s a -> (a -> Action s b) -> Action s b

(>>) :: Action s a -> Action s b -> Action s b

return :: a -> Action s a

fail :: String -> Action s a

Functor (Action s)

Defined in Yggdrasil.ExecutionModel

Methods

fmap :: (a -> b) -> Action s a -> Action s b

(<$) :: a -> Action s b -> Action s a

MonadFail (Action s)

Defined in Yggdrasil.ExecutionModel

Methods

fail :: String -> Action s a

Applicative (Action s)

Defined in Yggdrasil.ExecutionModel

Methods

pure :: a -> Action s a

(<*>) :: Action s (a -> b) -> Action s a -> Action s b

liftA2 :: (a -> b -> c) -> Action s a -> Action s b -> Action s c

(*>) :: Action s a -> Action s b -> Action s b

(<*) :: Action s a -> Action s b -> Action s a

type family Operations s c (xs :: [(*, *)]) = (ys :: [*]) | ys -> xs where ...

Given a list of tuples of input and output types, construct a corresponding list of Operation types.

Equations

Operations s c '[] = '[]

Operations s c ('(a, b) ': xs) = Operation s c a b ': Operations s c xs

type family Interfaces s (xs :: [(*, *)]) = (ys :: [*]) | ys -> xs where ...

Given a list of tuples of input and output types, construct a corresponding list of Interface types.

Equations

Interfaces s '[] = '[]

Interfaces s ('(a, b) ': xs) = (a -> Action s b) ': Interfaces s xs

data Functionality s c ops

A functionality is a stateful node, with an initial state, and an interface typed by a list of input/output type tuples, and defined through a HList of Operations.

Constructors

Functionality c (HList (Operations s c ops))

Instances

CreateAdversarial s c as bs (WithAdversary' s c bs cs) (Functionality s c cs)

Defined in Yggdrasil.Adversarial

Methods

createAdversarial :: Adversary s c as bs -> WithAdversary' s c bs cs -> Action s (HList (Interfaces s as), Functionality s c cs)

class InterfaceMap s c (ts :: [(*, *)]) where

States we can create interfaces from operations. Implemented for all ts.

Minimal complete definition

ifmap

Methods

ifmap :: RealRef s c -> HList (Operations s c ts) -> HList (Interfaces s ts)

Instances

InterfaceMap s c ([] :: [(*, *)])

Defined in Yggdrasil.ExecutionModel

Methods

ifmap :: RealRef s c -> HList (Operations s c []) -> HList (Interfaces s [])

InterfaceMap s c as => InterfaceMap s c ((,) a b ': as)

Defined in Yggdrasil.ExecutionModel

Methods

ifmap :: RealRef s c -> HList (Operations s c ((a, b) ': as)) -> HList (Interfaces s ((a, b) ': as))

class ForceSample t where

States that we can forcibly sample from a type, such that with negligible probabily there is a collision between samples.

Minimal complete definition

forceSample

Methods

forceSample :: Action s t

Instances

ForceSample [Bool]

Defined in Yggdrasil.ExecutionModel

Methods

forceSample :: Action s [Bool]

run :: (forall s. Action s b) -> DistributionT Maybe b

Simulates a world running an external action.