{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

module Test.Control.State.Transition.Examples.CommitReveal where

import Cardano.Crypto.Hash (Hash, HashAlgorithm)
import Cardano.Crypto.Hash.Short (ShortHash)
import Cardano.Ledger.Binary (EncCBOR (..), hashEncCBOR)
import Control.State.Transition (
  Environment,
  PredicateFailure,
  STS (..),
  Signal,
  State,
  TRC (TRC),
  initialRules,
  judgmentContext,
  transitionRules,
  (?!),
 )
import Data.Kind (Type)
import Data.List.Unique (allUnique)
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Typeable (Typeable)
import qualified Test.Control.State.Transition.Trace as Trace
import qualified Test.Control.State.Transition.Trace.Generator.QuickCheck as STS.Gen
import Test.QuickCheck (
  Arbitrary,
  Property,
  arbitrary,
  choose,
  elements,
  oneof,
  shrink,
  withMaxSuccess,
 )
import Prelude hiding (id)

-- | Commit-reveal transition system, where data hashes are committed and then
-- revealed.
--
-- The first type parameter denotes the type of hash algorithm used.
--
-- The second parameter denotes the structure used to associate a commit to its
-- hash. See 'CRSt'
--
-- The third parameter is the data that will be associated to the 'Commit'
-- signal.
data CR hashAlgo (hashToDataMap :: Type -> Type -> Type) commitData

-- | Commit-reveal transition system state.
data CRSt hashAlgo hashToDataMap commitData = CRSt
  { forall hashAlgo (hashToDataMap :: * -> * -> *) commitData.
CRSt hashAlgo hashToDataMap commitData
-> hashToDataMap (Hash hashAlgo Data) commitData
hashToData :: !(hashToDataMap (Hash hashAlgo Data) commitData)
  -- ^ Part of the state used to associate data to the hash that was committed.
  --
  -- This is used only by the generators, so 'hashToDataMap' will be
  -- instantiated to a 'Map' in the generators, for testing purposes; and it
  -- will be instantiated to 'NoOpMap' in an eventual implementation.
  --
  -- Here 'hashToData' is an example of a phantom variable, which wouldn't be
  -- present in the formal specification, but it is needed in the executable
  -- spec to be able to generate traces.
  , forall hashAlgo (hashToDataMap :: * -> * -> *) commitData.
CRSt hashAlgo hashToDataMap commitData -> Set (Hash hashAlgo Data)
committedHashes :: !(Set (Hash hashAlgo Data))
  }

deriving instance
  Eq (hashToDataMap (Hash hashAlgo Data) commitData) =>
  Eq (CRSt hashAlgo hashToDataMap commitData)

deriving instance
  Show (hashToDataMap (Hash hashAlgo Data) commitData) =>
  Show (CRSt hashAlgo hashToDataMap commitData)

class MapLike m k v where
  insert :: k -> v -> m k v -> m k v

  delete :: k -> m k v -> m k v

data NoOpMap a b = NoOpMap

-- | This is the 'MapLike' instance one would use if the executable spec would
-- be used in an implementation (where no generators are needed).
instance MapLike NoOpMap a b where
  insert :: a -> b -> NoOpMap a b -> NoOpMap a b
insert a
_ b
_ NoOpMap a b
_ = forall a b. NoOpMap a b
NoOpMap

  delete :: a -> NoOpMap a b -> NoOpMap a b
delete a
_ NoOpMap a b
_ = forall a b. NoOpMap a b
NoOpMap

instance Ord k => MapLike Map k v where
  insert :: k -> v -> Map k v -> Map k v
insert = forall k v. Ord k => k -> v -> Map k v -> Map k v
Map.insert

  delete :: k -> Map k v -> Map k v
delete = forall k v. Ord k => k -> Map k v -> Map k v
Map.delete

data CRSignal hashAlgo commitData
  = Commit (Hash hashAlgo Data) commitData
  | Reveal Data
  deriving (CRSignal hashAlgo commitData
-> CRSignal hashAlgo commitData -> Bool
CRSignal hashAlgo commitData
-> CRSignal hashAlgo commitData -> Ordering
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall {hashAlgo} {commitData}.
Ord commitData =>
Eq (CRSignal hashAlgo commitData)
forall hashAlgo commitData.
Ord commitData =>
CRSignal hashAlgo commitData
-> CRSignal hashAlgo commitData -> Bool
forall hashAlgo commitData.
Ord commitData =>
CRSignal hashAlgo commitData
-> CRSignal hashAlgo commitData -> Ordering
forall hashAlgo commitData.
Ord commitData =>
CRSignal hashAlgo commitData
-> CRSignal hashAlgo commitData -> CRSignal hashAlgo commitData
min :: CRSignal hashAlgo commitData
-> CRSignal hashAlgo commitData -> CRSignal hashAlgo commitData
$cmin :: forall hashAlgo commitData.
Ord commitData =>
CRSignal hashAlgo commitData
-> CRSignal hashAlgo commitData -> CRSignal hashAlgo commitData
max :: CRSignal hashAlgo commitData
-> CRSignal hashAlgo commitData -> CRSignal hashAlgo commitData
$cmax :: forall hashAlgo commitData.
Ord commitData =>
CRSignal hashAlgo commitData
-> CRSignal hashAlgo commitData -> CRSignal hashAlgo commitData
>= :: CRSignal hashAlgo commitData
-> CRSignal hashAlgo commitData -> Bool
$c>= :: forall hashAlgo commitData.
Ord commitData =>
CRSignal hashAlgo commitData
-> CRSignal hashAlgo commitData -> Bool
> :: CRSignal hashAlgo commitData
-> CRSignal hashAlgo commitData -> Bool
$c> :: forall hashAlgo commitData.
Ord commitData =>
CRSignal hashAlgo commitData
-> CRSignal hashAlgo commitData -> Bool
<= :: CRSignal hashAlgo commitData
-> CRSignal hashAlgo commitData -> Bool
$c<= :: forall hashAlgo commitData.
Ord commitData =>
CRSignal hashAlgo commitData
-> CRSignal hashAlgo commitData -> Bool
< :: CRSignal hashAlgo commitData
-> CRSignal hashAlgo commitData -> Bool
$c< :: forall hashAlgo commitData.
Ord commitData =>
CRSignal hashAlgo commitData
-> CRSignal hashAlgo commitData -> Bool
compare :: CRSignal hashAlgo commitData
-> CRSignal hashAlgo commitData -> Ordering
$ccompare :: forall hashAlgo commitData.
Ord commitData =>
CRSignal hashAlgo commitData
-> CRSignal hashAlgo commitData -> Ordering
Ord, CRSignal hashAlgo commitData
-> CRSignal hashAlgo commitData -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall hashAlgo commitData.
Eq commitData =>
CRSignal hashAlgo commitData
-> CRSignal hashAlgo commitData -> Bool
/= :: CRSignal hashAlgo commitData
-> CRSignal hashAlgo commitData -> Bool
$c/= :: forall hashAlgo commitData.
Eq commitData =>
CRSignal hashAlgo commitData
-> CRSignal hashAlgo commitData -> Bool
== :: CRSignal hashAlgo commitData
-> CRSignal hashAlgo commitData -> Bool
$c== :: forall hashAlgo commitData.
Eq commitData =>
CRSignal hashAlgo commitData
-> CRSignal hashAlgo commitData -> Bool
Eq, Int -> CRSignal hashAlgo commitData -> ShowS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall hashAlgo commitData.
Show commitData =>
Int -> CRSignal hashAlgo commitData -> ShowS
forall hashAlgo commitData.
Show commitData =>
[CRSignal hashAlgo commitData] -> ShowS
forall hashAlgo commitData.
Show commitData =>
CRSignal hashAlgo commitData -> String
showList :: [CRSignal hashAlgo commitData] -> ShowS
$cshowList :: forall hashAlgo commitData.
Show commitData =>
[CRSignal hashAlgo commitData] -> ShowS
show :: CRSignal hashAlgo commitData -> String
$cshow :: forall hashAlgo commitData.
Show commitData =>
CRSignal hashAlgo commitData -> String
showsPrec :: Int -> CRSignal hashAlgo commitData -> ShowS
$cshowsPrec :: forall hashAlgo commitData.
Show commitData =>
Int -> CRSignal hashAlgo commitData -> ShowS
Show)

isCommit :: CRSignal hashAlgo commitData -> Bool
isCommit :: forall hashAlgo commitData. CRSignal hashAlgo commitData -> Bool
isCommit Commit {} = Bool
True
isCommit CRSignal hashAlgo commitData
_ = Bool
False

newtype Data = Data {Data -> (Id, Int)
getData :: (Id, Int)}
  deriving (Data -> Data -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Data -> Data -> Bool
$c/= :: Data -> Data -> Bool
== :: Data -> Data -> Bool
$c== :: Data -> Data -> Bool
Eq, Int -> Data -> ShowS
[Data] -> ShowS
Data -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Data] -> ShowS
$cshowList :: [Data] -> ShowS
show :: Data -> String
$cshow :: Data -> String
showsPrec :: Int -> Data -> ShowS
$cshowsPrec :: Int -> Data -> ShowS
Show, Typeable Data
Data -> Encoding
(forall t. EncCBOR t => Proxy t -> Size) -> Proxy [Data] -> Size
(forall t. EncCBOR t => Proxy t -> Size) -> Proxy Data -> Size
forall a.
Typeable a
-> (a -> Encoding)
-> ((forall t. EncCBOR t => Proxy t -> Size) -> Proxy a -> Size)
-> ((forall t. EncCBOR t => Proxy t -> Size) -> Proxy [a] -> Size)
-> EncCBOR a
encodedListSizeExpr :: (forall t. EncCBOR t => Proxy t -> Size) -> Proxy [Data] -> Size
$cencodedListSizeExpr :: (forall t. EncCBOR t => Proxy t -> Size) -> Proxy [Data] -> Size
encodedSizeExpr :: (forall t. EncCBOR t => Proxy t -> Size) -> Proxy Data -> Size
$cencodedSizeExpr :: (forall t. EncCBOR t => Proxy t -> Size) -> Proxy Data -> Size
encCBOR :: Data -> Encoding
$cencCBOR :: Data -> Encoding
EncCBOR, Eq Data
Data -> Data -> Bool
Data -> Data -> Ordering
Data -> Data -> Data
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Data -> Data -> Data
$cmin :: Data -> Data -> Data
max :: Data -> Data -> Data
$cmax :: Data -> Data -> Data
>= :: Data -> Data -> Bool
$c>= :: Data -> Data -> Bool
> :: Data -> Data -> Bool
$c> :: Data -> Data -> Bool
<= :: Data -> Data -> Bool
$c<= :: Data -> Data -> Bool
< :: Data -> Data -> Bool
$c< :: Data -> Data -> Bool
compare :: Data -> Data -> Ordering
$ccompare :: Data -> Data -> Ordering
Ord, Gen Data
Data -> [Data]
forall a. Gen a -> (a -> [a]) -> Arbitrary a
shrink :: Data -> [Data]
$cshrink :: Data -> [Data]
arbitrary :: Gen Data
$carbitrary :: Gen Data
Arbitrary)

