Generate Haskell code for UpdateNonce

docs/agda-spec/src/Spec/BaseTypes.lagda

@@ -22,4 +22,7 @@ open import Data.Nat using (ℕ)
 OCertCounters : Type
 OCertCounters = KeyHashˢ ⇀ ℕ
 
+Slot   = ℕ
+Epoch  = ℕ
+
 \end{code}

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

@@ -1,4 +1,4 @@
 module Spec.Foreign.HSConsensus where
 
 open import Spec.Foreign.HSConsensus.TickNonce public
-
+open import Spec.Foreign.HSConsensus.UpdateNonce public

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

@@ -0,0 +1,27 @@
+module Spec.Foreign.HSConsensus.UpdateNonce where
+
+open import Spec.Foreign.ExternalFunctions
+
+open import Foreign.Haskell.Coerce
+
+open import Spec.Foreign.HSConsensus.BaseTypes
+open import Spec.UpdateNonce DummyCrypto DummyNonces DummyEpochStructure
+
+instance
+
+  HsTy-UpdateNonceEnv = autoHsType UpdateNonceEnv ⊣ withConstructor "MkUpdateNonceEnv"
+                                                  • fieldPrefix "ue"
+  Conv-UpdateNonceEnv = autoConvert UpdateNonceEnv
+
+  HsTy-UpdateNonceState = autoHsType UpdateNonceState ⊣ withConstructor "MkUpdateNonceState"
+                                                      • fieldPrefix "us"
+  Conv-UpdateNonceState = autoConvert UpdateNonceState
+
+module _ (ext : ExternalFunctions) where
+  open ExternalStructures ext hiding (Slot)
+  open import Spec.UpdateNonce.Properties HSCrypto HSNonces HSEpochStructure
+
+  updn-step : HsType (UpdateNonceEnv → UpdateNonceState → Slot → ComputationResult String UpdateNonceState)
+  updn-step = to (coerce ⦃ TrustMe ⦄ $ compute Computational-UPDN)
+
+  {-# COMPILE GHC updn-step as updnStep #-}

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

@@ -0,0 +1,8 @@
+module Spec.Foreign.Util where
+
+open import Ledger.Prelude
+
+postulate
+  error : {A : Set} → String → A
+{-# FOREIGN GHC import Data.Text #-}
+{-# COMPILE GHC error = \ _ s -> error (unpack s) #-}

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

@@ -3,9 +3,13 @@ module Lib
   , module Lib
   ) where
 
-import MAlonzo.Code.Spec.Foreign.HSTypes               as X
+import MAlonzo.Code.Spec.Foreign.HSTypes                 as X
   (ComputationResult(..)) -- TODO: Complete
-import MAlonzo.Code.Spec.Foreign.HSConsensus.TickNonce as X
+import MAlonzo.Code.Spec.Foreign.HSConsensus.TickNonce   as X
   (TickNonceEnv(..), TickNonceState(..), ticknStep)
-import MAlonzo.Code.Spec.Foreign.ExternalFunctions     as X
+import MAlonzo.Code.Spec.Foreign.HSConsensus.UpdateNonce as X
+  (UpdateNonceEnv(..), UpdateNonceState(..), updnStep)
+import MAlonzo.Code.Spec.Foreign.HSConsensus.BaseTypes   as X
+  (Slot, Epoch)
+import MAlonzo.Code.Spec.Foreign.ExternalFunctions       as X
   (ExternalFunctions(..), dummyExternalFunctions)

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

@@ -33,6 +33,7 @@ test-suite test
     main-is: Spec.hs
     other-modules:
         TickNonceSpec
+        UpdateNonceSpec
     build-depends:
         cardano-consensus-executable-spec,
         hspec,

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

@@ -0,0 +1,46 @@
+{-# LANGUAGE StandaloneDeriving #-}
+{-# OPTIONS -Wno-orphans #-}
+module UpdateNonceSpec (spec) where
+
+import Data.Text
+
+import Test.Hspec ( Spec, describe, it )
+import Test.HUnit ( (@?=) )
+
+import Lib
+
+initEnv :: UpdateNonceEnv
+initEnv = MkUpdateNonceEnv { ueΗ = 2 }
+
+initState :: UpdateNonceState
+initState = MkUpdateNonceState { usΗv = 3, usΗc = 4 }
+
+slotBeforeWindow :: Slot
+slotBeforeWindow = 1
+
+testUpdateNonceStepWithSlotBeforeWindow :: ComputationResult Text UpdateNonceState
+testUpdateNonceStepWithSlotBeforeWindow = updnStep dummyExternalFunctions initEnv initState slotBeforeWindow
+
+{-                      window = 20
+                      ______________
+                     /              \
+                     s
+ +---+---+---+---+---+---+---+---+---+---+---+---+
+ 0  1  2 ...         99  100         119 ... 199 200
+ \___________________/   \___________________/
+        epoch 0                 epoch 1
+-}
+
+slotAfterWindow :: Slot
+slotAfterWindow = 99
+
+testUpdateNonceStepWithSlotAfterWindow :: ComputationResult Text UpdateNonceState
+testUpdateNonceStepWithSlotAfterWindow = updnStep dummyExternalFunctions initEnv initState slotAfterWindow
+
+spec :: Spec
+spec = do
+  describe "updnStep" $ do
+    it "updnStep results in the expected state with slot before window" $
+      testUpdateNonceStepWithSlotBeforeWindow @?= Success (MkUpdateNonceState { usΗv = 3 + 2, usΗc = 3 + 2 })
+    it "updnStep results in the expected state with slot after window" $
+      testUpdateNonceStepWithSlotAfterWindow @?= Success (MkUpdateNonceState { usΗv = 3 + 2, usΗc = 4 })