From 8fbd7f2fd03bf1966307795f330ec2c06675202a Mon Sep 17 00:00:00 2001 From: paolo veronelli Date: Tue, 22 Nov 2022 13:12:57 +0100 Subject: [PATCH] add primitives for the new submissions store --- lib/wallet/cardano-wallet.cabal | 6 + .../Cardano/Wallet/Submissions/Primitives.hs | 138 +++++++++++++++++ .../Wallet/Submissions/Properties/Common.hs | 63 ++++++++ .../Submissions/Properties/Primitives.hs | 141 ++++++++++++++++++ .../Cardano/Wallet/Submissions/Submissions.hs | 61 ++++++++ .../Cardano/Wallet/Submissions/TxStatus.hs | 84 +++++++++++ 6 files changed, 493 insertions(+) create mode 100644 lib/wallet/src/Cardano/Wallet/Submissions/Primitives.hs create mode 100644 lib/wallet/src/Cardano/Wallet/Submissions/Properties/Common.hs create mode 100644 lib/wallet/src/Cardano/Wallet/Submissions/Properties/Primitives.hs create mode 100644 lib/wallet/src/Cardano/Wallet/Submissions/Submissions.hs create mode 100644 lib/wallet/src/Cardano/Wallet/Submissions/TxStatus.hs diff --git a/lib/wallet/cardano-wallet.cabal b/lib/wallet/cardano-wallet.cabal index 29f6a6880d7..5a2a79cfdd0 100644 --- a/lib/wallet/cardano-wallet.cabal +++ b/lib/wallet/cardano-wallet.cabal @@ -126,6 +126,7 @@ library , io-classes , iohk-monitoring , lattices + , lens , lifted-async , math-functions , memory @@ -336,6 +337,11 @@ library Cardano.Wallet.Shelley.Network.Discriminant Cardano.Wallet.Shelley.Network.Node Cardano.Wallet.Shelley.Transaction + Cardano.Wallet.Submissions.Primitives + Cardano.Wallet.Submissions.Properties.Common + Cardano.Wallet.Submissions.Properties.Primitives + Cardano.Wallet.Submissions.Submissions + Cardano.Wallet.Submissions.TxStatus Cardano.Wallet.TokenMetadata Cardano.Wallet.Transaction Cardano.Wallet.Version diff --git a/lib/wallet/src/Cardano/Wallet/Submissions/Primitives.hs b/lib/wallet/src/Cardano/Wallet/Submissions/Primitives.hs new file mode 100644 index 00000000000..39dccbd3376 --- /dev/null +++ b/lib/wallet/src/Cardano/Wallet/Submissions/Primitives.hs @@ -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) diff --git a/lib/wallet/src/Cardano/Wallet/Submissions/Properties/Common.hs b/lib/wallet/src/Cardano/Wallet/Submissions/Properties/Common.hs new file mode 100644 index 00000000000..c4a41793bf0 --- /dev/null +++ b/lib/wallet/src/Cardano/Wallet/Submissions/Properties/Common.hs @@ -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 diff --git a/lib/wallet/src/Cardano/Wallet/Submissions/Properties/Primitives.hs b/lib/wallet/src/Cardano/Wallet/Submissions/Properties/Primitives.hs new file mode 100644 index 00000000000..8cba332adef --- /dev/null +++ b/lib/wallet/src/Cardano/Wallet/Submissions/Properties/Primitives.hs @@ -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 diff --git a/lib/wallet/src/Cardano/Wallet/Submissions/Submissions.hs b/lib/wallet/src/Cardano/Wallet/Submissions/Submissions.hs new file mode 100644 index 00000000000..396f1dc15c9 --- /dev/null +++ b/lib/wallet/src/Cardano/Wallet/Submissions/Submissions.hs @@ -0,0 +1,61 @@ +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GADTSyntax #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE UndecidableInstances #-} + +{- | +Copyright: © 2022 IOHK +License: Apache-2.0 + +Data type 'Submissions' for storing a set of submitted transactions. + +-} +module Cardano.Wallet.Submissions.Submissions + ( Submissions (..) + , tip + , finality + , tipL + , finalityL + , transactionsL + , transactions) + where + +import Prelude + +import Cardano.Wallet.Submissions.TxStatus +import Control.Lens + ( makeLenses, view ) +import Data.Map.Strict + ( Map ) + +-- | Data type for keeping track of transactions, both pending and in ledger. +data Submissions slot tx = Submissions + { -- | Tracked transactions with their status. + _transactionsL :: Map (TxId tx) (TxStatus slot tx), + -- | Current finality slot. + -- No transactions before this slot are in control. + _finalityL :: slot, + -- | Current tip. + -- All transactions in Ledger should be accepted up to here. + _tipL :: slot + } + +deriving instance + (Show slot, Show (TxId tx), Show tx) => + (Show (Submissions slot tx)) + +makeLenses ''Submissions + +-- | Current slot tip. +tip :: Submissions slot tx -> slot +tip = view tipL + +-- | Current finality tip. +finality :: Submissions slot tx -> slot +finality = view finalityL + +transactions :: Submissions slot tx -> TxStatuses slot tx +transactions = view transactionsL diff --git a/lib/wallet/src/Cardano/Wallet/Submissions/TxStatus.hs b/lib/wallet/src/Cardano/Wallet/Submissions/TxStatus.hs new file mode 100644 index 00000000000..97c945e7a3f --- /dev/null +++ b/lib/wallet/src/Cardano/Wallet/Submissions/TxStatus.hs @@ -0,0 +1,84 @@ +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GADTSyntax #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE UndecidableInstances #-} + +{- | +Copyright: © 2022 IOHK +License: Apache-2.0 + +Data type 'Submissions' for storing a set of submitted transactions. + +-} +module Cardano.Wallet.Submissions.TxStatus + ( HasTxId (..) + , TxStatus (..) + , _Expired + , _InLedger + , _InSubmission + , _Unknown + , status + , slotObservation + , TxStatuses + ) + where + +import Prelude + +import Control.Lens + ( makePrisms ) +import Data.Map.Strict + ( Map ) +import Data.Maybe + ( fromMaybe ) + +import qualified Data.Map.Strict as Map + +-- | Classify values with an Id. +class HasTxId a where + type TxId a + txId :: a -> TxId a + +-- | Status of a transactions tracked in the submissions store. +data TxStatus slot tx where + -- | A transaction which is waiting to appear in on the blockchain. + InSubmission + :: slot -- ^ expiration slot + -> tx -- ^ transaction + -> TxStatus slot tx + -- | A transaction which has been accepted on the blockchain. + InLedger + :: slot -- ^ expiration slot + -> slot -- ^ accetpance slot + -> tx -- ^ transaction + -> TxStatus slot tx + -- | A transaction which has expired. + Expired + :: slot -- ^ expiration slot + -> tx -- ^ transaction + -> TxStatus slot tx + -- | A transaction which is not tracked by the submissions store. + Unknown :: TxStatus slot tx + deriving (Show, Eq) + +makePrisms ''TxStatus + +type TxStatuses slot tx = Map (TxId tx) (TxStatus slot tx ) + +-- | Extract a transaction status based on its identifier. +status + :: Ord (TxId tx) + => TxId tx + -> TxStatuses slot tx + -> TxStatus slot tx +status id' m = fromMaybe Unknown $ Map.lookup id' m + +slotObservation :: TxStatus slot tx -> Maybe slot +slotObservation = \case + InSubmission s _ -> Just s + InLedger _ s _ -> Just s + Expired s _ -> Just s + Unknown -> Nothing