newtype Id = Id {Id -> Int
getId :: Int}
  deriving (Id -> Id -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Id -> Id -> Bool
$c/= :: Id -> Id -> Bool
== :: Id -> Id -> Bool
$c== :: Id -> Id -> Bool
Eq, Int -> Id -> ShowS
[Id] -> ShowS
Id -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Id] -> ShowS
$cshowList :: [Id] -> ShowS
show :: Id -> String
$cshow :: Id -> String
showsPrec :: Int -> Id -> ShowS
$cshowsPrec :: Int -> Id -> ShowS
Show, Typeable Id
Id -> Encoding
(forall t. EncCBOR t => Proxy t -> Size) -> Proxy [Id] -> Size
(forall t. EncCBOR t => Proxy t -> Size) -> Proxy Id -> Size
forall a.
Typeable a
-> (a -> Encoding)
-> ((forall t. EncCBOR t => Proxy t -> Size) -> Proxy a -> Size)
-> ((forall t. EncCBOR t => Proxy t -> Size) -> Proxy [a] -> Size)
-> EncCBOR a
encodedListSizeExpr :: (forall t. EncCBOR t => Proxy t -> Size) -> Proxy [Id] -> Size
$cencodedListSizeExpr :: (forall t. EncCBOR t => Proxy t -> Size) -> Proxy [Id] -> Size
encodedSizeExpr :: (forall t. EncCBOR t => Proxy t -> Size) -> Proxy Id -> Size
$cencodedSizeExpr :: (forall t. EncCBOR t => Proxy t -> Size) -> Proxy Id -> Size
encCBOR :: Id -> Encoding
$cencCBOR :: Id -> Encoding
EncCBOR, Eq Id
Id -> Id -> Bool
Id -> Id -> Ordering
Id -> Id -> Id
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Id -> Id -> Id
$cmin :: Id -> Id -> Id
max :: Id -> Id -> Id
$cmax :: Id -> Id -> Id
>= :: Id -> Id -> Bool
$c>= :: Id -> Id -> Bool
> :: Id -> Id -> Bool
$c> :: Id -> Id -> Bool
<= :: Id -> Id -> Bool
$c<= :: Id -> Id -> Bool
< :: Id -> Id -> Bool
$c< :: Id -> Id -> Bool
compare :: Id -> Id -> Ordering
$ccompare :: Id -> Id -> Ordering
Ord, Gen Id
Id -> [Id]
forall a. Gen a -> (a -> [a]) -> Arbitrary a
shrink :: Id -> [Id]
$cshrink :: Id -> [Id]
arbitrary :: Gen Id
$carbitrary :: Gen Id
Arbitrary)

