Use the real crypto in formal spec tests

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

@@ -8,13 +8,15 @@ record ExternalFunctions : Type where
   field
     extSignˢ     : ℕ → ℕ → ℕ
     extIsSignedˢ : ℕ → ℕ → ℕ → Bool
+    extSignᵏ     : (ℕ → ℕ) → ℕ → ℕ → ℕ
     extIsSignedᵏ : ℕ → ℕ → ℕ → ℕ → Bool
     extExp       : F.Rational → F.Rational
     extLn        : F.Rational → F.Rational
 {-# FOREIGN GHC
   data ExternalFunctions = MkExternalFunctions
     { extSignDSIG     :: Integer -> Integer -> Integer
     , extIsSignedDSIG :: Integer -> Integer -> Integer -> Bool
+    , extSignKES      :: (Integer -> Integer) -> Integer -> Integer -> Integer
     , extIsSignedKES  :: Integer -> Integer -> Integer -> Integer -> Bool
     , extExp          :: Rational -> Rational
     , extLn           :: Rational -> Rational
@@ -26,6 +28,7 @@ dummyExternalFunctions : ExternalFunctions
 dummyExternalFunctions = record
   { extSignˢ     = λ _ _ → 0
   ; extIsSignedˢ = λ _ _ _ → true
+  ; extSignᵏ     = λ _ _ _ → 0
   ; extIsSignedᵏ = λ _ _ _ _ → true
   ; extExp       = λ p → to (rationalExtStructure≈ .exp (from p))
   ; extLn        = λ p → to (rationalExtStructure≈ .ln (from p) ⦃ if (from p) ℚ.> 0ℚ then (λ{p>0} → positive p>0) else error "Not a positive rational number" ⦄)

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

@@ -45,7 +45,7 @@ instance
     { pks              = HSPKScheme
     ; Sig              = ℕ
     ; isSigned         = λ vk n d σ → extIsSignedᵏ vk n d σ ≡ true
-    ; sign             = λ _ _ _ → 0 -- NOTE: Dummy for now
+    ; sign             = extSignᵏ
     ; isSigned-correct = error "isSigned-correct evaluated"
     ; Dec-isSigned     = ⁇ (_ ≟ _)
     }

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

@@ -38,12 +38,13 @@ test-suite test
     build-depends:
         cardano-consensus-executable-spec,
         cardano-crypto-class,
-        cardano-protocol-tpraos,
+        cardano-protocol-tpraos ^>=1.4,
         cardano-ledger-core,
         hspec,
         HUnit,
         text,
-        bytestring
+        bytestring,
+        io-classes >=1.4.0,
     build-tool-depends: hspec-discover:hspec-discover
     type: exitcode-stdio-1.0
     ghc-options:

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

@@ -2,59 +2,118 @@
 
 module Base (
   externalFunctions
-, sampleSignKey
-, deriveVkFromSk
+, sampleSKeyDSIGN
+, deriveVkeyDSIGFromSkeyDSIG
+, sampleSKeyKES
+, deriveVkeyKESFromSkeyKES
 ) where
 
 import Lib
 
 import Cardano.Ledger.Hashes (Hash, HASH, HashAlgorithm)
 import Cardano.Ledger.Keys (DSIGN, VKey (..))
-import Cardano.Crypto.DSIGN (DSIGNAlgorithm (..), SignedDSIGN (..), verifySignedDSIGN, signedDSIGN, Ed25519DSIGN)
+import Cardano.Crypto.DSIGN (DSIGNAlgorithm (..), SignedDSIGN (..), verifySignedDSIGN, signedDSIGN)
+import qualified Cardano.Crypto.KES as KES
 import Cardano.Crypto.Util (naturalToBytes, bytesToNatural)
 import Cardano.Crypto.Hash (hashFromBytes, sizeHash)
-import Cardano.Crypto.Seed (mkSeedFromBytes)
+import Cardano.Crypto.Seed (Seed, mkSeedFromBytes)
 import Data.Data (Proxy (..))
 import Data.ByteString (ByteString)
 import qualified Data.ByteString.Char8 as BC
 import Data.Either (isRight)
 import Data.Maybe (fromMaybe)
 
-vkeyFromInteger :: Integer -> Maybe (VKey kd)
-vkeyFromInteger = fmap VKey . rawDeserialiseVerKeyDSIGN . naturalToBytes 32 . fromInteger
+-- Hashes
 
-vkeyToInteger :: VKey kd -> Integer
-vkeyToInteger = toInteger . bytesToNatural . rawSerialiseVerKeyDSIGN . unVKey
+integerToHash :: forall h a. HashAlgorithm h => Integer -> Maybe (Hash h a)
+integerToHash = hashFromBytes . naturalToBytes (fromIntegral . sizeHash $ Proxy @h) . fromInteger
+
+-- DSIGN
+
+vkeyDSIGNFromInteger :: Integer -> Maybe (VKey kd)
+vkeyDSIGNFromInteger = fmap VKey . rawDeserialiseVerKeyDSIGN . naturalToBytes 32 . fromInteger
+
+vkeyDSIGNToInteger :: VKey kd -> Integer
+vkeyDSIGNToInteger = toInteger . bytesToNatural . rawSerialiseVerKeyDSIGN . unVKey
 
 skeyDSIGNFromInteger :: DSIGNAlgorithm v => Integer -> Maybe (SignKeyDSIGN v)
 skeyDSIGNFromInteger = rawDeserialiseSignKeyDSIGN . naturalToBytes 32 . fromInteger
 
 skeyDSIGNToInteger :: DSIGNAlgorithm v => SignKeyDSIGN v -> Integer
 skeyDSIGNToInteger = toInteger . bytesToNatural . rawSerialiseSignKeyDSIGN
 
-signatureFromInteger :: DSIGNAlgorithm v => Integer -> Maybe (SigDSIGN v)
-signatureFromInteger = rawDeserialiseSigDSIGN . naturalToBytes 64 . fromInteger
-
-signatureToInteger :: DSIGNAlgorithm v => SigDSIGN v -> Integer
-signatureToInteger = toInteger . bytesToNatural . rawSerialiseSigDSIGN
+sigDSIGNFromInteger :: DSIGNAlgorithm v => Integer -> Maybe (SigDSIGN v)
+sigDSIGNFromInteger = rawDeserialiseSigDSIGN . naturalToBytes 64 . fromInteger
 
-integerToHash :: forall h a. HashAlgorithm h => Integer -> Maybe (Hash h a)
-integerToHash = hashFromBytes . naturalToBytes (fromIntegral . sizeHash $ Proxy @h) . fromInteger
+sigDSIGNToInteger :: DSIGNAlgorithm v => SigDSIGN v -> Integer
+sigDSIGNToInteger = toInteger . bytesToNatural . rawSerialiseSigDSIGN
 
 signedDSIGNFromInteger :: forall v a. DSIGNAlgorithm v => Integer -> SignedDSIGN v a
 signedDSIGNFromInteger n =
   SignedDSIGN
     . fromMaybe
-      (error "Failed to decode the signature")
-    $ signatureFromInteger n
+      (error "Failed to decode the DSIGN signature")
+      $ sigDSIGNFromInteger n
 
 signedDSIGNToInteger :: DSIGNAlgorithm v => SignedDSIGN v a -> Integer
-signedDSIGNToInteger (SignedDSIGN x) = signatureToInteger x
+signedDSIGNToInteger (SignedDSIGN x) = sigDSIGNToInteger x
+
+deriveVkeyDSIGFromSkeyDSIG :: Integer -> Integer
+deriveVkeyDSIGFromSkeyDSIG sk = vkeyDSIGNToInteger $ VKey $ deriveVerKeyDSIGN skey
+  where
+    skey =
+      fromMaybe
+        (error "Failed to convert an Agda DSIGN SKey to a Haskell DSIGN SKey")
+        $ skeyDSIGNFromInteger sk
+
+-- KES
+
+type KESAlg = KES.Sum6KES DSIGN HASH
+
+vkeyKESFromInteger :: forall v. KES.KESAlgorithm v => Integer -> Maybe (KES.VerKeyKES v)
+vkeyKESFromInteger = KES.rawDeserialiseVerKeyKES . naturalToBytes (fromIntegral $ KES.sizeVerKeyKES $ Proxy @KESAlg) . fromInteger
+
+vkeyKESToInteger :: KES.KESAlgorithm v => KES.VerKeyKES v -> Integer
+vkeyKESToInteger = toInteger . bytesToNatural . KES.rawSerialiseVerKeyKES
+
+skeyKESFromInteger :: forall v. KES.UnsoundPureKESAlgorithm v => Integer -> Maybe (KES.UnsoundPureSignKeyKES v)
+skeyKESFromInteger = KES.rawDeserialiseUnsoundPureSignKeyKES . naturalToBytes (fromIntegral $ KES.sizeSignKeyKES $ Proxy @KESAlg) . fromInteger
+
+skeyKESToInteger :: KES.UnsoundPureKESAlgorithm v => KES.UnsoundPureSignKeyKES v -> Integer
+skeyKESToInteger = toInteger . bytesToNatural . KES.rawSerialiseUnsoundPureSignKeyKES
+
+sigKESFromInteger :: forall v. KES.KESAlgorithm v => Integer -> Maybe (KES.SigKES v)
+sigKESFromInteger = KES.rawDeserialiseSigKES . naturalToBytes (fromIntegral $ KES.sizeSigKES $ Proxy @KESAlg) . fromInteger
+
+sigKESToInteger :: KES.KESAlgorithm v => KES.SigKES v -> Integer
+sigKESToInteger = toInteger . bytesToNatural . KES.rawSerialiseSigKES
+
+signedKESFromInteger :: forall v a. KES.KESAlgorithm v => Integer -> KES.SignedKES v a
+signedKESFromInteger n =
+  KES.SignedKES
+    . fromMaybe
+        (error "Failed to decode the KES signature")
+        $ sigKESFromInteger n
+
+signedKESToInteger :: KES.KESAlgorithm v => KES.SignedKES v a -> Integer
+signedKESToInteger (KES.SignedKES x) = sigKESToInteger x
+
+deriveVkeyKESFromSkeyKES :: Integer -> Integer
+deriveVkeyKESFromSkeyKES sk = vkeyKESToInteger @KESAlg $ KES.unsoundPureDeriveVerKeyKES skey
+  where
+    skey =
+      fromMaybe
+        (error "Failed to convert an Agda KES SKey to a Haskell KES SKey")
+        $ skeyKESFromInteger sk
+
+-- External functions
 
 externalFunctions :: ExternalFunctions
 externalFunctions = dummyExternalFunctions
   { extSignDSIG     = extSignDSIG'
   , extIsSignedDSIG = extIsSignedDSIG'
+  , extSignKES      = extSignKES'
+  , extIsSignedKES  = extIsSignedKES'
   }
   where
     extSignDSIG' sk ser =
@@ -73,7 +132,7 @@ externalFunctions = dummyExternalFunctions
         hash =
           fromMaybe
             (error $ "Failed to get hash from integer:\n" <> show ser)
-          $ integerToHash ser
+            $ integerToHash ser
 
     extIsSignedDSIG' vk ser sig =
       isRight $
@@ -88,21 +147,66 @@ externalFunctions = dummyExternalFunctions
         vkey =
           unVKey
             . fromMaybe (error "Failed to convert an Agda VKey to a Haskell VKey")
-            $ vkeyFromInteger vk
+            $ vkeyDSIGNFromInteger vk
         hash =
           fromMaybe
             (error $ "Failed to get hash from integer:\n" <> show ser)
             $ integerToHash ser
         signature =
           signedDSIGNFromInteger sig
 
-sampleSignKey :: Integer
-sampleSignKey = skeyDSIGNToInteger $ genKeyDSIGN @Ed25519DSIGN (mkSeedFromBytes $ BC.pack $ replicate 32 '0')
+    extSignKES' skf n ser =
+      sigKESToInteger $
+        KES.unsoundPureSignKES
+          @KESAlg
+          @(Hash HASH ByteString)
+          ()
+          kp
+          hash
+          skey
+      where
+        skey =
+          fromMaybe
+            (error "Failed to convert an Agda KES SKey to a Haskell KES SKey")
+            $ skeyKESFromInteger (skf n)
+        kp =
+          fromIntegral n
+        hash =
+          fromMaybe
+            (error $ "Failed to get hash from integer:\n" <> show ser)
+            $ integerToHash ser
 
-deriveVkFromSk :: Integer -> Integer
-deriveVkFromSk sk = vkeyToInteger $ VKey $ deriveVerKeyDSIGN skey
-  where
-    skey =
-      fromMaybe
-        (error "Failed to convert an Agda SKey to a Haskell SKey")
-        $ skeyDSIGNFromInteger sk
+    extIsSignedKES' vk n ser sig =
+      isRight $
+        KES.verifySignedKES
+          @KESAlg
+          @(Hash HASH ByteString)
+          ()
+          vkey
+          kp
+          hash
+          signature
+      where
+        vkey =
+          fromMaybe
+            (error "Failed to convert an Agda KES VKey to a Haskell KES VKey")
+            $ vkeyKESFromInteger vk
+        kp =
+          fromIntegral n
+        hash =
+          fromMaybe
+            (error $ "Failed to get hash from integer:\n" <> show ser)
+            $ integerToHash ser
+        signature =
+          signedKESFromInteger sig
+
+-- Utilities
+
+sampleSeed :: Seed
+sampleSeed = mkSeedFromBytes $ BC.pack $ replicate 32 '0'
+
+sampleSKeyDSIGN :: Integer
+sampleSKeyDSIGN = skeyDSIGNToInteger $ genKeyDSIGN @DSIGN sampleSeed
+
+sampleSKeyKES :: Integer
+sampleSKeyKES = skeyKESToInteger @KESAlg $ KES.unsoundPureGenKeyKES sampleSeed

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

@@ -8,14 +8,30 @@ import Test.Hspec ( Spec, describe, it )
 import Test.HUnit ( (@?=) )
 
 import Lib
-import Base (externalFunctions, sampleSignKey, deriveVkFromSk)
+import Base (
+    externalFunctions
+  , sampleSKeyDSIGN
+  , deriveVkeyDSIGFromSkeyDSIG
+  , sampleSKeyKES
+  , deriveVkeyKESFromSkeyKES)
 
 (.->) :: a -> b -> (a, b)
 (.->) = (,)
 
--- Context
 coldSk :: Integer
-coldSk = sampleSignKey
+coldSk = sampleSKeyDSIGN
+
+hotSk :: Integer
+hotSk = sampleSKeyKES
+
+-- Since kp = kesPeriod bhbSlot = kesPeriod 0 = 0 / SlotsPerKESPeriodᶜ = 0 / 5 = 0,
+-- then period = kp -ᵏ ocC₀ = 0 - 0 = 0.
+period :: Integer
+period = 0
+
+skf :: Integer -> Integer
+skf 0 = hotSk -- for period 0
+skf _ = succ hotSk
 
 stpools :: OCertEnv
 stpools = MkHSSet []
@@ -34,19 +50,19 @@ cs' = MkHSMap
 
 oc :: OCert
 oc = MkOCert
-  { ocVkₕ = 123
+  { ocVkₕ = deriveVkeyKESFromSkeyKES hotSk
   , ocN   = 234
   , ocC₀  = 0
   , ocΣ   = ocΣ'
   }
   where
-    encodedOc = 0 -- since encode (ocVkₕ , ocN , ocC₀) == 0
+    encodedOc = 0 -- since encode (ocVkₕ , ocN , ocC₀) = 0
     ocΣ'      = externalFunctions.extSignDSIG coldSk encodedOc
 
 bhb :: BHBody
 bhb = MkBHBody
   { bhbPrevHeader = Nothing
-  , bhbIssuerVk   = deriveVkFromSk coldSk
+  , bhbIssuerVk   = deriveVkeyDSIGFromSkeyDSIG coldSk
   , bhbVrfVk      = 567
   , bhbBlockNo    = 1
   , bhbSlot       = 0
@@ -61,8 +77,11 @@ bhb = MkBHBody
 bh :: BHeader
 bh = MkBHeader
   { bhBody = bhb
-  , bhSig  = 901
+  , bhSig  = bhSig'
   }
+  where
+    encodedBhb = 0 -- since encode bhb = 0
+    bhSig'     = externalFunctions.extSignKES skf period encodedBhb
 
 hk :: KeyHashS
 hk = succ (bhbIssuerVk bhb) -- i.e., hash (bhbIssuerVk bhb)
@@ -77,12 +96,12 @@ hk = succ (bhbIssuerVk bhb) -- i.e., hash (bhbIssuerVk bhb)
 -- ∙ kp < ocC₀ +ᵏ MaxKESEvo <=> 0 < 0 + 30 <=> 0 < 30 <=> true
 -- ∙ just 233 ≡ currentIssueNo stpools cs hk × (234 ≡ 233 ⊎ 234 ≡ suc 233))
 -- ∙ isSignedˢ bhbIssuerVk (encode (ocVkₕ , ocN , ocC₀)) ocΣ
---    <=> isSignedˢ bhbIssuerVk (encode (123 , 234 , 0)) ocΣ
+--    <=> isSignedˢ bhbIssuerVk (encode (ocVkₕ , 234 , 0)) ocΣ
 --    <=> isSignedˢ bhbIssuerVk 0 ocΣ
 --    <=> true
--- ∙ isSignedᵏ ocVkₕ t (encode bhb) 901
---    <=> isSignedᵏ 123 0 (encode bhb) 901
---    <=> isSignedᵏ 123 0 0 901
+-- ∙ isSignedᵏ ocVkₕ t (encode bhb) bhSig
+--    <=> isSignedᵏ ocVkₕ 0 (encode bhb) bhSig
+--    <=> isSignedᵏ ocVkₕ 0 0 bhSig
 --    <=> true
 
 spec :: Spec