Add alias for type of 64-byte VRF outputs

Author: javierdiaz72

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

@@ -34,6 +34,7 @@ record BlockStructure : Type₁ where
 \emph{Concrete types}
 \begin{code}
   BlockNo = ℕ -- block number
+  Certifiedℕ = ∃[ n ] n < 2 ^ 512 -- [0, 2^512) (64-byte VRF output)
 \end{code}
 \emph{Operational Certificate}
 \begin{AgdaSuppressSpace}
@@ -87,7 +88,7 @@ record BlockStructure : Type₁ where
       headerSize      : BHeader → ℕ -- size of a block header
       slotToSeed      : Slot → Seed -- big-endian encoding of the slot number in 8 bytes
       prevHashToNonce : Maybe HashHeader → Nonce
-      serHashToℕ      : SerHash → ∃[ n ] n < 2 ^ 512 -- [0, 2^512) (64-byte VRF output)
+      serHashToℕ      : SerHash → Certifiedℕ
       serHashToNonce  : SerHash → Nonce
 \end{code}
 \end{AgdaAlign}

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

@@ -93,15 +93,15 @@ data
 \begin{figure*}[h]
 \emph{Protocol helper functions}
 \begin{code}
-hBLeader : BHBody → ∃[ n ] n < 2 ^ 512 -- [0, 2^512)
+hBLeader : BHBody → Certifiedℕ
 hBLeader bhb = serHashToℕ (hash (encode "L" ∥ encode vrfRes))
   where open BHBody bhb
 
 hBNonce : BHBody → Nonce
 hBNonce bhb = serHashToNonce (hash (encode "N" ∥ encode vrfRes))
   where open BHBody bhb
 
-checkLeaderVal : ∃[ n ] n < 2 ^ 512 → PosUnitInterval → ℚ → Type
+checkLeaderVal : Certifiedℕ → PosUnitInterval → ℚ → Type
 checkLeaderVal (certℕ , certℕprf) (f , posf , f≤1) σ =
    if f ≡ 1ℚ then ⊤ else λ{f≢1ℚ} →
      let