Yggdrasil.Adversarial

Exposes type for reasoning about adversaries. Generally speaking, a Functionality may request interfaces from an Adversary, which need to be supplied for it to run. The adversary also exposes some power to the environment to arbitrarily control these interfaces. Functionalities should be aware that the adversary may respond with anything correctly typed, and is explicitly permitted to returning Nothing. WithAdversary' provides an interface to repair unacceptable responses before the functionality itself is called.

Documentation

type Adversary s c as bs = Functionality s c (as +|+ MaybeMap bs)

An adversary is a functionality that exposes some interfaces to the environment, and some interfaces returning Maybes to some other party.

type family MaybeMap (bs :: [(*, *)]) = (ys :: [(*, *)]) | ys -> bs where ...

Maps a list of '(in, out) type tuples to '(in, Maybe out).

Equations

MaybeMap '[] = '[]

MaybeMap ('(a, b) ': xs) = '(a, Maybe b) ': MaybeMap xs

data WithAdversary s (ts :: [(*, *)]) b

Allows construction of b given a list of interfaces ts from the adversary. The adversarial interfaces return Maybes on all interfaces.

Instances

CreateAdversarial s c as bs (WithAdversary s bs b) b

Defined in Yggdrasil.Adversarial

Methods

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

data WithAdversary' s c (as :: [(*, *)]) (bs :: [(*, *)])

Allows construction of a Functionality with state c and interface bs whjen given a list of interfaces as from the adversary. The adversarial interface is corrected, by passing it through a filter ensuring valid responses.

Constructors

WithAdversary' (HList (Interfaces s (MaybeMap as)) -> HList (Operations s c as)) (HList (Operations s c as) -> Functionality s c bs)

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 NoAdversary s (bs :: [(*, *)]) where

The empty adversary returns Nothing.

Minimal complete definition

nullOperations

Methods

nullOperations :: HList (Operations s () (MaybeMap bs))

noAdversary :: Adversary s () '[] bs

Instances

NoAdversary s ([] :: [(*, *)])

Defined in Yggdrasil.Adversarial

Methods

nullOperations :: HList (Operations s () (MaybeMap []))

noAdversary :: Adversary s () [] []

NoAdversary s xs => NoAdversary s ((,) a b ': xs)

Defined in Yggdrasil.Adversarial

Methods

nullOperations :: HList (Operations s () (MaybeMap ((a, b) ': xs)))

noAdversary :: Adversary s () [] ((a, b) ': xs)

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

Closely corresponding to Interfaces, but also receiving a reference to the original sender.

Equations

DummyInterfaces s '[] = '[]

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

class DummyAdversary s (bs :: [(*, *)]) where

A dummy adversary executes the interfaces the environments hands it.

Minimal complete definition

operations

Methods

operations :: HList (DummyInterfaces s (MaybeMap bs)) -> HList (Operations s () (MaybeMap bs))

dummyAdversary :: HList (DummyInterfaces s (MaybeMap bs)) -> Adversary s () '[] bs

Instances

DummyAdversary s ([] :: [(*, *)])

Defined in Yggdrasil.Adversarial

Methods

operations :: HList (DummyInterfaces s (MaybeMap [])) -> HList (Operations s () (MaybeMap []))

dummyAdversary :: HList (DummyInterfaces s (MaybeMap [])) -> Adversary s () [] []

DummyAdversary s bs => DummyAdversary s ((,) a b ': bs)

Defined in Yggdrasil.Adversarial

Methods

operations :: HList (DummyInterfaces s (MaybeMap ((a, b) ': bs))) -> HList (Operations s () (MaybeMap ((a, b) ': bs)))

dummyAdversary :: HList (DummyInterfaces s (MaybeMap ((a, b) ': bs))) -> Adversary s () [] ((a, b) ': bs)

class CreateAdversarial s c as bs adv b where

Creates an adversarial functionality given a suitable adversary.

Minimal complete definition

createAdversarial

Methods

createAdversarial :: (HSplit (Interfaces s (as +|+ MaybeMap bs)) (Interfaces s as) (Interfaces s (MaybeMap bs)), InterfaceMap s c (as +|+ MaybeMap bs)) => Adversary s c as bs -> adv -> Action s (HList (Interfaces s as), b)

Instances

CreateAdversarial s c as bs (WithAdversary s bs b) b

Defined in Yggdrasil.Adversarial

Methods

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

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)