Renamed exported types

Author: yveshauser

formal-spec/Leios/Foreign/Export.agda

@@ -10,7 +10,7 @@ open import Tactic.Derive.Convertible
 open import Tactic.Derive.HsType
 
 open import Leios.Prelude
-open import Leios.Trace
+open import Leios.Trace renaming (EndorserBlock to EndorserBlockAgda; IBHeader to IBHeaderAgda)
 open import Leios.Foreign.BaseTypes
 open import Leios.Foreign.HSTypes
 
@@ -20,20 +20,20 @@ instance
   HsTy-SlotUpkeep = autoHsType SlotUpkeep ⊣ onConstructors (S.concat ∘ (S.wordsByᵇ ('-' Char.≈ᵇ_)))
   Conv-SlotUpkeep = autoConvert SlotUpkeep
 
-record IBHeaderHs : Type where
+record IBHeader : Type where
   field slotNumber : Int
         producerID : Int
 
 {-# FOREIGN GHC
-data IBHeaderHs = IBHeaderHs Integer Integer
+data IBHeader = IBHeader Integer Integer
   deriving (Show, Eq, Generic)
 #-}
 
-{-# COMPILE GHC IBHeaderHs = data IBHeaderHs (IBHeaderHs) #-}
+{-# COMPILE GHC IBHeader = data IBHeader (IBHeader) #-}
 
 instance
-  HsTy-IBHeader = MkHsType IBHeader IBHeaderHs
-  Conv-IBHeader : Convertible IBHeader IBHeaderHs
+  HsTy-IBHeader = MkHsType IBHeaderAgda IBHeader
+  Conv-IBHeader : Convertible IBHeaderAgda IBHeader
   Conv-IBHeader = record
     { to = λ (record { slotNumber = sl ; producerID = pid }) → record { slotNumber = + sl ; producerID = + toℕ pid }
     ; from = λ (record { slotNumber = sl ; producerID = pid }) →
@@ -64,23 +64,23 @@ instance
   Conv-ℕ : HsConvertible ℕ 
   Conv-ℕ = Convertible-Refl
 
-record EndorserBlockHs : Type where
+record EndorserBlock : Type where
   field slotNumber : Int
         producerID : Int
         ibRefs     : List Int
 
 {-# FOREIGN GHC
-data EndorserBlockHs = EndorserBlockHs Integer Integer [Integer]
+data EndorserBlock = EndorserBlock Integer Integer [Integer]
   deriving (Show, Eq, Generic)
 #-}
 
-{-# COMPILE GHC EndorserBlockHs = data EndorserBlockHs (EndorserBlockHs) #-}
+{-# COMPILE GHC EndorserBlock = data EndorserBlock (EndorserBlock) #-}
 
 instance
 
-  HsTy-EndorserBlock = MkHsType EndorserBlock EndorserBlockHs
+  HsTy-EndorserBlock = MkHsType EndorserBlockAgda EndorserBlock
 
-  Conv-EndorserBlock : Convertible EndorserBlock EndorserBlockHs
+  Conv-EndorserBlock : Convertible EndorserBlockAgda EndorserBlock
   Conv-EndorserBlock =
     record
       { to = λ (record { slotNumber = sl ; producerID = pid }) → record { slotNumber = + sl ; producerID = + toℕ pid ; ibRefs = [] }

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

@@ -23,44 +23,42 @@ data EnvAction
   | NewVote Vote
   deriving (Eq, Show)
 
-instance FromJSON InputBlock where
-  parseJSON = undefined
+instance FromJSON IBHeader
+instance FromJSON IBBody
+instance FromJSON InputBlock
 
-instance ToJSON InputBlock where
-  toJSON = undefined
+instance ToJSON IBHeader
+instance ToJSON IBBody
+instance ToJSON InputBlock
 
 instance Pretty InputBlock where
-  pPrint (InputBlock _ _) = "InputBlock"
-
--- TODO: use EndorserBlock extracted from Agda
-data EndorserBlock = EndorserBlock
-  deriving (Show, Eq, Generic)
+  pPrint (InputBlock {}) = "InputBlock"
 
 instance FromJSON EndorserBlock
 instance ToJSON EndorserBlock
 instance Pretty EndorserBlock where
-  pPrint EndorserBlock = "EndorserBlock"
-
--- TODO: use Vote extracted from Agda
-data Vote = Vote
-  deriving (Show, Eq, Generic)
-
-instance FromJSON Vote
-instance ToJSON Vote
-instance Pretty Vote where
-  pPrint Vote = "Vote"
-
--- TODO: use LeiosState extracted from Agda
-data NodeModel = NodeModel
-  { currentSlot :: Integer
-  , ibs :: [InputBlock]
-  , ebs :: [EndorserBlock]
-  , votes :: [Vote]
-  }
-  deriving Show
+  pPrint (EndorserBlock {}) = "EndorserBlock"
+
+type Vote = () -- TODO: use Vote extracted from Agda
+type NodeModel = LeiosState
 
 initialModelState :: NodeModel
-initialModelState = NodeModel 0 [] [] []
+initialModelState = LeiosState
+  { v = ()
+  , sD = MkHSMap []
+  , fFDState = ()
+  , ledger = []
+  , toPropose = []
+  , iBs = []
+  , eBs = []
+  , vs = []
+  , slot = 0
+  , iBHeaders = []
+  , iBBodies = []
+  , upkeep = MkHSSet []
+  , baseState = ()
+  , votingState = ()
+  }
 
 --TODO
 makeIB :: NodeModel -> Maybe InputBlock
@@ -75,13 +73,13 @@ makeVote :: NodeModel -> Maybe Vote
 makeVote _ = Nothing
 
 addIB :: InputBlock -> NodeModel -> NodeModel
-addIB ib nm@NodeModel{..} = nm { ibs = ib : ibs }
+addIB ib nm@LeiosState{..} = nm { iBs = ib : iBs }
 
 addEB :: EndorserBlock -> NodeModel -> NodeModel
-addEB eb nm@NodeModel{..} = nm { ebs = eb : ebs }
+addEB eb nm@LeiosState{..} = nm { eBs = eb : eBs }
 
 addVote :: Vote -> NodeModel -> NodeModel
-addVote v nm@NodeModel{..} = nm { votes = v : votes }
+addVote x nm@LeiosState{..} = nm { vs = [x] : vs }
 
 -- TODO: Leios executable specification
 transition :: NodeModel -> EnvAction -> Maybe (([InputBlock], [EndorserBlock], [Vote]), NodeModel)

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

@@ -103,7 +103,7 @@ type Runtime = StateT RunState IO
 
 instance Realized IO ([InputBlock], [EndorserBlock], [Vote]) ~ ([InputBlock], [EndorserBlock], [Vote]) => RunModel NetworkModel Runtime where
 
-  perform net@NetworkModel{nodeModel = NodeModel{..}} (Step a) _ = case a of
+  perform net@NetworkModel{nodeModel = LeiosState{..}} (Step a) _ = case a of
     Tick -> do
       rs@RunState{..} <- get
       modify $ \rs' -> rs' {unfetchedIBs = mempty, unfetchedEBs = mempty, unfetchedVotes = mempty}
@@ -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 && currentSlot s == currentSlot s' + 1) $
-      monitorPost . counterexample $ "  -- new slot: " ++ show (currentSlot s')
+    when (a == Tick && slot s == slot s' + 1) $
+      monitorPost . counterexample $ "  -- new slot: " ++ show (slot s')
     unless (null ibs) $
       monitorPost . counterexample . show $ "  --      got InputBlocks:" <+> pPrint ibs
     when (ibs /= expectedIBs) $