Browse Source

Now with State monad.

tags/0.1.0.0
Thomas Kerber 1 year ago
parent
commit
8621537555
Signed by: Thomas Kerber <tk@drwx.org> GPG Key ID: 8489B911F9ED617B
6 changed files with 48 additions and 35 deletions
  1. +7
    -5
      src/Yggdrasil/Distribution.hs
  2. +5
    -4
      src/Yggdrasil/ExecutionModel.hs
  3. +30
    -21
      src/Yggdrasil/Functionalities.hs
  4. +1
    -1
      src/Yggdrasil/HList.hs
  5. +4
    -4
      tests/FunctTests.hs
  6. +1
    -0
      yggdrasil.cabal

+ 7
- 5
src/Yggdrasil/Distribution.hs View File

@@ -14,6 +14,7 @@ module Yggdrasil.Distribution
) where

import Control.Monad (ap)
import Control.Monad.State.Lazy (State, runState, state)
import Control.Monad.Trans.Class (MonadTrans (lift))
import Crypto.Random (SystemDRG, randomBytesGenerate)
import Data.Bits ((.&.))
@@ -22,18 +23,19 @@ import Data.Maybe (fromJust)

newtype Distribution b =
Distribution (forall s. Sampler s =>
s -> (b, s))
State s b)

instance Functor Distribution where
fmap f x = pure f <*> x

instance Applicative Distribution where
pure x = Distribution (x, )
pure x = Distribution $ state (x, )
(<*>) = ap

