-
Notifications
You must be signed in to change notification settings - Fork 155
/
Core.hs
185 lines (172 loc) · 6.48 KB
/
Core.hs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module Test.Cardano.Ledger.Conformance.ExecSpecRule.Core (
ExecSpecRule (..),
conformsToImpl,
computationResultToEither,
) where
import Cardano.Ledger.BaseTypes (Inject, ShelleyBase)
import Cardano.Ledger.Core (EraRule)
import qualified Constrained as CV2
import Constrained.Base (Spec (..), shrinkWithSpec)
import Control.State.Transition.Extended (STS (..))
import Data.Bifunctor (Bifunctor (..))
import Data.Bitraversable (bimapM)
import Data.Typeable (Typeable)
import GHC.Base (Constraint, NonEmpty, Symbol, Type)
import GHC.TypeLits (KnownSymbol)
import qualified Lib as Agda
import Test.Cardano.Ledger.Conformance.SpecTranslate.Core (SpecTranslate (..), runSpecTransM)
import Test.Cardano.Ledger.Imp.Common (
MonadGen (..),
NFData,
Property,
ToExpr,
counterexample,
diffExpr,
expectRightExpr,
forAllShrinkShow,
showExpr,
)
import Test.Cardano.Ledger.Shelley.ImpTest (
ImpTestM,
ShelleyEraImp,
impAnn,
logEntry,
tryRunImpRule,
)
type ForAllRuleTypes (c :: Type -> Constraint) rule era =
( c (Environment (EraRule rule era))
, c (State (EraRule rule era))
, c (Signal (EraRule rule era))
)
class
( ForAllRuleTypes (CV2.HasSpec fn) rule era
, ForAllRuleTypes (SpecTranslate (ExecContext fn rule era)) rule era
, ForAllRuleTypes ToExpr rule era
, ForAllRuleTypes NFData rule era
, CV2.HasSpec fn (ExecContext fn rule era)
, Inject (ExecContext fn rule era) (SpecTransContext (Environment (EraRule rule era)))
, Inject (ExecContext fn rule era) (SpecTransContext (State (EraRule rule era)))
, Inject (ExecContext fn rule era) (SpecTransContext (Signal (EraRule rule era)))
, Inject (ExecContext fn rule era) (SpecTransContext (PredicateFailure (EraRule rule era)))
, Eq (Event (EraRule rule era))
, Typeable (Event (EraRule rule era))
, KnownSymbol rule
, STS (EraRule rule era)
, BaseM (EraRule rule era) ~ ShelleyBase
, NFData (TestRep (PredicateFailure (EraRule rule era)))
, SpecTranslate (ExecContext fn rule era) (PredicateFailure (EraRule rule era))
) =>
ExecSpecRule fn (rule :: Symbol) era
where
type ExecContext fn rule era
type ExecContext fn rule era = ()
environmentSpec ::
CV2.Spec fn (Environment (EraRule rule era))
stateSpec ::
Environment (EraRule rule era) ->
CV2.Spec fn (State (EraRule rule era))
signalSpec ::
Environment (EraRule rule era) ->
State (EraRule rule era) ->
CV2.Spec fn (Signal (EraRule rule era))
execContextSpec :: CV2.Spec fn (ExecContext fn rule era)
default execContextSpec ::
ExecContext fn rule era ~ () =>
CV2.Spec fn (ExecContext fn rule era)
execContextSpec = TrueSpec
runAgdaRule ::
SpecRep (Environment (EraRule rule era)) ->
SpecRep (State (EraRule rule era)) ->
SpecRep (Signal (EraRule rule era)) ->
Either
(NonEmpty (SpecRep (PredicateFailure (EraRule rule era))))
(SpecRep (State (EraRule rule era)))
impSpecTrans ::
SpecTranslate ctx a =>
ctx ->
a ->
ImpTestM era (SpecRep a)
impSpecTrans ctx x = do
let res = runSpecTransM ctx $ toSpecRep x
expectRightExpr res
runConformance ::
forall (rule :: Symbol) (fn :: [Type] -> Type -> Type) era.
( ExecSpecRule fn rule era
, NFData (SpecRep (Environment (EraRule rule era)))
, NFData (SpecRep (State (EraRule rule era)))
, NFData (SpecRep (Signal (EraRule rule era)))
) =>
Environment (EraRule rule era) ->
State (EraRule rule era) ->
Signal (EraRule rule era) ->
ImpTestM
era
( Either
(NonEmpty (TestRep (PredicateFailure (EraRule rule era))))
(TestRep (State (EraRule rule era)))
, Either
(NonEmpty (TestRep (PredicateFailure (EraRule rule era))))
(TestRep (State (EraRule rule era)))
)
runConformance env st sig = do
(execContext :: ctx) <- liftGen . CV2.genFromSpec_ $ execContextSpec @fn @rule @era
specEnv <- impAnn "Translating the environment" $ impSpecTrans execContext env
specSt <- impAnn "Translating the state" $ impSpecTrans execContext st
specSig <- impAnn "Translating the signal" $ impSpecTrans execContext sig
let agdaRes = runAgdaRule @fn @rule @era specEnv specSt specSig
implRes <- fmap fst <$> tryRunImpRule @rule @era env st sig
implResTest <-
impAnn "Translating implementation values to SpecRep" . expectRightExpr . runSpecTransM execContext $
bimapM (traverse toTestRep) toTestRep implRes
let
agdaResTest =
bimap
(fmap $ specToTestRep @ctx @(PredicateFailure (EraRule rule era)))
(specToTestRep @ctx @(State (EraRule rule era)))
agdaRes
pure (implResTest, agdaResTest)
conformsToImpl ::
forall (rule :: Symbol) fn era.
( ShelleyEraImp era
, ExecSpecRule fn rule era
, NFData (SpecRep (Environment (EraRule rule era)))
, NFData (SpecRep (State (EraRule rule era)))
, NFData (SpecRep (Signal (EraRule rule era)))
) =>
Property
conformsToImpl =
let envSpec = environmentSpec @fn @rule @era
in forAllShrinkShow (CV2.genFromSpec_ envSpec) (shrinkWithSpec envSpec) showExpr $ \env ->
let stSpec = stateSpec @fn @rule @era env
in forAllShrinkShow (CV2.genFromSpec_ stSpec) (shrinkWithSpec stSpec) showExpr $ \st ->
let sigSpec = signalSpec @fn @rule @era env st
in forAllShrinkShow (CV2.genFromSpec_ sigSpec) (shrinkWithSpec sigSpec) showExpr $ \sig ->
resize 5 $ do
logEntry @era . show $ signalSpec @fn @rule @era env st
(implResTest, agdaResTest) <- runConformance @rule @fn env st sig
let
failMsg =
unlines
[ ""
, "===== DIFF ====="
, diffExpr implResTest agdaResTest
, ""
, "Legend:"
, "\t\ESC[91mImplemenation"
, "\t\ESC[92mSpecification\ESC[39m"
]
pure . counterexample failMsg $ implResTest == agdaResTest
computationResultToEither :: Agda.ComputationResult e a -> Either e a
computationResultToEither (Agda.Success x) = Right x
computationResultToEither (Agda.Failure e) = Left e