Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
add primitives for the new submissions store
- Loading branch information
Showing
6 changed files
with
493 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
138 changes: 138 additions & 0 deletions
138
lib/wallet/src/Cardano/Wallet/Submissions/Primitives.hs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,138 @@ | ||
{-# LANGUAGE FlexibleContexts #-} | ||
{-# LANGUAGE GADTSyntax #-} | ||
{-# LANGUAGE ScopedTypeVariables #-} | ||
|
||
{- | | ||
Copyright: © 2022 IOHK | ||
License: Apache-2.0 | ||
Primitive operations over the Submissions store. | ||
These operations are guaranteed to follow the specifications individually. | ||
For store consistence use 'Operations' module where they are composed for | ||
that goal. | ||
-} | ||
|
||
module Cardano.Wallet.Submissions.Primitives | ||
( Primitive (..) | ||
, applyPrimitive | ||
) | ||
where | ||
|
||
import Prelude | ||
|
||
import Cardano.Wallet.Submissions.Submissions | ||
( Submissions | ||
, finality | ||
, finalityL | ||
, tip | ||
, tipL | ||
, transactions | ||
, transactionsL | ||
) | ||
import Cardano.Wallet.Submissions.TxStatus | ||
( HasTxId (..), TxStatus (Expired, InLedger, InSubmission) ) | ||
import Control.Lens | ||
( over, (%~), (&), (.~) ) | ||
import Control.Monad | ||
( guard ) | ||
import Data.Foldable | ||
( Foldable (..) ) | ||
import Data.Maybe | ||
( fromMaybe ) | ||
|
||
import qualified Data.Map.Strict as Map | ||
|
||
-- | Primitive operations to change a 'Submissions' store. | ||
data Primitive slot tx where | ||
-- | Insert tx new transaction in the local submission store. | ||
AddSubmission :: | ||
{_expiring :: slot, _transaction :: tx} -> | ||
Primitive slot tx | ||
-- | Change a transaction state to 'InLedger'. | ||
MoveToLedger :: | ||
{_acceptance :: slot, _transaction :: tx} -> | ||
Primitive slot tx | ||
-- | Move the submission store tip slot. | ||
MoveTip :: | ||
{_tip :: slot} -> | ||
Primitive slot tx | ||
-- | Move the submission store finality slot. | ||
MoveFinality :: | ||
{_finality :: slot} -> | ||
Primitive slot tx | ||
-- | Remove a transaction from tracking in the submissions store. | ||
Forget :: | ||
{_transaction :: tx} -> | ||
Primitive slot tx | ||
deriving (Show) | ||
|
||
defaultToDoNothing :: (t -> Maybe t) -> t -> t | ||
defaultToDoNothing f x = fromMaybe x $ f x | ||
|
||
-- | Apply a 'Primitive' to a submission. | ||
-- | ||
-- Not all primitives will eventually change the store, the specifications | ||
-- should be used to define when a primitive is allowed to act. | ||
-- When a primitive doesn't meet the specs, a no-op will be computed. | ||
applyPrimitive | ||
:: forall slot tx | ||
. (Ord slot, Ord (TxId tx), HasTxId tx) | ||
=> Primitive slot tx | ||
-> Submissions slot tx | ||
-> Submissions slot tx | ||
applyPrimitive (AddSubmission expiring tx) = | ||
defaultToDoNothing $ \s -> do | ||
guard $ expiring > tip s | ||
guard $ Map.notMember (txId tx) (transactions s) | ||
pure $ | ||
s & transactionsL | ||
%~ Map.insert (txId tx) (InSubmission expiring tx) | ||
applyPrimitive (MoveToLedger acceptance tx) = \s -> | ||
s & over transactionsL (Map.adjust (f s) (txId tx)) | ||
where | ||
f s x@(InSubmission expiring tx') | ||
| acceptance > (tip s) && acceptance <= expiring = | ||
InLedger expiring acceptance tx' | ||
| otherwise = x | ||
f _ x = x | ||
applyPrimitive (MoveTip newTip) = | ||
defaultToDoNothing $ \s -> do | ||
pure $ s | ||
& (finalityL .~ if newTip <= finality s then newTip else finality s) | ||
. (tipL .~ newTip) | ||
. (transactionsL %~ fmap f) | ||
where | ||
f :: TxStatus slot tx -> TxStatus slot tx | ||
f s@(InLedger expiring acceptance tx) | ||
| acceptance > newTip = InSubmission expiring tx | ||
| otherwise = s | ||
f s@(InSubmission expiring tx) | ||
| expiring <= newTip = Expired expiring tx | ||
| otherwise = s | ||
f s@(Expired expiring tx) | ||
| expiring > newTip = InSubmission expiring tx | ||
| otherwise = s | ||
f s = s | ||
applyPrimitive (MoveFinality newFinality) = | ||
defaultToDoNothing $ \s -> do | ||
let finality' | ||
| newFinality >= tip s = tip s | ||
| newFinality <= finality s = finality s | ||
| otherwise = newFinality | ||
pure $ s | ||
& (finalityL .~ finality') | ||
. (transactionsL %~ g finality') | ||
where | ||
g finality' m = foldl' (flip $ Map.alter (>>= f)) m (Map.keys m) | ||
where | ||
f :: TxStatus slot tx -> Maybe (TxStatus slot tx) | ||
f s@(InLedger _expiring acceptance _tx) | ||
| acceptance <= finality' = Nothing | ||
| otherwise = Just s | ||
f s@(Expired expiring _tx) | ||
| expiring <= finality' = Nothing | ||
| otherwise = Just s | ||
f s = Just s | ||
applyPrimitive (Forget tx) = transactionsL %~ Map.delete (txId tx) |
63 changes: 63 additions & 0 deletions
63
lib/wallet/src/Cardano/Wallet/Submissions/Properties/Common.hs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,63 @@ | ||
{-# LANGUAGE FlexibleContexts #-} | ||
{-# LANGUAGE StandaloneDeriving #-} | ||
{-# LANGUAGE TemplateHaskell #-} | ||
{-# LANGUAGE TypeApplications #-} | ||
{-# LANGUAGE UndecidableInstances #-} | ||
|
||
module Cardano.Wallet.Submissions.Properties.Common | ||
( | ||
Step (..) | ||
, deltaState, oldState, newState | ||
, that, verify, forAllIn | ||
, (#) | ||
) | ||
where | ||
|
||
import Prelude | ||
|
||
import Cardano.Wallet.Submissions.Submissions | ||
( Submissions ) | ||
import Cardano.Wallet.Submissions.TxStatus | ||
( HasTxId (TxId) ) | ||
import Control.Lens | ||
( makeLenses ) | ||
import Control.Monad.Trans.Writer | ||
( Writer, execWriter, tell ) | ||
import Data.Foldable | ||
( toList ) | ||
import Data.Set | ||
( Set ) | ||
import Test.QuickCheck | ||
( Property, Testable (..), conjoin, counterexample ) | ||
|
||
infixr 1 # | ||
(#) :: Testable t => t -> String -> Property | ||
(#) = flip counterexample | ||
|
||
forAllIn | ||
:: Show a | ||
=> Set a | ||
-> (a -> Property) | ||
-> Property | ||
forAllIn db f = conjoin $ fmap g (toList db) | ||
where g i = counterexample (show i) $ f i | ||
|
||
type Prop t a = Writer [t] a | ||
|
||
that :: Testable t => String -> t -> Prop Property () | ||
that s = tell . pure . counterexample s | ||
|
||
verify :: Testable t => Prop t a -> Property | ||
verify = conjoin . execWriter | ||
|
||
-- | Encode a change of the store, for inspection | ||
data Step delta slot tx = Step | ||
{ _oldState :: Submissions slot tx | ||
, _newState :: Submissions slot tx | ||
, _deltaState :: delta slot tx | ||
} | ||
|
||
deriving instance (Show slot, Show (TxId tx), Show tx, Show (delta slot tx)) | ||
=> Show (Step delta slot tx) | ||
|
||
makeLenses ''Step |
141 changes: 141 additions & 0 deletions
141
lib/wallet/src/Cardano/Wallet/Submissions/Properties/Primitives.hs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,141 @@ | ||
{-# LANGUAGE FlexibleContexts #-} | ||
{-# LANGUAGE MultiWayIf #-} | ||
{-# OPTIONS_GHC -Wno-incomplete-patterns #-} | ||
|
||
module Cardano.Wallet.Submissions.Properties.Primitives | ||
( properties | ||
, txIds | ||
) | ||
where | ||
|
||
import Prelude | ||
|
||
import Cardano.Wallet.Submissions.Primitives | ||
( Primitive (..) ) | ||
import Cardano.Wallet.Submissions.Properties.Common | ||
( Step (Step), forAllIn, that, verify, ( # ) ) | ||
|
||
import Cardano.Wallet.Submissions.Submissions | ||
( Submissions, finality, tip, transactions ) | ||
import Cardano.Wallet.Submissions.TxStatus | ||
( HasTxId (..) | ||
, TxStatus (Expired, InLedger, InSubmission, Unknown) | ||
, status | ||
) | ||
import Data.Set | ||
( Set, singleton ) | ||
import Test.QuickCheck | ||
( Property, counterexample, (.&.), (===) ) | ||
|
||
import qualified Data.Map.Strict as Map | ||
|
||
txIds :: Submissions slot tx -> Set (TxId tx) | ||
txIds = Map.keysSet . transactions | ||
|
||
-- | Translations of primitive properties from specifications. | ||
properties | ||
:: (Ord (TxId tx), Eq tx, HasTxId tx | ||
, Ord slot, Show (TxId tx), Show slot, Show tx) | ||
=> Step Primitive slot tx -> Property | ||
properties (Step xs xs' (AddSubmission expiring x)) = do | ||
let world = txIds xs <> txIds xs' <> singleton (txId x) | ||
counterexample "on add-submission" $ verify $ do | ||
that "tip and finality are not changed" | ||
$ tip xs === tip xs' | ||
.&. finality xs === finality xs' | ||
that "finality should never change" | ||
$ finality xs === finality xs' | ||
that "changes transaction statuses" $ forAllIn world $ \y -> | ||
let old = status y $ transactions xs | ||
new = status y $ transactions xs' | ||
in case old of | ||
Unknown | ||
| expiring > tip xs | ||
&& txId x == y | ||
-> | ||
new === InSubmission expiring x | ||
# "required should go to in-submission if unknown" | ||
_ -> new === old | ||
properties (Step xs xs' (MoveToLedger acceptance x)) = do | ||
let world = txIds xs <> txIds xs' <> singleton (txId x) | ||
counterexample "on move-to-ledger" $ verify $ do | ||
that "tip and finality are not changed" | ||
$ tip xs === tip xs' | ||
.&. finality xs === finality xs' | ||
that "changes transaction statuses" $ forAllIn world $ \y -> | ||
let old = status y $ transactions xs | ||
new = status y $ transactions xs' | ||
in case old of | ||
InSubmission expiring _ | ||
| acceptance > tip xs | ||
&& acceptance <= expiring | ||
&& txId x == y | ||
-> | ||
new === InLedger expiring acceptance x | ||
# "required should go in ledger if acceptance is\ | ||
\ after tip and before expiration" | ||
_ -> old === new | ||
properties (Step xs xs' (MoveTip newTip)) = do | ||
let world = txIds xs <> txIds xs' | ||
counterexample "on move-tip" $ verify $ do | ||
that "changes the tip" | ||
$ tip xs' === newTip | ||
that "can change finality" $ if | ||
| newTip < finality xs -> finality xs' === newTip | ||
| newTip >= finality xs -> finality xs' === finality xs | ||
that "changes transaction statuses" $ forAllIn world $ \y -> | ||
let old = status y $ transactions xs | ||
new = status y $ transactions xs' | ||
in case old of | ||
InSubmission expiring tx | ||
| expiring <= newTip -> | ||
new === Expired expiring tx | ||
# "in-submission should have expired" | ||
Expired expiring tx | ||
| expiring > newTip-> | ||
new === InSubmission expiring tx | ||
# "expired should be in-submission" | ||
InLedger expiring acceptance tx | ||
| acceptance > newTip -> | ||
new === InSubmission expiring tx | ||
# "accepted should be in-submission" | ||
_ -> new === old | ||
properties (Step xs xs' (MoveFinality newFinality)) = do | ||
let world = txIds xs <> txIds xs' | ||
counterexample "on move-tip" $ verify $ do | ||
that "tip do not change" | ||
$ tip xs' === tip xs | ||
that "finality changes" $ if | ||
| newFinality > finality xs && newFinality < tip xs | ||
-> finality xs' === newFinality | ||
| newFinality <= finality xs | ||
-> finality xs' === finality xs | ||
| newFinality >= tip xs' | ||
-> finality xs' === tip xs | ||
that "changes transaction statuses" $ forAllIn world $ \y -> | ||
let old = status y $ transactions xs | ||
new = status y $ transactions xs' | ||
in case old of | ||
InLedger _expiring acceptance _ | ||
| acceptance <= finality xs'-> | ||
new === Unknown | ||
# "accepted should have been pruned" | ||
Expired expiring _ | ||
| expiring <= finality xs' -> | ||
new === Unknown | ||
# "expired should have been pruned" | ||
_ -> new === old | ||
properties (Step xs xs' (Forget x)) = do | ||
let world = txIds xs <> txIds xs' <> singleton (txId x) | ||
counterexample "on move-tip" $ verify $ do | ||
that "tip shouldn't have changed" $ tip xs === tip xs' | ||
that "finality shouldn't have changed" $ finality xs === finality xs' | ||
that "changes transaction statuses" $ forAllIn world $ \y -> | ||
let old = status y $ transactions xs | ||
new = status y $ transactions xs' | ||
in case old of | ||
_ | txId x == y | ||
-> | ||
new === Unknown | ||
# "transaction should have been removed" | ||
_ -> new === old |
Oops, something went wrong.