Browse Source

Yggdrasil is a distribution + minor changes.

tags/0.1.0.0
Thomas Kerber 1 year ago
parent
commit
e0d48b818f
Signed by: Thomas Kerber <t.kerber@ed.ac.uk> GPG Key ID: 8489B911F9ED617B
8 changed files with 89 additions and 65 deletions
  1. +1
    -1
      default.nix
  2. +10
    -7
      src/Yggdrasil/Distribution.hs
  3. +33
    -31
      src/Yggdrasil/ExecutionModel.hs
  4. +5
    -5
      src/Yggdrasil/Functionalities.hs
  5. +5
    -4
      tests/ExecTests.hs
  6. +10
    -10
      tests/FunctTests.hs
  7. +20
    -5
      yggdrasil.cabal
  8. +5
    -2
      yggdrasil.nix

+ 1
- 1
default.nix View File

@@ -1,2 +1,2 @@
{ pkgs ? import <nixpkgs> { } }:
pkgs.haskellPackages.callPackage ./cabal.nix { }
pkgs.haskellPackages.callPackage ./yggdrasil.nix { }

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

@@ -1,10 +1,10 @@
{-# LANGUAGE MultiParamTypeClasses,
ExistentialQuantification,
Rank2Types,
ScopedTypeVariables,
TupleSections #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}

module Yggdrasil.Distribution (Distribution, Sampler, sample, coin, uniform) where
module Yggdrasil.Distribution (
Distribution, Sampler, sample, sample', coin, uniform
) where

import Control.Monad
import Crypto.Random
@@ -29,7 +29,7 @@ class Sampler s where
sampleCoin :: s -> (Bool, s)

instance Sampler SystemDRG where
sampleCoin s = (if b .&. 1 == 1 then True else False, s')
sampleCoin s = (b .&. 1 == 1, s')
where
(ba :: B.Bytes, s') = randomBytesGenerate 1 s
(b, _) = fromJust $ B.uncons ba
@@ -37,6 +37,9 @@ instance Sampler SystemDRG where
sample :: Sampler s => s -> Distribution b -> (b, s)
sample s (Distribution f) = f s

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

coin :: Distribution Bool
coin = Distribution sampleCoin


+ 33
- 31
src/Yggdrasil/ExecutionModel.hs View File

@@ -1,10 +1,8 @@
{-# LANGUAGE TypeFamilies,
GADTs,
FlexibleContexts,
ConstraintKinds,
ScopedTypeVariables,
TypeOperators,
TupleSections #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeOperators #-}

module Yggdrasil.ExecutionModel (
Operation, WeakRef, Action, Functionality(..), type (->>), (->>), external,
@@ -12,6 +10,8 @@ module Yggdrasil.ExecutionModel (
) where

import Control.Monad
import Control.Monad.Trans.Class
import Control.Monad.Trans.Maybe
import Data.Dynamic
import Yggdrasil.Distribution

@@ -21,7 +21,7 @@ newtype World = World [Dynamic]
-- state 's'.
type Operation s a b = (s, WeakRef, a) -> Action (s, b)

data Functionality s b = Functionality s (Action b)
data Functionality s a b = Functionality s (a -> Action b)

data a ->> b where
Ref :: Typeable s => Int -> Operation s a b -> (a ->> b)
@@ -70,7 +70,7 @@ data Action b where
Self :: Action WeakRef
Sample :: Distribution b -> Action b
Send :: a -> (a ->> b) -> Action b
Create :: Typeable s => Functionality s b -> Action b
Create :: Typeable s => Functionality s a b -> a -> Action b
Compose :: Action c -> (c -> Action b) -> Action b

-- Export visible constructors as functions.
@@ -94,7 +94,7 @@ doSample = Sample
(->>) = Send
-- | Creates a new autonomous party, with a given initial state, and a given
-- program.
create :: Typeable s => Functionality s b -> Action b
create :: Typeable s => Functionality s a b -> a -> Action b
create = Create

instance Functor Action where
@@ -106,26 +106,28 @@ instance Monad Action where
a >>= b = Compose a b

-- | Execute a top-level action in the Yggdrasil execution model.
run :: Sampler s => s -> Action b -> Maybe (b, s)
run s a = (\(_, b, s') -> (b, s')) <$> run' s (World []) external a

run' :: Sampler s =>
s -> World -> WeakRef -> Action b -> Maybe (World, b, s)
run' _ _ _ Abort = Nothing
run' s wld slf (StrengthenSelf f) =
(wld, , s) <$> strengthen wld slf f
run' s wld slf Self = return (wld, slf, s)
run' s wld _ (Sample d) = let (y, s') = sample s d in Just (wld, y, s')
run' s (World xs) from (Send m to@(Ref idx func)) = do
dyns <- safeIdx xs idx
st <- fromDynamic dyns
run :: Action b -> Distribution (Maybe b)
run a = runMaybeT $ snd <$> run' (World []) external a

--run :: Sampler s => s -> Action b -> Maybe (b, s)
--run s a = (\(_, b, s') -> (b, s')) <$> run' s (World []) external a

run' :: World -> WeakRef -> Action b -> MaybeT Distribution (World, b)
run' _ _ Abort = MaybeT $ return Nothing
run' wld slf (StrengthenSelf f) = MaybeT $ return $
(wld,) <$> strengthen wld slf f
run' wld slf Self = MaybeT $ return $ Just (wld, slf)
run' wld _ (Sample d) = lift $ (wld,) <$> d
run' (World xs) from (Send m to@(Ref idx func)) = do
dyns <- MaybeT $ return $ safeIdx xs idx
st <- MaybeT $ return $ fromDynamic dyns
let action = func (st, from, m)
(World xs', (st', y), s') <- run' s (World xs) (weaken to) action
xs'' <- safeWriteIdx xs' idx (toDyn st')
return (World xs'', y, s')
(World xs', (st', y)) <- run' (World xs) (weaken to) action
xs'' <- MaybeT $ return $ safeWriteIdx xs' idx (toDyn st')
return (World xs'', y)
-- Note: This could cause a re-entrancy style bug!
run' s wld _ (Create (Functionality st a)) =
let (wld', from') = new wld st in run' s wld' from' a
run' s wld from (Compose a f) = do
(wld', b, s') <- run' s wld from a
run' s' wld' from (f b)
run' wld _ (Create (Functionality st f) x) =
let (wld', from') = new wld st in run' wld' from' (f x)
run' wld from (Compose a f) = do
(wld', b) <- run' wld from a
run' wld' from (f b)

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

@@ -1,7 +1,7 @@
{-# LANGUAGE TypeOperators #-}

module Yggdrasil.Functionalities (
commonRandomString, randomOracle
ROState, commonRandomString, randomOracle
) where

import Data.Dynamic
@@ -12,8 +12,8 @@ crsOp :: Distribution b -> Operation (Maybe b) () b
crsOp _ (Just x, _, ()) = return (Just x, x)
crsOp d (Nothing, _, ()) = (\x -> (Just x, x)) <$> doSample d
commonRandomString :: Typeable b =>
Distribution b -> Functionality (Maybe b) (() ->> b)
commonRandomString d = Functionality Nothing (interface (crsOp d))
Functionality (Maybe b) (Distribution b) (() ->> b)
commonRandomString = Functionality Nothing (interface . crsOp)

type ROState a b = [(a, b)]
roLookup :: Eq a => ROState a b -> a -> Maybe b
@@ -27,5 +27,5 @@ roOp d (xs, _, x') = case roLookup xs x' of
y <- doSample d
return ((x', y):xs, y)
randomOracle :: (Eq a, Typeable a, Typeable b) =>
Distribution b -> Functionality (ROState a b) (a ->> b)
randomOracle d = Functionality [] (interface (roOp d))
Functionality (ROState a b) (Distribution b) (a ->> b)
randomOracle = Functionality [] (interface . roOp)

+ 5
- 4
tests/ExecTests.hs View File

@@ -26,9 +26,10 @@ spec :: IO Spec
spec = do
rnd <- getSystemDRG
return $ describe "action" $ do
prop "obeys return" $ \(x::String) -> do
(fmap fst (run rnd (return x))) == Just x
prop "obeys return" $ \(x::String) ->
sample' rnd (run (return x)) == Just x
it "is exteral" $
(fmap fst (run rnd self) == Just external) `shouldBe` True
sample' rnd (run self) == Just external `shouldBe` True
it "samples evenly" $
inSampleRange (fst $ fromJust (run rnd sampleTest)) `shouldBe` True
inSampleRange (fromJust $ sample' rnd (run sampleTest))
`shouldBe` True

+ 10
- 10
tests/FunctTests.hs View File

@@ -1,5 +1,5 @@
{-# LANGUAGE ScopedTypeVariables,
TypeOperators #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}

module FunctTests (spec) where

@@ -11,33 +11,33 @@ import Yggdrasil.Functionalities

crsSameTest :: Action Bool
crsSameTest = do
crsHandle <- create $ commonRandomString (uniform [0..10000::Int])
crsHandle <- create commonRandomString (uniform [0..10000::Int])
fst' <- () ->> crsHandle
snd' <- () ->> crsHandle
return (fst' == snd')

roSameTest :: Action Bool
roSameTest = do
roHandle :: (Int ->> Int) <- create $ randomOracle (uniform [0..1000::Int])
roHandle :: (Int ->> Int) <- create randomOracle (uniform [0..1000::Int])
fst' <- 1 ->> roHandle
snd' <- 1 ->> roHandle
return (fst' == snd')

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

spec :: IO Spec
spec = do
rnd <- getSystemDRG
return $ do
describe "common random string" $ do
describe "common random string" $
it "returns the same value" $
(fmap fst (run rnd crsSameTest)) `shouldBe` Just True
sample' rnd (run crsSameTest) `shouldBe` Just True
describe "random oracle" $ do
it "returns the same for the same query" $
(fmap fst (run rnd roSameTest)) `shouldBe` Just True
sample' rnd (run roSameTest) `shouldBe` Just True
it "is random with different queries" $
(fmap fst (run rnd roAllEqual)) `shouldBe` Just False
sample' rnd (run roAllEqual) `shouldBe` Just False

+ 20
- 5
yggdrasil.cabal View File

@@ -17,10 +17,19 @@ extra-source-files: ChangeLog.md
cabal-version: >=1.10

library
exposed-modules: Yggdrasil.Distribution, Yggdrasil.ExecutionModel, Yggdrasil.Functionalities
exposed-modules: Yggdrasil.Distribution
Yggdrasil.ExecutionModel
Yggdrasil.Functionalities
-- other-modules:
other-extensions: ExistentialQuantification, MultiParamTypeClasses, AllowAmbiguousTypes, TypeFamilies, GADTs, FlexibleContexts, ScopedTypeVariables
build-depends: base, cryptonite, memory
other-extensions: GADTs
Rank2Types
ScopedTypeVariables
TupleSections
TypeOperators
build-depends: base
, cryptonite
, memory
, transformers
hs-source-dirs: src
default-language: Haskell2010
ghc-options: -Wall -Werror
@@ -28,9 +37,15 @@ library
test-suite spec
type: exitcode-stdio-1.0
other-extensions: ScopedTypeVariables
TypeOperators
default-language: Haskell2010
hs-source-dirs: tests
ghc-options: -Wall -Werror
main-is: Spec.hs
other-modules: ExecTests, FunctTests
build-depends: cryptonite, base, hspec, QuickCheck, yggdrasil
other-modules: ExecTests
FunctTests
build-depends: cryptonite
, base
, hspec
, QuickCheck
, yggdrasil

cabal.nix → yggdrasil.nix View File

@@ -1,9 +1,12 @@
{ mkDerivation, base, random, stdenv }:
{ mkDerivation, base, cryptonite, hspec, memory, QuickCheck, stdenv
, transformers
}:
mkDerivation {
pname = "yggdrasil";
version = "0.1.0.0";
src = ./.;
libraryHaskellDepends = [ base random ];
libraryHaskellDepends = [ base cryptonite memory transformers ];
testHaskellDepends = [ base cryptonite hspec QuickCheck ];
homepage = "https://git.drwx.org/phd/yggdrasil";
description = "Executable specifications of composable security protocols";
license = stdenv.lib.licenses.agpl3;

Loading…
Cancel
Save