diff --git a/MultiChor.cabal b/MultiChor.cabal --- a/MultiChor.cabal +++ b/MultiChor.cabal @@ -1,6 +1,6 @@ cabal-version: 3.0 name: MultiChor -version: 1.0.1.1 +version: 1.1.0.0 license-files: , LICENSE , LICENSE.inherited @@ -67,172 +67,3 @@ Choreography.Polymorphism Control.Monad.Freer -common lib-dependent - import: basic-config - build-depends: MultiChor - -Flag test - Description: Enable debug support - Default: False - Manual: True - -common example - import: lib-dependent - if flag(test) - buildable: True - hs-source-dirs: examples - build-depends: - , async >= 2.2 && < 2.3 - , binary >= 0.8.9.0 && < 0.10.1.0 - -- trying to get hls to work with TestSuite - , Cabal >= 3.6.3 && < 3.13 - --, cabal-detailed-quickcheck >= 0.2.0 && < 0.3 - -- - , containers >= 0.6 && < 0.7 - , cryptonite >= 0.10 && < 0.31 - , finite-field >= 0.10.0 && < 0.11.0 - , split >= 0.2 && < 0.3 - , random >= 1.2 && < 1.3 - , time >= 1.11 && < 1.15 - , transformers >= 0.5 && < 0.7 - , QuickCheck >= 2.14 && < 3 - other-modules: Distribution.TestSuite.QuickCheck - , CLI - else - buildable: False - -Test-Suite testExamples - import: example - type: detailed-0.9 - test-module: Tests - other-modules: Data - , Bank2PC - , Bookseller0Network - , Bookseller1Simple - , Bookseller2HigherOrder - , Bookseller3LocPoly - , BooksellerFancy - , CardGame - , ChooseTeams - , DelegationFig20 - , DiffieHellman - , GMWReal - , Karatsuba - , KVS1Simple - , KVS2PrimaryBackup - , KVS3HigherOrder - , KVS4LocPoly - , KVS5Fig17 - , KVS6SizePoly - , KVS7SimplePoly - , Lottery - , MergeSort - , MPCFake - , ObliviousTransfer - , QuickSort - , RingLeader - ---executable bank-2pc --- import: example --- main-is: Bank2PC.hs --- ghc-options: --- -main-is Bank2PC --- ---executable lottery --- import: example --- main-is: Lottery.hs --- ghc-options: --- -main-is Lottery --- --- ---executable bookseller-0-network --- import: example --- main-is: Bookseller0Network.hs --- ghc-options: --- -main-is Bookseller0Network --- ---executable bookseller-1-simple --- import: example --- main-is: Bookseller1Simple.hs --- ghc-options: --- -main-is Bookseller1Simple --- ---executable bookseller-2-higher-order --- import: example --- main-is: Bookseller2HigherOrder.hs --- ghc-options: --- -main-is Bookseller2HigherOrder --- ---executable bookseller-3-loc-poly --- import: example --- main-is: Bookseller3LocPoly.hs --- ghc-options: --- -main-is Bookseller3LocPoly --- ---executable diffiehellman --- import: example --- main-is: DiffieHellman.hs --- ghc-options: --- -main-is DiffieHellman --- ---executable gmw-real --- import: example --- main-is: GMWReal.hs --- ghc-options: --- -main-is GMWReal --- other-modules: --- ObliviousTransfer --- ---executable karatsuba --- import: example --- main-is: Karatsuba.hs --- ghc-options: --- -main-is Karatsuba --- ---executable kvs1 --- import: example --- main-is: KVS1Simple.hs --- ghc-options: --- -main-is KVS1Simple --- ---executable kvs2 --- import: example --- main-is: KVS2PrimaryBackup.hs --- ghc-options: --- -main-is KVS2PrimaryBackup --- ---executable kvs3 --- import: example --- main-is: KVS3HigherOrder.hs --- ghc-options: --- -main-is KVS3HigherOrder --- ---executable kvs4 --- import: example --- main-is: KVS4LocPoly.hs --- ghc-options: --- -main-is KVS4LocPoly --- ---executable mergesort --- import: example --- main-is: MergeSort.hs --- ghc-options: --- -main-is MergeSort --- ---executable oblivious-transfer --- import: example --- main-is: ObliviousTransfer.hs --- ghc-options: --- -main-is ObliviousTransfer --- ---executable quicksort --- import: example --- main-is: QuickSort.hs --- ghc-options: --- -main-is QuickSort --- ---executable ring-leader --- import: example --- main-is: RingLeader.hs --- ghc-options: --- -main-is RingLeader diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -17,7 +17,7 @@ - `a` is the returned value, typically this will be a `Located` or `Faceted` value as described below. - MultiChor is an _embedded_ DSL, as interoperable with the rest of the Haskell ecosystem as any other monad. In particular, MultiChor gets recursion, polymorphism, and location-polymorphism "for free" as features of Haskell! -- MultiChor uses enclaves, and multiply-located values to achieve excellent expressivity and efficient Knowledge of Choice management. +- MultiChor uses conclaves, and multiply-located values to achieve excellent expressivity and efficient Knowledge of Choice management. - A value of type `Located ls a` is a single `a` known to all the parties listed in `ls`. In a well-typed choreography, other parties, who may not know the `a`, will never attempt to use it. - In the expression `(s, v) ~> rs`, a sender `s` sends the value `v` to _all_ of the recipients in `rs`, resulting in a `Located rs v`. @@ -60,7 +60,7 @@ putNote $ "All cards on the table: " ++ show hand1 getInput "I'll ask for another? [True/False]" hand2 <- fanOut \(player :: Member player players) -> - enclave (inSuper players player @@ dealer @@ nobody) do + conclave (inSuper players player @@ dealer @@ nobody) do let dealer' = listedSecond @"dealer" choice <- broadcast (listedFirst @player, localize player wantsNextCard) if choice @@ -91,8 +91,8 @@ `wantsNextCard` is the result of a parallel computation (CLI interaction); it's type is `Faceted players '[] Bool`. The computation of `hand2` is private between each player and the dealer, so we `fanOut` over the players -and then `enclave` a sub-choreography involving only the given player and `"dealer"`. -The `broadcast` inside the enclave shares that player's value of `wantsNextCard` with everyone _who's present_, which is just `"dealer"`. +and then `conclave` a sub-choreography involving only the given player and `"dealer"`. +The `broadcast` inside the conclave shares that player's value of `wantsNextCard` with everyone _who's present_, which is just `"dealer"`. At the end, the players each observer if they've won or lost in parallel. Check the source repository for many more example choreographies. diff --git a/examples/Bank2PC.hs b/examples/Bank2PC.hs deleted file mode 100644 --- a/examples/Bank2PC.hs +++ /dev/null @@ -1,178 +0,0 @@ -{-# LANGUAGE BlockArguments #-} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TemplateHaskell #-} - -{- -# Example: bank-2pc - -## Overview - -This example implements the two-phase commit protocol. - -This system models a bank. Alice and Bob each have their accounts on the bank, and the balance of each account is stored at separate locations `alice` and `bob`. This bank has a policy that does not allow balances to be negative. - -As a bank administrator, you can change the balance of accounts. An `Action` changes a single account's balance by specifying the account (`String`, "alice" or "bob") and the amount to add to the account (Int, can be negative to indicate withdrawal). A `Transaction` is a list of `Action`s. - -When executing a `Transaction`, the system will perform Alice's actions at `alice` and Bob's actions at `bob`. However, the transaction aborts if one of the actions violates the bank policy and makes the balance negative. We use the two-phase commit protocol to ensure consistency between `alice` and `bob`. - -In the voting phase, `alice` and `bob` check if the given transaction violates the policy. If one or more locations determine that the transaction violates the policy, the entire transaction aborts. If the transaction is valid, each location will commit the transaction. - -## Execution - -For simplicity, this example uses `runChoreo` and executes the choreography directly. On the terminal, you can write transactions as follows. Both accounts' balances are initialized to 0. - -```text -> cabal run bank-2pc -Command? (alice|bob {amount};)+ -alice 10; bob 10 # deposit 10 each to Alice and Bob's accounts -Committed -Alice's balance: 10 -Bob's balance: 10 -Command? (alice|bob {amount};)+ # deposit 20 to Alice's and withdraw 10 from Bob's -alice 20; bob -5 -Committed -Alice's balance: 30 -Bob's balance: 5 -Command? (alice|bob {amount};)+ # move 10 from Bob to Alice (Invalid, Bob's account will be negative) -alice 10; bob -10 -Not committed -Alice's balance: 30 -Bob's balance: 5 -``` --} - -module Bank2PC where - -import CLI -import Choreography -import Control.Monad (unless) -import Data (TestArgs, reference) -import Data.List (intercalate, transpose) -import Data.List.Split (splitOn) -import Data.Maybe (mapMaybe) -import Data.Proxy (Proxy (Proxy)) -import GHC.TypeLits (KnownSymbol, symbolVal) -import Test.QuickCheck (Arbitrary, arbitrary, elements, listOf, listOf1) -import Text.Read (readMaybe) - -$(mkLoc "client") -$(mkLoc "coordinator") -$(mkLoc "alice") -$(mkLoc "bob") - -type Participants = ["client", "coordinator", "alice", "bob"] - -type State = (Located '["alice"] Int, Located '["bob"] Int) - -type Action = (String, Int) - -type Transaction = [Action] - -newtype Args p q = Args [Transaction] deriving (Eq, Show, Read) - -instance (KnownSymbol p, KnownSymbol q) => TestArgs (Args p q) [[String]] where - reference (Args tx) = addCoordinator . transpose $ showAll <$> ref start tx - where - start = (,0) <$> [symbolVal (Proxy @p), symbolVal (Proxy @q)] - ref _ [] = [] - ref state (t : ts) = - let (s', r) = refAs state t - s'' = if r then s' else state - in (r, s'') : ref s'' ts - refAs state [] = (state, True) - refAs state (a : as) = - let (s', r) = refA state a - in if r then refAs s' as else (state, False) - refA state (name, amount) = - let (otherL, (_, s) : otherR) = ((== name) . fst) `break` state - s' = s + amount - in (otherL ++ ((name, s') : otherR), 0 <= s') - showAll :: (Bool, [(String, Int)]) -> [String] - showAll (clnt, servers) = show clnt : (show . snd <$> servers) - addCoordinator (clnt : servers) = clnt : [] : servers - addCoordinator _ = error "this can't happen, right? I could enforce it by types, but it's a core..." - -instance (KnownSymbol p, KnownSymbol q) => Arbitrary (Args p q) where - arbitrary = (Args . (++ [[]]) <$>) . listOf . listOf1 $ (,) <$> elements [symbolVal $ Proxy @p, symbolVal $ Proxy @q] <*> arbitrary - --- | `validate` checks if a transaction can be executed while keeping balance >= 0 --- returns if the transaction satisfies the property and the balance after the transaction -validate :: String -> Int -> Transaction -> (Bool, Int) -validate name balance tx = foldl (\(valid, i) (_, amount) -> (let next = i + amount in (valid && next >= 0, next))) (True, balance) actions - where - actions = filter (\(n, _) -> n == name) tx - -render :: Transaction -> String -render txns = intercalate ";" $ (\(a, b) -> a ++ " " ++ show b) <$> txns - --- | `parse` converts the user input into a transaction -parse :: String -> Transaction -parse s = tx - where - t = splitOn ";" s - f :: String -> Maybe Action - f l = do - [target, amountStr] <- return $ words l - amount <- readMaybe amountStr :: Maybe Int - target' <- if target == "alice" || target == "bob" then Just target else Nothing - return (target', amount) - tx = mapMaybe f t - --- | `handleTransaction` is a choreography that handles a transaction. --- Given the current state and a transaction, it will first ask alice and bob to vote, --- then it will decide whether to commit the transaction or not. --- If the transaction is committed, it will update the state. --- Otherwise, it will keep the state unchanged. -handleTransaction :: - (Monad m) => - State -> - Located '["coordinator"] Transaction -> - Choreo Participants m (Located '["coordinator"] Bool, State) -handleTransaction (aliceBalance, bobBalance) tx = do - -- Voting Phase - txa <- (coordinator, tx) ~> alice @@ nobody - voteAlice <- (alice, \un -> do { return $ fst $ validate "alice" (un alice aliceBalance) (un alice txa) }) ~~> coordinator @@ nobody - txb <- (coordinator, tx) ~> bob @@ nobody - voteBob <- (bob, \un -> do { return $ fst $ validate "bob" (un bob bobBalance) (un bob txb) }) ~~> coordinator @@ nobody - - -- Check if the transaction can be committed - canCommit <- coordinator `locally` \un -> do return $ un coordinator voteAlice && un coordinator voteBob - - -- Commit Phase - broadcast (coordinator, canCommit) >>= \case - True -> do - aliceBalance' <- alice `locally` \un -> do return $ snd $ validate "alice" (un alice aliceBalance) (un alice txa) - bobBalance' <- bob `locally` \un -> do return $ snd $ validate "bob" (un bob bobBalance) (un bob txb) - return (canCommit, (aliceBalance', bobBalance')) - False -> do - return (canCommit, (aliceBalance, bobBalance)) - --- | `bank` loops forever and handles transactions. -bank :: State -> Choreo Participants (CLI m) () -bank state = do - tx <- - ( client, - parse <$> getstr "Command? (alice|bob {amount};)+" - ) - -~> coordinator - @@ nobody - (committed, state') <- handleTransaction state tx - committed' <- (coordinator, committed) ~> client @@ nobody - client `locally_` \un -> putOutput "Committed?" (un client committed') - alice `locally_` \un -> putOutput "Alice's balance:" (un alice (fst state')) - bob `locally_` \un -> putOutput "Bob's balance:" (un bob (snd state')) - c <- coordinator `locally` (\un -> return $ null $ un coordinator tx) - broadcast (coordinator, c) >>= (`unless` bank state') -- repeat - --- | `startBank` is a choreography that initializes the states and starts the bank application. -startBank :: Choreo Participants (CLI m) () -startBank = do - aliceBalance <- alice `_locally` return 0 - bobBalance <- bob `_locally` return 0 - bank (aliceBalance, bobBalance) - -main :: IO () -main = do - runCLIIO $ runChoreo startBank diff --git a/examples/Bookseller0Network.hs b/examples/Bookseller0Network.hs deleted file mode 100644 --- a/examples/Bookseller0Network.hs +++ /dev/null @@ -1,63 +0,0 @@ -module Bookseller0Network where - -{- -# Bookseller as individual network programs - -This example implmenets the bookseller protocol as individual network -programs (non-choreographic way). See -[`bookseller-1-simple`](../bookseller-1-simple) for a description of -the protocol. - -## Running the example - -Same as [`bookseller-1-simple`](../bookseller-1-simple) but with `cabal run bookseller-0-network`. --} - -import CLI -import Choreography.Network -import Choreography.Network.Http -import Data (deliveryDateOf, priceOf) -import Data.Time -import System.Environment - -buyer :: Network (CLI m) () -buyer = do - budget <- run $ getInput @Int "Enter your total budget:" - title <- run $ getstr "Enter the title of the book to buy:" - send title ["seller"] - price <- recv "seller" - if price <= budget - then do - send True ["seller"] - (deliveryDate :: Day) <- recv "seller" - run $ putOutput "The book will be delivered on:" deliveryDate - else do - send False ["seller"] - run $ putNote "The book's price is out of the budget" - -seller :: Network (CLI m) () -seller = do - database <- run $ getInput "Enter the book database (for `Read`):" - title <- recv "buyer" - send (database `priceOf` title) ["buyer"] - decision <- recv "buyer" - if decision - then do - send (database `deliveryDateOf` title) ["buyer"] - else do - return () - -main :: IO () -main = do - [loc] <- getArgs - case loc of - "buyer" -> runCLIIO $ runNetwork cfg "buyer" buyer - "seller" -> runCLIIO $ runNetwork cfg "seller" seller - _ -> error "unknown party" - return () - where - cfg = - mkHttpConfig - [ ("buyer", ("localhost", 4242)), - ("seller", ("localhost", 4343)) - ] diff --git a/examples/Bookseller1Simple.hs b/examples/Bookseller1Simple.hs deleted file mode 100644 --- a/examples/Bookseller1Simple.hs +++ /dev/null @@ -1,68 +0,0 @@ -{-# LANGUAGE BlockArguments #-} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE TemplateHaskell #-} - -module Bookseller1Simple where - -import CLI -import Choreography -import Choreography.Network.Http -import Data (deliveryDateOf, priceOf) -import System.Environment - -$(mkLoc "buyer") -$(mkLoc "seller") - -type Participants = ["buyer", "seller"] - --- | `bookseller` is a choreography that implements the bookseller protocol. -bookseller :: Choreo Participants (CLI m) () -bookseller = do - database <- seller `_locally` getInput "Enter the book database (for `Read`):" - buyer_budget <- buyer `_locally` getInput "Enter your total budget:" - title <- buyer `_locally` getstr "Enter the title of the book to buy:" - - title' <- (buyer, title) ~> seller @@ nobody - price <- seller `locally` \un -> return $ priceOf (un seller database) (un seller title') - price' <- (seller, price) ~> buyer @@ nobody - decision <- buyer `locally` \un -> return $ un buyer price' <= un buyer buyer_budget - - broadcast (buyer, decision) >>= \case - True -> do - deliveryDate <- seller `locally` \un -> return $ deliveryDateOf (un seller database) (un seller title') - deliveryDate' <- (seller, deliveryDate) ~> buyer @@ nobody - buyer `locally_` \un -> putOutput "The book will be delivered on:" $ un buyer deliveryDate' - False -> do - buyer `_locally_` putNote "The book's price is out of the budget" - --- `bookseller'` is a simplified version of `bookseller` that utilizes `~~>` -bookseller' :: Choreo Participants (CLI m) () -bookseller' = do - database <- seller `_locally` getInput "Enter the book database (for `Read`):" - buyer_budget <- buyer `_locally` getInput "Enter your total budget:" - title <- (buyer, getstr "Enter the title of the book to buy:") -~> seller @@ nobody - price <- (seller, \un -> return $ priceOf (un seller database) (un seller title)) ~~> buyer @@ nobody - - inBuyerBudget <- buyer `locally` (\un -> return $ un buyer price <= un buyer buyer_budget) - broadcast (buyer, inBuyerBudget) >>= \case - True -> do - deliveryDate <- (seller, \un -> return $ deliveryDateOf (un seller database) (un seller title)) ~~> buyer @@ nobody - buyer `locally_` \un -> putOutput "The book will be delivered on:" $ un buyer deliveryDate - False -> do - buyer `_locally_` putNote "The book's price is out of the budget" - -main :: IO () -main = do - [loc] <- getArgs - delivery <- case loc of - "buyer" -> runCLIIO $ runChoreography cfg bookseller' "buyer" - "seller" -> runCLIIO $ runChoreography cfg bookseller' "seller" - _ -> error "unknown party" - print delivery - where - cfg = - mkHttpConfig - [ ("buyer", ("localhost", 4242)), - ("seller", ("localhost", 4343)) - ] diff --git a/examples/Bookseller2HigherOrder.hs b/examples/Bookseller2HigherOrder.hs deleted file mode 100644 --- a/examples/Bookseller2HigherOrder.hs +++ /dev/null @@ -1,122 +0,0 @@ -{-# LANGUAGE BlockArguments #-} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE TemplateHaskell #-} - -{- -# Higher-order bookseller - -This example implements the higher-order bookseller protocol where -how the buyer decides whether to buy the book is abstracted as an -argument, making it a higher-order choreography. -For a general description of the protocol, see [`bookseller-1-simple`](../bookseller-1-simple). - -We provide two decision-making functions: - -- `mkDecision1` only checks if buyer's budget is greater than the - book's price, which has the same behavior as [`bookseller-1-simple`](../bookseller-1-simple) -- `mkDecision2` asks buyer2 how much they're willing to contribute and - checks if the buyer's budget is greater than the book's price minus - buyer2's contribution. - -By default, this example uses `mkDecision2`. To use `mkDecision1`, -change the line `choreo = bookseller mkDecisiont2` to `choreo = bookseller mkDecision1`. - -## Running the protocol - -```bash -# in shell 1 -cabal run bookseller-2-higher-order buyer - -# in shell 2 -cabal run bookseller-2-higher-order buyer2 - -# in shell 3 -cabal run bookseller-2-higher-order seller - -# in shell 1 -> Enter the title of the book to buy -Homotopy Type Theory - -# in shell 2 -> How much you're willing to contribute? -100 - -# in shell 1 -The book will be delivered on 2023-01-01 -``` - -Note previously in [`bookseller-1-simple`](../bookseller-1-simple), -the buyer can't buy `Homotopy Type Theory` as it's out of the budget, -but with buyer2's contribution, now it can. --} - -module Bookseller2HigherOrder where - -import CLI -import Choreography -import Choreography.Network.Http -import Data (deliveryDateOf, priceOf) -import System.Environment - -$(mkLoc "buyer") -$(mkLoc "seller") -$(mkLoc "buyer2") - -type Participants = ["buyer", "seller", "buyer2"] - --- | `bookseller` is a choreography that implements the bookseller protocol. --- This version takes a choreography `mkDecision` that implements the decision making process. -bookseller :: - (Located '["buyer"] Int -> Choreo Participants (CLI m) (Located '["buyer"] Bool)) -> - Choreo Participants (CLI m) () -bookseller mkDecision = do - database <- seller `_locally` getInput "Enter the book database (for `Read`):" - title <- (buyer, getstr "Enter the title of the book to buy:") -~> seller @@ nobody - - -- the seller checks the price of the book and sends it to the buyer - price <- (seller, \un -> return $ priceOf (un seller database) (un seller title)) ~~> buyer @@ nobody - - -- the buyer makes a decision using the `mkDecision` choreography - decision <- mkDecision price - - -- if the buyer decides to buy the book, the seller sends the delivery date to the buyer - broadcast (buyer, decision) >>= \case - True -> do - deliveryDate <- (seller, \un -> return $ deliveryDateOf (un seller database) (un seller title)) ~~> buyer @@ nobody - buyer `locally_` \un -> putstr "The book will be delivered on:" $ show (un buyer deliveryDate) - False -> do - buyer `_locally_` putNote "The book's price is out of the budget" - --- | `mkDecision1` checks if buyer's budget is greater than the price of the book -mkDecision1 :: Located '["buyer"] Int -> Choreo Participants (CLI m) (Located '["buyer"] Bool) -mkDecision1 price = do - budget <- buyer `_locally` getInput "What are you willing to pay?" - buyer `locally` \un -> return $ un buyer price <= un buyer budget - --- | `mkDecision2` asks buyer2 how much they're willing to contribute and checks --- if the buyer's budget is greater than the price of the book minus buyer2's contribution -mkDecision2 :: Located '["buyer"] Int -> Choreo Participants (CLI m) (Located '["buyer"] Bool) -mkDecision2 price = do - contrib1 <- buyer `_locally` getInput "What are you willing to pay?" - contrib2 <- (buyer2, getInput "How much you're willing to contribute?") -~> buyer @@ nobody - buyer `locally` \un -> return $ un buyer price - un buyer contrib2 <= un buyer contrib1 - -main :: IO () -main = do - [loc] <- getArgs - _ <- case loc of - "buyer" -> runCLIIO $ runChoreography cfg choreo "buyer" - "seller" -> runCLIIO $ runChoreography cfg choreo "seller" - "buyer2" -> runCLIIO $ runChoreography cfg choreo "buyer2" - _ -> error "unknown party" - return () - where - choreo = bookseller mkDecision2 - - cfg = - mkHttpConfig - [ ("buyer", ("localhost", 4242)), - ("seller", ("localhost", 4343)), - ("buyer2", ("localhost", 4444)) - ] diff --git a/examples/Bookseller3LocPoly.hs b/examples/Bookseller3LocPoly.hs deleted file mode 100644 --- a/examples/Bookseller3LocPoly.hs +++ /dev/null @@ -1,69 +0,0 @@ -{-# LANGUAGE BlockArguments #-} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE TemplateHaskell #-} - -{- -# Location-polymorphic bookseller - -This example implements the location-polymorphic bookseller where the -buyer's location is abstracted away as an argument. - -For a general description of the protocol, see [`bookseller-1-simple`](../bookseller-1-simple). - -# Running the protocol - -Same as [`bookseller-1-simple`](../bookseller-1-simple) but with `cabal run bookseller-3-loc-poly`. --} - -module Bookseller3LocPoly where - -import CLI -import Choreography -import Choreography.Network.Http -import Data (deliveryDateOf, priceOf) -import GHC.TypeLits -import System.Environment - -$(mkLoc "buyer") -$(mkLoc "seller") - --- type Participants = ["buyer", "seller"] - --- | `bookseller` is a choreography that implements the bookseller protocol. --- This version takes the name of the buyer as a parameter (`someBuyer`). -bookseller :: (KnownSymbol a, KnownSymbols ps) => Member a ps -> Choreo ("seller" ': ps) (CLI m) () -bookseller someBuyer = do - let theBuyer = inSuper consSet someBuyer - database <- seller `_locally` getInput "Enter the book database (for `Read`):" - buyer_budget <- theBuyer `_locally` getInput "Enter your total budget:" - -- the buyer reads the title of the book and sends it to the seller - title <- (theBuyer, getstr "Enter the title of the book to buy") -~> seller @@ nobody - -- the seller checks the price of the book and sends it to the buyer - price <- (seller, \un -> return $ priceOf (un seller database) (un seller title)) ~~> theBuyer @@ nobody - - inBuyerBudget <- theBuyer `locally` (\un -> return $ un singleton price <= un singleton buyer_budget) - broadcast (theBuyer, inBuyerBudget) >>= \case - True -> do - deliveryDate <- (seller, \un -> return $ deliveryDateOf (un seller database) (un seller title)) ~~> theBuyer @@ nobody - - theBuyer `locally_` \un -> putOutput "The book will be delivered on:" $ un singleton deliveryDate - False -> do - theBuyer `_locally_` putNote "The book's price is out of the budget" - -main :: IO () -main = do - [loc] <- getArgs - _ <- case loc of - "buyer" -> runCLIIO $ runChoreography cfg choreo "buyer" - "seller" -> runCLIIO $ runChoreography cfg choreo "seller" - _ -> error "unknown party" - return () - where - choreo = bookseller $ singleton @"buyer" - - cfg = - mkHttpConfig - [ ("buyer", ("localhost", 4242)), - ("seller", ("localhost", 4343)) - ] diff --git a/examples/BooksellerFancy.hs b/examples/BooksellerFancy.hs deleted file mode 100644 --- a/examples/BooksellerFancy.hs +++ /dev/null @@ -1,94 +0,0 @@ -{-# LANGUAGE BlockArguments #-} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE TemplateHaskell #-} - -{- -# Maximally fancy bookseller --} - -module BooksellerFancy where - -import CLI -import Choreography -import Choreography.Network.Http -import Data (deliveryDateOf, priceOf) -import System.Environment - -$(mkLoc "buyer") -$(mkLoc "seller") - --- | `bookseller` is a choreography that implements the bookseller protocol. --- This version takes a choreography `mkDecision` that implements the decision making process. -bookseller :: - forall supporters {m}. - (KnownSymbols supporters) => - (Located '["buyer"] Int -> Choreo ("buyer" ': supporters) (CLI m) (Located '["buyer"] Bool)) -> - Choreo ("buyer" ': "seller" ': supporters) (CLI m) () -bookseller mkDecision = do - database <- seller `_locally` getInput "Enter the book database (for `Read`):" - title <- (buyer, getstr "Enter the title of the book to buy:") -~> seller @@ nobody - - -- the seller checks the price of the book and sends it to the buyer - price <- (seller, \un -> return $ priceOf (un seller database) (un seller title)) ~~> buyer @@ nobody - - -- the buyer and supporters (transactors) make a decision using the `mkDecision` choreography - decision <- enclave transactors $ mkDecision price - - -- if the buyer decides to buy the book, the seller sends the delivery date to the buyer - _ <- - enclave buyerAndSeller $ - broadcast (buyer, flatten explicitSubset allOf decision) >>= \case - True -> do - deliveryDate <- (seller, \un -> return $ deliveryDateOf (un seller database) (un seller title)) ~~> buyer @@ nobody - buyer `locally_` \un -> putstr "The book will be delivered on:" $ show (un buyer deliveryDate) - False -> do - buyer `_locally_` putNote "The book's price is out of the budget" - - return () - where - transactors :: Subset ("buyer" ': supporters) ("buyer" ': "seller" ': supporters) - transactors = explicitMember @@ (consSuper . consSuper $ refl) - - buyerAndSeller :: Subset '["buyer", "seller"] ("buyer" ': "seller" ': supporters) - buyerAndSeller = explicitSubset - --- | `mkDecision1` checks if buyer's budget is greater than the price of the book -mkDecision1 :: Located '["buyer"] Int -> Choreo ("buyer" ': supporters) (CLI m) (Located '["buyer"] Bool) -mkDecision1 price = do - budget <- buyer `_locally` getInput "What are you willing to pay?" - buyer `locally` \un -> return $ un buyer price <= un buyer budget - --- | `mkDecision2` asks supporters how much they're willing to contribute and checks --- if the buyer's budget is greater than the price of the book minus all supporters' contribution -mkDecision2 :: forall supporters {m}. (KnownSymbols supporters) => Located '["buyer"] Int -> Choreo ("buyer" ': supporters) (CLI m) (Located '["buyer"] Bool) -mkDecision2 price = do - budget <- buyer `_locally` getInput "What are you willing to pay?" - - contribs <- fanIn @supporters explicitSubset $ \supporter -> - (Later supporter, getInput "How much you're willing to contribute?") -~> buyer @@ nobody - contrib <- - buyer `locally` \un -> - return $ sum (un buyer contribs) - buyer `locally` \un -> return $ un buyer price <= un buyer budget + un buyer contrib - -main :: IO () -main = do - [loc] <- getArgs - _ <- case loc of - "buyer" -> runCLIIO $ runChoreography cfg choreo "buyer" - "seller" -> runCLIIO $ runChoreography cfg choreo "seller" - "buyer2" -> runCLIIO $ runChoreography cfg choreo "buyer2" - "buyer3" -> runCLIIO $ runChoreography cfg choreo "buyer3" - _ -> error "unknown party" - return () - where - choreo = bookseller @["buyer2", "buyer3"] mkDecision2 - - cfg = - mkHttpConfig - [ ("buyer", ("localhost", 4242)), - ("seller", ("localhost", 4343)), - ("buyer2", ("localhost", 4444)), - ("buyer3", ("localhost", 45454)) - ] diff --git a/examples/CLI.hs b/examples/CLI.hs deleted file mode 100644 --- a/examples/CLI.hs +++ /dev/null @@ -1,80 +0,0 @@ -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE ImpredicativeTypes #-} - --- | This module defines `Choreo`, the monad for writing choreographies. -module CLI where - -import Control.Monad (unless) -import Control.Monad.Freer -import Control.Monad.IO.Class (MonadIO (liftIO)) -import Control.Monad.State (MonadState (get, put), StateT (runStateT), lift) -import Data.Typeable (Typeable, typeRep) -import Text.Read (readMaybe) - -type Context = String - -data CLISig m a where - GetStr :: Context -> CLISig m String - PutStr :: Context -> String -> CLISig m () - Internal :: m a -> CLISig m a - -type CLI m = Freer (CLISig m) - -instance (MonadIO m) => MonadIO (CLI m) where - liftIO a = toFreer $ Internal $ liftIO a - -runCLIIO :: forall m a. (MonadIO m) => CLI m a -> m a -runCLIIO = interpFreer handler - where - handler :: CLISig m b -> m b - handler (GetStr prompt) = liftIO $ putStrLn prompt >> getLine - handler (PutStr context l) = liftIO $ putStrLn $ context ++ " " ++ l - handler (Internal m) = m - -getstr :: Context -> CLI m String -getstr context = toFreer $ GetStr context - -getln :: CLI m String -getln = getstr "" - -getInput :: forall a m. (Read a, Typeable a) => Context -> CLI m a -getInput context = do - str <- getstr context - case readMaybe str of - Just a -> return a - a@Nothing -> error $ "Failed to read \"" ++ str ++ "\" as a " ++ show (typeRep a) - -putstr :: Context -> String -> CLI m () -putstr context l = toFreer $ PutStr context l - -putNote :: Context -> CLI m () -putNote = (`putstr` "") - -putOutput :: (Show a) => Context -> a -> CLI m () -putOutput context a = putstr context $ show a - -data TTYEnv = TTYEnv - { inputs :: [String], - outputs :: [String] - } - -runCLIStateful :: forall m a. (MonadFail m, MonadIO m) => [String] -> CLI m a -> m ([String], a) -runCLIStateful ins tma = do - (a, e) <- runStateT stateful TTYEnv {inputs = ins, outputs = []} - return (reverse $ outputs e, a) - where - stateful :: StateT TTYEnv m a - stateful = interpFreer handler tma - handler :: forall b. CLISig m b -> StateT TTYEnv m b - handler (GetStr c) = do - env@TTYEnv {inputs} <- get - case inputs of - ln : lns -> do - put env {inputs = lns} - return ln - [] -> error $ "No input to go with prompt " ++ show c ++ "." - handler (PutStr _ o) = unless (null o) $ do - env@TTYEnv {outputs = os} <- get - put env {outputs = o : os} - handler (Internal m) = lift m diff --git a/examples/CardGame.hs b/examples/CardGame.hs deleted file mode 100644 --- a/examples/CardGame.hs +++ /dev/null @@ -1,85 +0,0 @@ -{-# LANGUAGE BlockArguments #-} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE ScopedTypeVariables #-} - -module CardGame where - -import CLI -import Choreography -import Control.Monad (void) -import Data (TestArgs, reference) -import Test.QuickCheck (Arbitrary, arbitrary, listOf1) - -_modulo :: Int -> Int -_modulo = (`mod` 21) - -newtype Card = Card_ Int deriving (Eq, Ord, Read, Show) - -card :: Int -> Card -card = Card_ . _modulo - -instance Num Card where - (Card_ a) + (Card_ b) = card $ a + b - (Card_ a) * (Card_ b) = card $ a * b - abs = id - signum = const 1 - fromInteger = card . fromInteger - negate (Card_ a) = card $ (-1) * a - -instance Arbitrary Card where - arbitrary = Card_ <$> arbitrary - -type Win = Bool - -data Args = Args - { deck :: [Card], - choices :: (Bool, Bool, Bool) - } - deriving (Eq, Show, Read) - -instance TestArgs Args (Bool, Bool, Bool) where - reference Args {deck, choices = (c1, c2, c3)} = - let h11 : h21 : h31 : deck1 = cycle deck -- should just use State - (h12, deck12) = if c1 then ([h11, head deck1], tail deck1) else ([h11], deck1) - (h22, deck22) = if c2 then ([h21, head deck12], tail deck12) else ([h21], deck12) - (h32, deck32) = if c3 then ([h31, head deck22], tail deck22) else ([h31], deck22) - common = head deck32 - [win1, win2, win3] = (> card 19) . sum . (common :) <$> [h12, h22, h32] - in (win1, win2, win3) - -instance Arbitrary Args where - arbitrary = Args <$> listOf1 arbitrary <*> arbitrary - -{- A simple black-jack-style game. The dealer gives everyone a card, face up. Each player may - - request a second card. Then the dealer reveals one more card that applies to everyone. Each - - player individually wins if the sum of their cards (modulo 21) is greater than 19. -} -game :: forall players m. (KnownSymbols players) => Choreo ("dealer" ': players) (CLI m) () -game = do - let players = consSuper (refl @players) - dealer = listedFirst @"dealer" -- listedFirst is just First with the type-arguments rearranged. - everyone = refl @("dealer" ': players) - hand1 <- - ( fanIn everyone \(player :: Member player players) -> do - card1 <- locally dealer (\_ -> getInput ("Enter random card for " ++ toLocTm player)) - (dealer, card1) ~> everyone - ) - >>= naked everyone - wantsNextCard <- parallel players \_ _ -> do - putNote $ "All cards on the table: " ++ show hand1 - getInput "I'll ask for another? [True/False]" - hand2 <- fanOut \(player :: Member player players) -> - enclave (inSuper players player @@ dealer @@ nobody) do - let dealer' = listedSecond @"dealer" - choice <- broadcast (listedFirst @player, localize player wantsNextCard) - if choice - then do - cd2 <- locally dealer' (\_ -> getInput (toLocTm player ++ "'s second card:")) - card2 <- broadcast (dealer', cd2) - return [getLeaf hand1 player, card2] - else return [getLeaf hand1 player] - tblCrd <- locally dealer (\_ -> getInput "Enter a single card for everyone:") - tableCard <- (dealer, tblCrd) ~> players - void $ parallel players \player un -> do - let hand = un player tableCard : viewFacet un player hand2 - putNote $ "My hand: " ++ show hand - putOutput "My win result:" $ sum hand > card 19 diff --git a/examples/ChooseTeams.hs b/examples/ChooseTeams.hs deleted file mode 100644 --- a/examples/ChooseTeams.hs +++ /dev/null @@ -1,45 +0,0 @@ -{-# LANGUAGE BlockArguments #-} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE ScopedTypeVariables #-} - -module ChooseTeams where - -import CLI -import Choreography -import Control.Monad (when) -import Data (TestArgs, reference) -import Data.Foldable (toList) -import Data.Maybe (catMaybes) -import Test.QuickCheck (Arbitrary, arbitrary) - -newtype Args = Args - { choices :: (Int, Int) - } - deriving (Eq, Show, Read) - -instance TestArgs Args ([Int], [Int], [Int], [Int], [Int]) where - reference Args {choices = (c1, c2)} = ([c1, c2], [], [c1, c2], [], [c1, c2]) - -instance Arbitrary Args where - arbitrary = Args <$> arbitrary - -chooseTeams :: [LocTm] -> ([LocTm], [LocTm]) -- Probably could find it off-the-shelf somewhere... -chooseTeams [] = ([], []) -chooseTeams (a : as) = - let (t1, t2) = chooseTeams as - in (t2, a : t1) - --- the game is just red-team sending numbers to blue team. -game :: forall players m. (KnownSymbols players) => Choreo players (CLI m) () -game = do - let players = allOf @players - let (red, blue) = chooseTeams $ toLocs players - numbers <- fanIn players \p -> - if toLocTm p `elem` red - then (p, Just <$> getInput @Int "A number to send:") -~> players - else enclave players $ return Nothing - parallel_ players \p un -> - when (toLocTm p `elem` blue) $ - putOutput "Numbers recieved:" $ - catMaybes . toList $ - un p numbers diff --git a/examples/Data.hs b/examples/Data.hs deleted file mode 100644 --- a/examples/Data.hs +++ /dev/null @@ -1,78 +0,0 @@ -{-# LANGUAGE FunctionalDependencies #-} - -module Data where - -import Data.Time (Day (ModifiedJulianDay), fromGregorian) -import Test.QuickCheck (Arbitrary, Positive (Positive), arbitrary, arbitraryPrintableChar, elements, getPositive, listOf1) - -data Book = Book - { name :: String, - price :: Int, - deliverable :: Day - } - deriving (Eq, Read, Show) - -instance Arbitrary Book where - arbitrary = - Book - <$> listOf1 arbitraryPrintableChar - <*> (getPositive <$> arbitrary) - <*> (ModifiedJulianDay . getPositive <$> arbitrary) - -type Database = [Book] - -textbooks :: Database -textbooks = - [ Book - { name = "Types and Programming Languages", - price = 80, - deliverable = fromGregorian 2023 12 19 - }, - Book - { name = "Homotopy Type Theory", - price = 120, - deliverable = fromGregorian 2023 09 18 - } - ] - -priceOf :: Database -> String -> Int -priceOf books title = price $ head $ filter ((== title) . name) books - -deliveryDateOf :: Database -> String -> Day -deliveryDateOf books title = deliverable $ head $ filter ((== title) . name) books - -data BooksellerArgs = BooksellerArgs - { books :: Database, - choice :: String, - budget :: Int - } - deriving (Read, Show) - -instance Arbitrary BooksellerArgs where - arbitrary = do - books <- listOf1 arbitrary - choice <- name <$> elements books - budget <- getPositive <$> arbitrary - return BooksellerArgs {books, choice, budget} - -class TestArgs a r | a -> r where - reference :: a -> r - -instance TestArgs BooksellerArgs (Maybe Day) where - reference (BooksellerArgs {books, choice, budget}) = - if budget < priceOf books choice - then Nothing - else Just $ deliveryDateOf books choice - -instance TestArgs (BooksellerArgs, Positive Int) (Maybe Day) where - reference (BooksellerArgs {books, choice, budget}, Positive contrib) = - if budget < (priceOf books choice - contrib) - then Nothing - else Just $ deliveryDateOf books choice - --- a scenario where there's four buyers (one primary and three supporter) -instance TestArgs (BooksellerArgs, Positive Int, Positive Int, Positive Int) (Maybe Day) where - reference (BooksellerArgs {books, choice, budget}, Positive contrib, Positive contrib2, Positive contrib3) = - if budget < (priceOf books choice - contrib - contrib2 - contrib3) - then Nothing - else Just $ deliveryDateOf books choice diff --git a/examples/DelegationFig20.hs b/examples/DelegationFig20.hs deleted file mode 100644 --- a/examples/DelegationFig20.hs +++ /dev/null @@ -1,89 +0,0 @@ -{-# LANGUAGE BlockArguments #-} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TemplateHaskell #-} - -module DelegationFig20 where - -{- -let choice : ()+()@[alice, bob] = com[alice][alice, bob] alices_choice; -let query : Query@[alice] = case[alice, bob] choice of -Inl _ => com[bob][alice] bobs_query; -Inr _ => alices_query; -let answerer : (Query@[carroll] -> Response@[carroll])@[carroll] = carrolls_func; -let response = com[carroll][bob, alice] (answerer (com[alice][carroll] query)); -case[alice, bob] choice of -Inl _ => bobs_terminal response; -Inr _ => alices_terminal response; - -} - -import CLI -import Choreography -import Data (TestArgs, reference) -import Data.List (sort) -import Data.Maybe (fromMaybe) -import Test.QuickCheck (Arbitrary, arbitrary, arbitraryPrintableChar, elements, listOf1) - -$(mkLoc "alice") -$(mkLoc "bob") -$(mkLoc "carroll") - -type Participants = ["alice", "bob", "carroll"] - -data Args = Args - { choice :: Bool, - aliceQ :: String, - bobQ :: String, - carrollF :: String - } - deriving (Eq, Show, Read) - -data Result = Result - { aliceR :: [String], - bobR :: [String], - carrollR :: [String] - } - deriving (Eq, Show, Read) - -instance TestArgs Args Result where - reference Args {choice, aliceQ, bobQ, carrollF} = - let f = fromMaybe carrollsDefault $ carrollF `lookup` carrollsFunctions - result = f $ if choice then aliceQ else bobQ - in Result {aliceR = [result | choice], bobR = [result | not choice], carrollR = []} - -instance Arbitrary Args where - arbitrary = - Args - <$> arbitrary - <*> listOf1 arbitraryPrintableChar -- Avoiding wierd behavior of CLI on empty outputs :( - <*> listOf1 arbitraryPrintableChar - <*> elements (fst <$> carrollsFunctions) - -carrollsFunctions :: [(String, String -> String)] -carrollsFunctions = - [ ("reverse", reverse), - ("alphabetize", sort) - ] - -carrollsDefault :: String -> String -carrollsDefault = const "No Handler" - -mainCho :: Choreo Participants (CLI m) () -mainCho = do - choice <- (alice, getInput "Alice's choice:") -~> alice @@ bob @@ nobody - query <- - flatten (alice @@ nobody) (alice @@ nobody) - <$> cond (explicitSubset, (refl, choice)) \case - False -> (bob, getstr "Bob's query:") -~> alice @@ nobody - True -> alice `_locally` getstr "Alice's query:" - answerer <- - carroll `_locally` do - handlerName <- getstr "Carrol's function (reverse or alphabetize):" - return $ fromMaybe carrollsDefault $ handlerName `lookup` carrollsFunctions - query' <- (alice, query) ~> carroll @@ nobody - response <- (carroll, \un -> return $ un carroll answerer (un carroll query')) ~~> alice @@ bob @@ nobody - (_ :: Located '["alice", "bob"] ()) <- cond (explicitSubset, (refl, choice)) \case - False -> bob `locally_` \un -> putstr "Recieved:" (un bob response) - True -> alice `locally_` \un -> putstr "Recieved:" (un alice response) - return () diff --git a/examples/DiffieHellman.hs b/examples/DiffieHellman.hs deleted file mode 100644 --- a/examples/DiffieHellman.hs +++ /dev/null @@ -1,113 +0,0 @@ -{-# LANGUAGE BlockArguments #-} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE TemplateHaskell #-} - -{- -# Example: diffie-hellman key exchange - -## Overview - -This example implements the [diffie-hellman key exchange protocol](https://en.wikipedia.org/wiki/Diffie%E2%80%93Hellman_key_exchange). - -In this example, two locations, `alice` and `bob`, exchange the secret key without sending the key over the network. - -## Execution - -To run this example, you will need to run two locations (alice and bob) at the same time. Alice initiates the exchange, and Bob waits for Alice. When both locations are ready, press "enter" on Alice's terminal to start the protocol. - -``` -> cabal run diffiehellman bob -waiting for alice to initiate key exchange - -# on a different terminal -> cabal run diffiehellman alice -enter to start key exchange... -[Enter] - -# Alice's terminal -alice's shared key: 1544 - -# Bob's terminal -bob's shared key: 1544 -``` - -This sample uses [`System.Random`](https://hackage.haskell.org/package/random-1.2.1.1/docs/System-Random.html) and will generate different keys at each invocation. --} - -module DiffieHellman where - -import CLI -import Choreography -import Choreography.Network.Http -import Control.Monad.IO.Class (MonadIO) -import System.Environment -import System.Random - --- helper functions around prime number --- https://nulldereference.wordpress.com/2012/02/04/generating-prime-numbers-with-haskell/ -divisors :: Integer -> [Integer] -divisors 1 = [1] -divisors x = 1 : [y | y <- [2 .. (x `div` 2)], x `mod` y == 0] ++ [x] - -isPrime :: Integer -> Bool -isPrime x = divisors x == [1, x] - -primeNums :: [Integer] -primeNums = [x | x <- [2 ..], isPrime x] - -$(mkLoc "alice") -$(mkLoc "bob") - -type Participants = ["alice", "bob"] - -diffieHellman :: - (MonadIO m) => - Choreo Participants (CLI m) () -diffieHellman = do - -- wait for alice to initiate the process - _ <- alice `_locally` getstr "enter to start key exchange..." - bob `_locally_` putNote "waiting for alice to initiate key exchange" - - -- alice picks p and g and sends them to bob - pa <- - alice `_locally` do - x <- randomRIO (200, 1000 :: Int) - return $ primeNums !! x - pb <- (alice, pa) ~> bob @@ nobody - ga <- alice `locally` \un -> do randomRIO (10, un alice pa) - gb <- (alice, ga) ~> bob @@ nobody - - -- alice and bob select secrets - a <- alice `_locally` randomRIO (200, 1000 :: Integer) - b <- bob `_locally` randomRIO (200, 1000 :: Integer) - - -- alice and bob computes numbers that they exchange - a' <- alice `locally` \un -> do return $ un alice ga ^ un alice a `mod` un alice pa - b' <- bob `locally` \un -> do return $ un bob gb ^ un bob b `mod` un bob pb - - -- exchange numbers - a'' <- (alice, a') ~> bob @@ nobody - b'' <- (bob, b') ~> alice @@ nobody - - -- compute shared key - alice `locally_` \un -> - let s = un alice b'' ^ un alice a `mod` un alice pa - in putOutput "alice's shared key:" s - bob `locally_` \un -> - let s = un bob a'' ^ un bob b `mod` un bob pb - in putOutput "bob's shared key:" s - -main :: IO () -main = do - [loc] <- getArgs - _ <- case loc of - "alice" -> runCLIIO $ runChoreography config diffieHellman "alice" - "bob" -> runCLIIO $ runChoreography config diffieHellman "bob" - _ -> error "unknown party" - return () - where - config = - mkHttpConfig - [ ("alice", ("localhost", 5000)), - ("bob", ("localhost", 5001)) - ] diff --git a/examples/Distribution/TestSuite/QuickCheck.hs b/examples/Distribution/TestSuite/QuickCheck.hs deleted file mode 100644 --- a/examples/Distribution/TestSuite/QuickCheck.hs +++ /dev/null @@ -1,442 +0,0 @@ -{-# LANGUAGE BlockArguments #-} -{-# LANGUAGE NamedFieldPuns #-} -{-# LANGUAGE RecordWildCards #-} -{-# LANGUAGE TypeApplications #-} - --- | --- Module: Distribution.TestSuite.QuickCheck --- Description: Convert QuickCheck properties into Cabal tests --- Copyright: ⓒ Anselm Schüler 2022 --- License: MIT --- Maintainer: Anselm Schüler --- Stability: stable --- Portability: Portable --- --- This module allows you to easily make Cabal tests for the @detailed-0.9@ interface. See the [docs](https://cabal.readthedocs.io/en/3.6/cabal-package.html#example-package-using-detailed-0-9-interface). --- It sets sensible option declarations for the tests. --- --- This module re-uses record names from "Distribution.TestSuite" and "Test.QuickCheck". --- It is recommended that you enable the [@DisambiguateRecordFields@](https://downloads.haskell.org/ghc/latest/docs/html/users_guide/exts/disambiguate_record_fields.html) extension in GHC and/or import the module qualified. --- For many basic tests, you don’t need to import "Distribution.TestSuite". --- --- To make a test, simply construct a 'PropertyTest' and call 'getPropertyTest' on it. --- --- A simple sample test suite: --- --- @ --- module Tests (tests) where --- import "Distribution.TestSuite.QuickCheck" --- import "Test.QuickCheck" --- tests = [ --- 'getPropertyTest' 'PropertyTest' { --- 'name' = /"addition-is-commutative"/, --- 'tags' = [], --- 'property' = \\a b -> a + b 'QC.===' b + a --- } --- ] --- @ --- --- The tests you get as a result support several parameters: --- --- +--------------------+--------------+---------------------------------------------------------------------------------+ --- | Property name | Valid values | Effect | --- +====================+==============+=================================================================================+ --- | @silent@ | booleans | If true, all output is disabled. | --- | | | Sets 'verbosity' to 'Silent'. See 'QC.chatty'. | --- | | | Disabling Silent raises the verbosity to Chatty if it is not already higher. | --- +--------------------+--------------+---------------------------------------------------------------------------------+ --- | @chatty@ | booleans | If true, the default amount of output is emitted by QuickCheck. | --- | | | Sets 'verbosity' to 'Chatty'. See 'QC.chatty'. | --- | | | Note that setting this verbosity option to false does not undo setting it to | --- | | | true, but lowers the verbosity by one level if it is not already lower. | --- +--------------------+--------------+---------------------------------------------------------------------------------+ --- | @verbose@ | booleans | If true, prints checked values as output. | --- | | | Sets 'verbosity' to 'Verbose'. See 'QC.verbose'. | --- | | | Note that setting this verbosity option to false does not undo setting it to | --- | | | true, but lowers the verbosity by one level if it is not already lower. | --- +--------------------+--------------+---------------------------------------------------------------------------------+ --- | @verboseShrinking@ | booleans | If true, prints all checked and shrunk values as output. | --- | | | See 'QC.verboseShrinking'. | --- +--------------------+--------------+---------------------------------------------------------------------------------+ --- | @verbosity@ | @Silent@, | Sets the 'verbosity' to the desired level. | --- | | @Chatty@, | | --- | | or @Verbose@ | | --- +--------------------+--------------+---------------------------------------------------------------------------------+ --- | @maxDiscardRatio@ | positive | Maximum number of discarded tests per successful test before giving up. | --- | | integer | See 'QC.maxDiscardRatio'. | --- +--------------------+--------------+---------------------------------------------------------------------------------+ --- | @noShrinking@ | booleans | Disables shrinking of test cases. | --- | | | See 'QC.noShrinking'. | --- +--------------------+--------------+---------------------------------------------------------------------------------+ --- | @shrinking@ | booleans | Opposite of @noShrinking@. | --- +--------------------+--------------+---------------------------------------------------------------------------------+ --- | @maxShrinks@ | nonnegative | Maximum number of shrinks before giving up or zero to disable shrinking. | --- | | integer | See 'QC.maxShrinks'. | --- +--------------------+--------------+---------------------------------------------------------------------------------+ --- | @maxSuccess@ | positive | Maximum number of successful tests before succeeding. | --- | | integer | See 'QC.maxSuccess'. | --- +--------------------+--------------+---------------------------------------------------------------------------------+ --- | @maxSize@ | positive | Size to use for the biggest test cases. | --- | | integer | See 'QC.maxSize'. | --- +--------------------+--------------+---------------------------------------------------------------------------------+ --- | @sizeScale@ | positive | Scales all sizes by a number. | --- | | integer | See 'QC.mapSize'. | --- +--------------------+--------------+---------------------------------------------------------------------------------+ --- | @replay@ | tuple of | Replays a previous test case. Pass a string representing a tuple of | --- | | 'QCGen' and | the 'QC.usedSeed' and 'QC.usedSize' values of a test case. Use empty string to | --- | | nonnegative | disable. | --- | | integer or | | --- | | empty | | --- +--------------------+--------------+---------------------------------------------------------------------------------+ --- --- You can set default values by using 'getPropertyTestWith' --- You can access these values in your test by using 'getPropertyTestUsing'. --- Do both with 'getPropertyTestWithUsing'. -module Distribution.TestSuite.QuickCheck - ( -- * Create tests - getPropertyTest, - getPropertyTestWith, - getPropertyTestUsing, - getPropertyTestWithUsing, - getPropertyTests, - propertyTestGroup, - - -- * Argument data types - PropertyTest (..), - TestArgs (..), - Verbosity (..), - - -- * Functions for using arguments - argsToTestArgs, - argsToTestArgsWith, - testArgsToArgs, - stdTestArgs, - ) -where - -import Data.Bool (bool) -import Data.Functor ((<&>)) -import Distribution.TestSuite qualified as T -import Test.QuickCheck qualified as QC -import Test.QuickCheck.Random (QCGen) -import Text.Read (readMaybe) - --- | Datatype for setting the verbosity of tests -data Verbosity - = -- | QuickCheck prints nothing. This sets @'QC.chatty' = 'False'@. - Silent - | -- | Print basic statistics. This sets @'QC.chatty' = 'True'@. - Chatty - | -- | Print every test case. This applies 'QC.verbose'. - Verbose - deriving - ( Eq, - -- | 'Silent' < 'Chatty' < 'Verbose' - Ord, - Show, - Read, - Enum, - Bounded - ) - --- ! [PARTIAL] This function fails when passed Silent -switchVerbosity :: Verbosity -> Bool -> Verbosity -> Verbosity -switchVerbosity v' True v = v' -switchVerbosity v' False v = min (pred v') v - --- | Arguments for altering property test behaviour. --- These can be altered in the final Cabal 'T.Test' using 'T.setOption'. -data TestArgs = TestArgs - { -- | Verbosity for tests. See 'QC.verbose' and 'QC.chatty'. - verbosity :: Verbosity, - -- TODO Consider joining verboseShrinking back into verbosity - - -- | Whether QuickCheck should print shrinks. See 'QC.verboseShrinking'. - verboseShrinking :: Bool, - -- | Maximum discarded tests per successful test. See 'QC.maxDiscardRatio'. - maxDiscardRatio :: Int, - -- | Disable shrinking. See 'QC.noShrinking'. - noShrinking :: Bool, - -- | Maximum number of shrink attempts. See 'QC.maxShrinks'. - maxShrinks :: Int, - -- | Maximum number of successful checks before passing. See 'QC.maxSuccess'. - maxSuccess :: Int, - -- | Maximum size of test cases. See 'QC.maxSize'. - maxSize :: Int, - -- | Scale size by an integer using 'QC.mapSize'. - sizeScale :: Int, - -- | Replay a previous test. Pass the seed and size given by 'QC.usedSeed' and 'QC.usedSize'. - replay :: Maybe (QCGen, Int) - } - --- | Transform a QuickCheck 'QC.Args' value to a 'TestArgs' value, defaulting all missing properties --- --- @'argsToTestArgs' = 'argsToTestArgsWith' 'stdTestArgs'@ -argsToTestArgs :: QC.Args -> TestArgs -argsToTestArgs = argsToTestArgsWith stdTestArgs - --- | Transform a QuickCheck 'QC.Args' value to a 'TestArgs' value, with fallbacks for missing properties given by the first argument. -argsToTestArgsWith :: TestArgs -> QC.Args -> TestArgs -argsToTestArgsWith testArgs QC.Args {..} = - testArgs - { verbosity = if chatty then Chatty else Silent, - maxDiscardRatio, - maxShrinks, - maxSuccess, - maxSize, - replay - } - --- | Recover arguments passed to 'QC.quickCheck' from a 'TestArgs' -testArgsToArgs :: TestArgs -> QC.Args -testArgsToArgs TestArgs {..} = - QC.Args - { replay, - maxSuccess, - maxDiscardRatio, - maxSize, - chatty = verbosity >= Chatty, - maxShrinks - } - --- | Default arguments for property tests -stdTestArgs :: TestArgs -stdTestArgs = - TestArgs - { verbosity = Chatty, - verboseShrinking = False, - maxDiscardRatio = 10, - noShrinking = False, - maxShrinks = maxBound, - maxSuccess = 100, - maxSize = 100, - sizeScale = 1, - replay = Nothing - } - -switchVIn :: Verbosity -> Bool -> TestArgs -> TestArgs -switchVIn v' q args@TestArgs {verbosity} = args {verbosity = switchVerbosity v' q verbosity} - -setArgStr :: String -> String -> Maybe (TestArgs -> TestArgs) -setArgStr "silent" str = - readMaybe str <&> \val args@TestArgs {verbosity} -> - if val - then args {verbosity = Silent} - else args {verbosity = max Chatty verbosity} -setArgStr "chatty" str = readMaybe str <&> switchVIn Chatty -setArgStr "verbose" str = readMaybe str <&> switchVIn Verbose -setArgStr "verboseShrinking" str = - readMaybe str <&> \val args -> - args {verboseShrinking = val} -setArgStr "verbosity" str = - readMaybe str <&> \val args -> - args {verbosity = val} -setArgStr "maxDiscardRatio" str = - readMaybe str <&> \val args -> - args {maxDiscardRatio = val} -setArgStr "noShrinking" str = - readMaybe str <&> \val args -> - args {noShrinking = val} -setArgStr "shrinking" str = - readMaybe str <&> \val args -> - args {noShrinking = not val} -setArgStr "maxShrinks" str = - readMaybe str <&> \val args -> - args {maxShrinks = val} -setArgStr "maxSuccess" str = - readMaybe str <&> \val args -> - args {maxSuccess = val} -setArgStr "maxSize" str = - readMaybe str <&> \val args -> - args {maxSize = val} -setArgStr "sizeScale" str = - readMaybe str <&> \val args -> - args {sizeScale = val} -setArgStr "replay" str = - case str of - "" -> Just \args -> args {replay = Nothing} - _ -> - readMaybe str <&> \val args -> - args {replay = Just val} -setArgStr _ _ = Nothing - -positiveIntType :: T.OptionType -positiveIntType = - T.OptionNumber - { optionNumberIsInt = True, - optionNumberBounds = (Just "1", Nothing) - } - -getOptionDescrs :: TestArgs -> [T.OptionDescr] -getOptionDescrs TestArgs {..} = - [ T.OptionDescr - { optionName = "silent", - optionDescription = "Suppress QuickCheck output", - optionType = T.OptionBool, - optionDefault = Just . show $ verbosity == Silent - }, - T.OptionDescr - { optionName = "chatty", - optionDescription = "Print QuickCheck output", - optionType = T.OptionBool, - optionDefault = Just . show $ verbosity > Chatty - }, - T.OptionDescr - { optionName = "verbose", - optionDescription = "Print checked values", - optionType = T.OptionBool, - optionDefault = Just . show $ verbosity > Verbose - }, - T.OptionDescr - { optionName = "verboseShrinking", - optionDescription = "Print all checked and shrunk values", - optionType = T.OptionBool, - optionDefault = Just . show $ verboseShrinking - }, - T.OptionDescr - { optionName = "verbosity", - optionDescription = "Verbosity level", - optionType = T.OptionEnum ["Silent", "Chatty", "Verbose", "VerboseShrinking"], - optionDefault = Just $ show verbosity - }, - T.OptionDescr - { optionName = "maxDiscardRatio", - optionDescription = "Maximum number of discarded tests per successful test before giving up", - optionType = positiveIntType, - optionDefault = Just $ show maxDiscardRatio - }, - T.OptionDescr - { optionName = "noShrinking", - optionDescription = "Disable shrinking", - optionType = T.OptionBool, - optionDefault = Just $ show noShrinking - }, - T.OptionDescr - { optionName = "shrinking", - optionDescription = "Enable shrinking", - optionType = T.OptionBool, - optionDefault = Just . show $ not noShrinking - }, - T.OptionDescr - { optionName = "maxShrinks", - optionDescription = "Maximum number of shrinks before giving up or zero to disable shrinking", - optionType = - T.OptionNumber - { optionNumberIsInt = True, - optionNumberBounds = (Just "0", Nothing) - }, - optionDefault = Just $ show maxShrinks - }, - T.OptionDescr - { optionName = "maxSuccess", - optionDescription = "Maximum number of successful tests before succeeding", - optionType = positiveIntType, - optionDefault = Just $ show maxSuccess - }, - T.OptionDescr - { optionName = "maxSize", - optionDescription = "Size to use for the biggest test cases", - optionType = positiveIntType, - optionDefault = Just $ show maxSize - }, - T.OptionDescr - { optionName = "sizeScale", - optionDescription = "Scale all sizes by a number", - optionType = positiveIntType, - optionDefault = Just $ show sizeScale - }, - T.OptionDescr - { optionName = "replay", - optionDescription = "Replay a previous test", - optionType = T.OptionString False, - optionDefault = Just $ show @(Maybe (QCGen, Int)) Nothing - } - ] - -getModifiers :: (QC.Testable a) => TestArgs -> a -> QC.Property -getModifiers TestArgs {verbosity, noShrinking, verboseShrinking, sizeScale} = - foldr (.) QC.property $ - snd - <$> filter - fst - [ (verbosity == Verbose, QC.verbose), - (verboseShrinking, QC.verboseShrinking), - (noShrinking, QC.noShrinking), - (sizeScale /= 1, QC.mapSize (* sizeScale)) - ] - --- | Property test declaration with metadata -data PropertyTest prop = PropertyTest - { -- | Name of the test, for Cabal. See See Cabal’s 'T.name'. - name :: String, - -- | Tags of the test, for Cabal. See Cabal’s 'T.tags'. - tags :: [String], - -- | Property to check. This should usually be or return an instance of 'QC.Testable'. - property :: prop - } - -qcTestArgs :: (QC.Testable a) => TestArgs -> a -> IO QC.Result -qcTestArgs args property = QC.quickCheckWithResult (testArgsToArgs args) (getModifiers args property) - --- | Get a Cabal 'T.Test' with custom 'TestArgs' from a 'PropertyTest' that takes the test arguments and returns a 'QC.testable' value -getPropertyTestWithUsing :: - (QC.Testable prop) => - -- | The arguments for the test - TestArgs -> - -- | A property test whose 'property' takes a 'TestArgs' argument - PropertyTest (TestArgs -> prop) -> - T.Test -getPropertyTestWithUsing originalArgs PropertyTest {..} = - let withArgs args = - T.TestInstance - { run = do - result <- qcTestArgs args (property args) - let resultStr = "\n" ++ show result - return $ T.Finished case result of - QC.Success {} -> T.Pass - QC.GaveUp {} -> - T.Error $ "GaveUp: QuickCheck gave up" ++ resultStr - QC.Failure {} -> - T.Fail $ "Failure: A property failed" ++ resultStr - QC.NoExpectedFailure {} -> - T.Fail $ "NoExpectedFailure: A property that should have failed did not" ++ resultStr, - name, - tags, - options = getOptionDescrs originalArgs, - setOption = \opt str -> case setArgStr opt str of - Nothing -> Left "Parse error" - Just f -> Right . withArgs $ f args - } - in T.Test $ withArgs originalArgs - --- | Get a Cabal 'T.Test' from a 'PropertyTest' that takes the test arguments and returns a 'QC.Testable' value -getPropertyTestUsing :: - (QC.Testable prop) => - -- | A property test whose 'property' takes a 'TestArgs' argument - PropertyTest (TestArgs -> prop) -> - T.Test -getPropertyTestUsing = getPropertyTestWithUsing stdTestArgs - -discardingTestArgs :: PropertyTest prop -> PropertyTest (TestArgs -> prop) -discardingTestArgs test@PropertyTest {property} = test {property = const property} - --- | Get a Cabal 'T.Test' from a 'PropertyTest' with custom 'TestArgs' -getPropertyTestWith :: - (QC.Testable prop) => - -- | The arguments for the test - TestArgs -> - PropertyTest prop -> - T.Test -getPropertyTestWith args = getPropertyTestWithUsing args . discardingTestArgs - --- | Get a Cabal 'T.Test' from a 'PropertyTest' -getPropertyTest :: (QC.Testable prop) => PropertyTest prop -> T.Test -getPropertyTest = getPropertyTestWithUsing stdTestArgs . discardingTestArgs - --- | Get a list of 'T.Test's from a list of 'PropertyTest's -getPropertyTests :: (QC.Testable prop) => [PropertyTest prop] -> [T.Test] -getPropertyTests = (getPropertyTest <$>) - --- | Get a named test group from a list of 'PropertyTest's. These are assumed to be able to run in parallel. See 'T.testGroup' and 'T.Group'. -propertyTestGroup :: (QC.Testable prop) => String -> [PropertyTest prop] -> T.Test -propertyTestGroup name = T.testGroup name . getPropertyTests diff --git a/examples/GMWReal.hs b/examples/GMWReal.hs deleted file mode 100644 --- a/examples/GMWReal.hs +++ /dev/null @@ -1,202 +0,0 @@ -{-# LANGUAGE BlockArguments #-} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TemplateHaskell #-} - -module GMWReal where - -import CLI -import Choreography -import Choreography.Network.Http -import Control.Monad (void) -import Control.Monad.IO.Class (MonadIO, liftIO) -import Crypto.Random.Types qualified as CRT -import Data (TestArgs, reference) -import Data.Foldable (toList) -import Data.Kind (Type) -import Data.Maybe (fromJust) -import GHC.TypeLits (KnownSymbol) -import ObliviousTransfer -import System.Environment -import System.Random -import Test.QuickCheck (Arbitrary, arbitrary, chooseInt, elements, getSize, oneof, resize) - -$(mkLoc "trusted3rdParty") -$(mkLoc "p1") -$(mkLoc "p2") -$(mkLoc "p3") -$(mkLoc "p4") - -xor :: (Foldable f) => f Bool -> Bool -xor = foldr1 (/=) - -data Circuit :: [LocTy] -> Type where - InputWire :: (KnownSymbol p) => Member p ps -> Circuit ps - LitWire :: Bool -> Circuit ps - AndGate :: Circuit ps -> Circuit ps -> Circuit ps - XorGate :: Circuit ps -> Circuit ps -> Circuit ps - -instance Show (Circuit ps) where - show (InputWire p) = "InputWire<" ++ toLocTm p ++ ">" - show (LitWire b) = "LitWire " ++ show b - show (AndGate left right) = "(" ++ show left ++ ") AND (" ++ show right ++ ")" - show (XorGate left right) = "(" ++ show left ++ ") XOR (" ++ show right ++ ")" - -instance Arbitrary (Circuit '["p1", "p2", "p3", "p4"]) where - arbitrary = do - size <- getSize - if 1 >= size - then oneof $ (LitWire <$> arbitrary) : (pure <$> [InputWire p1, InputWire p2, InputWire p3, InputWire p4]) - else do - left <- chooseInt (1, size) - a <- resize left arbitrary - b <- resize (1 `max` (size - left)) arbitrary - op <- elements [AndGate, XorGate] - return $ a `op` b - -data Args = Args - { circuit :: Circuit '["p1", "p2", "p3", "p4"], - p1in :: Bool, -- These should be lists, but consuming them would be a chore... - p2in :: Bool, - p3in :: Bool, - p4in :: Bool - } - deriving (Show) - -instance Arbitrary Args where - arbitrary = Args <$> arbitrary <*> arbitrary <*> arbitrary <*> arbitrary <*> arbitrary - -instance TestArgs Args (Bool, Bool, Bool, Bool) where - reference Args {circuit, p1in, p2in, p3in, p4in} = (answer, answer, answer, answer) - where - recurse c = case c of - InputWire p -> fromJust $ toLocTm p `lookup` inputs - LitWire b -> b - AndGate left right -> recurse left && recurse right - XorGate left right -> recurse left /= recurse right - inputs = ["p1", "p2", "p3", "p4"] `zip` [p1in, p2in, p3in, p4in] - answer = recurse circuit - -genShares :: forall ps p m. (MonadIO m, KnownSymbols ps) => Member p ps -> Bool -> m (Quire ps Bool) -genShares p x = quorum1 p gs' - where - gs' :: forall q qs. (KnownSymbol q, KnownSymbols qs) => m (Quire (q ': qs) Bool) - gs' = do - freeShares <- sequence $ pure $ liftIO randomIO -- generate n-1 random shares - return $ qCons (xor (qCons @q x freeShares)) freeShares - -secretShare :: - forall parties p m. - (KnownSymbols parties, KnownSymbol p, MonadIO m) => - Member p parties -> - Located '[p] Bool -> - Choreo parties m (Faceted parties '[] Bool) -secretShare p value = do - shares <- locally p \un -> genShares p (un singleton value) - PIndexed fs <- scatter p (allOf @parties) shares - return $ PIndexed $ Facet . othersForget (First @@ nobody) . getFacet . fs - -reveal :: forall ps m. (KnownSymbols ps) => Faceted ps '[] Bool -> Choreo ps m Bool -reveal shares = xor <$> (gather ps ps shares >>= naked ps) - where - ps = allOf @ps - --- use OT to do multiplication -fAnd :: - forall parties m. - (KnownSymbols parties, MonadIO m, CRT.MonadRandom m) => - Faceted parties '[] Bool -> - Faceted parties '[] Bool -> - Choreo parties (CLI m) (Faceted parties '[] Bool) -fAnd uShares vShares = do - let genBools = sequence $ pure randomIO - a_j_s :: Faceted parties '[] (Quire parties Bool) <- _parallel (allOf @parties) genBools - bs :: Faceted parties '[] Bool <- fanOut \p_j -> do - let p_j_name = toLocTm p_j - b_i_s <- fanIn (p_j @@ nobody) \p_i -> - if toLocTm p_i == p_j_name - then _locally p_j $ pure False - else do - -- bb is the truth table - bb <- locally p_i \un -> - let a_ij = getLeaf (viewFacet un p_i a_j_s) p_j - u_i = viewFacet un p_i uShares - in pure (xor [u_i, a_ij], a_ij) - -- localize p_j vSHares is party j's share of v - enclaveTo (p_i @@ p_j @@ nobody) (listedSecond @@ nobody) (ot2 bb $ localize p_j vShares) - locally p_j \un -> pure $ xor $ un singleton b_i_s - parallel (allOf @parties) \p_i un -> - let computeShare u v a_js b = xor $ [u && v, b] ++ toList (qModify p_i (const False) a_js) - in pure $ - computeShare - (viewFacet un p_i uShares) - (viewFacet un p_i vShares) - (viewFacet un p_i a_j_s) - (viewFacet un p_i bs) - -gmw :: - forall parties m. - (KnownSymbols parties, MonadIO m, CRT.MonadRandom m) => - Circuit parties -> - Choreo parties (CLI m) (Faceted parties '[] Bool) -gmw circuit = case circuit of - InputWire p -> do - -- process a secret input value from party p - value :: Located '[p] Bool <- _locally p $ getInput "Enter a secret input value:" - secretShare p value - LitWire b -> do - -- process a publicly-known literal value - let chooseShare :: forall p. (KnownSymbol p) => Member p parties -> Choreo parties (CLI m) (Located '[p] Bool) - chooseShare p = congruently (p @@ nobody) $ \_ -> case p of - First -> b - Later _ -> False - fanOut chooseShare - AndGate l r -> do - -- process an AND gate - lResult <- gmw l - rResult <- gmw r - fAnd lResult rResult - XorGate l r -> do - -- process an XOR gate - lResult <- gmw l - rResult <- gmw r - parallel (allOf @parties) \p un -> pure $ xor [viewFacet un p lResult, viewFacet un p rResult] - -mpc :: - forall parties m. - (KnownSymbols parties, MonadIO m, CRT.MonadRandom m) => - Circuit parties -> - Choreo parties (CLI m) () -mpc circuit = do - outputWire <- gmw circuit - result <- reveal outputWire - void $ _parallel (allOf @parties) $ putOutput "The resulting bit:" result - -mpcmany :: - (KnownSymbols parties, MonadIO m, CRT.MonadRandom m) => - Circuit parties -> - Choreo parties (CLI m) () -mpcmany circuit = do - mpc circuit - -type Clients = '["p1", "p2"] -- , "p3", "p4"] - -main :: IO () -main = do - let circuit :: Circuit Clients = AndGate (LitWire True) (LitWire True) - [loc] <- getArgs - delivery <- case loc of - "p1" -> runCLIIO $ runChoreography cfg (mpcmany @Clients circuit) "p1" - "p2" -> runCLIIO $ runChoreography cfg (mpcmany @Clients circuit) "p2" - -- "p3" -> runCLIIO $ runChoreography cfg (mpcmany @Clients circuit) "p3" - -- "p4" -> runCLIIO $ runChoreography cfg (mpcmany @Clients circuit) "p4" - _ -> error "unknown party" - print delivery - where - cfg = - mkHttpConfig - [ ("p1", ("localhost", 4242)), - ("p2", ("localhost", 4343)) - -- , ("p3", ("localhost", 4344)) - -- , ("p4", ("localhost", 4345)) - ] diff --git a/examples/KVS1Simple.hs b/examples/KVS1Simple.hs deleted file mode 100644 --- a/examples/KVS1Simple.hs +++ /dev/null @@ -1,120 +0,0 @@ -{-# LANGUAGE BlockArguments #-} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TemplateHaskell #-} -{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-} - -{- -# This example was carried over from earlier work, likely HasChor. It doesn't yet have a unit test attached to it. - -# Example: Simple client-server key-value store - -This is the first version of the 4-stage key-value store tutorial and implements a simple client-server key-value store. The client can `PUT` a key-value pair to the server and `GET` a value for a given key. - -## Execution - -```bash -# start server -cabal run kvs1 server -# on a different terminal for client -cabal run kvs1 client -GET hello -> Nothing -PUT hello world -> Just "world" -GET hello -> Just "world" -``` --} - -module KVS1Simple where - -import Choreography -import Choreography.Network.Http -import Data.IORef -import Data.Map (Map) -import Data.Map qualified as Map -import System.Environment - -$(mkLoc "client") -$(mkLoc "server") - -type Participants = ["client", "server"] - -type State = Map String String - -data Request = Put String String | Get String deriving (Show, Read) - -type Response = Maybe String - --- | `readRequest` reads a request from the terminal. -readRequest :: IO Request -readRequest = do - putStrLn "Command?" - line <- getLine - case parseRequest line of - Just t -> return t - Nothing -> putStrLn "Invalid command" >> readRequest - where - parseRequest :: String -> Maybe Request - parseRequest s = - let l = words s - in case l of - ["GET", k] -> Just (Get k) - ["PUT", k, v] -> Just (Put k v) - _ -> Nothing - --- | `handleRequest` handle a request and returns the new the state. -handleRequest :: Request -> IORef State -> IO Response -handleRequest request stateRef = case request of - Put key value -> do - modifyIORef stateRef (Map.insert key value) - return (Just value) - Get key -> do - state <- readIORef stateRef - return (Map.lookup key state) - --- | `kvs` is a choreography that processes a single request located at the client and returns the response. -kvs :: - Located '["client"] Request -> - Located '["server"] (IORef State) -> - Choreo Participants IO (Located '["client"] Response) -kvs request stateRef = do - -- send the request to the server - request' <- (client, request) ~> server @@ nobody - -- the server handles the response and creates a response - response <- - server `locally` \un -> - handleRequest (un server request') (un server stateRef) - -- send the response back to the client - (server, response) ~> client @@ nobody - --- | `mainChoreo` is a choreography that serves as the entry point of the program. --- It initializes the state and loops forever. --- HIII :> (*>_*) -mainChoreo :: Choreo Participants IO () -mainChoreo = do - stateRef <- server `_locally` newIORef (Map.empty :: State) - loop stateRef - where - loop :: Located '["server"] (IORef State) -> Choreo Participants IO () - loop stateRef = do - request <- client `_locally` readRequest - response <- kvs request stateRef - client `locally_` \un -> do putStrLn ("> " ++ show (un client response)) - loop stateRef - -main :: IO () -main = do - [loc] <- getArgs - case loc of - "client" -> runChoreography config mainChoreo "client" - "server" -> runChoreography config mainChoreo "server" - _ -> error "unknown party" - return () - where - config = - mkHttpConfig - [ ("client", ("localhost", 3000)), - ("server", ("localhost", 4000)) - ] diff --git a/examples/KVS2PrimaryBackup.hs b/examples/KVS2PrimaryBackup.hs deleted file mode 100644 --- a/examples/KVS2PrimaryBackup.hs +++ /dev/null @@ -1,139 +0,0 @@ -{-# LANGUAGE BlockArguments #-} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TemplateHaskell #-} - -{- -# This example was carried over from earlier work, likely HasChor. It doesn't yet have a unit test attached to it. - -# Example: Primary-backup key-value store - -This is the second version of the 4-stage key-value store tutorial. This builds on the first version and adds a backup location to improve durability. - -```bash -# start primary -cabal run kvs2 primary -# on a different terminal, start backup -cabal run kvs2 backup -# another terminal for client -cabal run kvs2 client -GET hello -> Nothing -PUT hello world -> Just "world" -GET hello -> Just "world" -``` --} - -module KVS2PrimaryBackup where - -import Choreography -import Choreography.Network.Http -import Data.IORef -import Data.Map (Map) -import Data.Map qualified as Map -import System.Environment - -$(mkLoc "client") -$(mkLoc "primary") -$(mkLoc "backup") - -type Participants = ["client", "primary", "backup"] - -type State = Map String String - -data Request = Put String String | Get String deriving (Show, Read) - -type Response = Maybe String - --- | `readRequest` reads a request from the terminal. -readRequest :: IO Request -readRequest = do - putStrLn "Command?" - line <- getLine - case parseRequest line of - Just t -> return t - Nothing -> putStrLn "Invalid command" >> readRequest - where - parseRequest :: String -> Maybe Request - parseRequest s = - let l = words s - in case l of - ["GET", k] -> Just (Get k) - ["PUT", k, v] -> Just (Put k v) - _ -> Nothing - --- | `handleRequest` handle a request and returns the new the state. -handleRequest :: Request -> IORef State -> IO Response -handleRequest request stateRef = case request of - Put key value -> do - modifyIORef stateRef (Map.insert key value) - return (Just value) - Get key -> do - state <- readIORef stateRef - return (Map.lookup key state) - --- | `kvs` is a choreography that processes a single request located at the client and returns the response. --- If the request is a `PUT`, it will forward the request to the backup node. -kvs :: - Located '["client"] Request -> - (Located '["primary"] (IORef State), Located '["backup"] (IORef State)) -> - Choreo Participants IO (Located '["client"] Response) -kvs request (primaryStateRef, backupStateRef) = do - -- send request to the primary node - request' <- (client, request) ~> primary @@ nobody - - -- branch on the request - broadcast (primary, request') >>= \case - -- if the request is a `PUT`, forward the request to the backup node - Put _ _ -> do - request'' <- (primary, request') ~> backup @@ nobody - ack <- - backup `locally` \un -> do - handleRequest (un backup request'') (un backup backupStateRef) - _ <- (backup, ack) ~> primary @@ nobody - return () - _ -> do - return () - - -- process request on the primary node - response <- - primary `locally` \un -> - handleRequest (un primary request') (un primary primaryStateRef) - - -- send response to client - (primary, response) ~> client @@ nobody - --- | `mainChoreo` is a choreography that serves as the entry point of the program. --- It initializes the state and loops forever. -mainChoreo :: Choreo Participants IO () -mainChoreo = do - primaryStateRef <- primary `_locally` newIORef (Map.empty :: State) - backupStateRef <- backup `_locally` newIORef (Map.empty :: State) - loop (primaryStateRef, backupStateRef) - where - loop :: (Located '["primary"] (IORef State), Located '["backup"] (IORef State)) -> Choreo Participants IO () - loop stateRefs = do - request <- client `_locally` readRequest - response <- kvs request stateRefs - client `locally_` \un -> do putStrLn ("> " ++ show (un client response)) - loop stateRefs - -main :: IO () -main = do - [loc] <- getArgs - case loc of - "client" -> runChoreography config mainChoreo "client" - "primary" -> runChoreography config mainChoreo "primary" - "backup" -> runChoreography config mainChoreo "backup" - _ -> error "unknown party" - return () - where - config = - mkHttpConfig - [ ("client", ("localhost", 3000)), - ("primary", ("localhost", 4000)), - ("backup", ("localhost", 5000)) - ] diff --git a/examples/KVS3HigherOrder.hs b/examples/KVS3HigherOrder.hs deleted file mode 100644 --- a/examples/KVS3HigherOrder.hs +++ /dev/null @@ -1,174 +0,0 @@ -{-# LANGUAGE BlockArguments #-} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TemplateHaskell #-} - -{- -# This example was carried over from earlier work, likely HasChor. It doesn't yet have a unit test attached to it. - -# Example: Key-value store with higher-order choreography - -## Execution - -By default, `primaryBackupReplicationStrategy` will be used. Change `mainChoreo` to `nullReplicationChoreo` to use `nullReplicationStrategy`. - -```bash -# start primary -cabal run kvs3 primary -# on a different terminal, start backup -cabal run kvs3 backup -# another terminal for client -cabal run kvs3 client -GET hello -> Nothing -PUT hello world -> Just "world" -GET hello -> Just "world" -``` --} - -module KVS3HigherOrder where - -import Choreography -import Choreography.Network.Http -import Data.IORef -import Data.Map (Map) -import Data.Map qualified as Map -import System.Environment - -$(mkLoc "client") -$(mkLoc "primary") -$(mkLoc "backup") - -type Participants = ["client", "primary", "backup"] - -type State = Map String String - -data Request = Put String String | Get String deriving (Show, Read) - -type Response = Maybe String - --- | `readRequest` reads a request from the terminal. -readRequest :: IO Request -readRequest = do - putStrLn "Command?" - line <- getLine - case parseRequest line of - Just t -> return t - Nothing -> putStrLn "Invalid command" >> readRequest - where - parseRequest :: String -> Maybe Request - parseRequest s = - let l = words s - in case l of - ["GET", k] -> Just (Get k) - ["PUT", k, v] -> Just (Put k v) - _ -> Nothing - --- | `handleRequest` handle a request and returns the new the state. -handleRequest :: Request -> IORef State -> IO Response -handleRequest request stateRef = case request of - Put key value -> do - modifyIORef stateRef (Map.insert key value) - return (Just value) - Get key -> do - state <- readIORef stateRef - return (Map.lookup key state) - --- | ReplicationStrategy specifies how a request should be handled on possibly replicated servers --- `a` is a type that represent states across locations -type ReplicationStrategy a = - Located '["primary"] Request -> a -> Choreo Participants IO (Located '["primary"] Response) - --- | `nullReplicationStrategy` is a replication strategy that does not replicate the state. -nullReplicationStrategy :: ReplicationStrategy (Located '["primary"] (IORef State)) -nullReplicationStrategy request stateRef = do - primary `locally` \un -> - handleRequest (un primary request) (un primary stateRef) - --- | `primaryBackupReplicationStrategy` is a replication strategy that replicates the state to a backup server. -primaryBackupReplicationStrategy :: - ReplicationStrategy (Located '["primary"] (IORef State), Located '["backup"] (IORef State)) -primaryBackupReplicationStrategy request (primaryStateRef, backupStateRef) = do - -- relay request to backup if it is mutating (= PUT) - broadcast (primary, request) >>= \case - Put _ _ -> do - request' <- (primary, request) ~> backup @@ nobody - _ <- - ( backup, - \un -> - handleRequest (un backup request') (un backup backupStateRef) - ) - ~~> primary - @@ nobody - return () - _ -> do - return () - - -- process request on primary - primary `locally` \un -> - handleRequest (un primary request) (un primary primaryStateRef) - --- | `kvs` is a choreography that processes a single request at the client and returns the response. --- It uses the provided replication strategy to handle the request. -kvs :: - forall a. - Located '["client"] Request -> - a -> - ReplicationStrategy a -> - Choreo Participants IO (Located '["client"] Response) -kvs request stateRefs replicationStrategy = do - request' <- (client, request) ~> primary @@ nobody - - -- call the provided replication strategy - response <- replicationStrategy request' stateRefs - - -- send response to client - (primary, response) ~> client @@ nobody - --- | `nullReplicationChoreo` is a choreography that uses `nullReplicationStrategy`. -nullReplicationChoreo :: Choreo Participants IO () -nullReplicationChoreo = do - stateRef <- primary `_locally` newIORef (Map.empty :: State) - loop stateRef - where - loop :: Located '["primary"] (IORef State) -> Choreo Participants IO () - loop stateRef = do - request <- client `_locally` readRequest - response <- kvs request stateRef nullReplicationStrategy - client `locally_` \un -> do print (un client response) - loop stateRef - --- | `primaryBackupChoreo` is a choreography that uses `primaryBackupReplicationStrategy`. -primaryBackupChoreo :: Choreo Participants IO () -primaryBackupChoreo = do - primaryStateRef <- primary `_locally` newIORef (Map.empty :: State) - backupStateRef <- backup `_locally` newIORef (Map.empty :: State) - loop (primaryStateRef, backupStateRef) - where - loop :: (Located '["primary"] (IORef State), Located '["backup"] (IORef State)) -> Choreo Participants IO () - loop stateRefs = do - request <- client `_locally` readRequest - response <- kvs request stateRefs primaryBackupReplicationStrategy - client `locally_` \un -> do putStrLn ("> " ++ show (un client response)) - loop stateRefs - -main :: IO () -main = do - [loc] <- getArgs - case loc of - "client" -> runChoreography config mainChoreo "client" - "primary" -> runChoreography config mainChoreo "primary" - "backup" -> runChoreography config mainChoreo "backup" - _ -> error "unknown party" - return () - where - mainChoreo = primaryBackupChoreo -- or `nullReplicationChoreo` - config = - mkHttpConfig - [ ("client", ("localhost", 3000)), - ("primary", ("localhost", 4000)), - ("backup", ("localhost", 5000)) - ] diff --git a/examples/KVS4LocPoly.hs b/examples/KVS4LocPoly.hs deleted file mode 100644 --- a/examples/KVS4LocPoly.hs +++ /dev/null @@ -1,217 +0,0 @@ -{-# LANGUAGE BlockArguments #-} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TemplateHaskell #-} - -{- -# This example was carried over from earlier work, likely HasChor. It doesn't yet have a unit test attached to it. - -# Example: Key-value store with location polymorphism - -This is the final version of the 4-stage key-value store tutorial where we define the location-polymorphic choreography `doBackup`. We use it to define `doubleBackupReplicationStrategy`, which replicates data to two backup locations (`backup1` and `backup2`). - -## Execution - -```bash -# start primary -cabal run kvs4 primary -# on a different terminal, start backup1 -cabal run kvs4 backup1 -# another terminal for backup2 -cabal run kvs4 backup2 -# yet another terminal for client -cabal run kvs4 client -GET hello -> Nothing -PUT hello world -> Just "world" -GET hello -> Just "world" -``` --} - -module KVS4LocPoly where - -import Choreography -import Choreography.Network.Http -import Data.IORef -import Data.Map (Map) -import Data.Map qualified as Map -import GHC.TypeLits (KnownSymbol) -import System.Environment - -$(mkLoc "client") -$(mkLoc "primary") -$(mkLoc "backup1") -$(mkLoc "backup2") - -type Participants = ["client", "primary", "backup1", "backup2"] - -type State = Map String String - -data Request = Put String String | Get String deriving (Show, Read) - -type Response = Maybe String - --- | `readRequest` reads a request from the terminal. -readRequest :: IO Request -readRequest = do - putStrLn "Command?" - line <- getLine - case parseRequest line of - Just t -> return t - Nothing -> putStrLn "Invalid command" >> readRequest - where - parseRequest :: String -> Maybe Request - parseRequest s = - let l = words s - in case l of - ["GET", k] -> Just (Get k) - ["PUT", k, v] -> Just (Put k v) - _ -> Nothing - --- | `handleRequest` handle a request and returns the new the state. -handleRequest :: Request -> IORef State -> IO Response -handleRequest request stateRef = case request of - Put key value -> do - modifyIORef stateRef (Map.insert key value) - return (Just value) - Get key -> do - state <- readIORef stateRef - return (Map.lookup key state) - --- | ReplicationStrategy specifies how a request should be handled on possibly replicated servers --- `a` is a type that represent states across locations -type ReplicationStrategy a = Located '["primary"] Request -> a -> Choreo Participants IO (Located '["primary"] Response) - --- | `nullReplicationStrategy` is a replication strategy that does not replicate the state. -nullReplicationStrategy :: ReplicationStrategy (Located '["primary"] (IORef State)) -nullReplicationStrategy request stateRef = do - primary `locally` \un -> case un primary request of - Put key value -> do - modifyIORef (un primary stateRef) (Map.insert key value) - return (Just value) - Get key -> do - state <- readIORef (un primary stateRef) - return (Map.lookup key state) - --- | `doBackup` relays a mutating request to a backup location. -doBackup :: - ( KnownSymbol a, - KnownSymbol b, - KnownSymbols ps - ) => - Member a ps -> - Member b ps -> - Located '[a] Request -> - Located '[b] (IORef State) -> - Choreo ps IO () -doBackup locA locB request stateRef = do - broadcast (locA, request) >>= \case - Put _ _ -> do - request' <- (locA, request) ~> locB @@ nobody - _ <- - (locB, \un -> handleRequest (un singleton request') (un singleton stateRef)) - ~~> locA - @@ nobody - return () - _ -> do - return () - --- | `primaryBackupReplicationStrategy` is a replication strategy that replicates the state to a backup server. -primaryBackupReplicationStrategy :: ReplicationStrategy (Located '["primary"] (IORef State), Located '["backup1"] (IORef State)) -primaryBackupReplicationStrategy request (primaryStateRef, backupStateRef) = do - -- relay request to backup if it is mutating (= PUT) - doBackup primary backup1 request backupStateRef - - -- process request on primary - primary `locally` \un -> handleRequest (un primary request) (un primary primaryStateRef) - --- | `doubleBackupReplicationStrategy` is a replication strategy that replicates the state to two backup servers. -doubleBackupReplicationStrategy :: - ReplicationStrategy - (Located '["primary"] (IORef State), Located '["backup1"] (IORef State), Located '["backup2"] (IORef State)) -doubleBackupReplicationStrategy - request - (primaryStateRef, backup1StateRef, backup2StateRef) = do - -- relay to two backup locations - doBackup primary backup1 request backup1StateRef - doBackup primary backup2 request backup2StateRef - - -- process request on primary - primary `locally` \un -> - handleRequest (un primary request) (un primary primaryStateRef) - --- | `kvs` is a choreography that processes a single request at the client and returns the response. --- It uses the provided replication strategy to handle the request. -kvs :: Located '["client"] Request -> a -> ReplicationStrategy a -> Choreo Participants IO (Located '["client"] Response) -kvs request stateRefs replicationStrategy = do - request' <- (client, request) ~> primary @@ nobody - - -- call the provided replication strategy - response <- replicationStrategy request' stateRefs - - -- send response to client - (primary, response) ~> client @@ nobody - --- | `nullReplicationChoreo` is a choreography that uses `nullReplicationStrategy`. -nullReplicationChoreo :: Choreo Participants IO () -nullReplicationChoreo = do - stateRef <- primary `_locally` newIORef (Map.empty :: State) - loop stateRef - where - loop :: Located '["primary"] (IORef State) -> Choreo Participants IO () - loop stateRef = do - request <- client `_locally` readRequest - response <- kvs request stateRef nullReplicationStrategy - client `locally_` \un -> do print (un client response) - loop stateRef - --- | `primaryBackupChoreo` is a choreography that uses `primaryBackupReplicationStrategy`. -primaryBackupChoreo :: Choreo Participants IO () -primaryBackupChoreo = do - primaryStateRef <- primary `_locally` newIORef (Map.empty :: State) - backupStateRef <- backup1 `_locally` newIORef (Map.empty :: State) - loop (primaryStateRef, backupStateRef) - where - loop :: (Located '["primary"] (IORef State), Located '["backup1"] (IORef State)) -> Choreo Participants IO () - loop stateRefs = do - request <- client `_locally` readRequest - response <- kvs request stateRefs primaryBackupReplicationStrategy - client `locally_` \un -> do print (un client response) - loop stateRefs - --- | `doubleBackupChoreo` is a choreography that uses `doubleBackupReplicationStrategy`. -doubleBackupChoreo :: Choreo Participants IO () -doubleBackupChoreo = do - primaryStateRef <- primary `_locally` newIORef (Map.empty :: State) - backup1StateRef <- backup1 `_locally` newIORef (Map.empty :: State) - backup2StateRef <- backup2 `_locally` newIORef (Map.empty :: State) - loop (primaryStateRef, backup1StateRef, backup2StateRef) - where - loop :: (Located '["primary"] (IORef State), Located '["backup1"] (IORef State), Located '["backup2"] (IORef State)) -> Choreo Participants IO () - loop stateRefs = do - request <- client `_locally` readRequest - response <- kvs request stateRefs doubleBackupReplicationStrategy - client `locally_` \un -> do putStrLn ("> " ++ show (un client response)) - loop stateRefs - -main :: IO () -main = do - [loc] <- getArgs - case loc of - "client" -> runChoreography config primaryBackupChoreo "client" - "primary" -> runChoreography config primaryBackupChoreo "primary" - "backup1" -> runChoreography config primaryBackupChoreo "backup1" - "backup2" -> runChoreography config primaryBackupChoreo "backup2" - _ -> error "unknown party" - return () - where - config = - mkHttpConfig - [ ("client", ("localhost", 3000)), - ("primary", ("localhost", 4000)), - ("backup1", ("localhost", 5000)), - ("backup2", ("localhost", 6000)) - ] diff --git a/examples/KVS5Fig17.hs b/examples/KVS5Fig17.hs deleted file mode 100644 --- a/examples/KVS5Fig17.hs +++ /dev/null @@ -1,112 +0,0 @@ -{-# LANGUAGE BlockArguments #-} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TemplateHaskell #-} - -{- -This is an implementation of the choreogrpahy shown in fig17 of We Know I Know You Know. --} - -module KVS5Fig17 where - -import CLI -import Choreography -import Choreography.Network.Http -import Data (TestArgs, reference) -import Data.List (sort) -import Data.Maybe (fromMaybe) -import System.Environment -import Test.QuickCheck (Arbitrary, arbitrary, elements) - -$(mkLoc "client") -$(mkLoc "primary") -$(mkLoc "backup") - -type Servers = ["primary", "backup"] - -type Participants = "client" ': Servers - -servers :: Subset Servers Participants -servers = primary @@ backup @@ nobody - -data Request = Put String String | Get String deriving (Eq, Show, Read) - -instance Arbitrary Request where - arbitrary = - ( \case - Nothing -> Get - Just s -> Put s - ) - <$> arbitrary - <*> arbitrary - -type Response = String - -data Args = Args - { request :: Request, - handler :: String - } - deriving (Eq, Show, Read) - -instance TestArgs Args Response where - reference Args {request, handler} = - let f = fromMaybe defaultHandler $ handler `lookup` handlers - in handleRequest f request - -instance Arbitrary Args where - arbitrary = - Args - <$> arbitrary - <*> elements (fst <$> handlers) - -handlers :: [(String, String -> String)] -handlers = - [ ("reverse", reverse), - ("alphabetize", sort) - ] - -defaultHandler :: String -> String -defaultHandler = const "No Handler" - --- | `handleRequest` handle a request. Since we don't have a way of locking paralell state, this is a mock. -handleRequest :: (String -> Response) -> Request -> Response -handleRequest handler request = case request of - Put key value -> show key ++ " saved as " ++ show value ++ "." - Get key -> handler key - -setup :: Choreo Servers (CLI m) (Located Servers (Request -> Response)) -setup = do - handlerName <- - (primary, getstr "How should we mock `Get` Requests? (reverse or alphabetize)") - -~> primary - @@ backup - @@ nobody - primary @@ backup @@ nobody `congruently` \un -> handleRequest (fromMaybe defaultHandler $ un refl handlerName `lookup` handlers) - --- | `kvs` is a choreography that processes a single request located at the client and returns the response. --- If the request is a `PUT`, it will forward the request to the backup node. -kvs :: Choreo Participants (CLI m) () -kvs = do - handler <- enclaveToAll servers setup - request <- (client, getInput "Enter the `read`able Request:") -~> primary @@ backup @@ nobody - response <- primary @@ backup @@ nobody `congruently` \un -> un refl handler $ un refl request - response' <- (primary, response) ~> client @@ nobody - client `locally_` \un -> putOutput "Recieved:" $ un client response' - -main :: IO () -main = do - [loc] <- getArgs - case loc of - "client" -> runCLIIO $ runChoreography config kvs "client" - "primary" -> runCLIIO $ runChoreography config kvs "primary" - "backup" -> runCLIIO $ runChoreography config kvs "backup" - _ -> error "unknown party" - return () - where - config = - mkHttpConfig - [ ("client", ("localhost", 3000)), - ("primary", ("localhost", 4000)), - ("backup", ("localhost", 5000)) - ] diff --git a/examples/KVS6SizePoly.hs b/examples/KVS6SizePoly.hs deleted file mode 100644 --- a/examples/KVS6SizePoly.hs +++ /dev/null @@ -1,198 +0,0 @@ -{-# LANGUAGE BlockArguments #-} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE ScopedTypeVariables #-} - -{- --} - -module KVS6SizePoly where - -import CLI -import Choreography -import Control.Monad.IO.Class (MonadIO, liftIO) -import Data.Foldable (toList) -import Data.IORef (IORef) -import Data.IORef qualified as IORef -import Data.List (nub) -import Data.Map (Map) -import Data.Map qualified as Map -import GHC.TypeLits (KnownSymbol) -import Test.QuickCheck (Arbitrary, arbitrary, frequency, listOf) -import Text.Read (readMaybe) - -readIORef :: (MonadIO m) => IORef a -> m a -readIORef = liftIO <$> IORef.readIORef - -modifyIORef :: (MonadIO m) => IORef a -> (a -> a) -> m a -modifyIORef ref f = do - a <- readIORef ref - liftIO $ IORef.modifyIORef ref f - return a - -newIORef :: (MonadIO m) => a -> m (IORef a) -newIORef = liftIO <$> IORef.newIORef - --- $(mkLoc "client") - --- $(mkLoc "primary") - --- $(mkLoc "backup1") - --- $(mkLoc "backup2") --- type Participants = ["client", "primary", "backup1", "backup2"] - -kvs :: (KnownSymbol client) => ReplicationStrategy ps (CLI m) -> Member client ps -> Choreo ps (CLI m) () -kvs ReplicationStrategy {setup, primary, handle} client = do - rigging <- setup - let go = do - request <- (client, readRequest) -~> primary @@ nobody - response <- handle rigging singleton request - case response of - Stopped -> return () - _ -> do - client `_locally_` putOutput "Recieved:" response - go - go - -naryReplicationStrategy :: - (KnownSymbol primary, KnownSymbols backups, KnownSymbols ps, MonadIO m) => - Member primary ps -> - Subset backups ps -> - ReplicationStrategy ps m -naryReplicationStrategy primary backups = - ReplicationStrategy - { primary, - setup = servers `_parallel` newIORef (Map.empty :: State), - handle = \stateRef pHas request -> do - request' <- (primary, (pHas, request)) ~> servers - localResponse <- - servers `parallel` \server un -> - handleRequest (viewFacet un server stateRef) (un server request') - responses <- gather servers (primary @@ nobody) localResponse - response <- - (primary @@ nobody) `congruently` \un -> - case nub (toList $ un refl responses) of - [r] -> r - rs -> Desynchronization rs - broadcast (primary, response) - } - where - servers = primary @@ backups - -data ReplicationStrategy ps m - = forall primary rigging. - (KnownSymbol primary) => - ReplicationStrategy - { primary :: Member primary ps, - setup :: Choreo ps m rigging, - handle :: - forall starts. - rigging -> - Member primary starts -> - Located starts Request -> - Choreo ps m Response - } - -data Request = Put String String | Get String | Stop deriving (Eq, Ord, Read, Show) - -data Response = Found String | NotFound | Stopped | Desynchronization [Response] - deriving (Eq, Ord, Read, Show) - --- | PUT returns the old stored value; GET returns whatever was stored. -handleRequest :: (MonadIO m) => IORef State -> Request -> m Response -handleRequest stateRef (Put key value) = mlookup key <$> modifyIORef stateRef (Map.insert key value) -handleRequest stateRef (Get key) = mlookup key <$> readIORef stateRef -handleRequest _ Stop = return Stopped - -mlookup :: String -> State -> Response -mlookup key = maybe NotFound Found . Map.lookup key - -type State = Map String String - -newtype Args = Args [Request] deriving (Eq, Ord, Read, Show) - -instance Arbitrary Args where - arbitrary = do - reqs <- pgs - return . Args $ reqs ++ [Stop] - where - pgs = - listOf $ - frequency - [ (1, Put <$> arbitrary <*> arbitrary), - (1, Get <$> arbitrary) - ] - -readRequest :: CLI m Request -readRequest = do - line <- getstr "Command?" - case line of - [] -> return Stop - _ -> case readMaybe line of - Just t -> return t - Nothing -> putNote "Invalid command" >> readRequest - --- | `nullReplicationStrategy` is a replication strategy that does not replicate the state. -nullReplicationStrategy :: - (KnownSymbol primary, KnownSymbols ps, MonadIO m) => - Member primary ps -> - ReplicationStrategy ps m -nullReplicationStrategy primary = - ReplicationStrategy - { primary, - setup = primary `_locally` newIORef (Map.empty :: State), - handle = \stateRef pHas request -> - ( (primary, \un -> handleRequest (un singleton stateRef) (un pHas request)) ~~> refl - ) - >>= naked refl - } - -naryHumans :: - (KnownSymbol primary, KnownSymbols backups, KnownSymbols ps, MonadIO m) => - Member primary ps -> - Subset backups ps -> - ReplicationStrategy ps (CLI m) -naryHumans primary backups = - ReplicationStrategy - { primary, - setup = primary `_locally` newIORef (Map.empty :: State), - handle = \stateRef pHas request -> do - request' <- (primary, (pHas, request)) ~> backups - backupResponse <- backups `parallel` \server un -> readResponse (un server request') - localResponse <- primary `locally` \un -> handleRequest (un singleton stateRef) (un pHas request) - responses <- gather backups (primary @@ nobody) backupResponse - response <- - (primary @@ nobody) `congruently` \un -> - case nub $ un refl localResponse : toList (un refl responses) of - [r] -> r - rs -> Desynchronization rs - ((primary, response) ~> refl) >>= naked refl - } - where - readResponse :: Request -> CLI m Response - readResponse r = do - line <- getstr $ show r ++ ": " - case line of - [] -> return NotFound - _ -> return $ Found line - -{-main :: IO () -main = do - [loc] <- getArgs - case loc of - "client" -> runChoreography config primaryBackupChoreo "client" - "primary" -> runChoreography config primaryBackupChoreo "primary" - "backup1" -> runChoreography config primaryBackupChoreo "backup1" - "backup2" -> runChoreography config primaryBackupChoreo "backup2" - _ -> error "unknown party" - return () - where - config = - mkHttpConfig - [ ("client", ("localhost", 3000)), - ("primary", ("localhost", 4000)), - ("backup1", ("localhost", 5000)), - ("backup2", ("localhost", 6000)) - ] - --} diff --git a/examples/KVS7SimplePoly.hs b/examples/KVS7SimplePoly.hs deleted file mode 100644 --- a/examples/KVS7SimplePoly.hs +++ /dev/null @@ -1,96 +0,0 @@ -{-# LANGUAGE BlockArguments #-} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE ScopedTypeVariables #-} - -module KVS7SimplePoly where - --- # This example was carried over from earlier work, likely HasChor. It doesn't yet have a unit test attached to it. - -import Choreography -import Data.IORef (IORef, newIORef, readIORef) - -type Response = Int - -type Key = String - -type State = String - -errorResponse :: Response -errorResponse = -1 - -data Request - = Get Key - | Put Key Int - deriving (Eq, Read, Show) - -handleGet :: IORef State -> Key -> IO Response -handleGet s k = do - readIORef s >>= putStrLn - return $ length k - -handlePut :: IORef State -> Key -> Int -> IO Response -handlePut s k v = do - readIORef s >>= putStrLn - return . fromEnum $ v /= length k - -isOk :: Response -> Bool -isOk = (== 0) - -handleRequest :: - forall backups. - (KnownSymbols backups) => - Located '["primary"] Request -> - (Located '["primary"] (IORef State), Faceted backups '[] (IORef State)) -> - Choreo ("primary" ': backups) IO (Located '["primary"] Response) -handleRequest request (primaryStateRef, backupsStateRefs) = - broadcast (primary, request) >>= \case - Put key value -> do - oks <- parallel backups \backup un -> - handlePut (viewFacet un backup backupsStateRefs) key value - gathered <- gather backups (primary @@ nobody) oks - locally primary \un -> - if all isOk (un primary gathered) - then handlePut (un primary primaryStateRef) key value - else return errorResponse - Get key -> locally primary \un -> handleGet (un primary primaryStateRef) key - where - primary :: forall ps. Member "primary" ("primary" ': ps) - primary = listedFirst - backups = consSuper refl - -kvs :: - forall backups. - (KnownSymbols backups) => - Located '["client"] Request -> - (Located '["primary"] (IORef State), Faceted backups '[] (IORef State)) -> - Choreo ("client" ': "primary" ': backups) IO (Located '["client"] Response) -kvs request stateRefs = do - request' <- (client, request) ~> primary @@ nobody - response <- enclave (primary @@ backups) (handleRequest request' stateRefs) - (primary, flatten (First @@ nobody) (First @@ nobody) response) ~> client @@ nobody - where - client :: forall ps. Member "client" ("client" ': ps) - primary :: forall ps p. Member "primary" (p ': "primary" ': ps) - client = listedFirst - primary = listedSecond - backups = consSuper $ consSuper refl - -mainChoreo :: (KnownSymbols backups) => Choreo ("client" ': "primary" ': backups) IO () -mainChoreo = do - stateRef <- primary `_locally` newIORef "I'm Primary" - bStRefs <- parallel backups \p _ -> newIORef ("I'm " ++ toLocTm p) - loop (stateRef, bStRefs) - where - primary :: forall ps p. Member "primary" (p ': "primary" ': ps) - primary = listedSecond - client :: forall ps. Member "client" ("client" ': ps) - client = listedFirst - backups = consSuper $ consSuper refl - loop state = do - request <- _locally client $ read @Request <$> getLine - response <- kvs request state - client `locally_` \un -> do putStrLn ("> " ++ show (un client response)) - loop state - -main :: IO () -main = runChoreo (mainChoreo @'["A", "B", "C", "D", "E", "F"]) diff --git a/examples/Karatsuba.hs b/examples/Karatsuba.hs deleted file mode 100644 --- a/examples/Karatsuba.hs +++ /dev/null @@ -1,129 +0,0 @@ -{-# LANGUAGE BlockArguments #-} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE TemplateHaskell #-} - -{- -# This example was carried over from earlier work, likely HasChor. It doesn't yet have a unit test attached to it. - -# Example: Karatsuba Fast Multiplication - -## Overview - -This example implements the three-way concurrent implementation of the Karatsuba fast multiplication algorithm shown in [Object-Oriented Choreographic Programming](https://arxiv.org/abs/2005.09520). - -## Execution - -The executable takes two integers as arguments and returns their product. It uses the local backend and distribute the computation over threads. - -```bash -cabal run karatsuba 100 200 -20000 -``` - -`Reference.h` contains a single-threaded reference implementation of the algorithm. --} - -module Karatsuba where - -import Choreography -import Choreography.Network.Local -import Control.Concurrent.Async (mapConcurrently_) -import GHC.TypeLits (KnownSymbol) -import System.Environment - -reference :: Integer -> Integer -> Integer -reference n1 n2 = - if n1 < 10 || n2 < 10 - then n1 * n2 - else result - where - log10 :: Integer -> Double - log10 = logBase 10 . fromIntegral - m = max (log10 n1) (log10 n2) + 1 - m2 :: Integer = floor (m / 2) - splitter = 10 ^ m2 - h1 = n1 `div` splitter - l1 = n1 `mod` splitter - h2 = n2 `div` splitter - l2 = n2 `mod` splitter - z0 = reference l1 l2 - z2 = reference h1 h2 - z1 = reference (l1 + h1) (l2 + h2) - z2 - z0 - result = z2 * splitter * splitter + z1 * splitter + z0 - -$(mkLoc "primary") -$(mkLoc "worker1") -$(mkLoc "worker2") - -type Participants = ["primary", "worker1", "worker2"] - -data KaratsubaNums = KaratsubaNums - { splitter :: Integer, - h1 :: Integer, - h2 :: Integer, - l1 :: Integer, - l2 :: Integer - } - -karatsuba :: - (KnownSymbol a, KnownSymbol b, KnownSymbol c) => - Member a Participants -> - Member b Participants -> - Member c Participants -> - Located '[a] Integer -> - Located '[a] Integer -> - Choreo Participants IO (Located '[a] Integer) -karatsuba a b c n1 n2 = do - done <- a `locally` \un -> return $ un singleton n1 < 10 || un singleton n2 < 10 - broadcast (a, done) - >>= \case - True -> do - a `locally` \un -> return $ un singleton n1 * un singleton n2 - False -> do - x <- a `locally` \un -> return $ f (un singleton n1) (un singleton n2) - l1' <- (a, \un -> return $ l1 (un singleton x)) ~~> b @@ nobody - l2' <- (a, \un -> return $ l2 (un singleton x)) ~~> b @@ nobody - h1' <- (a, \un -> return $ h1 (un singleton x)) ~~> c @@ nobody - h2' <- (a, \un -> return $ h2 (un singleton x)) ~~> c @@ nobody - z0' <- karatsuba b c a l1' l2' - z0 <- (b, z0') ~> a @@ nobody - z2' <- karatsuba c a b h1' h2' - z2 <- (c, z2') ~> a @@ nobody - s1 <- a `locally` \un -> return $ l1 (un singleton x) + h1 (un singleton x) - s2 <- a `locally` \un -> return $ l2 (un singleton x) + h2 (un singleton x) - z1' <- karatsuba a b c s1 s2 - z1 <- a `locally` \un -> return $ un singleton z1' - un singleton z2 - un singleton z0 - a `locally` \un -> - return - let s = splitter (un singleton x) - in (un singleton z2 * s * s) + (un singleton z1 * s) + un singleton z0 - where - f n1' n2' = KaratsubaNums {splitter = splitter, h1 = h1, l1 = l1, h2 = h2, l2 = l2} - where - log10 :: Integer -> Double - log10 = logBase 10 . fromIntegral - m = max (log10 n1') (log10 n2') + 1 - m2 :: Integer = floor (m / 2) - splitter = 10 ^ m2 - h1 = n1' `div` splitter - l1 = n1' `mod` splitter - h2 = n2' `div` splitter - l2 = n2' `mod` splitter - -mainChoreo :: Integer -> Integer -> Choreo Participants IO () -mainChoreo n1' n2' = do - n1 <- primary `_locally` pure n1' - n2 <- primary `_locally` pure n2' - result <- karatsuba primary worker1 worker2 n1 n2 - primary `locally_` \un -> do - print (un primary result) - -main :: IO () -main = do - [n1, n2] <- map read <$> getArgs - config <- mkLocalConfig locations - mapConcurrently_ (runChoreography config (mainChoreo n1 n2)) locations - return () - where - locations = ["primary", "worker1", "worker2"] diff --git a/examples/Lottery.hs b/examples/Lottery.hs deleted file mode 100644 --- a/examples/Lottery.hs +++ /dev/null @@ -1,156 +0,0 @@ -{-# LANGUAGE BlockArguments #-} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE TemplateHaskell #-} -{-# LANGUAGE TypeFamilies #-} - -module Lottery where - -import CLI -import Choreography -import Choreography.Network.Http -import Control.Exception (Exception, throwIO) -import Control.Monad (unless) -import Control.Monad.IO.Class (MonadIO (liftIO)) -import Crypto.Hash (Digest) -import Crypto.Hash qualified as Crypto -import Data (TestArgs, reference) -import Data.Bifunctor (first) -import Data.Binary qualified as Binary -import Data.ByteString (toStrict) -import Data.FiniteField (primeField) -import Data.Foldable (toList) -import GHC.TypeLits (KnownSymbol) -import System.Environment (getArgs) -import System.Random (Random, random, randomIO, randomR, randomRIO) -import Test.QuickCheck (Arbitrary, arbitrary, arbitraryBoundedEnum) - --- | Arbitrary "large" prime -newtype Fp = Fp $(primeField 999983) -- AFAICT the hint warning needs a newer version of hlint to go away: - deriving (Bounded, Enum, Eq, Ord, Num) -- https://github.com/ndmitchell/hlint/issues/1226 - -instance Read Fp where - readsPrec _ s = [(Fp (read s), "")] - -instance Show Fp where - show (Fp x) = show x - -instance Random Fp where - random g = toEnum `first` randomR (fromEnum @Fp minBound, fromEnum @Fp maxBound) g - randomR (l, h) g = toEnum `first` randomR (fromEnum l, fromEnum h) g - -instance Arbitrary Fp where - arbitrary = arbitraryBoundedEnum - -data LotteryError = CommitmentCheckFailed deriving (Show) - -instance Exception LotteryError - -data Args = Args - { secrets :: (Fp, Fp, Fp, Fp, Fp), -- we lock our test to the case of five clients and three servers - randomIs :: (Int, Int, Int) - } - deriving (Eq, Show, Read) - -instance TestArgs Args Fp where - reference Args {secrets = (c1, c2, c3, c4, c5), randomIs = (s1, s2, s3)} = - let i = (s1 + s2 + s3) `mod` 5 - in [c1, c2, c3, c4, c5] !! i - -instance Arbitrary Args where - arbitrary = - Args - <$> ((,,,,) <$> arbitrary <*> arbitrary <*> arbitrary <*> arbitrary <*> arbitrary) - <*> ((,,) <$> arbitrary <*> arbitrary <*> arbitrary) - --- | Federated Lottery example from DPrio https://www.semanticscholar.org/paper/DPrio%3A-Efficient-Differential-Privacy-with-High-for-Keeler-Komlo/ae1b2a4e5beaaa850183ad37e0880bb70ae34f4e -lottery :: - forall clients servers analyst census m _serv1 _serv2 _servTail _client1 _client2 _clientTail. - ( KnownSymbols clients, - KnownSymbols servers, - KnownSymbol analyst, - MonadIO m, - (_serv1 ': _serv2 ': _servTail) ~ servers, -- There must be at least be two servers - (_client1 ': _client2 ': _clientTail) ~ clients -- There must be at least be two clients - ) => - Subset clients census -> - Subset servers census -> - Member analyst census -> - Choreo census (CLI m) () -lottery clients servers analyst = do - secret <- _parallel clients (getInput @Fp "secret:") - clientShares <- - clients `parallel` \client un -> - ( case tySpine @servers of - TyCons -> do - -- I guess this explains to GHC that we have KnownSymbols _servTail? IDK - freeShares <- liftIO $ sequence $ pure $ randomIO @Fp - return $ (viewFacet un client secret - sum freeShares) `qCons` freeShares - ) - serverShares <- - fanOut - ( \server -> - -- Probably I've already got a nicer way to write this on hand; idk. - fanIn - (inSuper servers server @@ nobody) - ( \client -> do - serverShare <- - inSuper clients client `locally` \un -> - pure $ viewFacet un client clientShares `getLeaf` server - (inSuper clients client, serverShare) ~> inSuper servers server @@ nobody - ) - ) - -- 1) Each server selects a random number; τ is some multiple of the number of clients. - ρ <- _parallel servers (getInput "A random number from 1 to τ:") - -- Salt value - ψ <- _parallel servers (randomRIO (2 ^ (18 :: Int), 2 ^ (20 :: Int))) - -- 2) Each server computes and publishes the hash α = H(ρ, ψ) to serve as a commitment - α <- parallel servers \server un -> pure $ hash (viewFacet un server ψ) (viewFacet un server ρ) - α' <- gather servers servers α - -- 3) Every server opens their commitments by publishing their ψ and ρ to each other - ψ' <- gather servers servers ψ - ρ' <- gather servers servers ρ - -- 4) All servers verify each other's commitment by checking α = H(ρ, ψ) - parallel_ - servers - ( \server un -> - unless - (un server α' == (hash <$> un server ψ' <*> un server ρ')) - (liftIO $ throwIO CommitmentCheckFailed) - ) - -- 5) If all the checks are successful, then sum random values to get the random index. - ω <- servers `congruently` (\un -> sum (un refl ρ') `mod` length (toLocs clients)) - chosenShares <- servers `parallel` (\server un -> pure $ toList (viewFacet un server serverShares) !! un server ω) - -- Servers forward shares to an analyist. - allShares <- gather servers (analyst @@ nobody) chosenShares - analyst `locally_` \un -> putOutput "The answer is:" $ sum $ un singleton allShares - where - hash :: Int -> Int -> Digest Crypto.SHA256 - hash ρ ψ = Crypto.hash $ toStrict (Binary.encode ρ <> Binary.encode ψ) - -main :: IO () -main = do - [loc] <- getArgs - let clientProof :: Subset '["client1", "client2"] '["client1", "client2", "server1", "server2", "analyst"] - clientProof = explicitSubset - serverProof :: Subset '["server1", "server2"] '["client1", "client2", "server1", "server2", "analyst"] - serverProof = explicitSubset - analystProof :: Member "analyst" '["client1", "client2", "server1", "server2", "analyst"] - analystProof = explicitMember - _ <- case loc of - "client1" -> runCLIIO $ runChoreography config (lottery clientProof serverProof analystProof) "client1" - "client2" -> runCLIIO $ runChoreography config (lottery clientProof serverProof analystProof) "client2" - "server1" -> runCLIIO $ runChoreography config (lottery clientProof serverProof analystProof) "server1" - "server2" -> runCLIIO $ runChoreography config (lottery clientProof serverProof analystProof) "server2" - "analyst" -> runCLIIO $ runChoreography config (lottery clientProof serverProof analystProof) "analyst" - _ -> error "unknown party" - return () - where - config = - mkHttpConfig - [ ("client1", ("localhost", 5000)), - ("client2", ("localhost", 5001)), - ("server1", ("localhost", 5002)), - ("server2", ("localhost", 5003)), - ("analyst", ("localhost", 5004)) - ] diff --git a/examples/MPCFake.hs b/examples/MPCFake.hs deleted file mode 100644 --- a/examples/MPCFake.hs +++ /dev/null @@ -1,145 +0,0 @@ -{-# LANGUAGE BlockArguments #-} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TemplateHaskell #-} - -module MPCFake where - -import CLI -import Choreography -import Control.Monad.IO.Class (MonadIO, liftIO) -import Data (TestArgs, reference) -import Data.Kind (Type) -import Data.Maybe (fromJust) -import GHC.TypeLits (KnownSymbol) -import System.Random -import Test.QuickCheck (Arbitrary, arbitrary, chooseInt, elements, getSize, oneof, resize) - -$(mkLoc "trusted3rdParty") -$(mkLoc "p1") -$(mkLoc "p2") -$(mkLoc "p3") -$(mkLoc "p4") - -xor :: (Foldable f) => f Bool -> Bool -xor = foldr1 (/=) - -data Circuit :: [LocTy] -> Type where - InputWire :: (KnownSymbol p) => Member p ps -> Circuit ps - LitWire :: Bool -> Circuit ps - AndGate :: Circuit ps -> Circuit ps -> Circuit ps - XorGate :: Circuit ps -> Circuit ps -> Circuit ps - -instance Show (Circuit ps) where - show (InputWire p) = "InputWire<" ++ toLocTm p ++ ">" - show (LitWire b) = "LitWire " ++ show b - show (AndGate left right) = "(" ++ show left ++ ") AND (" ++ show right ++ ")" - show (XorGate left right) = "(" ++ show left ++ ") XOR (" ++ show right ++ ")" - -instance Arbitrary (Circuit '["p1", "p2", "p3", "p4"]) where - arbitrary = do - size <- getSize - if 1 >= size - then oneof $ (LitWire <$> arbitrary) : (return <$> [InputWire p1, InputWire p2, InputWire p3, InputWire p4]) - else do - left <- chooseInt (1, size) - a <- resize left arbitrary - b <- resize (1 `max` (size - left)) arbitrary - op <- elements [AndGate, XorGate] - return $ a `op` b - -data Args = Args - { circuit :: Circuit '["p1", "p2", "p3", "p4"], - p1in :: Bool, -- These should be lists, but consuming them would be a chore... - p2in :: Bool, - p3in :: Bool, - p4in :: Bool - } - deriving (Show) - -instance Arbitrary Args where - arbitrary = Args <$> arbitrary <*> arbitrary <*> arbitrary <*> arbitrary <*> arbitrary - -instance TestArgs Args (Bool, Bool, Bool, Bool) where - reference Args {circuit, p1in, p2in, p3in, p4in} = (answer, answer, answer, answer) - where - recurse c = case c of - InputWire p -> fromJust $ toLocTm p `lookup` inputs - LitWire b -> b - AndGate left right -> recurse left && recurse right - XorGate left right -> recurse left /= recurse right - inputs = ["p1", "p2", "p3", "p4"] `zip` [p1in, p2in, p3in, p4in] - answer = recurse circuit - -secretShare :: - forall p parties owners ps m. - (KnownSymbols parties, KnownSymbol p, MonadIO m) => - Subset parties ps -> - Member p ps -> - (Member p owners, Located owners Bool) -> - Choreo ps m (Faceted parties '[] Bool) -secretShare parties p (ownership, value) = do - shares <- p `locally` \un -> genShares (un ownership value) - PIndexed fs <- scatter p parties shares - return $ PIndexed $ Facet . othersForget (First @@ nobody) . getFacet . fs - where - genShares x = case tySpine @parties of - TyCons -> gs' - TyNil -> error "Can't secret-share to zero people." - where - gs' :: forall q qs. (KnownSymbol q, KnownSymbols qs) => m (Quire (q ': qs) Bool) - gs' = do - freeShares <- sequence $ pure $ liftIO randomIO -- generate n-1 random shares - return $ xor (qCons @q x freeShares) `qCons` freeShares - -reveal :: - forall ps m. - (KnownSymbols ps) => - Faceted ps '[] Bool -> - Choreo ps m Bool -reveal shares = do - let ps = allOf @ps - allShares <- gather ps ps shares - value <- ps `congruently` \un -> xor $ un ps allShares - naked ps value - -computeWire :: - (KnownSymbols ps, KnownSymbols parties, KnownSymbol trustedAnd, MonadIO m) => - Member trustedAnd ps -> - Subset parties ps -> - Circuit parties -> - Choreo ps (CLI m) (Faceted parties '[] Bool) -computeWire trustedAnd parties circuit = case circuit of - InputWire p -> do - value <- inSuper parties p `_locally` getInput "Enter a secret input value:" - secretShare parties (inSuper parties p) (singleton, value) - LitWire b -> do - let shares = partyNames `zip` (b : repeat False) - fanOut \p -> inSuper parties p `_locally` return (fromJust $ toLocTm p `lookup` shares) - AndGate l r -> do - lResult <- compute l - rResult <- compute r - inputShares <- fanIn (trustedAnd @@ nobody) \p -> do - (inSuper parties p, \un -> return (viewFacet un p lResult, viewFacet un p rResult)) ~~> trustedAnd @@ nobody - outputVal <- - (trustedAnd @@ nobody) `congruently` \un -> - let ovs = un refl inputShares - in xor (fst <$> ovs) && xor (snd <$> ovs) - secretShare parties trustedAnd (singleton, outputVal) - XorGate l r -> do - lResult <- compute l - rResult <- compute r - parties `parallel` \p un -> pure (viewFacet un p lResult /= viewFacet un p rResult) - where - compute = computeWire trustedAnd parties - partyNames = toLocs parties - -mpc :: - (KnownSymbols parties, MonadIO m) => - Circuit parties -> - Choreo ("trusted3rdParty" ': parties) (CLI m) () -mpc circuit = do - let parties = consSuper refl - outputWire <- computeWire trusted3rdParty parties circuit - result <- enclave parties $ reveal outputWire - parties `parallel_` \p un -> putOutput "The resulting bit:" $ un p result diff --git a/examples/MergeSort.hs b/examples/MergeSort.hs deleted file mode 100644 --- a/examples/MergeSort.hs +++ /dev/null @@ -1,141 +0,0 @@ -{-# LANGUAGE BlockArguments #-} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE TemplateHaskell #-} - -{- -# This example was carried over from earlier work, likely HasChor. It doesn't yet have a unit test attached to it. - -# Example: merge sort - -## Overview - -This example implements the three-way concurrent implementation of merge sort shown in [Object-Oriented Choreographic Programming](https://arxiv.org/abs/2005.09520). - -## Execution - -This choreography will sort the list `[1, 6, 5, 3, 4, 2, 7, 8]`. It requires three locations: `primary`, `worker1`, and `worker2`. - -```bash -# start two workers on separate terminals -cabal run mergesort worker1 -cabal run mergesort worker2 -# start primary on another terminal -cabal run mergesort primary -[1,2,3,4,5,6,7,8] -``` --} - -module MergeSort where - -import Choreography -import Choreography.Network.Http -import GHC.TypeLits (KnownSymbol) -import System.Environment - -divide :: [a] -> ([a], [a]) -divide xs = splitAt lhx xs - where - lhx = length xs `div` 2 - -$(mkLoc "primary") -$(mkLoc "worker1") -$(mkLoc "worker2") - -type Participants = ["primary", "worker1", "worker2"] - -sort :: - ( KnownSymbol a, - KnownSymbol c, - KnownSymbol b, - KnownSymbols ps - ) => - Member a ps -> - Member b ps -> - Member c ps -> - Located '[a] [Int] -> - Choreo ps IO (Located '[a] [Int]) -sort a b c lst = do - condition <- a `locally` \un -> do return $ length (un singleton lst) > 1 - broadcast (a, condition) >>= \case - True -> do - _ <- a `locally` \un -> do return $ length (un singleton lst) `div` 2 - divided <- a `locally` \un -> do return $ divide (un singleton lst) - l <- a `locally` \un -> do return $ fst (un singleton divided) - r <- a `locally` \un -> do return $ snd (un singleton divided) - l' <- (a, l) ~> b @@ nobody - r' <- (a, r) ~> c @@ nobody - ls' <- sort b c a l' - rs' <- sort c a b r' - merge a b c ls' rs' - False -> do - return lst - -merge :: - ( KnownSymbol a, - KnownSymbol c, - KnownSymbol b, - KnownSymbols ps - ) => - Member a ps -> - Member b ps -> - Member c ps -> - Located '[b] [Int] -> - Located '[c] [Int] -> - Choreo ps IO (Located '[a] [Int]) -merge a b c lhs rhs = do - lhsHasElements <- b `locally` \un -> do return $ not (null (un singleton lhs)) - broadcast (b, lhsHasElements) >>= \case - True -> do - rhsHasElements <- c `locally` \un -> do return $ not (null (un singleton rhs)) - broadcast (c, rhsHasElements) >>= \case - True -> do - rhsHeadAtC <- c `locally` \un -> do return $ head (un singleton rhs) - rhsHeadAtB <- (c, rhsHeadAtC) ~> b @@ nobody - takeLhs <- b `locally` \un -> do return $ head (un singleton lhs) <= un singleton rhsHeadAtB - broadcast (b, takeLhs) >>= \case - True -> do - -- take (head lhs) and merge the rest - lhs' <- b `locally` \un -> do return $ tail (un singleton lhs) - merged <- merge a b c lhs' rhs - lhsHeadAtB <- b `locally` \un -> do return $ head (un singleton lhs) - lhsHeadAtA <- (b, lhsHeadAtB) ~> a @@ nobody - a `locally` \un -> do return $ un singleton lhsHeadAtA : un singleton merged - False -> do - -- take (head rhs) and merge the rest - rhs' <- c `locally` \un -> do return $ tail (un singleton rhs) - merged <- merge a b c lhs rhs' - rhsHeadAtC' <- c `locally` \un -> do return $ head (un singleton rhs) - rhsHeadAtA <- (c, rhsHeadAtC') ~> a @@ nobody - a `locally` \un -> do return $ un singleton rhsHeadAtA : un singleton merged - False -> do - (b, lhs) ~> a @@ nobody - False -> do - (c, rhs) ~> a @@ nobody - -mainChoreo :: Choreo Participants IO () -mainChoreo = do - lst <- primary `_locally` return [1, 6, 5, 3, 4, 2, 7, 8] - sorted <- sort primary worker1 worker2 lst - _ <- - primary `locally` \un -> do - print (un primary sorted) - return () - return () - -main :: IO () -main = do - [loc] <- getArgs - case loc of - "primary" -> runChoreography config mainChoreo "primary" - "worker1" -> runChoreography config mainChoreo "worker1" - "worker2" -> runChoreography config mainChoreo "worker2" - _ -> error "unknown worker" - return () - where - config = - mkHttpConfig - [ ("primary", ("localhost", 3000)), - ("worker1", ("localhost", 4000)), - ("worker2", ("localhost", 5000)) - ] diff --git a/examples/ObliviousTransfer.hs b/examples/ObliviousTransfer.hs deleted file mode 100644 --- a/examples/ObliviousTransfer.hs +++ /dev/null @@ -1,279 +0,0 @@ -{-# LANGUAGE BlockArguments #-} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE TemplateHaskell #-} - -module ObliviousTransfer (ot2, ot4, main) where - -import CLI -import Choreography -import Choreography.Network.Http -import Control.Monad.IO.Class (MonadIO (liftIO)) --- For cryptonite - -import Crypto.Hash.Algorithms qualified as HASH -import Crypto.PubKey.RSA qualified as RSA -import Crypto.PubKey.RSA.OAEP qualified as OAEP -import Crypto.Random.Types qualified as CRT -import Data.Bits (shiftL) -import Data.ByteString qualified as BS -import Data.ByteString.Char8 (ByteString, pack) -import GHC.TypeLits (KnownSymbol) -import System.Environment - --- Helpers for RSA encryption -genKeyPair :: (CRT.MonadRandom m) => m (RSA.PublicKey, RSA.PrivateKey) -genKeyPair = RSA.generate 64 65537 - -encryptRSA :: (CRT.MonadRandom m) => RSA.PublicKey -> Bool -> m ByteString -encryptRSA p a = do - let bs = boolToByteString a - x <- OAEP.encrypt (OAEP.defaultOAEPParams HASH.SHA1) p bs - case x of - Left _ -> undefined - Right b -> return b - -decryptRSA :: (CRT.MonadRandom m) => RSA.PrivateKey -> ByteString -> m Bool -decryptRSA r bs = do - x <- OAEP.decryptSafer (OAEP.defaultOAEPParams HASH.SHA1) r bs - case x of - Left _ -> undefined - Right b -> return $ byteStringToBool b - -boolToByteString :: Bool -> BS.StrictByteString -boolToByteString = pack . show - -byteStringToBool :: BS.StrictByteString -> Bool -byteStringToBool bs - | bs == pack (show True) = True - | bs == pack (show False) = False - | otherwise = undefined - -generateFakePK :: (CRT.MonadRandom m) => m RSA.PublicKey -generateFakePK = do - bytes <- CRT.getRandomBytes 64 - return $ RSA.PublicKey 64 (bytesToInteger bytes) 65537 - where - bytesToInteger bs = foldl (\acc byte -> (acc `shiftL` 8) + fromIntegral byte) 0 (BS.unpack bs) - --------------------------------------------------- --- 1-out-of-2 Oblivious transfer --------------------------------------------------- -ot2Insecure :: - forall sender receiver m. - (KnownSymbol sender, KnownSymbol receiver, MonadIO m) => - Located '[sender] Bool -> - Located '[sender] Bool -> - Located '[receiver] Bool -> - Choreo '[sender, receiver] (CLI m) (Located '[receiver] Bool) -ot2Insecure b1 b2 s = do - let sender = listedFirst :: Member sender '[sender, receiver] - let receiver = listedSecond :: Member receiver '[sender, receiver] - sr <- (receiver, s) ~> sender @@ nobody - (sender, \un -> return $ un singleton $ if un singleton sr then b1 else b2) ~~> receiver @@ nobody - -genKeys :: (CRT.MonadRandom m) => Bool -> m (RSA.PublicKey, RSA.PublicKey, RSA.PrivateKey) -genKeys s = do - -- Generate keys for OT. One key is real, and one is fake - select bit decides - (pk, sk) <- genKeyPair - fakePk <- generateFakePK - return $ if s then (pk, fakePk, sk) else (fakePk, pk, sk) - -encryptS :: - (CRT.MonadRandom m) => -- Encryption based on select bit - (RSA.PublicKey, RSA.PublicKey) -> - Bool -> - Bool -> - m (ByteString, ByteString) -encryptS (pk1, pk2) b1 b2 = do c1 <- encryptRSA pk1 b1; c2 <- encryptRSA pk2 b2; return (c1, c2) - -decryptS :: - (CRT.MonadRandom m) => -- Decryption based on select bit - (RSA.PublicKey, RSA.PublicKey, RSA.PrivateKey) -> - Bool -> - (ByteString, ByteString) -> - m Bool -decryptS (_, _, sk) s (c1, c2) = if s then decryptRSA sk c1 else decryptRSA sk c2 - --- One out of two OT -ot2 :: - (KnownSymbol sender, KnownSymbol receiver, MonadIO m, CRT.MonadRandom m) => - Located '[sender] (Bool, Bool) -> - Located '[receiver] Bool -> - Choreo '[sender, receiver] (CLI m) (Located '[receiver] Bool) -ot2 bb s = do - let sender = listedFirst :: Member sender '[sender, receiver] - let receiver = listedSecond :: Member receiver '[sender, receiver] - - keys <- locally receiver \un -> liftIO $ genKeys $ un singleton s - pks <- - ( receiver, - \un -> - let (pk1, pk2, _) = un singleton keys - in return (pk1, pk2) - ) - ~~> sender - @@ nobody - encrypted <- - ( sender, - \un -> - let (b1, b2) = un singleton bb - in liftIO $ encryptS (un singleton pks) b1 b2 - ) - ~~> receiver - @@ nobody - locally receiver \un -> - liftIO $ - decryptS - (un singleton keys) - (un singleton s) - (un singleton encrypted) - --------------------------------------------------- --- 1-out-of-4 Oblivious transfer --------------------------------------------------- - -select4 :: Bool -> Bool -> a -> a -> a -> a -> a -select4 s1 s2 v1 v2 v3 v4 = case (s1, s2) of - (True, True) -> v1 - (True, False) -> v2 - (False, True) -> v3 - (False, False) -> v4 - -ot4Insecure :: - forall sender receiver m. - (KnownSymbol sender, KnownSymbol receiver, MonadIO m) => - Located '[sender] Bool -> -- sender - Located '[sender] Bool -> -- sender - Located '[sender] Bool -> -- sender - Located '[sender] Bool -> -- sender - Located '[receiver] Bool -> -- receiver - Located '[receiver] Bool -> -- receiver - Choreo '[sender, receiver] (CLI m) (Located '[receiver] Bool) -ot4Insecure b1 b2 b3 b4 s1 s2 = do - let sender = listedFirst :: Member sender '[sender, receiver] - let receiver = listedSecond :: Member receiver '[sender, receiver] - - s1r <- (receiver, s1) ~> sender @@ nobody - s2r <- (receiver, s2) ~> sender @@ nobody - (sender, \un -> return $ un singleton $ select4 (un singleton s1r) (un singleton s2r) b1 b2 b3 b4) ~~> receiver @@ nobody - --- Generate keys for OT, only one has a SK and the rest are fake -genKeys4 :: - (CRT.MonadRandom m) => - Bool -> - Bool -> - m (RSA.PublicKey, RSA.PublicKey, RSA.PublicKey, RSA.PublicKey, RSA.PrivateKey) -genKeys4 s1 s2 = do - (pk, sk) <- genKeyPair - fakePk1 <- generateFakePK - fakePk2 <- generateFakePK - fakePk3 <- generateFakePK - return $ case (s1, s2) of - (True, True) -> (pk, fakePk1, fakePk2, fakePk3, sk) - (True, False) -> (fakePk1, pk, fakePk2, fakePk3, sk) - (False, True) -> (fakePk1, fakePk2, pk, fakePk3, sk) - (False, False) -> (fakePk1, fakePk2, fakePk3, pk, sk) - --- Encryption based on select bit -enc4 :: - (CRT.MonadRandom m) => - (RSA.PublicKey, RSA.PublicKey, RSA.PublicKey, RSA.PublicKey) -> - Bool -> - Bool -> - Bool -> - Bool -> - m (ByteString, ByteString, ByteString, ByteString) -enc4 (pk1, pk2, pk3, pk4) b1 b2 b3 b4 = do - c1 <- encryptRSA pk1 b1 - c2 <- encryptRSA pk2 b2 - c3 <- encryptRSA pk3 b3 - c4 <- encryptRSA pk4 b4 - return (c1, c2, c3, c4) - --- Decryption based on select bit -dec4 :: - (CRT.MonadRandom m) => - (RSA.PublicKey, RSA.PublicKey, RSA.PublicKey, RSA.PublicKey, RSA.PrivateKey) -> - Bool -> - Bool -> - (ByteString, ByteString, ByteString, ByteString) -> - m Bool -dec4 (_, _, _, _, sk) s1 s2 (c1, c2, c3, c4) = decryptRSA sk $ select4 s1 s2 c1 c2 c3 c4 - --- One out of two OT -ot4 :: - (KnownSymbol sender, KnownSymbol receiver, MonadIO m, CRT.MonadRandom m) => - Located '[sender] Bool -> - Located '[sender] Bool -> - Located '[sender] Bool -> - Located '[sender] Bool -> - Located '[receiver] Bool -> - Located '[receiver] Bool -> - Choreo '[sender, receiver] (CLI m) (Located '[receiver] Bool) -ot4 b1 b2 b3 b4 s1 s2 = do - let sender = listedFirst :: Member sender '[sender, receiver] - let receiver = listedSecond :: Member receiver '[sender, receiver] - - keys <- receiver `locally` \un -> (liftIO $ genKeys4 (un singleton s1) (un singleton s2)) - pks <- (receiver, \un -> let (pk1, pk2, pk3, pk4, _) = (un singleton keys) in return (pk1, pk2, pk3, pk4)) ~~> sender @@ nobody - encrypted <- - ( sender, - \un -> - liftIO $ - enc4 - (un singleton pks) - (un singleton b1) - (un singleton b2) - (un singleton b3) - (un singleton b4) - ) - ~~> receiver - @@ nobody - decrypted <- - receiver `locally` \un -> - liftIO $ - dec4 - (un singleton keys) - (un singleton s1) - (un singleton s2) - (un singleton encrypted) - return decrypted - --- Test function -otTest :: (KnownSymbol p1, KnownSymbol p2, MonadIO m, CRT.MonadRandom m) => Choreo '[p1, p2] (CLI m) () -otTest = do - let p1 = listedFirst :: Member p1 '[p1, p2] - let p2 = listedSecond :: Member p2 '[p1, p2] - bb <- p1 `_locally` return (False, True) - b1 <- p1 `locally` \un -> pure . fst $ un singleton bb - b2 <- p1 `locally` \un -> pure . snd $ un singleton bb - s <- p2 `_locally` return False - otResultI <- ot2Insecure b1 b2 s - p2 `locally_` \un -> putOutput "OT2 insecure output:" $ un singleton otResultI - otResult <- ot2 bb s - p2 `locally_` \un -> putOutput "OT2 output:" $ un singleton otResult - - b3 <- p1 `_locally` return False - b4 <- p1 `_locally` return True - s2 <- p2 `_locally` return False - otResultI4 <- ot4Insecure b1 b2 b3 b4 s s2 - p2 `locally_` \un -> putOutput "OT4 insecure output:" $ un singleton otResultI4 - otResult4 <- ot4 b1 b2 b3 b4 s s2 - p2 `locally_` \un -> putOutput "OT4 output:" $ un singleton otResult4 - -main :: IO () -main = do - [loc] <- getArgs - delivery <- case loc of - "client1" -> runCLIIO $ runChoreography cfg (otTest @"client1" @"client2") "client1" - "client2" -> runCLIIO $ runChoreography cfg (otTest @"client1" @"client2") "client2" - _ -> error "unknown party" - print delivery - where - cfg = - mkHttpConfig - [ ("client1", ("localhost", 4242)), - ("client2", ("localhost", 4343)) - ] diff --git a/examples/QuickSort.hs b/examples/QuickSort.hs deleted file mode 100644 --- a/examples/QuickSort.hs +++ /dev/null @@ -1,83 +0,0 @@ -{-# LANGUAGE BlockArguments #-} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE TemplateHaskell #-} - -{- -# This example was carried over from earlier work, likely HasChor. It doesn't yet have a unit test attached to it. - -# Example: Quicksort - -## Overview - -This example implements the three-way concurrent implementation of quicksort. - -## Execution - -This choreography will sort the list `[1, 6, 5, 3, 4, 2, 7, 8]`. It uses the local backend and distribute the computation over threads. - -```bash -cabal run quicksort -[1,2,3,4,5,6,7,8] -``` - -`Reference.hs` contains a single-threaded reference implementation of the algorithm. --} - -module QuickSort where - -import Choreography -import Choreography.Network.Local -import Control.Concurrent.Async (mapConcurrently_) -import GHC.TypeLits (KnownSymbol) - -reference :: [Int] -> [Int] -reference [] = [] -reference (x : xs) = smaller ++ [x] ++ bigger - where - smaller = reference [a | a <- xs, a <= x] - bigger = reference [a | a <- xs, a > x] - -$(mkLoc "primary") -$(mkLoc "worker1") -$(mkLoc "worker2") - -type Participants = ["primary", "worker1", "worker2"] - -quicksort :: - (KnownSymbol a, KnownSymbol b, KnownSymbol c, KnownSymbols ps) => - Member a ps -> - Member b ps -> - Member c ps -> - Located '[a] [Int] -> - Choreo ps IO (Located '[a] [Int]) -quicksort a b c lst = do - isEmpty <- a `locally` \un -> pure (null (un singleton lst)) - broadcast (a, isEmpty) >>= \case - True -> do - a `_locally` pure [] - False -> do - smaller <- (a, \un -> let x : xs = un singleton lst in pure [i | i <- xs, i <= x]) ~~> b @@ nobody - smaller' <- quicksort b c a smaller - smaller'' <- (b, smaller') ~> a @@ nobody - bigger <- (a, \un -> let x : xs = un singleton lst in pure [i | i <- xs, i > x]) ~~> c @@ nobody - bigger' <- quicksort c a b bigger - bigger'' <- (c, bigger') ~> a @@ nobody - a `locally` \un -> pure $ un singleton smaller'' ++ [head (un singleton lst)] ++ un singleton bigger'' - -mainChoreo :: Choreo Participants IO () -mainChoreo = do - lst <- primary `_locally` return [1, 6, 5, 3, 4, 2, 7, 8] - sorted <- quicksort primary worker1 worker2 lst - primary `locally_` \un -> do - print (un primary sorted) - return () - return () - -main :: IO () -main = do - config <- mkLocalConfig locations - mapConcurrently_ (runChoreography config mainChoreo) locations - return () - where - locations = ["primary", "worker1", "worker2"] diff --git a/examples/RingLeader.hs b/examples/RingLeader.hs deleted file mode 100644 --- a/examples/RingLeader.hs +++ /dev/null @@ -1,93 +0,0 @@ -{-# LANGUAGE BlockArguments #-} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE TemplateHaskell #-} - -{- -# This example was carried over from earlier work, likely HasChor. It doesn't yet have a unit test attached to it. - -# Ring leader election - -Experinmental implementaion of ring leader election. --} - -module RingLeader where - -import Choreography -import Choreography.Network.Http -import Control.Monad.Trans.Class -import Control.Monad.Trans.State -import GHC.TypeLits (KnownSymbol) -import System.Environment - --- an edge of the ring is represented as a tuple of two locaitons l and l' where --- l is on the left of l' -data Edge g - = forall l l'. - (KnownSymbol l, KnownSymbol l') => - Edge (Member l g) (Member l' g) - --- a ring is a sequence of edges -type Ring g = [Edge g] - -type Label = Int - -ringLeader :: forall g. (KnownSymbols g) => Ring g -> Choreo g (StateT Label IO) () -- g for graph -ringLeader r = loop r - where - loop :: Ring g -> Choreo g (StateT Label IO) () - loop [] = loop r -- not very safe! - loop (x : xs) = do - finished <- talkToRight x - if finished - then return () - else loop xs - - talkToRight :: Edge g -> Choreo g (StateT Label IO) Bool - talkToRight (Edge left right) = do - ll <- left `_locally` get - labelLeft <- (left, ll) ~> right @@ nobody - labelRight <- right `_locally` get - - finished <- - right `locally` \un -> - return $ un singleton labelLeft == un singleton labelRight - - broadcast (right, finished) >>= \case - True -> do - right `_locally_` lift (putStrLn "I'm the leader") - return True - False -> do - right `locally_` \un -> put (max (un singleton labelLeft) (un singleton labelRight)) - return False - -$(mkLoc "nodeA") -$(mkLoc "nodeB") -$(mkLoc "nodeC") -$(mkLoc "nodeD") - -type Participants = ["nodeA", "nodeB", "nodeC", "nodeD"] - -ring :: Ring Participants -ring = - [ Edge nodeA nodeB, - Edge nodeB nodeC, - Edge nodeC nodeD, - Edge nodeD nodeA - ] - -main :: IO () -main = do - [loc] <- getArgs - putStrLn "Please input a label:" - label <- read <$> getLine - _ <- runStateT (runChoreography config (ringLeader ring) loc) label - return () - where - config = - mkHttpConfig - [ ("nodeA", ("localhost", 4242)), - ("nodeB", ("localhost", 4343)), - ("nodeC", ("localhost", 4444)), - ("nodeD", ("localhost", 4545)) - ] diff --git a/examples/Tests.hs b/examples/Tests.hs deleted file mode 100644 --- a/examples/Tests.hs +++ /dev/null @@ -1,625 +0,0 @@ -module Tests where - -import Bank2PC qualified -import Bookseller0Network qualified -import Bookseller1Simple qualified -import Bookseller2HigherOrder qualified -import Bookseller3LocPoly qualified -import BooksellerFancy qualified -import CLI (runCLIStateful) -import CardGame qualified -import ChooseTeams qualified -import Choreography -import Choreography.Network.Local (mkLocalConfig) -import Control.Concurrent.Async (mapConcurrently) -import Data (BooksellerArgs (..), reference) -import Data.Maybe (maybeToList) -import DelegationFig20 qualified -import DiffieHellman qualified -import Distribution.TestSuite (Test) -import Distribution.TestSuite.QuickCheck -import GMWReal qualified -import KVS5Fig17 qualified -import KVS6SizePoly qualified -import Lottery qualified -import MPCFake qualified -import Test.QuickCheck - ( Positive, - Testable, - getPositive, - ioProperty, - (===), - ) - -tests :: IO [Test] -tests = return tests' - -normalSettings :: TestArgs -normalSettings = stdTestArgs {verbosity = Verbose} - -getNormalPT :: (Testable prop) => PropertyTest prop -> Test -getNormalPT = getPropertyTestWith normalSettings - -tests' :: [Test] -tests' = - [ getNormalPT - PropertyTest - { name = "tautology", - tags = [], - property = \i -> (===) @Int i i - }, - getNormalPT - PropertyTest - { name = "bank-2pc", - tags = [], - property = \(args@(Bank2PC.Args txns) :: Bank2PC.Args "alice" "bob") -> ioProperty do - let situation = - [ ("client", Bank2PC.render <$> txns), - ("coordinator", []), - ("alice", []), - ("bob", []) - ] - config <- mkLocalConfig [l | (l, _) <- situation] - results <- - mapConcurrently - ( \(name, inputs) -> - fst - <$> runCLIStateful - inputs - (runChoreography config Bank2PC.startBank name) - ) - situation - return $ results === reference args - }, - getNormalPT - PropertyTest - { name = "bookseller-0-network", - tags = [], - property = \args@BooksellerArgs {books, choice, budget} -> ioProperty do - let situation = - [ ("seller", [show books], Bookseller0Network.seller), - ("buyer", [show budget, choice], Bookseller0Network.buyer) - ] - config <- mkLocalConfig [l | (l, _, _) <- situation] - [([], ()), (delivery, ())] <- - mapConcurrently - ( \(name, inputs, process) -> runCLIStateful inputs $ runNetwork config name process - ) - situation - return $ (read <$> delivery) === maybeToList (reference args) - }, - getNormalPT - PropertyTest - { name = "bookseller-1-simple", - tags = [], - property = \args@BooksellerArgs {books, choice, budget} -> ioProperty do - let situation = - [ ("seller", [show books]), - ("buyer", [show budget, choice]) - ] - config <- mkLocalConfig [l | (l, _) <- situation] - [([], ()), (delivery, ())] <- - mapConcurrently - ( \(name, inputs) -> runCLIStateful inputs $ runChoreography config Bookseller1Simple.bookseller name - ) - situation - return $ (read <$> delivery) === maybeToList (reference args) - }, - getNormalPT - PropertyTest - { name = "bookseller-1-prime", - tags = [], - property = \args@BooksellerArgs {books, choice, budget} -> ioProperty do - let situation = - [ ("seller", [show books]), - ("buyer", [show budget, choice]) - ] - config <- mkLocalConfig [l | (l, _) <- situation] - [([], ()), (delivery, ())] <- - mapConcurrently - ( \(name, inputs) -> - runCLIStateful inputs $ - runChoreography config Bookseller1Simple.bookseller' name - ) - situation - return $ (read <$> delivery) === maybeToList (reference args) - }, - getNormalPT - PropertyTest - { name = "bookseller-2-higher-order", - tags = [], - property = \args@(BooksellerArgs {books, choice, budget}, contrib :: Positive Int) -> ioProperty do - let situation = - [ ("seller", [show books]), - ("buyer", [choice, show budget]), - ("buyer2", [show $ getPositive contrib]) - ] - config <- mkLocalConfig [l | (l, _) <- situation] - [([], ()), (delivery, ()), ([], ())] <- - mapConcurrently - ( \(name, inputs) -> - runCLIStateful inputs $ - runChoreography config (Bookseller2HigherOrder.bookseller Bookseller2HigherOrder.mkDecision2) name - ) - situation - return $ (read <$> delivery) === maybeToList (reference args) - }, - getNormalPT - PropertyTest - { name = "bookseller-2-dummy", - tags = [], - property = \(args@BooksellerArgs {books, choice, budget}, contrib :: Positive Int) -> ioProperty do - let situation = - [ ("seller", [show books]), - ("buyer", [choice, show budget]), - ("buyer2", [show $ getPositive contrib]) -- buyer2 doesn't get used - ] - config <- mkLocalConfig [l | (l, _) <- situation] - [([], ()), (delivery, ()), ([], ())] <- - mapConcurrently - ( \(name, inputs) -> - runCLIStateful inputs $ - runChoreography config (Bookseller2HigherOrder.bookseller Bookseller2HigherOrder.mkDecision1) name - ) - situation - return $ (read <$> delivery) === maybeToList (reference args) - }, - getNormalPT - PropertyTest - { name = "bookseller-3-locpoly", - tags = [], - property = \args@BooksellerArgs {books, choice, budget} -> ioProperty do - let situation = - [ ("seller", [show books]), - ("buyer", [show budget, choice]) - ] - let buyer :: Member "buyer" '["buyer"] = singleton - config <- mkLocalConfig [l | (l, _) <- situation] - [([], ()), (delivery, ())] <- - mapConcurrently - ( \(name, inputs) -> - runCLIStateful inputs $ - runChoreography config (Bookseller3LocPoly.bookseller buyer) name - ) - situation - return $ (read <$> delivery) === maybeToList (reference args) - }, - getNormalPT - PropertyTest - { name = "bookseller-fancy", - tags = [], - property = \args@(BooksellerArgs {books, choice, budget}, contrib :: Positive Int, contrib2 :: Positive Int, contrib3 :: Positive Int) -> ioProperty do - let situation = - [ ("seller", [show books]), - ("buyer", [choice, show budget]), - ("buyer2", [show $ getPositive contrib]), - ("buyer3", [show $ getPositive contrib2]), - ("buyer4", [show $ getPositive contrib3]) - ] - config <- mkLocalConfig [l | (l, _) <- situation] - [([], ()), (delivery, ()), ([], ()), ([], ()), ([], ())] <- - mapConcurrently - ( \(name, inputs) -> - runCLIStateful inputs $ - runChoreography config (BooksellerFancy.bookseller @["buyer2", "buyer3", "buyer4"] BooksellerFancy.mkDecision2) name - ) - situation - return $ (read <$> delivery) === maybeToList (reference args) - }, - getNormalPT - PropertyTest - { name = "card-game", - tags = [], - property = \args@(CardGame.Args deck (c1, c2, c3)) -> ioProperty do - let situation = - [ ("dealer", show <$> cycle deck), - ("player1", [show c1]), - ("player2", [show c2]), - ("player3", [show c3]) - ] - config <- mkLocalConfig [l | (l, _) <- situation] - [[], [r1], [r2], [r3]] <- - mapConcurrently - ( \(name, inputs) -> - fst - <$> runCLIStateful - inputs - (runChoreography config (CardGame.game @'["player1", "player2", "player3"]) name) - ) - situation - return $ (read r1, read r2, read r3) === reference args - }, - getNormalPT - PropertyTest - { name = "choose-teams", - tags = [], - property = \args@(ChooseTeams.Args (c2, c4)) -> ioProperty do - let situation = - [ ("player1", []), - ("player2", [show c2]), - ("player3", []), - ("player4", [show c4]), - ("player5", []) - ] - config <- mkLocalConfig [l | (l, _) <- situation] - results <- - mapConcurrently - ( \(name, inputs) -> - fst - <$> runCLIStateful - inputs - (runChoreography config (ChooseTeams.game @'["player1", "player2", "player3", "player4", "player5"]) name) - ) - situation - let [r1, r2, r3, r4, r5] = [concatMap read r | r <- results] - return $ (r1, r2, r3, r4, r5) === reference args - }, - getNormalPT - PropertyTest - { name = "delegation-fig20", - tags = [], - property = - \args@DelegationFig20.Args - { DelegationFig20.choice = choice, - DelegationFig20.aliceQ = aliceQ, - DelegationFig20.bobQ = bobQ, - DelegationFig20.carrollF = carrollF - } -> ioProperty do - let situation = - [ ("alice", [show choice, aliceQ]), - ("bob", [bobQ]), - ("carroll", [carrollF]) - ] - config <- mkLocalConfig [l | (l, _) <- situation] - [aliceR, bobR, carrollR] <- - mapConcurrently - ( \(name, inputs) -> - fst - <$> runCLIStateful - inputs - (runChoreography config DelegationFig20.mainCho name) - ) - situation - return $ - DelegationFig20.Result - { DelegationFig20.aliceR = aliceR, - DelegationFig20.bobR = bobR, - DelegationFig20.carrollR = carrollR - } - === reference args - }, - getNormalPT - PropertyTest -- This test is kinda dumb, but I don't know how better to express "correctness" of DHKE. - { name = "diffie-hellman", - tags = [], - property = \() -> ioProperty do - let situation = - [ ("alice", [""]), - ("bob", []) - ] - config <- mkLocalConfig [l | (l, _) <- situation] - [[a], [b]] <- - mapConcurrently - ( \(name, inputs) -> - fst - <$> runCLIStateful - inputs - (runChoreography config DiffieHellman.diffieHellman name) - ) - situation - return $ read @Integer a === read @Integer b - }, - getNormalPT - PropertyTest - { name = "kvs-5-fig17", - tags = [], - property = - \args@KVS5Fig17.Args - { KVS5Fig17.request = request, - KVS5Fig17.handler = handler - } -> ioProperty do - let situation = - [ ("client", [show request]), - ("primary", [handler]), - ("backup", []) - ] - config <- mkLocalConfig [l | (l, _) <- situation] - [[response], [], []] <- - mapConcurrently - ( \(name, inputs) -> - fst - <$> runCLIStateful - inputs - (runChoreography config KVS5Fig17.kvs name) - ) - situation - return $ read response === reference args - }, - getNormalPT - PropertyTest - { name = "kvs-6-sizepoly", - tags = [], - property = \(KVS6SizePoly.Args requests) -> ioProperty do - let situation = - [ ("clientAlice", show <$> requests), - ("primaryBob", []), - ("backup1", []), - ("backup2", []), - ("backup3", []), - ("backup4", []), - ("backup5", []) - ] - config <- mkLocalConfig [l | (l, _) <- situation] - let strategy1 = - KVS6SizePoly.naryReplicationStrategy - ( explicitMember :: - Member - "primaryBob" - '[ "clientAlice", - "primaryBob", - "backup1", - "backup2", - "backup3", - "backup4", - "backup5" - ] - ) - (consSuper $ consSuper refl) - let client :: Member "clientAlice" '["clientAlice", "primaryBob", "backup1", "backup2", "backup3", "backup4", "backup5"] - client = explicitMember - [responsesA, [], [], [], [], [], []] <- - mapConcurrently - ( \(name, inputs) -> - fst - <$> runCLIStateful - inputs - (runChoreography config (KVS6SizePoly.kvs strategy1 client) name) - ) - situation - let strategy2 = - KVS6SizePoly.nullReplicationStrategy - ( explicitMember :: - Member - "primaryBob" - '[ "clientAlice", - "primaryBob", - "backup1", - "backup2", - "backup3", - "backup4", - "backup5" - ] - ) - (responsesB, ()) <- runCLIStateful (show <$> requests) $ runChoreo (KVS6SizePoly.kvs strategy2 client) - return $ responsesA === responsesB - }, - getNormalPT - PropertyTest - { name = "lottery", - tags = [], - property = - \args@Lottery.Args - { Lottery.secrets = (c1, c2, c3, c4, c5), - Lottery.randomIs = (s1, s2, s3) - } -> ioProperty do - let clientProof :: - Subset - '["client1", "client2", "client3", "client4", "client5"] - '[ "client1", - "client2", - "client3", - "client4", - "client5", - "server1", - "server2", - "server3", - "analyst" - ] - clientProof = explicitSubset - serverProof :: - Subset - '["server1", "server2", "server3"] - '[ "client1", - "client2", - "client3", - "client4", - "client5", - "server1", - "server2", - "server3", - "analyst" - ] - serverProof = explicitSubset - analystProof :: - Member - "analyst" - '[ "client1", - "client2", - "client3", - "client4", - "client5", - "server1", - "server2", - "server3", - "analyst" - ] - analystProof = explicitMember - let situation = - [ ("client1", [show c1]), - ("client2", [show c2]), - ("client3", [show c3]), - ("client4", [show c4]), - ("client5", [show c5]), - ("server1", [show s1]), - ("server2", [show s2]), - ("server3", [show s3]), - ("analyst", []) - ] - config <- mkLocalConfig [l | (l, _) <- situation] - [ [], - [], - [], - [], - [], -- clients return nothing - [], - [], - [], -- servers return nothing - [response] - ] <- - mapConcurrently - ( \(name, inputs) -> - fst - <$> runCLIStateful - inputs - (runChoreography config (Lottery.lottery clientProof serverProof analystProof) name) - ) - situation - return $ read @Lottery.Fp response === reference args - }, - getNormalPT - PropertyTest - { name = "lottery-central-semantics", -- We don't have good controls over the sequencing of party-loops or operations in the central semantics; - -- but at least it's deterministic and this will notice if it breaks! - tags = [], - property = - \Lottery.Args - { Lottery.secrets = (c1, c2, c3, c4, c5), - Lottery.randomIs = (s1, s2, s3) - } -> ioProperty do - let clientProof :: - Subset - '["client1", "client2", "client3", "client4", "client5"] - '[ "client1", - "client2", - "client3", - "client4", - "client5", - "server1", - "server2", - "server3", - "analyst" - ] - clientProof = explicitSubset - serverProof :: - Subset - '["server1", "server2", "server3"] - '[ "client1", - "client2", - "client3", - "client4", - "client5", - "server1", - "server2", - "server3", - "analyst" - ] - serverProof = explicitSubset - analystProof :: - Member - "analyst" - '[ "client1", - "client2", - "client3", - "client4", - "client5", - "server1", - "server2", - "server3", - "analyst" - ] - analystProof = explicitMember - lottery = Lottery.lottery clientProof serverProof analystProof - let situation = - [ ("client1", [show c1]), - ("client2", [show c2]), - ("client3", [show c3]), - ("client4", [show c4]), - ("client5", [show c5]), - ("server1", [show s1]), - ("server2", [show s2]), - ("server3", [show s3]), - ("analyst", []) - ] - config <- mkLocalConfig [l | (l, _) <- situation] - [ [], - [], - [], - [], - [], - [], - [], - [], - [response] - ] <- - mapConcurrently - ( \(name, inputs) -> - fst - <$> runCLIStateful - inputs - (runChoreography config lottery name) - ) - situation - [centralSemanticsResponse] <- - fst - <$> runCLIStateful - [ show c1, - show c2, - show c3, - show c4, - show c5, - show s1, - show s2, - show s3 - ] - (runChoreo lottery) - return $ read @Lottery.Fp response === read centralSemanticsResponse - }, - getNormalPT - PropertyTest - { name = "mpc-fake", - tags = [], - property = \args@(MPCFake.Args circuit p1in p2in p3in p4in) -> ioProperty do - let situation = - [ ("trusted3rdParty", []), - ("p1", repeat $ show p1in), - ("p2", repeat $ show p2in), - ("p3", repeat $ show p3in), - ("p4", repeat $ show p4in) - ] - config <- mkLocalConfig [l | (l, _) <- situation] - [[], [r1], [r2], [r3], [r4]] <- - mapConcurrently - ( \(name, inputs) -> - fst - <$> runCLIStateful - inputs - (runChoreography config (MPCFake.mpc circuit) name) - ) - situation - return $ (read r1, read r2, read r3, read r4) === reference args - }, - getPropertyTestWith - (stdTestArgs {verbosity = Verbose, maxSuccess = 100, maxSize = 10}) - PropertyTest - { name = "gmw-real", - tags = [], - property = \args@(GMWReal.Args circuit p1in p2in p3in p4in) -> ioProperty do - let situation = - [ ("p1", repeat $ show p1in), - ("p2", repeat $ show p2in), - ("p3", repeat $ show p3in), - ("p4", repeat $ show p4in) - ] - config <- mkLocalConfig [l | (l, _) <- situation] - [[r1], [r2], [r3], [r4]] <- - mapConcurrently - ( \(name, inputs) -> - fst - <$> runCLIStateful - inputs - (runChoreography config (GMWReal.mpc circuit) name) - ) - situation - return $ (read r1, read r2, read r3, read r4) === reference args - } - ] diff --git a/src/Choreography/Choreography.hs b/src/Choreography/Choreography.hs --- a/src/Choreography/Choreography.hs +++ b/src/Choreography/Choreography.hs @@ -19,7 +19,7 @@ infix 4 `locally` -locally l m = enclave (l @@ nobody) $ locally' m +locally l m = conclave (l @@ nobody) $ locally' m -- | Perform the exact same pure computation in replicate at multiple locations. -- The computation can not use anything local to an individual party, including their identity. @@ -32,7 +32,7 @@ infix 4 `congruently` -congruently ls a = enclave ls $ congruently' a +congruently ls a = conclave ls $ congruently' a -- | Unwrap a value known to the entire census. naked :: @@ -91,22 +91,22 @@ infix 4 ~> s ~> rs = do - x :: a <- enclave (presentToSend s @@ rs) $ broadcast' First (ownsMessagePayload s, structMessagePayload s) + x :: a <- conclave (presentToSend s @@ rs) $ broadcast' First (ownsMessagePayload s, structMessagePayload s) congruently rs (\un -> un consSet x) --- * Enclaves +-- * Conclaves -- | Lift a choreography involving fewer parties into the larger party space. --- This version, where the returned value is Located at the entire enclave, does not add a Located layer. -enclaveToAll :: forall ls a ps m. (KnownSymbols ls) => Subset ls ps -> Choreo ls m (Located ls a) -> Choreo ps m (Located ls a) +-- This version, where the returned value is Located at the entire conclave, does not add a Located layer. +conclaveToAll :: forall ls a ps m. (KnownSymbols ls) => Subset ls ps -> Choreo ls m (Located ls a) -> Choreo ps m (Located ls a) -infix 4 `enclaveToAll` +infix 4 `conclaveToAll` -enclaveToAll = (`enclaveTo` (refl @ls)) +conclaveToAll = (`conclaveTo` (refl @ls)) -- | Lift a choreography of involving fewer parties into the larger party space. -- This version, where the returned value is already Located, does not add a Located layer. -enclaveTo :: +conclaveTo :: forall ls a rs ps m. (KnownSymbols ls) => Subset ls ps -> @@ -114,6 +114,6 @@ Choreo ls m (Located rs a) -> Choreo ps m (Located rs a) -infix 4 `enclaveTo` +infix 4 `conclaveTo` -enclaveTo subcensus recipients ch = flatten recipients (refl @rs) <$> (subcensus `enclave` ch) +conclaveTo subcensus recipients ch = flatten recipients (refl @rs) <$> (subcensus `conclave` ch) diff --git a/src/Choreography/Choreography/Batteries.hs b/src/Choreography/Choreography/Batteries.hs --- a/src/Choreography/Choreography/Batteries.hs +++ b/src/Choreography/Choreography/Batteries.hs @@ -107,9 +107,9 @@ x <- l @@ nobody `congruently` \uns -> m $ uns . (@@ nobody) (l, x) ~> ls' --- * Enclaves +-- * Conclaves --- | Conditionally execute choreographies based on a located value. Automatically enclaves. +-- | Conditionally execute choreographies based on a located value. Automatically conclaves. cond :: (KnownSymbols ls) => -- | Tuple: Proof all the parties involved know the branch-guard @@ -118,4 +118,4 @@ -- | The body of the conditional as a function from the unwrapped value. (a -> Choreo ls m b) -> Choreo ps m (Located ls b) -cond (ls, (owns, a)) c = enclave ls $ naked owns a >>= c +cond (ls, (owns, a)) c = conclave ls $ naked owns a >>= c diff --git a/src/Choreography/Core.hs b/src/Choreography/Core.hs --- a/src/Choreography/Core.hs +++ b/src/Choreography/Core.hs @@ -10,7 +10,7 @@ -- , ChoreoSig(..) I can't think of any reasons why we _should_ export this, nor any reason why we shouldn't... locally', congruently', - enclave, + conclave, -- * Running choreographies epp, @@ -88,7 +88,7 @@ Member l ps -> -- from (Member l ls, Located ls a) -> -- value ChoreoSig ps m a - Enclave :: + Conclave :: (KnownSymbols ls) => Subset ls ps -> Choreo ls m b -> @@ -112,7 +112,7 @@ unwraps = unwrap . (\(Subset mx) -> mx First) -- wish i could write this better. in pure . f $ unwraps handler (Broadcast _ (p, a)) = pure $ unwrap p a - handler (Enclave (_ :: Subset ls (p ': ps)) c) = case tySpine @ls of + handler (Conclave (_ :: Subset ls (p ': ps)) c) = case tySpine @ls of TyNil -> pure Empty TyCons -> wrap <$> runChoreo c @@ -146,7 +146,7 @@ send (unwrap l a) otherRecipients pure . unwrap l $ a else recv sender - handler (Enclave proof ch) + handler (Conclave proof ch) | l' `elem` toLocs proof = wrap <$> epp ch l' | otherwise = pure Empty @@ -187,12 +187,12 @@ -- | Lift a choreography of involving fewer parties into the larger party space. -- Adds a `Located ls` layer to the return type. -enclave :: +conclave :: (KnownSymbols ls) => Subset ls ps -> Choreo ls m a -> Choreo ps m (Located ls a) -infix 4 `enclave` +infix 4 `conclave` -enclave proof ch = toFreer $ Enclave proof ch +conclave proof ch = toFreer $ Conclave proof ch