Use the real crypto in formal spec tests

docs/agda-spec/src/Ledger/Crypto.lagda

@@ -172,7 +172,9 @@ record KESScheme (srl : Serializer) : Type₁ where
 
 \begin{figure*}[h]
 \begin{code}[hide]
-record VRFScheme : Type₁ where
+record VRFScheme (srl : Serializer) : Type₁ where
+  open Serializer srl
+
   field
         pks : PKScheme
 
@@ -183,18 +185,18 @@ record VRFScheme : Type₁ where
 \emph{Types \& functions}
 \begin{code}
         Seed Proof : Type
-        verify     : {T : Type} → VKey → Seed → Proof × T → Type
-        evaluate   : {T : Type} → SKey → Seed → Proof × T
+        verify     : VKey → Seed → Proof × Ser → Type
+        evaluate   : SKey → Seed → Proof × Ser
         _XOR_      : Seed → Seed → Seed
 \end{code}
 \emph{Properties}
 \begin{code}[hide]
-  field ⦃ Dec-verify ⦄ : {T : Type} → verify {T} ⁇³
+  field ⦃ Dec-verify ⦄ : verify ⁇³
         verify-correct :
 \end{code}
 \begin{code}        
-          ∀ {T : Type} ((sk , vk , _) : KeyPair) (seed : Seed)
-            → verify {T = T} vk seed (evaluate sk seed)
+          ∀ ((sk , vk , _) : KeyPair) (seed : Seed)
+            → verify vk seed (evaluate sk seed)
 \end{code}
 \begin{code}[hide]         
         ⦃ DecEq-Seed  ⦄ : DecEq Seed
@@ -211,7 +213,7 @@ record Crypto : Type₁ where
   field srl  : Serializer
         dsig : DSigScheme srl
         kes  : KESScheme srl
-        vrf  : VRFScheme
+        vrf  : VRFScheme srl
 
   open Serializer srl public
   open DSigScheme dsig renaming (VKey to VKeyˢ; Sig to Sigˢ; isSigned to isSignedˢ) public

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

@@ -27,18 +27,16 @@ record BlockStructure : Type₁ where
 \begin{code}
     HashHeader : Type -- hash of a block header
     HashBBody  : Type -- hash of a block body
-    VRFRes     : Type -- VRF result value
 \end{code}
 \begin{code}[hide]
     ⦃ DecEq-HashHeader ⦄ : DecEq HashHeader
     ⦃ DecEq-HashBBody  ⦄ : DecEq HashBBody
-    ⦃ DecEq-VRFRes     ⦄ : DecEq VRFRes
     ⦃ Show-HashHeader  ⦄ : Show HashHeader
     ⦃ Show-HashBBody   ⦄ : Show HashBBody
-    ⦃ Show-VRFRes      ⦄ : Show VRFRes
 \end{code}
 \emph{Concrete types}
 \begin{code}
+  VRFRes = Ser -- VRF result value
   BlockNo = ℕ -- block number
   Certifiedℕ = ∃[ n ] n < 2 ^ 512 -- [0, 2^512) (64-byte VRF output)
 \end{code}

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

@@ -2,18 +2,27 @@ module Spec.Foreign.ExternalFunctions where -- TODO: Complete
 
 open import Ledger.Prelude
 import Spec.Foreign.HSTypes as F using (Rational)
+import Foreign.Haskell as F using (Pair; _,_)
 open import Spec.Foreign.HSConsensus.Core
 
 record ExternalFunctions : Type where
   field
+    extSignˢ     : ℕ → ℕ → ℕ
     extIsSignedˢ : ℕ → ℕ → ℕ → Bool
+    extSignᵏ     : (ℕ → ℕ) → ℕ → ℕ → ℕ
     extIsSignedᵏ : ℕ → ℕ → ℕ → ℕ → Bool
+    extEvaluate  : ℕ → ℕ → F.Pair ℕ ℕ
+    extVerify    : ℕ → ℕ → F.Pair ℕ ℕ → 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
+    , extSignKES      :: (Integer -> Integer) -> Integer -> Integer -> Integer
     , extIsSignedKES  :: Integer -> Integer -> Integer -> Integer -> Bool
+    , extEvaluate     :: Integer -> Integer -> (Integer , Integer)
+    , extVerify       :: Integer -> Integer -> (Integer , Integer) -> Bool
     , extExp          :: Rational -> Rational
     , extLn           :: Rational -> Rational
     }
@@ -22,8 +31,12 @@ record ExternalFunctions : Type where
 
 dummyExternalFunctions : ExternalFunctions
 dummyExternalFunctions = record
