Hooking up Haskell code in tests

Author: yveshauser

formal-spec/Everything.agda

@@ -3,3 +3,4 @@ module Everything where
 open import Leios.Simplified
 open import Leios.Short
 open import Leios.Network
+open import Leios.Foreign.Export

formal-spec/Leios/Foreign/Export.agda

@@ -25,7 +25,8 @@ record IBHeaderHs : Type where
         producerID : Int
 
 {-# FOREIGN GHC
-data IBHeaderHs = IBHeaderHs Integer Integer 
+data IBHeaderHs = IBHeaderHs Integer Integer
+  deriving (Show, Eq, Generic)
 #-}
 
 {-# COMPILE GHC IBHeaderHs = data IBHeaderHs (IBHeaderHs) #-}
@@ -70,6 +71,7 @@ record EndorserBlockHs : Type where
 
 {-# FOREIGN GHC
 data EndorserBlockHs = EndorserBlockHs Integer Integer [Integer]
+  deriving (Show, Eq, Generic)
 #-}
 
 {-# COMPILE GHC EndorserBlockHs = data EndorserBlockHs (EndorserBlockHs) #-}
@@ -95,4 +97,3 @@ instance
 
   HsTy-LeiosState = autoHsType LeiosState
   Conv-LeiosState = autoConvert LeiosState
-

formal-spec/hs-src/leios-spec.cabal

@@ -27,38 +27,11 @@ common globalOptions
         PatternSynonyms DeriveGeneric
     ghc-options:
         -Wno-overlapping-patterns
-
-test-suite test
-    import: globalOptions
-    hs-source-dirs: test
-    main-is: Spec.hs
-    other-modules:
-        UtxowSpec
-    build-depends:
-        leios-spec,
-        hspec,
-        HUnit,
-        text
-    build-tool-depends: hspec-discover:hspec-discover
-    type: exitcode-stdio-1.0
-    ghc-options:
-        -Wall
-        -threaded -rtsopts -with-rtsopts=-N
-        -fno-warn-type-defaults
-
-executable leios-spec
-    import: globalOptions
-    hs-source-dirs: exe
-    main-is: Main.hs
-    build-depends:
-        text,
-        ieee,
-        leios-spec
-
 library
     import: globalOptions
     hs-source-dirs: src
     exposed-modules:
+        Lib
     build-depends:
         text,
         ieee

leios-conformance/leios-conformance.cabal

@@ -30,6 +30,7 @@ library
     , bytestring
     , containers
     , data-default
+    , leios-spec
     , mtl
     , pretty
     , QuickCheck

leios-conformance/src/Leios/Conformance/Model.hs

@@ -1,28 +1,36 @@
 {-# LANGUAGE DeriveGeneric #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE RecordWildCards #-}
-module Leios.Conformance.Model where
-
-import Data.Aeson (FromJSON, ToJSON)
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# OPTIONS_GHC -Wno-orphans #-}
+module Leios.Conformance.Model
+  ( module Leios.Conformance.Model
+  , module Lib
+  ) where
+
+import Data.Aeson (FromJSON(..), ToJSON(..))
 import Data.Maybe (maybeToList)
 import GHC.Generics (Generic)
 import Text.PrettyPrint.HughesPJClass (Pretty (pPrint))
 
+import Lib
+
 data EnvAction
   = Tick
   | NewIB InputBlock
   | NewEB EndorserBlock
   | NewVote Vote
   deriving (Eq, Show)
 
--- TODO: use InputBlock extracted from Agda
-data InputBlock = InputBlock
-  deriving (Show, Eq, Generic)
+instance FromJSON InputBlock where
+  parseJSON = undefined
+
+instance ToJSON InputBlock where
+  toJSON = undefined
 
-instance FromJSON InputBlock
-instance ToJSON InputBlock
 instance Pretty InputBlock where
-  pPrint InputBlock = "InputBlock"
+  pPrint (InputBlock _ _) = "InputBlock"
 
 -- TODO: use EndorserBlock extracted from Agda
 data EndorserBlock = EndorserBlock
@@ -44,7 +52,7 @@ instance Pretty Vote where
 
 -- TODO: use LeiosState extracted from Agda
 data NodeModel = NodeModel
-  { slot :: Integer
+  { currentSlot :: Integer
   , ibs :: [InputBlock]
   , ebs :: [EndorserBlock]
   , votes :: [Vote]

leios-conformance/src/Leios/Conformance/Test.hs

@@ -11,7 +11,7 @@ module Leios.Conformance.Test where
 
 import Data.Maybe (isJust)
 import Test.QuickCheck (
-  frequency
+  frequency, Arbitrary (..)
  )
 import Test.QuickCheck.DynamicLogic (DynLogicModel)
 import Test.QuickCheck.StateModel (
@@ -65,6 +65,10 @@ instance Pretty EnvAction where
   pPrint (NewEB eb) = "NewEB" <+> pPrint eb
   pPrint (NewVote v) = "NewVote" <+> pPrint v
 
+instance Arbitrary InputBlock where
+
+instance Arbitrary EndorserBlock where
+
 instance StateModel NetworkModel where
   data Action NetworkModel a where
     Step :: EnvAction -> Action NetworkModel ([InputBlock], [EndorserBlock], [Vote])
@@ -78,8 +82,8 @@ instance StateModel NetworkModel where
   arbitraryAction _ _ =
         fmap (Some . Step) . frequency $
           [(1, pure Tick)]
-            ++ fmap (1,) (pure . NewIB <$> [InputBlock])
-            ++ fmap (1,) (pure . NewEB <$> [EndorserBlock])
+            ++ fmap (1,) [NewIB <$> arbitrary]
+            ++ fmap (1,) [NewEB <$> arbitrary]
 
   shrinkAction _ _ (Step Tick) = []
   shrinkAction _ _ Step{} = [Some (Step Tick)]

leios-conformance/src/Leios/Conformance/Test/External.hs

@@ -133,8 +133,8 @@ instance Realized IO ([InputBlock], [EndorserBlock], [Vote]) ~ ([InputBlock], [E
     let (expectedIBs, expectedEBs, expectedVotes) = maybe (mempty, mempty, mempty) fst $ transition s a
     let ok = (ibs, ebs) == (expectedIBs, expectedEBs)
     monitorPost . counterexample . show $ "  action $" <+> pPrint a
-    when (a == Tick && slot s == slot s' + 1) $
-      monitorPost . counterexample $ "  -- new slot: " ++ show (slot s')
+    when (a == Tick && currentSlot s == currentSlot s' + 1) $
+      monitorPost . counterexample $ "  -- new slot: " ++ show (currentSlot s')
     unless (null ibs) $
       monitorPost . counterexample . show $ "  --      got InputBlocks:" <+> pPrint ibs
     when (ibs /= expectedIBs) $