Safe Haskell	Safe-Inferred
Language	Haskell2010

Test.Control.State.Transition.Examples.CommitReveal

Synopsis

data CR hashAlgo (hashToDataMap ∷ Type → Type → Type) commitData
data CRSt hashAlgo hashToDataMap commitData = CRSt {
- hashToData ∷ !(hashToDataMap (Hash hashAlgo Data) commitData)
- committedHashes ∷ !(Set (Hash hashAlgo Data))
}
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
data CRSignal hashAlgo commitData
- = Commit (Hash hashAlgo Data) commitData
- | Reveal Data
isCommit ∷ CRSignal hashAlgo commitData → Bool
newtype Data = Data {
- getData ∷ (Id, Int)
}
newtype Id = Id {
- getId ∷ Int
}
data CRPredicateFailure hashAlgo (hashToDataMap ∷ Type → Type → Type) commitData
- = InvalidReveal Data
- | AlreadyComitted (Hash hashAlgo Data)
prop_qc_UniqueData ∷ Property
prop_qc_OnlyValidSignals ∷ Property

Documentation

data CR hashAlgo (hashToDataMap ∷ Type → Type → Type) commitData Source #

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.

Instances

Instances details

(HashAlgorithm hashAlgo, Typeable hashToDataMap, Typeable commitData, MapLike hashToDataMap (Hash hashAlgo Data) commitData, Monoid (hashToDataMap (Hash hashAlgo Data) commitData)) ⇒ STS (CR hashAlgo hashToDataMap commitData) Source #
Instance details Defined in Test.Control.State.Transition.Examples.CommitReveal Associated Types type State (CR hashAlgo hashToDataMap commitData) Source # type Signal (CR hashAlgo hashToDataMap commitData) Source # type Environment (CR hashAlgo hashToDataMap commitData) Source # type BaseM (CR hashAlgo hashToDataMap commitData) ∷ Type → Type Source # type Event (CR hashAlgo hashToDataMap commitData) Source # type PredicateFailure (CR hashAlgo hashToDataMap commitData) Source # Methods initialRules ∷ [InitialRule (CR hashAlgo hashToDataMap commitData)] Source # transitionRules ∷ [TransitionRule (CR hashAlgo hashToDataMap commitData)] Source # assertions ∷ [Assertion (CR hashAlgo hashToDataMap commitData)] Source # renderAssertionViolation ∷ AssertionViolation (CR hashAlgo hashToDataMap commitData) → String Source #
HashAlgorithm hashAlgo ⇒ HasTrace (CR hashAlgo Map Data) () Source #
Instance details Defined in Test.Control.State.Transition.Examples.CommitReveal Associated Types type BaseEnv (CR hashAlgo Map Data) Source # Methods interpretSTS ∷ HasCallStack ⇒ BaseEnv (CR hashAlgo Map Data) → BaseM (CR hashAlgo Map Data) a → a Source # envGen ∷ () → Gen (Environment (CR hashAlgo Map Data)) Source # sigGen ∷ () → Environment (CR hashAlgo Map Data) → State (CR hashAlgo Map Data) → Gen (Signal (CR hashAlgo Map Data)) Source # shrinkSignal ∷ Signal (CR hashAlgo Map Data) → [Signal (CR hashAlgo Map Data)] Source #
type BaseM (CR hashAlgo hashToDataMap commitData) Source #
Instance details Defined in Test.Control.State.Transition.Examples.CommitReveal type BaseM (CR hashAlgo hashToDataMap commitData) = Identity
type Environment (CR hashAlgo hashToDataMap commitData) Source #
Instance details Defined in Test.Control.State.Transition.Examples.CommitReveal type Environment (CR hashAlgo hashToDataMap commitData) = ()
type Event (CR hashAlgo hashToDataMap commitData) Source #
Instance details Defined in Test.Control.State.Transition.Examples.CommitReveal type Event (CR hashAlgo hashToDataMap commitData) = Void
type PredicateFailure (CR hashAlgo hashToDataMap commitData) Source #
Instance details Defined in Test.Control.State.Transition.Examples.CommitReveal type PredicateFailure (CR hashAlgo hashToDataMap commitData) = CRPredicateFailure hashAlgo hashToDataMap commitData
type Signal (CR hashAlgo hashToDataMap commitData) Source #
Instance details Defined in Test.Control.State.Transition.Examples.CommitReveal type Signal (CR hashAlgo hashToDataMap commitData) = CRSignal hashAlgo commitData
type State (CR hashAlgo hashToDataMap commitData) Source #
Instance details Defined in Test.Control.State.Transition.Examples.CommitReveal type State (CR hashAlgo hashToDataMap commitData) = CRSt hashAlgo hashToDataMap commitData
type BaseEnv (CR hashAlgo Map Data) Source #
Instance details Defined in Test.Control.State.Transition.Examples.CommitReveal type BaseEnv (CR hashAlgo Map Data) = ()

data CRSt hashAlgo hashToDataMap commitData Source #

