content: -- | Specification for Pos.Chain.Ssc.GodTossing.Toss.Pure
  
  module Test.Pos.Ssc.Toss.PureSpec
         ( spec
         ) where
  
  import           Universum
  
  import qualified Crypto.Random as Rand
  import           Data.Default (def)
  import           Test.Hspec (Spec, describe)
  import           Test.Hspec.QuickCheck (modifyMaxSuccess, prop)
  import           Test.QuickCheck (Arbitrary (..), Gen, Property, forAll, listOf,
                       suchThat, (===))
  import           Test.QuickCheck.Arbitrary.Generic (genericArbitrary,
                       genericShrink)
  
  import           Pos.Chain.Ssc (InnerSharesMap, Opening, SignedCommitment,
                       VssCertificate (..))
  import qualified Pos.Chain.Ssc as Toss
  import           Pos.Core (EpochOrSlot, StakeholderId, addressHash)
  
  import           Test.Pos.Core.Arbitrary ()
  import           Test.Pos.Infra.Arbitrary.Ssc ()
  
  spec :: Spec
  spec = describe "Toss" $ do
      let smaller n = modifyMaxSuccess (const n)
      describe "PureToss" $ smaller 30 $ do
          prop "Adding and deleting a signed commitment in the 'PureToss' monad is the\
               \ same as doing nothing"
               putDelCommitment
          prop "Adding and deleting an opening in the 'PureToss' monad is the same as doing\
               \ nothing"
               putDelOpening
          prop "Adding and deleting a share in the 'PureToss' monad is the same as doing\
               \ nothing"
               putDelShare
  
  data TossAction
      = PutCommitment SignedCommitment
      | PutOpening StakeholderId Opening
      | PutShares StakeholderId InnerSharesMap
      | PutCertificate VssCertificate
      | ResetCO
      | ResetShares
      | DelCommitment StakeholderId
      | DelOpening StakeholderId
      | DelShares StakeholderId
      | SetEpochOrSlot EpochOrSlot
      deriving (Show, Eq, Generic)
  
  instance Arbitrary TossAction where
      arbitrary = genericArbitrary
      shrink = genericShrink
  
  actionToMonad :: Toss.MonadToss m => TossAction -> m ()
  actionToMonad (PutCommitment sc)   = Toss.putCommitment sc
  actionToMonad (PutOpening sid o)   = Toss.putOpening sid o
  actionToMonad (PutShares sid ism)  = Toss.putShares sid ism
  actionToMonad (PutCertificate v)   = Toss.putCertificate v
  actionToMonad ResetCO              = Toss.resetCO
  actionToMonad ResetShares          = Toss.resetShares
  actionToMonad (DelCommitment sid)  = Toss.delCommitment sid
  actionToMonad (DelOpening sid)     = Toss.delOpening sid
  actionToMonad (DelShares sid)      = Toss.delShares sid
  actionToMonad (SetEpochOrSlot eos) = Toss.setEpochOrSlot eos
  
  emptyTossSt :: Toss.SscGlobalState
  emptyTossSt = def
  
  perform :: [TossAction] -> Toss.PureToss ()
  perform = mapM_ actionToMonad
  
  -- | Type synonym used for convenience. This quintuple is used to pass the randomness
  -- needed to run 'PureToss' actions to the testing property.
  type TossTestInfo = (Word64, Word64, Word64, Word64, Word64)
  
  -- | Operational equivalence operator in the 'PureToss' monad. To be used when
  -- equivalence between two sequences of actions in 'PureToss' is to be tested/proved.
  (==^)
      :: [TossAction]
      -> [TossAction]
      -> Gen TossAction
      -> TossTestInfo
      -> Property
  t1 ==^ t2 = \prefixGen ttInfo ->
      forAll ((listOf prefixGen) :: Gen [TossAction]) $ \prefix ->
      forAll (arbitrary :: Gen [TossAction]) $ \suffix ->
          let applyAction x =
                  view _2 .
                  fst . Rand.withDRG (Rand.drgNewTest ttInfo) .
                  Toss.runPureToss emptyTossSt $ (perform $ prefix ++ x ++ suffix)
          in applyAction t1 === applyAction t2
  
  {- A note on the following tests
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  
  The reason these tests have to pass a custom generator for the prefix of the action list
  to '(==^)' is that in each case, there is a particular sequence of actions for which
  the property does not hold. Using one of the following tests as an example:
  
  Let 'o, o´ :: Opening' such that 'o /= o´'. This sequence of actions
  in the 'PureToss' monad:
  
      [PutOpening sid o´, PutOpening sid o, DelOpening sid]
  
  is not, in operational semantics terms, equal to the sequence
  
      [PutOpening sid o´]
  
  It is instead equivalent to
  
      []
  
  Because these actions are performed from left to right, performing an insertion with the
  same key several times without deleting it in between those insertions means only the
  last insertion actually matters for these tests.
  
  As such, prefixes with an insertion with the same key as the action being tested in the
  property will cause it to fail.
  -}
  
  putDelCommitment :: SignedCommitment -> TossTestInfo -> Property
  putDelCommitment sc =
      let actionPrefixGen = arbitrary `suchThat` (\case
              PutCommitment sc' -> sc ^. _1 /= sc'^. _1
              _                 -> True)
      in ([PutCommitment sc, DelCommitment $ addressHash $ sc ^. _1] ==^ []) actionPrefixGen
  
  putDelOpening
      :: StakeholderId
      -> Opening
      -> TossTestInfo
      -> Property
  putDelOpening sid o =
      let actionPrefixGen = arbitrary `suchThat` (\case
              PutOpening sid' _ -> sid /= sid'
              _                 -> True)
      in ([PutOpening sid o, DelOpening sid] ==^ []) actionPrefixGen
  
  putDelShare
      :: StakeholderId
      -> InnerSharesMap
      -> TossTestInfo
      -> Property
  putDelShare sid ism =
      let actionPrefixGen = arbitrary `suchThat` (\case
              PutShares sid' _ -> sid' /= sid
              _                -> True)
      in ([PutShares sid ism, DelShares sid] ==^ []) actionPrefixGen
  