instance Monad Distribution where
a >>= b =
Distribution
Distribution $
state
(\s ->
let (a', s') = sample s a
(b', s'') = sample s' (b a')
@@ -72,13 +74,13 @@ instance Sampler SystemDRG where
(b, _) = fromJust $ B.uncons ba

sample :: Sampler s => s -> Distribution b -> (b, s)
sample s (Distribution f) = f s
sample s (Distribution st) = runState st s

sample' :: Sampler s => s -> Distribution b -> b
sample' s = fst . sample s

coin :: Distribution Bool
coin = Distribution sampleCoin
coin = Distribution $ state sampleCoin

uniform :: [a] -> Distribution a
uniform xs = do

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

@@ -26,15 +26,16 @@ module Yggdrasil.ExecutionModel
import Control.Monad (ap)
import Control.Monad.Fail (MonadFail (fail))
import Control.Monad.ST (ST, runST)
import Control.Monad.State.Lazy (StateT, runStateT)
import Control.Monad.Trans.Class (lift)
import Control.Monad.Trans.Maybe (MaybeT (MaybeT), runMaybeT)
import Data.STRef (STRef, newSTRef, readSTRef,
writeSTRef)
import Yggdrasil.Distribution (Distribution, DistributionT (DistributionT, runDistT),
liftDistribution)
import Yggdrasil.HList (HList (Cons, Nil))
import Yggdrasil.HList (HList ((:::), Nil))

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

type family Operations s c (xs :: [(*, *)]) :: [*] where
Operations s c '[] = '[]
@@ -102,7 +103,7 @@ run' _ Abort = DistributionT $ \_ -> MaybeT $ return Nothing
run' _ (Sample d) = liftDistribution d
run' from (Send to@(SendRef (RealRef (ptr :: STRef s c) _) op) msg) = do
c <- lift . lift $ readSTRef ptr
(c', b) <- run' (weaken to) (op c from msg)
(b, c') <- run' (weaken to) (runStateT (op from msg) c)
lift . lift $ writeSTRef ptr c'
return b
run' _ (Create (Functionality c ops)) = do
@@ -119,4 +120,4 @@ instance InterfaceMap s c '[] where
ifmap _ Nil = Nil

instance InterfaceMap s c as => InterfaceMap s c ('( a, b) ': as) where
ifmap ref (Cons x xs) = Cons (\a -> Send (SendRef ref x) a) (ifmap ref xs)
ifmap ref (x ::: xs) = (\a -> Send (SendRef ref x) a) ::: ifmap ref xs

+ 30
- 21
src/Yggdrasil/Functionalities.hs View File

@@ -1,4 +1,5 @@
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TypeOperators #-}

module Yggdrasil.Functionalities
@@ -11,40 +12,48 @@ module Yggdrasil.Functionalities
--, robustSignature
) where

import Control.Monad.State.Lazy (get, modify, put)
import Control.Monad.Trans.Class (lift)

--import Yggdrasil.Adversarial (WithAdversary)
import Yggdrasil.Distribution (Distribution)
import Yggdrasil.ExecutionModel (Action (Sample),
Functionality (Functionality),
Operation)
import Yggdrasil.HList (HList (Cons, Nil))
import Yggdrasil.Distribution (Distribution)
import Yggdrasil.ExecutionModel (Action (Sample),
Functionality (Functionality),
Operation)
import Yggdrasil.HList (HList ((:::), Nil))

crsOp :: Distribution b -> Operation s (Maybe b) () b
crsOp _ (Just x) _ () = return (Just x, x)
crsOp d Nothing _ () = (\x -> (Just x, x)) <$> Sample d
crsOp d _ () =
get >>= \case
Just x -> return x
Nothing -> do
x <- lift $ Sample d
put $ Just x
return x

commonRandomString ::
Distribution b -> Functionality s (Maybe b) ('( (), b) ': '[])
commonRandomString d = Functionality Nothing (Cons (crsOp d) Nil)
commonRandomString :: Distribution b -> Functionality s (Maybe b) '[ '( (), b)]
commonRandomString d = Functionality Nothing (crsOp d ::: Nil)

type ROState a b = [(a, b)]

roLookup :: Eq a => ROState a b -> a -> Maybe b
roLookup [] _ = Nothing
roLookup ((x, y):_) x'
roLookup :: Eq a => a -> ROState a b -> Maybe b
roLookup _ [] = Nothing
roLookup x' ((x, y):_)
| x == x' = Just y
roLookup (_:xs) x = roLookup xs x
roLookup x (_:xs) = roLookup x xs

roOp :: Eq a => Distribution b -> Operation s (ROState a b) a b
roOp d xs _ x =
case roLookup xs x of
Just y -> return (xs, y)
roOp d _ x =
(roLookup x <$> get) >>= \case
Just y -> return y
Nothing -> do
y <- Sample d
return ((x, y) : xs, y)
y <- lift $ Sample d
modify ((x, y) :)
return y

randomOracle ::
Eq a => Distribution b -> Functionality s (ROState a b) ('( a, b) ': '[])
randomOracle d = Functionality [] (Cons (roOp d) Nil)
Eq a => Distribution b -> Functionality s (ROState a b) '[ '( a, b)]
randomOracle d = Functionality [] (roOp d ::: Nil)
-- TODO: Don't abort with bad adversaries? Would probably need a specialised s
-- though.
--type SigState m s = [(m, s, Ref)]

+ 1
- 1
src/Yggdrasil/HList.hs View File

@@ -9,4 +9,4 @@ module Yggdrasil.HList

data HList :: [*] -> * where
Nil :: HList '[]
Cons :: a -> HList as -> HList (a ': as)
(:::) :: a -> HList as -> HList (a ': as)

+ 4
- 4
tests/FunctTests.hs View File

@@ -10,11 +10,11 @@ import Test.Hspec (Spec, describe, it, shouldBe)
import Yggdrasil.Distribution (runDistT, uniform)
import Yggdrasil.ExecutionModel (Action (Create), run)
import Yggdrasil.Functionalities (commonRandomString, randomOracle)
import Yggdrasil.HList (HList (Cons, Nil))
import Yggdrasil.HList (HList ((:::), Nil))

crsSameTest :: Action s Bool
crsSameTest = do
(Cons crsHandle Nil) <-
(crsHandle ::: Nil) <-
Create $ commonRandomString (uniform [0 .. 10000 :: Int])
fst' <- crsHandle ()
snd' <- crsHandle ()
@@ -22,7 +22,7 @@ crsSameTest = do

roSameTest :: Action s Bool
roSameTest = do
(Cons (roHandle :: Int -> Action s Int) Nil) <-
((roHandle :: Int -> Action s Int) ::: Nil) <-
Create $ randomOracle (uniform [0 .. 1000 :: Int])
fst' <- roHandle 1
snd' <- roHandle 1
@@ -30,7 +30,7 @@ roSameTest = do

roAllEqual :: Action s Bool
roAllEqual = do
(Cons (roHandle :: Int -> Action s Int) Nil) <-
((roHandle :: Int -> Action s Int) ::: Nil) <-
Create $ randomOracle (uniform [0 .. 1000 :: Int])
xs <- sequence [roHandle i | i <- [1 .. 1000]]
return $ all (== head xs) (tail xs)

+ 1
- 0
yggdrasil.cabal View File

@@ -26,6 +26,7 @@ library
build-depends: base >= 4.11 && < 4.12
, cryptonite >= 0.25 && < 0.26
, memory >= 0.14 && < 0.15
, mtl >= 2.2 && < 2.3
, transformers >= 0.5 && < 0.6
hs-source-dirs: src
default-language: Haskell2010

Loading…
Cancel
Save