{-# 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
_ = NoOpMap a b
forall a b. NoOpMap a b
NoOpMap

  delete :: a -> NoOpMap a b -> NoOpMap a b
delete a
_ NoOpMap a b
_ = 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 = k -> v -> Map k v -> Map k v
forall k v. Ord k => k -> v -> Map k v -> Map k v
Map.insert

  delete :: k -> Map k v -> Map k v
delete = k -> Map k v -> Map k v
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 (Eq (CRSignal hashAlgo commitData)
Eq (CRSignal hashAlgo commitData) =>
(CRSignal hashAlgo commitData
 -> CRSignal hashAlgo commitData -> Ordering)
-> (CRSignal hashAlgo commitData
    -> CRSignal hashAlgo commitData -> Bool)
-> (CRSignal hashAlgo commitData
    -> CRSignal hashAlgo commitData -> Bool)
-> (CRSignal hashAlgo commitData
    -> CRSignal hashAlgo commitData -> Bool)
-> (CRSignal hashAlgo commitData
    -> CRSignal hashAlgo commitData -> Bool)
-> (CRSignal hashAlgo commitData
    -> CRSignal hashAlgo commitData -> CRSignal hashAlgo commitData)
-> (CRSignal hashAlgo commitData
    -> CRSignal hashAlgo commitData -> CRSignal hashAlgo commitData)
-> Ord (CRSignal hashAlgo commitData)
CRSignal hashAlgo commitData
-> CRSignal hashAlgo commitData -> Bool
CRSignal hashAlgo commitData
-> CRSignal hashAlgo commitData -> Ordering
CRSignal hashAlgo commitData
-> CRSignal hashAlgo commitData -> CRSignal hashAlgo commitData
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
$ccompare :: forall hashAlgo commitData.
Ord commitData =>
CRSignal hashAlgo commitData
-> CRSignal hashAlgo commitData -> Ordering
compare :: CRSignal hashAlgo commitData
-> CRSignal hashAlgo commitData -> Ordering
$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
>= :: CRSignal hashAlgo commitData
-> CRSignal hashAlgo commitData -> Bool
$cmax :: forall hashAlgo commitData.
Ord commitData =>
CRSignal hashAlgo commitData
-> CRSignal hashAlgo commitData -> CRSignal hashAlgo commitData
max :: CRSignal hashAlgo commitData
-> CRSignal hashAlgo commitData -> CRSignal hashAlgo commitData
$cmin :: forall hashAlgo commitData.
Ord commitData =>
CRSignal hashAlgo commitData
-> CRSignal hashAlgo commitData -> CRSignal hashAlgo commitData
min :: CRSignal hashAlgo commitData
-> CRSignal hashAlgo commitData -> CRSignal hashAlgo commitData
Ord, CRSignal hashAlgo commitData
-> CRSignal hashAlgo commitData -> Bool
(CRSignal hashAlgo commitData
 -> CRSignal hashAlgo commitData -> Bool)
-> (CRSignal hashAlgo commitData
    -> CRSignal hashAlgo commitData -> Bool)
-> Eq (CRSignal hashAlgo commitData)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall hashAlgo commitData.
Eq commitData =>
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
/= :: CRSignal hashAlgo commitData
-> CRSignal hashAlgo commitData -> Bool
Eq, Int -> CRSignal hashAlgo commitData -> ShowS
[CRSignal hashAlgo commitData] -> ShowS
CRSignal hashAlgo commitData -> String
(Int -> CRSignal hashAlgo commitData -> ShowS)
-> (CRSignal hashAlgo commitData -> String)
-> ([CRSignal hashAlgo commitData] -> ShowS)
-> Show (CRSignal hashAlgo commitData)
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
$cshowsPrec :: forall hashAlgo commitData.
Show commitData =>
Int -> CRSignal hashAlgo commitData -> ShowS
showsPrec :: Int -> CRSignal hashAlgo commitData -> ShowS
$cshow :: forall hashAlgo commitData.
Show commitData =>
CRSignal hashAlgo commitData -> String
show :: CRSignal hashAlgo commitData -> String
$cshowList :: forall hashAlgo commitData.
Show commitData =>
[CRSignal hashAlgo commitData] -> ShowS
showList :: [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
(Data -> Data -> Bool) -> (Data -> Data -> Bool) -> Eq Data
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Data -> Data -> Bool
== :: Data -> Data -> Bool
$c/= :: Data -> Data -> Bool
/= :: Data -> Data -> Bool
Eq, Int -> Data -> ShowS
[Data] -> ShowS
Data -> String
(Int -> Data -> ShowS)
-> (Data -> String) -> ([Data] -> ShowS) -> Show Data
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Data -> ShowS
showsPrec :: Int -> Data -> ShowS
$cshow :: Data -> String
show :: Data -> String
$cshowList :: [Data] -> ShowS
showList :: [Data] -> ShowS
Show, Typeable Data
Typeable Data =>
(Data -> Encoding)
-> ((forall t. EncCBOR t => Proxy t -> Size) -> Proxy Data -> Size)
-> ((forall t. EncCBOR t => Proxy t -> Size)
    -> Proxy [Data] -> Size)
-> EncCBOR 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
$cencCBOR :: Data -> Encoding
encCBOR :: Data -> Encoding
$cencodedSizeExpr :: (forall t. EncCBOR t => Proxy t -> Size) -> Proxy Data -> Size
encodedSizeExpr :: (forall t. EncCBOR t => Proxy t -> Size) -> Proxy Data -> Size
$cencodedListSizeExpr :: (forall t. EncCBOR t => Proxy t -> Size) -> Proxy [Data] -> Size
encodedListSizeExpr :: (forall t. EncCBOR t => Proxy t -> Size) -> Proxy [Data] -> Size
EncCBOR, Eq Data
Eq Data =>
(Data -> Data -> Ordering)
-> (Data -> Data -> Bool)
-> (Data -> Data -> Bool)
-> (Data -> Data -> Bool)
-> (Data -> Data -> Bool)
-> (Data -> Data -> Data)
-> (Data -> Data -> Data)
-> Ord 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
$ccompare :: Data -> Data -> Ordering
compare :: Data -> Data -> Ordering
$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
>= :: Data -> Data -> Bool
$cmax :: Data -> Data -> Data
max :: Data -> Data -> Data
$cmin :: Data -> Data -> Data
min :: Data -> Data -> Data
Ord, Gen Data
Gen Data -> (Data -> [Data]) -> Arbitrary Data
Data -> [Data]
forall a. Gen a -> (a -> [a]) -> Arbitrary a
$carbitrary :: Gen Data
arbitrary :: Gen Data
$cshrink :: Data -> [Data]
shrink :: Data -> [Data]
Arbitrary)

newtype Id = Id {Id -> Int
getId :: Int}
  deriving (Id -> Id -> Bool
(Id -> Id -> Bool) -> (Id -> Id -> Bool) -> Eq Id
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Id -> Id -> Bool
== :: Id -> Id -> Bool
$c/= :: Id -> Id -> Bool
/= :: Id -> Id -> Bool
Eq, Int -> Id -> ShowS
[Id] -> ShowS
Id -> String
(Int -> Id -> ShowS)
-> (Id -> String) -> ([Id] -> ShowS) -> Show Id
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Id -> ShowS
showsPrec :: Int -> Id -> ShowS
$cshow :: Id -> String
show :: Id -> String
$cshowList :: [Id] -> ShowS
showList :: [Id] -> ShowS
Show, Typeable Id
Typeable Id =>
(Id -> Encoding)
-> ((forall t. EncCBOR t => Proxy t -> Size) -> Proxy Id -> Size)
-> ((forall t. EncCBOR t => Proxy t -> Size) -> Proxy [Id] -> Size)
-> EncCBOR 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
$cencCBOR :: Id -> Encoding
encCBOR :: Id -> Encoding
$cencodedSizeExpr :: (forall t. EncCBOR t => Proxy t -> Size) -> Proxy Id -> Size
encodedSizeExpr :: (forall t. EncCBOR t => Proxy t -> Size) -> Proxy Id -> Size
$cencodedListSizeExpr :: (forall t. EncCBOR t => Proxy t -> Size) -> Proxy [Id] -> Size
encodedListSizeExpr :: (forall t. EncCBOR t => Proxy t -> Size) -> Proxy [Id] -> Size
EncCBOR, Eq Id
Eq Id =>
(Id -> Id -> Ordering)
-> (Id -> Id -> Bool)
-> (Id -> Id -> Bool)
-> (Id -> Id -> Bool)
-> (Id -> Id -> Bool)
-> (Id -> Id -> Id)
-> (Id -> Id -> Id)
-> Ord 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
$ccompare :: Id -> Id -> Ordering
compare :: Id -> Id -> Ordering
$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
>= :: Id -> Id -> Bool
$cmax :: Id -> Id -> Id
max :: Id -> Id -> Id
$cmin :: Id -> Id -> Id
min :: Id -> Id -> Id
Ord, Gen Id
Gen Id -> (Id -> [Id]) -> Arbitrary Id
Id -> [Id]
forall a. Gen a -> (a -> [a]) -> Arbitrary a
$carbitrary :: Gen Id
arbitrary :: Gen Id
$cshrink :: Id -> [Id]
shrink :: Id -> [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
(CRPredicateFailure hashAlgo hashToDataMap commitData
 -> CRPredicateFailure hashAlgo hashToDataMap commitData -> Bool)
-> (CRPredicateFailure hashAlgo hashToDataMap commitData
    -> CRPredicateFailure hashAlgo hashToDataMap commitData -> Bool)
-> Eq (CRPredicateFailure hashAlgo hashToDataMap commitData)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall hashAlgo (hashToDataMap :: * -> * -> *) commitData.
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
/= :: CRPredicateFailure hashAlgo hashToDataMap commitData
-> CRPredicateFailure hashAlgo hashToDataMap commitData -> Bool
Eq, Int
-> CRPredicateFailure hashAlgo hashToDataMap commitData -> ShowS
[CRPredicateFailure hashAlgo hashToDataMap commitData] -> ShowS
CRPredicateFailure hashAlgo hashToDataMap commitData -> String
(Int
 -> CRPredicateFailure hashAlgo hashToDataMap commitData -> ShowS)
-> (CRPredicateFailure hashAlgo hashToDataMap commitData -> String)
-> ([CRPredicateFailure hashAlgo hashToDataMap commitData]
    -> ShowS)
-> Show (CRPredicateFailure hashAlgo hashToDataMap commitData)
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
$cshowsPrec :: forall hashAlgo (hashToDataMap :: * -> * -> *) commitData.
Int
-> CRPredicateFailure hashAlgo hashToDataMap commitData -> ShowS
showsPrec :: Int
-> CRPredicateFailure hashAlgo hashToDataMap commitData -> ShowS
$cshow :: forall hashAlgo (hashToDataMap :: * -> * -> *) commitData.
CRPredicateFailure hashAlgo hashToDataMap commitData -> String
show :: CRPredicateFailure hashAlgo hashToDataMap commitData -> String
$cshowList :: forall hashAlgo (hashToDataMap :: * -> * -> *) commitData.
[CRPredicateFailure hashAlgo hashToDataMap commitData] -> ShowS
showList :: [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 =
    [ CRSt hashAlgo hashToDataMap commitData
-> F (Clause (CR hashAlgo hashToDataMap commitData) 'Initial)
     (CRSt hashAlgo hashToDataMap commitData)
forall a.
a -> F (Clause (CR hashAlgo hashToDataMap commitData) 'Initial) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CRSt hashAlgo hashToDataMap commitData
 -> F (Clause (CR hashAlgo hashToDataMap commitData) 'Initial)
      (CRSt hashAlgo hashToDataMap commitData))
-> CRSt hashAlgo hashToDataMap commitData
-> F (Clause (CR hashAlgo hashToDataMap commitData) 'Initial)
     (CRSt hashAlgo hashToDataMap commitData)
forall a b. (a -> b) -> a -> b
$!
        CRSt
          { hashToData :: hashToDataMap (Hash hashAlgo Data) commitData
hashToData = hashToDataMap (Hash hashAlgo Data) commitData
forall a. Monoid a => a
mempty
          , committedHashes :: Set (Hash hashAlgo Data)
committedHashes = Set (Hash hashAlgo Data)
forall a. Set a
Set.empty
          }
    ]

  transitionRules :: [TransitionRule (CR hashAlgo hashToDataMap commitData)]
transitionRules =
    [ do
        TRC ((), CRSt {hashToDataMap (Hash hashAlgo Data) commitData
hashToData :: forall hashAlgo (hashToDataMap :: * -> * -> *) commitData.
CRSt hashAlgo hashToDataMap commitData
-> hashToDataMap (Hash hashAlgo Data) commitData
hashToData :: hashToDataMap (Hash hashAlgo Data) commitData
hashToData, Set (Hash hashAlgo Data)
committedHashes :: forall hashAlgo (hashToDataMap :: * -> * -> *) commitData.
CRSt hashAlgo hashToDataMap commitData -> Set (Hash hashAlgo Data)
committedHashes :: Set (Hash hashAlgo Data)
committedHashes}, Signal (CR hashAlgo hashToDataMap commitData)
crSignal) <- Rule
  (CR hashAlgo hashToDataMap commitData)
  'Transition
  (RuleContext 'Transition (CR hashAlgo hashToDataMap commitData))
F (Clause (CR hashAlgo hashToDataMap commitData) 'Transition)
  (TRC (CR hashAlgo hashToDataMap commitData))
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 Hash hashAlgo Data -> Set (Hash hashAlgo Data) -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.notMember` Set (Hash hashAlgo Data)
committedHashes Bool
-> PredicateFailure (CR hashAlgo hashToDataMap commitData)
-> Rule (CR hashAlgo hashToDataMap commitData) 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! Hash hashAlgo Data
-> CRPredicateFailure hashAlgo hashToDataMap commitData
forall hashAlgo (hashToDataMap :: * -> * -> *) commitData.
Hash hashAlgo Data
-> CRPredicateFailure hashAlgo hashToDataMap commitData
AlreadyComitted Hash hashAlgo Data
dataHash
            CRSt hashAlgo hashToDataMap commitData
-> F (Clause (CR hashAlgo hashToDataMap commitData) 'Transition)
     (CRSt hashAlgo hashToDataMap commitData)
forall a.
a
-> F (Clause (CR hashAlgo hashToDataMap commitData) 'Transition) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CRSt hashAlgo hashToDataMap commitData
 -> F (Clause (CR hashAlgo hashToDataMap commitData) 'Transition)
      (CRSt hashAlgo hashToDataMap commitData))
-> CRSt hashAlgo hashToDataMap commitData
-> F (Clause (CR hashAlgo hashToDataMap commitData) 'Transition)
     (CRSt hashAlgo hashToDataMap commitData)
forall a b. (a -> b) -> a -> b
$!
              CRSt
                { hashToData :: hashToDataMap (Hash hashAlgo Data) commitData
hashToData = Hash hashAlgo Data
-> commitData
-> hashToDataMap (Hash hashAlgo Data) commitData
-> hashToDataMap (Hash hashAlgo Data) commitData
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 = Hash hashAlgo Data
-> Set (Hash hashAlgo Data) -> Set (Hash hashAlgo Data)
forall a. Ord a => a -> Set a -> Set a
Set.insert Hash hashAlgo Data
dataHash Set (Hash hashAlgo Data)
committedHashes
                }
          Reveal Data
someData -> do
            Version -> Data -> Hash hashAlgo Data
forall h a.
(HashAlgorithm h, EncCBOR a) =>
Version -> a -> Hash h a
hashEncCBOR Version
forall a. Bounded a => a
minBound Data
someData
              Hash hashAlgo Data -> Set (Hash hashAlgo Data) -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set (Hash hashAlgo Data)
committedHashes
              Bool
-> PredicateFailure (CR hashAlgo hashToDataMap commitData)
-> Rule (CR hashAlgo hashToDataMap commitData) 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! Data -> CRPredicateFailure hashAlgo hashToDataMap commitData
forall hashAlgo (hashToDataMap :: * -> * -> *) commitData.
Data -> CRPredicateFailure hashAlgo hashToDataMap commitData
InvalidReveal Data
someData
            CRSt hashAlgo hashToDataMap commitData
-> F (Clause (CR hashAlgo hashToDataMap commitData) 'Transition)
     (CRSt hashAlgo hashToDataMap commitData)
forall a.
a
-> F (Clause (CR hashAlgo hashToDataMap commitData) 'Transition) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CRSt hashAlgo hashToDataMap commitData
 -> F (Clause (CR hashAlgo hashToDataMap commitData) 'Transition)
      (CRSt hashAlgo hashToDataMap commitData))
-> CRSt hashAlgo hashToDataMap commitData
-> F (Clause (CR hashAlgo hashToDataMap commitData) 'Transition)
     (CRSt hashAlgo hashToDataMap commitData)
forall a b. (a -> b) -> a -> b
$!
              CRSt
                { hashToData :: hashToDataMap (Hash hashAlgo Data) commitData
hashToData =
                    Hash hashAlgo Data
-> hashToDataMap (Hash hashAlgo Data) commitData
-> hashToDataMap (Hash hashAlgo Data) commitData
forall (m :: * -> * -> *) k v. MapLike m k v => k -> m k v -> m k v
delete
                      (Version -> Data -> Hash hashAlgo Data
forall h a.
(HashAlgorithm h, EncCBOR a) =>
Version -> a -> Hash h a
hashEncCBOR Version
forall a. Bounded a => a
minBound Data
someData)
                      hashToDataMap (Hash hashAlgo Data) commitData
hashToData
                , committedHashes :: Set (Hash hashAlgo Data)
committedHashes =
                    Hash hashAlgo Data
-> Set (Hash hashAlgo Data) -> Set (Hash hashAlgo Data)
forall a. Ord a => a -> Set a -> Set a
Set.delete
                      (Version -> Data -> Hash hashAlgo Data
forall h a.
(HashAlgorithm h, EncCBOR a) =>
Version -> a -> Hash h a
hashEncCBOR Version
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 ()
_ = () -> Gen ()
forall a. a -> Gen a
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 :: forall hashAlgo (hashToDataMap :: * -> * -> *) commitData.
CRSt hashAlgo hashToDataMap commitData
-> hashToDataMap (Hash hashAlgo Data) commitData
hashToData :: Map (Hash hashAlgo Data) Data
hashToData, Set (Hash hashAlgo Data)
committedHashes :: forall hashAlgo (hashToDataMap :: * -> * -> *) commitData.
CRSt hashAlgo hashToDataMap commitData -> Set (Hash hashAlgo Data)
committedHashes :: Set (Hash hashAlgo Data)
committedHashes} =
    if Set (Hash hashAlgo Data) -> Bool
forall a. Set a -> Bool
Set.null Set (Hash hashAlgo Data)
committedHashes
      then Gen (Signal (CR hashAlgo Map Data))
Gen (CRSignal hashAlgo Data)
genCommit
      else [Gen (CRSignal hashAlgo Data)] -> Gen (CRSignal hashAlgo Data)
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 (Int -> Id) -> Gen Int -> Gen Id
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Int
forall a. Arbitrary a => Gen a
arbitrary
        Int
n <- (Int, Int) -> Gen Int
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)
        CRSignal hashAlgo Data -> Gen (CRSignal hashAlgo Data)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CRSignal hashAlgo Data -> Gen (CRSignal hashAlgo Data))
-> CRSignal hashAlgo Data -> Gen (CRSignal hashAlgo Data)
forall a b. (a -> b) -> a -> b
$! Hash hashAlgo Data -> Data -> CRSignal hashAlgo Data
forall hashAlgo commitData.
Hash hashAlgo Data -> commitData -> CRSignal hashAlgo commitData
Commit (Version -> Data -> Hash hashAlgo Data
forall h a.
(HashAlgorithm h, EncCBOR a) =>
Version -> a -> Hash h a
hashEncCBOR Version
forall a. Bounded a => a
minBound Data
newData) Data
newData
      genReveal :: Gen (CRSignal hashAlgo Data)
genReveal = do
        Hash hashAlgo Data
hashToReveal <- [Hash hashAlgo Data] -> Gen (Hash hashAlgo Data)
forall a. HasCallStack => [a] -> Gen a
elements ([Hash hashAlgo Data] -> Gen (Hash hashAlgo Data))
-> [Hash hashAlgo Data] -> Gen (Hash hashAlgo Data)
forall a b. (a -> b) -> a -> b
$ Set (Hash hashAlgo Data) -> [Hash hashAlgo Data]
forall a. Set a -> [a]
Set.toList Set (Hash hashAlgo Data)
committedHashes
        let dataToReveal :: Data
dataToReveal = Map (Hash hashAlgo Data) Data
hashToData Map (Hash hashAlgo Data) Data -> Hash hashAlgo Data -> Data
forall k a. Ord k => Map k a -> k -> a
Map.! Hash hashAlgo Data
hashToReveal
        CRSignal hashAlgo Data -> Gen (CRSignal hashAlgo Data)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CRSignal hashAlgo Data -> Gen (CRSignal hashAlgo Data))
-> CRSignal hashAlgo Data -> Gen (CRSignal hashAlgo Data)
forall a b. (a -> b) -> a -> b
$! Data -> CRSignal hashAlgo Data
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) =
    Data -> CRSignal hashAlgo Data
forall {hashAlgo}.
HashAlgorithm hashAlgo =>
Data -> CRSignal hashAlgo Data
recalculateCommit (Data -> CRSignal hashAlgo Data)
-> [Data] -> [CRSignal hashAlgo Data]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Data -> [Data]
forall a. Arbitrary a => a -> [a]
shrink Data
someData
    where
      recalculateCommit :: Data -> CRSignal hashAlgo Data
recalculateCommit Data
shrunkData =
        Hash hashAlgo Data -> Data -> CRSignal hashAlgo Data
forall hashAlgo commitData.
Hash hashAlgo Data -> commitData -> CRSignal hashAlgo commitData
Commit
          (Version -> Data -> Hash hashAlgo Data
forall h a.
(HashAlgorithm h, EncCBOR a) =>
Version -> a -> Hash h a
hashEncCBOR Version
forall a. Bounded a => a
minBound Data
shrunkData)
          Data
shrunkData
  shrinkSignal (Reveal Data
someData) = Data -> CRSignal hashAlgo Data
forall hashAlgo commitData. Data -> CRSignal hashAlgo commitData
Reveal (Data -> CRSignal hashAlgo Data)
-> [Data] -> [CRSignal hashAlgo Data]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Data -> [Data]
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 ([CRSignal ShortHash Data] -> Bool)
-> (Trace (CR ShortHash Map Data) -> [CRSignal ShortHash Data])
-> Trace (CR ShortHash Map Data)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TraceOrder
-> Trace (CR ShortHash Map Data)
-> [Signal (CR ShortHash Map Data)]
forall s. TraceOrder -> Trace s -> [Signal s]
Trace.traceSignals TraceOrder
Trace.OldestFirst)
  where
    noDuplicatedData :: [CRSignal ShortHash Data] -> Bool
    noDuplicatedData :: [CRSignal ShortHash Data] -> Bool
noDuplicatedData = [CRSignal ShortHash Data] -> Bool
forall a. Ord a => [a] -> Bool
allUnique ([CRSignal ShortHash Data] -> Bool)
-> ([CRSignal ShortHash Data] -> [CRSignal ShortHash Data])
-> [CRSignal ShortHash Data]
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CRSignal ShortHash Data -> Bool)
-> [CRSignal ShortHash Data] -> [CRSignal ShortHash Data]
forall a. (a -> Bool) -> [a] -> [a]
filter CRSignal ShortHash Data -> Bool
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 =
  Int -> Property -> Property
forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
5000 (Property -> Property) -> Property -> Property
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 ()