data CRPredicateFailure hashAlgo (hashToDataMap :: Type -> Type -> Type) commitData
  = InvalidReveal Data
  | AlreadyComitted (Hash hashAlgo Data)
  deriving (CRPredicateFailure hashAlgo hashToDataMap commitData
-> CRPredicateFailure hashAlgo hashToDataMap commitData -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall hashAlgo (hashToDataMap :: * -> * -> *) commitData.
CRPredicateFailure hashAlgo hashToDataMap commitData
-> CRPredicateFailure hashAlgo hashToDataMap commitData -> Bool
/= :: CRPredicateFailure hashAlgo hashToDataMap commitData
-> CRPredicateFailure hashAlgo hashToDataMap commitData -> Bool
$c/= :: forall hashAlgo (hashToDataMap :: * -> * -> *) commitData.
CRPredicateFailure hashAlgo hashToDataMap commitData
-> CRPredicateFailure hashAlgo hashToDataMap commitData -> Bool
== :: CRPredicateFailure hashAlgo hashToDataMap commitData
-> CRPredicateFailure hashAlgo hashToDataMap commitData -> Bool
$c== :: forall hashAlgo (hashToDataMap :: * -> * -> *) commitData.
CRPredicateFailure hashAlgo hashToDataMap commitData
-> CRPredicateFailure hashAlgo hashToDataMap commitData -> Bool
Eq, Int
-> CRPredicateFailure hashAlgo hashToDataMap commitData -> ShowS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall hashAlgo (hashToDataMap :: * -> * -> *) commitData.
Int
-> CRPredicateFailure hashAlgo hashToDataMap commitData -> ShowS
forall hashAlgo (hashToDataMap :: * -> * -> *) commitData.
[CRPredicateFailure hashAlgo hashToDataMap commitData] -> ShowS
forall hashAlgo (hashToDataMap :: * -> * -> *) commitData.
CRPredicateFailure hashAlgo hashToDataMap commitData -> String
showList :: [CRPredicateFailure hashAlgo hashToDataMap commitData] -> ShowS
$cshowList :: forall hashAlgo (hashToDataMap :: * -> * -> *) commitData.
[CRPredicateFailure hashAlgo hashToDataMap commitData] -> ShowS
show :: CRPredicateFailure hashAlgo hashToDataMap commitData -> String
$cshow :: forall hashAlgo (hashToDataMap :: * -> * -> *) commitData.
CRPredicateFailure hashAlgo hashToDataMap commitData -> String
showsPrec :: Int
-> CRPredicateFailure hashAlgo hashToDataMap commitData -> ShowS
$cshowsPrec :: forall hashAlgo (hashToDataMap :: * -> * -> *) commitData.
Int
-> CRPredicateFailure hashAlgo hashToDataMap commitData -> ShowS
Show)