-  { extIsSignedˢ = λ _ _ _ → true
+  { extSignˢ     = λ _ _ → 0
+  ; extIsSignedˢ = λ _ _ _ → true
+  ; extSignᵏ     = λ _ _ _ → 0
   ; extIsSignedᵏ = λ _ _ _ _ → true
+  ; extEvaluate  = λ _ _ → 0 F., 0
+  ; extVerify    = λ _ _ _ → 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

@@ -5,6 +5,7 @@ module Spec.Foreign.HSConsensus.ExternalStructures (externalFunctions : External
 open import Ledger.Crypto
 open import Ledger.Types.Epoch
 open import Spec.Foreign.HSConsensus.Core
+open import Foreign.Haskell.Coerce
 
 HSGlobalConstants = GlobalConstants ∋ record {Implementation}
 instance
@@ -33,7 +34,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     = ⁇ (_ ≟ _)
     }
@@ -45,25 +46,26 @@ 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     = ⁇ (_ ≟ _)
     }
     where
       open ExternalFunctions externalFunctions
 
-  -- NOTE: Dummy for now.
-  HSVRFScheme : VRFScheme
+  HSVRFScheme : VRFScheme HSSerializer
   HSVRFScheme = record
     { Implementation
     ; pks            = HSPKScheme
     ; Proof          = ℕ
-    ; verify         = λ _ _ _ → ⊤
-    ; evaluate       = error "evaluate evaluated"
+    ; verify         = λ vk seed out → extVerify vk seed (coerce out) ≡ true
+    ; evaluate       = coerce ∘ extEvaluate
     ; _XOR_          = _+_
     ; verify-correct = error "verify-correct evaluated"
-    ; Dec-verify     = λ {T = _} {_} {_} {_} → ⁇ (true because ofʸ tt)
+    ; Dec-verify     = ⁇ (_ ≟ _)
     }
+    where
+      open ExternalFunctions externalFunctions
 
   HSCrypto : Crypto
   HSCrypto = record
@@ -92,7 +94,6 @@ instance
   HSBlockStructure = record
     { HashHeader       = ℕ
     ; HashBBody        = ℕ
-    ; VRFRes           = ℕ
     ; DecEq-HashHeader = DecEq-ℕ
     }
 

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

@@ -86,7 +86,7 @@ module _ (ext : ExternalFunctions) where
                   ∷ ("slotToSeed slot                     \t: " +ˢ show stsslot)
                   ∷ ("nonceToSeed η₀                      \t: " +ˢ show ntsη₀)
                   ∷ ("seed                                \t: " +ˢ show seed)
-                  ∷ ("verify vrfVk seed (vrfPrf , vrfRes) \t: " +ˢ show (⌊ ¿ verify {T = VRFRes} ¿³ vrfVk seed (vrfPrf , vrfRes) ⌋))
+                  ∷ ("verify vrfVk seed (vrfPrf , vrfRes) \t: " +ˢ show (⌊ ¿ verify ¿³ vrfVk seed (vrfPrf , vrfRes) ⌋))
                   ∷ ("hBLeader bhb                        \t: " +ˢ Show-Certifiedℕ {DummyBlockStructure} .show t)
                   ∷ ("f                                   \t: " +ˢ show ActiveSlotCoeff)
                   ∷ ("checkLeaderVal? (hBLeader bhb) f σ  \t: " +ˢ show (⌊ checkLeaderVal? t ActiveSlotCoeff σ ⌋))

docs/agda-spec/src/Spec/Protocol/Properties.agda

@@ -51,7 +51,7 @@ vrfChecks? η₀ pd f bhb
 ... | nothing          = no λ ()
 ... | just (σ , vrfHK) =
         vrfHK ≟ hash vrfVk
-        ×-dec ¿ verify {T = VRFRes} ¿³ vrfVk seed (vrfPrf , vrfRes)
+        ×-dec ¿ verify ¿³ vrfVk seed (vrfPrf , vrfRes)
         ×-dec checkLeaderVal? (hBLeader bhb) f σ
   where
     open BHBody bhb

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,16 @@ test-suite test
         ChainHeadSpec
     build-depends:
         cardano-consensus-executable-spec,
+        cardano-crypto-class,
+        cardano-crypto-praos >= 2.2.1.0,
+        cardano-protocol-tpraos ^>=1.4,
+        cardano-ledger-core,
+        ouroboros-consensus-protocol,
         hspec,
         HUnit,
-        text
+        text,
+        bytestring,
+        io-classes >=1.4.0,
     build-tool-depends: hspec-discover:hspec-discover
     type: exitcode-stdio-1.0
     ghc-options: