Browse Source

Remove 'from' parameter. Fixes #1.

oldhaskell
Thomas Kerber 1 year ago
parent
commit
aadbb5765b
Signed by: tk <tk@drwx.org> GPG Key ID: 8489B911F9ED617B
4 changed files with 44 additions and 71 deletions
  1. +5
    -10
      src/Yggdrasil/Adversarial.hs
  2. +13
    -34
      src/Yggdrasil/ExecutionModel.hs
  3. +22
    -22
      src/Yggdrasil/Functionalities.hs
  4. +4
    -5
      src/Yggdrasil/MetaProtocol.hs

+ 5
- 10
src/Yggdrasil/Adversarial.hs View File

@@ -25,7 +25,6 @@ module Yggdrasil.Adversarial
, WithAdversary
, WithAdversary'(..)
, NoAdversary(..)
, DummyInterfaces
, DummyAdversary(..)
, CreateAdversarial(..)
) where
@@ -35,7 +34,7 @@ import Control.Monad.Trans.Class (lift)
import Yggdrasil.ExecutionModel (Action (Create),
Functionality (Functionality),
InterfaceMap, Interfaces, Operation,
Operations, Ref)
Operations)
import Yggdrasil.HList (type (+|+), HList ((:::), Nil),
HSplit (hsplit))

@@ -71,21 +70,15 @@ instance NoAdversary s '[] where
nullOperations = Nil

instance NoAdversary s xs => NoAdversary s ('( a, b) ': xs) where
nullOperations = (\_ _ -> return Nothing) ::: nullOperations @s @xs

type family DummyInterfaces s (xs :: [(*, *)]) = (ys :: [*]) | ys -> xs where
DummyInterfaces s '[] = '[]
DummyInterfaces s ('( a, b) ': xs) = (Ref s -> a -> Action s b) ': DummyInterfaces s xs
nullOperations = (\_ -> return Nothing) ::: nullOperations @s @xs

-- | A dummy adversary executes the interfaces the environments hands it.
class DummyAdversary s (bs :: [(*, *)]) where
operations ::
HList (DummyInterfaces s (MaybeMap bs))
HList (Interfaces s (MaybeMap bs))
-> HList (Operations s () (MaybeMap bs))
dummyAdversary ::
HList (DummyInterfaces s (MaybeMap bs)) -> Adversary s () '[] bs
HList (Interfaces s (MaybeMap bs)) -> Adversary s () '[] bs
dummyAdversary = Functionality () . operations @s @bs

instance DummyAdversary s '[] where
@@ -93,7 +86,7 @@ instance DummyAdversary s '[] where

instance DummyAdversary s bs => DummyAdversary s ('( a, b) ': bs) where
operations (b ::: bs) =
((\ref x -> lift $ b ref x) :: Operation s () a (Maybe b)) :::
(lift . b :: Operation s () a (Maybe b)) :::
operations @s @bs bs

-- | Creates an adversarial functionality given a suitable adversary.


+ 13
- 34
src/Yggdrasil/ExecutionModel.hs View File