Commit-reveal transition system state.

Constructors

CRSt

Fields

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.
committedHashes ∷ !(Set (Hash hashAlgo Data))

Instances

Instances details

Show (hashToDataMap (Hash hashAlgo Data) commitData) ⇒ Show (CRSt hashAlgo hashToDataMap commitData) Source #
Instance details Defined in Test.Control.State.Transition.Examples.CommitReveal Methods showsPrec ∷ Int → CRSt hashAlgo hashToDataMap commitData → ShowS Source # show ∷ CRSt hashAlgo hashToDataMap commitData → String Source # showList ∷ [CRSt hashAlgo hashToDataMap commitData] → ShowS Source #
Eq (hashToDataMap (Hash hashAlgo Data) commitData) ⇒ Eq (CRSt hashAlgo hashToDataMap commitData) Source #
Instance details Defined in Test.Control.State.Transition.Examples.CommitReveal Methods (==) ∷ CRSt hashAlgo hashToDataMap commitData → CRSt hashAlgo hashToDataMap commitData → Bool Source # (/=) ∷ CRSt hashAlgo hashToDataMap commitData → CRSt hashAlgo hashToDataMap commitData → Bool Source #

class MapLike m k v where Source #

Methods

insert ∷ k → v → m k v → m k v Source #

delete ∷ k → m k v → m k v Source #

Instances

Instances details

Ord k ⇒ MapLike Map k v Source #
Instance details Defined in Test.Control.State.Transition.Examples.CommitReveal Methods insert ∷ k → v → Map k v → Map k v Source # delete ∷ k → Map k v → Map k v Source #
MapLike NoOpMap a b Source #	This is the `MapLike` instance one would use if the executable spec would be used in an implementation (where no generators are needed).
Instance details Defined in Test.Control.State.Transition.Examples.CommitReveal Methods insert ∷ a → b → NoOpMap a b → NoOpMap a b Source # delete ∷ a → NoOpMap a b → NoOpMap a b Source #

data NoOpMap a b Source #

Constructors

NoOpMap

Instances

Instances details

MapLike NoOpMap a b Source #	This is the `MapLike` instance one would use if the executable spec would be used in an implementation (where no generators are needed).
Instance details Defined in Test.Control.State.Transition.Examples.CommitReveal Methods insert ∷ a → b → NoOpMap a b → NoOpMap a b Source # delete ∷ a → NoOpMap a b → NoOpMap a b Source #

data CRSignal hashAlgo commitData Source #

Constructors

Commit (Hash hashAlgo Data) commitData
Reveal Data

Instances

Instances details

Show commitData ⇒ Show (CRSignal hashAlgo commitData) Source #
Instance details Defined in Test.Control.State.Transition.Examples.CommitReveal Methods showsPrec ∷ Int → CRSignal hashAlgo commitData → ShowS Source # show ∷ CRSignal hashAlgo commitData → String Source # showList ∷ [CRSignal hashAlgo commitData] → ShowS Source #
Eq commitData ⇒ Eq (CRSignal hashAlgo commitData) Source #
Instance details Defined in Test.Control.State.Transition.Examples.CommitReveal Methods (==) ∷ CRSignal hashAlgo commitData → CRSignal hashAlgo commitData → Bool Source # (/=) ∷ CRSignal hashAlgo commitData → CRSignal hashAlgo commitData → Bool Source #
Ord commitData ⇒ Ord (CRSignal hashAlgo commitData) Source #
Instance details Defined in Test.Control.State.Transition.Examples.CommitReveal Methods compare ∷ CRSignal hashAlgo commitData → CRSignal hashAlgo commitData → Ordering Source # (<) ∷ CRSignal hashAlgo commitData → CRSignal hashAlgo commitData → Bool Source # (<=) ∷ CRSignal hashAlgo commitData → CRSignal hashAlgo commitData → Bool Source # (>) ∷ CRSignal hashAlgo commitData → CRSignal hashAlgo commitData → Bool Source # (>=) ∷ CRSignal hashAlgo commitData → CRSignal hashAlgo commitData → Bool Source # max ∷ CRSignal hashAlgo commitData → CRSignal hashAlgo commitData → CRSignal hashAlgo commitData Source # min ∷ CRSignal hashAlgo commitData → CRSignal hashAlgo commitData → CRSignal hashAlgo commitData Source #

isCommit ∷ CRSignal hashAlgo commitData → Bool Source #

newtype Data Source #

Constructors

Data
Fields getData ∷ (Id, Int)

Instances

Instances details