instance
  ( HashAlgorithm hashAlgo
  , Typeable hashToDataMap
  , Typeable commitData
  , MapLike hashToDataMap (Hash hashAlgo Data) commitData
  , Monoid (hashToDataMap (Hash hashAlgo Data) commitData)
  ) =>
  STS (CR hashAlgo hashToDataMap commitData)
  where
  type Environment (CR hashAlgo hashToDataMap commitData) = ()

  type
    State (CR hashAlgo hashToDataMap commitData) =
      CRSt hashAlgo hashToDataMap commitData

  type
    Signal (CR hashAlgo hashToDataMap commitData) =
      CRSignal hashAlgo commitData

  type
    PredicateFailure (CR hashAlgo hashToDataMap commitData) =
      CRPredicateFailure hashAlgo hashToDataMap commitData

  initialRules :: [InitialRule (CR hashAlgo hashToDataMap commitData)]
initialRules =
    [ forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$!
        CRSt
          { hashToData :: hashToDataMap (Hash hashAlgo Data) commitData
hashToData = forall a. Monoid a => a
mempty
          , committedHashes :: Set (Hash hashAlgo Data)
committedHashes = forall a. Set a
Set.empty
          }
    ]

  transitionRules :: [TransitionRule (CR hashAlgo hashToDataMap commitData)]
