Generate Haskell code for ChainHead

docs/agda-spec/src/Spec/Foreign/HSConsensus.agda

@@ -5,3 +5,4 @@ open import Spec.Foreign.HSConsensus.UpdateNonce public
 open import Spec.Foreign.HSConsensus.OperationalCertificate public
 open import Spec.Foreign.HSConsensus.Protocol public
 open import Spec.Foreign.HSConsensus.TickForecast public
+open import Spec.Foreign.HSConsensus.ChainHead public

docs/agda-spec/src/Spec/Foreign/HSConsensus/ChainHead.agda

@@ -0,0 +1,31 @@
+module Spec.Foreign.HSConsensus.ChainHead where
+
+open import Spec.Foreign.ExternalFunctions
+
+open import Foreign.Haskell.Coerce
+
+open import Spec.Foreign.HSConsensus.BaseTypes
+open import Spec.ChainHead DummyCrypto DummyNonces DummyEpochStructure DummyBlockStructure DummyAbstractFunctions DummyLedgerInterface DummyRationalExtStructure
+
+unquoteDecl = do
+  hsTypeAlias ChainHeadEnv
+
+instance
+  HsTy-LastAppliedBlock = autoHsType LastAppliedBlock ⊣ withConstructor "MkLastAppliedBlock"
+                                                      • fieldPrefix "lab"
+  Conv-LastAppliedBlock = autoConvert LastAppliedBlock
+
+  HsTy-ChainHeadState = autoHsType ChainHeadState ⊣ withConstructor "MkChainHeadState"
+                                                  • fieldPrefix "chs"
+  Conv-ChainHeadState = autoConvert ChainHeadState
+
+module _ (ext : ExternalFunctions) where
+  open import Spec.Foreign.HSConsensus.ExternalStructures ext hiding (BHeader)
+  open import Spec.Foreign.HSConsensus.BlockDefinitions
+  open import Spec.ChainHead.Properties HSCrypto HSNonces HSEpochStructure HSBlockStructure HSAbstractFunctions HSLedgerInterface HSRationalExtStructure
+
+  chainhead-step : HsType (ChainHeadEnv → ChainHeadState → BHeader → ComputationResult String ChainHeadState)
+  -- FIXME: Investigate why `A` needs to be manually supplied.
+  chainhead-step = to {ChainHeadEnv → ChainHeadState → BHeader → ComputationResult String ChainHeadState} (coerce ⦃ TrustMe ⦄ $ compute Computational-CHAINHEAD)
+
+  {-# COMPILE GHC chainhead-step as chainheadStep #-}

docs/agda-spec/src/Spec/hs-src/Lib.hs

@@ -17,6 +17,8 @@ import MAlonzo.Code.Spec.Foreign.HSConsensus.Protocol                          a
   (PrtclEnv(..), PrtclState(..), prtclStep, prtclDebug, PoolDistr)
 import MAlonzo.Code.Spec.Foreign.HSConsensus.TickForecast                      as X
   (tickfStep, NewEpochState)
+import MAlonzo.Code.Spec.Foreign.HSConsensus.ChainHead                         as X
+  (ChainHeadEnv, ChainHeadState(..), LastAppliedBlock(..), chainheadStep)
 import MAlonzo.Code.Spec.Foreign.HSConsensus.BaseTypes                         as X
   (Slot, Epoch, KeyHashS, KeyHashV)
 import MAlonzo.Code.Spec.Foreign.ExternalFunctions                             as X

docs/agda-spec/src/Spec/hs-src/cardano-consensus-executable-spec.cabal

@@ -32,6 +32,7 @@ test-suite test
         OperationalCertificateSpec
         ProtocolSpec
         TickForecastSpec
+        ChainHeadSpec
     build-depends:
         cardano-consensus-executable-spec,
         hspec,

docs/agda-spec/src/Spec/hs-src/test/ChainHeadSpec.hs

@@ -0,0 +1,136 @@
+module ChainHeadSpec (spec) where
+
+import Data.Text
+
+import Test.Hspec ( Spec, describe, it )
+import Test.HUnit ( (@?=) )
+
+import Lib
+
+(.->) :: a -> b -> (a, b)
+(.->) = (,)
+
+che :: ChainHeadEnv
+che = 123
+
+lab :: LastAppliedBlock
+lab = MkLastAppliedBlock
+  { labBℓ = 0
+  , labSℓ = 0
+  , labH  = 2
+  }
+
+chs :: ChainHeadState
+chs = MkChainHeadState
+  { chsCs  = MkHSMap [ 457 .-> 233 , 999 .-> 888 ]
+  , chsΗ₀  = 3
+  , chsΗv  = 4
+  , chsΗc  = 2
+  , chsΗh  = 4
+  , chsLab = Just lab
+  }
+
+oc :: OCert
+oc = MkOCert
+  { ocVkₕ = 123
+  , ocN   = 234
+  , ocC₀  = 0
+  , ocΣ   = 345
+  }
+
+bhb :: BHBody
+bhb = MkBHBody
+  { bhbPrevHeader = Just 2
+  , bhbIssuerVk   = 456
+  , bhbVrfVk      = 567
+  , bhbBlockNo    = 1
+  , bhbSlot       = 2
+  , bhbVrfRes     = 678
+  , bhbVrfPrf     = 789
+  , bhbBodySize   = 1
+  , bhbBodyHash   = 890
+  , bhbOc         = oc
+  , bhbPv         = (1, 0)
+  }
+
+bh :: BHeader
+bh = MkBHeader
+  { bhBody = bhb
+  , bhSig  = 901
+  }
+
+lab' :: LastAppliedBlock
+lab' = MkLastAppliedBlock
+  { labBℓ = 1
+  , labSℓ = 2
+  , labH  = 2
+  }
+
+chs' :: ChainHeadState
+chs' = MkChainHeadState
+  { chsCs  = MkHSMap [ 457 .-> 234 , 999 .-> 888 ]
+  , chsΗ₀  = 3
+  , chsΗv  = 5
+  , chsΗc  = 5
+  , chsΗh  = 4
+  , chsLab = Just lab'
+  }
+
+{-
+  NOTE: Why should this test succeed? Here's the explanation:
+
+  Given
+
+    nes = 123
+    lab = Just ⟦ 0 , 0 , 2 ⟧ℓ
+    cs = [ 457  .-> 233 , 999 .-> 888 ]
+    ⟦ cs , η₀ , ηv , ηc , ηh , lab ⟧ᶜˢ = ⟦ cs , 3 , 4 , 2 , 4 , lab ⟧ᶜˢ
+
+  then
+
+    _ ⊢ nes ⇀⦇ slot ,TICKF⦈ forecast <===> _ ⊢ 123 ⇀⦇ 2 ,TICKF⦈ 126 <===> True
+
+  Also,
+
+    lastAppliedHash lab = lastAppliedHash (Just ⟦ 0 , 0 , 2 ⟧ℓ) = Just 2
+
+    e₁ = getEpoch nes = getEpoch 123 = 1
+    e₂ = getEpoch forecast = getEpoch 126 = 1
+    ne = (e₁ ≠ e₂) = (1 ≠ 1) = False
+    pp = getPParams forecast = getPParams 126 = { maxHeaderSize = 1; maxBlockSize = 2; pv = (1 , 0) }
+    nₚₕ = prevHashToNonce (lastAppliedHash lab) = prevHashToNonce 2 = 0
+    pd = getPoolDistr forecast = getPoolDistr 126 = ❴ 457 , (1 / 3 , 568) ❵
+    lab′ = Just ⟦ blockNo , slot , headerHash bh ⟧ℓ = Just ⟦ 1 , 2 , 2 ⟧ℓ
+
+  then
+
+    prtlSeqChecks lab bh = prtlSeqChecks (just ⟦ 0 , 0 , 2 ⟧ℓ) bh = 0 < 2 × 0 + 1 ≡ 1 × Just 2 ≡ Just 2 = True
+
+    chainChecks MaxMajorPV (pp .maxHeaderSize , pp .maxBlockSize , pp .pv) bh
+      = chainChecks 1 (1 , 2 , (1 , 0)) bh
+      = 1 ≤ 1 × 1 ≤ 1 × 1 ≤ 2
+      = True
+
+    ⟦ ηc , nₚₕ ⟧ᵗᵉ ⊢ ⟦ η₀ , ηh ⟧ᵗˢ ⇀⦇ ne ,TICKN⦈ ⟦ η₀′ , ηh′ ⟧ᵗˢ
+    <===>
+    ⟦ 2 , 0 ⟧ᵗᵉ ⊢ ⟦ 3 , 4 ⟧ᵗˢ ⇀⦇ False ,TICKN⦈ ⟦ 3 , 4 ⟧ᵗˢ
+
+    ⟦ pd , η₀′ ⟧ᵖᵉ ⊢ ⟦ cs , ηv , ηc ⟧ᵖˢ ⇀⦇ bh ,PRTCL⦈ ⟦ cs′ , ηv′ , ηc′ ⟧ᵖˢ
+    <===>
+    ⟦ ❴ 457 , (1 / 3 , 568) ❵ , 3 ⟧ᵖᵉ ⊢ ⟦ cs , 4 , 2 ⟧ᵖˢ ⇀⦇ bh ,PRTCL⦈ ⟦ [ 457 .-> 234 , 999 .-> 888 ] , 5 , 5 ⟧ᵖˢ
+
+  Finally,
+
+    nes ⊢ ⟦ cs , η₀ , ηv , ηc , ηh , lab ⟧ᶜˢ ⇀⦇ bh ,CHAINHEAD⦈ ⟦ cs′ , η₀′ , ηv′ , ηc′ , ηh′ , lab′ ⟧ᶜˢ
+    <===>
+    123 ⊢
+      ⟦ [ 457 .-> 233 , 999 .-> 888 ] , 3 , 4 , 2 , 4 , Just ⟦ 0 , 0 , 2 ⟧ℓ ⟧ᶜˢ
+      ⇀⦇ bh ,CHAINHEAD⦈
+      ⟦ [ 457 .-> 234 , 999 .-> 888 ] , 3 , 5 , 2 , 4 , Just ⟦ 1 , 2 , 2 ⟧ℓ ⟧ᶜˢ
+-}
+
+spec :: Spec
+spec = do
+  describe "chainheadStep" $ do
+    it "chainheadStep results in the expected state" $
+      chainheadStep dummyExternalFunctions che chs bh @?= Success chs'

docs/agda-spec/src/Spec/hs-src/test/ProtocolSpec.hs

@@ -24,7 +24,7 @@ ps :: PrtclState
 ps = MkPrtclState
   { psCs = MkHSMap [ hk  .-> 233 , 999 .-> 888 ]
   , psΗv = 3
-  , psΗc = 4
+  , psΗc = 5
   }
 
 oc :: OCert
@@ -64,7 +64,7 @@ hkv = 568
 
 ps' :: PrtclState
 ps' = MkPrtclState
-  { psCs = MkHSMap [(457, 234), (999, 888)],
+  { psCs = MkHSMap [(hk, 234), (999, 888)],
     psΗv = 4,
     psΗc = 4
   }
@@ -82,7 +82,7 @@ ps' = MkPrtclState
                   = id 1
                   = 1
 
-  ∙ ⟦ 1 ⟧ᵘᵉ ⊢ ⟦ 3 , 4 ⟧ᵘˢ ⇀⦇ 0 ,UPDN⦈ ⟦ 3 + 1 , 4 ⟧ᵘˢ
+  ∙ ⟦ 1 ⟧ᵘᵉ ⊢ ⟦ 3 , 5 ⟧ᵘˢ ⇀⦇ 0 ,UPDN⦈ ⟦ 3 + 1 , 3 + 1 ⟧ᵘˢ
 
   ∙ { hk } ⊢ [ hk .-> 233 , 999 .-> 888 ] ⇀⦇ bh ,OCERT⦈ [ hk .-> 234 , 999 .-> 888 ]
 
@@ -142,7 +142,7 @@ ps' = MkPrtclState
               = 0
   ===>
 
-  ⟦ pd , 2 ⟧ᵖᵉ ⊢ ⟦ [ hk .-> 233 , 999 .-> 888 ] , 3 , 4 ⟧ᵖˢ ⇀⦇ bh ,PRTCL⦈ ⟦ [ hk .-> 234 , 999 .-> 888 ] , 4 , 4 ⟧ᵖˢ
+  ⟦ pd , 2 ⟧ᵖᵉ ⊢ ⟦ [ hk .-> 233 , 999 .-> 888 ] , 3 , 5 ⟧ᵖˢ ⇀⦇ bh ,PRTCL⦈ ⟦ [ hk .-> 234 , 999 .-> 888 ] , 4 , 4 ⟧ᵖˢ
 
 -}