Arbitrary Data Source #
Instance details Defined in Test.Control.State.Transition.Examples.CommitReveal Methods arbitrary ∷ Gen Data Source # shrink ∷ Data → [Data] Source #
Show Data Source #
Instance details Defined in Test.Control.State.Transition.Examples.CommitReveal Methods showsPrec ∷ Int → Data → ShowS Source # show ∷ Data → String Source # showList ∷ [Data] → ShowS Source #
EncCBOR Data Source #
Instance details Defined in Test.Control.State.Transition.Examples.CommitReveal Methods encCBOR ∷ Data → Encoding Source # encodedSizeExpr ∷ (∀ t. EncCBOR t ⇒ Proxy t → Size) → Proxy Data → Size Source # encodedListSizeExpr ∷ (∀ t. EncCBOR t ⇒ Proxy t → Size) → Proxy [Data] → Size Source #
Eq Data Source #
Instance details Defined in Test.Control.State.Transition.Examples.CommitReveal Methods (==) ∷ Data → Data → Bool Source # (/=) ∷ Data → Data → Bool Source #
Ord Data Source #
Instance details Defined in Test.Control.State.Transition.Examples.CommitReveal Methods compare ∷ Data → Data → Ordering Source # (<) ∷ Data → Data → Bool Source # (<=) ∷ Data → Data → Bool Source # (>) ∷ Data → Data → Bool Source # (>=) ∷ Data → Data → Bool Source # max ∷ Data → Data → Data Source # min ∷ Data → Data → Data Source #
HashAlgorithm hashAlgo ⇒ HasTrace (CR hashAlgo Map Data) () Source #
Instance details Defined in Test.Control.State.Transition.Examples.CommitReveal Associated Types type BaseEnv (CR hashAlgo Map Data) Source # Methods interpretSTS ∷ HasCallStack ⇒ BaseEnv (CR hashAlgo Map Data) → BaseM (CR hashAlgo Map Data) a → a Source # envGen ∷ () → Gen (Environment (CR hashAlgo Map Data)) Source # sigGen ∷ () → Environment (CR hashAlgo Map Data) → State (CR hashAlgo Map Data) → Gen (Signal (CR hashAlgo Map Data)) Source # shrinkSignal ∷ Signal (CR hashAlgo Map Data) → [Signal (CR hashAlgo Map Data)] Source #
type BaseEnv (CR hashAlgo Map Data) Source #
Instance details Defined in Test.Control.State.Transition.Examples.CommitReveal type BaseEnv (CR hashAlgo Map Data) = ()

newtype Id Source #

Constructors

Id
Fields getId ∷ Int

Instances

Instances details

Arbitrary Id Source #
Instance details Defined in Test.Control.State.Transition.Examples.CommitReveal Methods arbitrary ∷ Gen Id Source # shrink ∷ Id → [Id] Source #
Show Id Source #
Instance details Defined in Test.Control.State.Transition.Examples.CommitReveal Methods showsPrec ∷ Int → Id → ShowS Source # show ∷ Id → String Source # showList ∷ [Id] → ShowS Source #
EncCBOR Id Source #
Instance details Defined in Test.Control.State.Transition.Examples.CommitReveal Methods encCBOR ∷ Id → Encoding Source # encodedSizeExpr ∷ (∀ t. EncCBOR t ⇒ Proxy t → Size) → Proxy Id → Size Source # encodedListSizeExpr ∷ (∀ t. EncCBOR t ⇒ Proxy t → Size) → Proxy [Id] → Size Source #
Eq Id Source #
Instance details Defined in Test.Control.State.Transition.Examples.CommitReveal Methods (==) ∷ Id → Id → Bool Source # (/=) ∷ Id → Id → Bool Source #
Ord Id Source #
Instance details Defined in Test.Control.State.Transition.Examples.CommitReveal Methods compare ∷ Id → Id → Ordering Source # (<) ∷ Id → Id → Bool Source # (<=) ∷ Id → Id → Bool Source # (>) ∷ Id → Id → Bool Source # (>=) ∷ Id → Id → Bool Source # max ∷ Id → Id → Id Source # min ∷ Id → Id → Id Source #

data CRPredicateFailure hashAlgo (hashToDataMap ∷ Type → Type → Type) commitData Source #

Constructors

InvalidReveal Data
AlreadyComitted (Hash hashAlgo Data)

Instances

Instances details

Show (CRPredicateFailure hashAlgo hashToDataMap commitData) Source #
Instance details Defined in Test.Control.State.Transition.Examples.CommitReveal Methods showsPrec ∷ Int → CRPredicateFailure hashAlgo hashToDataMap commitData → ShowS Source # show ∷ CRPredicateFailure hashAlgo hashToDataMap commitData → String Source # showList ∷ [CRPredicateFailure hashAlgo hashToDataMap commitData] → ShowS Source #
Eq (CRPredicateFailure hashAlgo hashToDataMap commitData) Source #
Instance details Defined in Test.Control.State.Transition.Examples.CommitReveal Methods (==) ∷ CRPredicateFailure hashAlgo hashToDataMap commitData → CRPredicateFailure hashAlgo hashToDataMap commitData → Bool Source # (/=) ∷ CRPredicateFailure hashAlgo hashToDataMap commitData → CRPredicateFailure hashAlgo hashToDataMap commitData → Bool Source #

prop_qc_UniqueData ∷ Property Source #

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_OnlyValidSignals ∷ Property Source #

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.