transitionRules =
    [ do
        TRC ((), CRSt {hashToDataMap (Hash hashAlgo Data) commitData
hashToData :: hashToDataMap (Hash hashAlgo Data) commitData
hashToData :: forall hashAlgo (hashToDataMap :: * -> * -> *) commitData.
CRSt hashAlgo hashToDataMap commitData
-> hashToDataMap (Hash hashAlgo Data) commitData
hashToData, Set (Hash hashAlgo Data)
committedHashes :: Set (Hash hashAlgo Data)
committedHashes :: forall hashAlgo (hashToDataMap :: * -> * -> *) commitData.
CRSt hashAlgo hashToDataMap commitData -> Set (Hash hashAlgo Data)
committedHashes}, Signal (CR hashAlgo hashToDataMap commitData)
crSignal) <- forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
        case Signal (CR hashAlgo hashToDataMap commitData)
crSignal of
          Commit Hash hashAlgo Data
dataHash commitData
commitData -> do
            Hash hashAlgo Data
dataHash forall a. Ord a => a -> Set a -> Bool
`Set.notMember` Set (Hash hashAlgo Data)
committedHashes forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! forall hashAlgo (hashToDataMap :: * -> * -> *) commitData.
Hash hashAlgo Data
-> CRPredicateFailure hashAlgo hashToDataMap commitData
AlreadyComitted Hash hashAlgo Data
dataHash
            forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$!
              CRSt
                { hashToData :: hashToDataMap (Hash hashAlgo Data) commitData
hashToData = forall (m :: * -> * -> *) k v.
MapLike m k v =>
k -> v -> m k v -> m k v
insert Hash hashAlgo Data
dataHash commitData
commitData hashToDataMap (Hash hashAlgo Data) commitData
hashToData
                , committedHashes :: Set (Hash hashAlgo Data)
committedHashes = forall a. Ord a => a -> Set a -> Set a
Set.insert Hash hashAlgo Data
dataHash Set (Hash hashAlgo Data)
committedHashes
                }
          Reveal Data
someData -> do
            forall h a.
(HashAlgorithm h, EncCBOR a) =>
Version -> a -> Hash h a
hashEncCBOR forall a. Bounded a => a
minBound Data
someData
              forall a. Ord a => a -> Set a -> Bool
`Set.member` Set (Hash hashAlgo Data)
committedHashes
              forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! forall hashAlgo (hashToDataMap :: * -> * -> *) commitData.
Data -> CRPredicateFailure hashAlgo hashToDataMap commitData
InvalidReveal Data
someData
            forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$!
              CRSt
                { hashToData :: hashToDataMap (Hash hashAlgo Data) commitData
hashToData =
                    forall (m :: * -> * -> *) k v. MapLike m k v => k -> m k v -> m k v
delete
                      (forall h a.
(HashAlgorithm h, EncCBOR a) =>
Version -> a -> Hash h a
hashEncCBOR forall a. Bounded a => a
minBound Data
someData)
                      hashToDataMap (Hash hashAlgo Data) commitData
hashToData
                , committedHashes :: Set (Hash hashAlgo Data)
committedHashes =
                    forall a. Ord a => a -> Set a -> Set a
Set.delete
                      (forall h a.
(HashAlgorithm h, EncCBOR a) =>
Version -> a -> Hash h a
hashEncCBOR forall a. Bounded a => a
minBound Data
someData)
                      Set (Hash hashAlgo Data)
committedHashes
                }
    ]