@@ -18,8 +18,6 @@
-- it.
module Yggdrasil.ExecutionModel
( Operation
, RealRef
, Ref(External)
, Action(Abort, Sample, Create, SecParam)
, Operations
, Interfaces
@@ -43,7 +41,7 @@ import Yggdrasil.HList (HList ((:::), Nil))

-- | Describes what a node with internal state of type @c@ does when passed an
-- input of type @a@ by @Ref s@.
type Operation s c a b = Ref s -> a -> StateT c (Action s) b
type Operation s c a b = a -> StateT c (Action s) b

-- | Given a list of tuples of input and output types, construct a
-- corresponding list of 'Operation' types.
@@ -64,30 +62,10 @@ data Functionality s c ops =
Functionality c
(HList (Operations s c ops))

type ID s = STRef s ()

data SendRef s a b =
forall c. SendRef (RealRef s c)
forall c. SendRef (STRef s c)
(Operation s c a b)

data RealRef s a =
RealRef (STRef s a)
(ID s)

data Ref s
= forall a. Ref (RealRef s a)
| External

instance Eq (Ref s) where
External == External = True
Ref (RealRef _ a) == Ref (RealRef _ b) = a == b
_ == _ = False

weaken :: SendRef s a b -> Ref s
weaken (SendRef ref _) = Ref ref

-- | Yggdrasil's version of 'IO'. Is self-contained, and can be opened with
-- 'run'.
data Action s b where
@@ -121,27 +99,26 @@ instance MonadFail (Action s) where
-- | Simulates a world running an external action.
run :: (forall s. Action s b) -> DistributionT Maybe b
run a =
DistributionT $ \rng -> runST $ runMaybeT $ runDistT (run' External a) rng
DistributionT $ \rng -> runST $ runMaybeT $ runDistT (run' a) rng

run' :: Ref s -> Action s b -> DistributionT (MaybeT (ST s)) b
run' _ Abort = DistributionT $ \_ -> MaybeT $ return Nothing
run' :: Action s b -> DistributionT (MaybeT (ST s)) b
run' Abort = DistributionT $ \_ -> MaybeT $ return Nothing
-- TODO: Make a parameter
run' _ SecParam = return 128
run' _ (Sample d) = liftDistribution d
run' from (Send to@(SendRef (RealRef (ptr :: STRef s c) _) op) msg) = do
run' SecParam = return 128
run' (Sample d) = liftDistribution d
run' (Send (SendRef (ptr :: STRef s c) op) msg) = do
c <- lift . lift $ readSTRef ptr
(b, c') <- run' (weaken to) (runStateT (op from msg) c)
(b, c') <- run' (runStateT (op msg) c)
lift . lift $ writeSTRef ptr c'
return b
run' _ (Create (Functionality c ops)) = do
run' (Create (Functionality c ops)) = do
ptr <- lift . lift $ newSTRef c
id' <- lift . lift $ newSTRef ()
return $ ifmap (RealRef ptr id') ops
run' from (Compose a f) = run' from a >>= run' from . f
return $ ifmap ptr ops
run' (Compose a f) = run' a >>= run' . f

-- | States we can create interfaces from operations. Implemented for all @ts@.
class InterfaceMap s c (ts :: [(*, *)]) where
ifmap :: RealRef s c -> HList (Operations s c ts) -> HList (Interfaces s ts)
ifmap :: STRef s c -> HList (Operations s c ts) -> HList (Interfaces s ts)

instance InterfaceMap s c '[] where
ifmap _ Nil = Nil


+ 22
- 22
src/Yggdrasil/Functionalities.hs View File

@@ -21,12 +21,12 @@ import Yggdrasil.Distribution (Distribution)
import Yggdrasil.ExecutionModel (Action (Sample),
ForceSample (forceSample),
Functionality (Functionality),
Interfaces, Operation, Operations,
Ref)
Interfaces, Operation, Operations)
import Yggdrasil.HList (HList ((:::), Nil))
import Yggdrasil.Nat (Zn)

crsOp :: Distribution b -> Operation s (Maybe b) () b
crsOp d _ () =
crsOp d () =
get >>= \case
Just x -> return x
Nothing -> do
@@ -49,7 +49,7 @@ roLookup x' ((x, y):_)
roLookup x (_:xs) = roLookup x xs

roOp :: Eq a => Distribution b -> Operation s (ROState a b) a b
roOp d _ x =
roOp d x =
(roLookup x <$> get) >>= \case
Just y -> return y
Nothing -> do
@@ -64,45 +64,45 @@ randomOracle d = Functionality [] (roOp d ::: Nil)

-- | The state of a 'signature' functionality. Consists of previously recorded
-- signatures, and their corresponding messages and signers.
type SigState s msg sig = [(msg, sig, Ref s)]
type SigState s n msg sig = [(Zn n, (msg, sig))]

verifyOp ::
(Eq msg, Eq sig) => Operation s (SigState s msg sig) (msg, sig, Ref s) Bool
verifyOp _ s = (s `elem`) <$> get
(Eq msg, Eq sig) => Operation s (SigState s n msg sig) (Zn n, (msg, sig)) Bool
verifyOp s = (s `elem`) <$> get

fixAdv ::
(Eq msg, Eq sig, ForceSample sig)
=> HList (Interfaces s '[ '( (msg, Ref s), Maybe sig)])
-> HList (Operations s (SigState s msg sig) '[ '( (msg, Ref s), sig)])
=> HList (Interfaces s '[ '( (Zn n, msg), Maybe sig)])
-> HList (Operations s (SigState s n msg sig) '[ '( (Zn n, msg), sig)])
fixAdv (sign ::: Nil) = sign' ::: Nil
where
sign' _ (msg, ref) = do
sign' (p, msg) = do
sig <-
lift (sign (msg, ref)) >>= \case
lift (sign (p, msg)) >>= \case
Just s -> do
st <- get
if (msg, s, ref) `elem` st
then forceSample' msg ref
if (p, (msg, s)) `elem` st
then forceSample' msg p
else return s
Nothing -> forceSample' msg ref
modify ((msg, sig, ref) :)
Nothing -> forceSample' msg p
modify ((p, (msg, sig)) :)
return sig
forceSample' msg ref = do
forceSample' msg p = do
sig <- lift forceSample
st <- get
-- This may recursive infinitely iff the signature space is too small!
-- This is a feature, not a bug.
if (msg, sig, ref) `elem` st
then forceSample' msg ref
if (p, (msg, sig)) `elem` st
then forceSample' msg p
else return sig

-- | A robust signature functionality.
signature ::
(Eq msg, Eq sig, ForceSample sig)
=> WithAdversary' s (SigState s msg sig)
'[ '( (msg, Ref s), sig)]
'[ '( (msg, Ref s), sig)
, '( (msg, sig, Ref s), Bool)
=> WithAdversary' s (SigState s n msg sig)
'[ '( (Zn n, msg), sig)]
'[ '( (Zn n, msg), sig)
, '( (Zn n, (msg, sig)), Bool)
]
signature =
WithAdversary'


+ 4
- 5
src/Yggdrasil/MetaProtocol.hs View File

@@ -7,6 +7,7 @@
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeFamilyDependencies #-}
@@ -46,9 +47,7 @@ instance RelayN s n '[] where
relayNOperations _ _ = Nil

instance RelayN s n xs => RelayN s n ('( a, b) ': xs) where
relayNOperations (f ::: xs) n = lifted ::: relayNOperations @s @n @xs xs n
where
lifted _ a = lift (f (n, a))
relayNOperations (f ::: xs) n = lift . f . (n, ) ::: relayNOperations @s @n @xs xs n

type family WithZn n (ops :: [(*, *)]) = (ys :: [(*, *)]) | ys -> ops where
WithZn n '[] = '[]
@@ -69,7 +68,7 @@ npartyIdeal ::
'[ '( (), HList (NCopies n (HList (Interfaces s ops))))]
npartyIdeal f = Functionality Nothing (mkOp ::: Nil)
where
mkOp _ _ =
mkOp _ =
get >>= \case
Just i -> return i
Nothing -> do
@@ -94,7 +93,7 @@ npartyReal ::
'[ '( (), HList (NCopies n (HList (Interfaces s ops))))]
npartyReal f = Functionality Nothing (mkOp ::: Nil)
where
mkOp _ _ =
mkOp _ =
get >>= \case
Just i -> return i
Nothing -> do


Loading…
Cancel
Save