From 9302544e072f5e0f82fc4de7973de6904c67ccf9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Javier=20D=C3=ADaz?= <javier.diaz@iohk.io>
Date: Thu, 5 Dec 2024 19:33:12 +0000
Subject: [PATCH] Generate Haskell code for `UpdateNonce`

---
 docs/agda-spec/src/Spec/BaseTypes.lagda       |  3 ++
 .../src/Spec/Foreign/HSConsensus.agda         |  2 +-
 .../Spec/Foreign/HSConsensus/UpdateNonce.agda | 27 +++++++++++
 docs/agda-spec/src/Spec/Foreign/Util.agda     |  8 ++++
 docs/agda-spec/src/Spec/hs-src/Lib.hs         | 10 ++--
 .../cardano-consensus-executable-spec.cabal   |  1 +
 .../src/Spec/hs-src/test/UpdateNonceSpec.hs   | 46 +++++++++++++++++++
 7 files changed, 93 insertions(+), 4 deletions(-)
 create mode 100644 docs/agda-spec/src/Spec/Foreign/HSConsensus/UpdateNonce.agda
 create mode 100644 docs/agda-spec/src/Spec/Foreign/Util.agda
 create mode 100644 docs/agda-spec/src/Spec/hs-src/test/UpdateNonceSpec.hs

diff --git a/docs/agda-spec/src/Spec/BaseTypes.lagda b/docs/agda-spec/src/Spec/BaseTypes.lagda
index 5049a61c8e..38e5c06045 100644
--- a/docs/agda-spec/src/Spec/BaseTypes.lagda
+++ b/docs/agda-spec/src/Spec/BaseTypes.lagda
@@ -22,4 +22,7 @@ open import Data.Nat using (ℕ)
 OCertCounters : Type
 OCertCounters = KeyHashˢ ⇀ ℕ
 
+Slot   = ℕ
+Epoch  = ℕ
+
 \end{code}
diff --git a/docs/agda-spec/src/Spec/Foreign/HSConsensus.agda b/docs/agda-spec/src/Spec/Foreign/HSConsensus.agda
index add652d055..a5fa43ee47 100644
--- a/docs/agda-spec/src/Spec/Foreign/HSConsensus.agda
+++ b/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
diff --git a/docs/agda-spec/src/Spec/Foreign/HSConsensus/UpdateNonce.agda b/docs/agda-spec/src/Spec/Foreign/HSConsensus/UpdateNonce.agda
new file mode 100644
index 0000000000..6e0025a005
--- /dev/null
+++ b/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 #-}
diff --git a/docs/agda-spec/src/Spec/Foreign/Util.agda b/docs/agda-spec/src/Spec/Foreign/Util.agda
new file mode 100644
index 0000000000..32136269ce
--- /dev/null
+++ b/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) #-}
diff --git a/docs/agda-spec/src/Spec/hs-src/Lib.hs b/docs/agda-spec/src/Spec/hs-src/Lib.hs
index 5097326e53..45b343a4cf 100644
--- a/docs/agda-spec/src/Spec/hs-src/Lib.hs
+++ b/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)
diff --git a/docs/agda-spec/src/Spec/hs-src/cardano-consensus-executable-spec.cabal b/docs/agda-spec/src/Spec/hs-src/cardano-consensus-executable-spec.cabal
index 434d4a5167..75777362c5 100644
--- a/docs/agda-spec/src/Spec/hs-src/cardano-consensus-executable-spec.cabal
+++ b/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,
diff --git a/docs/agda-spec/src/Spec/hs-src/test/UpdateNonceSpec.hs b/docs/agda-spec/src/Spec/hs-src/test/UpdateNonceSpec.hs
new file mode 100644
index 0000000000..6a2ed72a51
--- /dev/null
+++ b/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 })