instance
  HashAlgorithm hashAlgo =>
  STS.Gen.HasTrace (CR hashAlgo Map Data) ()
  where
  envGen :: HasCallStack => () -> Gen (Environment (CR hashAlgo Map Data))
envGen ()
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

  sigGen :: HasCallStack =>
()
-> Environment (CR hashAlgo Map Data)
-> State (CR hashAlgo Map Data)
-> Gen (Signal (CR hashAlgo Map Data))
sigGen () () CRSt {Map (Hash hashAlgo Data) Data
hashToData :: Map (Hash hashAlgo Data) Data
hashToData :: forall hashAlgo (hashToDataMap :: * -> * -> *) commitData.
CRSt hashAlgo hashToDataMap commitData
-> hashToDataMap (Hash hashAlgo Data) commitData
hashToData, Set (Hash hashAlgo Data)
committedHashes :: Set (Hash hashAlgo Data)
committedHashes :: forall hashAlgo (hashToDataMap :: * -> * -> *) commitData.
CRSt hashAlgo hashToDataMap commitData -> Set (Hash hashAlgo Data)
committedHashes} =
    if forall a. Set a -> Bool
Set.null Set (Hash hashAlgo Data)
committedHashes
      then Gen (CRSignal hashAlgo Data)
genCommit
      else forall a. HasCallStack => [Gen a] -> Gen a
oneof [Gen (CRSignal hashAlgo Data)
genCommit, Gen (CRSignal hashAlgo Data)
genReveal]
    where
      genCommit :: Gen (CRSignal hashAlgo Data)
genCommit = do
        Id
id <- Int -> Id
Id forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Arbitrary a => Gen a
arbitrary
        Int
n <- forall a. Random a => (a, a) -> Gen a
choose (-Int
2, Int
2)
        let newData :: Data
newData = (Id, Int) -> Data
Data (Id
id, Int
n)
        forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! forall hashAlgo commitData.
Hash hashAlgo Data -> commitData -> CRSignal hashAlgo commitData
Commit (forall h a.
(HashAlgorithm h, EncCBOR a) =>
Version -> a -> Hash h a
hashEncCBOR forall a. Bounded a => a
minBound Data
newData) Data
newData
      genReveal :: Gen (CRSignal hashAlgo Data)
