Browse Source

Fix potential issue of using references between worlds.

tags/0.1.0.0
Thomas Kerber 1 year ago
parent
commit
b011684870
Signed by: Thomas Kerber <t.kerber@ed.ac.uk> GPG Key ID: 8489B911F9ED617B
4 changed files with 50 additions and 34 deletions
  1. +36
    -24
      src/Yggdrasil/ExecutionModel.hs
  2. +8
    -5
      tests/ExecTests.hs
  3. +4
    -3
      tests/FunctTests.hs
  4. +2
    -2
      yggdrasil.cabal

+ 36
- 24
src/Yggdrasil/ExecutionModel.hs View File

@@ -5,10 +5,9 @@

module Yggdrasil.ExecutionModel
( Operation
, Ref
, Ref(External)
, Action
, Functionality(..)
, external
, weaken
, abort
, interface
@@ -24,10 +23,11 @@ import Control.Monad.Trans.Class (lift)
import Control.Monad.Trans.Maybe (MaybeT (MaybeT), runMaybeT)
import Data.Dynamic (Dynamic, Typeable, fromDynamic,
toDyn)
import Yggdrasil.Distribution (Distribution)
import Yggdrasil.Distribution (Distribution, coin)

newtype World =
data World =
World [Dynamic]
[Bool]

-- | An operation is a stateful function of @('Ref, a) -> 'Action' b@ over
-- the state @s@.
@@ -38,34 +38,36 @@ data Functionality s b =
(Action b)

data SendRef a b where
SendRef :: Typeable s => Int -> Operation s a b -> SendRef a b
SendRef :: Typeable s => RealRef -> Operation s a b -> SendRef a b

newtype Ref =
Ref Int
data RealRef =
RealRef Int
[Bool]
deriving (Eq)

external :: Ref
external = Ref (-1)
data Ref
= Ref RealRef
| External
deriving (Eq)

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

strengthen ::
Typeable s => World -> Ref -> Operation s a b -> Maybe (SendRef a b)
strengthen (World []) _ _ = Nothing
strengthen (World (x:_)) (Ref 0) (f :: Operation s a b) = do
Typeable s => World -> RealRef -> Operation s a b -> Maybe (SendRef a b)
strengthen (World [] _) _ _ = Nothing
strengthen (World _ wid) (RealRef _ wid') _
| wid /= wid' = Nothing
strengthen (World (x:_) _) ref@(RealRef 0 _) (f :: Operation s a b) = do
_ :: s <- fromDynamic x
return $ SendRef 0 f
strengthen (World (_:xs)) wref f = do
(SendRef i f') <- strengthen (World xs) wref f
return $ SendRef (i + 1) f'
return $ SendRef ref f
strengthen (World (_:xs) wid) wref f = do
(SendRef (RealRef i w) f') <- strengthen (World xs wid) wref f
return $ SendRef (RealRef (i + 1) w) f'

new :: Typeable s => World -> s -> (World, Ref)
new (World xs) s = (World (xs ++ [toDyn s]), Ref (length xs))
new (World xs wid) s =
(World (xs ++ [toDyn s]) wid, Ref (RealRef (length xs) wid))

safeIdx :: [a] -> Int -> Maybe a
safeIdx [] _ = Nothing
@@ -128,22 +130,28 @@ instance Monad Action where
a >>= b = Compose a b

-- | Execute a top-level action in the Yggdrasil execution model.
run :: Action b -> Distribution (Maybe b)
run a = runMaybeT $ snd <$> run' (World []) external a
run :: Int -> Action b -> Distribution (Maybe b)
run secparam a =
runMaybeT
(do wid <- (lift . sequence) $ map (const coin) [0 .. secparam]
snd <$> run' (World [] wid) External a)

run' :: World -> Ref -> Action b -> MaybeT Distribution (World, b)
run' _ _ Abort = MaybeT $ return Nothing
run' wld slf (StrengthenSelf f) =
run' _ External (StrengthenSelf _) = MaybeT $ return Nothing
run' wld (Ref slf) (StrengthenSelf f) =
MaybeT $ return $ (wld, ) . Send <$> 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 to@(SendRef idx func) m) = do
run' (World _ wid) _ (Send (SendRef (RealRef _ wid') _) _)
| wid /= wid' = MaybeT $ return Nothing
run' wld@(World xs _) from (Send (SendRef to@(RealRef idx _) func) m) = do
dyns <- MaybeT $ return $ safeIdx xs idx
st <- MaybeT $ return $ fromDynamic dyns
let action = func (st, from, m)
(World xs', (st', y)) <- run' (World xs) (weaken to) action
(World xs' wid', (st', y)) <- run' wld (Ref to) action
xs'' <- MaybeT $ return $ safeWriteIdx xs' idx (toDyn st')
return (World xs'', y)
return (World xs'' wid', y)
-- Note: This could cause a re-entrancy style bug!
run' wld _ (Create (Functionality st a)) =
let (wld', from') = new wld st

+ 8
- 5
tests/ExecTests.hs View File

@@ -9,8 +9,8 @@ import Data.Maybe (fromJust)
import Test.Hspec (Spec, describe, it, shouldBe)
import Test.Hspec.QuickCheck (prop)
import Yggdrasil.Distribution (sample', uniform)
import Yggdrasil.ExecutionModel (Action, doSample, external, run,
self)
import Yggdrasil.ExecutionModel (Action, Ref (External), doSample,
run, self)

inSampleRange :: Int -> Bool
inSampleRange x = x > 4700 && x < 5300
@@ -28,10 +28,13 @@ sampleTest = sampleTest' 10000
spec :: IO Spec
spec = do
rnd <- getSystemDRG
let secparam = 128
return $
describe "action" $ do
prop "obeys return" $ \(x :: String) ->
sample' rnd (run (return x)) == Just x
it "is exteral" $ sample' rnd (run self) == Just external `shouldBe` True
sample' rnd (run secparam (return x)) == Just x
it "is exteral" $
sample' rnd (run secparam self) == Just External `shouldBe` True
it "samples evenly" $
inSampleRange (fromJust $ sample' rnd (run sampleTest)) `shouldBe` True
inSampleRange (fromJust $ sample' rnd (run secparam sampleTest)) `shouldBe`
True

+ 4
- 3
tests/FunctTests.hs View File

@@ -35,12 +35,13 @@ roAllEqual = do
spec :: IO Spec
spec = do
rnd <- getSystemDRG
let secparam = 128
return $ do
describe "common random string" $
it "returns the same value" $
sample' rnd (run crsSameTest) `shouldBe` Just True
sample' rnd (run secparam crsSameTest) `shouldBe` Just True
describe "random oracle" $ do
it "returns the same for the same query" $
sample' rnd (run roSameTest) `shouldBe` Just True
sample' rnd (run secparam roSameTest) `shouldBe` Just True
it "is random with different queries" $
sample' rnd (run roAllEqual) `shouldBe` Just False
sample' rnd (run secparam roAllEqual) `shouldBe` Just False

+ 2
- 2
yggdrasil.cabal View File

@@ -27,14 +27,14 @@ library
, transformers >= 0.5 && < 0.6
hs-source-dirs: src
default-language: Haskell2010
ghc-options: -Wall -Werror
ghc-options: -Wall -Wcompat -Wincomplete-record-updates -Wincomplete-uni-patterns -Wredundant-constraints -Werror

test-suite spec
type: exitcode-stdio-1.0
other-extensions: ScopedTypeVariables
default-language: Haskell2010
hs-source-dirs: tests
ghc-options: -Wall -Werror
ghc-options: -Wall -Wcompat -Wincomplete-record-updates -Wincomplete-uni-patterns -Wredundant-constraints -Werror
main-is: Spec.hs
other-modules: ExecTests
FunctTests

Loading…
Cancel
Save