add primitives for the new submissions store

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

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)

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

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