genReveal = do
        Hash hashAlgo Data
hashToReveal <- forall a. HasCallStack => [a] -> Gen a
elements forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList Set (Hash hashAlgo Data)
committedHashes
        let dataToReveal :: Data
dataToReveal = Map (Hash hashAlgo Data) Data
hashToData forall k a. Ord k => Map k a -> k -> a
Map.! Hash hashAlgo Data
hashToReveal
        forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! forall hashAlgo commitData. Data -> CRSignal hashAlgo commitData
Reveal Data
dataToReveal

  shrinkSignal :: HasCallStack =>
Signal (CR hashAlgo Map Data) -> [Signal (CR hashAlgo Map Data)]
shrinkSignal (Commit Hash hashAlgo Data
_ Data
someData) =
    forall {hashAlgo}.
HashAlgorithm hashAlgo =>
Data -> CRSignal hashAlgo Data
recalculateCommit forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Arbitrary a => a -> [a]
shrink Data
someData
    where
      recalculateCommit :: Data -> CRSignal hashAlgo Data
recalculateCommit Data
shrunkData =
        forall hashAlgo commitData.
Hash hashAlgo Data -> commitData -> CRSignal hashAlgo commitData
Commit
          (forall h a.
(HashAlgorithm h, EncCBOR a) =>
Version -> a -> Hash h a
hashEncCBOR forall a. Bounded a => a
minBound Data
shrunkData)
          Data
shrunkData
  shrinkSignal (Reveal Data
someData) = forall hashAlgo commitData. Data -> CRSignal hashAlgo commitData
Reveal forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Arbitrary a => a -> [a]
shrink Data
someData

-- | Check that unique data is generated. This is supposed to fail, since
-- there's nothing in the STS that prevents two commits of the same data. The
-- resulting minimal counterexample should be a trace of the form:
--
-- > commit (hash d0) -> reveal d0 -> commit (hash d0)
--
-- where it shouldn't be possible to shrink @d0@ any further.
prop_qc_UniqueData :: Property
prop_qc_UniqueData :: Property
prop_qc_UniqueData =
  forall sts traceGenEnv prop.
(HasTrace sts traceGenEnv, Testable prop,
 Show (Environment sts)) =>
BaseEnv sts
-> Word64 -> traceGenEnv -> (Trace sts -> prop) -> Property
STS.Gen.forAllTrace @(CR ShortHash Map Data) @()
    ()
    Word64
100
    ()
    ([CRSignal ShortHash Data] -> Bool
noDuplicatedData forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s. TraceOrder -> Trace s -> [Signal s]
Trace.traceSignals TraceOrder
Trace.OldestFirst)
  where
    noDuplicatedData :: [CRSignal ShortHash Data] -> Bool
    noDuplicatedData :: [CRSignal ShortHash Data] -> Bool
noDuplicatedData = forall a. Ord a => [a] -> Bool
allUnique forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Bool) -> [a] -> [a]
filter forall hashAlgo commitData. CRSignal hashAlgo commitData -> Bool
isCommit

-- | Check that only valid signals are generated.
--
-- This property should fail since the generators don't check that the generated
-- commits are unique. The resulting minimal counterexample should be a trace of
-- the form:
--
-- > commit (hash d0) -> commit (hash d0)
--
-- where it shouldn't be possible to shrink @d0@ any further.
prop_qc_OnlyValidSignals :: Property
prop_qc_OnlyValidSignals :: Property
prop_qc_OnlyValidSignals =
  forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
5000 forall a b. (a -> b) -> a -> b
$ -- We need to test a large
  -- number of times to make sure
  -- we get a collision in the
  -- generated data
    forall sts traceGenEnv.
(HasTrace sts traceGenEnv, Show (Environment sts),
 Show (Signal sts)) =>
BaseEnv sts -> Word64 -> traceGenEnv -> Property
STS.Gen.onlyValidSignalsAreGenerated @(CR ShortHash Map Data) @() () Word64
150 ()