Use the real crypto in formal spec tests

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

@@ -6,13 +6,15 @@ open import Spec.Foreign.HSConsensus.Core
 
 record ExternalFunctions : Type where
   field
+    extSignˢ     : ℕ → ℕ → ℕ
     extIsSignedˢ : ℕ → ℕ → ℕ → Bool
     extIsSignedᵏ : ℕ → ℕ → ℕ → ℕ → Bool
     extExp       : F.Rational → F.Rational
     extLn        : F.Rational → F.Rational
 {-# FOREIGN GHC
   data ExternalFunctions = MkExternalFunctions
-    { extIsSignedDSIG :: Integer -> Integer -> Integer -> Bool
+    { extSignDSIG     :: Integer -> Integer -> Integer
+    , extIsSignedDSIG :: Integer -> Integer -> Integer -> Bool
     , extIsSignedKES  :: Integer -> Integer -> Integer -> Integer -> Bool
     , extExp          :: Rational -> Rational
     , extLn           :: Rational -> Rational
@@ -22,7 +24,8 @@ record ExternalFunctions : Type where
 
 dummyExternalFunctions : ExternalFunctions
 dummyExternalFunctions = record
-  { extIsSignedˢ = λ _ _ _ → true
+  { extSignˢ     = λ _ _ → 0
+  ; extIsSignedˢ = λ _ _ _ → true
   ; 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

@@ -33,7 +33,7 @@ instance
     { pks              = HSPKScheme
     ; Sig              = ℕ
     ; isSigned         = λ vk d σ → extIsSignedˢ vk 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/cabal.project

@@ -1,2 +1,23 @@
 -- TODO: Remove this file when code is properly integrated to the existing setup
+
+-- Custom repository for cardano haskell packages, see CONTRIBUTING for more
+repository cardano-haskell-packages
+  url: https://chap.intersectmbo.org/
+  secure: True
+  root-keys:
+    3e0cce471cf09815f930210f7827266fd09045445d65923e6d0238a6cd15126f
+    443abb7fb497a134c343faf52f0b659bd7999bc06b7f63fa76dc99d631f9bea1
+    a86a1f6ce86c449c46666bda44268677abf29b5b2d2eb5ec7af903ec2f117a82
+    bcec67e8e99cabfa7764d75ad9b158d72bfacf70ca1d0ec8bc6b4406d1bf8413
+    c00aae8461a256275598500ea0e187588c35a5d5d7454fb57eac18d9edb86a56
+    d4a35cd3121aa00d18544bb0ac01c3e1691d618f462c46129271bccf39f7e8ee
+
+-- See CONTRIBUTING for some Nix commands you will need to run if you
+-- update either of these.
+index-state:
+  -- Bump this if you need newer packages from Hackage
+  , hackage.haskell.org 2025-06-03T21:29:34Z
+  -- Bump this if you need newer packages from CHaP
+  , cardano-haskell-packages 2025-06-03T13:42:38Z
+
 packages: .

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

@@ -27,6 +27,8 @@ test-suite test
     hs-source-dirs: test
     main-is: Spec.hs
     other-modules:
+        Base
+        SpecHook
         TickNonceSpec
         UpdateNonceSpec
         OperationalCertificateSpec
@@ -35,9 +37,13 @@ test-suite test
         ChainHeadSpec
     build-depends:
         cardano-consensus-executable-spec,
+        cardano-crypto-class,
+        cardano-protocol-tpraos,
+        cardano-ledger-core,
         hspec,
         HUnit,
-        text
+        text,
+        bytestring
     build-tool-depends: hspec-discover:hspec-discover
     type: exitcode-stdio-1.0
     ghc-options:

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

@@ -0,0 +1,108 @@
+{-# LANGUAGE TypeApplications #-}
+
+module Base (
+  externalFunctions
+, sampleSignKey
+, deriveVkFromSk
+) 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.Util (naturalToBytes, bytesToNatural)
+import Cardano.Crypto.Hash (hashFromBytes, sizeHash)
+import Cardano.Crypto.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
+
+vkeyToInteger :: VKey kd -> Integer
+vkeyToInteger = 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
+
+integerToHash :: forall h a. HashAlgorithm h => Integer -> Maybe (Hash h a)
+integerToHash = hashFromBytes . naturalToBytes (fromIntegral . sizeHash $ Proxy @h) . fromInteger
+
+signedDSIGNFromInteger :: forall v a. DSIGNAlgorithm v => Integer -> SignedDSIGN v a
+signedDSIGNFromInteger n =
+  SignedDSIGN
+    . fromMaybe
+      (error "Failed to decode the signature")
+    $ signatureFromInteger n
+
+signedDSIGNToInteger :: DSIGNAlgorithm v => SignedDSIGN v a -> Integer
+signedDSIGNToInteger (SignedDSIGN x) = signatureToInteger x
+
+externalFunctions :: ExternalFunctions
+externalFunctions = dummyExternalFunctions
+  { extSignDSIG     = extSignDSIG'
+  , extIsSignedDSIG = extIsSignedDSIG'
+  }
+  where
+    extSignDSIG' sk ser =
+      signedDSIGNToInteger $
+        signedDSIGN
+          @DSIGN
+          @(Hash HASH ByteString)
+          ()
+          hash
+          skey
+      where
+        skey =
+          fromMaybe
+            (error "Failed to convert an Agda SKey to a Haskell SKey")
+            $ skeyDSIGNFromInteger sk
+        hash =
+          fromMaybe
+            (error $ "Failed to get hash from integer:\n" <> show ser)
+          $ integerToHash ser
+
+    extIsSignedDSIG' vk ser sig =
+      isRight $
+        verifySignedDSIGN
+          @DSIGN
+          @(Hash HASH ByteString)
+          ()
+          vkey
+          hash
+          signature
+      where
+        vkey =
+          unVKey
+            . fromMaybe (error "Failed to convert an Agda VKey to a Haskell VKey")
+            $ vkeyFromInteger 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')
+
+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

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

@@ -1,3 +1,5 @@
+{-# LANGUAGE OverloadedRecordDot #-}
+
 module OperationalCertificateSpec (spec) where
 
 import Data.Text
@@ -6,10 +8,15 @@ import Test.Hspec ( Spec, describe, it )
 import Test.HUnit ( (@?=) )
 
 import Lib
+import Base (externalFunctions, sampleSignKey, deriveVkFromSk)
 
 (.->) :: a -> b -> (a, b)
 (.->) = (,)
 
+-- Context
+coldSk :: Integer
+coldSk = sampleSignKey
+
 stpools :: OCertEnv
 stpools = MkHSSet []
 
@@ -30,13 +37,16 @@ oc = MkOCert
   { ocVkₕ = 123
   , ocN   = 234
   , ocC₀  = 0
-  , ocΣ   = 345
+  , ocΣ   = ocΣ'
   }
+  where
+    encodedOc = 0 -- since encode (ocVkₕ , ocN , ocC₀) == 0
+    ocΣ'      = externalFunctions.extSignDSIG coldSk encodedOc
 
 bhb :: BHBody
 bhb = MkBHBody
   { bhbPrevHeader = Nothing
-  , bhbIssuerVk   = 456
+  , bhbIssuerVk   = deriveVkFromSk coldSk
   , bhbVrfVk      = 567
   , bhbBlockNo    = 1
   , bhbSlot       = 0
@@ -57,21 +67,18 @@ bh = MkBHeader
 hk :: KeyHashS
 hk = succ (bhbIssuerVk bhb) -- i.e., hash (bhbIssuerVk bhb)
 
-externalFunctions :: ExternalFunctions
-externalFunctions = dummyExternalFunctions { extIsSignedDSIG = \ _ _ sig -> sig > 0 }
-
 -- NOTE: Why should this test succeed? Here's the explanation:
 --
--- hk = hash bhbIssuerVk = hash 456 = 457
+-- hk = hash bhbIssuerVk = succ bhbIssuerVk
 -- kp = kesPeriod bhbSlot = kesPeriod 0 = 0 / SlotsPerKESPeriodᶜ = 0 / 5 = 0
 -- t = kp -ᵏ ocC₀ = 0 - 0 = 0
 --
 -- ∙ ocC₀ ≤ kp <=> 0 ≤ 0 <=> true
 -- ∙ 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ˢ 456 (encode (123 , 234 , 0)) 345
---    <=> isSignedˢ 456 0 345
+--    <=> isSignedˢ bhbIssuerVk (encode (123 , 234 , 0)) ocΣ
+--    <=> isSignedˢ bhbIssuerVk 0 ocΣ
 --    <=> true
 -- ∙ isSignedᵏ ocVkₕ t (encode bhb) 901
 --    <=> isSignedᵏ 123 0 (encode bhb) 901

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

@@ -0,0 +1,8 @@
+module SpecHook where
+
+import Test.Hspec
+import Cardano.Crypto.Init (cryptoInit)
+
+hook :: Spec -> Spec
+hook = before_ cryptoInit
+

nix/agda.nix

@@ -108,7 +108,17 @@ let
     hsExe = customAgda.haskell.lib.disableLibraryProfiling (customAgda.haskellPackages.callCabal2nixWithOptions "cardano-consensus-executable-spec" "${hsSrc}/haskell/Spec" "--no-haddock" { });
 
     shell = pkgs.mkShell {
-      packages = [ agda latex customAgda.ghc customAgda.cabal-install ];
+      packages = [
+        agda
+        latex
+        customAgda.ghc
+        customAgda.cabal-install
+        final.pkg-config
+        final.libsodium-vrf
+        final.blst
+        final.secp256k1
+        final.zlib
+      ];
     };
   };
 in